RTL linting (structural) is widely adopted because it is very fast, has clear value, and is easy to use.
Even so, RTL linting does not address control logic issues that require sequential analysis. Additionally, trying to get coverage closure for control logic using simulation is a lengthy and challenging process for complex design. It is also difficult to know if coverage closure is ever reached.
Formal technology has the necessary sequential analysis to find all control logic issues. However, using traditional formal tools requires deep expertise and extensive manual effort to write complex assertions. Thus, it is generally relegated to a formal verification expert.
There is an opportunity for the designers to use automated formal linting during their design process to leverage “exhaustive coverage of formal” with minimal time investment – and no manual writing of assertions.
- Formal linting detects corner-case functional issues early, identifying coverage issues that can be missed in simulation and cannot be detected with structural linting.
- Formal linting has high value control and coverage checks, including FSM deadlocks, unreachable state checks, bus contention, floating bus, range violation, constant net, dead code, and toggle tests, etc.
A two-phase process — RTL Linting + Formal Linting — improves design quality early, before simulation, greatly reducing simulation time and effort by minimizing iterations.