LEADER 03785nam  22006615  450 
001 996466242603316
005 20200630015608.0
010   $a3-540-48401-9
024 7 $a10.1007/3-540-57960-5
035   $a(CKB)1000000000234107
035   $a(DE-He213)978-3-540-48401-1
035   $a(PPN)155170090
035   $a(EXLCZ)991000000000234107
100   $a20121227d1994      u|             0
101 0 $aeng
135   $aurnn|008mamaa
181   $ctxt$2rdacontent
182   $cc$2rdamedia
183   $acr$2rdacarrier
200 10$aFM8501: A Verified Microprocessor$b[electronic resource] /$fby Warren A. Jr. Hunt
205   $a1st ed. 1994.
210  1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1994.
215   $a1 online resource (XIV, 342 p.) 
225 1 $aLecture Notes in Artificial Intelligence ;$v795
311   $a3-540-57960-5 
327   $aA hardware model -- Notation and bit vectors -- Numeric definitions and operations -- The verification approach -- FM8501: A conventional description -- Commonly used functions -- The ALU -- Instruction fields -- Update and accessor functions -- The FM8501 hardware interpreter -- FM8501: A formal specification -- Correctness of FM8501 -- Expansion of FM8501 -- Conclusions.
330   $aThe FM 8501 microprocessor was invented as a generic microprocessor somewhat similar to a PDP-11. The principal idea of the FM 8501 effort was to see if it was possible to express the user-level specification and the design implementation using a formal logic, the Boyer-Moore logic; this approach permitted a complete mechanically checked proof that the FM 8501 implementation fully implemented its specification. The implementation model for the FM 8501 was inadequate for industrial hardware design but the effort was an important step in the evolution to the design verification methodology now employed by the author. The original version of this monograph was submitted as a dissertation at the University of Texas at Austin under the advisorship of R. Boyer and J. Moore.
410  0$aLecture Notes in Artificial Intelligence ;$v795
606   $aArtificial intelligence
606   $aArchitecture, Computer
606   $aComputer engineering
606   $aLogic design
606   $aMathematical logic
606   $aArithmetic and logic units, Computer
606   $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000
606   $aComputer System Implementation$3https://scigraph.springernature.com/ontologies/product-market-codes/I13057
606   $aComputer Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I27000
606   $aLogic Design$3https://scigraph.springernature.com/ontologies/product-market-codes/I12050
606   $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048
606   $aArithmetic and Logic Structures$3https://scigraph.springernature.com/ontologies/product-market-codes/I12026
615  0$aArtificial intelligence.
615  0$aArchitecture, Computer.
615  0$aComputer engineering.
615  0$aLogic design.
615  0$aMathematical logic.
615  0$aArithmetic and logic units, Computer.
615 14$aArtificial Intelligence.
615 24$aComputer System Implementation.
615 24$aComputer Engineering.
615 24$aLogic Design.
615 24$aMathematical Logic and Formal Languages.
615 24$aArithmetic and Logic Structures.
676   $a006.3
700   $aHunt$b Warren A. Jr$4aut$4http://id.loc.gov/vocabulary/relators/aut$0714626
906   $aBOOK
912   $a996466242603316
996   $aFM8501$91381964
997   $aUNISA