Title :
TheoSim: combining symbolic simulation and theorem proving for hardware verification
Author :
Sammane, G. AI ; Schmaltz, J. ; Toma, D. ; Ostier, P. ; Borrione, D.
Author_Institution :
TIMA Lab., VDS Group, Grenoble, France
Abstract :
TheoSim is a symbolic verification tool that fills the gap between the simulation of test cases, and the use of theorem provers, for the validation of initial specifications, and the exploration of the very first design steps of digital integrated systems. The principles of Theosim are presented, followed by its application to the verification of the first design step of a state-of-the-art network on chip architecture.
Keywords :
digital integrated circuits; digital systems; formal verification; hardware description languages; integrated circuit design; symbol manipulation; system-on-chip; theorem proving; TheoSim; digital integrated systems; hardware verification; network on chip architecture; symbolic simulation; symbolic verification tool; theorem proving; Artificial intelligence; Circuit simulation; Computational modeling; Digital systems; Hardware; Laboratories; Logic programming; Network-on-a-chip; Permission; System testing;
Conference_Titel :
Integrated Circuits and Systems Design, 2004. SBCCI 2004. 17th Symposium on
Print_ISBN :
1-58113-947-0
DOI :
10.1109/SBCCI.2004.240978