Hi , i want to assert using SVA that signal B is stable ( its value is unchanged whether it was 1 or 0 at the start of rise of signal A ) during the rise and fall of signal A how can i do that
In reply to bassem yasser:
Assuming signals “a” and “b” are outputs of FFs, this will work:
http://systemverilog.us/vf/test_ab.sv // includes a simple testbench
http://systemverilog.us/vf/test_ab.png // results
property p_ab;
bit v;
($rose(a), v=b) |=> b==v[*0:$] ##1 $fell(a);
endproperty
ap_ab: assert property(@ (posedge clk) p_ab);
// A variation
ap_ab2: assert property(@ (posedge clk)($rose(a), v=b) |=> $past(b)[*0:$] ##1 $fell(a);
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
- VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
- http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
- “Using SVA for scoreboarding and TB designs”
http://systemverilog.us/papers/sva4scoreboarding.pdf - “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
October 2013 | Volume 9, Issue 3 | Verification Academy - SVA in a UVM Class-based Environment
SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
In reply to ben@SystemVerilog.us:
Hi Ben,
Would it be okay to use until_with in this case?
($rose(a), v=b) |=> (b==v until_with $fell(a));
Complementarily,
($fell(a), v=b) |=> (b==v until_with $rose(a));
Thank you for your response.
In reply to kernalmode1:
In reply to ben@SystemVerilog.us:
Hi Ben,
Would it be okay to use until_with in this case?
($rose(a), v=b) |=> (b==v until_with $fell(a));
Complementarily,
($fell(a), v=b) |=> (b==v until_with $rose(a));
Absolutely yes. Actually, my response should have been
($rose(a), v=b) |=> b==v[*0:$] ##1 $fell(a) && b==v; // same as with the until_with
Ben SystemVerilog.us
In reply to ben@SystemVerilog.us:
In reply to kernalmode1:
Absolutely yes. Actually, my response should have been
($rose(a), v=b) |=> b==v[*0:$] ##1 $fell(a) && b==v; // same as with the until_with
Ben SystemVerilog.us
Hi Ben can i use $stable , and how ?
In reply to bassem yasser:
$rose(a) |-> $stable(b) until_with $fell(a));
It’s not clear what b can do on the fall of a.
In reply to dave_59:
// minor adjustments for the 1st cycld
##1 $rose(a) |-> $stable(b) until_with $fell(a));
// another option
$rose(a) |=> $stable(b}[×1;$] ##0 $fell(a);
Ben systemverilog.us
// All roads lead to Rome…