aboutsummaryrefslogtreecommitdiffstats
path: root/examples/smtbmc/demo1.v
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2016-09-02 13:54:24 +0200
committerClifford Wolf <clifford@clifford.at>2016-09-02 13:54:24 +0200
commit068d5bc02ffea9ba627bbf7151fdb36500eae0f2 (patch)
treea92a035176090941205a653bbe3b93c50073f2e8 /examples/smtbmc/demo1.v
parent948aac9e1eaed04aa8de08e62cfb078d6337e9c9 (diff)
downloadyosys-068d5bc02ffea9ba627bbf7151fdb36500eae0f2.tar.gz
yosys-068d5bc02ffea9ba627bbf7151fdb36500eae0f2.tar.bz2
yosys-068d5bc02ffea9ba627bbf7151fdb36500eae0f2.zip
Made examples/smtbmc/demo1.v more interesting
Diffstat (limited to 'examples/smtbmc/demo1.v')
-rw-r--r--examples/smtbmc/demo1.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/examples/smtbmc/demo1.v b/examples/smtbmc/demo1.v
index d9be41513..567dde148 100644
--- a/examples/smtbmc/demo1.v
+++ b/examples/smtbmc/demo1.v
@@ -9,7 +9,7 @@ module demo1(input clk, input addtwo, output iseven);
`ifdef FORMAL
assert property (cnt != 15);
- initial assume (!cnt[3] && !cnt[0]);
+ initial assume (!cnt[2]);
`endif
endmodule