yosys/manual/PRESENTATION_ExOth/equiv.ys

18 lines
512 B
Plaintext
Raw Normal View History

2014-06-21 09:33:33 -05:00
# read test design
read_verilog ../PRESENTATION_ExSyn/techmap_01.v
hierarchy -top test
# create two version of the design: test_orig and test_mapped
copy test test_orig
rename test test_mapped
# apply the techmap only to test_mapped
techmap -map ../PRESENTATION_ExSyn/techmap_01_map.v test_mapped
2015-08-14 03:56:05 -05:00
# create a miter circuit to test equivalence
2014-06-21 09:33:33 -05:00
miter -equiv -make_assert -make_outputs test_orig test_mapped miter
flatten miter
2015-08-14 03:56:05 -05:00
# run equivalence check
2014-06-21 09:33:33 -05:00
sat -verify -prove-asserts -show-inputs -show-outputs miter