Formal Apps for Everyday Problems
Targeted formal flows that solve common problems with little effort: connectivity, control/status registers, reusable protocol checkers, unreachable coverage, X-propagation and post-silicon debug.
What you will learn
- Recognise problems that a formal "app" solves better than hand-written FPV or simulation.
- Generate connectivity assertions from a spreadsheet-style specification.
- Write register (CSR) properties for RW, RO and W1C fields.
- Build a protocol checker that flips between assume and assert depending on the side being verified.
- Use formal to remove unreachable coverage holes and to reproduce lab failures.
Lessons
- 7.1What makes something a formal app?Fixed property patterns + automatic property generation.
- 7.2Connectivity verificationFrom a connection table to hundreds of generated assertions.
- 7.3Control and status registersProperties for RW, RO, W1C and reserved registers.
- 7.4Reusable protocol checkersWrite interface rules once and flip assume/assert by role.
- 7.5Unreachable coverage eliminationLet formal prove which coverage holes can never be filled.
- 7.6X-propagation, security and post-silicon debugThree more apps in brief.
- ✎Chapter quiz (4 questions)