diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/arith.sail | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/lib/arith.sail b/lib/arith.sail index 61a1ff76..e61ec473 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -50,7 +50,25 @@ val "prerr_int" : (string, int) -> unit // ***** Integer shifts ***** -val shl_int = "shl_int" : (int, int) -> int +/*! +A common idiom in asl is to take two bits of an opcode and convert in into a variable like +``` +let elsize = shl_int(8, UInt(size)) +``` +THIS ensures that in this case the typechecker knows that the end result will be a value in the set `{8, 16, 32, 64}` +*/ +val _shl8 = "shl_int" : + forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> int('m) with 'm in {8, 16, 32, 64} + +/*! +Similarly, we can shift 32 by either 0 or 1 to get a value in `{32, 64}` +*/ +val _shl32 = "shl_int" : + forall 'n, 'n in {0, 1}. (int(32), int('n)) -> int('m) with 'm in {32, 64} + +val _shl_int = "shl_int" : (int, int) -> int + +overload shl_int = {_shl8, _shl32, _shl_int} val shr_int = "shr_int" : (int, int) -> int |