[SVA] Need help in writing assertion for this requirement

SystemVerilog
,
2

In reply to BhaRath@Intel:
You are trying to express your requirements using an SVA notation with so many implication operators that it is hard to really understand what you need.
You need to express your requirement in English. The implication opr has a very significant meaning. I attempted at making sense on what you wrote, but it does not make sense. I am posting my attempt, not as a solution, but as failed attempt because it is totally unclear.


property_statement ::=   // 1800'2017
property_expr ;
 | case ( expression_or_dist ) property_case_item
   { property_case_item } endcase
| if ( expression_or_dist ) property_expr
  [ else property_expr ]

// ??? 
ap_very_ambiguous: assert property(@ (posedge clk) $rose(sig1) |-> 
  if(sig4==1) $rose(sig5) ##1 $fell(sig1) ##1 $fell(sig5)
  else  $rose(sig1)-> $rose(sig4)->$rose(sig5)-> $fell(sig1)-> $fell(sig4)-> $fell(sig5)
// Way way too many |->. 
// Also, all these 4rose at the same time? Can you use the && or the ##0? 
// What is the English requirement 

//????
 //  -It should be error if sig1->
 //  followed by sig5 asserted without sig1,
  ap_ambiguous_Englis: assert property(@ (posedge clk) not sig5 && sig1 );

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

** 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 | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers: