The uptake of formal verification methodologies is held back by ten persistent myths, according to Professor Ashish Darbari, principal hardware design engineer and member of the advanced verification methodology group at SOC IP company Imagination Technologies.
"The blocks to the adoption of formal methods are myths," he told the Formal Verification Conference, organised by TVS in Reading, England, last week. "Writing formal tools is tricky but the application of formal is not rocket science. It just takes common sense."
Darbari, who is a visiting professor at the University of Southampton, said that the first myth aboutformal is that you need a PhD to use it. He said this myth is gradually disappearing, and is rooted in a poor understanding of how to use formal effectively. Part of this is down to the use of specialist terms and mathematical notations that engineers are not trained to understand. There's also a wide gap between the high-end academic research in formal verification and what engineers care about in industry, which can be bridged with appropriate training materials.
The second myth is that formal verification is hard because you need specifications, and RTL is not a
substitute for a specification. Why do people say this? Darbari argued it is because some people don't have a specification to start with, formal methods blur the distinction between informal and executable specifications, and that using the techniques exposes poor specifications quickly.
"The boon and the bane of formal is that you start to get failures earlier in the flow, so you start to feel the shortcoming of the specification sooner," said Darbari. "Clear, precise, non-ambiguous specifications are a key for all forms of design and verification."
Darbari's third myth is that formal techniques don't scale: "It's a convenient reason for some people not to try." He says people argue that formal can’t be applied to large designs, that you need to choose the right design size, and that you definitely can’t verify a SoC with formal. The truth is that scale is a problem for all verification techniques, and that the application of formal approaches should be regarded as the “art of possible”.
The fourth myth is that formal techniques don't offer any coverage metrics, so it is hard to know if you have done enough, and to convince your boss that you’re meeting the requirements of metrics-driven verification strategies.
"The idea that formal doesn't have any coverage was quite true five years ago but it isn’t true today," he said. "If you want numbers, the tools can spit out numbers.
"There is an obsession with metric-driven verification and I'm not opposed to that, so long as the right set of questions is asked at the same time."
Darbari argued that formal tools offer: structural checks of code, toggles, and FSM; semantic coverage of trace, cover properties, over-constraint detection; and mutation-based analysis, which can offer an extra layer of confidence.
The fifth myth is that formal techniques takes a long time: "It is not true, but where do you start?"
Darbari argued that it is easy to get started with formal techniques in a few steps:
- define your clocks and reset
- apply your design reset
- load an initial state
- define effort and solvers
- hit the 'prove' command
The tools can run quickly, especially if you have bugs in the design or its testbench, such as missing constraints, or wrong asserts/covers. Full proofs requires ‘appropriate’ formal models, in the same way that getting good simulation results needs good simulation models.
The sixth, and one of the oldest, myths is that formal techniques are only useful for building proofs.
"In fact, model checking is fantastic for bug hunting."
The seventh myth is that formal techniques are only useful for finding corner-case bugs.
"It is good for this but it also good for doing bring up and basic testing, such as whether it is possible to fill a FIFO, drain a buffer, or to have two mutually exclusive threads accessing a shared resource at once.
"Why would you write a Verilog/VHDL testbench when you can write a cover property or a simple assertion?" Darbari asked.
The eighth myth is that formal is only useful for verification, whereas it can actually be used in validation, for visualising scenarios, during design bring-up to establish whereto there are bugs in individual blocks, for bug hunting, and for architects to specify interfaces and other details of the design. In this case, these specs can then become executable checks of those aspects of the design. Darbari added that automated flows relying on formal techniques underpin linters, X-propagation checks, clock domain crossing verification, pin-connectivity checks and so on.
His ninth myth is that once you have applied formal techniques, you needn't simulate. In fact, he argued, simulation is necessary to drive all the key interface assertions at the system level, especially those used as constraints for block-level formal checks. Simulation is also useful for getting rid of common mode errors, by re-exercising a few sets of assertions in simulation to get an extra level of checking. Simulation can also be used to address issues where formal techniques were unable to complete proofs.
The tenth and final myth that Darbari listed was the idea that if you have done simulation with 100% coverage, you don't need formal techniques.
"Coverage will only give you confidence that a design works 'somewhat', not that it always works and is starvation-free, deadlock-free, livelock-free and so on. You need to get your guarantees whenever you can, and simulate if you must."
Darbari ended his presentation by arguing that "verification is risk management, and we're all in it together.
"Don’t believe the myths. To verify multi-million flop designs to get the right trade-off between quality and time-to-market you need formal early, with good methodology, efficiency and reuse. Think of combining it with simulation.
"There must be no religion other than rational thinking," he added. "You need a careful balancing of choices and methodologies."
To download Professor Ashish Darbari's presentation, click here.
To access more presentations from the TVS Formal Verification Conference, click here.