Design verification is unequivocally, the “pain point” of modern hardware and embedded systems. In terms of computational and human resources spent, this is the bottleneck of every system development process. The reason is that correctness is not a negotiable feature in any system; however, the size and complexity of the systems that we want to build surpasses the computational capacity available to assure this correctness. In other words, we design systems we do not know to verify. There are many manifestations of the verification problem. Formal verification or exhaustive traversal of all reachable states to ensure correctness, although highly scalable now, cannot be used to verify the complete system due to computational capacity. Input stimulus generation is intractable for all system inputs. Constrained random testing or formal verification involves manually specifying constraints tediously. Coverage metrics that can capture the real value of tests and properties (assertions) are as yet elusive. Our research group has been working towards each of these issues in the larger verification problem.
Automatic input stimulus/test generation:
Generating interesting, high coverage tests is a computationally complex problem. We have developed HYBRO and STAR, algorithms for generating test inputs based on static and dynamic analysis of the control data flow graph (CDFG) of the RTL design.
A GoldMine based counterexample guided decision tree learning method we invented, can achieve coverage closure and indicate when testing is “done” and can be stopped. This is a major challenge in verification, with most test coverage curves looking like plateaus after initial high coverage. Such an algorithm that monotonically increases coverage and converges to a provably correct, canonical data structure has not been shown before. This result has implications on the currently perceived limitations of random pattern generation and directed tests.
Emulation, debugging and coverage:
Simulation time for even the subset of inputs that we generate tests for is considerably high. Hence emulation methodologies are frequently used for expediting the simulation speed. Although the performance speedup is observed to be of the order of 300X, emulation has the handicap of having little to no observability. As a result, it is very difficult to assess coverage of a test that has passed during emulation, or determine what is in error when the test fails. These two aspects- coverage of a passing test and debugging of a failed test are two sides of the same coin. A related, emerging problem is debugging of the Register Transfer Level (RTL) design in general. When a test or an assertion fails, the resulting obligations are to localize the problem and diagnose what it is. Amidst thousands of lines of RTL source code, and heterogeneous IPs at the system level, manual debugging is a very arduous, time consuming process. Automatic methods for diagnosis and debug are highly desirable.
Formal methods for equivalence checking and property checking:
We have developed methods based on static analysis of the design CDFG, that can perform equivalence checking between system level and RTL, as well as reduce the design space for model checking and other verification technologies. We have also developed automated deductive methods to verify circuits that are known to be hard for bit level verification algorithms like 128-bit multipliers.
- Links for downloading HYBRO and STAR: HYBRO
- GoldMine’s test coverage closure tool is available with the GoldMine download at http://goldmine.csl.illinois.edu
- Viraj Athavale,Sam Hertz, Darshan Jetly, Vijay Ganesan, Jim Krysl and Shobha Vasudevan, Using static analysis for coverage extraction from emulation/prototyping platforms, IEEE/ACM/IFIP international conference on Hardware/software codesign and system synthesis, (CODES+ISSS) 2012: 207-214
- Lingyi Liu and Shobha Vasudevan Efficient validation input generation in RTL using hybridized source code analysis, Design Automation and Test in Europe (DATE) 2011: 1596-1601
- Lingyi Liu and Shobha Vasudevan STAR: Generating Validation Inputs by Static Analysis of RTL, International High Level Design Validation and Test Workshop (HLDVT) 2009: 32-37
- Lingyi Liu, Shobha Vasudevan, Scaling RTL property checking using feasible path analysis and decomposition, ACM Great Lakes Symposium on VLSI (GLSVLSI) 2013, pp 173-178
- Shobha Vasudevan, E. A. Emerson and J. A. Abraham. Improved Verification of Hardware Designs through Antecedent Conditioned Slicing, International Journal on Software Tools and Technology Transfer (STTT), 9(1): 89-101 (2007)
- Shobha Vasudevan, Vinod Viswanath, and J. A. Abraham . Efficient Microprocessor Verification Using Antecedent Conditioned Slicing, International Conference on (VLSI Design) 2007: 43-49
- Shobha Vasudevan and Jacob A. Abraham. Static Program Transformations for Efficient Software Model Checking, Book chapter in World Congress of Computers (WCC), 2004. IFIP Congress Topical Sessions 2004: 257-282
- Seyed Nematollah Ahmadyan and Shobha Vasudevan, Efficient Stochastic SAT Solving Using Random Graphs. Invited paper in Workshop for Constraints in Formal Verification (CFV), 2013
- Sankar Gurumurthy, Shobha Vasudevan and J. A. Abraham. Automated Mapping of Pre-Computed Module-Level Test Sequences to Processor Instructions, International Test Conference (ITC)2005:10-20
- Sankar Gurumurthy, Shobha Vasudevan and J. A. Abraham. Automated functional propagation of module level test responses, International Test Conference (ITC) 2006: 1-9