aboutsummaryrefslogtreecommitdiffstats
path: root/examples/aiger/demo.v
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2016-12-01 13:42:17 +0100
committerClifford Wolf <clifford@clifford.at>2016-12-01 13:42:17 +0100
commit105b6374ae8d8f3892f907ca61bb62d35b8d7d4d (patch)
tree6455eede1117cd95344ac0698b27f7e9580b4588 /examples/aiger/demo.v
parent88b9733253c587eba45d488355e73f1879091fff (diff)
downloadyosys-105b6374ae8d8f3892f907ca61bb62d35b8d7d4d.tar.gz
yosys-105b6374ae8d8f3892f907ca61bb62d35b8d7d4d.tar.bz2
yosys-105b6374ae8d8f3892f907ca61bb62d35b8d7d4d.zip
Added examples/aiger/
Diffstat (limited to 'examples/aiger/demo.v')
-rw-r--r--examples/aiger/demo.v12
1 files changed, 12 insertions, 0 deletions
diff --git a/examples/aiger/demo.v b/examples/aiger/demo.v
new file mode 100644
index 000000000..bb54ba4ef
--- /dev/null
+++ b/examples/aiger/demo.v
@@ -0,0 +1,12 @@
+module demo(input clk, reset, ctrl);
+ localparam NBITS = 10;
+ reg [NBITS-1:0] counter;
+ initial counter[NBITS-2] = 0;
+ initial counter[0] = 1;
+ always @(posedge clk) begin
+ counter <= reset ? 0 : ctrl ? counter + 1 : counter - 1;
+ assume(counter != 0);
+ assume(counter != 1 << (NBITS-1));
+ assert(counter != (1 << NBITS)-1);
+ end
+endmodule