My first post served as a context for this blog. It also telegraphed my intention to set down a few reasons for the initial difficulties faced by long-time simulation users, specifically verification engineers, in applying formal property verification (FPV). Here is my Top-5 list in no particular order.1. Procedural Versus Declarative Expression Of IntentSimulation languages like Verilog, SystemC, e and the rest are procedural languages (blurring the lesser differences between OOP, AoP and procedural code). Simulation testbenches that model the verification environment are typically modeled using procedural code, though there is an increasing shift to declarative idioms with constraint specifications in sophisticated environments.FPV environments on the other hand are almost completely declarative (PSL, SVA and OVL), whether they are assertions that state something about the design behavior or constraints that model the design environment.I have found that, much like the procedural versus declarative debates in the AI community, the debate between FPV and simulation evangelists (the former in shorter supply) is ultimately irrelevant. I think there is increasing consensus that each has strengths that are complementary in most cases. The point remains that the two are distinct ways of thinking about verification problems and knowledge of one (idioms and patterns) does not always translate to the other.2. If Not Simulation, Then What?If only I had a penny for every discussion I have had about whether formal analysis is basically like an under-the-hood simulation within the set of constraints. While such a constraint-based simulation is definitely possible, FPV does not use simulation in converging assertions to proofs. Instead it relies on clever representations and algorithms to get mathematical proofs for the assertions about the design.Considering that there are about a handful of people that can talk intelligently about the algorithms used in FPV, this watered-down answer does not satisfy an engineer in the trenches. This is in contrast to the simulation world where most engineers understand the mechanics of event-driven simulation and there is no notion of not converging to a desired result.Verification engineers are paid to suspect and are properly suspicious of anything that is presented to them as black-magic. In cases where I have encountered this sort of thing, I like to point to that poster-child of formal methods - equivalency checking. Formal tools use algorithmic techniques to analyze a state transition only once, and can examine many state transitions simultaneously. Contrast this with simulation in which there are numerous repetitions of state transitions. It is in this sense that formal analysis increases coverage per unit time.
As in simulation, there is feedback from the analysis that allows the fine-tuning of the verification environment. Only, this feedback is different from that in simulation. It is a matter of training and application to get comfortable with any new technology and FPV is no exception.3. The Capacity IssueSimulation users make an implicit assumption about their environments - that they will scale with their design as long as they are able to crank the requisite number of simulation cycles. This is typically done by throwing more machines at the problem, or even relying on hardware accelerators for larger designs.This is typically not true for FPV. Complexity in formal analysis is exponential in design size. Despite rapid strides in improved performance and capacity of formal engines, commercial FPV tools do not scale like simulation.New users can get discouraged with FPV as a result. Almost every instance in which I have seen this happen, the problem has been the imbalance of design choice versus user experience. Choosing a target design (or function within a design) commensurate with the experience of the verification engineer is a critical component of successful FPV application. Which leads us to...4. Inadequate PlanningLike simulation, FPV requires thorough planning to focus the verification effort. Unfortunately, it is common to encounter situations where FPV is applied without a set of clear goals. Perhaps this has to do with the economy of expression in property specification languages, that allows easy setup of an FPV environment. Be that as it may, experience shows that successful application of FPV, that justifies the investment, is deterministic only in the context of a verification plan.A plan should address the following questions amongst others -