NameDateSize

..25-Jul-20196

armLib.sigH A D25-Jul-2019503

armLib.smlH A D25-Jul-20193.4 KiB

armScript.smlH A D25-Jul-201930.5 KiB

coreScript.smlH A D25-Jul-201941 KiB

correctness/H25-Jul-201911

io_onestepScript.smlH A D25-Jul-201963.6 KiB

lemmasScript.smlH A D25-Jul-201921.8 KiB

my_listScript.smlH A D25-Jul-20195.3 KiB

onestepScript.smlH A D25-Jul-201921.4 KiB

READMEH A D25-Jul-2019608

README

1This example contains a correctness proof for the ARM6 microprocessor design.
2
3The files are as follows:  
4
5 * armScript.sml: A HOL specification of the ARM instruction set (v4).
6
7 * coreScript.sml: A HOL specification of the ARM6 micro-architecture.
8    This is based on Daniel Schostak's specification (Leeds). 
9
10 * onestepScript.sml and io_onestepScript.sml: A framework for carrying out
11    processor verifications.
12
13 * lemmasScript.sml: Some basic theorems about the ARM models.
14
15 * armLib: Some simple tactics and simpsets.
16
17 * correctness/: contains a proof of correctness (be patient when running!).
18