[ImportVerilog] How to implement SVA in Moore?

[chenbo-again]

Hello fabian and hailong:
@fabianschuiki @hailongSun2000
I'm trying to implement SVA for moore, and the main problem is how to implement property and sequence for moore, I find that dialect LTL is a good choice to model SVA.

The main goal of the ltl dialect is to capture the core formalism underpinning SystemVerilog Assertions (SVAs), the de facto standard for describing temporal logic sequences and properties in hardware verification. (See IEEE 1800-2017 section 16 “Assertions”.) We expressly try not to model this dialect like an AST for SVAs, but instead try to strip away all the syntactic sugar and Verilog quirks, and distill out the core foundation as an IR. Within the CIRCT project, this dialect intends to enable emission of rich temporal assertions as part of the Verilog output, but also provide a foundation for formal tools built ontop of CIRCT.

I think it's a good choice to directly convert SVA to LTL and bypass Moore, we can saving out time and avoid to model sva property again.

[fabianschuiki]

SVA support in ImportVerilog would be absolutely amazing! 🥳 🚀

You could definitely try to directly lower to ops in the LTL` dialect. I'm not entirely sure if this will work, but it's worth experimenting with. Directly going to LTL is similar to directly emitting HW/Comb/Seq in ImportVerilog: it's theoretically possible, but SV has a very weird type system and semantics that make a direct conversion very complicated.

A few weird things in SVA are going to be annoying. One thing I remember are very strange clock inference rules for sequences and properties, where you have to traverse the AST to find a parent always @(*edge ...) construct, or a @(*edge ...) property, or a clocking block, or a default clocking block, to figure out what the clock for an LTL sequence is. LTL also has no concept of property and sequence declarations and reuse, variable capture, etc..

My guess is that you'll want to capture the SVAs in the Moore dialect pretty quickly, because there are going to be some impedance mismatches between the low-level nature of LTL and the craziness that is SystemVerilog. But you definitely don't have to start out with that 😃! Make sure to emit errors for all the SVA expressions and cases that are not supported 😃