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