summaryrefslogtreecommitdiff
path: root/manual/PRESENTATION_ExOth/equiv.ys
diff options
context:
space:
mode:
Diffstat (limited to 'manual/PRESENTATION_ExOth/equiv.ys')
-rw-r--r--manual/PRESENTATION_ExOth/equiv.ys17
1 files changed, 17 insertions, 0 deletions
diff --git a/manual/PRESENTATION_ExOth/equiv.ys b/manual/PRESENTATION_ExOth/equiv.ys
new file mode 100644
index 00000000..09a4045d
--- /dev/null
+++ b/manual/PRESENTATION_ExOth/equiv.ys
@@ -0,0 +1,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