blob: 567dde1483e9307cd188bbb31875c8045da9e294 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
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
|
