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

fYear

2004

fDate

7-11 Sept. 2004

Firstpage

60

Lastpage

65

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Integrated Circuits and Systems Design, 2004. SBCCI 2004. 17th Symposium on

Print_ISBN

1-58113-947-0

Type

conf

DOI

10.1109/SBCCI.2004.240978

Filename

1360545