Which of the following would be the correct way of writing the property?

SystemVerilog
, , ,
1

which would be the correct way of writing the property (scenario is: for a valid signal, seq1 and either seq2 or seq3 needs to be high.

Eg: property P1
@(posedge clk)
valid-> seq1 && (seq2 || seq3);
endproperty

property P2
@(posedge clk)
valid-> seq1 and (seq2 or seq3);
endproperty.

if P1 is incorrect,why cannot we use logical symbols while using sequences(&& or ||)?

2

In reply to 100rabhh:

property P2; // Correct 
@(posedge clk)
valid-> seq1 and (seq2 or seq3);
endproperty.
  • 1800 requires the use of the or, and operators with sequences.
  • Sequences and/or operators need to be different than than Boolean && || operators for several reasons:

// 1) Resolve issues and intent
ap1: assert property(@ (posedge clk) a ##1 b || c ##1 d);
// interpreted as (a ##1 (b || c) ##1 d)
ap2: assert property(@ (posedge clk) a ##1 b or c ##1 d);
// interpreted as  (a ##1 b) or (c ##1 d)
// ## has higher precedence than "or", "and"
// 2) The flow through and handling of local variables in the ORing and ANDing threads.
/* If the sequence makes assignments to local variables, then each of the sequence involved in the ORing carries its own individual and separate copy of the local variables. Those separate copies of the local variables are carried all the way through each of the ORed sequence thread.
Each matching thread of an or operand continues as a separate thread; that matching thread carries with it its own copy of the local variables, which flow out of the composite sequence and out of the implication operator (i.e., |->, |=>). Thus, in summary, the local variables in properties with an antecedent and consequent are handled in the following manner:
1) If a multithreaded antecedent updates a local variable within its thread, each thread carries its own copy of the local variable.
2) If that property local variable is used in the consequent, the copy of that local variable is carried for each of those threads.
Consider the following property: */
property p_abv;
bit v;
(a, v=1) or (b, v=0) |=> v==1;
endproperty : p_abv
/* The antecedent of this property has two threads (a, v=1) and (b, v=0); each of those thread carries its own individual copy of the local variable. In the consequent, each antecedent thread must be evaluated with consequent. In this case, the individual copy of the local variable for each thread is carried into the consequent when that thread is evaluated. Thus for thread (a, v=1) the v in the consequent is the copy used in that thread. Similarly, for thread (b, v=0) the v in the consequent is the copy used in that thread.
The equivalent property to p_abv is the following: */
property p_abv_eqv;
bit v1, v2;
( (a, v1=1'b1) |=> v1==1) and
( (b, v2=1'b0) |=> v2==1);
endproperty : p_abv_eqv
/* In the above example, if a==1'b1, and b==1'b1, then the property will fail.
 Rule: There are strict rules on the flowing out of the local variable copied into each of the ORed sequences. [1] A local variable flows out of the composite sequence if it flows out of each of the operand sequences, as is the case for the above example. If the local variable is not assigned before the start of the composite sequence and it is assigned in only one of the operand sequences, then it does not flow out of the composite sequence. For example: */
sequence q_no_flow_out; // ch2/2.7/or_multi.sv
int v_x, v_y;
((a ##1 (b, v_x = data, v_y = data1) ##1 c) or // v_x and v_ y assigned
(d ##1 (`true, v_x = data) ##0 (e==v_x))) // v_x assigned, v_ y unassigned
// Thus, v_x flows out, and v_y does not flow out
##1 (v_y==data2); //  Local variable v_y referenced in expression where it does not flow.
/ Illegal: v_y cannot be read in thread 2 because it was not uninitialized
// in the thread or during the initialization of the local variable at declaration.
endsequence : q_no_flow_out
sequence q_flow_out1; // OK
int v_x, v_y;
((a ##1 (b, v_x = data, v_y = data1) ##1 c) or // v_x and v_ y assigned
(d ##1 (`true, v_x = data, v_y=0) ##0 (e==v_x))) // v_x and v_ y assigned
##1 (v_y==data2);
endsequence : q_flow_out1

Thus, use the Boolean && || for the sequence and or needs to be differentiated, as they are handled differently by SVA.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
3

In reply to 100rabhh:

which would be the correct way of writing the property (scenario is: for a valid signal, seq1 and either seq2 or seq3 needs to be high.
Eg: property P1
@(posedge clk)
valid-> seq1 && (seq2 || seq3);
endproperty
property P2
@(posedge clk)
valid-> seq1 and (seq2 or seq3);
endproperty.
if P1 is incorrect, why cannot we use logical symbols while using sequences(&& or ||)?

It depends on what you want to accomplish.
If you want to check sequence has finished execution then you can actually use logical check.
For example, let’s say you want to check the sequences have finished execution on valid. Then

property p1;
@(posedge clk) valid |-> seq1.triggered && (seq2.triggered || seq3.triggered);
endproperty

But this will expect the condition to be true on all valid, so you tweak it.

property p1;
@(posedge clk) $rose(valid) |-> seq1.triggered && (seq2.triggered || seq3.triggered);
endproperty