Search code examples
yosys

What are yosys formal capabilities with verific?

I'm trying to use Yosys formal verification capabilities along with Verific parser.

What are the supported capabilities of yosys with verific for formal verification, compared to the "read_verilog -formal" command? For example, a quick compilation of formal code that works with read_verilog gave me an error for "assume property" syntax: "The sva directive is not sensitive to a clock. Unclocked directives are not supported"

I'm not sure if I should modify the Verific library flags in any way to make it support more capabilities, or it's something that is not supported.

Solution

  • Currently Yosys only has very limited support for SVA with or without Verific. However, we plan on vastly extending the Yosys support for SVA via Verific in the near future. The goal is to provide pretty much complete support for everything Verific can parse.

    Regarding the "The sva directive is not sensitive to a clock. Unclocked directives are not supported" error message: That's a Verific error message and I don't think there is a Verific library flag to bypass it. (But I'm not sure.) Technically unclocked properties are not part of the SystemVerilog standard afaik. (The syntax would allow it, but the standard text does not define a semantic for it.)

    Yosys supports unclocked SVA properties. (But only trivial expression properties.)

    Both Verific and Yosys do support immediate assertions and assumptions. (That is assertions and assumptions in always blocks.) Right now this is the thing I recommend for most cases where people write new properties, also because most simulators have better support for immediate assertions (or it would be easier to add if the support is missing so far).

    Right now I'd say the biggest advantage of using Verific with Yosys is support for non-SVA System Verilog (and VHDL) code. In a few months we will hopefully have support for much more SVA constructs via Verific, but that isn't implemented yet.

    Edit/Update: SVA support via Verific is slowy improving now. See this directory for examples that can be processed via Verific. New examples are added as new features are added to the Verific bindings. Currently counter.sv is the most advanced example there.