[SVA] Need help in writing assertion for this requirement

SystemVerilog
,
4

In reply to BhaRath@Intel:
You still have some ambiguity in the English definition of the requirements, something that when translating the English into SVA clearly brings out. BTW, this is one of the nice things of SVA, it forces the user to clarify the requirements.
Specifically, you were ambiguous as to when the “then” means, SAME cycle or the NEXT cycle.
I made some assumptions for you, but you need to fix it according to your real requirements.
I also changed the name of clkreq to req.



module top; 
    timeunit 1ns/100ps; 
     bit clk, req, valid, force_on, force_on_ack, ack;  
     default clocking @(posedge clk); 
     endclocking
     initial forever #10 clk=!clk;  

     // 1.when req asserted I should check for valid that needs to be get asserted within 500clocks,
     // then ack should get asserted IN THE NEXT CYCLE.
     ap_req_valid: assert property(@ (posedge clk) $rose(req) |-> 
                                      first_match(##[1:500] valid) ##1 ack);  
    // first_match() is needed here 
    // -------------------- 
    // If force_on asserted then valid must be asserted IN THE NEXT CYCLE(?)
    // then (##0 or ##1 ?)force_on_ack must be asserted followed IN THE NEXT CYCLE by force_on deassert, 
    // valid deassert, force_on_ack deassert.  
    ap_force_on: assert property(@ (posedge clk) $rose(force_on) |-> 
       ##1 force_on_ack ##1 $fell(force_on) ##0  !valid ##0 !force_on_ack);  
       // ##0 or ##1 spec is poorly defined 
    // -----------------------
    /* In second case when force_on asserted it will check for valid (NExt or same cycle?) , 
  If valid already asserted due to clkreq it should go ahead 
  and check for force_on_ack assertion followed 
  we need to check for force_on deassertion and force_on_ack deassertion. */ 
  ap_force_on_valid: assert property(@ (posedge clk) $rose(force_on) ##1 valid |-> 
       ##1 force_on_ack ##1 $fell(force_on) ##0  !force_on_ack);  
 endmodule

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: