Formal Verification Techniques for SystemC

PhD Qualifying Examination


Title: "Formal Verification Techniques for SystemC"

Mr. Xiuqiang He


Abstract:

SystemC is an industry-standard C++ library for Electronic System-Level
design. It can be used to build higher-level abstraction models and
enable faster simulation than low-level hardware description languages
such as Verilog or VHDL. Verification of SystemC models is traditionally
based on time-consuming simulation. There are two main challenges to
effective verification of SystemC models. First, SystemC is inherently
concurrent, and interleaving among the parallel threads can cause state
space explosion in model-checking. Second, real-time can be explicitly
modeled in SystemC, and the verification of time-related property brings
new challenges, especially when combined with concurrency. There are many
differences as well as similarities between verification of concurrent
multithreaded software, i.e., Java, and verification of SystemC models.
Formal methods, such as model checking, SAT (Satisfiability Solving), SMT
(Satisfiability Modulo Theories), QBF (Quantified Boolean Formula), ILP
(Integer Linear Programming), have been widely used in both software and
hardware verification, and there have been some attempts at applying them
to verify SystemC models. In this report, I present a survey on recent
work on formal verification techniques for SystemC as well as concurrent
software.


Date:     		Wednesday, 16 April 2008

Time:                   3:30p.m.-5:30p.m.

Venue:                  Room 3402
			lifts 17-18

Committee Members:      Dr. Zonghua Gu (Supervisor)
			Dr. Shing-Chi Cheung (Chairperson)
			Dr. Jogesh Muppala
			Prof. Vincent Shen


**** ALL are Welcome ****