ARM instruction evaluator: About
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.