hol88/computer/microcode.ml

7 %     This theory is the specification of the microcode resulting in    %
8 %  32 axioms (one for each word of microcode).  The microcode and the   %
10 %     Where Gordon's original specification of the microcode only       %
11 %  used the top 26 words of microcode store, we now specify the         %
12 %  'unused' part of the store.  This was needed to eliminate the        %
13 %  possibility of the computer looping forever in the 'unused' part     %
14 %  of the store upon powering up.                                       %
16 %  from 1 to 2 because of a minor change in the decode unit which is    %
47  mk_ADDR [b4;b3;b2;b1;b0] n  gives a list of the positions of bits that
48                              are 1 if n is represented in the 5-bit
61  mk_A_ADDR n gives a list of the positions of bits in the A-address
64  mk_B_ADDR n gives a list of the positions of bits in the B-address
72  test_button(n,m) gives a list of the bits that are 1 if the address of the
80  test_acc(n,m) gives a list of the bits that are 1 if the address of the
88  jump n  gives a list of the bits that are 1 if the address of the
95  jump_knob n  gives a list of the bits that are 1 if the address of the
103  jump_opcode n  gives a list of the bits that are 1 if the address of the
113  mk_micro_ins l  takes a list of numbers representing the positions of bits
115                  a micro-word (i.e. a value of type ":word30") with the
130  define_microinstruction(addr,cont)  generates an axiom of the form:
132                                      where n is the ROM-address corresponding
133                                      to the ML integer addr, and w is a
134                                      microinstruction word generated from the
144  The following generates axioms defining the host's microcode MICROCODE