I am trying to write an assertion to check that signal b has only changed once btw rising edge of a and rising edge of c.
Somehow, the assertion below cannot guarantee that b has only changed once(1->0->1). In other words, even b changes twice, the assertion below will still pass rather than fail.
Can someone point me how to improve it?
module tb;
bit a, b, c;
bit clk;
always #1 clk = !clk;
//this assertion will PASS even b change more than once
//how to make it FAIL if b change(1->0->1) more than once?
property b_chg_once_ac_within(s, e, b);
@(posedge clk)
$rose(s) |-> (##1 $fell(b)[->1] ##1 b[->1]) within e[->1];
endproperty
B_CHG_ONCE_AC_1: assert property (b_chg_once_ac_within(.s(a), .e(c), .b(b)));
initial begin
b = 1;
repeat(1) @(posedge clk);
repeat(1) begin
repeat(1) @(posedge clk);
a = 1;
//b go low & high repeat twice
repeat(4) begin
@(posedge clk);
b = !b;
end
repeat(2) @(posedge clk);
a = 1;
end
repeat(1) @(posedge clk);
c = 1;
repeat(5) @(posedge clk);
$finish();
end // initial begin
initial begin
$dumpfile("dump.vcd");
$dumpvars(0,tb);
end
endmodule
In reply to mlsxdx:
The use of the English word “within” in an assertion is misleading when b[=n] is the
last term of a seq1 and the within is used (i.e., seq1 within seq2)
Lengthy explanation, but bear with me.
1800: "The construct seq1 within seq2 is an abbreviation for the following:"
// (1[*0:$] ##1 seq1 ##1 1[*0:$]) intersect seq2
thus,
$rose(a) |-> (##1 $fell(b)[->1] ##1 b[=1]) within e[->1];
is per LRM definition same as rose(a) |-> (1[*0:] ##1fell(b)[->1] ##1 b[=1]** ##1 1[*0:]) intersect e[->1];
Also by expanding b[=1] to b[->1] ##1 !b[*0:$], we can say that this is same as rose(a) |-> (1[*0:] ##1fell(b)[->1] ##1 b[->1] ##1 !b[*0:] ##1 1[*0:$])
intersect e[->1];
// expanding the thread, rose(a) |-> (1[*0:] ##1fell(b)[->1] ##1 b[->1] ##1 **!b[*0] ##1 1[*0:]) or
(1[*0:$] ##1fell(b)[->1] ##1 b[->1] ##1 **!b[*1] ##1 1[*0:]**) or
… intersect e[->1];
b[->1] ##1 !b[*0] ##1 1[*0:]) is same as
b[->1] ##1 1[*0:])
//Thus, ignoring the other !b[*n] "or" threads, we can say
$rose(a) |-> (##1 $fell(b)[->1] ##1 b[=1]) within e[->1];
//is same as
$rose(a) |-> (1[*0:$] ##1 $fell(b)[->1] ##1 b[->1] ##1 1[*0:$]) intersect e[->1];
Thus, any 2 or more b occurrences will not cause a failure.
For a pass we need 1 “b”.
There is no such issue with the intersect
$rose(a) |-> (##1 $fell(b)[->1] ##1 b[=1]) intersect e[->1]
Then b[=1]) intersect e[->1] is the right formulation, except that b could coincide with e. If it should happen before e then perhaps (b[=1] ##1 !b) intersect e[->1] would work.
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
Thanks for your detailed explanation on why within does not work as expected due to the unbounded expansion(##1 1[*0:$]).
I really appreciate that you bring deep insight on within & [->1] by doing the expansion of the formulation. Well, in my application, if the rising edge of e may or may not overlap with rising edge of b, will the following property work?
//if the rising edge of e may or may not overlap with rising edge of b,
// the following allows that
$rose(s) |-> (##1 $fell(b)[->1] ##1 b[=1]) intersect e[->1];
// But
$rose(s) |-> (##1 $fell(b)[->1] ##1 b[=1] ##[0:$] !b) intersect e[->1];
// will not allow b==1 in the same cycle as e==1
(##1 $fell(b)[->1] ##1 b[=1] ##[0:$] !b) // is same as
(##1 $fell(b)[->1] ##1 b[->1] ##1 !b[*0:$] ##[0] !b) // same as
(##1 $fell(b)[->1] ##1 b[->1] ##1 !b[*0] ##[1] !b) or
(##1 $fell(b)[->1] ##1 b[->1] ##1 !b[*0] ##[2] !b) or
...
This gets simplified to
(##1 $fell(b)[->1] ##1 b[->1] ##1 !b[*0:$] ##[0] !b) // null
(##1 $fell(b)[->1] ##1 b[->1] ##1 !b) or
(##1 $fell(b)[->1] ##1 b[->1] ##1 ##1 !b) or
..
You can just use the following if b and e cannot be in the same cycle
(##1 $fell(b)[->1] ##1 b[=1] ##1 !b) intersect e[->1];
// same as
(##1 $fell(b)[->1] ##1 b[->1] ##1 !b[*0:$] ##1 !b); // same as
(##1 $fell(b)[->1] ##1 b[->1] ##1 !b) or
(##1 $fell(b)[->1] ##1 b[->1] ##1 !b[*1:$] ##1 !b)
//if the rising edge of e may or may not overlap with rising edge of b,
// the following allows that
$rose(s) |-> (##1 $fell(b)[->1] ##1 b[=1]) intersect e[->1];
// But
$rose(s) |-> (##1 $fell(b)[->1] ##1 b[=1] ##[0:$] !b) intersect e[->1];
// will not allow b==1 in the same cycle as e==1
(##1 $fell(b)[->1] ##1 b[=1] ##[0:$] !b) // is same as
(##1 $fell(b)[->1] ##1 b[->1] ##1 !b[*0:$] ##[0] !b) // same as
(##1 $fell(b)[->1] ##1 b[->1] ##1 !b[*0] ##[1] !b) or
(##1 $fell(b)[->1] ##1 b[->1] ##1 !b[*0] ##[2] !b) or
...
This gets simplified to
(##1 $fell(b)[->1] ##1 b[->1] ##1 !b[*0:$] ##[0] !b) // null
(##1 $fell(b)[->1] ##1 b[->1] ##1 !b) or
(##1 $fell(b)[->1] ##1 b[->1] ##1 ##1 !b) or
..
You can just use the following if b and e cannot be in the same cycle
(##1 $fell(b)[->1] ##1 b[=1] ##1 !b) intersect e[->1];
// same as
(##1 $fell(b)[->1] ##1 b[->1] ##1 !b[*0:$] ##1 !b); // same as
(##1 $fell(b)[->1] ##1 b[->1] ##1 !b) or
(##1 $fell(b)[->1] ##1 b[->1] ##1 !b[*1:$] ##1 !b)
Sorry for my confusion. I just got the part you explain earlier.
Therefore, the property can handle b, e overlap case $rose(s) |-> (##1 $fell(b)[->1] ##1 b[=1]) intersect e[->1];
But if b, e requires non-overlap, then (##1 $fell(b)[->1] ##1 b[=1] ##1 !b) intersect e[->1];
I was confused on the 4 combination among b[=1] within, b[=1] intersect, b[->1] within, b[->1] intersect. Let me summarize them and put 4 property together and bring my questions back.
In reply to mlsxdx:
The use of the English word “within” in an assertion is misleading when b[=n] is the
last term of a seq1 and the within is used (i.e., seq1 within seq2)
Lengthy explanation, but bear with me.
1800: "The construct seq1 within seq2 is an abbreviation for the following:"
// (1[*0:$] ##1 seq1 ##1 1[*0:$]) intersect seq2
thus,
$rose(a) |-> (##1 $fell(b)[->1] ##1 b[=1]) within e[->1];
is per LRM definition same as rose(a) |-> (1[*0:] ##1fell(b)[->1] ##1 b[=1]** ##1 1[*0:]) intersect e[->1];
Also by expanding b[=1] to b[->1] ##1 !b[*0:$], we can say that this is same as rose(a) |-> (1[*0:] ##1fell(b)[->1] ##1 b[->1] ##1 !b[*0:] ##1 1[*0:$])
intersect e[->1];
// expanding the thread, rose(a) |-> (1[*0:] ##1fell(b)[->1] ##1 b[->1] ##1 **!b[*0] ##1 1[*0:]) or
(1[*0:$] ##1fell(b)[->1] ##1 b[->1] ##1 **!b[*1] ##1 1[*0:]**) or
… intersect e[->1];
b[->1] ##1 !b[*0] ##1 1[*0:]) is same as
b[->1] ##1 1[*0:])
//Thus, ignoring the other !b[*n] "or" threads, we can say
$rose(a) |-> (##1 $fell(b)[->1] ##1 b[=1]) within e[->1];
//is same as
$rose(a) |-> (1[*0:$] ##1 $fell(b)[->1] ##1 b[->1] ##1 1[*0:$]) intersect e[->1];
Thus, any 2 or more b occurrences will not cause a failure.
For a pass we need 1 “b”.
There is no such issue with the intersect
$rose(a) |-> (##1 $fell(b)[->1] ##1 b[=1]) intersect e[->1]
Then b[=1]) intersect e[->1] is the right formulation, except that b could coincide with e. If it should happen before e then perhaps (b[=1] ##1 !b) intersect e[->1] would work.
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
Ben :
Would you explain more how you got " Thus, any 2 or more b occurrences will not cause a failure." ?
Thanks
In reply to VE:
I demonstrated that
(##1fell(b)[->1] ##1 b[=1]) within e[->1];
expands to this
(1[*0:] ##1fell(b)[->1] ##1 b[->1] ##1 !b[*0] ##1 1[*0:]) or // thread1
(1[*0:$] ##1fell(b)[->1] ##1 b[->1] ##1 !b[*1] ##1 1[*0:]) or //thread 2
(1[*0:$] ##1fell(b)[->1] ##1 b[->1] ##1 !b[*2] ##1 1[*0:]) or
…
Thus any of those threads can pass.
Consider thread1
**(1[*0:$] ##1fell(b)[->1] ##1 b[->1] ##1 !b[*0] ##1 1[*0:])
**
This expands to:
(1[*0:$] ##1fell(b)[->1] ##1 b[->1] ##1 !b[*0] ##1 1[*0]) or
// x[*0] ##1[*0] w // is a no match (1[*0:] ##1fell(b)[->1] ##1 b[->1] ##1 !b[*0] ##1 1[*1]) or
(1[*0:] ##1fell(b)[->1] ##1 b[->1] ##1 !b[*0] ##1 1[*1]) or
// x[*0] ##1[*1] /w/ is same as w
// thus that one above gets reduced to
(1[*0:] ##1fell(b)[->1] ##1 b[->1] ##1 1[*1]
(1[*0:] ##1fell(b)[->1] ##1 b[->1] ##1 1[*2])
..
(1[*0:] ##1fell(b)[->1] ##1 b[->1] ##1 1[*n])
Thus, we can say that
**(1[*0:] ##1fell(b)[->1] ##1 b[->1] ##1 !b[*0] ##1 1[*0:])
**
is same as
**(1[*0:$] ##1fell(b)[->1] ##1 b[->1] ##1 1[*0:])
**
In this thread, after a fall of b and then 1 occurrence of b you have many
threads of true with one of them matching the intersection of an occurrence of e.
Any second occurrence of “b” is ignored. Note *b[->1] ##1 1[0:$]
In reply to mlsxdx:
The (##1 $fell(b)[->1] ##1 b[=1] ##1 !b) intersect e[->1];
says that between b and e there must be at least 1 !b; there can be more.
Tou could also write a separate assertion like
not(b && e);
Hi Ben,
Using intersect e[->1] instead of within e[->1] require that the rising edge of b strongly related to rising edge of e.
In my application, the rising edge of b and rising edge of c are not strict related. In other words,
when b go high, it could be many clock cycles, then e go high. If this is the case, do you have any suggestion to attack the problem?
Using intersect e[->1] instead of within e[->1] require that the rising edge of b strongly related to rising edge of e.
In my application, the rising edge of b and rising edge of c are not strict related. In other words, when b go high, it could be many clock cycles, then e go high. If this is the case, do you have any suggestion to attack the problem?
(##1 $fell(b)[->1] ##1 b[=1] ##1 !b) intersect e[->1]
This requires that b go low aligning with e go high by using intersect. In my case, b from high to low is after e go high.
// If b cannot fall after the rise then
(##1 $fell(b)[->1] ##1 b[->1] ##1 b[*0:$]) intersect e[->1]
// if b is a pulse then
(##1 $fell(b)[->1] ##1 $rose(b)[=1]) intersect e[->1]
// equivalent to
(##1 !fell(b)[*0:$] ##1 $fell(b) ##1 !$rose(b)[*0:$] ##1 $rose(b) ##1 !$rose(b)[*0:$])
intersect e[->1]
// If b cannot fall after the rise then
(##1 $fell(b)[->1] ##1 b[->1] ##1 b[*0:$]) intersect e[->1]
// if b is a pulse then
(##1 $fell(b)[->1] ##1 $rose(b)[=1]) intersect e[->1]
// equivalent to
(##1 !fell(b)[*0:$] ##1 $fell(b) ##1 !$rose(b)[*0:$] ##1 $rose(b) ##1 !$rose(b)[*0:$])
intersect e[->1]
Can you share some insight why using $rose(b) instead of b makes such difference?
I put both in the same stimulus, and one without $rose failed 1 cc after rising edge of b.
- b
(##1 !fell(b)[*0:$] ##1fell(b) ##1 !b[*0:] ##1 b ##1 !b[*0:$]) intersect e[->1]
Let’s say @9, b 0 → 1, it expanded to multiple threads. Which thread is the one to make the assertion failed @11? Why the assertion not continuously wait on thread 2,3… until rising edge of e coming out?
**- rose(b)**
(##1 !fell(b)[*0:] ##1 $fell(b) ##1 !rose(b)[*0:] ##1 $rose(b) ##1 !rose(b)[*0:]) intersect e[->1]
Instead, why $rose make such difference, and it waiting until the end of the simulation?
Can you share some insight why using $rose(b) instead of b makes such difference?
I put both in the same stimulus, and one without $rose failed 1 cc after rising edge of b. $rose makes difference - EDA Playground
(##1 $fell(b)[->1] ##1 $rose(b)[=1]) intersect e[->1]
After the fall of b, then any cycle later(1 or more) you expect a rise of b.
Thereafter, any cycle later (1 or more), b can stay at 1’b1 or can fall to 1’b0.
If it falls, “b” cannot rise again, else failure until an occurrence of e (the intersect).
(##1 $fell(b)[->1] ##1 (b)[=1]) intersect e[->1]
After the fall of b, then any cycle later(1 or more) you expect b==1 (a rise of b).
Thereafter, in the next cycle b stays at 1’b0 forever until an occurrence of e (the intersect).
We seem to go frame SVA to requirements, instead of requirements to SVA.
(##1 !fell(b)[*0:$] ##1fell(b) ##1 !b[*0:] ##1 b ##1 !b[*1]) intersect e[->1] //thread1
cause the failure because the fell o b is at t7, rise of b at t9, and at t11 b==1 instead of 0
$rose(s) |-> (##1 $fell(b)[->1] ##1 $rose(b)[=1]) intersect e[->1];
After the rose of b ar t9, I don’t see any violation of !$rose(b) because b==1 forever after the rose.
Add err signals to see the effect on the waveforms. Se my changes to your code at