Verification of Synchronization in SpecC Description with the Use of Difference Decision Diagrams
Thanyapat Sakunkonchak, Masahiro Fujita · Kluwer Academic Publishers eBooks · 2006
SpecC language is designated to handle the design of entire system from specification to implementation and of hardware/software co-design. In this paper, we introduce an on-going work, which helps verifying the synchronization of events in SpecC. The original SpecC code containing synchronization semantics is parsed and translated into a Boolean SpecC code. The difference decision diagrams (DDDs) is used to verify for event synchronization on boolean SpecC code. The counter example for tracing back to the original source should be given when the verification result turns out to be unsatisfied. Here we introduce our overall idea and preset some preliminary results.