Asynchronous Assertions

SystemVerilog
, ,
1

Hi,
I have multiple asynchronous signals without clock .
The input should be in sequence Signal A1 , A2 , A3.
Can you suggest me way to write immediate assertion so that I can check sequence.
Thank You.

2

In reply to Satputesb:

The input should be in sequence Signal A1 , A2 , A3.

Unclear what that really mean?
input==value_A1 then value_A2 then Value_A3
or input== constant_A1 then constant_A2 then Constant_A3?
Show some code; What causes a transition?

3

In reply to Satputesb:
You still ar enot clear, sorry. WHere is the observaltion of these 3 signals? and when?
Are you saying you have an input in1 where in1–A1, then in1==A2, then in1==A3?
What triggered the selection? I started a module but quickly gave up.
In asynchronous designs, state transitions occur upon events, like sig1==1 then state=N,
then from state N sig2==1 transtions state to state K, and so on.


module m;
  bit A, B, C, in1;  
  bit[1:0] state; 
//  First input signal A1 asserted then input signal A2 and then input signal A3.
// This is the sequence in which A1 , A2 and A3 are arriving. 
  always_latch begin
     if(state==2'b00 && A ) state==2'b01; 
     if(state==2'b01 && B && !A ) state==2'b10; 
     if(state==2'b10 && C && !A && !B) state==2'b11; 
  end
4

In reply to ben@SystemVerilog.us:

Let me re frame the question there are three different “single bit inputs”
Input A1(Single bit);
Input A2(single bit);
Input A3(Single bit);

All these inputs arrive in specific sequence. which
Fisrt A1 is asserted and kept high. Then after sometime A2 is asserted and kept high. And then A3 is asserted and kept high. These inputs are externally driven. I would like to write assertion for checking if these are being asserted in specific sequence.
Thank you

5

I think the below sva code suffice your requirement. Let me if this meets your criteria.


property seq_check;
@(posedge clk);
A1 |-> A1 [*1:$] ##1 (A2 && A1) [*1:$] ##1 (A3 && A2 && A1) [*1:$];
endproperty

assert property(seq_check);

//You may as well use $rose(A1) before the implication operator.

6

In reply to Satputesb:
The following works but it has an issue if B and C occur simultaneously because the order of processing of the fork elements is not predictable. Thus if fork2 is processed before fork1 you can get an OK. The concept demoed here may guide you into a better approach.


module m;
    `include "uvm_macros.svh"     import uvm_pkg::*;
  bit A, B, C, run;   
  event t0, t1, ta, tb, tc;  

    /*nLet me re frame the question there are three different "single bit inputs"
    Input A1(Single bit);
    Input A2(single bit);
    Input A3(Single bit);
    
    All these inputs arrive in specific sequence. which
    Fisrt A1 is asserted and kept high. 
    Then after sometime A2 is asserted and kept high. 
    And then A3 is asserted and kept high. 
    These inputs are externally driven. 
    I would like to write assertion for checking if these are being asserted in specific sequence. */ 

    task automatic t_abc; 
        automatic bit a, b, c, oka, okb, okc; // history + status 
        -> t0;  // debug
        fork
            fork1: begin 
                @(A) a=1;
                am_A1_B0_C0: assert(!B && !C && !b && !c) oka=1;
                -> ta;
            end
            fork2: begin 
                @(B) am_A1_B1_C0: assert(!A && !C && a && !c) okb=1;
                b=1; 
                -> tb;
            end
            fork3: begin 
                @(C) am_A1_B1_C1: assert(!A && !B && a && b) okc=1;
                c=1; 
                -> tc;  
            end
        join
        am_ABC: assert(oka && okb && okc);
        -> t1;  
    endtask 

    always @(posedge run) begin
        t_abc(); 
    end

	initial begin 
        bit a0, b0, c0;
		repeat(250) begin 
			#20
            if (!randomize(a0, b0, c0, run)  with 
					{ a0 dist {1'b1:=1, 1'b0:=4};
					  b0 dist {1'b1:=1, 1'b0:=4};
                      c0 dist {1'b1:=1, 1'b0:=4};
                      run dist {1'b1:=1, 1'b0:=15};
					}) `uvm_error("MYERR", "This is a randomize error")
            #5; A=a0; B=b0; C=c0; 
		end 
		$stop; 
	end 

endmodule

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** 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) https://rb.gy/cwy7nb
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

7

In reply to sureshhs:

I think the below sva code suffice your requirement. Let me if this meets your criteria.


property seq_check;
@(posedge clk);
A1 |-> A1 [*1:$] ##1 (A2 && A1) [*1:$] ##1 (A3 && A2 && A1) [*1:$];
endproperty
assert property(seq_check);

//You may as well use $rose(A1) before the implication operator.

There is NO clk, it is asynchoous!

8

In reply to Satputesb:

A couple of things you do not mention. What happens after A3 goes high? Does you care? Do you expect A1-A3 to go low in any order? Do you need to repeat the check once the sequence is detected? I’m going to assume you don’t care what happens after A3 goes high. I prefer to use wait statements rather than events.

 bit A1,A2,A3;
  bit OK;
  
  initial  begin
    OK = 0;
    fork
      begin
        wait (A1)  assert (!A2 && !A3);
        wait (!A1) assert (OK);
      end
      begin
        wait (A2)  assert (A1 && !A3);
        wait (!A2) assert (OK);
      end
      begin
        wait (A3) assert (A1 && A2);
        OK = 1;
        wait (!A3);
      end
    join
  end

If you need to repeat this sequence check then this code will have to be modified depending on your answers.

9

In reply to dave_59:

A better approach, thanks,
Ben