CheckSyC: an efficient property checker for RTL SystemC designs

Author

Große, Daniel ; Drechsler, Rolf

Author_Institution

Inst. of Comput. Sci., Bremen Univ., Germany

fYear

2005

fDate

23-26 May 2005

Firstpage

4167

Abstract

To cope with the increasing complexity of today´s circuits and systems, new design methodologies are needed. Modeling at higher levels of abstraction and hardware/software integration become more and more important. A language that offers this features is SystemC, a C++ class library. Besides efficient modeling, the correct functional behavior has to be ensured. We present a property checker, CheckSyC, for SystemC descriptions on the register transfer level (RTL). A SystemC design and a temporal property are converted into a satisfiability (SAT) problem. If the SAT problem is unsatisfiable, the property holds. To demonstrate the efficiency of CheckSyC, different designs are studied.

Keywords

C++ language; computability; electronic design automation; hardware-software codesign; modelling; software libraries; C++ class library; RTL SystemC designs; SystemC descriptions; hardware/software integration; property checker; register transfer level; satisfiability problem; Circuit simulation; Circuit synthesis; Circuits and systems; Computer science; Concurrent computing; Design methodology; Hardware design languages; Process design; Software libraries; Timing;

fLanguage

English

Publisher

ieee

Conference_Titel

Circuits and Systems, 2005. ISCAS 2005. IEEE International Symposium on

Print_ISBN

0-7803-8834-8

Type

conf

DOI

10.1109/ISCAS.2005.1465549

Filename

1465549