1 files changed, 19 insertions, 0 deletions
diff --git a/examples/smtbmc/demo1.v b/examples/smtbmc/demo1.v
new file mode 100644
index 00000000..567dde14
--- /dev/null
+++ b/examples/smtbmc/demo1.v
@@ -0,0 +1,19 @@
+module demo1(input clk, input addtwo, output iseven);
+	reg [3:0] cnt;
+	wire [3:0] next_cnt;
+
+	inc inc_inst (addtwo, iseven, cnt, next_cnt);
+
+	always @(posedge clk)
+		cnt = (iseven ? cnt == 10 : cnt == 11) ? 0 : next_cnt;
+
+`ifdef FORMAL
+	assert property (cnt != 15);
+	initial assume (!cnt[2]);
+`endif
+endmodule
+
+module inc(input addtwo, output iseven, input [3:0] a, output [3:0] y);
+	assign iseven = !a[0];
+	assign y = a + (addtwo ? 2 : 1);
+endmodule