Invalid temporal expression in SVA

In reply to SriGanesh D:
A few errors + a recommendation:

  1. (data_syn and loc_awlen) // ERROR
    // *** “and” is a sequential operator, you need &&
  2. Expression defined as a sequence
    No need to do this, particularly since there are different rules for sequences and expressions. Use the let instead
  3. Antecedent is multithreaded, limit to one match
    An antecedent with multiple threads requires ALL threads to be tested for a success.
    Use the first_match() or the goto operator
    property p;
bit x;
w ##1 (a, x=1)[->1] |-> b;  // goto is preferred for style, first_match() is OK though
endproperty

 // <--------------------The fix ---------------------------------->  
 let addr_syn=(S_AXI_AWREADY && S_AXI_AWVALID);
 let data_syn=(S_AXI_WREADY && S_AXI_WVALID);
 let resp_syn=(S_AXI_BVALID && S_AXI_BREADY); 
    
   property axi_id_check;
       // @(posedge clk);
        int loc_awid;
        int loc_awlen;
    
        int loc_wid[bit];
        int loc_bid;
    
   (addr_syn, loc_awid = S_AXI_AWID, loc_awlen = S_AXI_AWLEN) 
   //Getting the AWID and AWLEN
   first_match(##[0:$]((data_syn && loc_awlen), loc_wid[S_AXI_WID] = S_AXI_WID, loc_awlen=loc_awlen-1))
   // Getting all WID of write data
       |=>(resp_syn, loc_bid = S_AXI_BID) ##0 id_check(loc_awid,loc_wid,loc_bid);
        //Getting respones ID BID.    
   endproperty 
    
    //.. 
    A1:assert property(axi_id_check);

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: