| Presentation | 1996/12/13 Formal Verification for Hardware Structure by Higher Order Predicate Logic Kazuya SUZUKI, Takeo YOSHIDA, Yukiya MIURA, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | We propose a method for verifying a correctness of hardware structure. Hardware including structural loops cannot be expressed by first order predicate logic which is used generally, because first order predicate logic cannot express functions recursively. This problem can be solved by using higher order predicate logic. In this method, two models that are formulas of higher order predicate logic are made from both specification description and design description. From these formulas, we make a correctness formulas which means that the design description satisfies with specification description. We show procedure for proving the correctness formulas using a theorem prover. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | higher order predicate logic / formal verification / behavioral description / structural description |
| Paper # | VLD96-70,CPSY96-82 |
| Date of Issue |
| Conference Information | |
| Committee | VLD |
|---|---|
| Conference Date | 1996/12/13(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) | Formal Verification for Hardware Structure by Higher Order Predicate Logic |
| Sub Title (in English) | |
| Keyword(1) | higher order predicate logic |
| Keyword(2) | formal verification |
| Keyword(3) | behavioral description |
| Keyword(4) | structural description |
| 1st Author's Name | Kazuya SUZUKI |
| 1st Author's Affiliation | Faculty of Engineering,Tokyo Metropolitan University() |
| 2nd Author's Name | Takeo YOSHIDA |
| 2nd Author's Affiliation | Faculty of Engineering,Tokyo Metropolitan University |
| 3rd Author's Name | Yukiya MIURA |
| 3rd Author's Affiliation | Faculty of Engineering,Tokyo Metropolitan University |
| Date | 1996/12/13 |
| Paper # | VLD96-70,CPSY96-82 |
| Volume (vol) | vol.96 |
| Number (no) | 425 |
| Page | pp.pp.- |
| #Pages | 8 |
| Date of Issue | |