Hello, I am interested in using Yosys for SystemVerilog Assertions(SVA) based designs. However, I have some confusion about the extent of support available.
Does the Yosys version support SystemVerilog assertions at all? Do I need to use SBY(TabbyCAD license) for any kind of SVA feature?
The Yosys docs describe the features supported in the open source (read_verilog) front end, Non-standard or SystemVerilog features for formal verification. This allows for SVA-style immediate assertions, but not concurrent assertions or the richer SVA syntax. The getting started guide for SBY has an example of this. It is possible to implement the necessary state machines to achieve the same functionality, but if you want full SVA support you do need a TabbyCAD license.
1 Like