verify_window
Check temporal properties over clock windows in waveforms, returning a precise holds/counterexample verdict with sampled values to prove or disprove RTL behavior.
Instructions
Evaluate a temporal predicate over a clock window and return a precise verdict (holds) plus a concrete witness/counterexample (cycle + sampled values). You state the predicate; the tool checks it against the waveform over thousands of cycles you cannot read yourself. Templates, not a DSL: a term is {signal, op, value} (op: eq/ne/gt/ge/lt/le/is_x/is_known); a predicate is a list of terms (implicit AND — run two calls for OR). Modes: always(P), never(P), eventually(P), implication (A |-> B within N cycles, the protocol-response template; set overlap=false for |=> = a stability/hold property where B must STILL hold the NEXT cycle, e.g. HTRANS/valid held through a wait state), and sequence (the per-accepted-beat increment of a signal — address-stride checks like AHB haddr +stride; supports modulo for WRAP bursts and restart_when for burst boundaries). x/z cycles are reported as unknown (never silently passed); an implication whose response window runs past end-of-trace is reported inconclusive (never silently failed). On a finding it sets violating_signal + a next_action to explain_signal_driver (bus facts do not self-attribute master/slave). Use to prove/disprove an RTL inference in one call. Reads existing waveforms only.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| edge | No | Clock edge to sample on. Default posedge. | posedge |
| mode | Yes | Temporal template to evaluate. | |
| clock | Yes | 1-bit clock signal full path. | |
| delta | No | sequence only: check the per-accepted-beat increment of one signal. predicate is the accepted-beat gate (e.g. hready==1 && htrans active). E.g. AHB byte INCR: {signal:'top.haddr', value:1}. For WRAP bursts pass modulo = burst region bytes (size*len) so the wrap-around beat is accepted via (cur-prev) mod modulo. Pass restart_when (a predicate, e.g. htrans==NONSEQ) to re-seed at each new burst so burst boundaries are not flagged. | |
| overlap | No | implication only. true (default, |->): the response window includes A's own cycle. false (|=>): the window starts the NEXT cycle [i+1, i+within] — use this for a stability/hold property ('B must STILL hold next cycle', e.g. HTRANS/valid held through a wait state) where A already implies B on its own cycle. With overlap=true such a property is a VACUOUS pass (flagged in result.vacuous + warnings); overlap=false requires within_cycles>=1. | |
| predicate | No | always/never/eventually: list of {signal, op, value} terms, AND-combined. | |
| wave_path | Yes | Waveform (FSDB or VCD). | |
| antecedent | No | implication only: the A predicate (list of terms). | |
| consequent | No | implication only: the B predicate that must follow A. | |
| cursor_name | No | Optional explicit cursor name for the witness/counterexample. | |
| cursor_note | No | Optional note for the registered cursor. | |
| end_time_ps | No | Window end. -1 = end of trace. | |
| start_time_ps | No | Window start (ps int, '@cursor', or unit literal). Default 0. | |
| within_cycles | No | implication only: B must hold within this many cycles of A. The response window is [i, i+within] when overlap=true (includes A's cycle) or [i+1, i+within] when overlap=false. Default 1. |