forked from tanchou/Verilog
49 lines
1.3 KiB
Systemverilog
49 lines
1.3 KiB
Systemverilog
`default_nettype none
|
|
|
|
module counter_formal (
|
|
input wire clk, // global clock
|
|
input wire reset, // synchronous reset signal
|
|
(*anyseq*) input wire en, // enable signal
|
|
input wire strobe, // output strobe
|
|
input wire [counter.WIDTH-1:0] counter_reg
|
|
|
|
);
|
|
|
|
`ifdef VERIFIC
|
|
internal_check: assert property (@(posedge clk)
|
|
disable iff (reset)
|
|
en && (counter_reg==11)|=>(counter_reg==10)) ;
|
|
|
|
decrease_enable_check: assert property (@(posedge clk)
|
|
disable iff (reset || !en)
|
|
(counter_reg >0 ) |=> (counter_reg == $past(counter_reg) - 1));
|
|
|
|
roll_enable_check: assert property (@(posedge clk)
|
|
disable iff (reset || !en)
|
|
(counter_reg == 0 ) |=> (counter_reg == counter.INITIAL_VALUE));
|
|
|
|
max_value_assert_check: assert property (
|
|
@(posedge clk)
|
|
(counter_reg <= counter.INITIAL_VALUE)
|
|
);
|
|
|
|
cover_0: cover property(
|
|
@(posedge clk)
|
|
(counter_reg == 0)
|
|
);
|
|
|
|
cover_2stb: cover property(
|
|
@(posedge clk)
|
|
(strobe == 1) |-> ##[+] (strobe == 1)
|
|
);
|
|
|
|
|
|
`endif
|
|
|
|
endmodule
|
|
|
|
bind counter counter_formal counter_f_inst(.*);
|
|
|
|
|
|
//testing: assert property (@(posedge clk)(counter_reg==111)|=>(counter_reg==10));
|