Assert Property disable iff not fully converted to Verilog

[HakamAtassi]

Hello!

I'm using sv2v to convert chisel generated SV code to V for use with Symbiyosys.

Currently, the way chisel generates assertions is through:

import chisel3.ltl._
AssertProperty(/*property*/)

which generates something like:

wire hasBeenReset = hasBeenResetReg === 1'h1 & reset === 1'h0;
  wire disable_0 = ~hasBeenReset;
  assert property (@(posedge clock) disable iff (disable_0) _GEN);
  wire disable_2 = ~hasBeenReset;
  assume property (@(posedge clock) disable iff (disable_2) _GEN);

which sv2v then converts the following verilog via the command ../../sv2v/bin/sv2v bru.sv -E assert -w=test.v:

assert property (@(posedge clock) disable iff (disable_0)
	_GEN
) ;
wire disable_2 = ~hasBeenReset;
assume property (@(posedge clock) disable iff (disable_2)
	_GEN
) ;

which unfortunately causes yosys to complain:

SBY  3:04:26 [test_bmc] base: test.v:129: ERROR: syntax error, unexpected '@'
SBY  3:04:26 [test_bmc] base: finished (returncode=1)
SBY  3:04:26 [test_bmc] base: task failed. ERROR.

If I had to guess what is happening here, I would assume the "-E assert" causes the entire assert block to be excluded, leaving its content unchanged, while not using -E assert causes the assert to just be "optimized out".

[punzik]

Hi! Yosys, and thus it sby, does not support SVA, so it does not understand such asserts. To support SVA you need a commercial parser from Verific, which is included in the paid TabbyCad distribution.

[zachjs]

There are a few different confusions here (my fault):

1. Though the first sentence in the readme already states sv2v has "an emphasis on supporting synthesizable language constructs", this may not make it clear that some non-synthesizable constructs are supported by the frontend but aren't themselves converted to Verilog (though, e.g., expressions they contain are still elaborated).
2. The -E/--exclude is confusingly named. More clear might be --exclude-conversion-pass or --disable-the-conversion-of. -E logic, for example, doesn't exclude logic from the output. Instead, it disables the conversion of logic into reg or wire by the logic conversion pass in Logic.hs. So by default, there should be no logic in the output, but the user can specify -E logic to disable this conversion if they know the downstream tool supports logic natively.
3. This is confusing for assertions, where the "conversion" pass in Assert.hs actually just removes assertions because they aren't synthesizable (and ought to be side-effect free). -E assert, then, disables this removal, leaving assertions in the output. This feature potentially allows targeting Symbiyosys, but indeed many high-level SV assertion features like disable iff aren't converted by sv2v and may not be supported by downstream tools.

As sv2v is mainly intended for synthesis flows, I don't have immediate plans to add more advanced elaboration of assertions. However, I would be happy to accept contributions in this vein and to learn more about community interest in this feature.