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.
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?
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
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
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.
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
…
- SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
- 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 - Papers:
- Understanding the SVA Engine,
Verification Horizons - July 2020 | Verification Academy - SVA Alternative for Complex Assertions
Verification Horizons - March 2018 Issue | Verification Academy - SVA in a UVM Class-based Environment
SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
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/
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!
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.