SVA assertion to check condition is satisfied until one signal asserted

SystemVerilog
1

I would like to check if a certain condition is satisfied in the formal tool during the running of the program until the result is ready:
for example: if START is the initiated signal that tells the system to start executing,
READY is the signal that indicates if the result is ready
COND is the condition that needs to be satisfied from the time the START signal is
asserted until the result is ready (READY asserted)
I tried this:
property p1;
@(posedge clk)
(START ##1 !START) |=> COND until $rose(READY);
endproperty

The problem is the COND is checked only when READY is asserted and not before that.

2 
(START ##1!START) // says the $fell of START
|=> // One cycle after the fell 
COND until $rose(READY); // COND is true until, but necessarily with the rose of READY
// what you need is 
$rose(START) |-> COND until_with $rose(READY);
// when rose of start, in the same cycle then COND holds at 1'b1 
// until and with the rose of ready

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

4

Is there a way to check if the condition is satisfied until the first occurrence of $Rose(ready)

5 
(START ##1!START) // says the $fell of START
|=> // One cycle after the fell 
COND until $rose(READY);

Are you asking if this assertion is correct? It is.
Or are you asking for a testbench to verify it?
Ben

6

The assertion is correct, but it evaluates the condition every time the ready signal is asserted. Is there a way to examine the condition only during the initial rise of the ready signal.

7

[You]“but it evaluates the condition every time the ready signal is asserted. Is there a way to examine the condition only during the initial rise of the ready signal.”
[Ben] Use

$rose(READY) |-> COND;  // Is this what you want 
// Or this
$rose(START) |-> COND until $rose(READY);
// or use 
$rose(START) |-> (COND[*1:$] ##1 1) intersect $rose(READY)[->1];
8

$rose(READY) |-> COND; // this will check the COND only once during that clock cycle
$rose(START) |-> COND until $rose(READY); // this will pass if the COND does not occurred
I need to check if COND is always true from the $rose(start) and remains true until the first $rose(ready) occurs.

9 
$rose(START) |-> COND until $rose(READY);
 // cond==1 at all cycles until, but not with the new ready
// or use 
$rose(START) |-> COND until_with $rose(READY); 
// cond==1 at all cycles until, but also with the new ready
// or use 
$rose(START) |-> (COND[*1:$] ) intersect $rose(READY)[->1];
// cond==1 at all cycles until, but also with the new ready

see my paper Reflections on Users’ Experiences with SVA, part 2

Addresses the usage of these four relationship operators: throughout, until, intersect, implies

10

The second one I need. Thank you so much.