What is the difference between "implication", "implies", and 'if-else"?

SystemVerilog
, , ,
1

Hello.

I’m studying an assertion to the IEEE 1800-2017 standard for SystemVerilog. I read the “implication” and “if-else” properties. I think they are pretty similar. When I read the “implies” property, I was confused as the 3 statements are similar meanings. What is the difference between these three statements? Please provide explanations and examples.

Thanks to your reply.

2

In reply to jh_veryveri:

Yes these properties have similar and in some cases overlapping functionality. They all have the form Antecedent operator Consequent.

Implication is the most common and has the form

sequence_expr_A |-> property_expr_C

This means the property_expr must be true starting from the cycle that sequence_expr has a match. When the sequence_expr is just a 1-cycle boolean expression, you can write this as

if ( boolean_expr ) property_expr
// same as 
boolean_expr_A |->  property_expr_C

Most people still chose the implication using using a simple if. The expressiveness comes from using the if with an accompanying else

if ( boolean_expr_A ) property_expr_C1 else property_expr_C2
// same as 
  boolean_expr_A |-> property_expr_C1
! boolean_expr_A |-> property_expr_C2


property_expr_A implies property_expr_C

The above property overlaps the functionality of implication when the antecedent is just a 1-cycle boolean expression. However when the antecedent is a sequence or property, the consequent gets evaluated concurrently with the antecedent instead of waiting for the antecedent to become true. This implies property operator is for very complicated properties and usually involved nested multi-clock implication properties.

3

In reply to dave_59:

Hello, Dave.

Thanks to your explanation. It helps to understand “implication statement” for me.

I have a question more. The standard document says

property_expr1 implies property_expr2
// A property of this form evaluates to true if, and only if, either property_expr1 evaluates to false or property_expr2 evaluates to true.

And, you explained that

However when the antecedent is a sequence or property, the consequent gets evaluated concurrently with the antecedent instead of waiting for the antecedent to become true.

Is the property true regardless of the outcome of the antecedent if the evaluation of the consequent is completed for true during the evaluation of the antecedent?
If the consequent is false in this case, is the property false?

Thanks always for your explanations and comments.

4

In reply to jh_veryveri:

That is correct, the property is true once the consequent becomes true. Another level of complexity is the concept of vacuous and non-vacuous success. An assertion of this kind of property only succeeds (passes) if both the antecedent and consequent are true.

5

In reply to dave_59:

Thanks to your reply, Dave.

The subsequent expression must be true for the property to be non-vacuous true! If the sequence expression is false, the property seems to be vacuous true.

Thanks.