I have an assertion to check signal ‘b’ is stable between two events in which one is signal ‘a’ going low and other is signal ‘c’ going high.These signals are not clock dependent. whenever a triggers, this needs to be checked.
Please correct my assertion below
assert1: assert property (@(negedge a) (b) |-> (b throughout c[->1]));
But the above assertion is starting but remained as unfinished, eventhough Iam seeing c is going high. Please let me know what is the reason and how can I modify it? And also I need to display error if its not stable?
In reply to Anudeep J:
SVA relies on clocking events, typically a clock. Thus, the following is correct
assert1: assert property (@(posedge clk) $fell(a) |-> (b throughout c[->1]));
// Also, "stable" is defined as
// $stable returns true if the sampled value of the expression did not change between the
// sampled value at the previous cycle and the sampled value at the current cycle.
// Otherwise, it returns false. Thus,
assert_stable: assert property (@(posedge clk) ##1 $fell(a) |->
($stable(b) throughout c[->1]));
However, what you want is something that is asynchronous. For that, I suggest the use of tasks with fork/join_any. For example:
task automatic t1();
bit fail;
fork
begin : check_stable
@(b) fail=1;
end : check_stable
begin : at_end
@(posedge c);
end : at_end
join_any
assert(!fail) else $display("b is unstable %t", $realtime);
endtask
initial
forever @(negedge a) t1();
In reply to ben@SystemVerilog.us:
Hi Ben,
What is the use of ##1, in the above property? Isn’t that just moving the assertion success just clock ahead?
$stable(b) requires information about the previous sampling cycle. In the very first cycle, the previous sample value is its default or initial value.
This can yield an unexpected error.
Isn’t that just moving the assertion success just clock ahead?
No; $fell(a) is sampled in cycle 2, 3, 4,
NOTE:$fell(a) is not sampled in cycle 1.
Without that ##1, $fell(a) is sampled in cycle 1, 2, 3, 4,…
I came accross this thread and I was wondering shouldn’t we have disable fork; just after join any in your example for asynchronous check. With disable fork, we will avoid assertion failure after the @(posedge c) occurrance.
*In reply to ben@SystemVerilog.us:*I was wondering shouldn’t we have disable fork; just after join any in your example for asynchronous check. With disable fork, we will avoid assertion failure after the @(posedge c) occurrence.
If @(b) occurs in the same time step as @(c) then you would have an assertion failure.
The question then is: Should that be a failure? But in any case, after the join_any
we test for the fail task variable. This is s join_any. If you put the disable fork; just after join any then you would not test the assertion. Maybe you are suggesting the following instead.
assert1: assert property (@(posedge clk) $fell(a) |-> (b throughout c[->1]));
// Also, "stable" is defined as
// $stable returns true if the sampled value of the expression did not change between the
// sampled value at the previous cycle and the sampled value at the current cycle.
// Otherwise, it returns false. Thus,
assert_stable: assert property (@(posedge clk) ##1 $fell(a) |->
($stable(b) throughout c[->1]));
However, what you want is something that is asynchronous. For that, I suggest the use of tasks with fork/join_any. For example:
task automatic t1();
// bit fail;
fork
begin : check_stable
@(b) assert(!fail) else $display("b is unstable %t", $realtime);
// fail=1;
return; // maybe disable fork?
end : check_stable
begin : at_end
@(posedge c);
end : at_end
join_any
// assert(!fail) else $display("b is unstable %t", $realtime);
endtask
initial
forever @(negedge a) t1();
You are right, I missed the part with assertion test after the join any. And yes, we are usually doing assertion testing inside fork/join_any boundery (begin : check_stable … end : check_stable in your example.).