Design verification is universally thought of as a "pain point" of the modern system design cycle. We build systems that we do not know how to verify. Then, we spend a lot of human and computing resources and time trying to convince ourselves that what we built is correct. At the heart of the verification process is the necessity to "know what one is looking for," or specifications of how the system should behave. The verification itself is only as good as the specifications or properties that are being checked for. Assertions provide a mechanism to express desirable properties or invariants in the system.
Assertions can express internal system behavior beyond input/output based simulations. They also provide more design visibility for verification and debug. Verification teams have been migrating steadily towards assertions, and this is only projected to increase. The big question in assertion based verification is- who's to write the assertions? Temporal reasoning is hard for the human mind and inter-modular assertions can be infeasible to write. Most importantly, the "design perspective" should be different from the "verification perspective", i.e., checking for exactly the same attributes that the designer had in mind will not expose as many bugs as an independent set of checkers will. As a result, assertions are accepted to be effective, but require a lot of manual effort and time to generate, with no guarantees about the quality or coverage of assertions produced.
The GoldMine Solution
GoldMine is an automatic assertion generation tool from Prof. Shobha Vasudevan's research group at the University of Illinois. GoldMine generates assertions in Verilog RTL. GoldMine can generate propositional (input/output behavior assertions) as well as temporal (across time cycles) assertions. Assertions generated by GoldMine can span multiple clock cycles as well as multiple RTL modules. GoldMine can generate assertions that are very close to assertions generated by expert humans. Complex assertions in GoldMine can surpass human generated assertions in their subtlety, scope and behavioral coverage. GoldMine assertions for a target variable are rank ordered according to their value as determined by our ranking algorithms. GoldMine assertions have been optimized for high readability and usability, despite expressing subtle, wide scope behavior. GoldMine also provides statement code coverage of assertions generated, thereby giving a value proposition for every generated assertion.
GoldMine uses data mining along with static analysis to generate assertions. There are multiple data mining algorithms implemented in GoldMine. Static analysis of the design used to guide the data mining engine. The likely invariants generated by the data miner from dynamic simulation behavior are validated using formal verification. Hence GoldMine assertions are all true (invariant) in the RTL design. Considerable research has gone into making GoldMine an accessible technology, with respect to the ability of a human to understand and utilize the assertions. We have also developed technology to estimate and report the coverage of an assertion. GoldMine is an inherently scalable methodology. Recently, we have shown that GoldMine scales to the OpenSparc T1 processor, PCI bus and other industrial scale designs. GoldMine can be used for giving hints to designers to write assertions. It can also be used as a regression testing suite for a legacy or known good design. GoldMine can be made to generate assertions for random input stimulus, providing static checkers that can calibrate the highly unpredictable random pattern generation process. GoldMine can also generate assertions in System C at the Transaction Level Modeling (TLM) level. These assertions are generated from the System C specifications, so they can be used for checking equivalence of the corresponding RTL implementation. GoldMine also generates high coverage input stimulus for design validation as a side effect of the assertion generation.