LEADER 04623oam 2200661 450 001 996465910703316 005 20210803201641.0 010 $a3-540-49519-3 024 7 $a10.1007/3-540-49519-3 035 $a(CKB)1000000000211021 035 $a(SSID)ssj0000323227 035 $a(PQKBManifestationID)11247940 035 $a(PQKBTitleCode)TC0000323227 035 $a(PQKBWorkID)10296278 035 $a(PQKB)11493359 035 $a(DE-He213)978-3-540-49519-2 035 $a(MiAaPQ)EBC3073203 035 $a(MiAaPQ)EBC6495042 035 $a(PPN)155174320 035 $a(EXLCZ)991000000000211021 100 $a20210803d1998 uy 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 00$aFormal methods in computer-aided design $esecond international conference, FMCAD '98, Palo Alto, CA, USA, November 4-6, 1998 : proceedings /$fGanesh Gopalakrishnan, Phillip Windley (editors) 205 $a1st ed. 1998. 210 1$aBerlin :$cSpringer,$d[1998] 210 4$d©1998 215 $a1 online resource (X, 538 p.) 225 1 $aLecture notes in computer science ;$v1522 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-65191-8 320 $aIncludes bibliographical references and index. 327 $aMinimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification -- Reducing Manual Abstraction in Formal Verification of Out- of- Order Execution -- Bit-Level Abstraction in the Verification of Pipelined Microprocessors by Correspondence Checking -- Solving Bit-Vector Equations -- The Formal Design of 1M-Gate ASICs -- Design of Experiments for Evaluation of BDD Packages Using Controlled Circuit Mutations -- A Tutorial on Stålmarck?s Proof Procedure for Propositional Logic -- Almana: A BDD Minimization Tool Integrating Heuristic and RewritingMethods -- Bisimulation Minimization in an Automata-Theoretic Verification Framework -- Automatic Verification of Mixed-Level Logic Circuits -- A Timed Automaton-Based Method for Accurate Computation of Circuit Delay in the Presence of Cross-Talk -- Maximum Time Separation of Events in Cyclic Systems with Linear and Latest Timing Constraints -- Using MTBDDs for Composition and Model Checking of Real-Time Systems -- Formal Methods in CAD from an Industrial Perspective -- A Methodology for Automated Verification of Synthesized RTL Designs and Its Integration with a High-Level Synthesis Tool -- Combined Formal Post- and Presynthesis Verification in High Level Synthesis -- Formalization and Proof of a Solution to the PCI 2.1 Bus Transaction Ordering Problem -- A Performance Study of BDD-Based Model Checking -- Symbolic Model Checking Visualization -- Input Elimination and Abstraction in Model Checking -- Symbolic Simulation of the JEM1 Microprocessor -- Symbolic Simulation: An ACL2 Approach -- Verification of Data-Insensitive Circuits: An In-Order-Retirement Case Study -- Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification -- Formally Verifying Data and Control with Weak Reachability Invariants -- Generalized Reversible Rules -- An Assume-Guarantee Rule for Checking Simulation -- Three Approaches to Hardware Verification: HOL, MDG, and VIS Compared -- An Instruction Set Process Calculus -- Techniques for Implicit State Enumeration of EFSMs -- Model Checking on Product Structures -- BDDNOW: A Parallel BDD Package -- Model Checking VHDL with CV -- Alexandria: A Tool for Hierarchical Verification -- PV: An Explicit Enumeration Model-Checker. 410 0$aLecture notes in computer science ;$v1522. 606 $aDigital integrated circuits$xComputer-aided design$vCongresses 606 $aComputer engineering$xComputer-aided design$vCongresses 606 $aIntegrated circuits$xVerification$vCongresses 606 $aAutomatic theorem proving$vCongresses 606 $aFormal methods (Computer science)$vCongresses 615 0$aDigital integrated circuits$xComputer-aided design 615 0$aComputer engineering$xComputer-aided design 615 0$aIntegrated circuits$xVerification 615 0$aAutomatic theorem proving 615 0$aFormal methods (Computer science) 676 $a621.392 702 $aWindley$b Phillip J.$f1958- 702 $aGopalakrishnan$b Ganesh 712 12$aFMCAD '98 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bUtOrBLW 906 $aBOOK 912 $a996465910703316 996 $aFormal Methods in Computer-Aided Design$91891319 997 $aUNISA