aboutsummaryrefslogtreecommitdiffstats
path: root/tests/sat/counters.ys
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-02-06 01:00:11 +0100
committerClifford Wolf <clifford@clifford.at>2014-02-06 01:00:56 +0100
commit849fd62cfed9b6623865c7af76dd1bfbc6adf457 (patch)
tree3b745d082500ef0a54e6c4b14bc18c9f82636fb2 /tests/sat/counters.ys
parente915043144d52e2ff97e2b4638ed1af84426e359 (diff)
downloadyosys-849fd62cfed9b6623865c7af76dd1bfbc6adf457.tar.gz
yosys-849fd62cfed9b6623865c7af76dd1bfbc6adf457.tar.bz2
yosys-849fd62cfed9b6623865c7af76dd1bfbc6adf457.zip
Added counters sat test case
Diffstat (limited to 'tests/sat/counters.ys')
-rw-r--r--tests/sat/counters.ys10
1 files changed, 10 insertions, 0 deletions
diff --git a/tests/sat/counters.ys b/tests/sat/counters.ys
new file mode 100644
index 000000000..330895f82
--- /dev/null
+++ b/tests/sat/counters.ys
@@ -0,0 +1,10 @@
+
+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
+