Assertion issue

SystemVerilog
, ,
1

Hi,

I have the following property check the behaviour on my interface.


property tlbwrite_rise_property;
    @(posedge clock)
      disable iff (reset)
        $rose(tlbwrite_i_m) |-> ##1 $rose(mmu_stall_o);
  endproperty

  property tlbwrite_fall_property;
    @(posedge clock)
      disable iff (reset)
        $fell(tlbwrite_i_m) |-> ##[1:9] $fell(mmu_stall_o);
  endproperty

  tlbwrite_rise_SVA: assert property (tlbwrite_rise_property) else
    `uvm_fatal("tlbwrite_rise_SVA", $psprintf("[tlbwrite_rise_SVA] ERROR: mmu_stall_o MUST rise 1 clock cycle after tlbwrite rised"))

  tlbwrite_fall_SVA: assert property (tlbwrite_fall_property) else
    `uvm_fatal("tlbwrite_fall_SVA", $psprintf("[tlbwrite_fall_SVA] ERROR: mmu_stall_o MUST fall between [1-9] clock cycle(s) after tlbwrite fell"))

I have now a fatal because of tlbwrite_rise_SVA and I know why the issue is how to handle it.

This was fine as I was writing to the translation lookaside buffers (TLB) at the beginning of my simulation.
Now I am doing the TLB dynamically while there is some MMU traffic

mmu_stall_o is driven if
1: I have a TLB write: tlbwrite_i_m
2: I have a MMU transaction which stalls the MMU via mmu_stall_o

So as mmu_stall_o is already high then if I try do a TLB write tlbwrite_i_m then the rise condition of mmu_stall_o will not happen as it is already high.

So is the ther way to tell the property something like ?

$rose(tlbwrite_i_m) |-> ##1 $rose(mmu_stall_o) || (mmu_stall_o)

so that it tase into account that mmu_stall_o is high

Thank you in advance.

2

In reply to Ep1c F4iL:
$rose(mmu_stall_o) || (mmu_stall_o)
is the same as
(mmu_stall_o)
Maybe you want

$rose(tlbwrite_i_m) && !(mmu_stall_o) |=> $rose(mmu_stall_o);