Where Assertions Live

Three homes, three tradeoffs

Every assertion lives in one of three places: inline in the RTL next to the logic it guards, in an interface alongside the signals it constrains, or in a separate checker module attached with bind . The choice decides who owns the file, what the assertion can see, whether it survives reuse, and how it flows to synthesis and formal — it is an architecture decision wearing a style-question costume.

PLACEMENT TRADEOFFS — the comparison interviewers want

  criterion        INLINE RTL          INTERFACE           BIND + CHECKER
  ──────────────────────────────────────────────────────────────────────
  sees internals   yes (full scope)    ports only          yes (bind scope)
  owner            designer            shared/DV           DV
  RTL edits        yes                 no (if/def free)    none at all
  reuse            travels w/ module   travels w/ protocol travels w/ DV env
  synth exposure   needs guards        usually excluded    never compiled
  best for         design intent,      protocol rules at   legacy code, VIP-
                   FSM/cnt invariants  every instance      style rule sets
  typical author   RTL engineer        protocol owner      verification eng
  failure debug    points at exact     points at the       points at module
                   line of logic       interface instance  type instance

Each option in code

// 1) INLINE — designer documents intent next to the logic.
//    Sees internal state (gnt_q, state) without ports.
module arbiter (...);
  ...
`ifndef SYNTHESIS
  ap_onehot: assert property (@(posedge clk) disable iff (!rst_n)
    $onehot0(gnt_q)) else $error("multi-grant");
`endif
endmodule

// 2) INTERFACE — protocol rule rides with the bus definition;
//    every instance of the interface checks itself.
interface axi_lite_if (input logic clk, rst_n);
  logic awvalid, awready; logic [31:0] awaddr;
  ap_aw_stable: assert property (@(posedge clk) disable iff (!rst_n)
    awvalid && !awready |=> awvalid && $stable(awaddr))
    else $error("AW channel unstable while stalled");
endinterface

// 3) BIND — zero RTL edits; DV-owned file attaches a checker
//    to every instance of a module type, seeing its internals.
bind fifo_core fifo_chk #(.DEPTH(16)) u_chk (
  .clk(clk), .rst_n(rst_n),
  .push(wr_en && !full), .pop(rd_en && !empty),
  .count(occupancy_q));            // internal signal — bind can see it

Ownership in practice

• Designers own inline assertions: micro-architectural invariants (one-hot, counter bounds, FSM legality) that only they know — written while the intent is fresh.

• Protocol owners own interface assertions: handshake stability, channel ordering — one definition, enforced at every instance automatically.

• DV owns bind files and checker libraries: end-to-end and reused checks, plus everything on legacy or third-party RTL nobody may edit.

• Review rule: a failing inline assertion pages the designer; a failing bind checker pages DV first — placement is also a triage routing table.

Surviving synthesis and tool flows

Concurrent assertions are not synthesizable, and while most synthesis tools ignore them, relying on every tool in the flow to ignore them is how builds break at midnight . Inline assertions get guarded; interface and bound assertions are usually structurally excluded from the synthesis file list anyway.

// Standard guard pattern for inline assertions
`ifndef SYNTHESIS
  ap_no_ov: assert property (@(posedge clk) disable iff (!rst_n)
    !(push && full));
`endif

// Some flows use pragmas instead — equivalent intent:
// synopsys translate_off
//   ...assertions...
// synopsys translate_on

// Project hygiene: define ONE guard macro convention and lint for
// unguarded asserts in RTL files; mixed conventions rot fast.

Formal vs simulation reuse

• The same property text serves both engines — that is SVA's core promise; placement decides how easily formal can compile it.

• Bind + checker is the most formal-friendly home: the formal tool compiles RTL plus bind files, no testbench needed.

• Simulation-only constructs leak in via action blocks and TB hierarchy paths — keep properties pure, side effects in the action block only.

• In formal, assertions on inputs become assume candidates: the same checker's input-protocol properties flip from assert to assume at the block boundary.

• Bounded-liveness windows tuned for sim (##[1:200]) may be relaxed back to s_eventually in formal where liveness is provable — parameterize the bound.

Reuse across projects

REUSE PATHS — what travels with what

  inline assertion ───── travels with the MODULE
       arbiter.sv reused → its invariants come along free
  interface assertion ── travels with the PROTOCOL
       axi_lite_if reused → every new project's AXI gets checked
  checker + bind ─────── travels with the VERIF ENVIRONMENT
       fifo_chk.sv + bind file → drop onto any project's FIFOs

  Anti-pattern: protocol rules written inline in ONE master's RTL.
  → next project uses a different master; the rules don't travel,
    get rewritten slightly differently, and the two copies diverge.

Interview angle

This is a judgment question, so give a framework, not a favorite: "Where would you put assertions for a FIFO?" — structural invariants (no push-when-full, count bounds) inline or bound to the FIFO since they need internals; the valid/ready rules of the surrounding stream in the interface so every instance inherits them; data-integrity end-to-end checks in a DV-owned bound checker. Always mention ownership (designer vs DV) and the synthesis guard — forgetting ifndef SYNTHESIS on inline assertions is a classic follow-up trap, and noting that bind needs no guard at all (never in the synthesis file list) closes the answer well.

Key takeaways

• Inline = designer-owned intent with full internal visibility; needs synthesis guards.

• Interface = protocol rules that auto-deploy at every instance of the bus definition.

• Bind + checker = DV-owned, zero RTL edits, sees internals, the most formal-friendly home.

• Placement routes triage: inline failures page designers, bound-checker failures page DV.

• Reuse follows placement — module, protocol, or verification environment travel paths.

Common pitfalls

• Unguarded inline assertions reaching synthesis or lint flows — broken builds far from the author.

• Protocol rules inline in one module's RTL — they don't travel; copies diverge across projects.

• Bind by instance path instead of module type — newly added instances silently unchecked.

• Action blocks referencing testbench hierarchy from checkers meant for formal — formal compile breaks.

• No ownership convention — failures bounce between design and DV while the bug ages.