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
|
(* XXX types are wrong *)
val extern forall Type 'a, Type 'b, Type 'c . ( 'a * 'b ) -> 'c effect pure (deinfix + ) = "add"
val extern forall Type 'a . ( 'a * 'a ) -> 'a effect pure (deinfix mod ) = "mod"
val extern forall Type 'a, Type 'b, Type 'c .
( 'a * 'b ) -> 'c effect pure (deinfix : ) = "vec_concat"
val extern forall Type 'a . 'a -> nat effect pure to_num_inc = "to_num_inc"
val extern forall Type 'a . 'a -> nat effect pure to_num_dec = "to_num_dec"
val extern forall Type 'a . nat -> 'a effect pure to_vec_inc = "to_vec_inc"
val extern forall Type 'a . nat -> 'a effect pure to_vec_dec = "to_vec_dec"
val extern forall Type 'a . ( 'a * 'a ) -> bit effect pure (deinfix == ) = "eq"
val extern forall Type 'a . ( 'a * 'a ) -> bit effect pure (deinfix != ) = "neq"
val extern forall Type 'a . 'a -> 'a effect pure (deinfix ~ ) = "bitwise-not"
val extern forall Type 'a . ( 'a * 'a ) -> 'a effect pure (deinfix ^ ) = "bitwise-xor"
val extern forall Type 'a . ( 'a * 'a ) -> 'a effect pure (deinfix || ) = "bitwise-or"
val extern forall Type 'a . ( 'a * 'a ) -> 'a effect pure (deinfix & ) = "bitwise-and"
val extern bit -> bool effect pure is_one = "is_one"
(* XXX sign extension *)
function forall Type 'a . 'a exts ( x ) = x
register (vector<0, 16, inc, (vector<0, 63, inc, bit>)> ) GPR
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 ] := ( exts ( SI )) else GPR[ RT ] := ( (GPR[ RA ]) + ( exts ( 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 + ( exts ( 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 ) ) =
{
if ( RA == 0 ) then b := 0 else b := (GPR[ RA ]) ;
EA := ( b + ( exts ( 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 ]) + ( exts ( D )) ) ;
MEM( EA , 4 ) := (( (GPR[ RS ]) )[ 32 .. 63 ]) ;
GPR[ RA ] := EA ;
}
end decode
end execute
end ast
register ast instr (* monitor decoded instructions *)
function rec unit main () = {
NIA := CIA + 4;
instr := decode(MEM(CIA, 4));
execute(instr);
CIA := NIA;
main ()
}
|
