1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
|
register (vector <0, 63, inc, bit>) GPR0
register (vector <0, 63, inc, bit>) GPR1
register (vector <0, 63, inc, bit>) GPR2
register (vector <0, 63, inc, bit>) GPR3
register (vector <0, 63, inc, bit>) GPR4
register (vector <0, 63, inc, bit>) GPR5
register (vector <0, 63, inc, bit>) GPR6
register (vector <0, 63, inc, bit>) GPR7
register (vector <0, 63, inc, bit>) GPR8
register (vector <0, 63, inc, bit>) GPR9
register (vector <0, 63, inc, bit>) GPR10
register (vector <0, 63, inc, bit>) GPR11
register (vector <0, 63, inc, bit>) GPR12
register (vector <0, 63, inc, bit>) GPR13
register (vector <0, 63, inc, bit>) GPR14
register (vector <0, 63, inc, bit>) GPR15
register (vector <0, 63, inc, bit>) GPR16
register (vector <0, 63, inc, bit>) GPR17
register (vector <0, 63, inc, bit>) GPR18
register (vector <0, 63, inc, bit>) GPR19
register (vector <0, 63, inc, bit>) GPR20
register (vector <0, 63, inc, bit>) GPR21
register (vector <0, 63, inc, bit>) GPR22
register (vector <0, 63, inc, bit>) GPR23
register (vector <0, 63, inc, bit>) GPR24
register (vector <0, 63, inc, bit>) GPR25
register (vector <0, 63, inc, bit>) GPR26
register (vector <0, 63, inc, bit>) GPR27
register (vector <0, 63, inc, bit>) GPR28
register (vector <0, 63, inc, bit>) GPR29
register (vector <0, 63, inc, bit>) GPR30
register (vector <0, 63, inc, bit>) GPR31
let (vector <0, 32, inc, (register<(vector<0, 63, inc, bit>)>) >) GPR =
[ GPR0, GPR1, GPR2, GPR3, GPR4, GPR5, GPR6, GPR7, GPR8, GPR9, GPR10,
GPR11, GPR12, GPR13, GPR14, GPR15, GPR16, GPR17, GPR18, GPR19, GPR20,
GPR21, GPR22, GPR23, GPR24, GPR25, GPR26, GPR27, GPR28, GPR29, GPR30, GPR31
]
register (bit[64]) NIA (* next instruction address *)
register (bit[64]) CIA (* current instruction address *)
(* XXX endianess; also, bit[64] translates to 0:64, not 0:63??? *)
register (bit[32 : 63]) CR
register (bit[64]) CTR
register (bit[64]) LR
register (bit[64]) XER
let nat SO = 32
let nat OV = 33
let nat CA = 34
val extern ( nat * nat ) -> (bit[64]) effect { wmem , rmem } MEM
register bool mode64bit
scattered function unit execute
scattered typedef ast = const union
scattered function ast decode
union ast member bit [ 4 ] (* RA *) * bit [ 4 ] (* RT *) * bit [ 15 ] (* SI *) AddImmediate
function clause decode (([ 0 = bitzero, 1 = bitzero, 2 = bitone, 3 = bitone, 4 = bitone, 5 = bitzero ] as instr)) =
AddImmediate ( instr[11..15] (* RA *), instr[6..10] (* RT *), instr[16..31] (* SI *) )
function clause execute ( AddImmediate ( RA, RT, SI ) ) =
{
if ( RA == 0 ) then GPR[ RT ] := ( ( SI )) else GPR[ RT ] := ( (GPR[ RA ]) + ( ( SI )) ) ;
}
union ast member bit [ 1 ] (* BH *) * bit [ 4 ] (* BI *) * bit [ 4 ] (* BO *) * bit (* LK *) BranchConditionaltoLinkRegister
function clause decode (([ 0 = bitzero, 1 = bitone, 2 = bitzero, 3 = bitzero, 4 = bitone, 5 = bitone, 21 = bitzero, 22 = bitzero, 23 = bitzero, 24 = bitzero, 25 = bitzero, 26 = bitone, 27 = bitzero, 28 = bitzero, 29 = bitzero, 30 = bitzero ] as instr)) =
BranchConditionaltoLinkRegister ( instr[19..20] (* BH *), instr[11..15] (* BI *), instr[6..10] (* BO *), instr[31] (* LK *) )
function clause execute ( BranchConditionaltoLinkRegister ( BH, BI, BO, LK ) ) =
{
if mode64bit then M := 0 else M := 32 ;
if ( ~ ( (( BO )[ 2 ]) )) then CTR := ( CTR - 1 ) ;
ctr_ok := ( (( BO )[ 2 ]) | ( ( (( CTR )[ M .. 63 ]) != 0 ) ^ (( BO )[ 3 ]) ) ) ;
cond_ok := ( (( BO )[ 0 ]) | ( (( CR )[ ( BI + 32 ) ]) ^ ( ~ ( (( BO )[ 1 ]) )) ) ) ;
if ( ctr_ok & cond_ok ) then NIA := ( (( LR )[ 0 .. 61 ]) : 0b00 ) ;
if LK then LR := ( CIA + 4 ) ;
}
union ast member bit [ 15 ] (* D *) * bit [ 4 ] (* RA *) * bit [ 4 ] (* RT *) LoadWordandZero
function clause decode (([ 0 = bitone, 1 = bitzero, 2 = bitzero, 3 = bitzero, 4 = bitzero, 5 = bitzero ] as instr)) =
LoadWordandZero ( instr[16..31] (* D *), instr[11..15] (* RA *), instr[6..10] (* RT *) )
function clause execute ( LoadWordandZero ( D, RA, RT ) ) =
{
if ( RA == 0 ) then b := 0 else b := (GPR[ RA ]) ;
EA := ( b + ( ( D )) ) ;
GPR[ RT ] := ( 0b00000000000000000000000000000000 : MEM( EA , 4 ) ) ;
}
union ast member bit [ 4 ] (* RA *) * bit [ 4 ] (* RB *) * bit [ 4 ] (* RS *) * bit (* Rc *) OR
function clause decode (([ 0 = bitzero, 1 = bitone, 2 = bitone, 3 = bitone, 4 = bitone, 5 = bitone, 21 = bitzero, 22 = bitone, 23 = bitone, 24 = bitzero, 25 = bitone, 26 = bitone, 27 = bitone, 28 = bitone, 29 = bitzero, 30 = bitzero ] as instr)) =
OR ( instr[11..15] (* RA *), instr[16..20] (* RB *), instr[6..10] (* RS *), instr[31] (* Rc *) )
function clause execute ( OR ( RA, RB, RS, Rc ) ) =
GPR[ RA ] := ( (GPR[ RS ]) | (GPR[ RB ]) )
union ast member bit [ 15 ] (* D *) * bit [ 4 ] (* RA *) * bit [ 4 ] (* RS *) StoreWord
function clause decode (([ 0 = bitone, 1 = bitzero, 2 = bitzero, 3 = bitone, 4 = bitzero, 5 = bitzero ] as instr)) =
StoreWord ( instr[16..31] (* D *), instr[11..15] (* RA *), instr[6..10] (* RS *) )
function clause execute ( StoreWord ( D, RA, RS ) ) =
{
(bit[64]) b := 0;
if ( RA == 0 ) then b := 0 else b := (GPR[ RA ]) ;
EA := ( b + ( ( D )) ) ;
MEM( EA , 4 ) := (( (GPR[ RS ]) )[ 32 .. 63 ]) ;
}
union ast member bit [ 15 ] (* D *) * bit [ 4 ] (* RA *) * bit [ 4 ] (* RS *) StoreWordwithUpdate
function clause decode (([ 0 = bitone, 1 = bitzero, 2 = bitzero, 3 = bitone, 4 = bitzero, 5 = bitone ] as instr)) =
StoreWordwithUpdate ( instr[16..31] (* D *), instr[11..15] (* RA *), instr[6..10] (* RS *) )
function clause execute ( StoreWordwithUpdate ( D, RA, RS ) ) =
{
EA := ( (GPR[ RA ]) + ( ( D )) ) ;
MEM( EA , 4 ) := (( (GPR[ RS ]) )[ 32 .. 63 ]) ;
GPR[ RA ] := EA ;
}
end decode
end execute
end ast
register ast instr (* monitor decoded instructions *)
(* fetch-decode-execute loop *)
function rec unit fde_loop () = {
NIA := CIA + 4;
instr := decode(MEM(CIA, 4));
execute(instr);
CIA := NIA;
fde_loop ()
}
function unit init() = {
(* CIA is initialiazed externally, as well as MEM *)
GPR1 := 0;
GPR31 := 0;
}
function unit main () = {
init();
fde_loop();
}
|
