Q&A: Methodology & Placement

Q: Who should write assertions — designers or verification engineers?

Direct answer: both, on different layers. Designers write white-box assertions: FSM transition legality, onehot encodings, counter bounds, handshake invariants between internal blocks — they know the micro-architecture and its intent, and these assertions catch bugs at the point of cause. DV engineers write black-box assertions: interface protocol checkers, end-to-end ordering and integrity rules — independent of the designer's mental model, which is precisely the value: an assertion written from the same misunderstanding that produced the bug will agree with the bug.

LAYERED OWNERSHIP

  designer (white-box, inline or same-file)
    a_fsm_legal, a_state_onehot, a_fifo_count, a_grant_onehot
        │  catches bugs AT THE CAUSE, cheap to localize
        ▼
  DV (black-box, bind files on interfaces)
    ap_axi_handshake, ap_resp_ordering, ap_data_integrity
        │  catches bugs AT THE CONTRACT, independent eyes
        ▼
  shared review: every spec MUST/SHALL traced to one of the two

Follow-up: 'What goes wrong when only one side writes them?'

• Designer-only: assertions inherit the designer's assumptions; spec-level misreadings go unchecked — the checker and the RTL share the bug.

• DV-only: internal corruption (state encoding, counter wrap) surfaces cycles later at an interface, multiplying debug distance; white-box assertions are the difference between failing at the cause and failing at the symptom.

Junior vs senior answer

• Junior: picks a side ('DV owns verification').

• Senior: layered ownership with the independence argument for DV protocol checks and the debug-distance argument for designer white-box checks.

Q: Inline assertions vs bind files — tradeoffs?

Direct answer: inline (in the RTL module) gives direct visibility of internal signals, travels with the code through reuse, and is naturally maintained by the designer who edits that module. bind attaches a separate checker module to instances from outside — zero RTL modification (vital for third-party or silicon-proven IP no one may touch), clean separation for DV ownership, one checker reusable across instances and projects, and the whole thing drops out of synthesis by construction. Standard split: micro-architectural invariants inline; protocol/interface checkers bound.

// checker module — knows nothing about who instantiates it
module fifo_checker #(parameter DEPTH = 16) (
  input logic clk, rst_n, push, pop, full, empty
);
  a_no_push_full: assert property (
    @(posedge clk) disable iff (!rst_n) full |-> !push);
  a_no_pop_empty: assert property (
    @(posedge clk) disable iff (!rst_n) empty |-> !pop);
endmodule

// bound to every fifo instance — RTL file untouched:
bind fifo fifo_checker #(.DEPTH(DEPTH)) u_fifo_chk (.*);

Follow-up: 'Costs of bind?'

• Port-list maintenance: RTL signal renames break the bind silently-at-elaboration; .* helps and hurts (implicit matches can rebind to the wrong renamed net).

• Internal signals must be reachable — binding into the module scope helps, but deep hierarchy references get brittle.

• Discoverability: the checker lives far from the code it checks; reviewers must know to look.

Junior vs senior answer

• Junior: 'bind is for when you can't edit the file'.

• Senior: the ownership/reuse/synthesis triple for bind, the locality argument for inline, the standard inline-microarch/bound-protocol split, and bind's maintenance costs.

Q: What happens to assertions in synthesis?

Direct answer: standard logic synthesis ignores concurrent assertions — they are verification constructs with no hardware semantics, typically also fenced with synthesis translate_off guards or stripped because they live in bind files never handed to the synthesis flow. Two important refinements: formal and emulation flows DO consume assertions (emulators can compile them into hardware monitors — assertion cost suddenly matters); and immediate assertions inside RTL processes must not have side effects in their action blocks, or simulation and synthesized netlist behavior diverge.

Follow-up: 'Any hardware design styles where assertions effectively reach silicon?'

