summaryrefslogtreecommitdiff
path: root/manual/PRESENTATION_ExOth/equiv.ys
blob: 09a4045db4d9f50c9f957eb0738de1f117bb74b0 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
# 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

# create a miter circuit to test equivialence
miter -equiv -make_assert -make_outputs test_orig test_mapped miter
flatten miter

# run equivialence check
sat -verify -prove-asserts -show-inputs -show-outputs miter