[formal] Opentitan FPV using Symbiyosys

lowRISC / opentitan

OpenTitan: Open source silicon root of trust

https://www.opentitan.org

Apache License 2.0

2.5k stars 745 forks source link

[formal] Opentitan FPV using Symbiyosys #1263

Open cindychip opened 4 years ago

cindychip commented 4 years ago

This is a tracking bug. Comment if you have suggestions or updates

Symbiyosys currently support limited functionalities for FPV methodology.

Yosys

Symbiyosys uses Yosys to synthesize SV. Current list of unsupported Yosys syntax is listed in the link here.

[ ] Use util/syn_yosys.sh to convert SV file to Verilog.

Symbiyosys

Symbiyosys has been adding supports for FPV related syntax. Here are the list of supported syntax

Still exploring:

[ ] Symbolic variable
[ ] Code and COI coverages
[ ] Import a filelist in .sby file

imphil commented 4 years ago

Note that https://symbiyosys.readthedocs.io/en/latest/verific.html#supported-sva-property-syntax is talking about the Verific bindings, which are not part of the open source offering. I'm not sure what syntax is supported without Verific, the documentation is slightly confusing to me in that respect.

cindychip commented 4 years ago

Hi Phillip,

Thank you for pointing this out. I did not realize that Verific is not part of the OpenSource. Here are some discussion about Symbiyosys support SV in Verific. Link I tried locally and I do not think SymbiYosys without Verific can support bind. Other than that, seems like most of the unsupported items have some workarounds. Not supporting bind is definitely a limitation, but SymbiYosys still can potentially use it to test assertions written within the RTL file.