In reply to a72:
In reply to shashankvm:
Hello Shashank,
Thanks for presenting a solution. I have a question though. Please correct me, if I am missing something.
Let us assume, that there is no ACK in the first 5 clocks of the 10 clock window. Your shift register would be empty (no '1’s in the register). Your continuous assignment will show count_ack_in_window to be ‘0’ (zero). But the assertion keeps firing every posedge clock and for the first five clocks, it will keep failing because count_ack_in_window is zero. The requirement is to see how many ACKs have arrived ‘over’ the 10 clock period and then report a failure/pass. Wait for the 10 clock window to occur and then count # of ACKs over that 10 clock window and then check for pass/fail.
Right, we can add a counter to count the number of cycles, then enable the assertion only if the 10 cycles have passed.
I ran it in a Formal tool and verified the property by Ben is equivalent to the below one:
module count_ack(input logic clk, reset, ack);logic [9:0] serial_shift_reg;
logic [2:0] count_ack_in_window;
logic [3:0] count_cycle;
logic count_ten_cycle;
always_ff @(posedge clk or posedge reset)
if (reset) begin
serial_shift_reg <= 'b0;
count_cycle <= 'b0;
count_ten_cycle <= 'b0;
end else begin
count_cycle <= count_cycle + 1;
serial_shift_reg <= serial_shift_reg << 1;
count_ten_cycle <= (count_cycle == 4’b1001) ? 1 : count_ten_cycle;
if (ack)
serial_shift_reg[0] <= 1’b1;
end
assign count_ack_in_window = $countones(serial_shift_reg);
assume property (@(posedge clk) disable iff (reset) ack[=1:3] intersect 1[*10]);
assert property (@(posedge clk) disable iff (reset) count_ten_cycle |-> ((count_ack_in_window >= 1) and (count_ack_in_window <= 3)));
endmodule