synlig
synlig copied to clipboard
read_systemverilog `-formal` support
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?