| Presentation | 2006-01-17 Boolean Equivalence Checking Using a Subset of First-Order Logic Atsushi MORITOMO, Kiyoharu HAMAGUCHI, Toshinobu KASHIWABARA, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | In recent years, design verification becomes more difficult as the scale of semiconductor circuits becomes larger. Designs are commonly checked by simulation-based verification, and exhaustive verification is difficult by simulation-based verification. As for equivalence checking, however, formal verification methods have been spreading. Formal equivalence checking at Boolean function level requires a large amount of cost. Therefore, formal verification based on first-order logic has been considered. Since validity checking of quantifier-free first-order logic with equality which is a subclass of first-order logic is decidable, the verification methods using this logic has been proposed. In this logic, however, arithmetic operations are abstracted away by functional symbols. The result of equivalence checking with this logic can differ from that of the conventional Boolean equivalence checking. This report shows an equivalence checking algorithm of the logic formula using Boolean substitution only for function/predicate symbols which cannot be checked by first-order logic. This algorithm achieves the accuracy of equivalence checking at Boolean level. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Equivalence Checking / Boolean Function / First-Order Logic |
| Paper # | VLD2005-96,CPSY2005-52,RECONF2005-85 |
| Date of Issue |
| Conference Information | |
| Committee | RECONF |
|---|---|
| Conference Date | 2006/1/10(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 | Reconfigurable Systems (RECONF) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Boolean Equivalence Checking Using a Subset of First-Order Logic |
| Sub Title (in English) | |
| Keyword(1) | Equivalence Checking |
| Keyword(2) | Boolean Function |
| Keyword(3) | First-Order Logic |
| 1st Author's Name | Atsushi MORITOMO |
| 1st Author's Affiliation | Dept. of Bioinformatic Engineering, Graduate School of Information Science and Technology, Osaka University() |
| 2nd Author's Name | Kiyoharu HAMAGUCHI |
| 2nd Author's Affiliation | Dept. of Bioinformatic Engineering, Graduate School of Information Science and Technology, Osaka University |
| 3rd Author's Name | Toshinobu KASHIWABARA |
| 3rd Author's Affiliation | Dept. of Bioinformatic Engineering, Graduate School of Information Science and Technology, Osaka University |
| Date | 2006-01-17 |
| Paper # | VLD2005-96,CPSY2005-52,RECONF2005-85 |
| Volume (vol) | vol.105 |
| Number (no) | 517 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |