diff options
| author | Robert Norton | 2016-05-12 12:03:54 +0100 |
|---|---|---|
| committer | Robert Norton | 2016-05-12 12:03:54 +0100 |
| commit | 326683143803c615b7d1ede0107eb0a2f13ea56f (patch) | |
| tree | 2837b5c87372aaee674c08cfe784c11c75fef07f | |
| parent | 19a026fb51378c727d6f2da70bc828b796ab514d (diff) | |
update/add some comments
| -rw-r--r-- | mips/mips_prelude.sail | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail index c338adf1..a8d3f8d5 100644 --- a/mips/mips_prelude.sail +++ b/mips/mips_prelude.sail @@ -34,14 +34,14 @@ register (bit[64]) CP0BadVAddr typedef StatusReg = register bits [31:0] { 31 .. 28 : CU; (* co-processor enable bits *) (* RP/FR/RE/MX/PX not implemented *) - 22 : BEV; (* use boot exception vectors XXX initialise to one *) + 22 : BEV; (* use boot exception vectors (initialised to one) *) (* TS/SR/NMI not implemented *) 15 .. 8 : IM; (* Interrupt mask *) 7 : KX; (* kernel 64-bit enable *) 6 : SX; (* supervisor 64-bit enable *) 5 : UX; (* user 64-bit enable *) 4 .. 3 : KSU; (* Processor mode *) - 2 : ERL; (* error level XXX initialise to one *) + 2 : ERL; (* error level (should be initialised to one, but BERI is different) *) 1 : EXL; (* exception level *) 0 : IE; (* interrupt enable *) } @@ -102,11 +102,13 @@ val bit[64] -> bool effect pure NotWordVal function bool NotWordVal (word) = (word[31] ^^ 32) != word[63..32] +(* Read numbered GP reg. ($0 always zero) *) val bit[5] -> bit[64] effect {rreg} rGPR function bit[64] rGPR idx = { if idx == 0 then 0 else GPR[idx] } +(* Write numbered GP reg. (writes to $0 ignored) *) val (bit[5], bit[64]) -> unit effect {wreg} wGPR function unit wGPR (idx, v) = { if idx == 0 then () else GPR[idx] := v |