ARM instruction evaluator: About

| Home | About | Learn more | Feedback |
This Common Gateway Interface (CGI) dynamic web site is generated by a compiled instance of the HOL4 interactive theorem prover. The evaluator tool provides an interface to our higher-order logic formalization of the ARM instruction set architecture. For each evaluation, a HOL4 theorem over the ARM model is derived, in real-time, using forward proof. This theorem describes the semantics of the instruction and it is used to produce the HTML description of the behaviour.

Although we have striven to make the model as accurate as possible, errors and misinterpretations may exist. The HOL4 model has not been certified or endorsed by ARM Ltd. Please feel free to use the feedback facility.

More information can be found here.