Formal Hardware Verification: Methods and Systems in ComparisonThomas Kropf Springer Science & Business Media, 27/08/1997 - 376 من الصفحات This state-of-the-art monograph presents a coherent survey of a variety of methods and systems for formal hardware verification. It emphasizes the presentation of approaches that have matured into tools and systems usable for the actual verification of nontrivial circuits. All in all, the book is a representative and well-structured survey on the success and future potential of formal methods in proving the correctness of circuits. The various chapters describe the respective approaches supplying theoretical foundations as well as taking into account the application viewpoint. By applying all methods and systems presented to the same set of IFIP WG10.5 hardware verification examples, a valuable and fair analysis of the strenghts and weaknesses of the various approaches is given. |
المحتوى
III | 3 |
VI | 5 |
VII | 6 |
VIII | 7 |
X | 8 |
XI | 9 |
XII | 10 |
XIII | 11 |
XCVI | 160 |
XCVIII | 162 |
C | 164 |
CII | 165 |
CIII | 168 |
CIV | 171 |
CV | 173 |
CVI | 174 |
XIV | 12 |
XV | 14 |
XVI | 21 |
XVIII | 22 |
XIX | 24 |
XXI | 25 |
XXII | 32 |
XXIII | 39 |
XXIV | 40 |
XXV | 41 |
XXVI | 42 |
XXVII | 44 |
XXVIII | 49 |
XXX | 54 |
XXXI | 58 |
XXXII | 62 |
XXXIII | 65 |
XXXIV | 66 |
XXXV | 68 |
XXXVI | 69 |
XXXVIII | 76 |
XXXIX | 79 |
XLI | 80 |
XLII | 81 |
XLIII | 83 |
XLIV | 84 |
XLVI | 87 |
XLVII | 93 |
XLVIII | 96 |
XLIX | 99 |
LI | 100 |
LII | 103 |
LIII | 104 |
LIV | 105 |
LV | 107 |
LVI | 109 |
LVII | 112 |
LVIII | 114 |
LIX | 115 |
LX | 116 |
LXII | 122 |
LXIII | 124 |
LXV | 125 |
LXVI | 127 |
LXVII | 128 |
LXVIII | 129 |
LXIX | 130 |
LXX | 131 |
LXXI | 132 |
LXXII | 133 |
LXXIII | 135 |
LXXIV | 136 |
LXXV | 137 |
LXXVI | 138 |
LXXVII | 140 |
LXXVIII | 142 |
LXXXI | 143 |
LXXXII | 145 |
LXXXIII | 146 |
LXXXV | 147 |
LXXXVI | 148 |
LXXXVIII | 151 |
LXXXIX | 153 |
XC | 154 |
XCI | 156 |
XCIII | 157 |
XCIV | 158 |
CVIII | 175 |
CIX | 176 |
CX | 177 |
CXI | 179 |
CXII | 183 |
CXIII | 189 |
CXIV | 190 |
CXV | 192 |
CXVI | 193 |
CXVII | 197 |
CXVIII | 200 |
CXX | 201 |
CXXI | 204 |
CXXIII | 205 |
CXXIV | 206 |
CXXVI | 209 |
CXXVII | 210 |
CXXVIII | 214 |
CXXIX | 219 |
CXXX | 222 |
CXXXI | 223 |
CXXXII | 228 |
CXXXIII | 230 |
CXXXIV | 234 |
CXXXV | 235 |
CXXXVI | 244 |
CXXXVIII | 245 |
CXL | 246 |
CXLII | 247 |
CXLIV | 248 |
CXLVI | 252 |
CXLVII | 254 |
CXLVIII | 255 |
CXLIX | 256 |
CL | 257 |
CLII | 261 |
CLIII | 262 |
CLIV | 265 |
CLV | 266 |
CLVI | 268 |
CLVII | 273 |
CLVIII | 274 |
CLIX | 275 |
CLX | 282 |
CLXI | 284 |
CLXII | 285 |
CLXIII | 286 |
CLXIV | 287 |
CLXV | 291 |
CLXVI | 297 |
CLXVII | 303 |
CLXVIII | 307 |
CLXIX | 310 |
CLXX | 312 |
CLXXI | 317 |
CLXXII | 328 |
CLXXIII | 330 |
CLXXVI | 331 |
CLXXIX | 332 |
CLXXXIII | 333 |
CLXXXIV | 334 |
CLXXXVI | 337 |
CLXXXVIII | 340 |
CLXXXIX | 341 |
CXC | 343 |
349 | |
طبعات أخرى - عرض جميع المقتطفات
عبارات ومصطلحات مألوفة
abstract data types adder algorithm approach arbiter array assertion automated automatically behavior benchmark bit-vector Black-Jack dealer boolean cardready cards cell circuit clock cycle combinational components computation concrete constraints controller correctness COSPAN data path decision procedures defined definition described design description design model disjunction E.M. Clarke equations example expressions Figure finite finite state machine formal formal verification full adder function symbols given Global hardware verification hitme implementation induction input invariant lemma machine microprocessor model checking module multiplier nodes opcode operations output predicate prefix formula processor proof properties protocol prove reachable recursive represented reset result rising edge ROBDD score Sect sequence signal simulation Single Pulser specification strategy symbolic simulation SYNCHRONIZED TRANSITIONS systolic array temporal logic theorem prover tion TL formulas trajectory evaluation transition relation tunnel variables vector VHDL
مقاطع مشهورة
الصفحة 2 - Department of Computer Science, University of British Columbia 2366 Main Mall, Vancouver, BC Canada V6T 1Z4 email: conati@cs . ubc.