Assertion checker for interface protocol

UVM
1

Depending on other signals (not shown) you can have the following relationships between CSEL and ACK.

  1. CSEL , ACK immediately asserts. Fine
  2. CSEL , ACK will assert some cycles later.
  3. Back to back transactions, all valid.

My main issue is identifying a “unique” antecedent. In scenario 2, how do I cause the first attempt to fire, but prevent the following 2 from occurring. Is there some way to “lock-out” the assertion until it completes? There is no pipelining on this bus.

csel |-> (ack==0)[*0:10] ##1 ack ; // not unique, fails scenario 2
$rose(csel) |-> (ack==0)[*0:10] ##1 ack ; // unique, but fails scenario 3 (only catches the 1st instance)

2

In reply to bmorris:

Is there some way to “lock-out” the assertion until it completes?

  • In the antecedent test for an entry gate, a module variable
  • If successful entry, lock that gate.
  • If pass or fail, release the gate

Below is an example that I had before. It uses the sequence-match-item and function call. Upon pass or fail, that action item is used.


module thruout2;// /ch10/10.27/thruout2.sv
  bit clk, sof, eof;
  bit busy_sof;
  default clocking @(posedge clk); endclocking
  function void setval4busy(bit d);
   busy_sof=d;
  endfunction
  // This is not catching multiple sof's and one eof within valid.
  // It should check that for one sof, there should be only one eof.
  ap_sof_eof: assert property
   // Once antecedent fires, no other one will fire again 
   ((sof && busy_sof==1'b0, setval4busy(1'b1)) |-> 
    ##[1:5] (eof)) setval4busy(1'b0); // reset flag if property is true
                   else  setval4busy(1'b0); // reset flag if property is false 
    
  ap_neversof_when_busy: assert property(not(sof && busy_sof));
endmodule

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

3

The solution above is more of a lockout of other assertions until the current one completes.
It uses a semaphore. If this is what you want, you may want to add another assertion that states that no other valid potential assertions occur during this lockout.

Another topic of uniqueness is that each thread s unique, and the ending of one thread does not complete other current threads. I address that at:
https://verificationacademy.com/forums/systemverilog/assertion-expected-data-check/review-users-question

Uniqueness This is exclusivity or uniqueness of each attempted thread sequences).I explain this issue in my SVA Handbook 4th Edition, I also addressed that topic at counting number of events on clock a, while clock o is forbidden | Verification Academy
Hint: use the module variables int ticket, now_serving;

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