| Presentation | 1999/1/11 Formal Verification of Hardwere Described in HDL Using Temporal Logic Tadashi Araragi, Hiroshi Sawada, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | In this paper, we introduce a method of formally verifying specifications on hardware directly from their descriptions in HDL (Hardware Description Language). The method is focused on SFL, the HDL of the hardware synthesis system PARTHENON. The essential part of the method is transformation of SFL descriptions to the Boolean formulas which represent the relation of state transition of the hardware. In this transformation, several devices are required to create the Boolean formula that behaves precisely in accordance with the semantics of SFL when it is applied to the standard backward model checking algorithm of temporal logic CTL. We discuss the problem in detail. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | formal verification / HDL / temporal logic / architecture synthesis / PARTHENON |
| Paper # | AI98-66 |
| Date of Issue |
| Conference Information | |
| Committee | AI |
|---|---|
| Conference Date | 1999/1/11(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 | Artificial Intelligence and Knowledge-Based Processing (AI) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Formal Verification of Hardwere Described in HDL Using Temporal Logic |
| Sub Title (in English) | |
| Keyword(1) | formal verification |
| Keyword(2) | HDL |
| Keyword(3) | temporal logic |
| Keyword(4) | architecture synthesis |
| Keyword(5) | PARTHENON |
| 1st Author's Name | Tadashi Araragi |
| 1st Author's Affiliation | NTT Communication Science Laboratories() |
| 2nd Author's Name | Hiroshi Sawada |
| 2nd Author's Affiliation | NTT Communication Science Laboratories |
| Date | 1999/1/11 |
| Paper # | AI98-66 |
| Volume (vol) | vol.98 |
| Number (no) | 498 |
| Page | pp.pp.- |
| #Pages | 8 |
| Date of Issue | |