Assertions Interview Questions

An implication has an antecedent (the left side) and a consequent (the right side). On every clock tick where the antecedent does not match, the implication succeeds vacuously. There is nothing to check, so those attempts count as passes. An assertion whose antecedent never fires reports success without ever checking the consequent. Cover the antecedent, and read the real hit count before trusting a clean run.

An attempt starts at every clock tick, so one assertion is evaluated thousands of times. The implication says "whenever a holds, b must follow". A tick without a breaks no promise, so it has to succeed. If it failed instead, the assertion would fire on every idle cycle and be useless.

No. The consequent starts only from an end point of the antecedent. A partial match has no end point, so the attempt ends as a vacuous success. A half-started request therefore counts as a pass. Cover the full antecedent to see whether complete requests happened.

Cover the antecedent with the same clock and reset: cover property (@(posedge clk) disable iff (rst) req);. A nonzero count shows the consequent was checked at least that often. Many teams also cover the whole scenario, req ##1 ack, to show the good path happened.

Every attempt is disabled, so the assertion reports no passes and no failures. A summary that only lists failures looks clean, which is the same trap as vacuity. An antecedent cover with the same disable iff reads zero and exposes it.

A typical one is a bind mistake: the assertion's req is tied to a signal that never goes high. Every attempt is then vacuous while the real handshake is broken. Another is a test that never reaches the mode where req is raised. Both show up only as an antecedent cover stuck at zero.

Pair every implication with an antecedent cover. Make "every antecedent hit in regression" a sign-off item, and review zero-hit covers like failures. In formal, run the covers too, and treat an unreachable antecedent as a vacuous proof. Track the counts per assertion in the verification plan. Then a property that stops firing after a design change is caught.

assert states a rule the design must obey. assume states a rule the environment, meaning the inputs, must obey. cover asks to see a scenario happen at least once. A simulator checks an assume just like an assert and reports when the stimulus breaks it. A formal tool uses the assume to limit the inputs it explores, and tries to prove each assert for all remaining inputs.

The same file runs in formal and in simulation. If the simulation stimulus breaks an assumption, either the stimulus is wrong or the assumption is too strict. Both are worth knowing, because a too-strict assumption makes formal proofs too easy.

In formal, the assumption removes behaviour the design can really produce. A bug that needs that behaviour then disappears from the proof. In simulation it fires only if the tests reach that state, and they may never do. Write assumptions on input ports only.

The constraint shapes what the testbench generates. The assume states the same rule as a property. Formal tools use it to limit their inputs, and simulators check it against whatever the stimulus did. Keeping both lets the assume catch a stimulus that breaks the rule, for example a directed test that bypasses the constraint.

Formal tools work on the design and its bound checkers, not on class-based testbench code. Checks inside class methods cannot be reused there. Rewrite the interface rules as concurrent properties over DUT signals, in a checker module you can bind. Leave only transaction-level checks in the classes. The same file then runs in simulation as assertions and in formal as proof targets, with the input rules switched to assumptions.

Check that the covers are reachable. Add a cover for each important scenario and for each assertion's antecedent. If a cover is unreachable, an assumption has probably removed the inputs that lead there. Then the proof says nothing about those inputs.

A cover property counts how many attempts matched the sequence. It is a temporal check: it can see "ack within 1 to 3 cycles of req". A covergroup samples values at chosen moments and counts them into bins. Use covers for sequences of events, and covergroups for value combinations and their crosses.

cover property counts each attempt once, at its first match. cover sequence counts every match, so one attempt of req ##[1:3] ack can add up to three hits. Use cover property to ask "did it happen?", and cover sequence to ask "how many ways did it happen?".

Every match is a different timing of the same scenario. Counting them shows whether the tests reached each latency in the window, such as ack after 1, 2 and 3 cycles. A plain yes or no would hide a test that only ever produced one latency.

No. The count adds up matches of every latency, so all 300 could be latency 1. Write one cover per latency: req ##1 ack, req ##2 ack and req ##3 ack. Or sample the latency into a covergroup with one bin per value.

Each temporal scenario in the plan gets a cover property, next to the covergroups for values. The plan also lists one antecedent cover per important assertion. Coverage closure then needs every cover hit in regression. A cover that stays at zero is reviewed like a failure, because it means a check never ran.

Write the assertion in its own module, then use bind counter counter_props u_props (.clk, .rst, .inc, .count_q);. The bind puts an instance of the checker inside every counter, without touching the RTL file. The port connections are resolved inside the target, so the checker can read internal signals such as count_q. Each failure message then names the instance where it happened.

Design and verification are often owned by different people. Bind keeps checkers out of the design files, so adding a check never needs an RTL change or an RTL review. It also lets one checker attach to a block the team cannot edit, such as third-party IP.

