#|
Copyright (C) 1994 by Yuan Yu.  All Rights Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Yuan Yu PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS PROVIDED "AS IS"
WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING, BUT NOT
LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU ASSUME THE COST OF
ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
IN NO EVENT WILL Yuan Yu BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST PROFITS,
LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT
OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT NOT LIMITED TO LOSS
OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY THIRD
PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH DAMAGES, OR
FOR ANY CLAIM BY ANY OTHER PARTY.
|#

A Formal Specification of Some User Mode Instructions for the

Motorola 68020

Robert S. Boyer and Yuan Yu

Technical Report Computer Sciences Department University of Texas at Austin

Austin, Texas 78712

December, 1992

Contents

1 Introduction 1 2 A Few Basic Functions 2 3 Start Up 3 4 Some Constants 3 5 Bit Vector Arithmetic 6 6 Integer Arithmetic 9 7 Binary Trees for Memory 12 8 Operands from Memory 16 9 Storing the Result 19 10 Retrieving the Operand According to Oplen 22 11 Effective Address Calculation 23 12 The Individual Instructions 33 13 Stepi and Stepn 102 14 Auxiliary Functions 102 15 An Example of Simulation 104 16 Acknowledgements 106 17 Syntax Summary 107 Index 110

A Formal Specification of Some User Mode Instructions for the Motorola 68020^{1}

Robert S. Boyer and Yuan Yu

Computer Sciences and Mathematics Departments University of Texas at Austin Austin, Texas 78712

December, 1992

telephone: (512) 471-9745 email: boyer@cs.utexas.edu or yuan@cs.utexas.edu

Technical Report TR-92-04 (rev. 2.3 - dissertation version)

Abstract. We present a formal specification of approximately 80% of the ‘user mode’ instructions of the Motorola MC68020 microprocessor. The specification is given in the form of definitions in the logic of Nqthm, the Boyer-Moore system. The definitions are displayed in a conventional mathematical syntax. The specification has been used in the mechanical verification of several dozen machine code programs, whose binary was generated by ‘industrial strength’ C and Ada compilers.

1 Introduction

This report contains a formal specification of approximately 80% of the ‘user mode’ instructions of the Motorola MC68020 microprocessor. An earlier report [3] describes how we have used this specification to prove mechanically the correctness of several dozen machine code programs, most of them generated by ‘industrial strength’ compilers for C or Ada. Our specification is based upon the user’s manual for the MC68020 [4].

The function definitions below are ordered so that a function is defined before it is referenced by another function. One of the very last functions defined, ‘stepn’, p. 102, emulates the MC68020. Like all the functions in this specification, ‘stepn’ is a recursive and hence computable function. Approximately speaking, if we are given an MC68020 state s and a positive integer n, we can compute the state s’ that results from executing an MC68020 for n instructions, starting in state s, by applying ‘stepn’ to s and n. If an illegal instruction or an instruction not among those covered in this specification is encountered during execution, then s’ will exhibit an indication of the error. If no such error indication is exhibited, then the returned state correctly represents the state that a ‘real’ MC68020 would have after running n instructions provided that (i) the caches are initially consistent with memory, (ii) no interrupts happen during execution, and, of course, (iii) no externally caused changes to the state occur during execution. In Section 15 is a theorem that illustrates the use of ‘stepn’ to emulate an MC68020 on a specific state, one that contains machine code for Euclid’s GCD algorithm.

1The work described here was supported in part by NSF Grant MIP-9017499.

Disclaimer: The development of this formal specification is part of a small scientific project aimed at examining the feasibility of mechanically checking the correctness of machine code programs that run on widely-used microprocessors. The accuracy with which the specification presented here represents a ‘real’ MC68020 is something we do not know how to ascertain with the certainty of a mathematical proof. One can only become increasingly confident by such activities as critical reading, testing, and bug fixing. It is in a spirit of scientific cooperation that we distribute this specification, but we distribute it without any warranty of any kind, on an ‘as is’ basis.

The definitions below were written in the logic described in A Computational Logic Handbook, [2], with syntactic extensions for ‘let’ and ‘cond’. The definitions have been admitted under the definitional principle described in that book, using the mechanical theorem prover also described in that book. Although the logic and prover use the prefix, parenthesized notation of Church’s lambda calculus and McCarthy’s Lisp, in this report, we use a notation that is conventional. This new syntax is summarized in Section 17.

Our principal purpose in writing this technical report is to communicate precisely the formal, mathematical definitions of our specification of the MC68020. This report is decidedly not a tutorial on the MC68020 or on our specification of it. The reader will find it easier to read this specification after having read [3]. The reader will also find it invaluable to have a copy of [4] handy. Readers in search of a less stark introduction to this specification will find it in the Ph. D. dissertation of Yuan Yu. There also will be found a review of the related scientific literature.

2 A Few Basic Functions

The objects we use in this specification are truth values, integers, ordered pairs, and symbols. The precise axioms and notations for these objects and the builtin functions that operate on these objects may be found in [2]. Here are a few brief remarks about some of these objects and functions.

• The constant ‘true’, abbreviated t, is the true truth value.

• The constant ‘false’, abbreviated f, is the false truth value.

• ‘if’ is a function of three arguments. if x then y else z endif returns z if x is equal to f, and y otherwise.

• ‘cons’ is a function of two arguments. cons (x, y) returns an ordered pair whose first component is x and whose second is y.

• ‘car’ is a function of one argument. car (x) returns the first component if x is an ordered pair; otherwise, it returns 0.

• ‘cdr’ is a function of one argument. cdr (x) returns the second component if x is an ordered pair; otherwise, it returns 0.

• ‘list’ is a function of any number of arguments. list (x, y, z) is cons (x, cons (y, cons (z, nil))). nil is a symbol, and is used to denote the empty list.

Except for nil, symbols are printed in a typewriter font, preceded by a single

quotation mark, e.g., 'running and 'read unavailable memory.

3 Start Up

Event: Start with the library "mc20-0" using the compiled version.

Our initial library mc20-0 contains (i) the basic axioms and definitions of Nqthm, which are described in Chapter 4 of [2], (ii) some proved arithmetic lemmas that are used to help in the admission of the following definitions, and (iii) a definition of the nonnegative integer exponentiation function ‘exp’, which is defined as: exp (x, y) = if y ≃ 0 then 1 else x ∗ exp (x, y − 1) endif.

4 Some Constants

We first define a few constants.

In the MC68020, a “byte” is 8 bits long. A “word” is 16 bits long. A “long word” is 32 bits long. A “quad word” is 64 bits long.

Definition: b = 8

Definition: w = 16

Definition: l = 32 Definition: q = 64 Definition: bsz = 1 Definition: wsz = 2 Definition: lsz = 4 Definition: qsz = 8

Some error signals. Definition: read-signal = 'read unavailable memory

Definition: write-signal = 'write rom or unavailable memory

Definition:

reserved-signal = 'motorola reserved for future development

Definition: pc-signal = 'pc outside rom Definition: pc-odd-signal = 'pc at odd address Definition: mode-signal

= 'illegal addressing mode in current instruction

Throughout our specification, we have frequent need to refer to bits and bitvectors. In our model, bit ::= 0 | 1, and bit-vectors ::= nonnegative integers. If the operation is signed, we use the two conversion functions ‘nat-to-int’ and ‘int-to-nat’.

‘bitp’ is a function of one argument, x. ‘bitp’ returns t or f according to whether x is a bit or not. Definition: bitp (x) = ((x = 0) ∨ (x = 1))

We frequently use the bits 0 and 1. For clarity, to identify informally when we are using these integers as bits, we use the two constants ‘b1’ and ‘b0’. Definition: b1 = 1 Definition: b0 = 0

We frequently test a bit to see whether it is 0 or 1. We define the functions ‘b1p’ and ‘b0p’ to return t or f according to whether their arguments are 0 or non-0 respectively. Definition: b0p (x) = (x = b0)

Definition: b1p (x) = (x ≠ b0)

Definition: fix-bit (c) = if b0p (c) then b0

else b1 endif

Here are the definitions of some operators for logical arithmetic on bits. ‘b-not’ returns the complement of its argument.

Definition: b-not (x) = if b0p (x) then b1

else b0 endif

‘b-and’ returns the logical and of its two arguments.

Definition: b-and (x, y) = if b0p (x) then b0

elseif b0p (y) then b0 else b1 endif

‘b-or’ returns the logical or of its two arguments.

Definition: b-or (x, y) = if b0p (x)

then if b0p (y) then b0 else b1 endif

else b1 endif

‘b-nor’ returns the logical nor of its two arguments.

Definition: b-nor (x, y) = if b0p (x)

then if b0p (y) then b1 else b0 endif

else b0 endif

‘b-nand’ returns the logical nand of its two arguments.

Definition: b-nand (x, y) = if b0p (x) then b1

elseif b0p (y) then b1 else b0 endif

‘b-eor’ returns the exclusive or of its two arguments.

Definition: b-eor (x, y) = if b0p (x)

then if b0p (y) then b0 else b1 endif elseif b0p (y) then b1 else b0 endif

‘b-equal’ returns the logical equal of its two arguments.

Definition: b-equal (x, y) = if b0p (x) then b0p (y)

else b1p (y) endif

5 Bit Vector Arithmetic

‘bcar’ returns the first bit of x.

Definition: bcar (x) = (x mod 2)

‘bcdr’ returns a natural number by cutting off the first bit of x. For any natural number x, (bcar (x) + (x ∗ bcdr (x))) = x.

Definition: bcdr (x) = (x ÷ 2)

‘head’ is a function of two arguments, x and n. x and n should be nonnegative integers. ‘head’ returns the remainder of x divided by 2^{n}.

Definition: head (x, n) = (x mod exp (2, n))

‘tail’ is a function of two arguments, x and n. x and n should be nonnegative integers. ‘tail’ returns the quotient of x divided by 2^{n}.

Definition: tail (x, n) = (x ÷ exp (2, n))

We next define some logical operations on bit-vectors. ‘lognot’ takes two naturals as its arguments and returns the logical complement of its second argument.

Definition: lognot (n, x) = ((exp (2, n) − head (x, n)) − 1)

‘logand’ takes two naturals as arguments and returns their logical and.

Definition: logand (x, y) = if (x ≃ 0) ∨ (y ≃ 0) then 0

else b-and (bcar (x), bcar (y))

+ (2 ∗ logand (bcdr (x), bcdr (y))) endif

‘logor’ takes two naturals as arguments and returns the logical (inclusive) or of the two arguments.

Definition: logor (x, y) = if x ≃ 0 then fix (y)

elseif y ≃ 0 then fix (x)

else b-or (bcar (x), bcar (y)) + (2 ∗ logor (bcdr (x), bcdr (y))) endif

‘logeor’ takes two naturals as arguments and returns the logical exclusive or of the two arguments.

Definition: logeor (x, y) = if (x ≃ 0) ∧ (y ≃ 0) then 0

else b-eor (bcar (x), bcar (y))

+ (2 ∗ logeor (bcdr (x), bcdr (y))) endif

‘bitn’ retrieves the nth bit of x. Indexing is 0-based.

Definition: bitn (x, n) = bcar (tail (x, n))

‘mbit’ returns the most significant bit of x, assuming that x is a bit vector of n bits.

Definition: mbit (x, n) = bitn (x, n − 1)

‘bits’ returns bits i through j as a natural number. ‘bits’ is a function of three arguments, x, i, and j . x, i, and j should be natural numbers. Intuitively, bits extracts bits of x from bit i to bit j . Normally, i should be less than or equal to j .

Definition: bits (x, i, j ) = head (tail (x, i), 1 + (j − i))

‘setn’ updates the n^{th} bit of x by the given value c. Indexing is 0-based.

Definition: setn (x, n, c) = if n ≃ 0 then fix-bit (c) + (2 ∗ bcdr (x))

else bcar (x) + (2 ∗ setn (bcdr (x), n − 1, c)) endif

‘adder’ takes four arguments and returns the addition of x, y, and c modulo 2^{n}. That is, (x + y + c) mod exp (n, 2). Typically, c is either 0 or 1.

Definition: adder (n, c, x, y) = head (c + x + y, n)

‘add’ takes three arguments and returns the addition of x and y modulo 2^{n}. That is, (x + y) mod exp (n, 2).

Definition: add (n, x, y) = head (x + y, n)

‘subtracter’ takes four arguments and returns the subtraction of y and (x + c) mod exp (n, 2). That is, (y − (x + c)) mod exp (n, 2). Typically, c is either 0 or 1.

Definition: subtracter (n, c, x, y) = adder (n, b-not (c), y, lognot (n, x))

‘sub’ takes three arguments and returns, in the form of 2’s complement, the subtraction of y and x. That is, (y − x) mod exp (n, 2).

Definition: sub (n, x, y) = head (y + (exp (2, n) − head (x, n)), n)

‘app’ “appends” two naturals. ‘app’ takes three arguments, n, x, and y.

Definition: app (n, x, y) = (head (x, n) + (y ∗ exp (2, n)))

‘replace’ replaces x partially by y in the head. ‘replace’ is a function of three arguments, n, x and y, all of which should be naturals. ‘replace’ is frequently used when updating only one byte or one word in a register, leaving the other bytes alone.

Definition: replace (n, x, y) = app (n, x, tail (y, n))

‘ext’ is a function of three arguments, n, x and size. ‘ext’ is used frequently to do “sign-extension”. For instance, in the MC68020, we often extract a byte or word and wish to add it into a 32-bit sum, but we first sign-extend the extracted quantity to obtain a meaningful sum.

Definition: ext (n, x, size) = if n < size

then if b0p (bitn (x, n − 1)) then head (x, n)

else app (n, x, exp (2, size − n) − 1) endif else head (x, size) endif

Shift operations.

Logical shift left.

Definition: lsl (len, x, cnt) = head (x ∗ exp (2, cnt), len)

Arithmetic shift left.

Definition: asl (len, x, cnt) = head (x ∗ exp (2, cnt), len)

Logical shift right.

Definition: lsr (x, cnt) = tail (x, cnt)

Arithmetic shift right.

Definition: asr (n, x, cnt) = if x < exp (2, n − 1) then tail (x, cnt)

elseif n < cnt then exp (2, n) − 1

else app (n − cnt, tail (x, cnt), exp (2, cnt) − 1) endif

6 Integer Arithmetic

Throughout most of this MC68020 specification, we restrict our attention to arithmetic on the nonnegative integers. However, in the definition of two machine instructions, those for signed multiplication and division, we also consider all of the integers, both nonnegative and negative. The Nqthm logic adds the negative integers almost as an afterthought, and the basic, built-in arithmetic operations of the Nqthm logic work only for nonnegative integers. To do arithmetic on all the integers, we must define appropriate operations explicitly, as we do below.

The Nqthm logic has the peculiarity that − 0 is not the same as 0 . However, we will restrict our domain so that − 0 is not considered. A negative integer is defined to be of the form − x with x nonzero.

Definition: negp (i) = (negativep (i) ∧ (i ≠ (− 0)))

x is an integer iff x is either a nonnegative number or a negative number.

Definition: integerp (x) = ((x ∈ N) ∨ negp (x))

Definition: fix-int (x) = if integerp (x) then x

else 0 endif

Definition: izerop (x) = (fix-int (x) = 0)

Definition: abs (x) = if negp (x) then negative-guts (x)

else fix (x) endif Definition: ilessp (i, j ) = if negp (i)

then if negp (j ) then negative-guts (j ) < negative-guts (i)

else t endif elseif negp (j ) then f else i < j endif

Definition: ileq (i, j ) = (¬ ilessp (j , i))

Definition: iplus (x, y) = if negp (x)

then if negp (y) then − (negative-guts (x) + negative-guts (y)) elseif y < negative-guts (x) then − (negative-guts (x) − y) else y − negative-guts (x) endif

elseif negp (y)

then if x < negative-guts (y) then − (negative-guts (y) − x)

else x − negative-guts (y) endif else x + y endif

Definition: ineg (x) = if izerop (x) then 0

elseif negp (x) then negative-guts (x)

else − x endif

Definition: idifference (x, y) = iplus (x, ineg (y))

Definition: itimes (x, y) = if negp (x)

then if negp (y) then negative-guts (x) ∗ negative-guts (y) else fix-int (− (negative-guts (x) ∗ y)) endif elseif negp (y) then fix-int (− (x ∗ negative-guts (y))) else x ∗ y endif

Definition: iremainder (x, y) = if negp (x) then fix-int (− (negative-guts (x) mod abs (y)))

else x mod abs (y) endif

Definition: iquotient (x, y) = if negp (x) then if negp (y) then negative-guts (x) ÷ negative-guts (y) else fix-int (− (negative-guts (x) ÷ y)) endif elseif negp (y) then fix-int (− (x ÷ negative-guts (y))) else x ÷ y endif

The size of bit vectors. ‘nat-rangep’ returns t, if nat < exp (n, 2), but returns f, otherwise.

Definition: nat-rangep (nat, n) = (nat < exp (2, n))

The size of an unsigned integer. ‘uint-rangep’ returns t, if 0 ≤ x ≤ exp (n, 2), and returns f, otherwise.

Definition: uint-rangep (x, n) = (x < exp (2, n))

Two conversion functions for unsigned integer interpretation.

Definition: nat-to-uint (x) = fix (x)

Definition: uint-to-nat (x) = fix (x)

The size of an integer. ‘int-rangep’ returns t, if ((− exp (2, n − 1)) ≤ int) ∧ (int < exp (2, n − 1)), and returns f, otherwise.

Definition: int-rangep (int, n) = if n ≃ 0 then fix-int (int) = 0

elseif negativep (int) then negative-guts (int) ≤ exp (2, n − 1)

else int < exp (2, n − 1) endif

Two conversion functions for signed integer interpretation. ‘nat-to-int’ converts natural numbers to integers, ‘int-to-nat’ converts integers to natural numbers.

Definition: nat-to-int (x, n) = if x < exp (2, n − 1) then fix (x)

else − (exp (2, n) − x) endif

Definition: int-to-nat (x, size) = if negativep (x) then exp (2, size) − negative-guts (x)

else fix (x) endif

7 Binary Trees for Memory

A binary tree is either nil or an object of the form (value bt0 . bt1 ), where bt0 and bt1 are binary trees and value is any object stored at that node.

‘value-field’ is a function of one argument. ‘value-field’ returns the object stored at the current node, i.e., the ‘car’.

Definition: value-field (bt) = if listp (bt) then car (bt)

else 0 endif

‘branch0’ is a function of one argument, which should be a non-nil binary tree. ‘branch0’ returns the left branch, i.e., the ‘cadr’.

Definition: branch0 (bt) = if listp (bt) then cadr (bt)

else nil endif

‘branch1’ is a function of one argument, which should be a non-nil bin-tree. ‘branch1’ returns the right branch, i.e., the ‘cddr’.

Definition: branch1 (bt) = if listp (bt) ∧ listp (cdr (bt)) then cddr (bt)

else nil endif

Construct a binary tree (value br0 . br1 ).

Definition: make-bt (value, br0 , br1 ) = cons (value, cons (br0 , br1 ))

In order to execute MC68020 instructions reasonably efficiently in an applicative programming language, we implement memory using binary trees rather than simple linear lists or association lists. Binary trees give us logarithmic access and change times.

A memory state in this specification is actually given by a ‘cons’ of two binary trees, one that tells us ‘protection’ information about each byte of the memory and one that is the ‘physical’ memory, i.e., the byte of data stored at each 32-bit address.

A completely ‘full’ binary tree would contain 2^{32} tips, and the explicit representation of such a tree would vastly exceed the memory capacity of any known implementation of Nqthm. Therefore, we assign meaning to non-full, i.e., partially full, binary trees, both for protection and for data.

To characterize, informally, the content and protection of an address in memory, let us momentarily view an address as a sequence of 32 bits, most significant bit on the left. By an ‘initial sequence’ of an address x, we mean a sequence to which one can append another possibly empty sequence on the right to obtain x. Thus 001 is an initial sequence of 0010011. For a given memory data tree bt and address x, what is the content of bt at x? Answer: if the subtree of bt obtained by taking the path through bt determined by any initial sequence of x is nil, then the content of bt at x is 0. Otherwise, the content is the value field at the subtree of bt determined by x. In other words, if bt is not sufficiently deep along the path x, then the content of bt at x is 0.

A memory protection tree map is a binary tree which has stored at each node, in the value cell, either nil, '(unavailable), '(rom), or '(unavailable rom). (The last of these has the same meaning as '(unavailable).) For a given memory protection tree map and address x, what is the protection status of map at x? Answer: if 'unavailable is a member of the value cell at any subtree of map obtained by taking the path through map determined by any initial subsequence of x, then the address x is said to be unavailable, and it may not be read or written (even as part of a word or long word operation) by any instruction. Moreover, if an address x is not unavailable by the preceding rule, but 'rom is a member of any such value cell, then the address is said to be ROM and may not be written by any instruction. Instructions must come entirely from such ROM addresses. Finally, if an address is not unavailable or ROM by the preceding rules, we say that it is RAM, and it may be read or written by any instruction.

‘readp’ is a function of three arguments, x, map, and n. map should be a memory protection binary tree. x should be a natural number. n is the index of the ‘next bit’ to select upon in x while walking the x path through map. Typically ‘readp’ is called with n initially equal to 32 and map equal to the current memory protection map. ‘readp’ returns f if it encounters an 'unavailable at a node on the x path through map (considering only the least n significant bits of x), and otherwise readp returns t .

Definition: readp (x, n, map) = if 'unavailable ∈ value-field (map) then f

elseif (map ≃ nil) ∨ (n ≃ 0) then t

elseif b0p (bitn (x, n − 1)) then readp (x, n − 1, branch0 (map))

else readp (x, n − 1, branch1 (map)) endif

In our specification, programs can only be stored in ROM. The function ‘pc-readp’ returns t only when it hits a 'rom at a node on the path x through map and only if there is no 'unavailable at each node on the path x. n serves the same role it does in ‘readp’, as an index into x.

Definition: pc-readp (x, n, map) = if 'unavailable ∈ value-field (map) then f

elseif 'rom ∈ value-field (map) then readp (x, n, map) elseif (map ≃ nil) ∨ (n ≃ 0) then f elseif b0p (bitn (x, n − 1)) then pc-readp (x, n − 1, branch0 (map)) else pc-readp (x, n − 1, branch1 (map)) endif

‘writep’ is a function of three arguments, x, n, and map. ‘map’ should be a memory protection binary tree. x should be a natural number. ‘writep’ returns t if it never encounters 'unavailable or 'rom at a node on the path x through map, otherwise f . n serves the same role it does in ‘readp’, as an index into x.

