SVA Assertion Two Valid signal shares one ready signal

SystemVerilog
,
1

I have question regarding the following condition to achieve in assertion.
There are two valid signals valid_a , valid_b share the common ready signal. Handshake can be valid_a ↔ ready or valid ↔ valid_b , then ready will stay high until either done_a or done_b asserted . Valid/Done signals are pulse only. In case, both valid comes at the same time , then valid_a will take ready signal then done_a comes, after some time ready will be asserted for valid_b as it was plused.

valid_a |-|_____________________

valid_b |-|_____________________

ready |--------------------||------------------|_

done_a |-|_____

done_b ____________________________________________|-|

I thought of doing tagging/counter, it won’t work if the counter/taggign is shared by two different event. Counter/taggign method will create race if they come at the same time. Another solution can be semaphore. Is there any another solution can be used ?

done_a can be asserted for other processes without valid_a
read will be high until done_a or done_b goes high for one cycle

2

In reply to kddholak:
The requirements are ambiguous. From what you wrote, I understood the following and converted as such to SVA. There are issues. You need to clarify the requirements. Consider many assertions that deal with each aspect of the 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; 
    ap_valida: assert property(@ (posedge clk) 
      valid_a |=> ready[*1:$] ##0 done_a ##1 !done_a);  

    ap_validb_noa: assert property(@ (posedge clk) 
      valid_b && !valid_a|=> ready[*1:$] ##0 done_b ##1 !done_b); 

    ap_validba: assert property(@ (posedge clk) 
      valid_b && valid_a |=>  done_a[->1] ##1 ready[*1:$] ##0 done_b ##1 !done_b); 
    // done_a can be asserted for other processes without valid_a 
    // Above can cause issues. Need some exclusion here. <<-------------------
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:
3

In reply to ben@SystemVerilog.us:

BTW, you need to address other conditions like:
valid_a ##e vslid_b ##4 ready ##0 done_(?)

You may also need support logic.

Your specs are weak; can’t expect good assertions with weak specs; sva is not the magic.
Writing good requirements is.
Ben systemverilog.us

4

Waveform Link…[i]
I have attached scenario where the above assertion will give false failure.

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:
6

In reply to ben@SystemVerilog.us:

Thanks, Ben, I used a different approach where I created the internal signal for the uniqueness of protocol instead of using a shared signal.