tmeissner/formal_hw_verification - formal_hw_verification - goodcleanfun Gitea

Trying to verify Verilog/VHDL designs with formal methods and tools

vhdl verilog assertions formal yosys systemverilog sva

20 lines

252 B

Raw Normal View History

Add simple VAI register file as base to try to formal verify FSM designs

5 years ago

smtbmc error test case 1

5 years ago

Add simple VAI register file as base to try to formal verify FSM designs

5 years ago

smtbmc error test case 2 solution (using --nomem)

5 years ago

smtbmc error test case 2

5 years ago

Add simple VAI register file as base to try to formal verify FSM designs

5 years ago

[options]
depth 30
wait on
mode prove
#mode bmc
#mode cover

[engines]
smtbmc --nomem
#abc pdr

[script]
verific -vhdl vai_reg.vhd
verific -formal properties.sv
verific -import -extnets -all vai_reg
prep -top vai_reg

[files]
vai_reg.vhd
properties.sv