What is "not" property operator in SystemVerilog Assertion?

SystemVerilog
1

What i “not” property operator in System verilog Assertion?
please explain with example.

2

In reply to Mukund Sojitra:

What is “not” property operator in System verilog Assertion?
please explain with example.

The answer is in 1800.

1800’2012

16.12.2 Negation property
A property is a negation if it has the form not property_expr. For each evaluation attempt of the property, there is an evaluation attempt of property_expr. The keyword not states that the evaluation of the property returns the opposite of the evaluation of the underlying property_expr. Thus, if property_expr evaluates to true, then not property_expr evaluates to false; and if property_expr evaluates to false, then not property_expr evaluates to true.
The not operator switches the strength of a property. In particular, one should be careful when negating a sequence. For example, consider the following assertion:
a1: assert property (@clk not a ##1 b);
Since the sequential property a ##1 b is used in an assertion, it is weak. This means that if clk stops ticking and a holds at the last tick of clk, the weak sequential property a ##1 b will also hold beginning at that tick, and so the assertion a1 will fail. In this case it is more reasonable to use:
a2: assert property (@clk not strong(a ##1 b));

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

3

In reply to Mukund Sojitra:

In temporal languages, there are 2 common styles of property description/specification viz:

  1. Express a property that shall hold
  2. Express a property that shall NOT/never hold

SVA’s property level not operator falls in #2 style above. In PSL it is called “never” - FWIW.

Consider a req signal that shall be a pulse - meaning it can be high for only one clock (per
access of-course). There are 2 styles to capture this requirement:

Style - 1:


  property p_sig_is_pulse (sig);
    sig !=> !sig; // Assume default clk, abort etc.
  endproperty : p_sig_is_pulse

Style - 2:


  property p_sign_shall_never_be_high_cont (sig);
    not (sig [*2];  // Assume default clk, abort etc.
  endproperty : p_sign_shall_never_be_high_cont

Which one to use - your choice. But I see many engineers using Style-1. And also consider that Style-2 has potential issues with implication operator etc. (As Ben pointed out).

HTH
Srini
www.verifworks.com

4

Thanks for your kind Help.

5

In reply to Mukund Sojitra:
From our SVA Handbook 4th Edition

Vacuity
[1] An evaluation attempt of a property of the form not property_expr is nonvacuous if, and only if, the underlying evaluation attempt of property_expr is nonvacuous. Thus, the not(vacuous_property) (e.g., not(a |-> b)) is vacuously false if a==0; this is because (a → b) is vacuously true. Simulators process a vacuous failure as a valid failure, and provide statistical contributions to the fail counter.
Guideline: Limit the use of the not property operator in properties where the property_expr is a sequence, Boolean, or property with until, eventually. Do not use the not operator in properties where the property_expr can be vacuous. The reason for this recommendation is that negated assertions that contain the implication operators are difficult to understand and can be misleading. The following property statement specifications demonstrate the issues. The requirements state that a request should never be followed by an acknowledge in the same cycle, thus if req ==1, ack must be ==0 in the same cycle). The table below demonstrates the difference in results between the following properties:

 
not (req |-> ack); //  Leads to incorrect results, AVOID THIS structure
req |-> not ack; //  // Use not for consequent that is a sequence , e.g. (a |-> not(b ##1 c))
req |-> !ack; //  // Use logical negation for negation of a variable
not(req ##0 ack); //  Does not provide meaningful coverage,

989×437 45.2 KB

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

6

Thank you very Much Ben. You are helping me a lot.