Exploring New RTL with Formal
Use formal as a designer's microscope: ask "can this happen?" with covers, poke at behaviours, and find spec holes before any testbench exists — on a 4-floor lift controller.
What you will learn
- Plan a lightweight design-exploration session: questions, simplifications and exit criteria.
- Use covers to generate waveforms on demand and read them critically.
- Steer the tool with temporary constraints to answer "what if" questions.
- Discover a liveness (starvation) problem and fix it in the design.
Lessons
- 5.1Formal as a designer's microscopeWhat design exploration is and why designers love it.
- 5.2The example: a 4-floor lift controllerSpecification and RTL for a small elevator controller.
- 5.3Planning an exploration sessionQuestions, simplifications and when to stop.
- 5.4First covers: watching the lift moveGenerate waveforms on demand and read them critically.
- 5.5Sharper questions with assertionsTurn intuitions into safety assertions and prove them.
- 5.6Liveness: finding starvationA loop counterexample exposes a spec hole; fix and re-prove.
- ✎Chapter quiz (4 questions)