synlig icon indicating copy to clipboard operation
synlig copied to clipboard

read_systemverilog `-formal` support

Open ollie-etl opened this issue 2 years ago • 8 comments

My appologies if i've missed this in the docs, but I'm unable to use as a front end for formal verification

This just fine: bmc, prove and cover statements all run ok

read -sv -formal dataflow_formal.sv
read -sv -formal dataflow_id.sv
prep -top dataflow_id

This does not

verilog_defines -DFORMAL=1 -USYNTHESIS
read_systemverilog -defer dataflow_formal.sv
read_systemverilog -defer dataflow_id.sv
read_systemverilog -link
prep -top dataflow_id

Specifically, it runs the checks, but it has no invarients in bmc and prove, and no cover statements are covered. Everything is marked pass. What is the preferred way to replace read with read_systemverilog for driving formal verification?

ollie-etl avatar Nov 14 '22 11:11 ollie-etl