| Presentation | 1999/6/11 Improvements of Decision Algorithm for Presburger Arithmetic in High Level Verification of Logic Circuits Hiroyuki KAGEYAMA, Junji KITAMICHI, Teruo HIGASHINO, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | We have been studying the high level verification of logic circuits. In the verification at high level, we use Presburger arithmetic, which includes integer variables and some operators for them. We proposed a new data structure for Presburger arithmetic and implemented a library for them. In this paper, we propose some improvements on algorithms for our data structure. We refined our library and describe the restults of some experiments of formal design verification using our methods. Our data structure is like BDDs (Binary Decision Diagramas). Out improvements include the variable ordering for BDDs, the refinement of the operation for existential quantifier and so on. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | High Level Design / Formal Verification / Presburger Sentence / Binary Decision Diagrams |
| Paper # | VLD99-30 |
| Date of Issue |
| Conference Information | |
| Committee | VLD |
|---|---|
| Conference Date | 1999/6/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 | VLSI Design Technologies (VLD) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Improvements of Decision Algorithm for Presburger Arithmetic in High Level Verification of Logic Circuits |
| Sub Title (in English) | |
| Keyword(1) | High Level Design |
| Keyword(2) | Formal Verification |
| Keyword(3) | Presburger Sentence |
| Keyword(4) | Binary Decision Diagrams |
| 1st Author's Name | Hiroyuki KAGEYAMA |
| 1st Author's Affiliation | Graduate School of Engineering Science, Osaka University() |
| 2nd Author's Name | Junji KITAMICHI |
| 2nd Author's Affiliation | Education Center for Information Processing, Osaka University |
| 3rd Author's Name | Teruo HIGASHINO |
| 3rd Author's Affiliation | Graduate School of Engineering Science, Osaka University |
| Date | 1999/6/11 |
| Paper # | VLD99-30 |
| Volume (vol) | vol.99 |
| Number (no) | 108 |
| Page | pp.pp.- |
| #Pages | 8 |
| Date of Issue | |