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

11 lines

205 B

Raw Permalink Normal View History

Making counter design work with GHDL synthesis * Remove unused SVA properties file * Makefile optimizations * Use prep auto-top option to prevent error with not founded top-level module when using generics * Add some simple PSL assertions

4 years ago

Add counter as example for initial reset problems

6 years ago

DUT := counter

.PHONY: cover bmc prove all clean

all: cover bmc prove

cover bmc prove: ${DUT}.vhd symbiyosys.sby
	sby --yosys "yosys -m ghdl" -f -d work/${DUT}-$@ symbiyosys.sby $@

clean:
	rm -rf work