Every handoff between RTL and silicon rewrites the design: synthesis maps it to cells, the clock tree adds skew, an ECO patches a wire. Equivalence checking proves the logic matches, but it does not prove the chip works with delays, resets and X values in place. Gate-level simulation runs the netlist with timing to find what the proofs abstract away. Its one job is the scope: what GLS can show that RTL cannot, and what it must never be asked to show.
GLS replays a slice of the RTL suite — sanity, sweeps, boot — on the synthesised netlist with delay annotation, and any divergence is a fidelity fact. The finds fall into four bins. Timing: a path that met constraints in isolation but fails with real clocks and skew, especially reset release and the crossing FIFOs. Library timing checks also report a setup or hold violation on an unsynchronised crossing such as planted bug 5 (the flop output goes to X), so gate-level simulation with annotation can flag it; the structural CDC check remains the guard that does not depend on a violation happening to occur. Reset: tree skew that staggers release across the domain, and clock-gate and clock-mux cells whose enables are unknown at start. ECO: a patched netlist whose equivalence was waived and whose behaviour moved, caught by equivalence as a gate to tapeout and by GLS as the backstop. X-handling: initialised flops that hide a missing reset in RTL but propagate X with delays, and the reverse — X optimism that masks a real bug.
# not-run: GLS cost rule, NanoSoC teaching values
# As a general guideline GLS runs many times slower than RTL on the same
# stimulus: the netlist has far more primitives and the delay engine evaluates
# every edge. So the GLS suite replays the fast suite — sanity, sweeps, short boot —
# and the full 12.581 ms boot once per final netlist (the readiness checklist
# requires it as a blocking item) and after any netlist change that touches the boot path.
# Weekly cadence, or on every netlist and ECO delivery, whichever is sooner.The GLS suite is named as a subset of the RTL suite with the selection reason per test, never a separate invention.
Every netlist delivery — synthesis, ECO, clock-tree change — names its GLS rerun before signoff consumes it.
Equivalence results gate the GLS run: a waived equivalence needs a GLS proof of the waived cone.
A GLS-only failure is bisected by annotation: rerun the same test with zero delays, then with unit delays, then with full annotation. Zero-delay green with full-delay red is timing; zero-delay red is a netlist functional change, usually an ECO or an uninitialised flop. Compare against the RTL run with identical stimulus and seed — the bench must be shared, or the comparison proves nothing.
No: it already fails with no delays, so timing is not the cause. Suspect a functional difference in the netlist: a flop with no reset that RTL initialised to zero, library-model X handling, or an ECO. Fix the comparison setup or the design before reading anything into delays.