Hi!
I have an problem to solve.
If signal A is asserted then signal B should repeats for exact n times (no more no less) until signal A is asserted.
I have written next assertion for this:
localparam n = 5;
wire A, B, C;
assert property(
@(posedge clk) disable iff (!rstn)
$rose(A) |-> B[=n] ##1 !A
);
And now I want add some condition: if signal C is negated the assertion should be stopped. Because this signal disable functionality that I want to check
And now I have 2 possible ways:
localparam n = 5;
wire A, B;
// First way path C to disable block
assert property(
@(posedge clk) disable iff (!rstn | !C)
$rose(A) |-> B[=n] ##1 !A
);
// Second way create sequence that will finish assertion using "or"
assert property(
@(posedge clk) disable iff (!rstn)
$rose(A) |-> B[=n] ##1 !A or seq_c_neg
);
Can you clarify the difference between this a approaches. As I understand it depends on how I want to finish assertion. In the first way I disable the whole assertion and in the second I finish my assertion with fail of pass. Is it correct?
P.S I don’t know how to write correctly seq_c_neg. I will ask it in another question.