aboutsummaryrefslogtreecommitdiffstats
path: root/examples/smtbmc/demo1.v
blob: 59e4978251e049b1923e1e954149efe28af1b350 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
module demo1(input clk, input addtwo, output iseven);
	reg [3:0] cnt = 0;
	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;
	
	assert property (cnt != 15);
	// initial expect ((iseven && addtwo) || cnt == 9);
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