need help with assertion to check if ack goes high only during ##[3:5] cycles after valid is asserted, if ack doesnt happen in ##[3:5] then it should stay low for [6:10]
In reply to saikishorereddy:
need help with assertion to check if ack goes high only during ##[3:5] cycles after valid is asserted, if ack doesnt happen in ##[3:5] then it should stay low for [6:10]
You have 2 threads in the consequent
ap_ack2vld: assert property($rose(valid) |->
(##[3:5] ack) or (##6 !ack[*5]) );
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
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- 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
- 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
See Papers: VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy
Thanks ben@systemverilog.us , I have a case where I have to check if the state transition happens to active state it has to stay in the active state for 16 cycles so I coded assertion in this way
assert property(@(posedge clk) disableiff(rst) ((state === active)&& ($past(state) !== active)) |-> ($stable(state)[*16])) however, this assertion failed even if the active condition is true is there any better way we can code this ?
In reply to saikishorereddy:
The issue with your assertion is that in the cycle the antecedent succeeds, $stable(state) is false. In the consequent, the way you wrote it, you are requiring that in the same cycle the antecedent succeeds, the $stabe(active) is true, but it is false!!! How could it be be stable and unstable in the same cycle?
1800: $stable returns true (1’b1) if the value of the expression did not change
ap_active_ERROR: assert property(@(posedge clk) disableiff(rst) // "A" means active
(state === active) && ($past(state) !== active) |-> $stable(state)[*15]);
// (state === active) && ($past(state) !== active) |-> $stable(state)[*1]
// state: !A !A A A A A
// assertion |-> // antecedent is true at this cycle
// $stable(state) 1 0 1
// Consequent wants $stable(active to be true here, it is not
SOLUTION
ap_active_OK: assert property(@(posedge clk) disableiff(rst) // "A" means active
(state === active) && ($past(state) !== active) |-> ##1 $stable(state)[*14]);
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
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- 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
- 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
See Paper: 1) VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy
2) http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
^^