Until and within operator

The Within Operator

The within operator ensures that a specific event or condition occurs within the time range defined by another event or condition.

Syntax

event1 within event2
  • event1: The event or condition that must occur.
  • event2: The time range during which event1 must occur.

Example: Data Transfer Completion

In a data transfer system, the transfer_complete signal must occur during the active period of the transfer_enable signal.

property transfer_within_enable;
    @(posedge clk) transfer_complete within transfer_enable;
endproperty

assert property (transfer_within_enable)
    else $error("Transfer did not complete within the enable period.");

Explanation

  • The assertion checks that transfer_complete occurs while transfer_enable is high.
  • If transfer_complete happens outside this period, the assertion fails.

The Until Operator

The until operator checks that a condition remains true until another event occurs. Once the terminating event occurs, the first condition is no longer monitored.

Syntax

condition1 until event
  • condition1: The condition that must remain true.
  • event: The event that terminates the monitoring of condition1.

Example: Reset Stability Until Load

The reset signal must remain active until the load operation begins.

property reset_until_load;
    @(posedge clk) reset until load_start;
endproperty

assert property (reset_until_load)
    else $error("Reset became inactive before load operation started.");

Explanation

  • The property checks that reset remains high until the load_start signal becomes active.
  • If reset drops before load_start occurs, the assertion fails.

Example:

Let’s take one more example. In a memory operation, the write signal must occur within the write_enable window, and no read operation should occur during this time.

property combined_example;
    @(posedge clk) (write within write_enable) and not (read);
endproperty

assert property (combined_example)
    else $error("Write failed within enable or read occurred during write.");

Explanation

  • The assertion ensures that write happens within the write_enable period.
  • Simultaneously, it ensures no read signal is active during this time.
Previous
Next