The problem statement is pretty straight forward. But I am not able to come up with an elegant solution.
Problem Statement:
Write an assertion to check that in a Sliding window of 10 clks, there should be 1 to 3 acks(at least 1 ack and at most 3 acks). If there are more than 3 acks within the 10 clocks window, the assertion should fail. If there is not at least 1 ack, the assertion should fail.
I tried with ‘throughout’, ‘intersection’ but no luck. So, I tried with local variables but it did not work. I am not able to figure out how to check for a condition ‘over’ 10 clocks.
Tried the following, but the #[1:10] does not seem correct. This solution did not work.
int ack_cnt;
always @(posedge clk) begin
if (ack) ack_cnt = ack_cnt+1;
end
In reply to a72:
The following should work.
*(ack[=3] intersect 1[10]) says at every attempt (every posedge clk) there should be for that attempt 3 not necessarily contiguous occurrences of ack with 10 cycles starting from that attempt. Edit code - EDA Playground
module m;
bit clk, ack;
always #5 clk=!clk;
/* Problem Statement:
Write an assertion to check that in a Sliding window of 10 clks, there should be 1 to 3 acks(at least 1 ack and at most 3 acks). If there are more than 3 acks within the 10 clocks window, the assertion should fail. If there is not at least 1 ack, the assertion should fail. */
int ack_cnt;
always @(posedge clk) begin
if (ack) ack_cnt = ack_cnt+1;
end
ap_3ack_in10clk: assert property(@(posedge clk)
ack[=3] intersect 1[*10]);
initial begin
$dumpfile("dump.vcd"); $dumpvars;
repeat(30) begin
@(posedge clk);
randomize(ack);
end
$finish;
end
endmodule
I prefer using auxiliary code for this. Here is my method:
Create a serial shift register having depth of 10, that shifts right by 1 on every cycle. On a given cycle if ack is HIGH, insert a 1 to the leftmost end of the shift register. The count of acks in the register, at any given cycle should be at least 1 and at most 3.
logic serial_shift_reg[0:9];
logic count_ack_in_window;
always_ff @(posedge clk or posedge reset)
if (reset)
serial_shift_reg <= 'b0;
else begin
serial_shift_reg <= serial_shift_reg >> 1;
if (ack)
serial_shift_reg[0] <= 1'b1;
end
assign count_ack_in_window = $countones(serial_shift_reg);
assert property (@(posedge clk disable iff reset) (count_ack_in_window >= 1) and (count_ack_in_window <= 3));
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.
In reply to shashankvm:
There is a saying all roads lead to Rome.
Sliding window: It is interesting that for this problem I see a pattern testing moving through time.
(ack[=1:3] intersect 1[*10]) is a sliding window where in any future slice of 10 bit I check for 3 not necessarily consecutive 3 ack. Thus,
at t100 I look for 3 ack from t100 thru t109.
at t101 I look for 3 ack from t101 thru t110.
Fixed window: Your solution is time moving thru a fixed slice searching for a pattern. Essentially, it’s a fixed window (serial_shift_reg[0:9]) and shift in time the ack.
Your solution as written has an issue with the very first 2 cycles and possibly the first 9 cycles with an initial sequence of ack 1 1 0 0 0 0 0 0 0 1.
Also, to solve this you have 2 solutions:
I generally try to avoid support logic unless I have to.
see my paper on SUPPORT LOGIC AND THE ALWAYS PROPERTY http://systemverilog.us/vf/support_logic_always.pdf
Your solution could have been written as:
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:
In reply to shashankvm:
There is a saying all roads lead to Rome.
Sliding window: It is interesting that for this problem I see a pattern testing moving through time.
(ack[=1:3] intersect 1[*10]) is a sliding window where in any future slice of 10 bit I check for 3 not necessarily consecutive 3 ack. Thus,
at t100 I look for 3 ack from t100 thru t109.
at t101 I look for 3 ack from t101 thru t110.
Fixed window: Your solution is time moving thru a fixed slice searching for a pattern. Essentially, it’s a fixed window (serial_shift_reg[0:9]) and shift in time the ack.
Your solution as written has an issue with the very first 2 cycles and possibly the first 9 cycles with an initial sequence of ack 1 1 0 0 0 0 0 0 0 1.
Also, to solve this you have 2 solutions:
I generally try to avoid support logic unless I have to.
see my paper on SUPPORT LOGIC AND THE ALWAYS PROPERTY http://systemverilog.us/vf/support_logic_always.pdf
Your solution could have been written as:
In reply to shashankvm:
The intersect is like an envelope input to an AND hardware gate to enable the other input to pass thru to the output. It defines a block of cycles, and to me, it is very visual.
Because there is an attempt at every cycle and because the failure is detected when it occurs, you can have more than 1 failure in a time stamp and that can be confusing.I am very sure that the code meets the requirements.
[You] “I ran it in a Formal tool and verified the property by Ben is equivalent to the below one”
In reply to shashankvm:
The intersect is like an envelope input to an AND hardware gate to enable the other input to pass thru to the output. It defines a block of cycles, and to me, it is very visual.
Because there is an attempt at every cycle and because the failure is detected when it occurs, you can have more than 1 failure in a time stamp and that can be confusing.I am very sure that the code meets the requirements.
[You] “I ran it in a Formal tool and verified the property by Ben is equivalent to the below one”
Ben
Now I got it why the ap_2 assertion is failing. The “(count_ack_in_window >= 1) && (count_ack_in_window <= 3)” is a Boolean expression so it is a sequence of length 1. The 1[*10] has length 10, so these 2 can never intersect, i.e. start and end at the same cycle.
// With my assertion, because of the (1, ..)[*10] I am repeating the shift of ack into a
// local variable , and then test for the count
property p_acks_in10;
bit[0:9] serial_shift_reg=0;
@(posedge clk) disable iff(reset)
(1, serial_shift_reg = {ack, serial_shift_reg[0:8]})[*10] ##0
$countones(serial_shift_reg) >=1 && $countones(serial_shift_reg) <=3;
endproperty
// With your assertion
int local_var;
($rose(ack), loval_var=1) |=> ($rose(ack),...) [*9]
// you are asserting that rose(ack) must occur at every cycle, and if it does not
// then the assertion fails. Also, why the rose?
// This should work
property ack_cnt;
int local_var;
($rose(ack), loval_var=0) |-> // counting the acks
(1, local_var = local_var+ack)[*10] ##0 (local_var >= 1) && (local_var <= 3)
endproperty
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.