SystemVerilog Assertions: There should be maximum two requests in 10 clock cycles

SystemVerilog
,
1

Hello,
I have written the following assertion for the above mentioned statement,

module assertions(clk,req,done,start);
input bit clk;
input bit req;
input bit done;
input bit start;

default clocking cb @(posedge clk); endclocking
**
property should_be_max_two_requests_in_ten_cycles(cb,sig0,sig1,sig2);
@(cb) (sig0 ##1 sig1[=2] ##1 sig2) within 1’b1[*10];
endproperty: should_be_max_two_requests_in_ten_cycles

ASSERTION_2_label: assert property (should_be_max_two_requests_in_ten_cycles(cb,start,req,done))
$display(“time=%2t: {A2}Two requests in ten cycles”, $time);
else $error(“time=%2t: {A2}One or more than two requests in ten cycles”, $time);**
endmodule

Testbench:
module testbench();
bit clk, req, done,start;

assertions A (.*);

initial forever clk= #5 ~clk;

bit [1:0] req_count;

initial begin
$vcdpluson();
req = 0;
done = 0;
start = 0;
#2 start = 1;;
for (int i=0;i<10;i++) begin
#10;
req = $urandom_range(0,1);
if (req == 1’b1) req_count++;
if (req_count > 2’b10) done = 1;
end
#100; $finish;
end

endmodule
When tested against various testcases, the assertion fails to through error when there are more than two requests in 10 cycles. I am unsure about the non-consecutive repetition that I used.
Can anyone help me in fixing this.
Thank You.

Regards,
Ramakrishna Melgiri

2

In reply to Ramakrishna Melgiri:

A quick, untested variant - for you to try:


property should_be_max_two_requests_in_ten_cycles(cb,sig0,sig1,sig2);
@(cb)	(sig0 |=> (sig1[->2] ##1 sig2) within 1'b1[*10];
endproperty:	should_be_max_two_requests_in_ten_cycles

You will need to fix the braces and perhaps the within operator’s applicability etc.

Am glad you are using a simple, unit test to verify this assertion. We will be demonstrating a similar concept with SVA examples and the unit tests shall be in Go2UVM framework. We will also use SVUnit’s UVM Report mock to expect/unexpect error. Stay tuned to DVCon India for the slides/paper.

Srini
www.go2uvm.org

3

In reply to Srini @ CVCblr.com:

Hello Srini,
Thank you for the reply.
I tried making changes to the property as you’ve shown, yet the assertion is supposed to fail when there are more than two requests in 10 cycle period but I’m unable to keep track of req signal after two req have been made.
The logic I wrote works like this:
After two req signals, the Non-consecutive operator waits for done bit (I’m changing done bit to 1 once I count 10 cycles from start - modified testbench) But, the Non-consecutive operator does not fail when there are more than 2 requests seen. I hope you understand the mistake that’s going on here.

Regards,
Ramakrishna Melgiri