Binding to the module name puts the checker in every instance of counter. Binding to a hierarchical instance path puts it only there. Use the module form for rules that every copy must obey. Use the instance form for a rule that depends on how one copy is used.

The bind port list can connect the wrong signal, for example a signal that never goes high. Every attempt then passes vacuously, which means the antecedent never matched and nothing was checked. An antecedent cover per assertion shows it as a cover stuck at zero.

No. It only says that some ready comes later, and with no deadline it can never fail in a finite test. It never checks valid in the cycles between. Write the rule cycle by cycle: valid && !ready |=> valid. Every cycle where the offer waits, the next cycle must still show valid.

The window has no end, so there is always a later cycle where ready might still arrive. In an assert, an attempt that is still waiting when the test ends counts as weak, so it does not fail. Only a strong form, such as s_eventually, fails when the test ends first.

Take it from the spec or the slave's datasheet, such as a maximum number of wait states. If the spec gives none, agree a system timeout with the architect and write it down. Use valid |-> ##[0:N] ready. Then cover the longest legal wait, so tests reach the bound.

Both catch a withdrawn offer. The cycle rule starts a short attempt on every waiting cycle, so it is easy to read and runs on every tool. The until_with form starts one attempt per offer and follows it to the handshake. It misses offers that start while valid is already high, such as back-to-back beats.

Its antecedent needs a stalled offer. If every test drives ready high, no attempt ever reaches the consequent, and the zero-failure report is vacuous. Count or cover valid && !ready and make a stalling sink part of the agent.

Keep a small model of the fill level in the checker, updated as level + push - pop on each accepted operation. Then assert four rules. No accepted push when full. No accepted pop when empty. full equals level at depth, and empty equals level at zero. Add covers for full, empty, and push with pop on the same cycle.

The fill level depends on the whole history of pushes and pops. A sequence can only look at a bounded window of cycles. A small counter keeps that history in one number, so each property stays short and checks only the current cycle.

Assertions use sampled values, taken before any flop updates at the edge. So the property sees the count after the previous edge, not after this push. Write the rules with that in mind: a push while the old count is full is an error now. A counter updated with <= matches the DUT's own timing.

Assertions check the control rules in the cycle where they break, and point straight at the cycle. A scoreboard checks that the data comes out in the right order and with the right values. Use both. The flags and limits suit assertions, and data ordering suits the scoreboard.

Add one rule against the same model: almost_full == (level >= DEPTH - 2). Then cover the two corners: the cycle it rises and the cycle it falls. The model already exists, so each new flag costs one line.

Safety rules: at most one grant, written $onehot0(gnt), and grants only to requesters, written (gnt & ~req) == 0. A third safety rule: a request is not granted while it is low. Fairness: a waiting request is granted within N cycles, where N follows from the round-robin order. Simulation checks the bounded form well. The unbounded form, "eventually granted", needs a formal tool or a strong property at the end of the test.

A simulation is finite, so "eventually" can only fail at the very end, and only in its strong form. A bounded wait fails at the exact cycle the promise breaks, which is much easier to debug. For round-robin, N is about the number of other requesters times their longest grant.

N is the worst wait: every other requester gets one grant before you, each held for its longest time. With four requesters that is about 3 × 8 cycles, plus the arbiter's own latency. If the hold time has no limit, no bound exists. Then the spec needs a hold-time rule first.

$onehot(v) is true when exactly one bit is 1. $onehot0(v) is true when at most one bit is 1, so all zeros pass. $countones(v) <= 1 means the same as $onehot0 and is clearer when the limit is not one.

Run the same safety and bounded-fairness assertions in a formal tool, with assumptions only for real protocol rules on the requesters. Formal explores every request pattern, including the rare one where two masters starve a third. Then check that the covers are reachable, so the proof is not empty. Simulation alone samples a small part of that space.

With x bits in an operand, == returns x, and an if treats x as false. So the error line never runs. Use $isunknown(data), which is true when any bit is x or z. In a design, write it as a concurrent assertion gated by the valid signal: valid |-> !$isunknown(data).

$isunknown is true when any bit is x or z, which is the check you want. === compares x and z bits literally, so r === 'x is true only when every bit is x and misses a half-driven bus. == returns x whenever an operand has an x bit, so it never gives a clean true. The run shows all three on xxxx0101.

The bus is allowed to be unknown when nothing is being transferred; only data that rvalid marks as valid must be known. Write rvalid |-> !$isunknown(rdata), and check the qualifier itself with a separate unconditional !$isunknown(rvalid) after reset.

A scoreboard may convert the data to a two-state type, where x becomes 0, or compare with !=, where x hides. An X check at the interface catches an undriven or unreset bus at the cycle it appears. It also points straight at the interface instead of at a later data mismatch.

