Formal verification of LTL formulas for SystemC designs

To handle today’s complexity, modern circuits and systems be specified at a high level of abstraction. Recently, SystemC has been proposed as a language that allows a fast on 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 simulationbased 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.

• Type: Conference
• Year: 2003
• Where: ISCAS
• Authors: Daniel Große, Rolf Drechsler
• Keywords: Concise Verification Methodology, ISCAS 2003, SystemC, first Formal Verification