I need help to write an assertion for following,
-We have 2 signals a & b.
-Falling of signal ‘a’ is triggering condition.
-From the fell of ‘a’, count no of pos edges of signal ‘b’ within 120ns.
-if count(no of pos edges of ‘b’ less than or equal to two assertion should fail, else (>2) assertion should pass
-Assertion should be active at all times
Be cause you have an analog type of requirement (the 120ns). I would use tasks, as described in my paper,link below.
task automatic t_AB;
bit status;
int count:
if ($fell(a))
fork
begin : the120ns
#120ns
end
begin : thecount
// count the b's
Statis=1: // under count values
end
join_any
assert(status);
endtask
always @(posedge clk)
fork t_AB();
join_none
Above is a framework for your code, you need to tune it.
See my paper 1) SVA Alternative for Complex Assertions
Verification Horizons - March 2018 Issue | Verification Academy
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
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
In reply to ben@SystemVerilog.us:
I am new to writing SVA assertions. This might not be 100% correct, I am just thinking this from a logic perspective on how to write it as of now.
task automatic t_AB;
bit status;
int count:
if ($fell(a))
fork
begin : the120ns
//#120ns: //wait till timeout
begin
`uvm_do_with(delay, {delay == 12000;}); //put some delay here equivalent to 120 ns units. can be a delay sequence too like here.
end
begin : thecount
// count the b's
//@(posegde clk) // the process inside fork is already spawned on a posedge clk.
$rose(b)|->(count ++);
end
end
join_any
assert(count>=2);
endtask
always @(posedge clk)
fork t_AB();
join_none
In reply to ben@SystemVerilog.us:
Be cause you have an analog type of requirement (the 120ns). I would use tasks, as described in my paper,link below.
task automatic t_AB;
bit status;
int count:
if ($fell(a))
fork
begin : the120ns
#120ns
end
begin : thecount
// count the b's
Statis=1: // under count values
end
join_any
assert(status);
endtask
always @(posedge clk)
fork t_AB();
join_none
Above is a framework for your code, you need to tune it.
See my paper 1) SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
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
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
- https://verificationacademy.com/news/verification-horizons-march-2018-issue
- SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
- SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
Hi Ben,
In your code I see that on every posedge clk, the task is called under a fork. This will just create multiple threads. Instead of this can’t we just move the alywas @posedge clk internal to the mutiple processes running inside fork .join. something like this:
task automatic t_AB;
bit status;
int count:
bit a_fall;
always@(posedge clock) begin: block_to_disable
if ($fell(a)) begin
a_fall = 1;
disable block_to_disable;
end
fork
begin
begin : the120ns
#120ns: //wait till timeout (excute a delay sequence here that waits till 120ns)
end
begin : thecount
// count the b’s
always@(posegde clk)
$rose(b)|->(count ++);
end
end
end
join_any
assert(count>=2);
endtask
fork t_AB();
join_none
In reply to ben@SystemVerilog.us:
Here are the 2 solutions, one woth the task approach and one woith SVA.
This is a complete testbench for the assertions.
import uvm_pkg::*; `include "uvm_macros.svh"
module top;
timeunit 1ns; timeprecision 100ps;
bit clk, a, b;
event e_pass, e_fail;
default clocking @(posedge clk); endclocking
initial forever #10 clk=!clk;
// -Falling of signal 'a' is triggering condition.
// -From the fell of 'a', count no of pos edges of signal 'b' within 120ns.
// 120ns is 6 clk periods
// -if count(no of pos edges of 'b' less than or equal to two
// assertion should fail, else (>2) assertion should pass
function int do_count (int d, bit b);
if($rose(b)) return d+1'b1;
else return d;
endfunction
property p_a2b;
int v_count=0;
$fell(a) |-> ( (1, v_count=do_count(v_count, b))[*1:$] intersect (1[*7]))
##0 v_count > 2;
endproperty
// the (1[*7])) account for the start repeat + 6 more
ap_a2b: assert property(@ (posedge clk) p_a2b );
task automatic t_AB;
automatic bit status=0;
automatic int count=0;
fork
begin : the120ns
#120ns;
end
begin : thecount
forever begin : fr1
// count the b's
@(posedge clk);
if($rose(b)) count=count+1'b1;
if(count>2)status=1;
end : fr1
end
join_any
if(status) -> e_pass;
else -> e_fail;
assert(status);
endtask
always @(posedge clk)
if ($fell(a)) fork t_AB();
join_none
initial begin
bit va, vb;
repeat(300) begin
@(posedge clk);
if (!randomize(va, vb) with
{ va dist {1'b1:=1, 1'b0:=10};
vb dist {1'b1:=1, 1'b0:=1};
}) `uvm_error("MYERR", "This is a randomize error")
a <= va;
b <= vb;
end
$stop;
end
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
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
- SVA Alternative for Complex Assertions
Verification Horizons - March 2018 Issue | Verification Academy - SVA: Package for dynamic and range delays and repeats | Verification Academy
- SVA in a UVM Class-based Environment
SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
FREE BOOK: Component Design by Example
… A Step-by-Step Process Using VHDL with UART as Vehicle
http://systemverilog.us/cmpts_free.pdf
In reply to ben@SystemVerilog.us:
Made an edition in the function to make it inclusive of all needed arguments. This insures that all needed variables are sampled correctly, and it enhances readability. In general, it is better to avoid side-tear effects when using functions.
The function header is now
function int do_count (int d, bit b);
// did not have the "bit b" before
Ben
HI Ben ,
i think above assertion code can be used with modification for checking the following condition
- 128 iterations of clock pattern(16 posedge clock cycles followed by 8 cycles of clock should be absent) with clock period of 500ps
- if less then 16 iterations are found … then it should throw error .
type or paste code here
``
// -Falling of signal 'a' is triggering condition.
// -From the fell of 'a', count no of pos edges of signal 'b' within 7500ps.
// 7500ps is 16 clk periods
// 4000ps 8clk period --> absent
// -if count(no of pos edges of 'b' less than or equal to two
// assertion should fail, else (>16) assertion should pass
function int do_count (int d, bit b);
if($rose(b)) return d+1'b1;
else return d;
endfunction
property p_a2b;
int v_count=0;
$fell(a) |-> ( (1, v_count=do_count(v_count, b))[*1:$] intersect (1[*16]))
##0 v_count > 16;
endproperty
// the (1[*7])) account for the start repeat + 6 more
ap_a2b: assert property(@ (posedge clk) p_a2b );
`
1) how to check for 8 clock cycle absent & 128 iterations .. can you help me on this .
Regards
rohit[Ben] 1) You have a situation where if($fell(a)) then
- You have 128 iterations of 16 cycles of clocks _ 8 time cycles of no clocks.
- Within each iteration you assert the existance of 2+ rose(b)
- After all the 128 iterations, you assert the existance of 16+ rose(b)
2) SVA needs clocks to work (model uses "clk"). Using a TB clock (e.g., "clkr") cannot test the clk.
3) If you have ONE iteration, you can use SVA for the test of rose(b) in 16 cycles,
and then thru the sequnce_match_item, call a task to check the lack of clocks.
In https://www.edaplayground.com/x/vaVy // untested
I tried looping the property 128 times, byt was reminded that
// Delays or wait statements in match item task calls are not supported.
The core of the code is:
```
function int do_count (int d, bit b);
if($rose(b)) return d+1'b1;
else return d;
endfunction
// My property for these requirements:
// @ fell(a) we have 16 posedge clk. "b" must change to 1'b1 twice or more.
// Following the 16 posedge, we must check for 4000ps of no clocks.
property p_a2b;
int v_count=0, v_total=0;
$fell(a) |->
(((1, v_count=do_count(v_count, b), v_total=do_count(v_total, b))[*1:$] intersect (1[*16]))
##0 (v_count >=2, t_AB())); // [*128] ##0 v_total>16;
// Delays or wait statements in match item task calls
// are not supported.
endproperty
// [Ben] ?? the (1[*7])) account for the start repeat + 6 more
ap_a2b: assert property(@ (posedge clk) p_a2b ) p1++; else f1++;
task automatic t_AB();
automatic int err=0;
fork
begin : the4000ps
#4000ps;
end
begin : thecount
forever begin : fr1
@(posedge clk) err=1;
end : fr1
end
join_any
assert(err);
endtask
```
4) To do the 128 interations that include cycles with clk, and cycles without clk,
you have to use tasks.
https://www.edaplayground.com/x/8pxN // untested
(In this code, I used 12 iterations instead of 128)
The core of the code is
```
always_ff @(posedge clk) begin
if($fell(a)) t_ab_iteration();
end
// @ fell(a) we have 16 posedge clk. "b" must change to 1'b1 twice or more.
// Following the 16 posedge, we must check for 4000ps of no clocks.
task automatic t_ab_iteration(); // p_a2b;
int v_count=0, v_total=0; // task called at $fell(a)
repeat(128) begin : iterations // change 12 to 128
repeat(16) begin : repeat16
@(posedge clk) if($rose(b)) begin : the16cyles
v_count++; v_total++;
end: the16cyles
end :repeat16
t_noclk8(); // check for noclocks in 4000ps
am_2in16: assert(v_count >=2); // check count per iteration
v_count=0; // reset iteration count for rose(b)
end : iterations
// (((1, v_count=do_count(v_count, b), v_total=do_count(v_total, b))[*1:$] intersect (1[*16]))
// ##0 (v_count >=2, t_AB()))[*128] ##0 v_total>16;
// Delays or wait statements in match item task calls are not supported.
am_16intoral: assert(v_total >=16); // check count per iteration
endtask
task automatic t_noclk8();
int err=0;
fork
begin : the4000ps
#4000ps;
end
begin : thecount
forever begin : fr1
@(posedge clk) err=1;
end : fr1
end
join_any
assert(err);
endtask
```
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
https://systemverilog.us/vf/Cohen_Links_to_papers_books.pdf
If you have a clk disable signal, you can use that signal in SVA instead of calling a task, thus keeping the whole assertion in SVA.
You can then use the assertion in FV.