Write $countones(active) <= 2. $countones returns the number of 1 bits, so any limit works. Pair it with a cover for exactly two active channels, so the test shows that the limit case really happened.

Draw the line at the DUT boundary: interfaces and monitors stay four-state, and every bus gets a valid |-> !$isunknown(data) assertion bound to it. Reset and power-up scenarios run on a four-state simulator as a sign-off item. Emulation normally runs two-state; X modes exist but cost speed, so reset-state X checks belong in four-state simulation. Two-state is allowed only behind that boundary, where speed matters and nothing samples the DUT.

!rst in the antecedent only stops new attempts from starting during reset. An attempt that started before reset keeps running and can fail when the design clears its state. disable iff (rst) abandons every attempt, including those in flight, as soon as the condition is true. An abandoned attempt counts as neither pass nor fail.

Reset is usually asynchronous: it can arrive with no clock running, and the design reacts at once. Suppose the disable condition were sampled. Then an attempt could still fail at the first edge after reset, because the sample came from just before reset rose. Using current values makes the check stop exactly when the design stops being bound by the rule.

A failure runs the else action and is counted as an error. A vacuous success is a pass, and the pass action runs for it. So a pass count can be huge with nothing checked. A disabled attempt is neither, and most summaries do not show it at all. That is why a clean summary needs a separate count of real antecedent matches outside reset.

Disable each property with the reset that clears the state it talks about. A rule on a block's FIFO uses that block's reset, not the chip's. A warm reset must not disable rules about state that survives it. That state gets its own checks that it really survived. Write the mapping into the checker's parameters and review it with the design owner, because a too-broad disable silently hides checks.

disable iff belongs to the property. It states when the rule does not apply, such as reset. It travels with the checker into every test and into formal. $assertoff, $asserton and $assertkill are switches in the test. They cover situations the rule cannot know about, such as an error-injection test or a power-down. $assertoff stops new attempts but lets attempts already running finish; $assertkill also aborts those.

With $assertoff that attempt runs to completion and can still fail; only attempts that would start later are suppressed. With $assertkill it is aborted at once and reports nothing. Use $assertkill when the scenario that started those attempts has become meaningless, for example after an injected error.

Switch off only the checker instance that would fire on the injected error, with a scoped call such as $assertkill(0, tb.dut.rx.u_crc_chk). Inject the error, wait for the error path to finish, then call $asserton(0, tb.dut.rx.u_crc_chk). Keep the error-response checks on, since they are what the test is for, and log both calls.

Some exceptions depend on what the test is doing, not on design signals. Examples are an injected fault, a power-aware run with a domain switched off, or a bring-up test that runs before configuration. Encoding those in every property would couple checkers to tests. Control tasks keep the checker generic and put the test-specific decision in the test.

The rest of the test then runs with those checks off, and it still passes. Scope the call to the assertions the fault affects and to the window it lasts. Turn them back on with $asserton at a known point. Log both calls, so a review can see what was off and when.

Route all control through one testbench utility that logs each call with its scope and time. Fail the test if any scope is still off at the end. Report per test which checkers were suppressed and for how long, and review that list like waivers. Prefer fixing an over-strict property to suppressing it.

Declare default clocking @(posedge clk); endclocking and default disable iff (!rst_n); at the top of the module, then write each rule as assert property (push |-> !full) else errors++;. Every assertion in that module without its own clock or disable iff inherits them. An assertion that needs a different reset writes its own disable iff, which overrides the default.

The default is part of the module's declaration and is resolved at compile time. So a module means the same thing wherever it is instantiated. If defaults flowed through instances, a reusable checker would change behaviour depending on who instantiated it. Each reusable module therefore declares its own defaults, usually from its own ports.

The DUT module's default does not reach into the bound checker, because defaults are resolved in each module's own declaration. So the checker's properties have no disable. They are evaluated during reset and can fail on reset values. Give the checker a reset port and its own default disable iff.

The default is shortest when one reset governs the whole module. A property with formal arguments, such as property p_hold(clk, rst, v, r);, carries its clock and reset with it. You can reuse it in modules with other resets, or in a library package. Libraries usually use arguments; a block's own checker usually uses defaults.

The standard infers the clock of a procedural concurrent assertion from the always block's event control, so the code is legal. Verilator 5.052 additionally demands a default clocking block for ## there, and also tests en at the wrong edge for multi-edge procedural rules. Move such rules out of the procedure as en && req |-> ##2 gnt, which is clearer anyway.

One shared register can remember only the newest request, so a back-to-back request overwrites it before the first check runs. Give each attempt its own copy with a local variable: property p; logic [7:0] v; (valid, v = data) |-> ##3 (out == v + 1); endproperty. The assignment runs when valid matches, using the sampled data, and each overlapping attempt keeps its own v.

