Name | Date | Size | ||
---|---|---|---|---|
.. | 25-Jul-2019 | 6 | ||
arm_emitScript.sml | H A D | 25-Jul-2019 | 10.1 KiB | |
arm_evalLib.sig | H A D | 25-Jul-2019 | 1.6 KiB | |
arm_evalLib.sml | H A D | 25-Jul-2019 | 27.9 KiB | |
arm_evalScript.sml | H A D | 25-Jul-2019 | 57.7 KiB | |
arm_rulesLib.sig | H A D | 25-Jul-2019 | 371 | |
arm_rulesLib.sml | H A D | 25-Jul-2019 | 4.3 KiB | |
arm_rulesScript.sml | H A D | 25-Jul-2019 | 32.5 KiB | |
armLib.sig | H A D | 25-Jul-2019 | 426 | |
armLib.sml | H A D | 25-Jul-2019 | 2.8 KiB | |
armParser.grm | H A D | 25-Jul-2019 | 12.6 KiB | |
armParser.lex | H A D | 25-Jul-2019 | 9.3 KiB | |
armScript.sml | H A D | 25-Jul-2019 | 33.2 KiB | |
assemblerML.sig | H A D | 25-Jul-2019 | 1.1 KiB | |
assemblerML.sml | H A D | 25-Jul-2019 | 32.4 KiB | |
Data.sml | H A D | 25-Jul-2019 | 3.1 KiB | |
Holmakefile | H A D | 25-Jul-2019 | 1.2 KiB | |
instructionScript.sml | H A D | 25-Jul-2019 | 10.8 KiB | |
instructionSyntax.sig | H A D | 25-Jul-2019 | 468 | |
instructionSyntax.sml | H A D | 25-Jul-2019 | 31.3 KiB | |
mlton/ | H | 25-Jul-2019 | 7 | |
my_listScript.sml | H A D | 25-Jul-2019 | 6 KiB | |
README | H A D | 25-Jul-2019 | 661 | |
run_arm_evalScript.sml | H A D | 25-Jul-2019 | 4.5 KiB | |
systemScript.sml | H A D | 25-Jul-2019 | 28.6 KiB | |
updateScript.sml | H A D | 25-Jul-2019 | 8.5 KiB |
README
1A model of the ARM instructions set. 2 3The files are as follows: 4 5 * armScript.sml: A HOL specification of the ARM instruction set. 6 7 * instructionScript.sml: Datatype and encoding functions for ARM instructions. 8 9 * bsubstScript.sml: Substitution using a list. 10 11 * my_listScript.sml: A collection of list lemmas. 12 13 * arm_evalScript.sml: Theorems about the ARM model and instruction encoding. 14 15 * arm_rulesScript.sml: Derived rules. 16 17 * arm_evalLib: Functions for assembling ARM code and running the model. 18 19 * run_arm_evalLib.sml: Some examples of running the model. 20 21 * Data.sml, Lexer.lex, Parser.grm, instructionSyntax.sml: 22 A parser and disassembler. 23