システムレベル設計における同期検証フレームワークの提案(高位設計-1, システムオンシリコン設計技術並びにこれを活用した VLSI)

概要

論文の詳細を見る
This paper presents a formal verification framework targeting the synchronization problem in SpecC language, a C-based system-level design language that supports HW/SW design seamlessly. Based on the Counter-Example Guided Abstraction Refinement (CEGAR) paradigm, we can briefly describe our framework as follows. The SpecC descriptions are abstracted and translated into descriptions that contain only boolean variables, or so called "boolean SpecC". The boolean SpecC descriptions are translated into an equality/inequality formula. This formula is then checked using an Integer Linear Programming (ILP) solver. Once the results are satisfied, the verification process stops with the synchronization property holds. Otherwise, a counterexample is given. The process of counterexample analysis and abstraction refinement is also proposed in this paper.
社団法人電子情報通信学会の論文
2005-03-03