diff options
| author | Brian Campbell | 2018-08-15 18:53:06 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-08-15 18:53:06 +0100 |
| commit | 5d3c6b295ca18efd8ca8c9e52245766f2c2c7394 (patch) | |
| tree | fb398ff46476a1a2949614f689c5024ac0e31782 /riscv/prelude.sail | |
| parent | 8d4bb9daefaf6dd28826e8da7e6c3a94f53bcefd (diff) | |
Temporary fix for RISC-V Lem generation
Diffstat (limited to 'riscv/prelude.sail')
| -rw-r--r-- | riscv/prelude.sail | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index d5c133fc..88bc00fb 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -496,3 +496,7 @@ function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) = function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) = let v64 : bits(64) = EXTS(v) in (v64 >> shift)[31..0] + +/* Special version of zero_extend that the Lem back-end knows will be at a + case split on 'm and uses a more generic type for. (Temporary hack, honest) */ +val zero_extend_type_hack = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) |