For a fixed latency they give the same verdicts: $past(data, 3) at the check edge is the data sampled at the request edge. $past keeps a history of depth 3 for every assertion, while the local variable keeps one value per open attempt. The local variable also generalises to variable latency, where no fixed depth exists.

Attempts overlap whenever the antecedent can match on consecutive edges, and each attempt describes a different transaction. A shared variable would make one transaction's check read another's data, which is exactly the false failure in the twin. Per-attempt copies make a property read as a statement about one transaction.

The standard form carries the local variable across the window, (req, v = data) |-> ##[1:4] (rsp && rdata == v), but with overlapping requests one response can satisfy several attempts. A robust checker keeps an in-order queue of expected data in auxiliary code. It pushes on each request, pops on each response, and asserts the popped value. That queue is a small scoreboard written next to the property.

Each attempt only asks whether ack is true at some edge of its own window. The attempts are evaluated independently, and none of them uses up the ack. So that one edge satisfies every window that contains it. Counting responses needs state outside the property, a ticket or a queue.

Assertions take the local, cycle-level rules: an ID is not reused while outstanding, every response matches an outstanding ID, deadlines are met. They report the exact cycle and also run in formal. The scoreboard takes end-to-end data correctness and anything needing a reference model. Overlap is deliberate: a lost response should be caught by both, at different distances from the bug.

Both windows contain the single ack at 45: the request at 15 looks at 25 to 55 and the request at 25 looks at 35 to 65. One ack satisfies both attempts, because nothing ties a response to a particular request. Tag each request: with in-order responses a ticket counter works, (req, t = issued) |-> ##4 (served + ack > t), so each request needs its own response by its deadline.

A ticket counter needs no design support, but it assumes responses return in order. It credits the n-th ack to the n-th request. A bus ID, such as an AXI ID, lets the checker match a response to its request even when responses reorder. Capture the ID in a local variable or key a table on it. Use the ticket only when the spec guarantees ordering.

Keep a small table in auxiliary code indexed by ID that records an outstanding request and its deadline or expected data. Assert on each response that its ID was outstanding, and on each cycle that no outstanding entry has passed its deadline. That is a per-ID scoreboard in miniature, and it keeps the properties one-edge checks that every tool runs.

