Hi All,
Consider the following property declaration
property ab;
@(posedge clk) a |=> b[=0];
endproperty
I observe that assertion is a pass whenever ‘b’ is false during evaluation of consequent.
If ‘b’ is true when consequent is evaluated then the assertion fails.
Generally equivalent expression for b[=1] is !b[*0:] ##1 b ##1 !b[*0:].
What would be the equivalent expression for b[=0] ? As per the output it seems in the equivalent expression one of the 'or’ed expression would be !b
In reply to Have_A_Doubt:
b[=0] means that there is no occurrence of b followed by no occurrence of b.
I would say that the equivalence is *!b[0:$]
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
In reply to ben@SystemVerilog.us:
Hi Ben,
*!b[0:$] would be equivalent to **!b[*0] or !b[*1] or !b[*2] or !b[3] or … or !b[N]
**As !b[0] is an empty sequence , it would never match right ?
So the assertion would pass at the earliest due to !b[1] and the implicit first_match for the consequent
In reply to Have_A_Doubt:
b[=1] is !b[*0:$] ##1 b[*1[ ##1 !b[*0:$]
//
b[=0] is !b[*0:$] ##1 b[*0] ##1 !b[*0:$]
!b[*0:$] ##1 !b[*0:$] // reduced
!b[*0:$]
// for the following
a |=> b[=0]
/* As !b[*0] is an empty sequence , it would never match right ?
YES
So the assertion would pass at the earliest due to !b[*1] and the implicit first_match for the consequent
Yes. */
//Typical use
a |=> b[=0] ##1 c
// I prefer to write it as
a |=> !b[*0:$] ##1 c
In reply to ben@SystemVerilog.us:
Hi Ben,
Generally b[=m] means that ‘b’ must be true on ‘m’ clocks (not necessarily consecutive)
So b[=0] would mean that ‘b’ must be true on ‘0’ clocks i.e ‘b’ should never be true.
The same can be cross checked via it’s equivalent expression: !b[*0:$] i.e ‘b’ should never be true.
However the assertion passes/fails on the very 1st clock that the consequent is evaluated using
property ab;
@(posedge clk) a |=> !b[0:$];
endproperty
It doesn’t actually check that ‘b’ is false throughout simulation, hence I tried the following:
// Attempt 1
property ab1;
@(posedge clk) a |=> always !b ;
endproperty
Using ‘ab1’ the assertion doesn’t pass even if ‘b’ is false throughout simulation
// Attempt 2
property ab2;
@(posedge clk) a |=> always strong(!b);
endproperty
Similar to ‘ab1’, the assertion doesn’t pass even if ‘b’ is false throughout simulation for ‘ab2’
// Attempt 3
property ab3;
@(posedge clk) a |=> s_always[1:10]!b; // s_always can't be unbounded
endproperty
Have a few questions related to attempt 3
[Q1] The simulation time could vary based on the test that is being run, so how do I generalize the range in s_always ?
[Q2] What does the 1 and 10 signify ?
If I were to write s_always[3:10] !b , if the antecedent is true at T0, then the consequent is evaluated from T1. What does range [3:10] indicate ?
[Q3] Is there any alternative to s_always to check that ‘b’ is false throughout simulation ?
I was thinking of something along the lines of :
bit simulatn_ends;
property ab4;
@(posedge clk) a |=> strong( !b throughout $rose( simulatn_ends )[->1] );
endproperty
final begin // Executes after $finish() is called in UVM Tb via uvm_top::run_test()
simulatn_ends = 1;
end
In reply to Have_A_Doubt:
Generally b[=m] means that ‘b’ must be true on ‘m’ clocks (not necessarily consecutive)
So b[=0] would mean that ‘b’ must be true on ‘0’ clocks i.e ‘b’ should never be true.
The same can be cross checked via it’s equivalent expression: !b[*0:$] i.e ‘b’ should never be true.
However the assertion passes/fails on the very 1st clock that the consequent is evaluated using
property ab;
@(posedge clk) a |=> b[=0];
endproperty
b[=1] is same as !b[*0:$] ##1 b[*1] ##1 !b[*0:$]
// There are many ORed threads.
b[=1] !b[*0:$] ##1 b[*1] ##1 !b[*0:$] // as a reference
// For the "=0"
b[=0] !b[*0:$] ##1 b[*0] ##1 !b[*0:$] // is same as
//
!b[*0] ##1 !b[*0] ##1 !b[*0] or
!b[*0] ##1 !b[*0] ##1 !b[*1] or
!b[*0] ##1 !b[*0] ##1 !b[*n]
// COnsider those threads and reducing them because a[*0] ##1 b is same as b
!b[*0] ##1 !b[*0] ##1 !b[*0] // is same as
!b[*0]
!b[*0] ##1 !b[*0] ##1 !b[*1]
!b[*1] // same as
Thus, you say that b[=0] is same as
!b[*0] or !b[*1] or !b[*2] or ...
// FOr your
a |=> b=0]; // same as
a |=> !b[*0] or !b[*1] or !b[*2] or ...
// Thus, b[=0] is NOT the same as always !b and
// the assertion passes/fails on the very 1st clock that the consequent is evaluated
// It would pass because of the !b[*1]
**
On the always**
always [cycle_delay_const_range_expression] property_expr Evaluates to true (vacuous or nonvacuous true) if property_expr holds at every current or future clock tick that is within the range of clock ticks specified by const_range. It is not required that all clock ticks within this range exist.
always [cycle_delay_const_range_expression] property_expr Evaluates to true (vacuous or nonvacuous true) if property_expr holds at every current or future clock tick that is within the range of clock ticks specified by const_range. It is not required that all clock ticks within this range exist.
@(posedge clk) a |=> s_always[1:10]!b
In the cycle after “a” (T0) then starting from the next cycle (T1) b== until T10.
The max range cannot use the $, but you can use a 2^31 (syntax? forgot it, sorry)
I don’t think that your approach with simulatn_ends = 1; will work because of sampling.
I think that you need to set the simulatn_ends = 1; before the end of sim
Ben
In reply to ben@SystemVerilog.us:
I don’t think that your approach with simulatn_ends = 1; will work because of sampling.
I think that you need to set the simulatn_ends = 1; before the end of sim
Thanks Ben for the pointer. Will have to work on some alternative logic
The max range cannot use the $, but you can use a 2^31 (syntax? forgot it)
I believe you meant 2**31
Later I was trying a variation of the consequent
property ab2;
@(posedge clk) a |=> b[->0]; // consequent changed from b[=0]
endproperty
As you have already explained above , *b[=0] is equivalent to !b[0:$]
What would the equivalent expression for b[->0] be ?
I am aware that :
b[->1] is equivalent to !b[*0:$] ##1 b[*1]
Shouldn't b[->0] be equivalent to !b[*0:$] ##1 b[*0] i.e !b[*0:$] ?
However I observe different results with consequent as b[->0] compared to b[=0] for following stimulus
always #5 clk = ~clk;
initial begin
#4; a = 1;
#10; a = 0;
#30; b = 1;
end
With b[=0] the assertion passes at T:15 whereas the assertion fails at T:15 with b[->0]
In reply to Have_A_Doubt:
Will have to work on some alternative logic
I am currently trying the following
bit simulatn_ends,clk ,a, b;
always #5 clk = !clk;
property ab4;
@(posedge clk) a |=> ( !b throughout $rose( simulatn_ends )[->1] ) or strong( @(simulatn_ends) 1 ) ;
endproperty
assert property(ab4) $display("T:%0t Pass",$time);
initial begin
#4;a=1;
#10;a=0;
#102;$finish();
end
final begin // Executes after $finish() is called in UVM Tb via uvm_top::run_test()
simulatn_ends = 1;
end
My understanding was on calling $finish(), only the final block and strong operator in effect will execute.Yet there is no pass once simulation ends
In reply to Have_A_Doubt:
b[->0] is equivalent to
!b[*0:$] ##1 b[*0] // expanding to
!b[*0] ##1 b[*0] or // same as b[*0]
!b[*1] ##1 b[*0] or ... // same as !b[*1] ##1 empty_match
// Same as
b[*0] or !b[*1] ##1 empty_match or !b[*2] ##1 empty_match
Thus, b[->0] always ends with an empty_match, which is a fail
I believe that optimization in the tool determines that there is no need to test all the other ORed threads because ALL of them end with an empty match
(2) - EDA Playground // code
EPWave Waveform Viewer // wave
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
In reply to ben@SystemVerilog.us:
Hi Ben,
!b[*1] ##1 b[*0] or … // same as !b[*1] ##1 empty_match
// Same as
b[*0] or !b[*1] ##1 empty_match or !b[*2] ##1 empty_match
I am not clear on this.
**Shouldn’t ( !b[*1] ##1 b[*0] ) be equivalent to ( !b[1] ##0 true ) i.e !b[1] ?
Similarly !b[*2] ##1 b[*0] be equivalent to !b[*2] ##0 true i.e !b[*2]
In general !b[*N] ##1 b[*0] be equivalent to !b[*N] ##0 true i.e !b[*N]
So the resultant equivalent expression would be **!b[*0] or !b[*1] or !b[2] or … !b[N]
In reply to Have_A_Doubt:
Shouldn’t ( !b[*1] ##1 b[*0] ) be equivalent to ( !b[*1] ##0 true )
[Ben] The below analysis seem to indicate that
b[>0] is equivalent to empty or !b[*1] ##0 true or !b[*2] ##0 true or …
However, 1800 pg 446 states:
1800 16.12.22 Nondegeneracy It is possible to define sequences that can never be matched. For example:
(1’b1) intersect(1’b1 ##1 1’b1)
It is also possible to define sequences that admit only empty matches. For example: 1’b1[*0]
A zero consecutive repetition means that there is no sample taken at any clock tick. Therefore, such a sequence can only match on an empty trace (as formally defined in F.4.3 ). *A sequence may admit both empty and nonempty matches, for example, a[0:2]. This sequence admits an empty match and up to two nonempty matches: a and a[*2]. A sequence that admits no match or that admits only empty matches is called degenerate. A sequence that admits at least one nonempty match is called nondegenerate. A more precise definition of nondegeneracy is given in F.5.2 and F.5.5 . The following restrictions apply:
a) Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match.
b) Any sequence that is used as the antecedent of an overlapping implication (|->) shall be nondegenerate.
c) Any sequence that is used as the antecedent of a nonoverlapping implication (|=>) shall admit at least one match. Such a sequence can admit only empty matches. The reason for these restrictions is because the use of degenerate sequences in forbidden ways results in counterintuitive property semantics, especially when the property is combined with a disable iff clause.
This 1800 limitation causes b[->0] to be inadmissible, regardless on how you expand it.
a) Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match.
a |-> (b [-> 0])
A sequence that is used as property must be non-degenerate and admit no
empty match.
1800’2017 16.9.2.1 Repetition, concatenation, and empty matches Using 0 as a sequence repetition number, an empty sequence (see 16.7 ) results, as in this example: a [*0]
Because empty matches occur over an interval of zero clock ticks and are thus of length 0, they follow the set of concatenation rules specified below. In the following rules, an empty sequence is denoted as empty, and another sequence (which may be empty or nonempty) is denoted as seq.
— (empty ##0 seq) does not result in a match.
— (seq ##0 empty) does not result in a match.
— (empty ##n seq), where n is greater than 0, is equivalent to (##(n-1) seq).
— (seq ##n empty), where n is greater than 0, is equivalent to (seq ##(n-1) true). Using simple decomposition, once would think that the following is true: b[->0] is equivalent to !b[*0:$] ##1 b[*0] // expanding to **!b[*0] ##1 b[*0] or** // (empty ##n seq) same as (seq ##(n-1) true)
b[*0] ##0 `true // (empty ##0 seq) does not result in a match.
// !b[*0] ##1 b[*0] is a no match
**!b[1] ##1 b[0] or // (seq ##n empty) same as (seq ##(n-1) true). !b[*1] ##0 true
**!b[2] ##1 b[0] or
!b[*2] ##0 `true
…
Shouldn’t ( !b[*1] ##1 b[*0] ) be equivalent to ( !b[*1] ##0 true )
My mistake, it looks like it should be equivalent to
empty or !b[*1] ##0 true or !b[*2] ##0 true or …
But 1800 prevents the use of b[->0] as mentioned above
Thanks for asking,
Ben
In reply to ben@SystemVerilog.us:
Hi Ben,
This 1800 limitation causes b[->0] to be inadmissible, regardless on how you expand it.
Could you please elaborate on this
As per 1800 16.12.22 Nondegeneracy :
A sequence that admits no match or that admits only empty matches is called degenerate. A sequence that admits at least one nonempty match is called nondegenerate.
Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match.
**[Q1]So by this definition wouldn’t b[->0] be a nondegenerate since it has non-empty match for !b[*1]/!b[*2]/!b[3]/…/!b[N] ?.
1800 16.12.22 mentions ::
a) Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match.
I find this statement a little confusing as **a nondegenerate can be an ‘or’ of empty as well as non-empty sequences used as property.
A nondegenerate sequence Eg: a[0:3] has an empty match (a[0]) as well as at least one non-empty match (a[*1]/a[*2]/a[*3])
*[Q2] So as per LRM would sequence a[0:3] be illegal as a consequent ? ( A case can be made for both )
I understand that we don’t discuss tool related issues here but I observe that one of tools throws a compilation error:
“A sequence that is used as property must be non-degenerate and admit no empty match.”
The error is observed when using consequent as either b[=0] / b[->0]
*[Q3] Irrespective of whether I write consequent as b[=0]/b[->1] as both their equivalent expression is the same i.e !b[0:$],
shouldn’t the error exist for both cases ?
A 2nd tool throws compilation error only for b[->1] with the following explanation :
xmhelp xmsim ZERPFS ::
xmsim/ZERPFS =
The property mentioned in the error message matches an empty sequence and is not supported.
The property, as written, can complete a match in zero cycles.
Examples of unsupported properties:
property empty_sequence_1;
@(negedge clk)
(a[*0]);
endproperty
property empty_sequence_2;
@(negedge clk)
(a |-> a[*0:3]);
endproperty
See https://verificationacademy.com/forums/systemverilog/q-why-b-0-b0-degenrate-and-empty-match
Q: Why is b[->0, b[=0]] degenerate and is an empty match?