Name
Title | ||
|---|---|---|
Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking |
Abstract | ||
|---|---|---|
This paper presents the formal verification of all sub-circuits in afloating-point arithmetic unit (FPU) from an Intel microprocessor using a wordlevelmodel checker. This work represents the first large-scale application ofword-level model checking techniques. The FPU can perform addition, subtraction,multiplication, square root, division, remainder, and rounding operations;verifying such a broad range of functionality required coupling the model checkerwith a number of other techniques,... |
Year | DOI | Venue |
|---|---|---|
1996 | 10.1007/BFb0031797 | FMCAD |
Keywords | Field | DocType |
word-level model checking,floating-point unit,floating point unit,model checking,formal verification,functional requirement | Single-precision floating-point format,Functional verification,Floating-point unit,Floating point,Computer science,Parallel computing,Arithmetic,Real-time computing,Runtime verification,Coprocessor,High-level verification,Extended precision | Conference |
Volume | ISSN | ISBN |
1166 | 0302-9743 | 3-540-61937-2 |
Citations | PageRank | References |
27 | 1.55 | 14 |
Authors | ||
8 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yirng-an Chen | 1 | 304 | 23.80 |
| Edmund M. Clarke | 2 | 20645 | 2418.32 |
| Pei-hsin Ho | 3 | 2577 | 305.29 |
| Yatin Vasant Hoskote | 4 | 54 | 5.39 |
| Timothy Kam | 5 | 109 | 6.33 |
| Manpreet Khaira | 6 | 27 | 1.55 |
| John W. O'Leary | 7 | 187 | 26.29 |
| Xudong Zhao | 8 | 361 | 69.26 |