diff options
| author | Prashanth Mundkur | 2018-05-21 15:33:02 -0700 |
|---|---|---|
| committer | Prashanth Mundkur | 2018-05-21 18:00:03 -0700 |
| commit | 715edc44ce58bd2d4f3b2206623fe89f65118ad5 (patch) | |
| tree | 04b76c2fa0f399446abe2a8a584e04302213cc9c /riscv/prelude.sail | |
| parent | b55481d0bafff8520ff6872dbca4ca616bce41ac (diff) | |
Add in the platform files and update the ocaml build. Disable the isabelle build until we add suitable platform definitions/stubs.
The platform bits are not yet hooked into the model, but only into the build, so are untested.
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 c92497c1..c6fb1054 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -401,3 +401,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] + +/* Copied from arith.sail. */ +val mult_atom = {ocaml: "mult", lem: "integerMult", c: "mult_int"} : forall 'n 'm. + (atom('n), atom('m)) -> atom('n * 'm) |