Assertion : Assume writing

SystemVerilog
,
1

HI All,

I am writing an assumption for the following requirement;
image

valid is an input signal. I want to constraint/write assume, once it goes HIGH, it should remain HIGH for at least 6 clock cycles and then it should go low.

I have written like this;

assume property (
@(posedge clk)
//$rose(valid) |-> ##[6:8] !valid; //case_1
$rose(valid) |-> ##[6:8] $fell(valid)
); //case_2
endproperty

both cases are not working as expected. After running this,
cover precodnition (antecedent) is getting passed,
but cover witness is getting undermined.
Result : property is keep running, looks like some issue.

Could you please suggest what could be wrong here?

2

I think your checker is not complete:

The correct one should be like below:
assert property (@(posedge clk) $rose(valid) |-> valid[*6:9] ##1 !valid );

3

with your assumption it can toggle in between and still satisfy assume .
there are many ways to correct it.
can you try
$rose(valid) |-> valid[*6] ##1 !valid ;