SVA Assertion Two Valid signal shares one ready signal

SystemVerilog
,
5

In reply to kddholak:
When you say the above assertion will give false failure, what I am interpreting is that your requirements are ill-defined. I now believe that what you are requesting is uniqueness in the valid/ready, meaning every valid has its unique interpretation of the common ready signal.
See my replies (last 2) at
https://verificationacademy.com/forums/systemverilog/assertion-req-and-gnt-signals

Thus, what is desired for this assertion is the exclusivity or uniqueness of each attempted thread sequences, meaning that one successful consequent does not terminate all concurrent attempts waiting for that consequent.

You also have one other requirement of priority to the “a” side. I did that by delaying the setup of the ticket/servingwhen this condition is true, thus giving the “a” side to start this setup first. Below is my untested code (it compiles and elaborates OK).
I also added my interpretation of the requirements. Hopefully, beltween the link above and my code, you can optimize the properties to your needs.
Again, everything is hinged on the requirements; bad requirements is the GIGO, and SVA will not save you here.


/* New clarifications on requirements: 
   a) every valid_a shall receive after "n" cycles a ready; 
      that ready if then immediately followed by a done_a
   b) every valid_b shall receive after "n" cycles a ready; 
      that ready if then immediately followed by a done_b
   c) valid_a sahll have a higher priority thatn valid_b.
   
   --------------------------------------------------------
   // OLD requirements
   1) There are two valid signals valid_a and valid_b. 
   2) Both valids share the common ready signal. 
   3) Handshake can be valid_a then ready then done_a 
   4) Handshake can be valid_a && !valid_b then ready then later done_a then later done_b
   5) ?? ready stay high until either done_a or done_b asserted .
   6) Valid/Done signals are pulse only.  
   7) done_a can be asserted for other processes without valid_a
   8) readY will be high until done_a or done_b goes high for one cycle */
module m; 
    bit valid_a, valid_b, ready, done_a, done_b, clk; 
    bit got_valid_a, got_valid_b; // for debug 
    int ticket, serving; // ticket number, unit being served 
    // support logic for requirement "a" and "b' 
    function automatic void set_got_valid_a (bit x);
      got_valid_a =x;
      if(x) ticket+=1'b1;  // increment the next ticket 
      else  serving +=1'b1; // increment the unit being served 
    endfunction

    function automatic void set_got_valid_b (bit x);
      got_valid_b =x;   
      if(x) ticket+=1'b1;  // increment the next ticket 
      else  serving +=1'b1; // increment the unit being served 
    endfunction

    property p_valid_a;
      int v_ticket;
      (@ (posedge clk) 
      // store the ticket, set state 
      (valid_a, v_ticket= ticket, set_got_valid_a(1'b1)) |=> 
               ready && v_ticket==serving [->1] ##0 (done_a, set_got_valid_a(1'b0)) ##1 !done_a); 
    endproperty 
    ap__valid_a: assert property(@ (posedge clk) p_valid_a ) else set_got_valid_a(1'b0);


    property p_valid_b_no_a; 
      int v_ticket;
      (@ (posedge clk) 
         (valid_b && !valid_a, v_ticket= ticket, set_got_valid_b(1'b1)) |=> 
          ready && v_ticket==serving [->1] ##0 (done_a, set_got_valid_a(1'b0)) ##1 !done_a); 
    endproperty 
    ap__valid_b_no_a: assert property(@ (posedge clk) p_valid_b_no_a ) else set_got_valid_b(1'b0);

    property p_valid_b_with_a; 
      int v_ticket;
      (@ (posedge clk) 
        (valid_b && valid_a) ##1 // wait 1 cycle for valid_a to set its things first
         (1'b1, v_ticket= ticket, set_got_valid_b(1'b1)) |=> 
          ready && v_ticket==serving [->1] ##0 (done_a, set_got_valid_a(1'b0)) ##1 !done_a); 
    endproperty 
    ap__valid_b_with_a: assert property(@ (posedge clk) p_valid_b_with_a ) else set_got_valid_b(1'b0);

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: