FM8501 : a verified microprocessor
The 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 pe...
Gorde:
| Egile nagusia: | |
|---|---|
| Formatua: | Livre numérique |
| Hizkuntza: | Anglais |
| Argitaratua: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Saila: | Lecture notes in computer science. Lecture notes in artificial intelligence
795 |
| Gaiak: | |
| Sarrera elektronikoa: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Oharra: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • FM8501, a verified microprocessor, Warren A. Hunt, Jr, Berlin, Springer-Verlag, 1994, 1 vol. (VII-333 p.), Lecture notes in computer science, 0-387-57960-5 • FM8501: A Verified Microprocessor, Texte imprimé, 9783662195932 |
Aurkibidea:
- A 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.