diff options
| author | Alasdair Armstrong | 2017-07-17 16:18:24 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-07-17 16:19:22 +0100 |
| commit | 6c75d9386a9c179969c22baf1231f1bd7b9a60a3 (patch) | |
| tree | 1280878478152fd7cb67756703063b54ec8177ac | |
| parent | c83a57f1abd967c0b808ee9b3108445954ccfd65 (diff) | |
Fixed multiply for MIPS in prelude so it correctly doubles bitvector
length, and removed redundant calls to extension functions.
| -rw-r--r-- | lib/prelude.sail | 4 | ||||
| -rw-r--r-- | mips_new_tc/mips_insts.sail | 12 |
2 files changed, 8 insertions, 8 deletions
diff --git a/lib/prelude.sail b/lib/prelude.sail index 48160749..bb19aa8d 100644 --- a/lib/prelude.sail +++ b/lib/prelude.sail @@ -150,7 +150,7 @@ val bool -> bit effect pure bool_to_bit val (int, int) -> int effect pure mul_int val forall Num 'n, Num 'o, Order 'ord. - (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure mul_vec + (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<2 * 'n - 1, 2 * 'n, 'ord, bit> effect pure mul_vec overload (deinfix * ) [ mul_vec; @@ -158,7 +158,7 @@ overload (deinfix * ) [ ] val forall Num 'n, Num 'o, Order 'ord. - (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<'o, 'n, 'ord, bit> effect pure mul_svec + (vector<'o, 'n, 'ord, bit>, vector<'o, 'n, 'ord, bit>) -> vector<2 * 'n - 1, 2 * 'n, 'ord, bit> effect pure mul_svec overload (deinfix *_s) [ mul_svec diff --git a/mips_new_tc/mips_insts.sail b/mips_new_tc/mips_insts.sail index ffc98981..1d3c5f4a 100644 --- a/mips_new_tc/mips_insts.sail +++ b/mips_new_tc/mips_insts.sail @@ -702,7 +702,7 @@ function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : Some(DMULT(rs, rt)) function clause execute (DMULT(rs, rt)) = { - (bit[128]) result := (exts (rGPR(rs))) *_s (exts (rGPR(rt))); + (bit[128]) result := rGPR(rs) *_s rGPR(rt); HI := (result[127..64]); LO := (result[63..0]); } @@ -713,7 +713,7 @@ function clause decode (0b000000 : (regno) rs : (regno) rt : 0b00000 : 0b00000 : Some(DMULTU(rs, rt)) function clause execute (DMULTU(rs, rt)) = { - (bit[128]) result := (extz (rGPR(rs))) * (extz (rGPR(rt))); + (bit[128]) result := rGPR(rs) * rGPR(rt); HI := (result[127..64]); LO := (result[63..0]); } @@ -729,7 +729,7 @@ function clause execute (MADD(rs, rt)) = (bit[64]) mul_result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then undefined else - ((exts (rsVal[31..0])) *_s (exts (rtVal[31..0]))); + rsVal[31..0] *_s rtVal[31..0]; (bit[64]) result := mul_result + (HI[31..0] : LO[31..0]); HI := EXTS(result[63..32]); LO := EXTS(result[31..0]); @@ -746,7 +746,7 @@ function clause execute (MADDU(rs, rt)) = (bit[64]) mul_result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then undefined else - ((extz (rsVal[31..0])) * (extz (rtVal[31..0]))); + rsVal[31..0] * rtVal[31..0]; (bit[64]) result := mul_result + (HI[31..0] : LO[31..0]); HI := EXTS(result[63..32]); LO := EXTS(result[31..0]); @@ -763,7 +763,7 @@ function clause execute (MSUB(rs, rt)) = (bit[64]) mul_result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then undefined else - ((exts (rsVal[31..0])) *_s (exts (rtVal[31..0]))); + rsVal[31..0] *_s rtVal[31..0]; (bit[64]) result := (HI[31..0] : LO[31..0]) - mul_result; HI := EXTS(result[63..32]); LO := EXTS(result[31..0]); @@ -780,7 +780,7 @@ function clause execute (MSUBU(rs, rt)) = (bit[64]) mul_result := if (NotWordVal(rsVal) | NotWordVal(rtVal)) then undefined else - ((extz (rsVal[31..0])) * (extz (rtVal[31..0]))); + rsVal[31..0] * rtVal[31..0]; (bit[64]) result := (HI[31..0] : LO[31..0]) - mul_result; HI := EXTS(result[63..32]); LO := EXTS(result[31..0]); |