Writing good formal properties is skilled work, which is one reason many teams use formal less than they could. Yet some of the most widely used formal tools in chip design need no properties at all. Synthesis teams prove every netlist equivalent to its RTL; integration teams prove every top-level wire connects where the specification says. These apps ask one fixed question, generate the properties themselves, and answer it exhaustively.
What questions can formal apps answer, and when should you use them?
The obvious way to check that a netlist matches its RTL, or that an SoC's pins connect correctly, is to rerun simulation on the new version. Simulation samples; a synthesis bug that changes one gate's behaviour under one rare input pattern, or a swapped wire used only in test mode, can pass every regression. These questions have a precise, mechanical form ("are these two the same?", "is A connected to B?"), which is exactly what formal answers completely.
App | Question | Needs |
|---|---|---|
Equivalence checking | Do two versions (RTL and netlist, or RTL before and after a change) behave identically? | Both designs; for sequential changes, a mapping or a sequential equivalence engine |
Connectivity checking | Does every specified connection exist, through the specified path and conditions? | A connection table, often a spreadsheet from integration |
X-propagation | Can an unknown value (uninitialised register, undriven net) reach an output or a control decision? | The design and its reset scheme |
Register checking | Do register addresses, reset values and access types match the register specification? | The machine-readable register map (lesson 2.4) |
Clock-domain crossing (CDC) | Is every crossing between clocks synchronised correctly? | Clock definitions; mostly structural analysis plus formal for protocols |
Unreachability (cover analysis) | Can this coverage bin or code ever be reached? | The design, its assumptions and the coverage database (lesson 6.6) |
Deadlock and liveness apps | Can the design reach a state from which it never progresses? | The design and fairness assumptions |
App | DCRouter question | Bug Zoo connection |
|---|---|---|
Register checking | Do CTRL's reset value, the ERR_CNT and PKT_CNT access types and the unmapped-address response match the register table? | BUG_17, BUG_18; part of BUG_16 and BUG_19 |
Equivalence checking | After a timing fix in the arbiter, is the router still equivalent to the version that passed regression? | Any of the 24 bugs introduced by an edit |
X-propagation | With the FIFO memories uninitialised, can an X reach out_data or a grant? | Reset bugs like BUG_17's class |
Unreachability | Is "CTRL lp_en 0" reachable? (yes; it is a legal write) | Lesson 6.6's holes |
Connectivity | In an SoC, does DCRouter's sleeping output reach the power controller? | Integration bugs (lesson 1.5) |
Run them as part of the flow, not as one-off checks: equivalence after every synthesis, connectivity after every integration change.
Feed them the real specifications: the register table and the connection table are the oracles (lesson 2.4).
Read their waivers carefully: an equivalence check with unmapped points or a CDC run with blanket waivers has proved less than its pass suggests.
Practice | Purpose |
|---|---|
Equivalence checking at every synthesis and ECO | Netlists proved to match the verified RTL |
Connectivity checks generated from integration spreadsheets | SoC wiring proved, not sampled |
Register checks from IP-XACT or SystemRDL | Every register's address, reset and access proved (fact V4) |
CDC and reset-domain analysis on every release | Structural crossing bugs found before simulation |
A team (illustrative) ran equivalence checking on every netlist but had, months earlier, marked a block's scan-chain reordering as "don't verify" to silence an early mismatch. A later ECO changed functional logic inside that region. The equivalence check passed, because the region was excluded, and the change broke a rarely used mode in silicon. Exclusions in an app are assumptions like any other (lesson 7.4).
Register checking: it compares CTRL's reset value with the machine-readable register map, which says 0x3F.
It proves two implementations are the same, not that either is right; a bug in the verified RTL is faithfully preserved in an equivalent netlist.
Formal apps answer one fixed question each, exhaustively and without hand-written properties.
Equivalence, connectivity, X-propagation, register, CDC and unreachability apps belong in the default flow.
Their exclusions are assumptions and must be reviewed.