RTL verification guide

RTL Linting: A Practical Verilog/SystemVerilog Lint Checklist

RTL lint is the cheapest, fastest defect filter you have. It reads the structure of every line in your Verilog or SystemVerilog — whether or not a testbench ever exercises it — and flags the patterns that cause simulation/synthesis mismatches and silent data loss before you spend a cycle simulating. This page is a practical, categorized lint checklist: what lint catches that simulation and synthesis miss, the rules grouped by area, how to tier them by severity, where lint sits relative to simulation and formal, and how to triage the findings honestly. It is structural evidence to act on, not a signoff.

What lint catches that simulation and synthesis miss

Simulation only sees the paths your stimulus drives. If a test never asserts a particular control combination, a bug on that path stays invisible — the run is green and the defect ships. Synthesis, for its part, will happily build hardware from ambiguous RTL: it infers a latch from an incomplete combinational block, zero-extends a narrow signal at a port, and drops carry bits on a truncating assignment, all while emitting warnings that are buried in noisy logs nobody reads.

Lint is static and exhaustive over the source. It does not need a stimulus and it does not wait for elaboration noise: it walks the AST and the structural graph and reports every rule match with file and line. That makes it the right tool for the whole class of defects that are about how the RTL is written rather than what value it computes on one trace — inferred latches, incomplete sensitivity, unread logic, multiple drivers, width surprises. None of these depend on a particular input, so a static check finds them once, cheaply, across the entire repository.

The lint checklist, by category

Organize your ruleset by the part of the design it protects. Each rule below maps to a deterministic structural check — ChipVerify AI's analyzers flag these patterns with file-and-line evidence.

Structural / connectivity

