LEADER 05724nam 22007575 450 001 996465594903316 005 20200705005237.0 010 $a3-540-49567-3 024 7 $a10.1007/BFb0031795 035 $a(CKB)1000000000234555 035 $a(SSID)ssj0000323226 035 $a(PQKBManifestationID)11937900 035 $a(PQKBTitleCode)TC0000323226 035 $a(PQKBWorkID)10296780 035 $a(PQKB)10311063 035 $a(DE-He213)978-3-540-49567-3 035 $a(PPN)155188062 035 $a(EXLCZ)991000000000234555 100 $a20121227d1996 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aFormal Methods in Computer-Aided Design$b[electronic resource] $eFirst International Conference, FMCAD '96, Palo Alto, CA, USA, November 6 - 8, 1996, Proceedings /$fedited by Mandayam Srivas, Albert Camilleri 205 $a1st ed. 1996. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1996. 215 $a1 online resource (X, 478 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v1166 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-61937-2 327 $aThe need for formal methods for integrated circuit design -- Verification of all circuits in a floating-point unit using word-level model checking -- *BMDs can delay the use of theorem proving for verifying arithmetic assembly instructions -- Modular verification of multipliers -- Verification of IEEE compliant subtractive division algorithms -- Hierarchical verification of two-dimensional high-speed multiplication in PVS: A case study -- Experiments in automating hardware verification using inductive proof planning -- Verifying nondeterministic implementations of deterministic systems -- A methodology for processor implementation verification -- Coverage-directed test generation using symbolic techniques -- Self-consistency checking -- Inverting the abstraction mapping: A methodology for hardware verification -- Validity checking for combinations of theories with equality -- A unified approach for combining different formalisms for hardware verification -- Verification using uninterpreted functions and finite instantiations -- Formal verification of the Island Tunnel Controller using Multiway Decision Graphs -- VIS -- PVS: Combining specification, proof checking, and model checking -- HOL Light: A tutorial introduction -- A tutorial on digital design derivation using DRS -- ACL2 theorems about commercial microprocessors -- Formal synthesis in circuit design ? A classification and survey -- Formal specification and verification of VHDL -- Specification of control flow properties for verification of synthesized VHDL designs -- An algebraic model of correctness for superscalar microprocessors -- Mechanically checking a lemma used in an automatic verification tool -- Automatic generation of invariants in processor verification -- A brief study of BDD package performance -- Local encoding transformations for optimizing OBDD-representations of finite state machines -- Decomposition techniques for efficient ROBDD construction -- BDDs vs. Zero-Suppressed BDDs: for CTL symbolic model checking of Petri nets -- HDL-based integration of formal methods and CAD tools in the PREVAIL environment. 330 $aThis 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. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v1166 606 $aComputer-aided engineering 606 $aComputers 606 $aComputer engineering 606 $aComputer hardware 606 $aComputer logic 606 $aMathematical logic 606 $aComputer-Aided Engineering (CAD, CAE) and Design$3https://scigraph.springernature.com/ontologies/product-market-codes/I23044 606 $aTheory of Computation$3https://scigraph.springernature.com/ontologies/product-market-codes/I16005 606 $aComputer Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I27000 606 $aComputer Hardware$3https://scigraph.springernature.com/ontologies/product-market-codes/I1200X 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 615 0$aComputer-aided engineering. 615 0$aComputers. 615 0$aComputer engineering. 615 0$aComputer hardware. 615 0$aComputer logic. 615 0$aMathematical logic. 615 14$aComputer-Aided Engineering (CAD, CAE) and Design. 615 24$aTheory of Computation. 615 24$aComputer Engineering. 615 24$aComputer Hardware. 615 24$aLogics and Meanings of Programs. 615 24$aMathematical Logic and Formal Languages. 676 $a621.39/2 702 $aSrivas$b Mandayam$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aCamilleri$b Albert$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aFMCAD '96 906 $aBOOK 912 $a996465594903316 996 $aFormal Methods in Computer-Aided Design$91891319 997 $aUNISA