Formal Methods in Computer-Aided Design: First International Conference, FMCAD '96, Palo Alto, CA, USA, November 6 - 8, 1996, ProceedingsSpringer Science & Business Media, 1996. gada 23. okt. - 470 lappuses 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. |
Saturs
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 | |
Citi izdevumi - Skatīt visu
Formal Methods in Computer-Aided Design: First International Conference ... Mandayam Srivas,Albert Camilleri Priekšskatījums nav pieejams - 2014 |
Bieži izmantoti vārdi un frāzes
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
Populāri fragmenti
434. lappuse - 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.