• Multiple drivers — a net assigned from more than one continuous or procedural source. In synthesis this is a bus-contention or last-write-wins ambiguity; almost always a bug.
• Undriven / unread signals — an output that is never assigned (driven to its default forever) or a wire that is read but never driven. A typo in a port name often shows up here as an implicit 1-bit wire.
• Dead / unread logic — a register or expression that is computed but feeds nothing observable. Either a leftover from a refactor or a missing connection.
• Implicit nets — Verilog auto-creates a 1-bit wire on an undeclared name. Put `default_nettype none at the top of every file so a typo is an error, not a silent net.

Datapath

• Width mismatches — implicit truncation drops carry/high bits; implicit extension hides intent. The standard requires tools to allow it and does not require a warning.
• Signed/unsigned mixing — mixed arithmetic promotes the expression to unsigned and sign-extension silently disappears. Cast at boundaries with $signed() / $unsigned().
• Bitwise vs logical operator confusion — & where you meant && yields a wide value with the wrong meaning — a width bug and a logic bug at once.
• Out-of-range constant / index — a literal or select that exceeds the declared range is clamped or truncated silently.

Control logic

• Inferred latches — a combinational block that does not assign a signal on every path infers a latch to hold the old value. The most common sim/synth-divergence bug.
• Incomplete sensitivity list — a classic Verilog-2001 always @(...) that misses a signal simulates as a latch but synthesises as combinational logic. Use always_comb (or always @*) so the sensitivity is inferred and the two cannot disagree.
• Case completeness — a case without a default, or a non-exhaustive enumerated case, infers a latch and can leave a state machine wedged. Mark genuinely exhaustive cases unique / priority so intent is explicit.
• Blocking vs non-blocking assignment — blocking = in a sequential block (or non-blocking <= in a combinational one) creates race conditions and sim/synth mismatch. One of the first rules to make fatal in CI.
• Full/parallel case pragmas — a // synopsys full_case comment that lies to synthesis creates a mismatch the simulator never sees. Flag the pragma; prefer unique case.

CDC-adjacent (structural hints, not a CDC signoff)

• Signals sampled in one clock domain but driven in another show up structurally as a flop in clock A feeding a flop in clock B. Lint can surface the structure; a real clock-domain-crossing review needs synchronizer recognition and is a separate analysis.
• Reset signals mixed across domains, asynchronous reset without a synchronized de-assert, and combinational logic in a reset path are all structural hints worth a flag — but treat them as triage pointers, not verdicts.

Worked example: the inferred latch

The single highest-value lint finding. A combinational block that forgets a branch silently becomes stateful. Simulation can pass if the missing branch is never the value the test cares about; the gate-level netlist then disagrees with the RTL.

// BUG: combinational block, but 'y' is only assigned on one branch.
// The synthesiser infers a latch to hold the old value of 'y' when
// sel == 0. Simulation may look fine; the gate-level result diverges.
always_comb begin
    if (sel)
        y = a;        // no 'else' -> 'y' latches when !sel
end

The fix is mechanical: assign the signal on every path. An unconditional default at the top of the block is the most robust form, because every branch after it becomes an override rather than a gap.

// FIX: assign on every path. A default at the top of the block is the
// most robust form -- every later branch is now an override, not a gap.
always_comb begin
    y = '0;           // unconditional default kills the latch
    if (sel)
        y = a;
end

Severity tiers: not every warning is equal

A flat list of thousands of warnings is useless. The discipline that makes lint actionable is tiering — decide once what each rule means for the build, then gate CI on the top tier only.

• Error (block the build). Defects where the simulator and the synthesised hardware can disagree, or where data is silently lost: inferred latch, incomplete sensitivity, blocking-in-sequential, multiple drivers, implicit truncation, lying full/parallel pragmas.
• Warning (fix soon, do not block). Defects that are usually real but occasionally intentional: dead/unread logic, out-of-range constants, unconnected instance ports, missing case default on a provably-exhaustive enum.
• Info / style (track, do not gate). Naming, magic numbers, line length, ordering. Valuable for consistency, never a reason to fail a build on their own.

On a fresh codebase, turn the error tier on from day one. On legacy RTL, freeze the current count and gate so the number can only go down.

Lint vs simulation vs formal

These three are layers, not alternatives. Each catches a class the others cannot, and the cost grows as you go right.

• Lint is static and exhaustive over the source, cheap (seconds on a whole repo), and finds structural defects regardless of stimulus. It says nothing about behaviour.
• Simulation confirms behaviour on the traces you write. It is only as complete as your stimulus and coverage, and it cannot see a path the testbench never drives.
• Formal proves a property over all legal inputs. It is exhaustive on behaviour but expensive and targeted — you specify each property, and proofs can time out into honest inconclusives.

The economical order is lint first (delete the structural defects), then simulation (functional behaviour with coverage), then formal on the properties that justify the cost. For the full picture of how these layers combine before tape-in, see our guide to pre-signoff RTL verification.

How to triage lint findings honestly

A lint report is evidence, not a verdict. Triaging it well is what turns noise into signal:

• Read the evidence, not just the count. Every finding should have a file, a line, and the rule it matched. Confirm the pattern at the source before you fix or waive it — a structural match is a strong hint, not proof of a behavioural bug.
• Fix the error tier; waive the rest with a reason. An intentional truncation or a vendor-IP warning can be waived — but the waiver should be documented, reviewed, and scoped to the exact finding, never a blanket suppression of a whole rule.
• Gate the trend. Configure CI so new error-tier findings cannot be added, even while you burn down the legacy backlog. A clean delta is more honest than a one-time clean run.
• Do not call a clean run a signoff. A green lint pass means the rules you enabled found no matches on the code you scanned. It is pre-signoff structural evidence on open tools — it does not prove correctness and it does not replace commercial EDA lint or a foundry signoff.

Open-source lint engines worth wiring up

• Verible: source-level style and structural rules at commit time — sensitivity, case, naming, implicit truncation — before any elaboration.
• Verilator (-Wall): elaborated warnings on width, unused signals, latches and more; promote the ones that matter to -Werror in CI.
• Yosys (check): structural checks on the synthesised netlist — multiple drivers, undriven nets, combinational loops.

FAQ

Run the whole checklist in one pass

You do not have to wire up and tune three lint engines by hand to get started. Sign in and point ChipVerify AI at your Verilog or SystemVerilog: it runs deterministic structural analyzers for width mismatches, inferred latches, incomplete sensitivity, multiple drivers, dead/unread logic, case completeness and blocking/non-blocking assignment, and returns every match with file-and-line evidence, tiered by impact. It is pre-signoff structural evidence on open tools — not a foundry signoff and not a replacement for commercial EDA lint.