tests/sat/counters.ys - third_party/yosys - Git at Google


 read_verilog counters.v
 proc; opt

 expose -shared counter1 counter2
 miter -equiv -make_assert -make_outputs counter1 counter2 miter

 cd miter; flatten; opt
 sat -verify -prove-asserts -tempinduct -set-at 1 in_rst 1 -seq 1 -show-inputs -show-outputs

	read_verilog counters.v
	proc; opt

	expose -shared counter1 counter2
	miter -equiv -make_assert -make_outputs counter1 counter2 miter

	cd miter; flatten; opt
	sat -verify -prove-asserts -tempinduct -set-at 1 in_rst 1 -seq 1 -show-inputs -show-outputs