How do I debug "Property operator usage is not allowed in sequence context."?

Hello,

I am currently trying to write an assertion and need to make use of the property operator

[*0:$]

. I tried using until but my compiler complains about it so I’m not sure if it is supported by the version of VCS that I’m using.

Anyway, I have two assertions as follows:


  property rsp_not_empty_alert_high_p(empty, alert);
    @(posedge clk) empty == 0 |=> alert == 1;
  endproperty

  property alert_bit_clear_p(reg_push, reg_alert_bit, reg_addr, raw_alert_bit);
    @(posedge clk) (reg_push and reg_alert_bit and (reg_addr == 32'h20000080 or reg_addr == 32'h20000088)) |-> ##3 $fell(raw_alert_bit);
  endproperty

I am trying to assert the properties as follows:


rsp_not_empty_alert_check: assert property (rsp_not_empty_alert_high_p(rsp.empty, 
                                                                       raw_alert[27]) [*0:$] ##1
                                            alert_bit_clear_p(reg.push,
                                                              reg.data[27],
                                                              reg.data[63:32],
                                                              raw_alert[27]));

When I try to run this, I get the error message saying “Property operator usage is not allowed in sequence context.”.

I am at a bit of a loss as to how to deal with this. Any help would be greatly appreciated!

In reply to sidmodi:
Looks to me like you are coming from the VHDL world.
In sequences, you have the following operators that are not equivalent than logical operators:


and or // sequential operators
&& || //  expression logica operator 
// thus, when you write 
.. (reg_push and reg_alert_bit and (reg_addr == 32'h20000080 or reg_addr == 32'h20000088)) 
// You have 3 sequences, each 1-cycle wide
// Sice sequences can be 1-cycle wide the compiler does not complain.
// However, using 1-cycle  "and" "or" have different connotaton than using the logical && ||
The following does read better and expresses the intent better. 
.. (reg_push && reg_alert_bit && (reg_addr == 32'h20000080 || reg_addr == 32'h20000088)) 

// On 
 property rsp_not_empty_alert_high_p(empty, alert);
    @(posedge clk) empty == 0 |=> alert == 1;
 endproperty

rsp_not_empty_alert_check: assert property (rsp_not_empty_alert_high_p
                                (rsp.empty, raw_alert[27]) [*0:$] ##1
                                            alert_bit_clear_p(reg.push,
                                                              reg.data[27],
                                                              reg.data[63:32],
                                                              raw_alert[27]));
The actual arguments being passed to  property (rsp_not_empty_alert_high_p are not compatible with the formal arguments.  In your case, formal argument  
// If you are going to use formal arguments, If all formals are bits, 
// I prefer to use untyped as the type. 
// However, if you intend to use sequences, then declare the type as a sequence; 
// it makes the code more readable. 
    sequence q_ab(z, y); 
        z ##2 y; 
    endsequence  
    property p_abc(x,  sequence w);
      x ##1 w;
    endproperty 
    ap: assert property(@ (posedge clk)   $rose(c) |=>
           p_abc(d, q_ab(d, q_ab(a, b))));  

// However, if those assertions are used once, why do you really bother with all these arguments? Just go straight for the kill 
  ap_better: assert property(@ (posedge clk)   $rose(c) |=>
       d ##1 a ##2 b);  //   p_abc(d, q_ab(d, q_ab(a, b))));  

// Even better, Use the defaults clocking and disables 
default disable iff (rst);
default clocking @(posedge clk); 
endclocking

 ap_better: assert property( $rose(c) |=>
         d ##1 a ##2 b);  //   p_abc(d, q_ab(d, q_ab(a, b))));  

  

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

In reply to ben@SystemVerilog.us:

Hi Ben,

To be honest, I’m coming from the firmware world. I am quite new to the hardware description world.

I understand what you mean about the difference between ‘and/or’ and ‘&& / ||’. It makes sense to use the logical operators in my case.

What I am still not clear about is your explanation regarding the arguments being passed to the property. I am defining the property with arguments because I intend to use the same property to verify the functionality of multiple signals. With arguments, I can verify all those signals using the same property. All the parameters to the ‘rsp_not_empty_alert_high_p’ and ‘alert_bit_clear_p’ properties are bits.

What I am trying to achieve in plain language is the following:

Once asserted, I want the property ‘rsp_not_empty_alert_high_p’ to be true until ‘alert_bit_clear_p’ gets asserted.

I tried to do this by declaring two separate properties and then inserting a property operator between them in the assertion. I am not quite sure what I’m doing wrong here…

What you are attempting to do:

 
//  'rsp_not_empty_alert_high_p' to be true until 'alert_bit_clear_p' gets asserted. 
// Or, looking at you code 
    property rsp_not_empty_alert_high_p(empty, alert);
      @(posedge clk) empty == 0 |=> alert == 1;
    endproperty
   
    property alert_bit_clear_p(reg_push, reg_alert_bit, reg_addr, raw_alert_bit);
      @(posedge clk) (reg_push and reg_alert_bit and (reg_addr == 32'h20000080 or reg_addr == 32'h20000088)) |-> ##3 $fell(raw_alert_bit);
    endproperty 

// And then breaking it down to the core: 
// You want    
   (empty == 0 |=> raw_alert[27]) [*0:$]) until 
       (reg_addr == 32'h20000080 or reg_addr == 32'h20000088)) |-> ##3 $fell(raw_alert_bit)
// In SVA, you do have the "until" operator 
property_expr1 until property_expr2
/* "An until property of the non-overlapping form (i.e., until, s_until) evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 (called the terminating property) evaluates to true" */
// To me, the "until operator is confusing and hard o understand for complex properties 
// unless those properties are single bits.  For example: 
   $rose(req) |=> busy until ready); // Enhanced readability, and Identical to
// $rose(req) |=> busy[*0:$] ##1 ready ; // equivalent property expression

// Perhaps what you need is the "intersect of 2 sequences", something like: 
(empty == 0 ##1 raw_alert[27] |-> raw_alert[27]) [*1:$]) intersect 
       (reg_addr == 32'h20000080 || reg_addr == 32'h20000088) ##3 $fell(raw_alert_bit)
// Or in English, if (empty == 0 ##1 raw_alert[27]  then 
// raw_alert[27]) holds at all cycles While this sequence is true 
//    (reg_addr == 32'h20000080 || reg_addr == 32'h20000088) ##3 $fell(raw_alert_bit)                          

KISS Keep it simple
:)
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