Symbolic simulation as a simplifying strategy for SoC verification
| Autor: | Dominique Borrione, E. Dumitrescu |
|---|---|
| Přispěvatelé: | Techniques de l'Informatique et de la Microélectronique pour l'Architecture des systèmes intégrés (TIMA), Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS), Techniques of Informatics and Microelectronics for integrated systems Architecture (TIMA), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA), Torella, Lucie |
| Jazyk: | angličtina |
| Rok vydání: | 2003 |
| Předmět: |
Model checking
Theoretical computer science Computer science [SPI.NANO] Engineering Sciences [physics]/Micro and nanotechnologies/Microelectronics Symbolic simulation simplifying-strategy 02 engineering and technology Abstraction model checking model-reduction-step 020202 computer hardware & architecture Reduction (complexity) model-checking-tool Industrial design PACS 85.42 Symbolic trajectory evaluation design-model-checking 0202 electrical engineering electronic engineering information engineering SoC-verification symbolic-simulation 020201 artificial intelligence & image processing System on a chip [SPI.NANO]Engineering Sciences [physics]/Micro and nanotechnologies/Microelectronics Formal verification |
| Zdroj: | Proceedings-3rd-IEEE-International-Workshop-on-System-on-Chip-for-Real-Time-Applications. Proceedings-3rd-IEEE-International-Workshop-on-System-on-Chip-for-Real-Time-Applications., 2003, Calgary, Alta., Canada. pp.378-83 IWSOC |
| Popis: | ISBN: 076951944X; The successful application of model-checking to industrial designs requires methods for reducing the complexity of the model. This paper presents an original strategy, for a well identified class of circuit behaviors; by running an appropriate symbolic simulation pattern before the actual proof of a temporal formula, an important FSM model simplification can be obtained. The actual model reduction step is formalized and illustrated. This method has been implemented within the CMU version of the SMV model checking tool and validated on a large industrial design. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|