summaryrefslogtreecommitdiff
path: root/tests/sat/counters-repeat.ys
diff options
context:
space:
mode:
Diffstat (limited to 'tests/sat/counters-repeat.ys')
-rw-r--r--tests/sat/counters-repeat.ys10
1 files changed, 10 insertions, 0 deletions
diff --git a/tests/sat/counters-repeat.ys b/tests/sat/counters-repeat.ys
new file mode 100644
index 00000000..b3dcfe08
--- /dev/null
+++ b/tests/sat/counters-repeat.ys
@@ -0,0 +1,10 @@
+
+read_verilog counters-repeat.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
+