|
 
|
[HMD11] Building SystemC Waiting State Automata
Conférence Internationale avec comité de lecture : On the Fifth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS), September 2011, pp.108-119 , Tunis, Tunisia,Mots clés: SystemC, automata, operational semantics, symbolic execution, compostional veriï¬cation
Résumé:
SystemC is becoming a de facto standard for the system-level description of system-on-chip. However most
formal veriï¬cation techniques used for verifying hardware components targets low level design, usually
netlist or RTL, but time-to-market requirements have rushed the industry towards design paradigms that
offer a very high level of abstraction. In previous works, we proposed a veriï¬cation methodology based
on SystemC waiting-state automata, an abstract formal model for verifying properties of SystemC at the
transaction level within a delta-cycle. The main drawback of this model is that it should be provided manually.
In this paper, we propose a method to automatically build the SystemC waiting-state automata from the
SystemC code. It is based on an extended symbolic execution of the SystemC design that takes care of
synchronous as well as asynchronous communications and that preserves the semantics of SystemC up to
a delta-cycle.
Equipe:
sys
BibTeX
| @inproceedings { | |||
| HMD11, | |||
| title | = | "{Building SystemC Waiting State Automata}", | |
| author | = | " N. Harrath and B. Monsuez and J. Delacroix ", | |
| booktitle | = | "{On the Fifth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS)}", | |
| year | = | 2011, | |
| month | = | "September", | |
| pages | = | "108-119 ", | |
| address | = | "Tunis, Tunisia", | |
| } | |||
