The following scenario should give errors as assertions should be violated (on purpose). But, the check is extending from one “run” to the next, and the assertion is being checked as valid.
I’ve used $rose(valid) so that the assertion begins only when valid has asserted HIGH, not for every clock cycle it finds valid to be high. Is there a better way to do this?? as this makes the assertion start at 20ns, while valid was asserted HIGH at 10ns.
module assertions_1;
bit valid, ready, clk;
always #5 clk = ~clk;
initial begin
repeat (5) run();
repeat (5) begin @(negedge clk);
end
$finish;
end
task run();
@(negedge clk) valid = 1;
repeat ($urandom_range(1,4)) begin
@(negedge clk);
end
ready = 1;
@(negedge clk) ready = 0; valid = 0;
endtask
property RUN;
@(negedge clk) $rose(valid) |-> valid ##[6:10] $stable(valid) && ready;
endproperty
assert property(RUN) $display($time, "ns Signal Transition is ok");
else $error($time, "ns Signal Transition has Issues");
endmodule
You need the $rose(valid). I don’t see any issue with your assertion. On your TB, I prefer to use nonblocking assignments as a style, though the model would work.
$rose(valid) |-> valid // at $rose(valid) valid==1, thus the valid in the consequent is not needed
task run();
@(negedge clk) valid <= 1;
// the valid=1 works because signals are sampled and
// use the values of the Preponed region of the time stamp.
repeat ($urandom_range(1,4)) begin
@(negedge clk);
end
ready <= 1;
@(negedge clk) ready <= 0; valid <= 0;
endtask
property RUN;
@(negedge clk) $rose(valid) |-> ##[6:10] $stable(valid) && ready;
endproperty
By saying you don’t want the assertion checking “from one “run” to the next”, I think you want this to fail if valid falls and ready has not been asserted. I think you might look to see if this meets your needs:
Thank You Mr. Dave,
This was what I was looking for.
But there remains an issue, I made slight changes, so that ready triggers, 4 to 7 clocks cycles after valid is HIGH. And the assertion will pass for when ready is triggered 6:10 cycles after valid.
In reply to dave_59:
Also, in case of $rose(valid) will start the assertion the next clock after the valid has actually gone HIGH. While stating only “valid” starts the assertion on every negative clock edge it finds valid to be HIGH.
Is there any way to start the assertion on exactly the time valid has gone HIGH and only then not every time the edge finds valid HIGH??
Write assertion for signal “B” will be low after the start bit becomes high within the range of [4:15] clock cycles. “B” will be high at posedge of “A” till this time “B” should be low. See the below diagram for reference.
I guess this will satiate your requirement. I am unsure whether I should use first_match over here cause I am assuming the tool will automatically defenestrate other possible scenarios.
property check_b ;
start && b && !a|-> ##[4:15] !b ;
endproperty
property check_a_b ;
start && a |-> b ;
endproperty
property check_a_b ;
start && a && $fell(b) |-> what will happen to a ? ;
endproperty
