Alternative via "throughout" and "s_until_with"

SystemVerilog
,
1

Specification ::

  • When request is asserted that grant is asserted the very next clock .
    grant must have been de-asserted prior to it’s assertion
  • grant must remain asserted as long as request is asserted
  • grant must de-assert the very next clock after request is de-asserted

  //   SOLUTION ::

  property  req_gnt ;

   @( posedge  clk )   $rose( req ) |->  ##1  $rose( grant ) ##0 grant[*1:$] ##0 $fell( req ) ##1 $fell( grant )  ;   

  endproperty

I then tried a few alternatives ::


  //   ALTERNATIVE1  ::

  sequence  seq_req_grant ;
  
   $rose( req )  ##1 $rose( grant ) ;  //   Implication  can't  be  Used  in  Sequence  ,  hence  ##1  !!  
                                       
  endsequence

  property  req_assert ;
  
     grant  s_until_with  $fell( req )  ;   //   ' grant '  remains  Asserted  till  ' req '   Goes  Low  !!  

  endproperty
  
  property  req_assert_grant ;
  
     seq_req_assert |=>  $fell( grant )  ;    //  ERROR  with  antecedent  !!  
    
  endproperty

  property  req_gnt ;

   @( posedge  clk )   req_grant  |->  req_assert_grant ; 

  endproperty

 


 //   ALTERNATIVE2  ::

   sequence  req_grant ;
  
   $rose( req )  ##1 $rose( grant ) ;  
                                      
  endsequence

  property  req_assert ;
  
     grant  throughout  ##[1:$] $fell( req )  ;   

  endproperty
  
  property  req_assert_grant ;
  
     req_assert |=>  $fell( grant )  ;    //  ERROR  with  antecedent  !!   
    
  endproperty

  property  req_gnt ;

   @( posedge  clk )   req_grant  |->  req_assert_grant ;

  endproperty

I believe using a property as antecedent of Implication Operator is Illegal .

Have a few questions ::

  1. Any suggestions for ALT1 and ALT2 ?
  2. For incomplete assertion , “s_until_with” throws a Failure at End of Simulation
    This seems like a better solution but does it have any implications ?
2

In reply to MICRO_91:
I like the way you clearly expressed the requirements. However, I am critical of the way you try to resolve each piece in a collective way by combining them in complex properties.
In general, it is best to write smaller assertions than larger more complex ones. Thius is my solution.


// 1) When request is asserted that grant is asserted the very next clock . 
//    grant must have been de-asserted prior to it's assertion
    $rose( req ) |->  ##1 $rose( grant);  
   
// 2) grant must remain asserted as long as request is asserted
    $rose( grant) |-> grant && req[*0:$] ##1 !req;  
   // Same as 
    $rose( grant) |-> grant && req s_until ##1 !req;  

// 3) grant must de-assert the very next clock after request is de-asserted 
   $fell(req) |->  ##1 $fell(grant);

I committed the strong in the qualification of the consequent. If this is of importance, then add the strong; for example:
rose( grant) |-> strong(grant && req[*0:] ##1 !req);

/If the strong or weak operator is omitted, then the evaluation of the sequence_expr (interpreted as a property) depends on the assertion statement in which it is used. If the assertion statement is assert property or assume property, then the sequence_expr is evaluated as weak(sequence_expr). Otherwise, the sequence_expr is evaluated as strong(sequence_expr)./

I believe using a property as antecedent of Implication Operator is Illegal .

You are correct. However, the implies has a similar connotation to the |-> but with differences.
The implies has the form: property_expr1 implies property_expr2
It evaluates to true if either property_expr1 evaluates to false or property_expr2 evaluates to true. With the exception of vacuity, it is equivalent to : (not property_expr1) or (property_expr2). Thus, with the implies property operator, both sides of the operator are properties start at the same evaluation time and may end at different cycles.
Also, An evaluation attempt of a property of the form property_expr1 implies property_expr2 is nonvacuous if, and only if, the underlying evaluation attempt of property_expr1 is true and nonvacuous, and the underlying evaluation attempt of property_expr2 is nonvacuous.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

3

In reply to ben@SystemVerilog.us:

is

$rose( grant) |-> grant && req[*0:$] ##1 !req;

same as

$rose( grant) |-> (grant && req)[*0:$] ##1 !req;

?

4

In reply to Jeff_Li_90:

Yes because the & & is an expression operator.
The expression grant && req is first evaluated before the sequential repeat operator.
However, the following is differen because of the ‘and’ sequential operator.

grant and req[*0:] ##1 !req; // same as (grant) and (req[*0:] ##1 !req) ;

For the property to be true, both concurrent sequences starting at the same cycle must be true.