What makes something a formal app?
General FPV asks you to think hard about properties. Many verification problems, however, have the same shape over and over again: "this pin is connected to that port in mode X", "this register field is read/write", "this coverage bin can never be hit". For such problems, tools and teams build formal apps: flows where the properties are generated from a structured description and the user mostly reviews results.
| App | Property source | What it proves |
|---|---|---|
| Connectivity | Spreadsheet / CSV of connections | Signals are connected (possibly through muxes and pipeline stages) under the right conditions |
| CSR / register | Register description (IP-XACT, SystemRDL, spreadsheet) | Access types, reset values, side effects of register fields |
| Protocol checkers | Reusable property library per protocol | Interface rules of AXI-like, valid/ready, credit protocols |
| Unreachable coverage (UCE) | Simulation coverage database | Which uncovered items can never be hit |
| X-propagation | Design + list of qualifiers | Unknown values cannot reach outputs when they matter |
| Sequential equivalence | Two versions of RTL | Changed design behaves like the original (Chapter 8) |
| Security / information flow | Secret sources and observable sinks | Secret data cannot influence certain outputs |
| Post-silicon debug | Lab symptoms | A trace that reproduces the failure |
In this chapter we build small versions of several apps by hand. Commercial tools automate the generation, but knowing what they do under the hood makes you much better at using — and debugging — them.