Assertion to check valid transition from value A to value B on a bus and this transition is only valid when strobe is high. If I try to use $past(bus== A) -> (bus ==B) & (strobe ==1). It does not work

[shals]

If I try to use if @bus disable (disable_flag) $past(bus== A) → (bus ==B) & (strobe ==1). It does not work. It does not even evaluate first transition of bus for A to C.

[ben2]

In reply to shals:
Your requirements are not clear.

let A=2'b10; let B=2'b11; 
ap_strobe: assert property(@(posedge clk) strobe |->  $past(bus== A) && (bus ==B)  ); 
/* above says that 
   when strobe==1, current value of bus==A, and past value of bus as B

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

[shals]

In reply to ben@SystemVerilog.us:

Hi Ben,
I am sorry for not being very clear.Here are the requirements.

1. Bus should change its value when strobe is high. Else assertion should generate error.
2. When strobe is high , if bus changes 2’b00 to 2’b10 it is valid. But if it changes to any other value assertion should generate error.

Thanks
Shals

[ben2]

In reply to shals:

In reply to ben@SystemVerilog.us:
Hi Ben,
I am sorry for not being very clear.Here are the requirements.

1. Bus should change its value when strobe is high. Else assertion should generate error.
2. When strobe is high , if bus changes 2’b00 to 2’b10 it is valid. But if it changes to any other value assertion should generate error.
   Thanks
   Shals

let A=2'b00; let B=2'b10; 
ap_strobe: assert property(@(posedge clk) strobe |-> 
                   $changed(bus) && $past(bus== A) && (bus ==B)); 
/* above says that 
   when strobe==1, bus changes its value.  Also, the current value of bus==B, and past value of bus was A

Ben SystemVerilog.us

[shals]

In reply to ben@SystemVerilog.us:

Hi Ben,
Thanks. I did not know about $changed option. That worked. I could use
ap_strobe: assert property(@(posedge clk)
$changed(bus) && $past(bus== A) |-> (strobe ==1) && (bus ==B));

By the way, I have your book and Appendix-C does list $changed :-)