Safety-critical and DFT-adjacent flows sometimes re-implement key assertions as synthesizable hardware checkers (error detection logic, bus monitors with error counters). The SVA itself is not synthesized — an engineer translates the property into RTL. Distinguishing 'assertions are ignored' from 'assertion INTENT can be productized as monitors' is the senior nuance.

Junior vs senior answer

• Junior: 'synthesis skips them'.

• Senior: skipped by logic synthesis, consumed by formal/emulation (with cost), action-block side-effect hazard, and the hand-translated hardware-monitor pattern in safety flows.

Q: What is your reset strategy for an assertion suite?

Direct answer: classify every assertion into one of three reset relationships. (1) Functional checks — silent during reset: disable iff (!rst_n), which also kills attempts in flight when a mid-sim reset lands, exactly the desired abort semantics. (2) Reset-behavior checks — outputs at reset values, busy clears within N: these run during reset and must NOT carry the disable, or they self-disable. (3) Reset-exit checks — no X after deassert, first transaction waits for init: anchored on $rose(rst_n), no disable on the same reset. The strategy is the classification — the bugs come from assertions filed in the wrong class.

RESET CLASSIFICATION CHECKLIST

  class            disable iff?   example
  ─────────────────────────────────────────────────────────
  functional       YES            $rose(req) |-> ##[1:4] ack
  during-reset     NO  (fatal!)   !rst_n |-> !valid
  reset-exit       NO             $rose(rst_n) |=> !$isunknown(ctrl)

  Extra rules:
  • async reset still sampled at clk — between-edge behavior unseen
  • mid-sim reset: disable iff aborts in-flight attempts = correct
  • multi-reset domains: each property disables on ITS domain only

Follow-up: 'disable iff vs sync_reject_on?'

disable iff is asynchronous-abort semantics evaluated on the live (not sampled) value, and the aborted attempt is removed without verdict. The accept/reject operators give finer-grained, sampled, sequence-level control. For suite-wide reset policy disable iff is the workhorse; knowing the distinction exists is usually all the interview wants.

Junior vs senior answer

• Junior: 'put disable iff (!rst_n) on everything' — erases the entire during-reset class.

• Senior: the three-class taxonomy, mid-sim abort semantics as a feature, and domain-correct disables in multi-reset designs.

Q: How many assertions is enough?

Direct answer: wrong axis — count is a vanity metric. The defensible measures are coverage of intent : every spec MUST/SHALL and every micro-architectural invariant traced to a property; effectiveness : assertions demonstrably fire on injected bugs (mutation testing) and are non-vacuous in regression; and failure quality : when one fires, it localizes the bug to a cycle and a rule, instead of 'something somewhere mismatched'. A block with 40 sharp, traced, non-vacuous assertions is better verified than one with 400 auto-generated stubs nobody can triage.

Follow-up: 'But management wants a number — what do you report?'

• Plan-trace ratio: spec rules with at least one mapped property / total rules.

• Non-vacuity ratio: assertions with non-vacuous activity in merged regression / total.

• Mutation kill rate on a sampled set — the closest thing to ground truth for checker quality.

• Report density (assertions per kLOC) only as a smell test for blocks at zero.

Junior vs senior answer

• Junior: offers a rule of thumb ('one per interface signal', 'N per kLOC').

• Senior: rejects raw count, substitutes traceability, non-vacuity and mutation-kill metrics, and still gives management a reportable dashboard.

Key takeaways

• Layer the ownership: designer white-box at the cause, DV black-box at the contract — independence is the point.

• Inline for micro-architecture, bind for protocol and untouchable IP; bind buys separation at a port-maintenance cost.

• Reset strategy = classifying every assertion into functional / during-reset / reset-exit, with disable iff only on the first.

Common pitfalls

• disable iff blanket-applied — during-reset checks silently self-disable (the classic).

• Bind files drifting after RTL renames — elaboration failures or, worse, silent mis-binding with .*.

• Selling assertion count as verification progress — vacuous stubs inflate it for free.