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

SystemVerilog
, ,
4

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