An immediate assertion is a procedural statement that tests its expression the moment it executes, with the values at that instant. A deferred assertion (assert #0 or assert final) is also procedural, but it reports later in the time step. So a short combinational glitch that settles is not reported. A concurrent assertion samples its signals at a clock event and can check behaviour over many cycles. Use immediate or deferred checks in procedures and functions, and concurrent ones for protocol rules.

A combinational block can run several times in one time step while its inputs settle. An immediate check reports every in-between value. A deferred check waits until later in the time step. If the block runs again first, the pending report is dropped, so only the settled value counts. It gives procedural code, including functions, a glitch-free check without needing a clock.

Not necessarily. The standard says the block's second run in that time step flushes the pending report, so no failure should appear. Some simulators, Verilator 5.052 among them, do not implement the flush and report the transient value. Confirm on another simulator, or move the rule to a clocked concurrent assertion that no simulator disagrees on.

Both evaluate when executed and both flush on a re-run. An observed deferred assertion (#0) matures in the Observed region and runs its action in the Reactive region. So its action can still change state in that time step. A final deferred assertion runs its action block in the Postponed region, after all activity, so the action may only report. Use final when even testbench reactions to the check must not cause further glitches.

expect (@(posedge clk) req ##[1:3] ack) else ...; is a procedural statement that blocks the calling process until that one property attempt passes or fails. It is a single attempt started where the statement runs, unlike an assert property, which starts an attempt every clock. Verilator 5.052 rejects expect, so on that engine wait with an explicit bounded loop instead.

It uses 0. Concurrent assertions sample their variables in the Preponed region, before anything in that time step runs. So they see the value from just before the edge. The new 1 is seen at the next edge. This is what makes assertions race-free against flops written at the same edge.

At an edge, flops written with <= update in the NBA region, and process order within a region is unspecified. Reading at evaluation time would make the result depend on whether the flops had updated yet. The Preponed sample is the value every flop saw at the edge, which matches what real hardware samples.

The sampled value is taken before that write, so the assertion sees the old value. A DUT flop may see the new one, because its process can run after the testbench write. Assertion and DUT then disagree about the same cycle. Drive inputs through a clocking block, or with <=.

They read the same value: both take the value from just before the clock event. The assertion's sample is built into its semantics. The clocking block makes the sample explicit, as a clockvar that testbench code reads. Other input skews, such as #2ns, sample earlier. Reading the raw signal in a monitor instead gives whichever value the process order happens to produce.

The check used the Preponed sample. The action block runs later, in the Reactive region, after the design updated data at that edge. So the message shows the new value, not the one that failed. Print $sampled(data) in action blocks to report what the assertion actually saw.

No, it fails on every request. |-> is overlapping implication. The consequent (the right side) starts at the same edge where the antecedent (the left side) matched. So it demands gnt in the same cycle as req. The spec needs |=>, which starts the consequent one edge later and is exactly req |-> ##1 gnt.

Registered outputs, the common case, answer one cycle later, so |=> keeps those rules short and readable. Overlapping implication fits a response in the same cycle. Examples are a combinational output, or a condition checked while a signal is held. Either can express the other with ##, so pick the one that matches the spec sentence.

The consequent starts at the end point of the antecedent, the edge where grant matched, one edge after req. So data_valid must be high in the same cycle as grant. With |=> it would be one edge after grant.

The implication is a conditional rule: on edges without req the attempt succeeds vacuously, and only edges with req check gnt. The plain sequence must match from every attempt, so every edge where req is low fails. A plain sequence fits a cover property that asks whether the scenario ever happened; assertions almost always need the implication.

It reads 0. $rose and $fell look only at the least significant bit of their argument, and bit 0 fell from 1 to 0 in this move. To detect a change of a multi-bit value, compare the old and new values with $past. Use $changed when any change will do.

$rose reports bit 0 rising, which fits single-bit strobes. $changed is true when any bit differs from the previous sample. $past(sig) != sig is the same idea written out. But != gives x for an unknown bit, and an if or an assertion treats x as false. Prefer the system functions for readability and the explicit form when you need a specific old and new value.

Neither $rose nor $changed says which transition happened. Write it out: $past(state) == IDLE && state == BUSY. Guard the first tick, because $past has no real history there. Use === if unknown values must count as a mismatch.

There is no earlier sample. So the past value is the value in the variable's declaration, not one set later in an initial block. If req was declared 0, or left unknown, a 1 at the first edge counts as a rise. A check that must not fire at time zero should be disabled by reset, which also covers the first edges after power-up.

A level antecedent starts a new attempt at every edge where req is high. The attempts started late in a long request have windows that end after the single ack. $rose(req) starts exactly one attempt per request. Use a level only when every cycle of the level really owes its own response.

$stable(data) compares the sampled value at this edge with the sample at the previous edge. The rule is valid && !ready |=> $stable(data): if the offer is stalled at this edge, the data must be unchanged at the next one. The tempting valid |-> $stable(data) fails on every new beat, because data legally changes at the edge where valid rises.

$stable only looks one edge back. $past(data, 3) returns the sample from three edges ago. You need it when a fixed-latency output must equal an older input, as in valid_out |-> dout == $past(din, 3). For variable latency, $past cannot know the depth; capture the value in a local variable instead.

The third argument gates the clock. $past(din, 1, en) returns din from the most recent earlier tick where en was true, skipping stalled ticks. That matches a pipeline register with an enable. Verilator 5.052 rejects the gating argument at compile time, so on that engine keep a shadow register updated under en instead.

Write one checker module with the payload width as a parameter. It holds the hold, stable and reset rules, plus a counter of stalled cycles. Bind one instance to each channel. Make "every channel saw at least N stalls" a regression check, so a channel that never stalls is reported, not silently passed.

$rose(gnt) && $rose(en) needs both signals to rise at the same edge. A grant that arrives while en is already high never starts the check. The event the spec describes is the condition gnt && en becoming true, which is $rose(gnt && en). A sampled value function applies to its whole argument expression, so where you put the parentheses changes the event.

The argument is an expression, and the function keeps a history of that expression's sampled value, one entry per clock tick. It compares the expression's value now with its value at the previous tick. So it detects the moment the combined condition changes, whatever each operand did.

$rose compares with the value at the previous tick of its own clock, not the previous time unit. If the clock stops, the previous tick is the last edge before the stop. A pulse that comes and goes during the stop is never seen. Use a free-running clock for checks that must see every change.

The edge form starts one attempt when the condition becomes true and says nothing about the following cycles. The level form starts an attempt at every edge the condition holds, so it also demands timer_on after each of those cycles. Choose by the spec: "starts when" is an edge, "runs while" is a level.

The standard bans output and ref arguments for functions in assertion expressions. It also expects them to be automatic, with no side effects. A function that reads a class object hides its real inputs from the assertion. Those inputs are not sampled with the rest of the expression. Pass every input as an argument, or compute the condition into a design-side variable that the assertion samples.

s.triggered is true at a clock tick where some match of s ends. It does not matter when that match started. So a property can ask "has the whole sequence just finished?" at the moment another signal rises. .matched does the same when s runs on a different clock. It holds the end point until the next tick of the reading clock. Use .triggered within one clock and .matched across clocks.

A property that starts from a sequence looks forward from its end. Some rules look backward instead: "when X happens, Y must have just finished". End points let a property check that backward rule at the moment X happens. They also let you build a sequence out of other sequences' end points.

Declare the handshake as a named sequence and write wait (hs.triggered); in the task. The task wakes in the time step where the handshake ends, with no hand-written state machine. .matched cannot be used in a wait; only .triggered can.

They mean the same thing. The 2005 standard used .ended inside sequences and .triggered elsewhere. Later standards allow .triggered everywhere and removed .ended. When you port old code, replace .ended with .triggered.

Write each protocol phase once as a named sequence with arguments, such as address phase, data beat and response. Build properties from those pieces, using end points for "this phase must have just finished" rules. Keep them in a package or a checker that every agent binds. A spec change then touches one sequence, not twenty properties.

The consequent is checked at the first clk_b edge strictly after the clk_a edge where req was seen. That may be much sooner than one clk_a period. Between subsequences on different clocks, only ##1 and ##0 are legal. ##1 moves to the nearest later tick of the new clock, and ##0 to the nearest tick at or after. So ##2 across the boundary is illegal.

The two clocks have no fixed relation, so "two cycles" has no single meaning across them. The next edge of the destination clock is the earliest moment that domain can observe anything. Every longer wait can then be written inside the destination clock's own subsequence.

Then the next strictly later clk_b edge is simply the next clock edge. So @(posedge clk_a) req ##1 @(posedge clk_b) ack behaves like @(posedge clk_a) req ##1 ack. The multiclock form costs nothing when the clocks match, and stays correct if they later split.

The multiclock property states the rule exactly as the spec says, across both domains. The synchronised copy is easier to read and runs on more tools. But it checks the copy, which arrives two or three cycles late. Then the property must allow for that delay. Many teams use the single-clock form for tool support, and keep multiclock properties for formal runs.

Start with structural analysis: define the clocks and their relationships. Then let the tool find every crossing and check that each has the right synchronizer for its type. Next comes protocol checking: each scheme's rules, such as hold times and Gray steps, become assertions in formal and simulation. Add reconvergence checks and reviewed waivers. Use metastability injection in simulation to expose designs that assume exact timing.

accept_on (c) ends the attempt as a pass when c is true. reject_on (c) ends it as a failure. disable iff (c) ends it as neither: the attempt is simply cancelled. Use accept_on or disable iff when an abort is legal. Use reject_on when the condition must never happen during the burst. The sync_ forms sample the condition only at clock edges.

They answer different questions. Reset means "this cycle does not count", so the attempt should vanish from the results. A legal abort means "the transfer ended properly", so it is a pass. A forbidden event means "this must never happen now", so it is a failure. One operator could not say all three.

disable iff wins, because it sits outside the whole property. The attempt is disabled and counts as neither pass nor fail. That is usually right, since reset means the cycle does not count. But a real error in a reset cycle is hidden, so check reset sequencing separately.

In front of the whole property, the abort also covers attempts whose antecedent did not match. So an err during an idle cycle fails the attempt that starts there. Inside the consequent, the abort only applies after start matched. Put it in the consequent unless the condition is forbidden at every cycle.

Only the strong one fails. In an assert, a sequence is weak by default, so an attempt still open at the end is not a failure. s_eventually is strong, so the open attempt fails when the test ends. Both forms keep every open attempt alive, which costs simulation time. Prefer a bound that the spec promises, such as ##[1:16].

Every test ends at some point, usually with traffic still in flight. If open attempts failed by default, almost every test would end with false failures. Weak by default means "no bad thing seen so far". You ask for strong, end-of-test failures only where you mean them.

A hang. If ack never comes, the weak attempt is still pending at the end and does not fail. The log shows no failure, even though the design locked up. Catch it with a bounded window, a strong form, or an end-of-test check that no request is outstanding.

The bounded form fails at cycle 16 of the attempt, right where the promise breaks, and it stops tracking the attempt there. s_eventually cannot fail until the test ends, so the failure shows up far from its cause. Use the bound whenever the spec gives one. Keep s_eventually for rules that truly have no limit.

The test stops while a legal request is still waiting for its answer. The strong attempt is still open at the end, so it fails, although the design would have answered one cycle later. Drain the test: stop new traffic, wait for outstanding responses, and only then call $finish.

Simulation checks the bounded version on real traffic, and the strong version flags requests left open at the end of each test. Formal can prove the unbounded property over all input sequences. It usually needs fairness assumptions, such as "the downstream eventually accepts". Review those assumptions carefully, because a wrong one makes the proof empty.

The antecedent req is a level, so a new attempt starts on every cycle req is high. Here that is four attempts for one request. The first three see the ack in their window. The attempt that started in cycle 4 has no ack left in cycles 5 to 7, so it fails. Write the antecedent as the event the spec means: $rose(req) |-> ##[1:3] ack.

A rule such as "every request is answered" must hold for each request, wherever it happens. Starting at every tick means no request can slip past while an older attempt is busy. Ticks where the antecedent does not match end at once, so they cost almost nothing.

About ten attempts are open at any time, one per request in flight. Each keeps its own threads and local variables, which is correct and expected. On busy buses with long windows, this costs simulation time. If it is too slow, tighten the window, or check order in a scoreboard instead.

If req stays high across the boundary between two requests, there is no rise for the second one. So it is never checked. For such protocols, start the attempt at "request accepted" or "first cycle of a new request", for example req && !$past(req) || (req && $past(ack)).

A strong answer starts from the spec, not the RTL. Interface rules go in the interface or a bound checker, so every bench gets them. Internal invariants, such as FIFO limits and one-hot states, sit next to the logic or are bound in. Each property has an antecedent cover and a line in the verification plan. "Enough" means every spec rule maps to a property or a scoreboard check, and every cover was hit.

An assertion written from the RTL describes what the code does. So it agrees with the code even when the code is wrong. An assertion written from the spec is an independent second opinion. That independence is the whole value of a check.

Do not copy the RTL into the assertion. Write the question down and get the architect to answer it in the spec or a decision log. Then write the assertion from that answer. If the RTL disagrees, one of them has a bug, and you found it early.

Look for properties that keep many attempts alive. Typical causes are level antecedents that start an attempt every cycle, and long or unbounded ranges such as ##[1:$]. Rewrite them with edge antecedents and the spec's bound. Keep the expensive checks in nightly runs if they still cost too much. Measure per property with the simulator's profiler before changing anything.

A delay range starts one thread per delay, so each attempt checks ack at the next three edges. The attempt from 15 passes at 35, the first edge where a thread matches. The attempt from 55 fails only at 85, when its last thread finds no ack, not at 65. Failures from a range are therefore reported at the end of the window.

Until the last edge, a later thread could still match and turn the attempt into a pass. The verdict is known only when every thread has matched or died. For a missing response, that is the last edge of the range. That is why a wide window delays the failure report and makes debug start later in the log.

A missing ack is reported 1000 cycles after the request, far from the cause in the log. Every open attempt also keeps its threads alive until the window ends, which slows simulation. Use the tightest window the spec allows. For long latencies, a scoreboard timeout with a clear message is easier to debug.

They say different things. The range demands at least one ack somewhere in the window. Three fixed-delay assertions demand ack at every one of those edges, so a design that answers once fails two of them. To split a range for debug, the honest equivalent is a sequence or of the fixed delays, not separate assertions.

No. busy[*2:4] is a sequence that matches as soon as busy has been high for two cycles. An implication passes at the first match of its consequent. Nothing after that match is checked, so a five-cycle busy passes. The upper bound needs its own check, such as req ##1 busy[*4] |=> !busy: after four cycles of busy, the next must be low.

A property built from a sequence asks whether the sequence can match. The implication succeeds as soon as one consequent match exists. Longer matches add nothing to that answer. Anything that must happen after the match has to be written as more sequence or as a separate rule.

Repetition keeps the rule in one line and is natural for short, fixed bounds. A counter can count up while busy is high and clear when it drops. Then any bound becomes a one-edge check such as busy |-> busy_len <= 4. It is easy to debug in a waveform and costs nothing per attempt. For long or parameterised bounds, the counter is usually clearer and cheaper.

In simulation, every cycle of busy can start an attempt, and each one stays open for up to 1000 edges. A long busy period then holds hundreds of open attempts. In formal, a deep bound makes the property expensive and may keep it from converging. A counter that stops at the limit makes it a one-edge check in both. The limit becomes a parameter that tests can shrink.

busy[*0] is an empty match, so one legal reading is req |=> done with no busy at all. Empty matches make the timing hard to read. The ##1 after an empty sequence does not add a cycle the way it seems to. Write the zero case as its own alternative, or avoid it.

Both wait for two occurrences of ack, not necessarily consecutive. Goto [->2] ends exactly at the second ack, so done must come on the very next edge. Non-consecutive [=2] may end any number of edges after the second ack, while no third ack appears. So done may arrive later. The difference is only visible in what follows.

gnt[->1] matches at the next edge where gnt is true, however long that takes, and ends exactly there. That is the shape of "until the grant arrives", so req throughout gnt[->1] reads as "req stays high until the next grant, inclusive".

gnt[->1] can match at the very first tick, if gnt is already true there. So req |-> req throughout gnt[->1] passes in one cycle when the grant is immediate. With |=>, the check starts one tick later and misses that grant. It then waits for the next grant, which may belong to another transfer.

The first only says a grant comes at some point. It is weak under assert, so it never fails if no grant arrives. The second also demands req at every edge up to and including the grant. So a request dropped early fails at once. The second shape is also one of the few goto forms Verilator 5.052 evaluates correctly.

Probe each operator on every tool with one property that must fail and one that must pass. Record which forms give the standard verdict. Allow only that subset in shared checkers, and enforce it with a lint rule. Rewrite the rest with auxiliary logic or simpler forms. Re-run the probes whenever a tool version changes.

Write ack[=2:3] ##1 done: between two and three occurrences of ack, with any idle edges, and done after them while no further ack appears. Remember that the property passes at its first match, so a fourth ack before done needs its own rule.

No. p until q requires p at every edge before the first edge where q holds, but not at that edge. So dropping req in the grant cycle passes. until_with also requires p at the edge where q arrives, which is what "up to and including" means. Both are weak: if gnt never comes they never fail, and s_until, s_until_with are the strong forms.

They give the same verdict when the grant comes: req must hold at every edge up to and including the first gnt. The difference is what they are. until_with is a property operator, so nothing can follow it in a sequence. throughout builds a sequence that you can extend or use in a cover. If the grant never arrives, both are weak and do not fail.

The rule is legal and should fail one edge after the grant when done is missing. Verilator 5.052 reports no failure for a throughout over a goto followed by more sequence, so the silence is the tool. Split it: keep req throughout gnt[->1] as the whole consequent, and add gnt |=> done as a second assertion.

The weak forms report nothing: an attempt still waiting at the end of simulation is not a failure. s_until is strong, so the open attempt fails at the end of simulation. Use the strong form when "the grant must come" is part of the rule. Make tests drain traffic before they stop, or legal stimulus fails it too.

until produces a property, a verdict over time, not a sequence with an end point, and ## concatenates sequences. Some tools accept the expression anyway, Verilator 5.052 among them, which makes it easy to ship illegal code. Use req throughout gnt[->1] when you need a sequence with an end point.

and needs both sequences to match from the same start. They may end at different edges, and the result ends at the later one. intersect also needs both, but they must end at the same edge, so it constrains length. or needs either one. s1 within s2 needs s1 to match somewhere inside the span of a match of s2, starting no earlier and ending no later.

1[*1:8] matches every length from one to eight edges and constrains nothing else. Intersecting with it keeps only the matches of the other sequence that finish within eight edges. It is a compact way to bound something like req ##1 ack[->1], whose goto could otherwise wait forever.

No match at all, because intersect needs both sequences to match with the same start and end. In an antecedent, the property then never triggers and passes vacuously. In a consequent, every attempt fails. Cover the intersected sequence, so you see that it can match.

As verdicts on each request they agree: both obligations must hold. The single property gives the conjunction an end point, so you can follow it with ##1 done measured from the later operand. Two assertions report separately, which makes the failing half obvious in the log. Prefer separate assertions unless something must follow the combined end.

Count instead of combining sequences. A counter clears at start and adds err_irq while the burst is open. Then last |-> err_cnt + err_irq == 1 checks the total on the last beat. A pure-SVA form built from err_irq[=1] and within a burst sequence is legal but hard to read. On Verilator 5.052 it also uses two constructs that engine cannot run, while the counter runs everywhere and shows up in the waveform.

a_plain passes: its thread through the second ack at +2 finds done at +3, and one matching thread is enough. a_first fails. first_match keeps only the earliest end point of the range, the ack at +1, so done must come at +2, and it does not. Use first_match when only the earliest occurrence may count, which is what "the first ack" means.

The pair is close but not the same. ack |=> done demands done after every ack, including the second pulse. The first_match form only cares about the first one. If every ack really owes a done, the pair is simpler, easier to debug and runs on every simulator. If later pulses must not owe one, you need the first_match form or a small model that marks the first ack.

Each end point of the antecedent starts its own check of the consequent. Without first_match, two grants inside the window start two obligations for one request, so busy is demanded after each. first_match keeps one end point per start and one obligation per request.

Take req |-> ##[1:3] gnt ##1 busy. Without first_match, the attempt passes if any grant in the window is followed by busy. With first_match(##[1:3] gnt) ##1 busy, only the first grant counts. If busy follows the second grant but not the first, the first form passes and the second fails.

Write a small directed test whose traffic must break the rule: here, an ack at +1 with done only at +3. Check that the assertion reports exactly that failure. If it does not, the tool is not evaluating the construct and the months of passes are worthless. This negative control belongs next to every non-trivial property.