title: Recursive and non-recursive property: Are these assertions equal?
body: <p>Consider the following specification:</p>
  
  <pre><code>"interrupt must hold until interrupt ack is received"
  </code></pre>
  
  <p><a href="https://i.stack.imgur.com/5VpyE.png" rel="nofollow noreferrer"><img src="https://i.stack.imgur.com/5VpyE.png" alt="enter image description here"></a></p>
  
  <p>Are these assertions equal and corresponding to the specification? </p>
  
  <p>1- First assertion (using a recursive property):</p>
  
  <pre><code>property intr_hold(intr, intrAck);
     intrAck or (intr and (1'b1 |=&gt; intr_hold(intr, intrAck)));
  endproperty 
  
  assert property @(posedge clk) $rose(intr) |=&gt; intr_hold(intr, intrAck);
  </code></pre>
  
  <p>2- Second assertion (using a non-recursive property):</p>
  
  <pre><code>assert property @(posedge clk) intr |=&gt; intr or past(intrAck);
  </code></pre>
  
  <p><em>Thank you</em></p>