Question is
Signal A must nor be asserted until the first signal of B(it can be asserted on the same cycle of B).
how can we write an assertion for this ??
Signal A must nor be asserted until the first signal of B(it can be asserted on the same cycle of B).
The way you write this assertion is by first clearly define the requirements.
The way you stated, it sounds like the requirements are:
[*] At every clocking event either signal A==1’b0 or B==1’b1.
Thus, one can expect a sequence such as !A ##1 !A ##1 !A ##1 B
Such an assertion can be expressed as:
ap_AB: assert property(@ (posedge clk)!A or B );
If on the other hand, you meant to say:
[*] Following the rice of C, signal A==1’b0 until B
ap_CAB: assert property(@ (posedge clk) %rose(C) |->
!B[*0:$] ##1 C );
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
- 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:
“Signal A must not be asserted until the first signal of B(it can be asserted on the same cycle of B).”
1)assert property(@ (posedge clk) $rose(B) |-> $rose(A); //in case A needs to fire in same clock, 2 would also work for same.
2)assert property(@ (posedge clk) rose(B) |-> ##[0:] ($rose(A));
This also checks if B is still held high when A goes high.
3)assert property(@ (posedge clk) rose(B) |-> ##[0:] ($rose(A)) ##0 B;
In reply to kushagar:
In case you have a requirement that B should be held high till A asserts… This can be used.
- assert property(@ (posedge clk) rose(B) |-> B ##[0:] $rose(A);