| Presentation | 2005/3/3 A Framework on Synchronization Verification in System-Level Design Thanyapat SAKUNKONCHAK, Satoshi KOMATSU, Masahiro FUJITA, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | 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. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | formal verification / model checking / predicate abstraction / abstraction refinement / synchronization verification |
| Paper # | VLD2004-136,ICD2004-232 |
| Date of Issue |
| Conference Information | |
| Committee | ICD |
|---|---|
| Conference Date | 2005/3/3(1days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | |
| Vice Chair | |
| Secretary | |
| Assistant | |
| Paper Information | |
| Registration To | Integrated Circuits and Devices (ICD) |
|---|---|
| Language | ENG |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | A Framework on Synchronization Verification in System-Level Design |
| Sub Title (in English) | |
| Keyword(1) | formal verification |
| Keyword(2) | model checking |
| Keyword(3) | predicate abstraction |
| Keyword(4) | abstraction refinement |
| Keyword(5) | synchronization verification |
| 1st Author's Name | Thanyapat SAKUNKONCHAK |
| 1st Author's Affiliation | () |
| 2nd Author's Name | Satoshi KOMATSU |
| 2nd Author's Affiliation | |
| 3rd Author's Name | Masahiro FUJITA |
| 3rd Author's Affiliation | |
| Date | 2005/3/3 |
| Paper # | VLD2004-136,ICD2004-232 |
| Volume (vol) | vol.104 |
| Number (no) | 710 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |