| Presentation | 1997/10/29 An Efficient Formal Verification Method for the Circuit Specification with Several Modules Takashi TAKENAKA, Junji KITAMICHI, Seishi NISHIKAWA, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | In this paper, We propose a formal verification method for the sequential circuit specifications which consist of several modules. We use extended finite state machines (EFSMs) to model the circuits, and use context-free grammars as a formalism to describe the circuits. In this grammar, the circuit is described inductively in production rules. In our method, The circuits have two abstraction levels, requirement and implementation. In the production rules of the description of requirement specification (functional level), the functions which is added to the circuit is described. In the production rules of the description of the implementation specification (structural level), the modules which is added to the circuit is described. According to the production rules, it is proved by induction that the functional level circuit with the added functions is realized correctly by the structural level circuit with added modules. In our method, we put three restrictions on the grammars and the design process. 1) The same grammar is used to describe both requirement specification and implementation specification. 2) The production rules of the grammars make the circuits structure liner. 3) The designer gives the correspond relation between requirement specification and implementation specification. And we applied the proposed method for the bus system which connects n devices. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | formal verification / theorem proving / several modules / context-free network grammars / parameterized specification |
| Paper # | VLD97-87 |
| Date of Issue |
| Conference Information | |
| Committee | VLD |
|---|---|
| Conference Date | 1997/10/29(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 | VLSI Design Technologies (VLD) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | An Efficient Formal Verification Method for the Circuit Specification with Several Modules |
| Sub Title (in English) | |
| Keyword(1) | formal verification |
| Keyword(2) | theorem proving |
| Keyword(3) | several modules |
| Keyword(4) | context-free network grammars |
| Keyword(5) | parameterized specification |
| 1st Author's Name | Takashi TAKENAKA |
| 1st Author's Affiliation | Department of Informatics and Mathematical Sciences, Graduate School of Engineering Science, Osaka University() |
| 2nd Author's Name | Junji KITAMICHI |
| 2nd Author's Affiliation | Department of Informatics and Mathematical Sciences, Graduate School of Engineering Science, Osaka University |
| 3rd Author's Name | Seishi NISHIKAWA |
| 3rd Author's Affiliation | Department of Informatics and Mathematical Sciences, Graduate School of Engineering Science, Osaka University |
| Date | 1997/10/29 |
| Paper # | VLD97-87 |
| Volume (vol) | vol.97 |
| Number (no) | 344 |
| Page | pp.pp.- |
| #Pages | 8 |
| Date of Issue | |