Equivalent expression for if-else property_expression

SystemVerilog
,
1

Hi All,


if (boolean_expression) property_expr;
 
// is equivalent to
 
booloen_expression |-> property_expr;

I was wondering what would be the equivalent expression for if-else property_expression ?

I tried the following code : edalink , here is what I observe ::
(a) For +define+SAME when all the 3 clock are of same clock period , the output is the same in both cases i.e using if-else as well the equivalent expression the output match

(b) However when the clock periods are different , I observe different output across tools.

For 1st stimulus i.e +define+M1 :
Using if-else the assertion passes at T:7 however when using the equivalent expression,
2 tools show pass at T:5 and 15 whereas only one tool shows pass at T:7 ( same o/p as if-else )

I understand that we don’t discuss tool related issues but I am curious on how the expression :

ap1:assert property ( ( @(posedge clk0) b |-> @(posedge clk1)  a  ) or ( @(posedge clk0) !b |-> @(posedge clk2) c )  )

is evaluated ?

On 1st posedge of clk0 at T:5 , one of the antecedent is vacuously true . Would the or operator return true due to this ? i.e resulting in pass at T:5 and 15

The output matches the if-else if I try using expression :

ap1:assert property (  @(posedge clk0) 1 |-> ( @(posedge clk1) a or  @(posedge clk2) c )  )

But I doubt that this can be termed as the equivalent expression for if-else in general

2

In reply to Have_A_Doubt:

I was wondering what would be the equivalent expression for if-else property_expression ?


// For (if(expr1) prop; else (prop2) I would write 2 properties
// 1) it's clearer and easier to debug
// I personally, as a matter of style I prefer to use the |-> instead of the "if
// Also, avoid property declarations if you are not using local variables or if 
// you are not reusing the property.
-------------------------------------
// Discussion of 
ap1:assert property ( ( @(posedge clk0) b |-> @(posedge clk1)  a  ) or 
                      ( @(posedge clk0) !b |-> @(posedge clk2) c )  );
// This assertion can never fail because the antecedent of one of the properties is a NO MATCH
// causing it to be vacuously true. 

------------------------------------
// Discussion of 
ap1:assert property (  @(posedge clk0) 1 |-> ( @(posedge clk1) a or  @(posedge clk2) c )  )
// But I doubt that this can be termed as the equivalent expression for if-else in general
// IT IS NOT equivalent to the if else. 
// KISS, write 2 separate assertions, one for each value of the expression of the antecedent.

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