Assertion for id should not change when request is high

SystemVerilog
, ,
1

Hi,

To check if the cmd_id should not change for the duration that cmd_req is high(from rising edge to the falling edge of the request), is this cover property correct?

stable_id_rose_cover: cover property(
  @(posedge i_clk) disable iff(!i_rst_n)
  $rose(cmd_req) ##1 ($stable(cmd_id) until $fell(cmd_req))
                    );

Will this also include the value of cmd_id at the rising edge of cmd_req/falling edge of cmd_req?

OR will this assertion be enough? Is there a difference between use $rose(cmd_req) and just cmd_req?

stable_id: assert property(
  @(posedge i_clk) disable iff(!i_rst_n)
  (cmd_req) |-> $stable(cmd_id) 
                    );

Thank you.

2

In reply to UVM_learner6:
The following check will work. In your overlapping assertion, if the cmd_id is set only when cmd_req is asserted high, then it will fail.
stable_id: assert property(
@(posedge i_clk) disable iff(!i_rst_n)
(cmd_req) |=> $stable(cmd_id)
);

3

In reply to kddholak:
$stable returns true if the sampled value of the expression did not change between the sampled value at the previous cycle and the sampled value at the current cycle. Otherwise, it returns false. $changed is a complement to $stable; $changed returns true if the sampled value of the expression changed. Otherwise, it returns false.


// use the until_with

$rose(cmd_req) |-> ##1 
  ($stable(cmd_id) until_with $fell(cmd_req))