Definition: writep (x, n, map) = if ('unavailable ∈ value-field (map))

∨ ('rom ∈ value-field (map)) then f elseif (map ≃ nil) ∨ (n ≃ 0) then t elseif b0p (bitn (x, n − 1)) then writep (x, n − 1, branch0 (map)) else writep (x, n − 1, branch1 (map)) endif

‘read’ is a function of three arguments, x, n, and bt. bt should be a binary tree, x and n should be natural numbers. ‘read’ returns the value component at the node reached by taking the path x through bt. n serves the same role it does in ‘readp’, as an index into x.

Definition: read (x, n, bt) = if n ≃ 0 then value-field (bt)

elseif b0p (bitn (x, n − 1)) then read (x, n − 1, branch0 (bt))

else read (x, n − 1, branch1 (bt)) endif

‘pc-read’ acts the same as read. But it is used in a quite different sense. So we introduce this dummy function.

Definition: pc-read (x, n, bt) = read (x, n, bt)

‘write’ is a function of four arguments, value, x, n, and bt. value, x, and n should be nonnegative integers, and bt should be a binary tree. ‘write’ returns the binary tree obtained by updating bt at the address x. n serves the same role it does in ‘readp’, as an index into x.

Definition: write (value, x, n, bt) = if n ≃ 0 then make-bt (value, branch0 (bt), branch1 (bt))

elseif b0p (bitn (x, n − 1)) then make-bt (value-field (bt),

write (value, x, n − 1, branch0 (bt)), branch1 (bt))

else make-bt (value-field (bt), branch0 (bt), write (value, x, n − 1, branch1 (bt))) endif

‘get-nth’ is a function of two arguments. The first should be a nonnegative integer and the second should be a list. ‘get-nth’ returns the n^{th} element of lst. Indexing is 0-based. For example, get-nth (0, list (a, b, c)) = a.

Definition: get-nth (n, lst) = if n ≃ 0 then car (lst)

else get-nth (n − 1, cdr (lst)) endif

‘put-nth’ is a function of three arguments: value, n, and lst. value and n should be natural numbers, and lst should be a list. ‘put-nth’ returns a list like lst except that the n^{th} element has been changed to be value. Indexing is 0-based, e.g., put-nth (d, 1, list (a, b, c)) = list (a, d, c).

Definition: put-nth (value, n, lst) = if n ≃ 0 then cons (value, cdr (lst))

else cons (car (lst), put-nth (value, n − 1, cdr (lst))) endif

The size of the operand, given the operation length.

Definition: op-sz (oplen) = (oplen ÷ b)

‘read-rn’ and ‘write-rn’ are two functions used to fetch and modify the register rn in the register file regs.

Definition: read-rn (oplen, rn, regs) = head (get-nth (rn, regs), oplen)

Definition: write-rn (oplen, value, rn, regs) = put-nth (replace (oplen, value, get-nth (rn, regs)), rn, regs)

A machine state is defined to be a list of length 5, say (status regs pc ccr mem), whose components have the following purposes: status, if it is not 'running, is the reason that execution was stopped; regs holds the data registers and the address registers; pc is the program counter; ccr is the 16-bit condition code register; and mem is the memory, including protection information. The status field is set when we encounter an instruction which we do not choose to handle for some reason. Among the many reasons that might arise for setting the status field are (1) an illegal instruction, (2) a legal MC68020 instruction (e.g., CALLM) that this specification does not handle, and (3) an illegal addressing mode. To construct a state one uses the 5 argument function ‘mc-state’, giving it as arguments, in order, the halt-reason, the data and address registers, the pc, the ccr, and the memory. The five fields of a state can be accessed with the five accessor functions ‘mc-status’, ‘mc-rfile’, ‘mc-pc’, ‘mc-ccr’, and ‘mc-mem’.

Definition: mc-state (status, regs, pc, ccr, mem) = list (status, regs, pc, ccr, mem)

Definition: mc-status (s) = car (s)

Definition: mc-rfile (s) = cadr (s)

Definition: mc-pc (s) = head (caddr (s), l)

Definition: mc-ccr (s) = head (cadddr (s), b)

Definition: mc-mem (s) = caddddr (s)

‘len’ is a function of one argument, lst, which should be a proper list. ‘len’ returns the length of lst, i.e., the number of elements in lst.

Definition: len (lst) = if lst ≃ nil then 0

else 1 + len (cdr (lst)) endif

‘mc-haltp’ returns t if some halting condition has been satisfied.

Definition: mc-haltp (s) = (mc-status (s) ≠ 'running)

8 Operands from Memory

Everything in this section is machine dependent. We assume the memory capacity is 2^{32}. In our specification, the memory is a binary tree with depth 32.

Definition: byte-readp (x, mem) = readp (x, 32, car (mem))

‘read-memp’ returns t if the k consecutive bytes in memory starting at x are readable, but returns f otherwise.

Definition: read-memp (x, mem, k) = if k ≃ 0 then t

else byte-readp (add (32, x, k − 1), mem) ∧ read-memp (x, mem, k − 1) endif

‘word-readp’ determines whether both bytes of the word at the memory address x are readable.

Definition: word-readp (x, mem) = read-memp (x, mem, wsz)

‘long-readp’ determines whether all four bytes of the longword at the memory address x are readable.

Definition: long-readp (x, mem) = read-memp (x, mem, lsz)

Programs can only be stored in ROM. Assume that x is a pointer in some program segment. ‘pc-read-memp’ returns t if the next k consecutive bytes are ROM.

Definition: pc-byte-readp (x, mem) = pc-readp (x, 32, car (mem))

Definition: pc-read-memp (x, mem, k) = if k ≃ 0 then t

else pc-byte-readp (add (32, x, k − 1), mem) ∧ pc-read-memp (x, mem, k − 1) endif

Definition: pc-word-readp (x, mem) = pc-read-memp (x, mem, wsz)

Definition: pc-long-readp (x, mem) = pc-read-memp (x, mem, lsz)

Read from the memory. ‘byte-read’ reads a byte from the memory.

Definition: byte-read (x, mem) = head (read (x, 32, cdr (mem)), b)

Read k consecutive bytes from the memory at x to form a natural number. ‘read-mem’ is a function of three arguments, x, mem, and k. ‘read-mem’ returns the natural number obtained by ‘appending’ together the n bytes that are obtained by reading from mem at locations addr, …, addr + n − 1. The most significant byte is the one with the lowest memory address, and conversely, the least significant byte is the one with the highest memory address. This is known as the ‘Big Endian’ scheme of memory.

Definition: read-mem (x, mem, k) = if k ≃ 0 then 0

else app (b, byte-read (add (32, x, k − 1), mem), read-mem (x, mem, k − 1)) endif

The two functions ‘word-read’ and ‘long-read’ use the function ‘read-mem’ to obtain a word or a long word from the memory.

Definition: word-read (x, mem) = read-mem (x, mem, wsz)

Definition: long-read (x, mem) = read-mem (x, mem, lsz)

Fetch instructions, by fetching bytes pointed to by the pc. This is the same as reading from memory. But we define a separate set of functions because we use them in a very different sense in our specification. ‘pc-byte-read’ reads a byte from the memory at pc. Definition: pc-byte-read (pc, mem) = head (pc-read (pc, 32, cdr (mem)), b) Definition: pc-read-mem (pc, mem, k) = if k ≃ 0 then 0

else app (b, pc-byte-read (add (32, pc, k − 1), mem), pc-read-mem (pc, mem, k − 1)) endif

‘pc-word-read’ reads a word from the memory at pc. Definition: pc-word-read (pc, mem) = pc-read-mem (pc, mem, wsz)

‘pc-long-read’ reads a longword from the memory at pc. Definition: pc-long-read (pc, mem) = pc-read-mem (pc, mem, lsz)

We define some bit field extractors. The function names reflect the meanings of the fields for MC68020 instructions.

The source register field. ‘s rn’ is a function of one argument, ins, which should be a word, i.e., a 16-bit bit-vector. Nonnegative integer value of bits 0..2 of ins. Definition: s rn (ins) = bits (ins, 0, 2)

The source mode field. Integer value of bits 3..5 of ins. Definition: s mode (ins) = bits (ins, 3, 5)

The destination mode field. Integer value of bits 6..8 of ins. Definition: d mode (ins) = bits (ins, 6, 8)

The destination register field. Integer value of bits 9..11 of ins. Definition: d rn (ins) = bits (ins, 9, 11)

The op-mode field. Integer value of bits 6..8 of ins. Definition: opmode-field (ins) = bits (ins, 6, 8)

The condition field. Integer value of bits 8..11 of ins. Definition: cond-field (ins) = bits (ins, 8, 11)

By the “oplen” of an instruction we mean whether an instruction deals with a byte, word, long word, or quad word operation.

The oplen of the operation is normally determined by bits 6 and 7. ‘oplen’ is a function of one argument, ins, which normally is the first word of an instruction.

67 (common bit numbers)
00 byte
10 word
01 long word
11 illegal, but we return (qsz).

Definition: op-len (ins) = (b ∗ exp (2, bits (ins, 6, 7)))

9 Storing the Result

‘byte-writep’ determines whether the location x is writable with respect to the current memory.

Definition: byte-writep (x, mem) = writep (x, 32, car (mem))

‘write-memp’ determines whether the k consecutive bytes starting at address x in the memory are writable.

Definition: write-memp (x, mem, k) = if k ≃ 0 then t

else byte-writep (add (32, x, k − 1), mem) ∧ write-memp (x, mem, k − 1) endif

‘write-mem’ is a function of four arguments, value, x, mem, and k. value should be a natural number, namely the thing we are storing; x should be a natural number, namely the address at which to store value; mem is the memory; k is the number of bytes to store. We store the bytes one byte at a time, storing the most significant byte of value first, at location x, and storing subsequently, decreasingly significant bytes at increasing addresses.

Definition: byte-write (value, x, mem) = cons (car (mem), write (head (value, b), x, 32, cdr (mem)))

Definition: write-mem (value, x, mem, k) = if k ≃ 0 then mem

else write-mem (tail (value, b), x, byte-write (value, add (32, x, k − 1), mem), k − 1) endif

Obtain c, v, z, n, and x from CCR. The following five functions ‘ccr-c’, ‘ccrv’, ‘ccr-z’, ‘ccr-n’, and ‘ccr-x’ simply access the five correspondingly named bits of the CCR. We use them to specify the condition cc in the bcc instruction.

Definition: ccr-c (ccr) = bitn (ccr, 0)

Definition: ccr-v (ccr) = bitn (ccr, 1)

Definition: ccr-z (ccr) = bitn (ccr, 2)

Definition: ccr-n (ccr) = bitn (ccr, 3)

Definition: ccr-x (ccr) = bitn (ccr, 4)

Whenever instructions update the CCR, ‘cvznx’ simply generates a new partial CCR consisting of the new cvznx-flags.

Definition: cvznx (c, v, z, n, x) = (fix-bit (c)

+ ((2 ∗ fix-bit (v))

+ ((4 ∗ fix-bit (z))

+ ((8 ∗ fix-bit (n)) + (16 ∗ fix-bit (x))))))

‘set-cvznx’ replaces the old flags in CCR by the given flags.

Definition: set-cvznx (cvznx, ccr) = replace (5, cvznx, ccr)

Definition: set-c (c, ccr) = set-cvznx (cvznx (c, ccr-v (ccr), ccr-z (ccr), ccr-n (ccr), ccr-x (ccr)), ccr)

Definition: set-v (v, ccr) = set-cvznx (cvznx (ccr-c (ccr), v, ccr-z (ccr), ccr-n (ccr), ccr-x (ccr)), ccr)

Definition: set-z (z, ccr) = set-cvznx (cvznx (ccr-c (ccr), ccr-v (ccr), z, ccr-n (ccr), ccr-x (ccr)), ccr)

Definition: set-n (n, ccr) = set-cvznx (cvznx (ccr-c (ccr), ccr-v (ccr), ccr-z (ccr), n, ccr-x (ccr)), ccr)

Definition: set-x (x, ccr) = set-cvznx (cvznx (ccr-c (ccr), ccr-v (ccr), ccr-z (ccr), ccr-n (ccr), x), ccr)

To halt the machine, we simply put the halting reason “signal” in the machine state.

Definition: halt (signal, s) = mc-state (signal, mc-rfile (s), mc-pc (s), mc-ccr (s), mc-mem (s))

To update the register file in the state s.

Definition: update-rfile (new-rfile, s) = mc-state (mc-status (s), new-rfile, mc-pc (s), mc-ccr (s), mc-mem (s))

To update the program counter in the state s.

Definition: update-pc (new-pc, s) = mc-state (mc-status (s), mc-rfile (s), new-pc, mc-ccr (s), mc-mem (s))

To update the condition code in the state s.

Definition: update-ccr (new-ccr, s) = mc-state (mc-status (s),

mc-rfile (s), mc-pc (s), set-cvznx (new-ccr, mc-ccr (s)), mc-mem (s))

To update the memory in the state s.

Definition: update-mem (new-mem, s) = mc-state (mc-status (s), mc-rfile (s), mc-pc (s), mc-ccr (s), new-mem)

‘read-dn’ and ‘read-an’ are used to fetch data and address registers in the machine state s.

Definition: read-dn (oplen, dn, s) = read-rn (oplen, dn, mc-rfile (s))

Definition: read-an (oplen, an, s) = read-rn (oplen, 8 + an, mc-rfile (s))

‘write-dn’ and ‘write-an’ are used to modify data and address registers in the machine state s. They return the modified machine state.

Definition: write-dn (oplen, value, dn, s) = update-rfile (write-rn (oplen, value, dn, mc-rfile (s)), s)

Definition: write-an (oplen, value, an, s) = update-rfile (write-rn (oplen, value, 8 + an, mc-rfile (s)), s)

‘sp’ is the constant 7, which refers to the stack pointer sp(a7) in the address register file.

Definition: sp = 7

‘read-sp’ is a function that fetches the stack pointer in the given state s.

Definition: read-sp (s) = read-an (l, sp, s)

‘write-sp’ is a function of two arguments, value and s. It returns a new machine state with the stack pointer updated to value.

Definition: write-sp (value, s) = write-an (l, value, sp, s)

‘push-up’ pushes value onto the sp stack and increments sp.

Definition: push-sp (opsz, value, s) = let sp be sub (l, opsz, read-sp (s))

in

if write-memp (sp, mc-mem (s), opsz)

then update-mem (write-mem (value, sp, mc-mem (s), opsz),

write-sp (sp, s))

else halt (write-signal, s) endif endlet

10 Retrieving the Operand According to Oplen

The function ‘operand’ returns the operand based on the given addr. addr should be a cons; the ‘car’ tells us where to retrieve the operand, the ‘cdr’ provides the real address.

Definition: operand (oplen, addr, s) = if car (addr) = 'd then read-dn (oplen, cdr (addr), s)

elseif car (addr) = 'a then read-an (oplen, cdr (addr), s)

elseif car (addr) = 'm

then read-mem (cdr (addr), mc-mem (s), op-sz (oplen))

else cdr (addr) endif

11 Effective Address Calculation

We now begin the definition of a collection of functions culminating in the function ‘effec-addr’, which computes “the effective address” for MC68020 instructions. (Actually, some instructions, e.g., the MOVE instruction, compute two effective addresses.)

In his Ph. D. thesis, Warren Hunt specified the FM8502 microprocessor in the Nqthm logic [1]. In Hunt’s FM8502 there is only one instruction format. Therefore in the FM8502 “soft-machine” specification one can compute the effective addresses before looking at the op-code. But in the MC68020, there are several instruction formats, and the algorithm for computing effective addresses depends upon what the op-code is. So we cannot handle instructions as uniformly as in FM8502. We have to know what the op-code is at a very early stage in the implementation.

Pre-effect and post-effect are two functions used in address register predecrement and postincrement.

Definition: post-effect (oplen, rn, addr) = if (rn = sp) ∧ (oplen = b) then add (l, addr, wsz)

else add (l, addr, op-sz (oplen)) endif

Definition: pre-effect (oplen, rn, addr) = if (rn = sp) ∧ (oplen = b) then sub (l, wsz, addr)

else sub (l, op-sz (oplen), addr) endif

For each of the different effective addressing modes, we define a function that “does the work.” In each case, the function takes as its argument the current value of the state, s. Some may take other parameters. In each case a ‘cons’ is returned, consisting of (a) an internal state with possible an and pc updates after the effective address calculation; (b) the effective address, normally another cons indicating where to look and where to get the operands.

Register direct modes. Data register direct (000) and address register direct (001). Number of extension words: 0.

‘dn-direct’ is a function of two arguments, rn and s. rn should be a natural number and s should be an mc-state. Mode 000.

Definition: dn-direct (rn, s) = cons (s, cons ('d, rn))

‘an-direct’ is a function of two arguments, rn and s. rn should be a natural number and s should be an mc-state. Mode 001.

Definition: an-direct (rn, s) = cons (s, cons ('a, rn))

Memory address modes. The pc argument to these effective address subroutines need not be the actual pc of the instruction. In the case of the MOVE instruction, which involves two effective address calculations, the pc will point to the word before the “next” possible byte in the memory which is to be used as an extension word. For example, the instruction

i: move (1,a0) (2,a2)

i.e., move the word at 1 + (a0) to 2 + (a2), requires altogether 3 words because two extension words are required, one for each of the displacements (1 and 2). When we invoke the function ‘addr-disp’ for the calculation of the first effective address, the pc will be i. But when we again invoke the function ‘addr-disp’ for the calculation of the second effective address, the pc will be i+2.

A subtlety about pc displacement. The one MC68020 instruction that involves two effective address calculations, the MOVE instruction, will have its second effective address calculation performed by us with the pc not pointing necessarily to the MOVE instruction but rather (possibly) pointing to the next word after the calculation of the first effective address. However, this discrepancy does not cause a problem with pc relative addressing because pc relative addressing is prohibited in the second effective address calculation.

Address register indirect, mode 010. Number of extension words: 0. ‘addrindirect’ is a function of two arguments, rn and s. rn should be a natural number and s should be a machine state. It returns the contents of the rn element of the address register file.

Definition: addr-indirect (rn, s) = cons (s, cons ('m, read-an (l, rn, s)))

Address register indirect with postincrement, mode 011. Number of extension words: 0.

Definition: addr-postinc (oplen, rn, s) = let addr be read-an (l, rn, s)

in

cons (write-an (l, post-effect (oplen, rn, addr), rn, s), cons ('m, addr)) endlet

Address register indirect with predecrement, mode 100. Number of extension words: 0. The function ‘addr-predec’ returns a cons of the given state s and the contents of the rn element of the register file after the register has been predecremented.

Definition: addr-predec (oplen, rn, s)

= let addr be read-an (l, rn, s)

in

cons (write-an (l, pre-effect (oplen, rn, addr), rn, s), cons ('m, pre-effect (oplen, rn, addr))) endlet

Address register indirect with index, mode 101. Number of extension words:

1. We now begin handling an effective address calculation which involves an extension word. In this mode, we add in the sign-extended 16-bit quantity in the word after the pc. We return a cons with (a) the state with pc incremented and (b) the sum of the address register rn and the sign-extended contents of the next word.

Definition: addr-disp (pc, rn, s) = if pc-word-readp (pc, mc-mem (s))

then cons (update-pc (add (l, pc, wsz), s),

cons ('m,

add (l, read-an (l, rn, s), ext (w, pc-word-read (pc, mc-mem (s)), l))))

else cons (halt (pc-signal, s), nil) endif

Address register indirect with index (8-bit displacement), mode 110. Number of extension words: 1.

Definition: index-rn (indexwd) = bits (indexwd, 12, 14)

Definition: index-register (indexwd, s) = if b0p (bitn (indexwd, 15))

then if b0p (bitn (indexwd, 11))

then ext (w, read-dn (w, index-rn (indexwd), s), l) else read-dn (l, index-rn (indexwd), s) endif

elseif b0p (bitn (indexwd, 11))

then ext (w, read-an (w, index-rn (indexwd), s), l)

else read-an (l, index-rn (indexwd), s) endif

Definition: ir-scaled (indexwd, s) = asl (l, index-register (indexwd, s), bits (indexwd, 9, 10))

Definition: addr-index-disp (pc, rn, indexwd, s) = cons (update-pc (pc, s),

cons ('m, add (l, add (l, read-an (l, rn, s), ext (b, head (indexwd, b), l)), ir-scaled (indexwd, s))))

Address register indirect with index (base displacement), mode 110. Number of extension words: 1, 2, or 3.

Definition: addr-index-bd (pc, addr, indexwd, s) = cons (update-pc (pc, s), cons ('m, add (l, addr, ir-scaled (indexwd, s))))

Memory indirect without index, mode 110. Number of extension words: 1, 2, 3, 4, or 5.

Definition: mem-indirect (pc, addr, olen, s) = if long-readp (addr, mc-mem (s))

then if pc-read-memp (pc, mc-mem (s), op-sz (olen))

then cons (update-pc (add (l, pc, op-sz (olen)), s),

cons ('m,

add (l, long-read (addr, mc-mem (s)), ext (olen,

pc-read-mem (pc, mc-mem (s), op-sz (olen)), l))))

else cons (halt (pc-signal, s), nil) endif else cons (halt (read-signal, s), nil) endif

Memory indirect postindexed mode.

Definition: mem-postindex (pc, addr, indexwd, olen, s) = if long-readp (addr, mc-mem (s))

then if pc-read-memp (pc, mc-mem (s), op-sz (olen))

then cons (update-pc (add (l, pc, op-sz (olen)), s),

cons ('m,

add (l,

add (l, long-read (addr, mc-mem (s)), ir-scaled (indexwd, s)),

ext (olen, pc-read-mem (pc, mc-mem (s), op-sz (olen)), l))))

else cons (halt (pc-signal, s), nil) endif else cons (halt (read-signal, s), nil) endif

Memory indirect preindexed mode.

Definition: mem-preindex (pc, addr, indexwd, olen, s) = mem-indirect (pc, add (l, addr, ir-scaled (indexwd, s)), olen, s)

Definition: i-is (indexwd) = bits (indexwd, 0, 2)

The base displacement has been added to addr, if necessary. ‘addr-index3’ is to consider the index register and index/indirect selection.

Definition: addr-index3 (pc, addr, indexwd, s) = if b0p (bitn (indexwd, 6))

then if i-is (indexwd) < 4

then if i-is (indexwd) < 2

then if i-is (indexwd) = 0 then addr-index-bd (pc, addr, indexwd, s) else mem-preindex (pc, addr, indexwd, 0, s) endif

elseif i-is (indexwd) = 2

then mem-preindex (pc, addr, indexwd, w, s) else mem-preindex (pc, addr, indexwd, l, s) endif

elseif i-is (indexwd) < 6 then if i-is (indexwd) = 4

then cons (halt (reserved-signal, s), nil)

else mem-postindex (pc, addr, indexwd, 0, s) endif elseif i-is (indexwd) = 6 then mem-postindex (pc, addr, indexwd, w, s) else mem-postindex (pc, addr, indexwd, l, s) endif

elseif i-is (indexwd) < 4 then if i-is (indexwd) < 2

then if i-is (indexwd) = 0 then cons (update-pc (pc, s), cons ('m, addr)) else mem-indirect (pc, addr, 0, s) endif

elseif i-is (indexwd) = 2 then mem-indirect (pc, addr, w, s) else mem-indirect (pc, addr, l, s) endif else cons (halt (reserved-signal, s), nil) endif

Definition: bd-sz (indexwd) = bits (indexwd, 4, 5)

The address register (base register) has been added to addr, if necessary. ‘addr-index2’ is to consider the base displacement.

Definition: addr-index2 (pc, addr, indexwd, s) = if bd-sz (indexwd) < 2

then if bd-sz (indexwd) = 0 then cons (halt (reserved-signal, s), nil)

else addr-index3 (pc, addr, indexwd, s) endif elseif bd-sz (indexwd) = 2 then if pc-word-readp (pc, mc-mem (s))

then addr-index3 (add (l, pc, wsz), add (l, addr, ext (w, pc-word-read (pc, mc-mem (s)), l)), indexwd, s) else cons (halt (pc-signal, s), nil) endif

elseif pc-long-readp (pc, mc-mem (s)) then addr-index3 (add (l, pc, lsz),

add (l, addr, pc-long-read (pc, mc-mem (s))), indexwd, s)

else cons (halt (pc-signal, s), nil) endif

Definition: bs-register (rn, indexwd, s) = if b0p (bitn (indexwd, 7)) then read-an (l, rn, s)

else 0 endif

‘addr-index1’ is to consider the address register (base register).

Definition: addr-index1 (pc, rn, indexwd, s) = if b0p (bitn (indexwd, 8)) then addr-index-disp (pc, rn, indexwd, s)

elseif b0p (bitn (indexwd, 3)) then addr-index2 (pc, bs-register (rn, indexwd, s), indexwd, s) else cons (halt (reserved-signal, s), nil) endif

Definition: addr-index (pc, rn, s) = if pc-word-readp (pc, mc-mem (s))

then addr-index1 (add (l, pc, wsz), rn, pc-word-read (pc, mc-mem (s)), s) else cons (halt (pc-signal, s), nil) endif

Absolute short address. Mode 111, rn 000.

Definition: absolute-short (pc, s) = if pc-word-readp (pc, mc-mem (s))

then cons (update-pc (add (l, pc, wsz), s),

cons ('m, ext (w, pc-word-read (pc, mc-mem (s)), l)))

else cons (halt (pc-signal, s), nil) endif

Absolute long address. Mode 111, rn 001.

Definition: absolute-long (pc, s) = if pc-long-readp (pc, mc-mem (s))

then cons (update-pc (add (l, pc, lsz), s),

cons ('m, pc-long-read (pc, mc-mem (s))))

else cons (halt (pc-signal, s), nil) endif

Surprisingly, the design of the MC68020 deliberately avoids having two program counter addressing modes. This specification here relies on this very fact.

Program counter indirect with displacement. Mode 111, rn 010. Number of extension words: 1.

Definition: pc-disp (pc, s) = if pc-word-readp (pc, mc-mem (s))

then cons (update-pc (add (l, pc, wsz), s),

cons ('m, add (l, pc, ext (w, pc-word-read (pc, mc-mem (s)), l))))

else cons (halt (pc-signal, s), nil) endif

Program counter indirect with index (8-bit displacement). mode 111, rn 011.

Definition: pc-index-disp (pc, indexwd, s) = cons (update-pc (add (l, pc, wsz), s),

cons ('m,

add (l, add (l, pc, ext (b, head (indexwd, b), l)), ir-scaled (indexwd, s))))

Program counter indirect with index (base displacement) mode. Program counter memory indirect postindexed mode. Program counter memory indirect preindexed mode.

Definition: bs-pc (pc, indexwd) = if b0p (bitn (indexwd, 7)) then pc

else 0 endif

Definition: pc-index1 (pc, indexwd, s) = if b0p (bitn (indexwd, 8)) then pc-index-disp (pc, indexwd, s)

elseif b0p (bitn (indexwd, 3))

then addr-index2 (add (l, pc, wsz), bs-pc (pc, indexwd), indexwd, s)

else cons (halt (reserved-signal, s), nil) endif Definition: pc-index (pc, s) = if pc-word-readp (pc, mc-mem (s))

then pc-index1 (pc, pc-word-read (pc, mc-mem (s)), s)

else cons (halt (pc-signal, s), nil) endif

Immediate data. Mode 111, rn 100. Number of extension words: 1 or 2.

Definition: immediate (oplen, pc, s) = if oplen = b

then if pc-word-readp (pc, mc-mem (s))

then cons (update-pc (add (l, pc, wsz), s),

cons ('i, pc-byte-read (add (l, pc, bsz), mc-mem (s))))

else cons (halt (pc-signal, s), nil) endif elseif pc-read-memp (pc, mc-mem (s), op-sz (oplen)) then cons (update-pc (add (l, pc, op-sz (oplen)), s),

cons ('i, pc-read-mem (pc, mc-mem (s), op-sz (oplen))))

else cons (halt (pc-signal, s), nil) endif

Effective address calculation. ‘effec-addr’ is a function of four arguments, oplen, mode, rn, and s. ‘oplen’ should be b, w, or l; it is the size of the datum we are computing the effective address of. mode is a natural number extracted from the first word of the instruction; mode indicates pre-decrement, post-increment, etc. rn is a natural number extracted from the first word of the instruction; rn designates a register. s the current machine state. ‘effec-addr’ returns a pair, or ‘cons’ as it is called in Lisp and Nqthm. The first element (or ‘car’) of this pair is an internal state after this effective address calculation. The second element (or cdr) is another ‘cons’ consisting of the direction (’d, ’a, ’m, or ’i), and the effective address (a nonnegative integer). Because MC68020 instructions can be as many as 11 words long, the calculation of the next pc is intimately tied to the effective address calculation.

Definition: effec-addr (oplen, mode, rn, s) = if mode < 4

then if mode < 2

then if mode = 0 then dn-direct (rn, s) else an-direct (rn, s) endif elseif mode = 2 then addr-indirect (rn, s) else addr-postinc (oplen, rn, s) endif

elseif mode < 6

then if mode = 4 then addr-predec (oplen, rn, s) else addr-disp (mc-pc (s), rn, s) endif elseif mode = 6 then addr-index (mc-pc (s), rn, s) elseif rn < 4 then if rn < 2

then if rn = 0 then absolute-short (mc-pc (s), s) else absolute-long (mc-pc (s), s) endif

elseif rn = 2 then pc-disp (mc-pc (s), s)

else pc-index (mc-pc (s), s) endif else immediate (oplen, mc-pc (s), s) endif

Given an effective address field, test if it is one of the existing addressing modes.

Definition: addr-modep (mode, rn) = if mode = 7 then rn ≤ 4

else t endif

Given an effective address field, test if it is a data addressing mode.

Definition: data-addr-modep (mode, rn) = if mode = 7 then rn ≤ 4

else mode ≠ 1 endif

Given an effective address field, test if it is a memory addressing mode.

Definition: memory-addr-modep (mode, rn) = if mode = 7 then rn ≤ 4

else mode ≥ 2 endif

Given an effective address field, test if it is a control addressing mode.

Definition: control-addr-modep (mode, rn) = if mode = 7 then rn ≤ 3

else (mode = 2) ∨ (mode ≥ 5) endif

Given an effective address field, test if it is an alterable addressing mode.

Definition: alterable-addr-modep (mode, rn) = ((mode ≠ 7) ∨ (rn = 0) ∨ (rn = 1))

‘dn-direct-modep’ returns t if the addressing mode is a data register direct. Returns f otherwise.

Definition: dn-direct-modep (mode) = (mode = 0)

‘an-direct-modep’ returns t if the addressing mode is an address register direct, and returns f otherwise.

Definition: an-direct-modep (mode) = (mode = 1)

Postincrement.

Definition: postinc-modep (mode) = (mode = 3)

Predecrement.

Definition: predec-modep (mode) = (mode = 4)

Definition: idata-modep (mode, rn) = ((mode = 7) ∧ (rn = 4))

In address register direct (001), a byte size operation is not allowed.

Definition: byte-an-direct-modep (oplen, mode) = ((oplen = b) ∧ an-direct-modep (mode))

An internal state in the execution of one instruction.

Definition: mc-instate (oplen, ins, s) = let s&addr be effec-addr (oplen, s mode (ins), s rn (ins), s)

in

if cadr (s&addr) = 'm

then if read-memp (cddr (s&addr), mc-mem (s), op-sz (oplen)) then s&addr else cons (halt (read-signal, s), nil) endif

else s&addr endif endlet

Mapping functions. ‘mapping’ finishes the execution of instructions. ‘mapping’ maps a machine state into the next state.

Definition: d-mapping (oplen, v&cvznx, addr, s) = mc-state (mc-status (s),

write-rn (oplen, car (v&cvznx), addr, mc-rfile (s)), mc-pc (s), set-cvznx (cdr (v&cvznx), mc-ccr (s)), mc-mem (s))

Definition: a-mapping (oplen, v&cvznx, addr, s) = mc-state (mc-status (s), write-rn (oplen, car (v&cvznx), 8 + addr, mc-rfile (s)), mc-pc (s), set-cvznx (cdr (v&cvznx), mc-ccr (s)), mc-mem (s))

Definition: m-mapping (oplen, v&cvznx, addr, s) = if write-memp (addr, mc-mem (s), op-sz (oplen))

then mc-state (mc-status (s), mc-rfile (s), mc-pc (s), set-cvznx (cdr (v&cvznx), mc-ccr (s)), write-mem (car (v&cvznx), addr, mc-mem (s), op-sz (oplen)))

else halt (write-signal, s) endif

Definition: mapping (oplen, v&cvznx, s&addr) = if cadr (s&addr) = 'd

then d-mapping (oplen, v&cvznx, cddr (s&addr), car (s&addr))

elseif cadr (s&addr) = 'a

then a-mapping (oplen, v&cvznx, cddr (s&addr), car (s&addr))

else m-mapping (oplen, v&cvznx, cddr (s&addr), car (s&addr)) endif

12 The Individual Instructions

ADD instruction. The computation of the condition code register(CCR).

Definition: add-c (n, sopd, dopd) = let result be add (n, sopd, dopd)

in

b-or (b-or (b-and (mbit (sopd, n), mbit (dopd, n)),

b-and (b-not (mbit (result, n)), mbit (dopd, n))), b-and (mbit (sopd, n), b-not (mbit (result, n)))) endlet

Definition: add-v (n, sopd, dopd) = let result be add (n, sopd, dopd)

in

b-or (b-and (b-and (mbit (sopd, n), mbit (dopd, n)), b-not (mbit (result, n))),

b-and (b-and (b-not (mbit (sopd, n)), b-not (mbit (dopd, n))), mbit (result, n))) endlet Definition: add-z (oplen, sopd, dopd) = if add (oplen, dopd, sopd) = 0 then b1

else b0 endif

Definition: add-n (oplen, sopd, dopd) = mbit (add (oplen, dopd, sopd), oplen)

Definition: add-cvznx (oplen, sopd, dopd) = cvznx (add-c (oplen, sopd, dopd),

add-v (oplen, sopd, dopd), add-z (oplen, sopd, dopd), add-n (oplen, sopd, dopd), add-c (oplen, sopd, dopd))

The effects of the execution of an ADD instruction are given as follows.

Definition: add-effect (oplen, sopd, dopd) = cons (add (oplen, dopd, sopd), add-cvznx (oplen, sopd, dopd))

Test if the addressing mode is legal.

Definition: add-addr-modep1 (oplen, ins) = (addr-modep (s mode (ins), s rn (ins))

∧ (¬ byte-an-direct-modep (oplen, s mode (ins))))

Definition: add-addr-modep2 (ins) = (alterable-addr-modep (s mode (ins), s rn (ins))

∧ memory-addr-modep (s mode (ins), s rn (ins)))

An execution of an ADD instruction.

Definition: add-ins1 (oplen, ins, s) = if add-addr-modep1 (oplen, ins)

then let s&addr be mc-instate (oplen, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else d-mapping (oplen,

add-effect (oplen,

operand (oplen, cdr (s&addr),

s),

read-dn (oplen, d rn (ins), s)),

d rn (ins),

car (s&addr)) endif endlet

else halt (mode-signal, s) endif

Definition: add-mapping (opd, oplen, ins, s) = let s&addr be mc-instate (oplen, ins, s)

in

if mc-haltp (car (s&addr)) then car (s&addr)

else mapping (oplen,

add-effect (oplen, opd, operand (oplen, cdr (s&addr), s)),

s&addr) endif endlet

Definition: add-ins2 (oplen, ins, s) = if add-addr-modep2 (ins)

then add-mapping (read-dn (oplen, d rn (ins), s), oplen, ins, s) else halt (mode-signal, s) endif

ADDA instruction.

Definition: adda-addr-modep (ins) = addr-modep (s mode (ins), s rn (ins))

Notice that the ADDA instruction does not affect CCR.

Definition: adda-ins (oplen, ins, s) = if adda-addr-modep (ins)

then let s&addr be mc-instate (oplen, ins, s)

in

if mc-haltp (car (s&addr)) then car (s&addr) else write-an (l,

add (l, read-an (l, d rn (ins), car (s&addr)), ext (oplen,

operand (oplen, cdr (s&addr), s), l)),

d rn (ins),

car (s&addr)) endif endlet

else halt (mode-signal, s) endif

ADDX instruction.

Definition: addx-c (n, x, sopd, dopd) = let result be adder (n, x, sopd, dopd)

in

b-or (b-or (b-and (mbit (sopd, n), mbit (dopd, n)),

b-and (b-not (mbit (result, n)), mbit (dopd, n))), b-and (mbit (sopd, n), b-not (mbit (result, n)))) endlet

Definition: addx-v (n, x, sopd, dopd) = let result be adder (n, x, sopd, dopd)

in

b-or (b-and (b-and (mbit (sopd, n), mbit (dopd, n)), b-not (mbit (result, n))),

b-and (b-and (b-not (mbit (sopd, n)), b-not (mbit (dopd, n))), mbit (result, n))) endlet

Definition: addx-z (oplen, z, x, sopd, dopd) = b-and (z,

if adder (oplen, x, dopd, sopd) = 0 then b1 else b0 endif)

Definition: addx-n (oplen, x, sopd, dopd) = mbit (adder (oplen, x, dopd, sopd), oplen)

Definition: addx-cvznx (oplen, z, x, sopd, dopd) = cvznx (addx-c (oplen, x, sopd, dopd),

addx-v (oplen, x, sopd, dopd), addx-z (oplen, z, x, sopd, dopd), addx-n (oplen, x, sopd, dopd), addx-c (oplen, x, sopd, dopd))

Definition: addx-effect (oplen, sopd, dopd, ccr) = cons (adder (oplen, ccr-x (ccr), dopd, sopd),

addx-cvznx (oplen, ccr-z (ccr), ccr-x (ccr), sopd, dopd))

Definition: addx-ins1 (oplen, ins, s) = d-mapping (oplen,

addx-effect (oplen, read-dn (oplen, s rn (ins), s), read-dn (oplen, d rn (ins), s), mc-ccr (s)),

d rn (ins), s)

Definition: addx-ins2 (oplen, ins, s) = let s&addr0 be addr-predec (oplen, s rn (ins), s)

in

if read-memp (cddr (s&addr0 ), mc-mem (s), op-sz (oplen))

then let s&addr be addr-predec (oplen, d rn (ins), car (s&addr0 )) in if read-memp (cddr (s&addr), mc-mem (s), op-sz (oplen)) then mapping (oplen,

addx-effect (oplen,

operand (oplen, cdr (s&addr0 ), car (s&addr0 )),

operand (oplen, cdr (s&addr), car (s&addr)),

mc-ccr (s)),

s&addr) else halt (read-signal, s) endif endlet

else halt (read-signal, s) endif endlet

Opcode 1101. The ADD instruction group includes three instructions ADD, ADDA, and ADDX.

Definition: add-group (opmode, ins, s) = if opmode < 4

then if opmode = 3 then adda-ins (w, ins, s) else add-ins1 (op-len (ins), ins, s) endif

elseif opmode = 7 then adda-ins (l, ins, s)

elseif s mode (ins) = 0 then addx-ins1 (op-len (ins), ins, s) elseif s mode (ins) = 1 then addx-ins2 (op-len (ins), ins, s) else add-ins2 (op-len (ins), ins, s) endif

SUB instruction. The computation of the condition code register (ccr).

Definition: sub-c (n, sopd, dopd) = let result be sub (n, sopd, dopd) in b-or (b-or (b-and (mbit (sopd, n), b-not (mbit (dopd, n))),

b-and (mbit (result, n), b-not (mbit (dopd, n)))), b-and (mbit (sopd, n), mbit (result, n))) endlet

Definition: sub-v (n, sopd, dopd) = let result be sub (n, sopd, dopd)

in

b-or (b-and (b-and (b-not (mbit (sopd, n)), mbit (dopd, n)),

b-not (mbit (result, n))), b-and (b-and (mbit (sopd, n), b-not (mbit (dopd, n))),

mbit (result, n))) endlet

Definition: sub-z (oplen, sopd, dopd) = if sub (oplen, sopd, dopd) = 0 then b1

else b0 endif

Definition: sub-n (oplen, sopd, dopd) = mbit (sub (oplen, sopd, dopd), oplen)

Definition: sub-cvznx (oplen, sopd, dopd) = cvznx (sub-c (oplen, sopd, dopd),

sub-v (oplen, sopd, dopd), sub-z (oplen, sopd, dopd), sub-n (oplen, sopd, dopd), sub-c (oplen, sopd, dopd))

The effect of an execution of a SUB instruction.

Definition: sub-effect (oplen, sopd, dopd) = cons (sub (oplen, sopd, dopd), sub-cvznx (oplen, sopd, dopd))

Test if the addressing mode is illegal.

Definition: sub-addr-modep1 (oplen, ins) = (addr-modep (s mode (ins), s rn (ins))

∧ (¬ byte-an-direct-modep (oplen, s mode (ins))))

Definition: sub-addr-modep2 (ins) = (alterable-addr-modep (s mode (ins), s rn (ins))

∧ memory-addr-modep (s mode (ins), s rn (ins)))

The execution of the SUB instruction.

Definition: sub-ins1 (oplen, ins, s) = if sub-addr-modep1 (oplen, ins)

then let s&addr be mc-instate (oplen, ins, s)

in

if mc-haltp (car (s&addr)) then car (s&addr) else d-mapping (oplen,

sub-effect (oplen,

operand (oplen, cdr (s&addr), s),

read-dn (oplen, d rn (ins), s)),

d rn (ins),

car (s&addr)) endif endlet

else halt (mode-signal, s) endif

Definition: sub-mapping (opd, oplen, ins, s) = let s&addr be mc-instate (oplen, ins, s)

in

if mc-haltp (car (s&addr)) then car (s&addr)

else mapping (oplen,

sub-effect (oplen, opd, operand (oplen, cdr (s&addr), s)),

s&addr) endif endlet

Definition: sub-ins2 (oplen, ins, s) = if sub-addr-modep2 (ins)

then sub-mapping (read-dn (oplen, d rn (ins), s), oplen, ins, s) else halt (mode-signal, s) endif

SUBA instruction.

Definition: suba-addr-modep (ins) = addr-modep (s mode (ins), s rn (ins))

Definition: suba-ins (oplen, ins, s) = if suba-addr-modep (ins)

then let s&addr be mc-instate (oplen, ins, s)

in if mc-haltp (car (s&addr)) then car (s&addr) else write-an (l,

sub (l,

ext (oplen, operand (oplen, cdr (s&addr), s), l),

read-an (l, d rn (ins), car (s&addr))), d rn (ins), car (s&addr)) endif endlet

else halt (mode-signal, s) endif

SUBX instruction.

Definition: subx-c (n, x, sopd, dopd) = let result be subtracter (n, x, sopd, dopd)

in

b-or (b-or (b-and (mbit (sopd, n), b-not (mbit (dopd, n))),

b-and (mbit (result, n), b-not (mbit (dopd, n)))), b-and (mbit (sopd, n), mbit (result, n))) endlet

Definition: subx-v (n, x, sopd, dopd) = let result be subtracter (n, x, sopd, dopd)

in

b-or (b-and (b-and (b-not (mbit (sopd, n)), mbit (dopd, n)),

b-not (mbit (result, n))), b-and (b-and (mbit (sopd, n), b-not (mbit (dopd, n))),

mbit (result, n))) endlet

Definition: subx-z (oplen, z, x, sopd, dopd) = b-and (z,

if subtracter (oplen, x, sopd, dopd) = 0 then b1 else b0 endif)

Definition: subx-n (oplen, x, sopd, dopd) = mbit (subtracter (oplen, x, sopd, dopd), oplen)

Definition: subx-cvznx (oplen, z, x, sopd, dopd) = cvznx (subx-c (oplen, x, sopd, dopd),

subx-v (oplen, x, sopd, dopd), subx-z (oplen, z, x, sopd, dopd), subx-n (oplen, x, sopd, dopd), subx-c (oplen, x, sopd, dopd))

Definition: subx-effect (oplen, sopd, dopd, ccr) = cons (subtracter (oplen, ccr-x (ccr), sopd, dopd),

subx-cvznx (oplen, ccr-z (ccr), ccr-x (ccr), sopd, dopd))

Definition: subx-ins1 (oplen, ins, s) = d-mapping (oplen,

subx-effect (oplen, read-dn (oplen, s rn (ins), s), read-dn (oplen, d rn (ins), s), mc-ccr (s)),

d rn (ins),

s)

Definition: subx-ins2 (oplen, ins, s) = let s&addr0 be addr-predec (oplen, s rn (ins), s)

in

if read-memp (cddr (s&addr0 ), mc-mem (s), op-sz (oplen))

then let s&addr be addr-predec (oplen, d rn (ins), car (s&addr0 )) in if read-memp (cddr (s&addr), mc-mem (s), op-sz (oplen)) then mapping (oplen,

subx-effect (oplen,

operand (oplen, cdr (s&addr0 ), car (s&addr0 )),

operand (oplen, cdr (s&addr), car (s&addr)),

mc-ccr (s)),

s&addr) else halt (read-signal, s) endif endlet

else halt (read-signal, s) endif endlet

Opcode 1001. The SUB instruction group includes three instructions SUB, SUBA, and SUBX.

Definition: sub-group (opmode, ins, s) = if opmode < 4

then if opmode = 3 then suba-ins (w, ins, s) else sub-ins1 (op-len (ins), ins, s) endif

elseif opmode = 7 then suba-ins (l, ins, s) elseif s mode (ins) = 0 then subx-ins1 (op-len (ins), ins, s) elseif s mode (ins) = 1 then subx-ins2 (op-len (ins), ins, s) else sub-ins2 (op-len (ins), ins, s) endif

AND instruction. The computation of the condition code register(CCR).

Definition: and-z (oplen, sopd, dopd) = if logand (sopd, dopd) = 0 then b1

else b0 endif

Definition: and-n (oplen, sopd, dopd) = mbit (logand (sopd, dopd), oplen)

Definition: and-cvznx (oplen, sopd, dopd, ccr) = cvznx (b0, b0, and-z (oplen, sopd, dopd), and-n (oplen, sopd, dopd), ccr-x (ccr))

The effect of the execution of the AND instruction.

Definition: and-effect (oplen, sopd, dopd, ccr) = cons (logand (sopd, dopd), and-cvznx (oplen, sopd, dopd, ccr))

Test if the addressing mode is legal.

Definition: and-addr-modep1 (ins) = data-addr-modep (s mode (ins), s rn (ins))

Definition: and-addr-modep2 (ins) = (alterable-addr-modep (s mode (ins), s rn (ins))

∧ memory-addr-modep (s mode (ins), s rn (ins)))

The execution of the AND instruction.

Definition: and-ins1 (oplen, ins, s) = if and-addr-modep1 (ins)

then let s&addr be mc-instate (oplen, ins, s)

in

if mc-haltp (car (s&addr)) then car (s&addr) else d-mapping (oplen,

and-effect (oplen,

operand (oplen, cdr (s&addr), s), read-dn (oplen, d rn (ins), s), mc-ccr (s)),

d rn (ins),

car (s&addr)) endif endlet

else halt (mode-signal, s) endif

Definition: and-mapping (sopd, oplen, ins, s) = let s&addr be mc-instate (oplen, ins, s)

in

if mc-haltp (car (s&addr)) then car (s&addr)

else mapping (oplen,

and-effect (oplen, sopd, operand (oplen, cdr (s&addr), s), mc-ccr (s)),

s&addr) endif endlet

Definition: and-ins2 (oplen, ins, s) = if and-addr-modep2 (ins)

then and-mapping (read-dn (oplen, d rn (ins), s), oplen, ins, s)

else halt (mode-signal, s) endif

MULU.W/MULS.W instruction. S * D → D. MULU expects x and y to be two natural numbers.

Definition: mulu (n, x, y, i) = head (x ∗ y, n)

MULS expects x and y to be two natural numbers.

Definition: muls (n, x, y, i) = head (int-to-nat (itimes (nat-to-int (x, i), nat-to-int (y, i)), 2 ∗ i), n)

Definition: mul&div-addr-modep (ins) = data-addr-modep (s mode (ins), s rn (ins))

The condition codes for MULU.

Definition: mulu-v (n, sopd, dopd, i) = if (sopd ∗ dopd) < exp (2, n) then b0

else b1 endif Definition: mulu-z (n, sopd, dopd, i) = if mulu (n, sopd, dopd, i) = 0 then b1

else b0 endif

Definition: mulu-n (n, sopd, dopd, i) = mbit (mulu (n, sopd, dopd, i), n)

Definition: mulu-cvznx (n, sopd, dopd, i, ccr) = cvznx (b0,

mulu-v (n, sopd, dopd, i), mulu-z (n, sopd, dopd, i), mulu-n (n, sopd, dopd, i), ccr-x (ccr))

Definition: mulu w-ins (sopd, dn, s) = let dopd be read-dn (w, dn, s)

in

update-ccr (mulu-cvznx (l, sopd, dopd, w, mc-ccr (s)), write-dn (l, mulu (l, sopd, dopd, w), dn, s)) endlet

The condition codes for MULS.

Definition: muls-v (n, sopd, dopd, i) = if int-rangep (itimes (nat-to-int (sopd, i), nat-to-int (dopd, i)), n)

then b0 else b1 endif

Definition: muls-z (n, sopd, dopd, i) = if muls (n, sopd, dopd, i) = 0 then b1

else b0 endif

Definition: muls-n (n, sopd, dopd, i) = mbit (muls (n, sopd, dopd, i), n)

Definition: muls-cvznx (n, sopd, dopd, i, ccr) = cvznx (b0,

muls-v (n, sopd, dopd, i), muls-z (n, sopd, dopd, i), muls-n (n, sopd, dopd, i), ccr-x (ccr))

Definition: muls w-ins (sopd, dn, s) = let dopd be read-dn (w, dn, s)

in

update-ccr (muls-cvznx (l, sopd, dopd, w, mc-ccr (s)), write-dn (l, muls (l, sopd, dopd, w), dn, s)) endlet

EXG instruction. Exchange the contents of two data registers.

Definition: exg-drdr-ins (ins, s) = let dx be read-dn (l, d rn (ins), s),

dy be read-dn (l, s rn (ins), s) in write-dn (l, dy, d rn (ins), write-dn (l, dx, s rn (ins), s)) endlet

Exchange the contents of two address registers.

Definition: exg-arar-ins (ins, s) = let ax be read-an (l, d rn (ins), s),

ay be read-an (l, s rn (ins), s) in write-an (l, ay, d rn (ins), write-an (l, ax, s rn (ins), s)) endlet

Exchange the contents of data and address registers.

Definition: exg-drar-ins (ins, s) = let dx be read-dn (l, d rn (ins), s),

ay be read-an (l, s rn (ins), s) in write-dn (l, ay, d rn (ins), write-an (l, dx, s rn (ins), s)) endlet

Definition: mul w-ins (ins, s) = if mul&div-addr-modep (ins)

then let s&addr be mc-instate (w, ins, s)

in

if mc-haltp (car (s&addr)) then car (s&addr) else let sopd be operand (w, cdr (s&addr), s)

in

if b0p (bitn (ins, 8)) then mulu w-ins (sopd,

d rn (ins), car (s&addr)) else muls w-ins (sopd,

d rn (ins),

car (s&addr)) endif endlet endif endlet

else halt (mode-signal, s) endif

Opcode 1100. The AND instruction group includes three instructions AND, MULS.W/MULU.W, and EXG. Detect ABCD.

Definition: and-group (oplen, ins, s) = if oplen = q then mul w-ins (ins, s)

elseif b0p (bitn (ins, 8)) then and-ins1 (oplen, ins, s)

elseif s mode (ins) < 2

then if oplen = b then halt ('abcd-unspecified, s) elseif oplen = w then if s mode (ins) = 0 then exg-drdr-ins (ins, s)

else exg-arar-ins (ins, s) endif elseif s mode (ins) = 0 then halt (reserved-signal, s) else exg-drar-ins (ins, s) endif

else and-ins2 (oplen, ins, s) endif

OR instruction. The computation of the condition code register.

Definition: or-z (oplen, sopd, dopd) = if logor (sopd, dopd) = 0 then b1

else b0 endif

Definition: or-n (oplen, sopd, dopd) = b-or (mbit (sopd, oplen), mbit (dopd, oplen))

Definition: or-cvznx (oplen, sopd, dopd, ccr) = cvznx (b0, b0, or-z (oplen, sopd, dopd), or-n (oplen, sopd, dopd), ccr-x (ccr))

The effect of an execution of an OR instruction.

Definition: or-effect (oplen, sopd, dopd, ccr) = cons (logor (sopd, dopd), or-cvznx (oplen, sopd, dopd, ccr))

Test if the addressing mode is illegal.

Definition: or-addr-modep1 (ins) = data-addr-modep (s mode (ins), s rn (ins))

Definition: or-addr-modep2 (ins) = (alterable-addr-modep (s mode (ins), s rn (ins))

∧ memory-addr-modep (s mode (ins), s rn (ins)))

The execution of the OR instruction.

Definition: or-ins1 (oplen, ins, s) = if or-addr-modep1 (ins)

then let s&addr be mc-instate (oplen, ins, s)

in

if mc-haltp (car (s&addr)) then car (s&addr) else d-mapping (oplen,

or-effect (oplen,

operand (oplen, cdr (s&addr), s),

read-dn (oplen, d rn (ins), s), mc-ccr (s)),

d rn (ins),

car (s&addr)) endif endlet

else halt (mode-signal, s) endif

Definition: or-mapping (sopd, oplen, ins, s) = let s&addr be mc-instate (oplen, ins, s)

in

if mc-haltp (car (s&addr)) then car (s&addr)

else mapping (oplen,

or-effect (oplen, sopd, operand (oplen, cdr (s&addr), s), mc-ccr (s)),

s&addr) endif endlet

Definition: or-ins2 (oplen, ins, s) = if or-addr-modep2 (ins)

then or-mapping (read-dn (oplen, d rn (ins), s), oplen, ins, s)

else halt (mode-signal, s) endif

DIVU.W/DIVS.W instructions. D(32)/S(16) → D(16r:16q). ‘iquot’ and ‘irem’ expect that s and d are unsigned integers. They are used in the DIV instruction.

Definition: iquot (n, s, i, d, j ) = head (int-to-nat (iquotient (nat-to-int (d, j ), nat-to-int (s, i)), j ), n)

Definition: irem (n, s, i, d, j ) = head (int-to-nat (iremainder (nat-to-int (d, j ), nat-to-int (s, i)), i), n)

DIVS.W instruction.

Definition: divs-v (n, sopd, i, dopd, j ) = if int-rangep (iquotient (nat-to-int (dopd, j ), nat-to-int (sopd, i)), n)

then b0 else b1 endif

Definition: divs-z (n, sopd, i, dopd, j ) = if iquot (n, sopd, i, dopd, j ) = 0 then b1

else b0 endif

Definition: divs-n (n, sopd, i, dopd, j ) = mbit (iquot (n, sopd, i, dopd, j ), n)

In our specification of DIV, we only make sure that the N and Z bits are set correctly when there is NO overflow. Since we test for overflow before this instruction is fully completed, the setting of CCR is actually the same as AND’s if NO overflow occurs. When an overflow is detected, we simply halt the machine with an error signal.

If overflow or divide by zero happens during the DIV instructions, then the MC68020 manual states that values of N, Z, and V are undefined. Thus one should not count on the validity of these values in the error state returned by ‘stepi’.

Definition: divs-cvznx (n, sopd, i, dopd, j , ccr) = cvznx (b0,

b0,

divs-z (n, sopd, i, dopd, j ), divs-n (n, sopd, i, dopd, j ), ccr-x (ccr))

32/16 → 16r:16q.

Definition: divs w-ins (sopd, dn, s)

= if nat-to-int (sopd, w) = 0 then halt ('trap-exception, s)

else let dopd be read-dn (l, dn, s) in if b0p (divs-v (w, sopd, w, dopd, l)) then update-ccr (divs-cvznx (w,

sopd, w, dopd, l, mc-ccr (s)),

write-dn (l,

app (w, iquot (w, sopd, w, dopd, l), irem (w, sopd, w, dopd, l)),

dn, s))

        else halt ('divs-overflow,

update-ccr (set-v (b1, mc-ccr (s)), s)) endif endlet endif

DIVU.W instruction.

Definition: quot (n, x, y) = head (y ÷ x, n)

Definition: rem (n, x, y) = head (y mod x, n)

The condition codes for DIVU.

Definition: divu-v (n, sopd, dopd) = if (dopd ÷ sopd) < exp (2, n) then b0

else b1 endif

Definition: divu-z (n, sopd, dopd) = if quot (n, sopd, dopd) = 0 then b1

else b0 endif

Definition: divu-n (n, sopd, dopd) = mbit (quot (n, sopd, dopd), n)

Same treatment as divs-cvznx.

Definition: divu-cvznx (n, sopd, dopd, ccr) = cvznx (b0, b0, divu-z (n, sopd, dopd), divu-n (n, sopd, dopd), ccr-x (ccr))

32/16 → 16r:16q.

Definition: divu w-ins (sopd, dn, s) = if nat-to-uint (sopd) = 0 then halt ('trap-exception, s)

else let dopd be read-dn (l, dn, s)

in

if b0p (divu-v (w, sopd, dopd))

then update-ccr (divu-cvznx (w, sopd, dopd, mc-ccr (s)),

write-dn (l,

app (w, quot (w, sopd, dopd), rem (w, sopd, dopd)),

dn, s))

        else halt ('divu-overflow,

update-ccr (set-v (b1, mc-ccr (s)), s)) endif endlet endif

Definition: div w-ins (ins, s) = if mul&div-addr-modep (ins)

then let s&addr be mc-instate (w, ins, s)

in

if mc-haltp (car (s&addr)) then car (s&addr) else let sopd be operand (w, cdr (s&addr), s)

in

if b0p (bitn (ins, 8)) then divu w-ins (sopd,

d rn (ins), car (s&addr))

else divs w-ins (sopd, d rn (ins), car (s&addr)) endif endlet endif endlet

else halt (mode-signal, s) endif

Opcode 1000. The OR instruction group includes two instructions OR and DIVU.W/DIVS.W.

Definition: or-group (oplen, ins, s) = if oplen = q then div w-ins (ins, s)

elseif b0p (bitn (ins, 8)) then or-ins1 (oplen, ins, s)

elseif s mode (ins) < 2

    then halt ('sbcd-pack-unpk-unspecified, s)

else or-ins2 (oplen, ins, s) endif

Rotate operations. Rotate left cnt times. len is supposed to be the length of x.

Definition: rol (len, x, cnt) = let n be cnt mod len

in

app (n, tail (x, len − n), head (x, len − n)) endlet

Rotate right cnt times. len is supposed to be the length of x.

Definition: ror (len, x, cnt) = let n be cnt mod len

in

app (len − n, tail (x, n), head (x, n)) endlet

For memory shift/rotate, only memory alterable addressing modes are allowed.

Definition: s&r-addr-modep (ins) = (memory-addr-modep (s mode (ins), s rn (ins))

∧ alterable-addr-modep (s mode (ins), s rn (ins)))

‘i-data’ returns a nonnegative integer. In register shift/rotate, it is the shift/rotate cnt. In ADDQ and SUBQ, it is the immediate data.

Definition: i-data (n) = if n ≃ 0 then 8

else n endif

Definition: sr-cnt (ins, s) = if b0p (bitn (ins, 5)) then i-data (d rn (ins))

else read-dn (b, d rn (ins), s) mod 64 endif

ROL and ROR instructions. We divide the ROL/ROR instruction into a few subinstructions.

Register ROL instruction. The setting of cvznx-flags for ROL.

Definition: rol-c (len, x, cnt) = if cnt = 0 then b0

else let n be cnt mod len in if n ≃ 0 then bcar (x) else bitn (x, len − n) endif endlet endif Definition: rol-z (len, x, cnt) = if x = 0 then b1

else b0 endif

Definition: rol-n (len, x, cnt) = bitn (x, (len − (cnt mod len)) − 1)

Definition: rol-cvznx (len, opd, cnt, ccr) = cvznx (rol-c (len, opd, cnt),

b0,

rol-z (len, opd, cnt), rol-n (len, opd, cnt), ccr-x (ccr))

Definition: rol-effect (len, opd, cnt, ccr) = cons (rol (len, opd, cnt), rol-cvznx (len, opd, cnt, ccr))

Definition: register-rol-ins (oplen, ins, s) = d-mapping (oplen,

rol-effect (oplen, read-dn (oplen, s rn (ins), s), sr-cnt (ins, s), mc-ccr (s)),

s rn (ins),

s)

Register ROR instruction.

Definition: ror-c (len, x, cnt) = if cnt = 0 then b0

else let n be cnt mod len in if n = 0 then bitn (x, len − 1) else bitn (x, n − 1) endif endlet endif

Definition: ror-z (len, opd, cnt) = if opd = 0 then b1

else b0 endif Definition: ror-n (len, x, cnt) = let n be cnt mod len

in

if n ≃ 0 then bitn (x, len − 1) else bitn (x, n − 1) endif endlet

Definition: ror-cvznx (len, opd, cnt, ccr) = cvznx (ror-c (len, opd, cnt),

b0,

ror-z (len, opd, cnt), ror-n (len, opd, cnt), ccr-x (ccr))

Definition: ror-effect (oplen, opd, cnt, ccr) = cons (ror (oplen, opd, cnt), ror-cvznx (oplen, opd, cnt, ccr))

Definition: register-ror-ins (oplen, ins, s) = d-mapping (oplen,

ror-effect (oplen, read-dn (oplen, s rn (ins), s), sr-cnt (ins, s), mc-ccr (s)),

s rn (ins),

s)

Memory ROL instruction. The operand size should be word, and the shift operation is one bit only.

Definition: mem-rol-effect (opd, ccr) = rol-effect (w, opd, 1, ccr)

Definition: mem-rol-ins (ins, s) = if s&r-addr-modep (ins)

then let s&addr be mc-instate (w, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else mapping (w,

mem-rol-effect (operand (w, cdr (s&addr), s), mc-ccr (s)),

s&addr) endif endlet

else halt (mode-signal, s) endif

Memory ROR instruction. The operand size should be word, and the shift operation is one bit only.

Definition: mem-ror-effect (opd, ccr) = ror-effect (w, opd, 1, ccr)

Definition: mem-ror-ins (ins, s) = if s&r-addr-modep (ins)

then let s&addr be mc-instate (w, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else mapping (w,

mem-ror-effect (operand (w, cdr (s&addr), s), mc-ccr (s)),

s&addr) endif endlet

else halt (mode-signal, s) endif

LSL and LSR instructions. We divided the LSL/LSR instruction into several subinstructions.

Register LSL instruction.

Definition: lsl-c (len, opd, cnt) = if cnt = 0 then b0

elseif len < cnt then b0

else bitn (opd, len − cnt) endif

Definition: lsl-z (len, opd, cnt) = if lsl (len, opd, cnt) = 0 then b1

else b0 endif

Definition: lsl-n (len, opd, cnt) = mbit (lsl (len, opd, cnt), len)

Definition: lsl-x (len, opd, cnt, ccr) = if cnt = 0 then ccr-x (ccr)

else lsl-c (len, opd, cnt) endif

Definition: lsl-cvznx (len, opd, cnt, ccr) = cvznx (lsl-c (len, opd, cnt),

b0,

lsl-z (len, opd, cnt), lsl-n (len, opd, cnt), lsl-x (len, opd, cnt, ccr))

Definition: lsl-effect (len, opd, cnt, ccr) = cons (lsl (len, opd, cnt), lsl-cvznx (len, opd, cnt, ccr))

Definition: register-lsl-ins (oplen, ins, s) = d-mapping (oplen,

lsl-effect (oplen, read-dn (oplen, s rn (ins), s), sr-cnt (ins, s), mc-ccr (s)),

s rn (ins),

s)

Register LSR instruction.

Definition: lsr-c (len, opd, cnt) = if cnt = 0 then b0

elseif len < cnt then b0 else bitn (opd, cnt − 1) endif

Definition: lsr-z (len, opd, cnt) = if lsr (opd, cnt) = 0 then b1

else b0 endif

Definition: lsr-n (len, opd, cnt) = mbit (lsr (opd, cnt), len)

Definition: lsr-x (len, opd, cnt, ccr) = if cnt = 0 then ccr-x (ccr)

else lsr-c (len, opd, cnt) endif

Definition: lsr-cvznx (len, opd, cnt, ccr) = cvznx (lsr-c (len, opd, cnt),

b0,

lsr-z (len, opd, cnt), lsr-n (len, opd, cnt), lsr-x (len, opd, cnt, ccr))

Definition: lsr-effect (len, opd, cnt, ccr) = cons (lsr (opd, cnt), lsr-cvznx (len, opd, cnt, ccr))

Definition: register-lsr-ins (oplen, ins, s) = d-mapping (oplen,

lsr-effect (oplen, read-dn (oplen, s rn (ins), s), sr-cnt (ins, s), mc-ccr (s)),

s rn (ins),

s)

Memory LSL instruction.

Definition: mem-lsl-effect (opd, ccr) = lsl-effect (w, opd, 1, ccr)

Definition: mem-lsl-ins (ins, s) = if s&r-addr-modep (ins)

then let s&addr be mc-instate (w, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else mapping (w,

mem-lsl-effect (operand (w, cdr (s&addr), s), mc-ccr (s)),

s&addr) endif endlet

else halt (mode-signal, s) endif

Memory LSR instruction.

Definition: mem-lsr-effect (opd, ccr) = lsr-effect (w, opd, 1, ccr)

Definition: mem-lsr-ins (ins, s) = if s&r-addr-modep (ins)

then let s&addr be mc-instate (w, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else mapping (w,

mem-lsr-effect (operand (w, cdr (s&addr), s), mc-ccr (s)),

s&addr) endif endlet

else halt (mode-signal, s) endif

ASL and ASR instructions.

Register ASL instruction.

Definition: asl-c (len, opd, cnt) = lsl-c (len, opd, cnt)

Definition: asl-v (len, opd, cnt) = if int-rangep (nat-to-int (opd, len), len − cnt) then b0

else b1 endif

Definition: asl-z (len, opd, cnt) = if asl (len, opd, cnt) = 0 then b1

else b0 endif

Definition: asl-n (len, opd, cnt) = mbit (asl (len, opd, cnt), len)

Definition: asl-x (len, opd, cnt, ccr) = if cnt = 0 then ccr-x (ccr)

else asl-c (len, opd, cnt) endif

Definition: asl-cvznx (len, opd, cnt, ccr) = cvznx (asl-c (len, opd, cnt),

asl-v (len, opd, cnt), asl-z (len, opd, cnt), asl-n (len, opd, cnt), asl-x (len, opd, cnt, ccr))

Definition: asl-effect (len, opd, cnt, ccr) = cons (asl (len, opd, cnt), asl-cvznx (len, opd, cnt, ccr))

Definition: register-asl-ins (oplen, ins, s) = d-mapping (oplen,

asl-effect (oplen, read-dn (oplen, s rn (ins), s), sr-cnt (ins, s), mc-ccr (s)),

s rn (ins),

s)

Register ASR instruction.

Definition: asr-c (len, opd, cnt) = if cnt = 0 then b0

elseif cnt < len then bitn (opd, cnt − 1)

else bitn (opd, len − 1) endif Definition: asr-z (len, opd, cnt) = if asr (len, opd, cnt) = 0 then b1

else b0 endif

Definition: asr-n (len, opd, cnt) = mbit (asr (len, opd, cnt), len)

Definition: asr-x (len, opd, cnt, ccr) = if cnt = 0 then ccr-x (ccr)

else asr-c (len, opd, cnt) endif

Definition: asr-cvznx (len, opd, cnt, ccr) = cvznx (asr-c (len, opd, cnt),

b0,

asr-z (len, opd, cnt), asr-n (len, opd, cnt), asr-x (len, opd, cnt, ccr))

Definition: asr-effect (len, opd, cnt, ccr) = cons (asr (len, opd, cnt), asr-cvznx (len, opd, cnt, ccr))

Definition: register-asr-ins (oplen, ins, s) = d-mapping (oplen,

asr-effect (oplen, read-dn (oplen, s rn (ins), s), sr-cnt (ins, s), mc-ccr (s)),

s rn (ins),

s)

Memory ASL instruction.

Definition: mem-asl-effect (opd, ccr) = asl-effect (w, opd, 1, ccr)

Definition: mem-asl-ins (ins, s) = if s&r-addr-modep (ins)

then let s&addr be mc-instate (w, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else mapping (w,

mem-asl-effect (operand (w, cdr (s&addr), s),

mc-ccr (s)),

s&addr) endif endlet

else halt (mode-signal, s) endif

Memory ASR instruction.

Definition: mem-asr-effect (opd, ccr) = asr-effect (w, opd, 1, ccr)

Definition: mem-asr-ins (ins, s) = if s&r-addr-modep (ins)

then let s&addr be mc-instate (w, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else mapping (w,

mem-asr-effect (operand (w, cdr (s&addr), s), mc-ccr (s)),

s&addr) endif endlet

else halt (mode-signal, s) endif

ROXL and ROXR instructions.

‘roxl’ defines the rotate left with extend operation.

Definition: roxl (len, opd, cnt, x) = let temp be x + (2 ∗ opd)

in

bcdr (rol (1 + len, temp, cnt)) endlet

‘roxr’ defines the rotate right with extend operation.

Definition: roxr (len, opd, cnt, x) = let temp be opd + (x ∗ exp (2, len))

in

head (ror (1 + len, temp, cnt), len) endlet

Register ROXL instruction.

Definition: roxl-c (len, opd, cnt, x) = let tmp be cnt mod (1 + len)

in

if tmp = 0 then fix-bit (x)

else bitn (opd, len − tmp) endif endlet Definition: roxl-z (len, opd, cnt, x) = if roxl (len, opd, cnt, x) = 0 then b1

else b0 endif

Definition: roxl-n (len, opd, cnt, x) = bitn (roxl (len, opd, cnt, x), len − 1)

Definition: roxl-cvznx (len, opd, cnt, x) = cvznx (roxl-c (len, opd, cnt, x),

b0,

roxl-z (len, opd, cnt, x), roxl-n (len, opd, cnt, x), roxl-c (len, opd, cnt, x))

Definition: roxl-effect (len, opd, cnt, ccr) = cons (roxl (len, opd, cnt, ccr-x (ccr)), roxl-cvznx (len, opd, cnt, ccr-x (ccr)))

Definition: register-roxl-ins (oplen, ins, s) = d-mapping (oplen,

roxl-effect (oplen, read-dn (oplen, s rn (ins), s), sr-cnt (ins, s), mc-ccr (s)),

s rn (ins),

s)

Register ROXR instruction.

Definition: roxr-c (len, opd, cnt, x) = let tmp be cnt mod (1 + len)

in

if tmp = 0 then fix-bit (x)

else bitn (opd, tmp − 1) endif endlet

Definition: roxr-z (len, opd, cnt, x) = if roxr (len, opd, cnt, x) = 0 then b1

else b0 endif

Definition: roxr-n (len, opd, cnt, x) = bitn (roxr (len, opd, cnt, x), len − 1)

Definition: roxr-cvznx (len, opd, cnt, x) = cvznx (roxr-c (len, opd, cnt, x),

b0,

roxr-z (len, opd, cnt, x), roxr-n (len, opd, cnt, x), roxr-c (len, opd, cnt, x))

Definition: roxr-effect (len, opd, cnt, ccr) = cons (roxr (len, opd, cnt, ccr-x (ccr)), roxr-cvznx (len, opd, cnt, ccr-x (ccr)))

Definition: register-roxr-ins (oplen, ins, s) = d-mapping (oplen,

roxr-effect (oplen, read-dn (oplen, s rn (ins), s), sr-cnt (ins, s), mc-ccr (s)),

s rn (ins),

s)

Memory ROXL instruction.

Definition: mem-roxl-effect (opd, ccr) = roxl-effect (w, opd, 1, ccr)

Definition: mem-roxl-ins (ins, s) = if s&r-addr-modep (ins)

then let s&addr be mc-instate (w, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else mapping (w,

mem-roxl-effect (operand (w, cdr (s&addr), s),

mc-ccr (s)),

s&addr) endif endlet

else halt (mode-signal, s) endif

Memory ROXR instruction.

Definition: mem-roxr-effect (opd, ccr) = roxr-effect (w, opd, 1, ccr)

Definition: mem-roxr-ins (ins, s) = if s&r-addr-modep (ins)

then let s&addr be mc-instate (w, ins, s)

in

if mc-haltp (car (s&addr)) then car (s&addr)

else mapping (w,

mem-roxr-effect (operand (w, cdr (s&addr), s),

mc-ccr (s)),

s&addr) endif endlet

else halt (mode-signal, s) endif

Memory shift/rotate.

Definition: memory-shift-rotate (ins, s) = if b0p (bitn (ins, 10))

then if b0p (bitn (ins, 9))

then if b0p (bitn (ins, 8)) then mem-asr-ins (ins, s)

else mem-asl-ins (ins, s) endif elseif b0p (bitn (ins, 8)) then mem-lsr-ins (ins, s) else mem-lsl-ins (ins, s) endif

elseif b0p (bitn (ins, 9)) then if b0p (bitn (ins, 8)) then mem-roxr-ins (ins, s)

else mem-roxl-ins (ins, s) endif elseif b0p (bitn (ins, 8)) then mem-ror-ins (ins, s) else mem-rol-ins (ins, s) endif

Register shift/rotate.

Definition: register-shift-rotate (oplen, ins, s) = if b0p (bitn (ins, 4))

then if b0p (bitn (ins, 3))

then if b0p (bitn (ins, 8)) then register-asr-ins (oplen, ins, s)

else register-asl-ins (oplen, ins, s) endif elseif b0p (bitn (ins, 8)) then register-lsr-ins (oplen, ins, s) else register-lsl-ins (oplen, ins, s) endif

elseif b0p (bitn (ins, 3)) then if b0p (bitn (ins, 8)) then register-roxr-ins (oplen, ins, s)

else register-roxl-ins (oplen, ins, s) endif elseif b0p (bitn (ins, 8)) then register-ror-ins (oplen, ins, s) else register-rol-ins (oplen, ins, s) endif

The bit field instruction group consists of BFxxx instructions. All of these instructions are new in the MC68020. Note that bit 15 in the extension word has to be 0!

Definition: bf-subgroup (ins, s) = halt ('i-will-do-it-later, s)

Opcode 1110. The shift/rotate instruction group includes the ASL/ASR, LSL/LSR, ROL/ROR, ROXL/RORL, BFTST, BFEXTU, BFCHG, BFEXTS, BFCLR, BFFFO, BFSET, and BFINS instructions. But it actually divides into many varieties of these instructions.

Definition: s&r-group (ins, s) = if op-len (ins) = q

then if b0p (bitn (ins, 11)) then memory-shift-rotate (ins, s)

else bf-subgroup (ins, s) endif else register-shift-rotate (op-len (ins), ins, s) endif

MOVE instruction.

Definition: move-addr-modep (oplen, ins) = (addr-modep (s mode (ins), s rn (ins))

∧ data-addr-modep (d mode (ins), d rn (ins)) ∧ alterable-addr-modep (d mode (ins), d rn (ins)) ∧ (¬ byte-an-direct-modep (oplen, s mode (ins))))

Definition: move-z (oplen, sopd) = if head (sopd, oplen) = 0 then b1

else b0 endif

Definition: move-n (oplen, sopd) = mbit (sopd, oplen)

The definition of cvznx-flags of MOVE instruction. It is also used in TST and TAS instructions.

Definition: move-cvznx (oplen, sopd, ccr) = cvznx (b0, b0, move-z (oplen, sopd), move-n (oplen, sopd), ccr-x (ccr))

Definition: move-effect (oplen, sopd, ccr) = cons (sopd, move-cvznx (oplen, sopd, ccr))

Definition: move-mapping (sopd, oplen, ins, s) = let s&addr be effec-addr (oplen, d mode (ins), d rn (ins), s)

in

if mc-haltp (car (s&addr)) then car (s&addr)

else mapping (oplen, move-effect (oplen, sopd, mc-ccr (s)), s&addr) endif endlet

Definition: move-ins (oplen, ins, s) = if move-addr-modep (oplen, ins)

then let s&addr be mc-instate (oplen, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else move-mapping (operand (oplen, cdr (s&addr), s),

oplen, ins, car (s&addr)) endif endlet

else halt (mode-signal, s) endif

MOVEA instruction. MOVEA differs from MOVE in several ways: ccr is not affected and word operation is sign-extended. Therefore, we define it separately.

Definition: movea-addr-modep (ins) = addr-modep (s mode (ins), s rn (ins))

Definition: movea-ins (oplen, ins, s) = if movea-addr-modep (ins)

then let s&addr be mc-instate (oplen, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else write-an (l,

ext (oplen, operand (oplen, cdr (s&addr), s), l), d rn (ins), car (s&addr)) endif endlet

else halt (mode-signal, s) endif

Opcode 0010 and 0011. The following definition is defined to distinguish MOVE and MOVEA instructions. This definition is only for word and long operations.

Definition: move-group (oplen, ins, s) = if d mode (ins) = 1 then movea-ins (oplen, ins, s)

else move-ins (oplen, ins, s) endif

LEA instruction.

Definition: lea-addr-modep (ins) = control-addr-modep (s mode (ins), s rn (ins))

‘lea-ins’ calls ‘effec-addr’, instead of ‘mc-instate’, since the effective address is JUST what we need. Notice that LEA and PEA only deal with memory address. The address direct modes are not allowed. Operation size: long.

Definition: lea-ins (smode, ins, s) = if lea-addr-modep (ins)

then let s&addr be effec-addr (l, smode, s rn (ins), s) in if mc-haltp (car (s&addr)) then car (s&addr) else write-an (l, cddr (s&addr), d rn (ins), car (s&addr)) endif endlet

else halt (mode-signal, s) endif

EXTB instruction. Sign-extend a byte to a longword. It is new in the MC68020.

Definition: ext-z (oplen, opd, size) = if ext (oplen, opd, size) = 0 then b1

else b0 endif

Definition: ext-n (oplen, opd, size) = mbit (ext (oplen, opd, size), size)

Definition: ext-cvznx (oplen, opd, size, ccr) = cvznx (b0, b0, ext-z (oplen, opd, size), ext-n (oplen, opd, size), ccr-x (ccr))

Definition: ext-effect (oplen, opd, size, ccr) = cons (ext (oplen, opd, size), ext-cvznx (oplen, opd, size, ccr))

Definition: extb-ins (ins, s) = d-mapping (l,

ext-effect (b, read-dn (b, s rn (ins), s), l, mc-ccr (s)), s rn (ins), s)

The LEA instruction subgroup includes LEA and EXTB instructions.

Definition: lea-subgroup (ins, s) = if s mode (ins) = 0

then if bits (ins, 9, 11) = 4 then extb-ins (ins, s) else halt (reserved-signal, s) endif

else lea-ins (s mode (ins), ins, s) endif

CLR instruction.

Definition: clr-addr-modep (ins) = (data-addr-modep (s mode (ins), s rn (ins))

∧ alterable-addr-modep (s mode (ins), s rn (ins)))

Definition: clr-cvznx (ccr) = cvznx (b0, b0, b1, b0, ccr-x (ccr))

Definition: clr-effect (ccr) = cons (0, clr-cvznx (ccr))

Definition: clr-ins (oplen, ins, s) = if clr-addr-modep (ins)

then let s&addr be effec-addr (oplen, s mode (ins), s rn (ins), s) in if mc-haltp (car (s&addr)) then car (s&addr) else mapping (oplen, clr-effect (mc-ccr (s)), s&addr) endif endlet

else halt (mode-signal, s) endif

MOVE from CCR instruction.

Definition: move-from-ccr-addr-modep (ins) = (data-addr-modep (s mode (ins), s rn (ins))

∧ alterable-addr-modep (s mode (ins), s rn (ins)))

This instruction has no effect on CCR. Therefore, the original CCR is copied for the updating. This is intended to have a uniform treatment for cvznx-flags. It makes it possible to use one theorem to characterize the action.

Definition: move-from-ccr-effect (ccr) = cons (ccr, ccr)

Definition: move-from-ccr-ins (ins, s) = if move-from-ccr-addr-modep (ins)

then let s&addr be mc-instate (w, ins, s)

in if mc-haltp (car (s&addr)) then car (s&addr) else mapping (w,

move-from-ccr-effect (mc-ccr (s)), s&addr) endif endlet

else halt (mode-signal, s) endif

The CLR instruction subgroup includes CLR and MOVE from CCR instructions.

Definition: clr-subgroup (ins, s) = if op-len (ins) = q then move-from-ccr-ins (ins, s)

else clr-ins (op-len (ins), ins, s) endif

NEGX instruction.

Definition: negx-addr-modep (ins) = (data-addr-modep (s mode (ins), s rn (ins))

∧ alterable-addr-modep (s mode (ins), s rn (ins)))

Definition: negx-ins (oplen, ins, s) = if negx-addr-modep (ins)

then let s&addr be mc-instate (oplen, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else mapping (oplen,

subx-effect (oplen,

operand (oplen, cdr (s&addr), s),

                               0,

mc-ccr (s)),

s&addr) endif endlet

else halt (mode-signal, s) endif

The NEGX instruction subgroup includes the NEGX instruction. Detect MOVE from SR.

Definition: negx-subgroup (ins, s) = if op-len (ins) = q then halt ('move-from-sr-privileged, s)

else negx-ins (op-len (ins), ins, s) endif

NEG instruction.

Definition: neg-addr-modep (ins) = (data-addr-modep (s mode (ins), s rn (ins))

∧ alterable-addr-modep (s mode (ins), s rn (ins)))

Definition: neg-ins (oplen, ins, s) = if neg-addr-modep (ins)

then let s&addr be mc-instate (oplen, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else mapping (oplen,

sub-effect (oplen, operand (oplen, cdr (s&addr), s), 0), s&addr) endif endlet

else halt (mode-signal, s) endif

MOVE to CCR instruction.

Definition: move-to-ccr-addr-modep (ins) = data-addr-modep (s mode (ins), s rn (ins))

Definition: move-to-ccr-ins (ins, s) = if move-to-ccr-addr-modep (ins)

then let s&addr be mc-instate (w, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else update-ccr (head (operand (w, cdr (s&addr), s), b), car (s&addr)) endif endlet

else halt (mode-signal, s) endif

The NEG instruction subgroup includes NEG and MOVE to CCR instructions.

Definition: neg-subgroup (ins, s) = if op-len (ins) = q then move-to-ccr-ins (ins, s)

else neg-ins (op-len (ins), ins, s) endif

PEA instruction.

Definition: pea-addr-modep (ins) = control-addr-modep (s mode (ins), s rn (ins))

Definition: pea-ins (smode, ins, s) = if pea-addr-modep (ins)

then let s&addr be effec-addr (l, smode, s rn (ins), s) in if mc-haltp (car (s&addr)) then car (s&addr) else push-sp (lsz, cddr (s&addr), car (s&addr)) endif endlet

else halt (mode-signal, s) endif

SWAP instruction.

Definition: swap-z (opd) = if fix (opd) = 0 then b1

else b0 endif

Definition: swap-n (opd) = bitn (opd, 15)

Definition: swap-cvznx (opd, ccr) = cvznx (b0, b0, swap-z (opd), swap-n (opd), ccr-x (ccr))

Definition: swap-effect (opd, ccr) = cons (app (w, tail (opd, w), head (opd, w)), swap-cvznx (opd, ccr))

Definition: swap-ins (ins, s) = d-mapping (l, swap-effect (read-dn (l, s rn (ins), s), mc-ccr (s)), s rn (ins), s)

The PEA instruction subgroup includes PEA and SWAP. Detect BKPT.

Definition: pea-subgroup (ins, s) = if s mode (ins) < 2

then if s mode (ins) = 0 then swap-ins (ins, s)

         else halt ('bkpt-unspecified, s) endif

else pea-ins (s mode (ins), ins, s) endif

EXT instruction.

Definition: ext-ins (ins, s) = if b0p (bitn (ins, 6))

then d-mapping (w, ext-effect (b, read-dn (b, s rn (ins), s), w, mc-ccr (s)), s rn (ins),

s)

else d-mapping (l, ext-effect (w, read-dn (w, s rn (ins), s), l, mc-ccr (s)), s rn (ins),

s) endif

MOVEM Rn to EA instruction. A pair of functions for multiple read/write on memory.

Definition: readm-mem (opsz, addr, mem, n) = if n ≃ 0 then nil

else cons (read-mem (addr, mem, opsz), readm-mem (opsz, add (l, addr, opsz), mem, n − 1)) endif

Definition: writem-mem (opsz, vlst, addr, mem) = if listp (vlst)

then writem-mem (opsz, cdr (vlst), add (l, addr, opsz), write-mem (car (vlst), addr, mem, opsz))

else mem endif

A pair of functions for multiple read/write on the register file.

Definition: readm-rn (oplen, rnlst, rfile) = if listp (rnlst)

then cons (read-rn (oplen, car (rnlst), rfile),

readm-rn (oplen, cdr (rnlst), rfile))

else nil endif

Definition: writem-rn (oplen, vlst, rnlst, rfile) = if listp (rnlst)

then writem-rn (oplen, cdr (vlst), cdr (rnlst), write-rn (l, ext (oplen, car (vlst), l), car (rnlst), rfile))

else rfile endif

A list of the number of registers to be moved.

Definition: movem-rnlst (mask, i)

= if mask ≃ 0 then nil elseif b0p (bcar (mask)) then movem-rnlst (bcdr (mask), 1 + i) else cons (i, movem-rnlst (bcdr (mask), 1 + i)) endif

Definition: movem-len (mask) = if mask ≃ 0 then 0

elseif b0p (bcar (mask)) then movem-len (bcdr (mask))

else 1 + movem-len (bcdr (mask)) endif

Definition: writemp (mask, oplen, addr, mem) = write-memp (addr, mem, op-sz (oplen) ∗ movem-len (mask))

In the case of predecrement, there are a few things we have to treat separately. The order of the mask is the reverse of the other cases.

Definition: movem-pre-rnlst (mask, i, lst) = if mask ≃ 0 then lst

elseif b0p (bcar (mask)) then movem-pre-rnlst (bcdr (mask), i − 1, lst) else movem-pre-rnlst (bcdr (mask), i − 1, cons (i, lst)) endif

The reason we modify the address register rn here is that if it is also moved to memory, it is changed before it is moved. This function returns a ‘cons’: the first element is an intermediate state with the address register rn changed, the second element is the starting memory address to move those registers.

Definition: movem-predec (mask, oplen, rn, s) = let addr be read-an (l, rn, s)

in

cons (write-an (l, pre-effect (oplen, rn, addr), rn, s), cons ('m, sub (l, op-sz (oplen) ∗ movem-len (mask), addr))) endlet

The addressing modes are control alterable plus predecrement. We deal with -(An) separately.

Definition: movem-rn-ea-addr-modep (ins) = (alterable-addr-modep (s mode (ins), s rn (ins))

∧ control-addr-modep (s mode (ins), s rn (ins)))

Note in the predecrement mode, if mask = 0, there is no action on An.

Definition: movem-rn-ea-ins (mask, oplen, ins, s)

= if predec-modep (s mode (ins))

then let s&addr be movem-predec (mask, oplen, s rn (ins), s) in if writemp (mask, oplen, cddr (s&addr), mc-mem (s)) then write-an (l,

cddr (s&addr), s rn (ins), update-mem (writem-mem (op-sz (oplen),

readm-rn (oplen,

movem-pre-rnlst (mask,

                                                           15,

nil),

mc-rfile (car (s&addr))),

cddr (s&addr), mc-mem (s)),

car (s&addr)))

else halt (write-signal, s) endif endlet elseif movem-rn-ea-addr-modep (ins) then let s&addr be effec-addr (oplen, s mode (ins), s rn (ins), s)

in if mc-haltp (car (s&addr)) then car (s&addr) elseif writemp (mask, oplen, cddr (s&addr), mc-mem (s)) then update-mem (writem-mem (op-sz (oplen),

readm-rn (oplen, movem-rnlst (mask, 0), mc-rfile (s)),

cddr (s&addr), mc-mem (s)),

car (s&addr))

else halt (write-signal, s) endif endlet else halt (mode-signal, s) endif

The EXT instruction subgroup includes EXT and MOVEM Rn to EA.

Definition: ext-subgroup (ins, s) = if s mode (ins) = 0 then ext-ins (ins, s)

elseif pc-word-readp (mc-pc (s), mc-mem (s)) then movem-rn-ea-ins (pc-word-read (mc-pc (s), mc-mem (s)),

if b0p (bitn (ins, 6)) then w

else l endif,

ins,

update-pc (add (l, mc-pc (s), wsz), s))

else halt (pc-signal, s) endif

TST instruction. MC68020 and MC68000 differ about addressing modes.

Definition: tst-addr-modep (oplen, ins) = if oplen = b then data-addr-modep (s mode (ins), s rn (ins))

else addr-modep (s mode (ins), s rn (ins)) endif

Definition: tst-ins (oplen, ins, s) = if tst-addr-modep (oplen, ins)

then let s&addr be mc-instate (oplen, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else update-ccr (move-cvznx (oplen,

operand (oplen, cdr (s&addr), s),

mc-ccr (s)),

car (s&addr)) endif endlet

else halt (mode-signal, s) endif

TAS instruction. It is usually used as a multiprocessor operation.

Definition: tas-addr-modep (ins) = (data-addr-modep (s mode (ins), s rn (ins))

∧ alterable-addr-modep (s mode (ins), s rn (ins)))

Definition: tas-effect (opd, ccr) = cons (setn (opd, 7, b1), move-cvznx (b, opd, ccr))

The opsize of the TAS instruction is byte.

Definition: tas-ins (ins, s) = if tas-addr-modep (ins)

then let s&addr be mc-instate (b, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else mapping (b,

tas-effect (operand (b, cdr (s&addr), s),

mc-ccr (s)),

s&addr) endif endlet

else halt (mode-signal, s) endif

The TST instruction subgroup includes TAS and TST. Detect ILLEGAL instruction.

Definition: tst-subgroup (ins, s) = if op-len (ins) = q

then if head (ins, 6) = 60 then halt ('illegal-unspecified, s)

else tas-ins (ins, s) endif else tst-ins (op-len (ins), ins, s) endif

DIVS L instructions. D / S → D. 32/32 → 32q, 32/32 → 32r:32q. The order of write-dn: remainder first, and then quotient. The overflow happens only when the dopd is −2^{31} and sopd is −1.

Definition: divsl l (sopd, dopd, dq, dr, s) = if b0p (divs-v (l, sopd, l, dopd, l))

then let q be iquot (l, sopd, l, dopd, l),

r be irem (l, sopd, l, dopd, l) in update-ccr (divs-cvznx (l, sopd, l, dopd, l, mc-ccr (s)),

write-dn (l, q, dq, write-dn (l, r, dr, s))) endlet

else halt ('divs-overflow, update-ccr (set-v (b1, mc-ccr (s)), s)) endif

64/32 → 32r:32q.

Definition: divs l (sopd, dopd low, dq, dr, s) = let dopd be app (l, dopd low, read-dn (l, dr, s))

in

if b0p (divs-v (l, sopd, l, dopd, q))

then let q be iquot (l, sopd, l, dopd, q),

r be irem (l, sopd, l, dopd, q) in update-ccr (divs-cvznx (l, sopd, l, dopd, q, mc-ccr (s)),

write-dn (l, q, dq, write-dn (l, r, dr, s))) endlet

    else halt ('divs-overflow,

update-ccr (set-v (b1, mc-ccr (s)), s)) endif endlet

DIVU L instructions. D / S → D. 32/32 → 32q, 32/32 → 32r:32q. In this case, overflow never happens! It is justified by the event quotient-nat-rangep.

Definition: divul l (sopd, dopd, dq, dr, s) = let q be quot (l, sopd, dopd),

r be rem (l, sopd, dopd) in update-ccr (divu-cvznx (l, sopd, dopd, mc-ccr (s)),

write-dn (l, q, dq, write-dn (l, r, dr, s))) endlet

64/32 → 32r:32q.

Definition: divu l (sopd, dopd low, dq, dr, s) = let dopd be app (l, dopd low, read-dn (l, dr, s))

in

if b0p (divu-v (l, sopd, dopd))

then let q be quot (l, sopd, dopd),

r be rem (l, sopd, dopd) in update-ccr (divu-cvznx (l, sopd, dopd, mc-ccr (s)),

write-dn (l, q, dq, write-dn (l, r, dr, s))) endlet

    else halt ('divu-overflow,

update-ccr (set-v (b1, mc-ccr (s)), s)) endif endlet

Definition: dq (word) = bits (word, 12, 14)

Definition: dr (word) = bits (word, 0, 2)

Definition: div l-ins (sopd, word, s) = let dopd low be read-dn (l, dq (word), s)

in

if b0p (bitn (word, 11))

then if nat-to-uint (sopd) = 0

         then halt ('trap-exception, s)

elseif b0p (bitn (word, 10))

then divul l (sopd, dopd low, dq (word), dr (word), s) else divu l (sopd, dopd low, dq (word), dr (word), s) endif

elseif nat-to-int (sopd, l) = 0

    then halt ('trap-exception, s)

elseif b0p (bitn (word, 10))

then divsl l (sopd, dopd low, dq (word), dr (word), s)

else divs l (sopd, dopd low, dq (word), dr (word), s) endif endlet

MULS/MULU-long instructions. S * D → D.

Definition: mulu l dl (sopd, dopd, dl, s) = update-ccr (mulu-cvznx (l, sopd, dopd, l, mc-ccr (s)),

write-dn (l, mulu (l, sopd, dopd, l), dl, s))

Definition: mulu l dldh (sopd, dopd, dl, dh, s) = if dl = dh then halt ('mc-undefined, s)

else update-ccr (mulu-cvznx (q, sopd, dopd, l, mc-ccr (s)), write-dn (l,

tail (mulu (q, sopd, dopd, l), l), dh, write-dn (l,

head (mulu (q, sopd, dopd, l), l), dl, s))) endif

Definition: muls l dl (sopd, dopd, dl, s) = update-ccr (muls-cvznx (l, sopd, dopd, l, mc-ccr (s)),

write-dn (l, muls (l, sopd, dopd, l), dl, s))

Definition: muls l dldh (sopd, dopd, dl, dh, s) = if dl = dh then halt ('mc-undefined, s)

else update-ccr (muls-cvznx (q, sopd, dopd, l, mc-ccr (s)),

write-dn (l, tail (muls (q, sopd, dopd, l), l), dh, write-dn (l,

head (muls (q, sopd, dopd, l), l), dl, s))) endif

Definition: dl (word) = bits (word, 12, 14)

Definition: dh (word) = bits (word, 0, 2)

Definition: mul l-ins (sopd, word, s) = let dopd be read-dn (l, dl (word), s)

in

if b0p (bitn (word, 11))

then if b0p (bitn (word, 10))

then mulu l dl (sopd, dopd, dl (word), s)

else mulu l dldh (sopd, dopd, dl (word), dh (word), s) endif elseif b0p (bitn (word, 10)) then muls l dl (sopd, dopd, dl (word), s) else muls l dldh (sopd, dopd, dl (word), dh (word), s) endif endlet

Definition: mul-div l-ins (word, ins, s) = if b0p (bitn (word, 15)) ∧ (bits (word, 3, 9) = 0)

then if mul&div-addr-modep (ins) then let s&addr be mc-instate (l, ins, s)

in

if mc-haltp (car (s&addr)) then car (s&addr) else let sopd be operand (l,

cdr (s&addr), car (s&addr))

in

if b0p (bitn (ins, 6)) then mul l-ins (sopd,

word,

car (s&addr))

else div l-ins (sopd, word, car (s&addr)) endif endlet endif endlet

else halt (mode-signal, s) endif else halt (reserved-signal, s) endif

MOVEM EA to RN instruction. The addressing modes are control plus postincrement. We deal with (An)+ separately.

Definition: movem-ea-rn-addr-modep (ins) = control-addr-modep (s mode (ins), s rn (ins))

Definition: readmp (mask, oplen, addr, mem) = read-memp (addr, mem, op-sz (oplen) ∗ movem-len (mask))

In the mode of postincrement, if the address register is also loaded from the memory, the value of it upon completion of this instruction has no difference from the other modes.

Definition: movem-ea-rn-ins (mask, oplen, ins, s) = if postinc-modep (s mode (ins))

then let addr be read-an (l, s rn (ins), s) in if readmp (mask, oplen, addr, mc-mem (s)) then write-an (l,

add (l, addr, op-sz (oplen)

∗ movem-len (mask)),

s rn (ins),

update-rfile (writem-rn (oplen,

readm-mem (op-sz (oplen), addr, mc-mem (s),

movem-len (mask)),

movem-rnlst (mask, 0), mc-rfile (s)),

s))

else halt (read-signal, s) endif endlet elseif movem-ea-rn-addr-modep (ins) then let s&addr be effec-addr (oplen, s mode (ins), s rn (ins), s)

in if mc-haltp (car (s&addr)) then car (s&addr) elseif readmp (mask, oplen, cddr (s&addr), mc-mem (s)) then update-rfile (writem-rn (oplen,

readm-mem (op-sz (oplen), cddr (s&addr), mc-mem (s), movem-len (mask)),

movem-rnlst (mask, 0), mc-rfile (s)),

car (s&addr))

else halt (read-signal, s) endif endlet else halt (mode-signal, s) endif

The MOVEM-EA-RN-SUBGROUP includes MOVEM, DIVS/U and MULS/U instructions.

Definition: movem-ea-rn-subgroup (ins, s) = if pc-word-readp (mc-pc (s), mc-mem (s))

then let word be pc-word-read (mc-pc (s), mc-mem (s)) in if b0p (bitn (ins, 7)) then mul-div l-ins (word,

ins,

update-pc (add (l, mc-pc (s), wsz), s))

else movem-ea-rn-ins (word, if b0p (bitn (ins, 6)) then w else l endif, ins, update-pc (add (l, mc-pc (s), wsz), s)) endif endlet

else halt (pc-signal, s) endif

LINK-long instruction. LINK and UNLK are somewhat complicated. When sp is used as an, the execution order seems different from a simple instantiation.

Definition: link-mapping (an, disp, s) = let sp be sub (l, lsz, read-sp (s))

in

if write-memp (sp, mc-mem (s), lsz)

then update-mem (write-mem (read-an (l, an, s), sp, mc-mem (s), lsz),

write-sp (add (l, sp, disp), write-an (l, sp, an, s)))

else halt (write-signal, s) endif endlet

Definition: link l-ins (an, s) = if pc-long-readp (mc-pc (s), mc-mem (s))

then link-mapping (an, pc-long-read (mc-pc (s), mc-mem (s)), update-pc (add (l, mc-pc (s), lsz), s))

else halt (pc-signal, s) endif

LINK-word instruction.

Definition: link w-ins (an, s) = if pc-word-readp (mc-pc (s), mc-mem (s))

then link-mapping (an, ext (w, pc-word-read (mc-pc (s), mc-mem (s)), l), update-pc (add (l, mc-pc (s), wsz), s))

else halt (pc-signal, s) endif

UNLK instruction.

Definition: unlk-ins (an, s) = let sp be read-an (l, an, s)

in

if long-readp (sp, mc-mem (s))

then write-an (l, long-read (sp, mc-mem (s)), an, write-sp (add (l, sp, lsz), s))

else halt (read-signal, s) endif endlet

The unlk instruction subgroup includes UNLK and LINK-word instructions. detect trap instruction.

Definition: unlk-subgroup (ins, s) = if b0p (bitn (ins, 4)) then halt ('trap-unspecified, s)

elseif b0p (bitn (ins, 3)) then link w-ins (s rn (ins), s)

else unlk-ins (s rn (ins), s) endif

NOP instruction. The machine state, except the program counter, is not affected. But we have already incremented pc when we read the first word of the current instruction. Therefore, we simply return s.

Definition: nop-ins (s) = s

RTD instruction.

Definition: rtd-mapping (sp, disp, s) = if long-readp (sp, mc-mem (s))

then let new-sp be add (l, add (l, sp, lsz), ext (w, disp, l)) in update-pc (long-read (sp, mc-mem (s)), write-sp (new-sp, s)) endlet

else halt (read-signal, s) endif

Definition: rtd-ins (s) = if pc-word-readp (mc-pc (s), mc-mem (s))

then rtd-mapping (read-sp (s), pc-word-read (mc-pc (s), mc-mem (s)), s) else halt (pc-signal, s) endif

RTS instruction. Notice that disp is 0.

Definition: rts-ins (s) = rtd-mapping (read-sp (s), 0, s)

RTR instruction. Notice that disp is 0.

Definition: rtr-ins (s) = let sp be read-sp (s)

in

if word-readp (sp, mc-mem (s)) then rtd-mapping (add (l, sp, wsz),

                    0,

update-ccr (word-read (sp, mc-mem (s)), s))

else halt (read-signal, s) endif endlet

TRAPV instruction. If the overflow is set, we simply halt the machine. Otherwise, nop. To handle this instruction in verifications, we intend to prove the overflow is not set, and hence the machine performs nop.

Definition: bvs (v) = fix-bit (v)

Definition: trapv-ins (s) = if b1p (bvs (ccr-v (mc-ccr (s)))) then halt ('trapv-exception, s)

else s endif

The NOP instruction subgroup includes NOP, RTD, RTS, and RTR instructions. Detect RESET, STOP, RTE, and TRAPV.

Definition: nop-subgroup (ins, s) = if b0p (bitn (ins, 2))

then if b0p (bitn (ins, 1))

then if b0p (bitn (ins, 0)) then halt ('reset-privileged, s)

else nop-ins (s) endif elseif b0p (bitn (ins, 0)) then halt ('stop-privileged, s) else halt ('rte-privileged, s) endif

elseif b0p (bitn (ins, 1))

then if b0p (bitn (ins, 0)) then rtd-ins (s)

else rts-ins (s) endif elseif b0p (bitn (ins, 0)) then trapv-ins (s) else rtr-ins (s) endif

JMP instruction. The JMP instruction is unsized. To calculate the effective address by effec-addr, one can arbitrarily supply the operand length. Note that the addr-predec, addr-postinc and immediate are not allowed.

Definition: jmp-addr-modep (ins) = control-addr-modep (s mode (ins), s rn (ins))

JMP does not affect CCR!

Definition: jmp-mapping (addr, s) = if mc-haltp (s) then s

else update-pc (addr, s) endif

Definition: jmp-ins (ins, s) = if jmp-addr-modep (ins)

then let s&addr be effec-addr (l, s mode (ins), s rn (ins), s) in jmp-mapping (cddr (s&addr), car (s&addr)) endlet

else halt (mode-signal, s) endif

JSR instruction. JSR does not affect CCR!

Definition: jsr-addr-modep (ins) = control-addr-modep (s mode (ins), s rn (ins))

Definition: jsr-ins (ins, s) = if jsr-addr-modep (ins) then let s&addr be effec-addr (l, s mode (ins), s rn (ins), s)

in

if mc-haltp (car (s&addr)) then car (s&addr) else jmp-mapping (cddr (s&addr),

push-sp (lsz, mc-pc (car (s&addr)), car (s&addr))) endif endlet

else halt (mode-signal, s) endif

NOT instruction.

Definition: not-addr-modep (ins) = (data-addr-modep (s mode (ins), s rn (ins))

∧ alterable-addr-modep (s mode (ins), s rn (ins)))

Definition: not-z (oplen, opd) = if lognot (oplen, opd) = 0 then b1

else b0 endif

Definition: not-n (oplen, opd) = mbit (lognot (oplen, opd), oplen)

Definition: not-cvznx (oplen, opd, ccr) = cvznx (b0, b0, not-z (oplen, opd), not-n (oplen, opd), ccr-x (ccr))

Definition: not-effect (oplen, opd, ccr) = cons (lognot (oplen, opd), not-cvznx (oplen, opd, ccr))

Definition: not-ins (oplen, ins, s) = if not-addr-modep (ins)

then let s&addr be mc-instate (oplen, ins, s)

in

if mc-haltp (car (s&addr)) then car (s&addr) else mapping (oplen,

not-effect (oplen, operand (oplen, cdr (s&addr), s), mc-ccr (s)),

s&addr) endif endlet

else halt (mode-signal, s) endif

Definition: not-subgroup (ins, s) = if op-len (ins) = q then halt ('move-to-sr-privileged, s)

else not-ins (op-len (ins), ins, s) endif

Opcode 0100. The miscellaneous instruction group includes LEA, CLR, MOVE from CCR, NEG, MOVE to CCR, NOT, SWAP, PEA, EXT-word, MOVEM to EA, TST, TAS, MOVEM to RN, LINK, UNLK, NOP, RTD, RTS, RTR, JSR, JMP.

Definition: misc-group (ins, s) = if b0p (bitn (ins, 8))

then if b0p (bitn (ins, 11))

then if b0p (bitn (ins, 10))

then if b0p (bitn (ins, 9)) then negx-subgroup (ins, s)

else clr-subgroup (ins, s) endif elseif b0p (bitn (ins, 9)) then neg-subgroup (ins, s) else not-subgroup (ins, s) endif

elseif b0p (bitn (ins, 10)) then if b0p (bitn (ins, 9))

then if b0p (bitn (ins, 7))

then if b0p (bitn (ins, 6))

then if b0p (bitn (ins, 5))

∧ b0p (bitn (ins, 4)) ∧ b1p (bitn (ins, 3)) then link l-ins (s rn (ins), s)

               else halt ('nbcd-unspecified, s) endif

else pea-subgroup (ins, s) endif else ext-subgroup (ins, s) endif

else tst-subgroup (ins, s) endif elseif b0p (bitn (ins, 9)) then movem-ea-rn-subgroup (ins, s) elseif b0p (bitn (ins, 7)) then if b0p (bitn (ins, 6)) then halt (reserved-signal, s)

elseif b0p (bitn (ins, 5)) then unlk-subgroup (ins, s) elseif b0p (bitn (ins, 4))

then halt ('move-usp-unspecified, s)

elseif b0p (bitn (ins, 3)) then nop-subgroup (ins, s)

else halt ('movec-unspecified, s) endif

elseif b0p (bitn (ins, 6)) then jsr-ins (ins, s) else jmp-ins (ins, s) endif

elseif b1p (bitn (ins, 6)) ∧ b1p (bitn (ins, 7)) then lea-subgroup (ins, s) else halt ('chk-unspecified, s) endif

Some useful definitions for Bcc and Scc instruction groups. Notice that bvs has been defined in TRAPV.

Definition: bcs (c) = fix-bit (c)

Definition: beq (z) = fix-bit (z)

Definition: bmi (n) = fix-bit (n)

Definition: ble (v, z, n) = b-or (z, b-or (b-and (n, b-not (v)), b-and (b-not (n), v)))

Definition: bgt (v, z, n) = b-and (b-or (b-and (n, v), b-and (b-not (n), b-not (v))), b-not (z))

Definition: blt (v, n) = b-or (b-and (n, b-not (v)), b-and (b-not (n), v))

Definition: bge (v, n) = b-or (b-and (n, v), b-and (b-not (n), b-not (v)))

Definition: bls (c, z) = b-or (c, z)

Definition: bhi (c, z) = b-and (b-not (c), b-not (z))

Definition: branch-cc (cond, ccr) = if cond < 8

then if cond < 4

then if cond < 2

then if cond = 0 then b1 else b0 endif

elseif cond = 2 then bhi (ccr-c (ccr), ccr-z (ccr)) else bls (ccr-c (ccr), ccr-z (ccr)) endif

elseif cond < 6

then if cond = 4 then b-not (bcs (ccr-c (ccr)))

else bcs (ccr-c (ccr)) endif elseif cond = 6 then b-not (beq (ccr-z (ccr))) else beq (ccr-z (ccr)) endif

elseif cond < 12 then if cond < 10

then if cond = 8 then b-not (bvs (ccr-v (ccr)))

else bvs (ccr-v (ccr)) endif elseif cond = 10 then b-not (bmi (ccr-n (ccr))) else bmi (ccr-n (ccr)) endif

elseif cond < 14

then if cond = 12 then bge (ccr-v (ccr), ccr-n (ccr)) else blt (ccr-v (ccr), ccr-n (ccr)) endif

elseif cond = 14 then bgt (ccr-v (ccr), ccr-z (ccr), ccr-n (ccr))

else ble (ccr-v (ccr), ccr-z (ccr), ccr-n (ccr)) endif

BSR instruction.

Definition: bsr-ins (pc, disp, s) = push-sp (lsz, pc, update-pc (add (l, mc-pc (s), disp), s))

Bcc and BRA instructions are specified as follows. The BSR instruction needs some auxiliary functions to specify it. We define BRA and Bcc together. Since 0000 is always true.

Definition: bcc-ra-sr (pc, cond, disp, s) = if cond = 0 then update-pc (add (l, mc-pc (s), disp), s)

elseif cond = 1 then bsr-ins (pc, disp, s)

elseif b0p (branch-cc (cond, mc-ccr (s))) then update-pc (pc, s)

else update-pc (add (l, mc-pc (s), disp), s) endif

Opcode 0110. The Bcc instruction group includes Bcc, BRA and BSR instructions.

Definition: bcc-group (disp, ins, s) = if disp = 0

then if pc-word-readp (mc-pc (s), mc-mem (s)) then bcc-ra-sr (add (l, mc-pc (s), wsz),

cond-field (ins),

ext (w, pc-word-read (mc-pc (s), mc-mem (s)), l), s) else halt (pc-signal, s) endif

elseif disp = 255

then if pc-long-readp (mc-pc (s), mc-mem (s)) then bcc-ra-sr (add (l, mc-pc (s), lsz),

cond-field (ins),

pc-long-read (mc-pc (s), mc-mem (s)),

s) else halt (pc-signal, s) endif

else bcc-ra-sr (mc-pc (s), cond-field (ins), ext (b, disp, l), s) endif

Scc instruction.

Definition: scc-addr-modep (ins) = (data-addr-modep (s mode (ins), s rn (ins))

∧ alterable-addr-modep (s mode (ins), s rn (ins)))

CCR is not affected by Scc.

Definition: scc-effect (cond, ccr) = cons (if b0p (branch-cc (cond, ccr)) then 0 else 255 endif, ccr)

Definition: scc-ins (ins, s) = if scc-addr-modep (ins)

then let s&addr be mc-instate (b, ins, s)

in

if mc-haltp (car (s&addr)) then car (s&addr) else mapping (b,

scc-effect (cond-field (ins), mc-ccr (s)), s&addr) endif endlet

else halt (mode-signal, s) endif

DBcc instruction.

Definition: dbcc-loop (rn, s) = let cnt be sub (w, 1, read-dn (w, rn, s))

in

if nat-to-int (cnt, w) = -1

then update-pc (add (l, mc-pc (s), wsz), write-dn (w, cnt, rn, s))

else update-pc (add (l, mc-pc (s), ext (w,

pc-word-read (mc-pc (s), mc-mem (s)), l)),

write-dn (w, cnt, rn, s)) endif endlet

Definition: dbcc-ins (ins, s) = if pc-word-readp (mc-pc (s), mc-mem (s))

then if b0p (branch-cc (cond-field (ins), mc-ccr (s)))

then dbcc-loop (s rn (ins), s)

else update-pc (add (l, mc-pc (s), wsz), s) endif else halt (pc-signal, s) endif

ADDQ instruction.

Definition: addq-addr-modep (oplen, ins) = (alterable-addr-modep (s mode (ins), s rn (ins))

∧ (¬ byte-an-direct-modep (oplen, s mode (ins))))

It seems to us that there is no difference between word and long word operations for the ADDQ instruction in the address register direct mode.

Definition: addq-ins (oplen, ins, s) = if addq-addr-modep (oplen, ins)

then if an-direct-modep (s mode (ins))

then write-an (l, add (l, read-an (l, s rn (ins), s), i-data (d rn (ins))), s rn (ins), s)

else add-mapping (i-data (d rn (ins)), oplen, ins, s) endif else halt (mode-signal, s) endif

SUBQ instruction. Same remark as for ADDQ.

Definition: subq-addr-modep (oplen, ins) = (alterable-addr-modep (s mode (ins), s rn (ins))

∧ (¬ byte-an-direct-modep (oplen, s mode (ins))))

Definition: subq-ins (oplen, ins, s) = if subq-addr-modep (oplen, ins)

then if an-direct-modep (s mode (ins))

then write-an (l, sub (l, i-data (d rn (ins)), read-an (l, s rn (ins), s)), s rn (ins), s)

else sub-mapping (i-data (d rn (ins)), oplen, ins, s) endif else halt (mode-signal, s) endif

Opcode 0101. The Scc instruction group includes Scc, DBcc, ADDQ, and SUBQ instructions.

Definition: scc-group (ins, s) = if op-len (ins) = q

then if s mode (ins) = 1 then dbcc-ins (ins, s)

elseif (s mode (ins) = 7) ∧ (1 < s rn (ins))

         then halt ('trapcc-unspecified, s)

else scc-ins (ins, s) endif elseif b0p (bitn (ins, 8)) then addq-ins (op-len (ins), ins, s) else subq-ins (op-len (ins), ins, s) endif

Opcode 0111. MOVEQ instruction.

Definition: moveq-ins (ins, s)

= if b0p (bitn (ins, 8))

then d-mapping (l, move-effect (l, ext (b, head (ins, b), l), mc-ccr (s)), d rn (ins), s) else halt (reserved-signal, s) endif

CMP instruction.

Definition: cmp-cvznx (oplen, sopd, dopd, ccr) = cvznx (sub-c (oplen, sopd, dopd),

sub-v (oplen, sopd, dopd), sub-z (oplen, sopd, dopd), sub-n (oplen, sopd, dopd), ccr-x (ccr))

; it is different from sub-x.

Definition: cmp-addr-modep (oplen, ins) = (addr-modep (s mode (ins), s rn (ins))

∧ (¬ byte-an-direct-modep (oplen, s mode (ins))))

The execution of the CMP instruction.

Definition: cmp-ins (oplen, ins, s) = if cmp-addr-modep (oplen, ins)

then let s&addr be mc-instate (oplen, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else update-ccr (cmp-cvznx (oplen,

operand (oplen, cdr (s&addr), car (s&addr)), read-dn (oplen, d rn (ins), s), mc-ccr (s)),

car (s&addr)) endif endlet

else halt (mode-signal, s) endif

CMPA instruction.

Definition: cmpa-addr-modep (ins) = addr-modep (s mode (ins), s rn (ins))

The cvznx-flag setting is the same as the CMP instruction. The only difference is that word operation is sign-extended to longword operation.

Definition: cmpa-ins (oplen, ins, s) = if cmpa-addr-modep (ins)

then let s&addr be mc-instate (oplen, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else update-ccr (cmp-cvznx (l,

ext (oplen,

operand (oplen, cdr (s&addr), s),

l), read-an (l,

d rn (ins), car (s&addr)),

mc-ccr (s)),

car (s&addr)) endif endlet

else halt (mode-signal, s) endif

EOR instruction.

Definition: eor-z (oplen, sopd, dopd) = if logeor (sopd, dopd) = 0 then b1

else b0 endif

Definition: eor-n (oplen, sopd, dopd) = b-eor (mbit (sopd, oplen), mbit (dopd, oplen))

Definition: eor-cvznx (oplen, sopd, dopd, ccr) = cvznx (b0, b0, eor-z (oplen, sopd, dopd), eor-n (oplen, sopd, dopd), ccr-x (ccr))

Definition: eor-effect (oplen, sopd, dopd, ccr) = cons (logeor (sopd, dopd), eor-cvznx (oplen, sopd, dopd, ccr))

Definition: eor&eori-addr-modep (ins) = (data-addr-modep (s mode (ins), s rn (ins))

∧ alterable-addr-modep (s mode (ins), s rn (ins)))

Definition: eor-mapping (sopd, oplen, ins, s) = let s&addr be mc-instate (oplen, ins, s)

in

if mc-haltp (car (s&addr)) then car (s&addr)

else mapping (oplen,

eor-effect (oplen, sopd, operand (oplen, cdr (s&addr), s), mc-ccr (s)),

s&addr) endif endlet

Definition: eor-ins (oplen, ins, s) = if eor&eori-addr-modep (ins)

then eor-mapping (read-dn (oplen, d rn (ins), s), oplen, ins, s)

else halt (mode-signal, s) endif

CMPM instruction.

Definition: cmpm-mapping (addr, oplen, ins, s) = let s&addr be addr-postinc (oplen, d rn (ins), s)

in

if read-memp (cddr (s&addr), mc-mem (s), op-sz (oplen))

then update-ccr (cmp-cvznx (oplen, operand (oplen, addr, s), operand (oplen, cdr (s&addr), s), mc-ccr (s)),

car (s&addr))

else halt (read-signal, s) endif endlet

Definition: cmpm-ins (oplen, ins, s) = let s&addr be addr-postinc (oplen, s rn (ins), s)

in

if read-memp (cddr (s&addr), mc-mem (s), op-sz (oplen)) then cmpm-mapping (cdr (s&addr), oplen, ins, car (s&addr)) else halt (read-signal, s) endif endlet

Opcode 1011. The CMP instruction group includes instructions CMP, CMPA, EOR, and CMPM.

Definition: cmp-group (oplen, ins, s)

= if b0p (bitn (ins, 8))

then if oplen = q then cmpa-ins (w, ins, s) else cmp-ins (oplen, ins, s) endif elseif oplen = q then cmpa-ins (l, ins, s) elseif s mode (ins) = 1 then cmpm-ins (oplen, ins, s) else eor-ins (oplen, ins, s) endif

MOVEP instruction. MOVEP moves a data register into alternate bytes of memory.

Definition: movep-writep (addr, mem, n) = if n ≃ 0 then t

else byte-writep (add (l, addr, 2 ∗ (n − 1)), mem) ∧ movep-writep (addr, mem, n − 1) endif

Definition: movep-write (value, addr, mem, n) = if n ≃ 0 then mem

else movep-write (tail (value, b), addr, byte-write (value,

add (l, addr, 2 ∗ (n − 1)), mem),

n − 1) endif

Definition: movep-to-mem (addr, oplen, ins, s) = if movep-writep (addr, mc-mem (s), op-sz (oplen))

then update-mem (movep-write (read-dn (oplen, d rn (ins), s), addr, mc-mem (s), op-sz (oplen)),

s)

else halt (write-signal, s) endif

MOVEP moves alternate bytes in memory into a data register.

Definition: movep-readp (addr, mem, n) = if n ≃ 0 then t

else byte-readp (addr, mem)

∧ movep-readp (add (l, addr, wsz), mem, n − 1) endif

Definition: movep-read (addr, mem, n)

= if n ≃ 0 then 0

else app (b, byte-read (add (l, addr, 2 ∗ (n − 1)), mem), movep-read (addr, mem, n − 1)) endif

Definition: movep-to-reg (addr, oplen, ins, s) = if movep-readp (addr, mc-mem (s), op-sz (oplen))

then write-dn (oplen, movep-read (addr, mc-mem (s), op-sz (oplen)), d rn (ins), s) else halt (read-signal, s) endif

Definition: evenp (x) = b0p (bcar (x))

Definition: movep-addr (s&addr) = if evenp (cddr (s&addr)) then cddr (s&addr)

else add (l, cddr (s&addr), bsz) endif

Definition: movep-ins (opmode, ins, s) = let s&addr be addr-disp (mc-pc (s), s rn (ins), s)

in

if mc-haltp (car (s&addr)) then car (s&addr)

elseif opmode < 6 then if opmode = 4

then movep-to-reg (movep-addr (s&addr), w, ins, car (s&addr)) else movep-to-reg (movep-addr (s&addr), l, ins, car (s&addr)) endif

elseif opmode = 6

then movep-to-mem (movep-addr (s&addr), w, ins, car (s&addr))

else movep-to-mem (movep-addr (s&addr), l, ins, car (s&addr)) endif endlet

Some functions for bit operations.

Definition: bxxx-oplen (smode) = if dn-direct-modep (smode) then l

else b endif

Definition: bxxx-num (smode, bnum) = if dn-direct-modep (smode) then head (bnum, 5)

else head (bnum, 3) endif

Definition: bxxx-opd (smode, s&addr) = if dn-direct-modep (smode) then read-dn (l, cddr (s&addr), car (s&addr))

else operand (b, cdr (s&addr), car (s&addr)) endif

BCHG instruction.

Definition: bchg-addr-modep (ins) = (data-addr-modep (s mode (ins), s rn (ins))

∧ alterable-addr-modep (s mode (ins), s rn (ins)))

Definition: bchg-effect (bnum, opd, ccr) = cons (setn (opd, bnum, b-not (bitn (opd, bnum))),

set-z (b-not (bitn (opd, bnum)), ccr))

Definition: bchg-ins (bnum, ins, s) = if bchg-addr-modep (ins)

then let s&addr be mc-instate (b, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else mapping (bxxx-oplen (s mode (ins)),

bchg-effect (bxxx-num (s mode (ins), bnum), bxxx-opd (s mode (ins),

s&addr),

mc-ccr (s)),

s&addr) endif endlet

else halt (mode-signal, s) endif

BCLR instruction.

Definition: bclr-addr-modep (ins) = (data-addr-modep (s mode (ins), s rn (ins))

∧ alterable-addr-modep (s mode (ins), s rn (ins)))

Definition: bclr-effect (bnum, opd, ccr) = cons (setn (opd, bnum, b0), set-z (b-not (bitn (opd, bnum)), ccr))

Definition: bclr-ins (bnum, ins, s) = if bclr-addr-modep (ins)

then let s&addr be mc-instate (b, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else mapping (bxxx-oplen (s mode (ins)),

bclr-effect (bxxx-num (s mode (ins), bnum), bxxx-opd (s mode (ins),

s&addr),

mc-ccr (s)),

s&addr) endif endlet

else halt (mode-signal, s) endif

BSET instruction.

Definition: bset-addr-modep (ins) = (data-addr-modep (s mode (ins), s rn (ins))

∧ alterable-addr-modep (s mode (ins), s rn (ins)))

Definition: bset-effect (bnum, opd, ccr) = cons (setn (opd, bnum, b1), set-z (b-not (bitn (opd, bnum)), ccr))

Definition: bset-ins (bnum, ins, s) = if bset-addr-modep (ins)

then let s&addr be mc-instate (b, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else mapping (bxxx-oplen (s mode (ins)),

bset-effect (bxxx-num (s mode (ins), bnum), bxxx-opd (s mode (ins),

s&addr),

mc-ccr (s)),

s&addr) endif endlet

else halt (mode-signal, s) endif

BTST instruction.

Definition: btst-addr-modep (ins) = data-addr-modep (s mode (ins), s rn (ins))

Definition: btst-ins (bnum, ins, s)

= if btst-addr-modep (ins)

then let s&addr be mc-instate (b, ins, s) in if mc-haltp (car (s&addr)) then car (s&addr) else update-ccr (set-z (b-not (bitn (bxxx-opd (s mode (ins),

s&addr),

bxxx-num (s mode (ins),

bnum))),

mc-ccr (s)), car (s&addr)) endif endlet

else halt (mode-signal, s) endif

‘bit-ins’ includes the BTST, BCLR, BCHG, and BSET instructions.

Definition: bit-ins (bnum, ins, s) = let type be bits (ins, 6, 7)

in

if type < 2

then if type = 0 then btst-ins (bnum, ins, s) else bchg-ins (bnum, ins, s) endif elseif type = 2 then bclr-ins (bnum, ins, s) else bset-ins (bnum, ins, s) endif endlet

Dynamic bit operation. BTST, BCLR, BCHG, and BSET instructions.

Definition: d-bit-subgroup (ins, s) = if s mode (ins) = 1 then movep-ins (opmode-field (ins), ins, s)

else bit-ins (read-dn (l, d rn (ins), s), ins, s) endif

Static bit operation. BTST, BCLR, BCHG, and BSET instructions.

Definition: s-bit-subgroup (ins, s) = if pc-word-readp (mc-pc (s), mc-mem (s))

then if pc-byte-read (mc-pc (s), mc-mem (s)) = 0

then bit-ins (pc-byte-read (add (l, mc-pc (s), bsz), mc-mem (s)), ins, update-pc (add (l, mc-pc (s), wsz), s))

else halt (reserved-signal, s) endif else halt (pc-signal, s) endif

ORI instruction.

Definition: ori-addr-modep (ins)

= (data-addr-modep (s mode (ins), s rn (ins))

∧ alterable-addr-modep (s mode (ins), s rn (ins)))

Definition: ori-ins (oplen, ins, s) = let s&idata be immediate (oplen, mc-pc (s), s)

in

if mc-haltp (car (s&idata)) then car (s&idata)

elseif ori-addr-modep (ins)

then or-mapping (cddr (s&idata), oplen, ins, car (s&idata))

else halt (mode-signal, s) endif endlet

ORI to CCR instruction.

Definition: ori-to-ccr-ins (pc, s) = if pc-word-readp (pc, mc-mem (s))

then if pc-byte-read (pc, mc-mem (s)) = 0

then update-ccr (logor (pc-byte-read (add (l, pc, bsz), mc-mem (s)),

mc-ccr (s)), update-pc (add (l, pc, wsz), s))

else halt (reserved-signal, s) endif else halt (pc-signal, s) endif

ORI and ORI to CCR instructions. Detect ORI to SR, CMP2, and CHK2.

Definition: ori-subgroup (oplen, ins, s)

= if oplen = q then halt ('cmp2-chk2-unspecified, s)

elseif head (ins, 6) = 60

then if oplen = b then ori-to-ccr-ins (mc-pc (s), s) elseif oplen = w then halt ('ori-to-sr-privileged, s) else halt (reserved-signal, s) endif

else ori-ins (oplen, ins, s) endif

ANDI instruction.

Definition: andi-addr-modep (ins) = (data-addr-modep (s mode (ins), s rn (ins))

∧ alterable-addr-modep (s mode (ins), s rn (ins)))

Definition: andi-ins (oplen, ins, s) = let s&idata be immediate (oplen, mc-pc (s), s)

in if mc-haltp (s) then car (s&idata) elseif andi-addr-modep (ins) then and-mapping (cddr (s&idata), oplen, ins, car (s&idata)) else halt (mode-signal, s) endif endlet

ANDI to CCR instruction.

Definition: andi-to-ccr-ins (pc, s) = if pc-word-readp (pc, mc-mem (s))

then if pc-byte-read (pc, mc-mem (s)) = 0

then update-ccr (logand (pc-byte-read (add (l, pc, bsz), mc-mem (s)),

mc-ccr (s)), update-pc (add (l, pc, wsz), s))

else halt (reserved-signal, s) endif else halt (pc-signal, s) endif

ANDI and ANDI to CCR instructions. Detect ANDI to SR, CMP2 and CHK2.

Definition: andi-subgroup (oplen, ins, s)

= if oplen = q then halt ('cmp2-chk2-unspecified, s)

elseif head (ins, 6) = 60 then if oplen = b then andi-to-ccr-ins (mc-pc (s), s)

elseif oplen = w then halt ('andi-to-sr-unspecified, s)

else halt (reserved-signal, s) endif else andi-ins (oplen, ins, s) endif

SUBI instruction. Detect CMP2 and CHK2.

Definition: subi-addr-modep (ins) = (data-addr-modep (s mode (ins), s rn (ins))

∧ alterable-addr-modep (s mode (ins), s rn (ins)))

Definition: subi-ins (oplen, ins, s) = let s&idata be immediate (oplen, mc-pc (s), s)

in if mc-haltp (car (s&idata)) then car (s&idata) elseif subi-addr-modep (ins) then sub-mapping (cddr (s&idata), oplen, ins, car (s&idata)) else halt (mode-signal, s) endif endlet Definition: subi-subgroup (oplen, ins, s)

= if oplen = q then halt ('cmp2-chk2-unspecified, s)

else subi-ins (oplen, ins, s) endif

ADDI instruction. Detect RTM and CALLM.

Definition: addi-addr-modep (ins) = (data-addr-modep (s mode (ins), s rn (ins))

∧ alterable-addr-modep (s mode (ins), s rn (ins)))

Definition: addi-ins (oplen, ins, s) = let s&idata be immediate (oplen, mc-pc (s), s)

in

if mc-haltp (car (s&idata)) then car (s&idata)

elseif addi-addr-modep (ins)

then add-mapping (cddr (s&idata), oplen, ins, car (s&idata)) else halt (mode-signal, s) endif endlet

Definition: addi-subgroup (oplen, ins, s)

= if oplen = q then halt ('rtm-callm-unspecified, s)

else addi-ins (oplen, ins, s) endif

EORI instruction.

Definition: eori-ins (oplen, ins, s) = let s&idata be immediate (oplen, mc-pc (s), s)

in

if mc-haltp (car (s&idata)) then car (s&idata)

elseif eor&eori-addr-modep (ins)

then eor-mapping (cddr (s&idata), oplen, ins, car (s&idata)) else halt (mode-signal, s) endif endlet

EORI to CCR instruction.

Definition: eori-to-ccr-ins (pc, s) = if pc-word-readp (pc, mc-mem (s))

then if pc-byte-read (pc, mc-mem (s)) = 0

then update-ccr (logeor (pc-byte-read (add (l, pc, bsz), mc-mem (s)),

mc-ccr (s)), update-pc (add (l, pc, wsz), s))

else halt (reserved-signal, s) endif else halt (pc-signal, s) endif

EORI and EORI to CCR instructions. Detect EORI to SR, CAS and CAS2 instructions!

Definition: eori-subgroup (oplen, ins, s) = if oplen = q then halt ('cas-cas2-unspecified, s)

elseif head (ins, 6) = 60

then if oplen = b then eori-to-ccr-ins (mc-pc (s), s) elseif oplen = w then halt ('eori-to-sr-unspecified, s) else halt (reserved-signal, s) endif

else eori-ins (oplen, ins, s) endif

CMPI instruction.

Definition: cmpi-addr-modep (ins) = (data-addr-modep (s mode (ins), s rn (ins))

∧ (¬ idata-modep (s mode (ins), s rn (ins))))

Definition: cmpi-mapping (idata, oplen, ins, s) = let s&addr be mc-instate (oplen, ins, s)

in

if mc-haltp (car (s&addr)) then car (s&addr)

else update-ccr (cmp-cvznx (oplen, idata, operand (oplen, cdr (s&addr), s), mc-ccr (s)),

car (s&addr)) endif endlet

Definition: cmpi-ins (oplen, ins, s) = let s&idata be immediate (oplen, mc-pc (s), s)

in

if mc-haltp (car (s&idata)) then car (s&idata)

elseif cmpi-addr-modep (ins)

then cmpi-mapping (cddr (s&idata), oplen, ins, car (s&idata))

else halt (mode-signal, s) endif endlet

The CMPI subgroup includes only the CMPI instruction. Detect CAS and CAS2 instructions!

Definition: cmpi-subgroup (oplen, ins, s) = if oplen = q then halt ('cas-cas2-unspecified, s)

else cmpi-ins (oplen, ins, s) endif

Opcode 0000. This instruction group includes instructions ORI, ORI to CCR, BTST, BCLR, BCHG, BSET, MOVEP, ANDI, ANDI to CCR, SUBI, ADDI, EORI, EORI to CCR, CMPI.

Definition: bit-group (ins, s) = if b0p (bitn (ins, 8))

then if b0p (bitn (ins, 11))

then if b0p (bitn (ins, 10))

then if b0p (bitn (ins, 9))

then ori-subgroup (op-len (ins), ins, s)

else andi-subgroup (op-len (ins), ins, s) endif elseif b0p (bitn (ins, 9)) then subi-subgroup (op-len (ins), ins, s) else addi-subgroup (op-len (ins), ins, s) endif

elseif b0p (bitn (ins, 10)) then if b0p (bitn (ins, 9)) then s-bit-subgroup (ins, s)

else eori-subgroup (op-len (ins), ins, s) endif elseif b0p (bitn (ins, 9)) then cmpi-subgroup (op-len (ins), ins, s)

else halt ('moves-cas-cas2-unspecified, s) endif

else d-bit-subgroup (ins, s) endif

The opcode field.

Definition: opcode-field (ins) = bits (ins, 12, 15)

Execute the current instruction. See Table 3-14 of [4] for this classification.

Definition: execute-ins (ins, s) = let opcode be opcode-field (ins)

in if opcode < 8 then if opcode < 4

then if opcode < 2

then if opcode = 0 then bit-group (ins, s) else move-ins (b, ins, s) endif elseif opcode = 2 then move-group (l, ins, s) else move-group (w, ins, s) endif

elseif opcode < 6 then if opcode = 4 then misc-group (ins, s)

else scc-group (ins, s) endif elseif opcode = 6 then bcc-group (head (ins, b), ins, s) else moveq-ins (ins, s) endif

elseif opcode < 12 then if opcode < 10 then if opcode = 8 then or-group (op-len (ins), ins, s) else sub-group (opmode-field (ins), ins, s) endif

elseif opcode = 10 then halt (reserved-signal, s) else cmp-group (op-len (ins), ins, s) endif

elseif opcode < 14

then if opcode = 12 then and-group (op-len (ins), ins, s) else add-group (opmode-field (ins), ins, s) endif

elseif opcode = 14 then s&r-group (ins, s)

    else halt ('coprocessor-unspecified, s) endif endlet

‘current-ins’ is a function of two arguments, pc and s. pc is the current value of the program counter, and s is the current state. ‘current-ins’ returns the current instruction (a word, not including any possible extension words), that is, the word pointed to by pc. To determine what instruction we are to execute, this word may only provide partial information. Many instructions require that we examine subsequent words to determine what to do. But to figure out how many words we need, we must start with the first word.

Definition: current-ins (pc, s) = pc-word-read (pc, mc-mem (s))

13 Stepi and Stepn

‘stepi’ maps a machine state to the next machine state by executing the current instruction.

Definition: stepi (s) = if evenp (mc-pc (s))

then if pc-word-readp (mc-pc (s), mc-mem (s))

then execute-ins (current-ins (mc-pc (s), s),

update-pc (add (l, mc-pc (s), wsz), s))

else halt (pc-signal, s) endif else halt (pc-odd-signal, s) endif

‘stepn’ is a function of two arguments: s is the current state of the machine, and n is the number of instructions to execute.

Definition: stepn (s, n) = if mc-haltp (s) ∨ (n ≃ 0) then s

else stepn (stepi (s), n − 1) endif

14 Auxiliary Functions

This section contains some auxiliary functions which are not needed to define ‘stepn’ but are used only in the example of the next section. ‘map-update’ updates the map in the memory. The map is a binary tree with a list of keys in the key field. By updating the map we assign new properties to the memory.

Definition: cons-key-lst (key, lst) = if key ∈ lst then lst

else cons (key, lst) endif

Definition: key-field (map) = if listp (map) then car (map)

else nil endif

Definition: make-map (key, map) = make-bt (cons-key-lst (key, key-field (map)), branch0 (map), branch1 (map))

Definition: map-update (key, x, n, map)

= if n ≃ 0 then make-map (key, map)

elseif b0p (bitn (x, n − 1)) then make-bt (key-field (map),

map-update (key, x, n − 1, branch0 (map)), branch1 (map))

else make-bt (key-field (map), branch0 (map), map-update (key, x, n − 1, branch1 (map))) endif

Load the values in the list into the memory starting from location addr.

Definition: load-lst-mem (opsz, lst, addr, mem) = if listp (lst)

then load-lst-mem (opsz, cdr (lst), add (32, addr, opsz), write-mem (car (lst), addr, mem, opsz))

else mem endif

Event: For efficiency, compile those definitions not yet compiled.

15 An Example of Simulation

Here is an utterly concrete theorem about ‘stepn’. Roughly speaking, the theorem states that if ‘stepn’ executes 37 instructions starting in a state that contains machine code instructions for Euclid’s GCD algorithm in ROM and the integers 54 and 42 on the stack, then the correct answer, 6, is the value of data register d0 in the resulting state. This theorem has, of course, an utterly trivial proof: we just run ‘stepn’ . We present this trivial theorem here only to illustrate setting up ‘stepn’ to run.

Theorem: gcd-example ((stack-pointer = EFFFE4016)

 ∧ (rfile = '(0 0 0 0 0 0 0 0 0 0 0 0 0 0 EFFFE4C16
              EFFFE4016))
 ∧ (pc = 22B616)

∧ (ccr = 0)

 ∧ (gcd-code = '(78 86 0 0 72 231 48 0 36 46 0 8 38 46 0
                 12 74 130 103 28 74 131 102 4 32 2 96 22
                 182 130 108 8 76 67 40 0 36 0 96 232 76
                 66 56 0 38 0 96 224 32 3 76 238 0 12 255
                 248 78 94 78 117))

∧ (empty-memory = '((nil

                        (nil (nil (nil (nil ((rom) nil))))))))

∧ (mem = load-lst-mem (4,

                        '(22B216 54 42),

stack-pointer,

load-lst-mem (1, gcd-code, pc, empty-memory)))

∧ (initial-state = mc-state ('running, rfile, pc, ccr, mem)) ∧ (final-state = stepn (initial-state, 37))) → ((mc-status (final-state) = 'running)

∧ (mc-rfile (final-state)

          = '(6 0 0 0 0 0 0 0 0 0 0 0 0 0
               EFFFE4C16 EFFFE4416))

∧ (mc-pc (final-state) = 22B216))

Here is a paraphrase of the foregoing theorem. The specific numbers in the theorem are derived from the compilation of a C program for GCD and from the result of loading that program on a Sun-3.

• If

1. stack-pointer = EFFFE4016,

2. the register file rfile is all 0’s excepting for A6 and SP, which are EFFFE4C16 and stack-pointer, respectively, 3. the program counter pc = 22B616 and the condition code register ccr

= 0,

4. gcd-code is the long list of integers above beginning with 78 and ending with 117,

5. empty-memory is a pair representing a 32-bit wide memory which has a 0 byte at every address, which is of type ROM from address 016 to address 07FFFFFF16, and which is of type RAM at all other addresses,

6. mem is the result of first loading gcd-code into an empty memory at pc and then further loading the two natural numbers 54 and 42 and the return address of the caller (22B216) at the location pointed to by stack-pointer,

7. initial-state is an mc-state whose five fields are 'running, rfile, pc, ccr, and mem, respectively, and finally

8. final-state is the result of running ‘stepn’ for 37 instructions starting with initial-state,

• then, if we examine final-state, we find:

1. the machine is still 'running,

2. the register file is '(60000000000000EFFFE4C16EFFFE4416),

observing that d0 is equal to 6, the GCD of 54 and 42, and

3. the program counter is set to 22B216, the return address to the caller.

This theorem should not be confused with the much more general theorem stating the correctness of the same GCD program on all input, a theorem whose mechanical proof is described in [3]. Event: Make the library "mc20-1" and compile it.

16 Acknowledgements

We would like to thank Bill Bevier, Don Good, Warren Hunt, Matt Kaufmann, J Moore, and Bill Schelter for their many constructive suggestions and discussions. Special thanks to Fay Goytowski for her meticulous reading of the MC68020 specification, which revealed a dozen or so errors, and to Ken Albin for setting up a test suite for our MC68020 model, which further revealed ??? errors. The general style of Nqthm formalization used in this MC68020 specification is the product of over a decade of study by the authors of Nqthm and their students. Especially influential was the FM8502 and Piton work [1]. The development of Nqthm was primarily supported by NSF, ONR, and DARPA.

17 Syntax Summary

Here is a summary of the conventional syntax used in this report in terms of the official syntax of the Nqthm logic described in [2]. (‘cond’ and ‘let’ are recent extensions not described in [2].)

1. Variables. x, y, z, etc. are printed in italics.

2. Function application. For any function symbol for which special syntax is not given below, an application of the symbol is printed with the usual notation; e.g., the term (fn x y z) is printed as fn (x, y, z). Note that the function symbol is printed in Roman. In the special case that ‘c’ is a function symbol of no arguments, i.e., it is a constant, the term (c) is printed merely as c, in small caps, with no trailing parentheses. Because variables are printed in italics, there is no confusion between the printing of variables and constants.

3. Other constants. t, f, and nil are printed in bold. Quoted constants are printed in the ordinary fashion of the Nqthm logic, e.g., '(a b c) is still printed just that way. #b001 is printed as 0012, #o765 is printed as 7658, and #xA9 is printed as A916 .

4. (if x y z) is printed as

if x then y else z endif.

5. (cond (test1 value1) (test2 value2) (t value3)) is printed as

if test1 then value1 elseif test2 then value2 else value3 endif.

6. (let ((var1 val1) (var2 val2)) form) is printed as

let var1 be val1 , var2 be val2 in form endlet.

7. The remaining function symbols that are printed specially are described in the following table.

Nqthm Syntax  Conventional Syntax

(or x y)  x ∨ y
(and x y)  x ∧ y
(times x y)  x ∗ y
(plus x y)  x + y
(remainder x y)  x mod y
(quotient x y)  x ÷ y
(difference x y)  x − y
(implies x y)  x → y
(member x y)  x ∈ y
(geq x y)  x ≥ y
(greaterp x y)  x > y
(leq x y)  x ≤ y
(lessp x y)  x < y
(equal x y)  x = y
(not (member x y))  x ∉ y
(not (geq x y))  x ≱ y
(not (greaterp x y))  x ≯ y
(not (leq x y))  x ≰ y
(not (lessp x y))  x ≮ y
(not (equal x y))  x ≠ y
(minus x)  − x
(add1 x)  1 + x
(nlistp x)  x ≃ nil
(zerop x)  x ≃ 0
(numberp x)  x ∈ N
(sub1 x)  x − 1
(not (nlistp x))  x ≄ nil
(not (zerop x))  x ≄ 0
(not (numberp x))  x ∉ N

References

[1] William Bevier, J Strother Moore, Warren Hunt, and William Young. Special issue on system verification. Journal of Automated Reasoning, 5(4), 1989.

[2] Robert S. Boyer and J Strother Moore. A Computational Logic Handbook. Academic Press, 1988.

[3] Robert S. Boyer and Yuan Yu. Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor, Technical Report TR-91-33, University of Texas at Austin, to appear in the proceedings of the 11th International Conference on Automated Deduction, Lecture Notes in Computer Science, Springer-Verlag, 1992.

[4] Motorola, Inc. MC68020 32-bit Microprocessor User’s Manual. Prentice Hall, New Jersey, 1989.

Index

a-mapping, 32, 33 abs, 9, 10 absolute-long, 29, 31 absolute-short, 28, 31 add, 8, 16–19, 23, 25–28, 30, 33–35,

70, 72, 77–80, 85–87, 91, 92, 95–98, 102, 103

add-addr-modep1, 34 add-addr-modep2, 34, 35 add-c, 33, 34 add-cvznx, 34 add-effect, 34, 35 add-group, 37, 101 add-ins1, 34, 37 add-ins2, 35, 37 add-mapping, 35, 87, 98 add-n, 34 add-v, 33, 34 add-z, 34 adda-addr-modep, 35 adda-ins, 35, 37 adder, 8, 36 addi-addr-modep, 98 addi-ins, 98 addi-subgroup, 98, 100 addq-addr-modep, 86, 87 addq-ins, 87 addr-disp, 25, 30, 92 addr-index, 28, 30 addr-index-bd, 26, 27 addr-index-disp, 25, 28 addr-index1, 28 addr-index2, 27–29 addr-index3, 27, 28 addr-indirect, 24, 30 addr-modep, 31, 34, 35, 38, 39, 63,

64, 73, 88 addr-postinc, 24, 30, 90 addr-predec, 24, 30, 37, 41 addx-c, 36 addx-cvznx, 36 addx-effect, 36, 37 addx-ins1, 36, 37 addx-ins2, 37 addx-n, 36 addx-v, 36 addx-z, 36 alterable-addr-modep, 31, 34, 38, 42,

47, 51, 63, 66–68, 71, 73, 82, 85–87, 89, 93, 94, 96– 98 an-direct, 23, 30 an-direct-modep, 32, 87 and-addr-modep1, 42 and-addr-modep2, 42, 43 and-cvznx, 42 and-effect, 42, 43 and-group, 46, 101 and-ins1, 42, 46 and-ins2, 43, 46 and-mapping, 43, 97 and-n, 42 and-z, 42 andi-addr-modep, 96, 97 andi-ins, 96, 97 andi-subgroup, 97, 100 andi-to-ccr-ins, 97 app, 8, 9, 17, 18, 49–51, 69, 74, 75,

92 asl, 9, 25, 57 asl-c, 56, 57 asl-cvznx, 57 asl-effect, 57, 58 asl-n, 57 asl-v, 57 asl-x, 57 asl-z, 57 asr, 9, 58 asr-c, 57, 58 asr-cvznx, 58 asr-effect, 58, 59 asr-n, 58 asr-x, 58 asr-z, 58

b, 3, 15–19, 23, 26, 29, 30, 32, 46, 51, 65, 68, 69, 73, 85, 86, 88, 91–97, 99, 100

b-and, 5, 7, 33, 36, 38, 40, 84 b-eor, 6, 7, 89 b-equal, 6 b-nand, 5 b-nor, 5 b-not, 5, 8, 33, 36, 38, 40, 84, 93–95 b-or, 5, 7, 36, 38, 40, 46, 84 b0, 4, 6, 34, 36, 38, 40, 42–44, 46,

48, 49, 51–55, 57, 58, 60, 61, 63, 65, 66, 69, 82, 84, 89, 93

b0p, 4–6, 8, 13, 14, 25, 27–29, 45, 46, 49–51, 62, 63, 69, 71, 72, 74–79, 81, 83, 85–88, 91, 92, 100, 103

b1, 4–6, 34, 36, 38, 40, 42–44, 46, 48–50, 52, 54, 55, 57, 58, 60, 63, 65, 66, 69, 73–75, 82, 84, 89, 94

b1p, 5, 6, 80, 83 bcar, 6, 7, 51, 71, 92 bcc-group, 85, 100 bcc-ra-sr, 85 bcdr, 6, 7, 59, 71 bchg-addr-modep, 93 bchg-effect, 93 bchg-ins, 93, 95 bclr-addr-modep, 93, 94 bclr-effect, 93, 94 bclr-ins, 94, 95 bcs, 83, 84 bd-sz, 27, 28 beq, 83, 84 bf-subgroup, 63 bge, 84 bgt, 84 bhi, 84 Big Endian, 17 binary tree, 13 bit-group, 100 bit-ins, 95 bitn, 7, 8, 13, 14, 20, 25, 27–29, 45,

46, 50–55, 57, 59, 60, 62, 63, 69, 72, 75–79, 81, 83, 87, 88, 91, 93–95, 100, 103

bitp, 4 bits, 7, 18, 19, 25, 27, 66, 75, 76, 95,

100 ble, 84 bls, 84 blt, 84 bmi, 84 branch-cc, 84–86 branch0, 12, 13, 102, 103 branch1, 12–14, 102, 103 bs-pc, 29 bs-register, 28 bset-addr-modep, 94 bset-effect, 94 bset-ins, 94, 95 bsr-ins, 85 bsz, 4, 30, 92, 95–98 btst-addr-modep, 94, 95 btst-ins, 94, 95 bvs, 80, 84 bxxx-num, 92–95 bxxx-opd, 93–95 bxxx-oplen, 92–94 byte-an-direct-modep, 32, 34, 38, 63,

86–88 byte-read, 17, 92 byte-readp, 16, 91 byte-write, 19, 91 byte-writep, 19, 91

ccr-c, 20 ccr-n, 20, 84 ccr-v, 20, 80, 84 ccr-x, 20, 36, 41, 42, 44, 46, 48, 49,

52–55, 57, 58, 60, 61, 63, 65, 66, 69, 82, 88, 89

ccr-z, 20, 36, 41, 84 clr-addr-modep, 66 clr-cvznx, 66 clr-effect, 66 clr-ins, 66, 67 clr-subgroup, 67, 83 cmp-addr-modep, 88 cmp-cvznx, 88–90, 99 cmp-group, 90, 101 cmp-ins, 88, 91 cmpa-addr-modep, 88, 89 cmpa-ins, 91 cmpi-addr-modep, 99 cmpi-ins, 99 cmpi-mapping, 99 cmpi-subgroup, 100 cmpm-ins, 90, 91 cmpm-mapping, 90 cond-field, 18, 85, 86 cons-key-lst, 102 control-addr-modep, 31, 65, 68, 71,

77, 81 current-ins, 101, 102 cvznx, 20, 34, 36, 38, 40, 42, 44, 46,

48, 49, 52–55, 57, 58, 60, 61, 63, 65, 66, 69, 82, 88, 89

d-bit-subgroup, 95, 100 d-mapping, 33, 35, 37, 39, 41, 43,

47, 52, 53, 55–58, 60, 61, 65, 69, 70, 88

d mode, 18, 63–65 d rn, 18, 35, 37, 39–41, 43, 45–47,

50, 51, 63–65, 87–92, 95 data-addr-modep, 31, 42, 43, 46, 63,

66–68, 73, 82, 85, 89, 93, 94, 96–99

dbcc-ins, 86, 87 dbcc-loop, 86 dh, 76 div l-ins, 75, 77 div w-ins, 50 divs-cvznx, 48, 49, 74 divs-n, 48 divs-v, 48, 49, 74 divs-z, 48 divs l, 74, 75 divs w-ins, 48, 50 divsl l, 74, 75 divu-cvznx, 49, 50, 74, 75 divu-n, 49 divu-v, 49, 50, 75 divu-z, 49 divu l, 75 divu w-ins, 50 divul l, 74, 75 dl, 76 dn-direct, 23, 30 dn-direct-modep, 31, 92, 93 dq, 75

effec-addr, 30, 32, 64–66, 69, 72, 78,

81, 82 Endian, 17 eor-cvznx, 89 eor-effect, 89, 90 eor-ins, 90, 91 eor-mapping, 90, 98 eor-z, 89 eor&eori-addr-modep, 89, 90, 98 eori-ins, 98, 99 eori-subgroup, 99, 100 eori-to-ccr-ins, 98, 99 evenp, 92, 102 execute-ins, 100, 102 exg-arar-ins, 45, 46 exg-drar-ins, 45, 46 exg-drdr-ins, 45, 46 exp, 3, 6–9, 11, 19, 43, 49, 59 ext, 8, 25, 26, 28, 29, 35, 40, 64, 65,

70, 79, 80, 85, 86, 88, 89 ext-cvznx, 65 ext-effect, 65, 69, 70 ext-ins, 69, 72 ext-n, 65 ext-subgroup, 72, 83 ext-z, 65 extb-ins, 65, 66 fix-bit, 5, 7, 20, 59, 60, 80, 84 fix-int, 9–11

gcd-example, 104 get-nth, 15

halt, 21, 22, 25–30, 32, 33, 35, 37, 39–41, 43, 46, 47, 49, 50, 53, 54, 56, 59, 61–69, 72– 83, 85–102

head, 6–9, 15–19, 26, 29, 43, 48, 49, 51, 59, 63, 68, 69, 74, 76, 88, 93, 96, 97, 99, 100

i-data, 51, 87 i-is, 27 idata-modep, 32, 99 idifference, 10 ileq, 10 ilessp, 10 immediate, 30, 31, 96–99 index-register, 25 index-rn, 25 ineg, 10 int-rangep, 11, 44, 48, 57 int-to-nat, 11, 43, 48 integerp, 9 iplus, 10 iquot, 48, 49, 74 iquotient, 10, 48 ir-scaled, 25–27, 29 irem, 48, 49, 74 iremainder, 10, 48 itimes, 10, 43, 44 izerop, 9, 10

jmp-addr-modep, 81 jmp-ins, 81, 83 jmp-mapping, 81, 82 jsr-addr-modep, 81 jsr-ins, 81, 83

key-field, 102, 103 l, 3, 16, 22–24, 26–30, 37, 40, 41,

44, 45, 49, 50, 64, 65, 69– 72, 74, 75, 77–82, 85–89, 91–93, 96–98, 100, 102

lea-addr-modep, 65 lea-ins, 65, 66 lea-subgroup, 66, 83 len, 16 link-mapping, 78, 79 link l-ins, 79, 83 link w-ins, 79 load-lst-mem, 103, 104 logand, 7, 42, 97 logeor, 7, 89, 98 lognot, 6, 8, 82 logor, 7, 46, 96 long-read, 17, 26, 79, 80 long-readp, 17, 26, 79, 80 lsl, 8, 54, 55 lsl-c, 54, 56 lsl-cvznx, 54, 55 lsl-effect, 55, 56 lsl-n, 54 lsl-x, 54 lsl-z, 54 lsr, 9, 55 lsr-c, 55 lsr-cvznx, 55 lsr-effect, 55, 56 lsr-n, 55 lsr-x, 55 lsr-z, 55 lsz, 4, 17, 18, 28, 29, 69, 79, 80, 82,

85

m-mapping, 33 make-bt, 12, 14, 102, 103 make-map, 102, 103 map-update, 102, 103 mapping, 33, 35, 37, 39, 41, 43, 47,

53, 54, 59, 61, 62, 64, 66– 68, 73, 82, 86, 90, 93, 94

mbit, 7, 33, 34, 36, 38, 40, 42, 44, 46, 48, 49, 54, 55, 57, 58,

63, 65, 82, 89 mc-ccr, 16, 32, 33, 37, 41, 43–45,

47, 49, 50, 52–62, 64–67, 69, 70, 73–76, 80, 82, 85, 86, 88–90, 93–99

mc-haltp, 16, 34, 35, 39, 40, 42, 43, 45, 47, 50, 53, 54, 56, 58, 59, 61, 62, 64–69, 72, 77, 78, 81, 82, 86, 88–90, 92– 99, 102

mc-instate, 32, 34, 35, 39, 42, 43, 45, 47, 50, 53, 54, 56, 58, 59, 61, 62, 64, 66–68, 73, 77, 82, 86, 88–90, 93–95, 99

mc-mem, 16, 21, 22, 25, 26, 28–30, 32, 33, 37, 41, 72, 77–80, 85, 86, 90–92, 95–98, 101, 102

mc-pc, 16, 21, 30–33, 72, 78–80, 82,

85, 86, 92, 95–99, 102, 104 mc-rfile, 16, 21, 22, 32, 33, 72, 78,

104 mc-state, 16, 21, 32, 33, 104 mc-status, 16, 21, 32, 33, 104 mem-asl-effect, 58, 59 mem-asl-ins, 58, 62 mem-asr-effect, 59 mem-asr-ins, 59, 62 mem-indirect, 26, 27 mem-lsl-effect, 56 mem-lsl-ins, 56, 62 mem-lsr-effect, 56 mem-lsr-ins, 56, 62 mem-postindex, 26, 27 mem-preindex, 27 mem-rol-effect, 53 mem-rol-ins, 53, 62 mem-ror-effect, 54 mem-ror-ins, 54, 62 mem-roxl-effect, 61 mem-roxl-ins, 61, 62 mem-roxr-effect, 61, 62 mem-roxr-ins, 62 memory, 13 memory-addr-modep, 31, 34, 38, 42,

47, 51 memory-shift-rotate, 62, 63 misc-group, 83, 100 mode-signal, 4, 35, 39, 40, 43, 46,

47, 50, 53, 54, 56, 59, 61, 62, 64–69, 72, 73, 77, 78, 81, 82, 86–90, 93–99

move-addr-modep, 63, 64 move-cvznx, 63, 73 move-effect, 63, 64, 88 move-from-ccr-addr-modep, 66 move-from-ccr-effect, 66, 67 move-from-ccr-ins, 66, 67 move-group, 65, 100 move-ins, 64, 65, 100 move-mapping, 64 move-n, 63 move-to-ccr-addr-modep, 68 move-to-ccr-ins, 68 move-z, 63 movea-addr-modep, 64 movea-ins, 64, 65 movem-ea-rn-addr-modep, 77, 78 movem-ea-rn-ins, 77, 78 movem-ea-rn-subgroup, 78, 83 movem-len, 71, 77, 78 movem-pre-rnlst, 71, 72 movem-predec, 71, 72 movem-rn-ea-addr-modep, 71, 72 movem-rn-ea-ins, 71, 72 movem-rnlst, 70–72, 78 movep-ins, 92, 95 movep-read, 91, 92 movep-readp, 91, 92 movep-to-mem, 91, 92 movep-to-reg, 92 movep-write, 91 movep-writep, 91 moveq-ins, 87, 100 mul-div l-ins, 76, 78 mul&div-addr-modep, 43, 45, 50, 76 mul l-ins, 76, 77 mul w-ins, 45, 46 muls, 43–45, 76 muls-cvznx, 44, 45, 76 muls-n, 44 muls-v, 44 muls l dl, 76 muls l dldh, 76 muls w-ins, 45, 46 mulu, 43, 44, 75, 76 mulu-cvznx, 44, 75 mulu-n, 44 mulu-v, 43, 44 mulu-z, 44 mulu l dl, 75, 76 mulu l dldh, 75, 76 mulu w-ins, 44, 45

nat-rangep, 11 nat-to-int, 11, 43, 44, 48, 49, 57, 75,

86 nat-to-uint, 11, 50, 75 neg-addr-modep, 68 neg-ins, 68 neg-subgroup, 68, 83 negp, 9–11 negx-addr-modep, 67 negx-ins, 67 negx-subgroup, 67, 83 nop-ins, 80, 81 nop-subgroup, 81, 83 not-addr-modep, 82 not-cvznx, 82 not-effect, 82 not-ins, 82 not-subgroup, 82, 83 not-z, 82

op-len, 19, 37, 41, 42, 63, 67, 68, 74,

82, 87, 100, 101 op-sz, 15, 22, 23, 26, 30, 32, 33, 37,

41, 71, 72, 77, 78, 90–92 opcode-field, 100 operand, 22, 35, 37, 39–43, 45, 47,

50, 53, 54, 56, 58, 59, 61, 62, 64, 67, 68, 73, 77, 82, 88–90, 93, 99

opmode-field, 18, 95, 101 or-addr-modep1, 46, 47 or-addr-modep2, 47 or-cvznx, 46 or-effect, 46, 47 or-group, 50, 101 or-ins1, 47, 50 or-ins2, 47, 50 or-mapping, 47, 96 or-n, 46 or-z, 46 ori-addr-modep, 95, 96 ori-ins, 96 ori-subgroup, 96, 100 ori-to-ccr-ins, 96

pc-byte-read, 18, 30, 95–97 pc-byte-readp, 17 pc-disp, 29, 31 pc-index, 30, 31 pc-index-disp, 29 pc-index1, 29, 30 pc-long-read, 18, 28, 29, 79, 85 pc-long-readp, 17, 28, 29, 79, 85 pc-odd-signal, 4, 102 pc-read, 14, 18 pc-read-mem, 18, 26, 30 pc-read-memp, 26, 30 pc-readp, 13, 17 pc-signal, 4, 25, 26, 28–30, 72, 78–

80, 85, 86, 95–98, 102 pc-word-read, 18, 25, 28–30, 72, 78–

80, 85, 86, 101 pc-word-readp, 17, 25, 28–30, 72,

78–80, 85, 86, 95–98, 102 pea-addr-modep, 68, 69 pea-ins, 69 pea-subgroup, 69, 83 post-effect, 23, 24 postinc-modep, 77 pre-effect, 23, 25, 71 predec-modep, 32, 72 protection, 13 push-sp, 22, 69, 82, 85 put-nth, 15

q, 4, 46, 50, 63, 67, 68, 74–76, 82,

87, 91, 96–99 qsz, 4 quot, 49, 50, 74, 75

RAM, 13 read, 14, 17 read-an, 21, 22, 24–26, 28, 35, 40,

45, 71, 77, 79, 87, 89 read-dn, 21, 22, 25, 35, 37, 39, 41,

43, 44, 47, 49–53, 55–58, 60, 61, 65, 69, 70, 74–76, 86, 88, 90, 91, 93, 95

read-mem, 17, 22, 70 read-memp, 16, 17, 32, 37, 41, 77,

90 read-rn, 15, 21, 70 read-signal, 26, 32, 37, 41, 78–80,

90, 92 read-sp, 22, 79, 80 reading memory, 17 readm-mem, 70, 78 readm-rn, 70, 72 readmp, 77, 78 readp, 13, 16 register-asl-ins, 57, 62 register-asr-ins, 58, 62 register-lsl-ins, 55, 62 register-lsr-ins, 56, 62 register-rol-ins, 52, 62 register-ror-ins, 53, 62 register-roxl-ins, 60, 62 register-roxr-ins, 61, 62 register-shift-rotate, 62, 63 rem, 49, 50, 74, 75 replace, 8, 15, 20 reserved-signal, 4, 27–29, 46, 66, 77,

83, 88, 95–99, 101 rol, 51, 52, 59 rol-c, 51, 52 rol-cvznx, 52 rol-effect, 52, 53 rol-n, 52 rol-z, 52 ROM, 13 ror, 53, 59 ror-c, 52, 53 ror-cvznx, 53 ror-effect, 53, 54 ror-n, 53 ror-z, 52, 53 roxl, 59, 60 roxl-c, 59, 60 roxl-cvznx, 60 roxl-effect, 60, 61 roxl-n, 60 roxr, 59–61 roxr-c, 60, 61 roxr-cvznx, 61 roxr-n, 60, 61 roxr-z, 60, 61 rtd-ins, 80, 81 rtd-mapping, 80 rtr-ins, 80, 81 rts-ins, 80, 81

s-bit-subgroup, 95, 100 s&r-addr-modep, 51, 53, 54, 56, 58,

59, 61, 62 s&r-group, 63, 101 s mode, 18, 32, 35, 37–39, 42, 43,

47, 50, 51, 63–69, 71–73, 77, 78, 81, 82, 85, 87–89, 91, 93–99

s rn, 18, 32, 34, 35, 37–39, 41–43, 45–47, 51–53, 55–58, 60, 61, 63, 64, 66–73, 77–79, 81– 83, 85, 87–90, 92–94, 97– 99

scc-addr-modep, 85, 86 scc-effect, 85, 86 scc-group, 87, 100 scc-ins, 86, 87 set-c, 20 set-cvznx, 20, 21, 32, 33 set-n, 20 set-v, 20, 49, 50, 75 set-x, 20 set-z, 20, 93–95 setn, 7, 73, 93, 94 sp, 22, 23 sr-cnt, 51–53, 55–58, 60, 61 stepi, 102 stepn, 102, 104 sub, 8, 22, 23, 37, 38, 40, 71, 79, 86,

87 sub-addr-modep1, 38, 39 sub-addr-modep2, 38, 39 sub-c, 37, 38, 88 sub-cvznx, 38 sub-effect, 38, 39, 68 sub-group, 41, 101 sub-ins1, 39, 41 sub-ins2, 39, 42 sub-mapping, 39, 87, 97 sub-n, 38, 88 sub-v, 38, 88 sub-z, 38, 88 suba-addr-modep, 39 suba-ins, 39, 41 subi-addr-modep, 97 subi-ins, 97, 98 subi-subgroup, 98, 100 subq-addr-modep, 87 subq-ins, 87 subtracter, 8, 40, 41 subx-c, 40 subx-cvznx, 40, 41 subx-effect, 41, 67 subx-ins1, 41, 42 subx-ins2, 41, 42 subx-n, 40 subx-v, 40 subx-z, 40 swap-cvznx, 69 swap-effect, 69 swap-ins, 69 swap-n, 69 swap-z, 69

tail, 6–9, 19, 51, 69, 76, 91

tas-addr-modep, 73

tas-effect, 73 tas-ins, 73, 74 trapv-ins, 80, 81 tst-addr-modep, 73 tst-ins, 73, 74 tst-subgroup, 74, 83

uint-rangep, 11 uint-to-nat, 11 unavailable, 13 unlk-ins, 79 unlk-subgroup, 79, 83 update-ccr, 21, 44, 45, 49, 50, 68,

73–76, 80, 88–90, 95–99 update-mem, 21, 22, 72, 79, 91 update-pc, 21, 25–30, 72, 78–81, 85, 86, 95–98, 102

update-rfile, 21, 22, 78

value-field, 12–14

w, 3, 25, 27–30, 37, 41, 44–46, 49, 50, 53, 54, 56, 58, 59, 61, 62, 66–70, 72, 78–80, 85, 86, 91, 92, 96, 97, 99, 100

word-read, 17, 80 word-readp, 16, 80 write, 14, 19 write-an, 22, 24, 25, 35, 40, 45, 64, 65, 71, 72, 78, 79, 87 write-dn, 21, 44, 45, 49, 50, 74–76,

86, 92 write-mem, 19, 22, 33, 70, 79, 103 write-memp, 19, 22, 33, 71, 79 write-rn, 15, 21, 22, 32, 33, 70 write-signal, 4, 22, 33, 72, 79, 91 write-sp, 22, 79, 80 writem-mem, 70, 72 writem-rn, 70, 78 writemp, 71, 72 writep, 14, 19 wsz, 4, 16–18, 23, 25, 28–30, 72, 78–

80, 85, 86, 91, 95–98, 102