Title :
Formal verification of LTL formulas for SystemC designs
Author :
Grosse, Daniel ; Drechsler, Rolf
Author_Institution :
Inst. of Comput. Sci., Bremen Univ., Germany
Abstract :
To handle today´s complexity, modern circuits and systems have to be specified at a high level of abstraction. Recently, SystemC has been proposed as a language that allows a fast simulation on a high level of abstraction and an efficient realization on RTL. To guarantee the correct behavior of a design, a concise verification methodology has to be developed. We present the first formal verification approach for SystemC that allows to prove the correctness of properties specified in linear temporal logic (LTL). In contrast to simulation-based techniques, completeness can be ensured. Our proof engine is based on symbolic manipulation, and a case study of a scalable bus arbiter shows the efficiency of the approach.
Keywords :
circuit CAD; formal verification; logic CAD; reachability analysis; temporal logic; LTL reasoning; RTL realization; SystemC designs; SystemC language; concise verification methodology; fast simulation; formal verification; linear temporal logic reasoning; scalable bus arbiter; symbolic manipulation; Circuit simulation; Circuits and systems; Computational modeling; Computer science; Data structures; Engines; Formal verification; Hardware; Reachability analysis; Sequential circuits;
Conference_Titel :
Circuits and Systems, 2003. ISCAS '03. Proceedings of the 2003 International Symposium on
Print_ISBN :
0-7803-7761-3
DOI :
10.1109/ISCAS.2003.1206243
