SVA语法疑问：##1 a |-> b与a |-> $past(b)的区别及b的周期取值

Great question! These two SVA constructs look similar at first glance, but they serve entirely different timing checks—let’s break them down clearly.

First: When is b sampled in ##1 a |-> b? #

Let’s start with your direct question. In the assertion ##1 a |-> b:

• The ##1 creates a 1-cycle delay before checking if a is true. So if we start evaluating the assertion in cycle N, a is checked in cycle N+1.
• When a is true in cycle N+1 (the sequence matches), the assertion checks b in that same cycle (N+1).

In short: b uses the next cycle’s value relative to the assertion’s starting cycle (or more precisely, the same cycle where a is matched after the 1-cycle delay).

Core Differences Between the Two Assertions #

Let’s contrast the two constructs side by side:

1. Timing of Trigger & Check #

• ##1 a |-> b:

  • Trigger condition: a is true 1 cycle after the assertion starts evaluating (cycle N+1).
  • Check: b must be true at the same time as the trigger (cycle N+1).
  • Think of it as: “In the next cycle, if a is high, b must also be high.”

• a |-> $past(b):

  • Trigger condition: a is true in the current evaluation cycle (cycle N).
  • Check: b must have been true 1 cycle before the trigger (cycle N-1).
  • Think of it as: “If a is high now, b must have been high in the previous cycle.”

2. Direction of Timing Logic #

• ##1 a |-> b uses forward-looking delay: it waits for a future event (a in N+1) then checks a concurrent condition.
• a |-> $past(b) uses backward-looking sampling: it reacts to a current event (a in N) then verifies a past condition.

3. Typical Use Cases #

• Use ##1 a |-> b when you need to enforce that a future event is paired with a concurrent condition. For example:

  “When the write enable signal goes high in the next cycle, the data bus must be valid at the same time.”
  ##1 wr_en |-> data_valid;

• Use a |-> $past(b) when you need to validate that a current event was preceded by a required condition. For example:

  “If the data is sampled now, the sample enable must have been high in the previous cycle.”
  data_sampled |-> $past(sample_en);

内容的提问来源于stack exchange，提问作者O.K.