I would like to implement a SystemVerilog assertion to check the following:
The clk must be active for at least two cycles during the assertion to zero of the reset signal.
I pasted my current solution below, but it is using an auxiliary fast clk, and has many limitations (including the ratio between the clk and the fast clk).
I was thinking about using variables inside of the property, but don’t know how to check for the number of clock pulses once the reset is deasserted.
My current solution:
sequence RESET_ASSERTED_THEN_RELEASED;
(!reset)[*1:$] ##1 reset;
endsequence
sequence CLK_PULSE;
!clk ##[1:20] clk[*1:20] ##[1:20] !clk;
endsequence
CLK_ACTIVE_DURING_RESET: assert property(@(posedge fastclk)
($past(reset) == 1'b1 && reset == 1'b0 |-> (CLK_PULSE ##1 CLK_PULSE) within (RESET_ASSERTED_THEN_RELEASED))
)
else $error("ERROR - clk didn't run at least 2 cycles after the assertion of reset (at %d)", $time);
I’m also experimenting with something like this, but not sure if it is the right direction:
// Add the fast clk
// You can add an test
let n=20; // Am guessing at the 20, need to specify
property count_cycles;
int cnt;
@(posedge fastclk) ($fell(reset), cnt = 0 )|=>
first_match( (CLK_PULSE, ++cnt) [*0:$]
##1 (reset, $display("cnt:%d", cnt)))
##0 cnt >= n;
endproperty
Can this be solved without using an auxiliary faster clock?
Yes, by using fork-joine_none. Basically, you fire 2 tasks: a 2-clock task and a timeout task. If timeout, then failure. See my paper Understanding the SVA Engine, link below. Note that an assertion can be expressed in many forms; SVA is one way.
module top;
bit clk, reset;
let period=10ns;
initial forever #5 clk=!clk;
// <<<<<<<<<<<<<SEE my response for the correction >>>
always @(posedge clk) begin : b0 // SEE BELOW, THIS IS IN ERROR
// Should be
// always @(negedge reset) begin : b0
bit got_2clk, done;
if($fell(reset, @(posedge clk))) // IN ERROR, comment this out
begin : fall_reset
fork
begin : one
repeat(2) @(posedge clk);
got_2clk=1'b1;
done=1'b1;
end : one
begin : two
#(period*2 +1);
done=1'b1;
end : two
join_none
wait(done);
a_2clk: assert(got_2clk); // 2clk is active
got_2clk=1'b0;
done=1'b0;
end : fall_reset
end : b0
initial begin
#100;
$finish;
end
endmodule
Thanks for your reply.
I played around with your implementation but if I made no mistake, then it can’t catch that scenario when the reset gates the clk immediately: https://www.edaplayground.com/x/859J (I hope EDA Playground links are allowed)
This solution is dependent on the clk so it is supposed to ‘check itself’ somehow - that’s why I thought that it can’t be solved without an auxiliary clk.
In reply to spoiled rabbit:
Apologies for my mistake; it always helps to test the code :)
The concept is correct. Below is code that works OK.
Instead of detecting a $fell that relies on the clock, I used always @(negedge reset) begin : b0
/* https://verificationacademy.com/forums/systemverilog/assertion-counting-clock-cycles-during-reset-pulse */
module top;
bit clk, reset;
let period=10ns;
event eclk, eanalog;
initial forever #5 clk=!clk;
initial begin
$dumpfile("dump.vcd"); $dumpvars;
#0 reset = 1;
#100 reset = 0;
force clk = 0;
#500 release clk;
#0 reset = 1;
#100 $finish;
end
always @(negedge reset) begin : b0
bit got_2clk, done;
// if($fell(reset, @(posedge clk)))
begin : fall_reset
fork
begin : one
repeat(2) @(posedge clk);
got_2clk=1'b1;
done=1'b1;
-> eclk;
end : one
begin : two
#(period*2 +1);
done=1'b1;
->eanalog;
end : two
join_none
wait(done);
a_2clk: assert(got_2clk); // 2clk is active
got_2clk=1'b0;
done=1'b0;
end : fall_reset
end : b0
endmodule
Sim result
ASSERT: Error: ASRT_0301 testbench.sv(40): Immediate assert condition “a_2clk” FAILED at time: 121ns, scope: top
In reply to Srini @ CVCblr.com:
Srini, my co-author on many books, I like your sva solution. I should have thought of it. A minor comment, if reset stayed low all the time the assertion would not fail. The ‘s_eventually’ issue. The fork-join_none solution addresses that.
Ben systemverilog.us
Thank you very much, with this update it works flawlessly.
The concept is really brilliant - perfect example of thinking outside the box, I think I will make good use of it in the future.
I like your solution really much, it’s simple and elegant.
Unfortunately the motivation is not to ensure the reset length, but to make sure that a possible ongoing transfer finishes. Because of this I prefer Ben’s solution for the reason he mentioned.
In reply to spoiled rabbit:
FWIW, this concept was a derivation of of my modeling SVA with fork-join_none.
I strongly encourage you to read my paper
Understanding the SVA Engine, Verification Horizons - July 2020 | Verification Academy
It will give more insights into how SVA works, and that will help you write better SVA code.
BTW, that paper is just a model of SVA, it is NOT how vendors implement it, but still, it is of value particualrly if you want to write a concurrent assertion in a class (where SVA is illegal). If you have dynamic repeats and delays, see my package (link below).