Equivalence of two assertions

[nithinpradeep]

Hello,

Lets consider this assertion from Harry Foster(related to arbiter verification):
~ This check is to ensure fairness of the arbiter,ie, arbiter should not grant channel 1 two times without servicing channel 0’s request which was already pending.

property(@posedge clk) disable iff (resten)
       not($rose(req[0]) ##1 (!gnt[0] throughout (gnt[1][->2]))
endproperty

I was wondering if the above property is equivalent to this one (using implication):

property(@posedge clk) disable iff (resetn)
       $rose(req[0]) |=> not(!gnt[0] throughout (gnt[1][->2]))
endproperty

If these two are not equivalent then kindly explain what is missed in the second one, which is covered in the original one. Thanks

[ben2]

Those two properties essentially do the same thing with one minor difference
requirement: NO grand channel 1 two times without servicing channel 0’s request which was already pending.

property p_arb_OK; 
 (@posedge clk) disable iff (resten)
       not($rose(req[0]) ##1 (!gnt[0] throughout (gnt[1][->2]))
endproperty

The following sequence should never occur:
A request from 0 with no grant for it while giving 2 grants to unit 2.
If $rose(req[0])==0, the assertion is nonvacuoulsly true.

property(@posedge clk) disable iff (resetn)
       $rose(req[0]) |=> not(!gnt[0] throughout (gnt[1][->2]))
endproperty

If $rose(req[0]) then there shall be no grant for it while giving 2 grants to unit 2.
If $rose(req[0])==0, the assertion is vacuoulsly true.

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

---

1. SVA Alternative for Complex Assertions
   Verification Horizons - March 2018 Issue | Verification Academy
2. SVA: Package for dynamic and range delays and repeats | Verification Academy
3. SVA in a UVM Class-based Environment
   SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy