Formal Methods in Computer-Aided Design: First International Conference, FMCAD '96, Palo Alto, CA, USA, November 6 - 8, 1996, ProceedingsSpringer Science & Business Media, 23/10/1996 - 470 من الصفحات This book constitutes the refereed proceedings of the First International Conference on Formal Methods in Computer-Aided Design, FMCAD '96, held in Palo Alto, California, USA, in November 1996. The 25 revised full papers presented were selected from a total of 65 submissions; also included are three invited survey papers and four tutorial contributions. The volume covers all relevant formal aspects of work in computer-aided systems design, including verification, synthesis, and testing. |
المحتوى
The Need for Formal Methods for Integrated Circuit Design | 1 |
Verification of All Circuits in a FloatingPoint Unit Using WordLevel Model Checking | 19 |
BMDs Can Delay the Use of Theorem Proving for Verifying Arithmetic Assembly Instructions | 34 |
Modular Verification of Multipliers | 49 |
Verification of IEEE Compliant Subtractive Division Algorithms | 64 |
A Case Study | 79 |
Experiments in Automating Hardware Verification Using Inductive Proof Planning | 94 |
Verifying Nondeterministic Implementations of Deterministic Systems | 109 |
Combining Specification Proof Checking and Model Checking | 257 |
A Tutorial Introduction | 265 |
A Tutorial on Digital Design Derivation Using DRS | 270 |
ACL2 Theorems About Commercial Microprocessors | 275 |
Formal Synthesis in Circuit Design A Classification and Survey | 294 |
Formal Specification and Verification of VHDL | 310 |
Specification of Control Flow Properties for Verification of Synthesized VHDL Designs | 327 |
An Algebraic Model of Correctness for Superscalar Microprocessors | 346 |
A Methodology for Processor Implementation Verification | 126 |
CoverageDirected Test Generation Using Symbolic Techniques | 143 |
SelfConsistency Checking | 159 |
A Methodology for Hardware Verification | 172 |
Validity Checking for Combinations of Theories with Equality | 187 |
A Unified Approach for Combining Different Formalisms for Hardware Verification | 202 |
Verification Using Uninterpreted Functions and Finite Instantiations | 218 |
Formal Verification of the Island Tunnel Controller Using Multiway Decision Graphs | 233 |
VIS | 248 |
Mechanically Checking a Lemma Used in an Automatic Verification Tool | 362 |
Automatic Generation of Invariants in Processor Verification | 377 |
A Brief Study of BDD Package Performance | 389 |
Local Encoding Transformations for Optimizing OBDDRepresentations of Finite State Machines | 404 |
Decomposition Techniques for Efficient ROBDD Construction | 419 |
for CTL Symbolic Model Checking of Petri Nets | 435 |
HDLBased Integration of Formal Methods and CAD Tools in the PREVAIL Environment | 450 |
| 469 | |
طبعات أخرى - عرض جميع المقتطفات
عبارات ومصطلحات مألوفة
ACL2 adder algorithm applied approach architecture arithmetic assertion automatically BDDs behavior binary binary decision diagrams bit-vector Boolean circuit complex Computer Science constraints correctness coverage data path decision diagrams decision procedures decomposition defined Design Automation Conference encoding equations equivalence example execution expressions Figure finite finite state machines floating point floating-point Formal Methods formal synthesis formal verification formula graph hardware verification HOL Light IEEE implementation induction input instruction integer interaction invariant iteration language latches lemmas logic loop machine memory methodology microprocessor model checking multiplier node Nqthm OBDD operands operations output packages Petri nets pipeline predicate processor proof planning properties proving reachable represent representation rewrite ROBDD Section self-consistency semantics sequence sequential signal simulation specification Srivas superscalar symbolic techniques theorem prover tion transformations transition relation uninterpreted functions variable order vector VHDL ZBDD
مقاطع مشهورة
الصفحة 434 - EM Sentovich, KJ Singh, L. Lavagno, C. Moon. R. Murgai, A. Saldanha, H. Savoj, PR Stephan. RK Brayton, and AL Sangiovanni-Vincentelli. SIS: A System for Sequential Circuit Synthesis.