Abstracts
| Verification of Embedded Software in Industrial Microprocessors |
| Eli Singerman (Intel Israel) |
| Abstract: The validation of embedded software in VLSI designs is becoming increasingly important with their growing prevalence and complexity. This talk will provide an overview of several methods we have developed for verification of embedded SW in industrial microprocessors. I will talk about a compositional approach to generate a formal model of the design, formal property and equivalence verification techniques, and on employing formal methods for improving traditional simulation based validation methodologies through automatic coverage and test-generation. I will conclude by briefly describing the application of these techniques to two variants of embedded SW, namely microcode and firmware for power management. |
| Pre- and Post-Silicon Verification and Debugging with High Level Design |
| Masahiro Fujita (University of Tokyo) |
| Abstract: Due to high complexity of today's system designs, verification should be performed as high and abstracted level as possible, since in higher levels designs, things to be reasoned about become much fewer than the ones in lower level such as RTL/gate. In this talk, pre-silicon formal verification techniques targeting C-based designs and even higher than them are first reviewed with an emphasis on our own verification framework called FLEC as well as our interactive generation methods of specifications through requirement analysis. Then application of such high level formal verification methods to post-silicon verification and debugging are introduced. As it is almost impossible to eliminate all of the bugs before silicon, post-silicon verification and debugging are becoming key issues for high quality hardware products. In this talk, we describe how post-silicon reasoning can become a lot more efficient by incorporating information from high level designs and establishing mapping between chip behaviors and high level ones. |
| On the Validation of Embedded Systems through Functional ATPG |
| Giuseppe Di Guglielmo (University of Verona / University of Tokyo) |
| Abstract: Increasing size and complexity of digital designs has made essential to address critical verification issues at the early stages of design cycle. Therefore, automated verification tools are necessary at higher levels of abstraction, but they are still in a prototyping phase. In this context, a valuable solution for the functional validation is represented by dynamic verification which uses simulation-based techniques for stimulating the whole design under verification (DUV). In this talk a functional automatic test pattern generator (ATPG) is proposed exploiting extended finite state machine (EFSM) paradigm. EFSMs are deterministically explored by using learning, walk heuristics, and backjumping. The integration of such strategies allows the ATPG to more efficiently analyze the state space of the DUV and generate effective test sequences. Besides the EFSM-based engine, a simulator for functional faults is proposed. The fault simulator exploits both a serial simulation engine, at functional level, and a parallel simulation engine, at bit-level. In particular, the parallel simulation engine adopts bit-level techniques, like vectorization and concurrency, by applying them to a C-representation of the design at logic-level. |
VLSI Design and Education Center (VDEC), The University of Tokyo