Assertion protocol checker

I’ve not got much experience with sequences within assertions , and have a seemingly simple protocol I want to write some checks for.

Three signal strobes ( single cycle) exist:
Start
Stop
End
Any number of cycles can occur in-between strobes.

I want assertions that check
1 - every start is followed by an end or a stop (start to start back to back cannot occur)
2 - every stop or end is followed by a start ( no back to back stops or ends)

So valid sequences are
Start stop start
Start end start

Examples of invalid sequences are
Start start
Start end end
Start stop stop
Start stop end

I have some sequences and assertions that I’ve written which fire and pass when correct sequences are present, but I cannot get my head around how to trap the invalid occurrences.

Any pointers please would be appreciated

Ta

In reply to Rocketfingers:
You need a supporting logic for the never cases that you identified.
I added the “started” flag that gets set when started, and reset when stop or done (end is a reserved word). For the never sequences, here is an example

ap_start_start: assert property(not(start ##1 (start && started[->1]))  );

That states that there should never be sequence start followed by an occurrence of start and the started flag. Come to think of it, could that be replaced with just:

ap_start_start: assert property(not( (start && started))  );

Below is my code with a testbench


/* I want assertions that check
1 - every start ( // 1 cycle)is followed by an end or a stop (start to start back to back cannot occur)
2 - every stop ( // 1 cycle ) or end (done  // 1 cycle)is followed by a start ( no back to back stops or ends)

So valid sequences are
Start stop start
Start end start

Examples of invalid sequences are
Start start
Start end end
Start stop stop
Start stop end */
import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
    timeunit 1ns;     timeprecision 100ps;    
    bit clk,start, stop, done, started; 
    default clocking @(posedge clk); 
    endclocking
    initial forever #10 clk=!clk;  
    
    function  void set_started(bit a); 
        started = a; 
    endfunction : set_started   
    // 1 - every start is followed by an end or a stop (start to start back to back cannot occur)
    ap_start_stopr_or_done: assert property( 
      (start, set_started(1)) |=> stop[->1] or done[->1]) 
      set_started(0); else set_started(0);  
    
    //  every stop ( // 1 cycle ) or end (done  // 1 cycle)is followed by a start ( no back to back stops or ends)
    ap_stop_done_to_start: assert property((stop || done) |=> start[->1] );
    
    //Start .. start with NO done or stop, i.e, when in the started state
    
    ap_start_start: assert property(not(start ##1 (start && started[->1]))  );  
    // Start end end
    ap_start_end_end: assert property(not(done && started==1'b0));  
    
    // Start stop stop
    ap_start_stop_stop: assert property(not(stop && started==1'b0));  
    
    // Start stop end 
    ap_start_stop_end: assert property(not(done && started==1'b0)  );  
       
    initial begin 
        bit va, vb, vc; 
        repeat(200) begin 
            @(posedge clk);   
            if (!randomize(va, vb, vc)  with 
            { va dist {1'b1:=1, 1'b0:=3};
            vb dist {1'b1:=1, 1'b0:=2};   
            vc dist {1'b1:=1, 1'b0:=2};      
        }) `uvm_error("MYERR", "This is a randomize error")
        start <= va; 
        stop <= vb;
        done <= vc;
    end 
    $stop; 
end 
endmodule   
 

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


  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

In reply to ben@SystemVerilog.us:

Many thanks I need to now digest this code

In reply to ben@SystemVerilog.us:

ok, so upon some reflection, I get how……:


function  void set_started(bit a); 
        started = a; 
    endfunction : set_started   
    // 1 - every start is followed by an end or a stop (start to start back to back cannot occur)
    ap_start_stopr_or_done: assert property( 
      (start, set_started(1)) |=> stop[->1] or done[->1]) 
      set_started(0); else set_started(0);


… is working. well… to my limited understanding I see this as the mechanism to call the function controlling the flag status, based on the sequencing of the start/stop and done.
This assertion never fails (?)

to my eyes, and very much in the style of “many different ways of skinning a cat”, would the following have not achieved the same:


always @(posedge clk or negedge !rst_n)
        if (!rst_n) started <= '0;
        else begin
            if (start) started <= '1;
            else if (done || stop) started <= '0;
        end

a little more supporting logic? but to my eyes (I suppose as a less hardcore ABV experienced engineer) easier to follow?

am I right? do they achieve the same thing?

In reply to Rocketfingers:

For the fail:


(start, set_started(1)) |=> (stop[->1] or done[->1])
                             and ( !start[*0:$]) 
 

The use of the “always” instead of the function would work in this case.
The use of the function and sequence match item calls the function only the attempted assertions; thus it is linked to that one attempt only. In most cases that is important.

Ben Ben@systemverilog.us

In reply to ben@SystemVerilog.us:

Other suggestions



  $rose(start) |=> !start until (stop or end);
  $rose(stop) |=> !stop until (start);
  $rose(end) |=> !end until (start);
 

Ben Ben@systemverilog.us

In reply to Rocketfingers:
Use $sampled(…


always @(posedge clk or negedge !rst_n)
        if (!rst_n) started <= '0;
        else begin
            if ($sampled(start)) started <= '1;
            else if ($sampled(done) || $sampled(stop)) started <= '0;
        end