SVA throughout operator

SystemVerilog
,
1

Hi, I am confused with throughout operator use. Condition: dout should remain stable at 0 for entire duration of reset. The solution is given below:

assert property (@(posedge clk) $rose(rst) |=> rst throughout ((dout == 0)[*1:$]))

The above appears as if rst should remain high throughout dout is stable.
Can someone please explain me with an easy example ?
(PS: I understand LHS of throughout has to be a boolean)

2

Throughout: The syntax for this sequence is:
expression_or_dist throughout sequence_expr
The throughout operator specifies that a signal (expression) must hold throughout a sequence.

      ( b throughout R ) // b is an expression, R is a sequence 
    //  is equivalent to
      ( b [*0:$] intersect R )

See my paper

3

Thank you @hdlcohen

So, according to this definition is the code given for the condition correct because for throughout the rhs can go low when lhs is high, so this would violate that dout=0 when rst is still high, right ?

4 
rst throughout ((dout == 0)[*1:$]))
// same as 
( rst[*0:$] intersect (dout == 0)[*1:$])) 
// thus 
rst       1 1 1 1 0 0 1
dout   0 1 1 x x x 
// the sequence rst[*1] intersects dout==0[*1]
// the consequent is a match. 
the consequent is same as 
rst[*1] intersect dout==0[*1]  or 
rst[*2] intersect dout==0[*2]  or 
..
rst[*n] intersect dout==0[*n]
// If any thread is a match, as a consequent, the assertion is a pass (and the property is true)
5

Hi Ben,
Since the min. requirement for assertion to pass is rst[*1] shouldn’t the following be true ::

( b throughout R ) // b is an expression, R is a sequence 
  //  should be equivalent to
( b [*1:$] intersect R )   // Changed from [*0:$] to [*1:$]
6

Unless you want to consider ALTERNATIVE FACTS, the above would be true.
1800 IS the BIBLE on SystemVerilog, and it says:

The construct exp throughout seq is an abbreviation for the following:
(exp) [*0:$] intersect seq

See 1800’2023 16.9.9 Conditions over sequences