LEADER 05424nam 22007815 450 001 996465375003316 005 20200705101651.0 010 $a0-387-34801-8 024 7 $a10.1007/0-387-97226-9 035 $a(CKB)1000000000228163 035 $a(SSID)ssj0000323715 035 $a(PQKBManifestationID)11245080 035 $a(PQKBTitleCode)TC0000323715 035 $a(PQKBWorkID)10300461 035 $a(PQKB)10499317 035 $a(DE-He213)978-0-387-34801-8 035 $a(PPN)155226754 035 $a(EXLCZ)991000000000228163 100 $a20121227d1990 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aHardware Specification, Verification and Synthesis: Mathematical Aspects$b[electronic resource] $eMathematical Sciences Institute Workshop. Cornell University Ithaca, New York, USA. July 5-7, 1989. Proceedings /$fedited by Miriam Leeser, Geoffrey Brown 205 $a1st ed. 1990. 210 1$aNew York, NY :$cSpringer New York :$cImprint: Springer,$d1990. 215 $a1 online resource (VIII, 404 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v408 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a0-387-97226-9 327 $aDesign for verifiability -- Verification of synchronous circuits by symbolic logic simulation -- Constraints, abstraction, and verification -- Formalising the design of an SECD chip -- Reasoning about state machines in higher-order logic -- A mechanically derived systolic implementation of pyramid initialization -- Behavior-preserving transformations for high-level synthesis -- From programs to transistors: Verifying hardware synthesis tools -- Combining engineering vigor with mathematical rigor -- Totally verified systems: Linking verified software to verified hardware -- What's in a timing discipline? Considerations in the specification and synthesis of systems with interacting asynchronous and synchronous components -- Complete trace structures -- The design of a delay-insensitive microprocessor: An example of circuit synthesis by program transformation -- Manipulating logical organization with system factorizations -- The verification of a bit-slice ALU -- Verification of a pipelined microprocessor using clio -- Verification of combinational logic in Nuprl -- Veritas+: A specification language based on type theory -- Categories for the working hardware designer. 330 $aCurrent research into formal methods for hardware design is presented in the papers in this volume. Because of the complexity of VLSI circuits, assuring design validity before circuits are manufactured is imperative. The goal of research in this area is to develop methods of improving the design process and the quality of the resulting designs. The major trend apparent at the workshop is that researchers are rapidly moving away from post hoc proof techniques with their great expense. A number of papers were presented that dealt with problems of synthesizing correct circuits and of designing with the goal of verification. Researchers are also beginning to deal with the theoretical issues of reasoning about concurrent systems and asynchronous systems, and to introduce new logical tools such as constructive type theory and category theory. Most of the research reported was performed in the United States. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v408 606 $aArchitecture, Computer 606 $aMicroprogramming  606 $aArithmetic and logic units, Computer 606 $aLogic design 606 $aElectronics 606 $aMicroelectronics 606 $aComputers 606 $aComputer System Implementation$3https://scigraph.springernature.com/ontologies/product-market-codes/I13057 606 $aControl Structures and Microprogramming$3https://scigraph.springernature.com/ontologies/product-market-codes/I12018 606 $aArithmetic and Logic Structures$3https://scigraph.springernature.com/ontologies/product-market-codes/I12026 606 $aLogic Design$3https://scigraph.springernature.com/ontologies/product-market-codes/I12050 606 $aElectronics and Microelectronics, Instrumentation$3https://scigraph.springernature.com/ontologies/product-market-codes/T24027 606 $aComputation by Abstract Devices$3https://scigraph.springernature.com/ontologies/product-market-codes/I16013 615 0$aArchitecture, Computer. 615 0$aMicroprogramming . 615 0$aArithmetic and logic units, Computer. 615 0$aLogic design. 615 0$aElectronics. 615 0$aMicroelectronics. 615 0$aComputers. 615 14$aComputer System Implementation. 615 24$aControl Structures and Microprogramming. 615 24$aArithmetic and Logic Structures. 615 24$aLogic Design. 615 24$aElectronics and Microelectronics, Instrumentation. 615 24$aComputation by Abstract Devices. 676 $a621.39/5 702 $aLeeser$b Miriam$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aBrown$b Geoffrey$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 02$aCornell University.$bMathematical Sciences Institute. 906 $aBOOK 912 $a996465375003316 996 $aHardware Specification, Verification and Synthesis: Mathematical Aspects$92831342 997 $aUNISA