mirror of https://github.com/YosysHQ/yosys.git
18 lines
461 B
Coq
18 lines
461 B
Coq
|
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
|