diff options
Diffstat (limited to 'build/riscv.v')
| -rw-r--r-- | build/riscv.v | 294 |
1 files changed, 294 insertions, 0 deletions
diff --git a/build/riscv.v b/build/riscv.v new file mode 100644 index 0000000..09457da --- /dev/null +++ b/build/riscv.v @@ -0,0 +1,294 @@ +(*Generated by Sail from riscv.*) +Require Import Sail.Base. +Require Import Sail.Real. +Require Import riscv_types. +Import ListNotations. +Open Scope string. +Open Scope bool. +Open Scope Z. + + +Definition is_none {a : Type} (opt : option a) : bool := + match opt with | Some _ => false | None => true end. + +Definition is_some {a : Type} (opt : option a) : bool := + match opt with | Some _ => true | None => false end. + +Definition eq_unit (_ : unit) (_ : unit) : {_bool : bool & ArithFact (_bool)} := build_ex (true). + +Definition neq_int (x : Z) (y : Z) : {_bool : bool & ArithFact (Bool.eqb (negb (x =? y)) _bool)} := + build_ex (negb (Z.eqb x y)). + +Definition neq_bool (x : bool) (y : bool) : bool := negb (Bool.eqb x y). + +Definition __id (x : Z) : {_retval : Z & ArithFact (_retval =? x)} := build_ex (x). + +Definition fdiv_int (n : Z) (m : Z) : Z := + if sumbool_of_bool (andb (Z.ltb n 0) (Z.gtb m 0)) then Z.sub (Z.quot (Z.add n 1) m) 1 + else if sumbool_of_bool (andb (Z.gtb n 0) (Z.ltb m 0)) then Z.sub (Z.quot (Z.sub n 1) m) 1 + else Z.quot n m. + +Definition fmod_int (n : Z) (m : Z) : Z := Z.sub n (Z.mul m (fdiv_int n m)). + +Definition concat_str_bits {n : Z} (str : string) (x : mword n) : string := + String.append str (string_of_bits x). + +Definition concat_str_dec (str : string) (x : Z) : string := String.append str (dec_str x). + + + +Definition sail_mask {v0 : Z} (len : Z) (v : mword v0) `{ArithFact ((len >=? 0) && (v0 >=? 0))} +: mword len := + if sumbool_of_bool (Z.leb len (length_mword v)) then vector_truncate v len else zero_extend v len. + +Definition sail_ones (n : Z) `{ArithFact (n >=? 0)} : mword n := not_vec (zeros n). + +Definition slice_mask (n : Z) (i : Z) (l : Z) `{ArithFact (n >=? 0)} : mword n := + if sumbool_of_bool (Z.geb l n) then shiftl (sail_ones n) i + else + let one : bits n := sail_mask n ('b"1" : bits 1) in + shiftl (sub_vec (shiftl one l) one) i. + +Definition EXTS {n : Z} (m : Z) (v : mword n) `{ArithFact (m >=? n)} : mword m := sign_extend v m. + +Definition EXTZ {n : Z} (m : Z) (v : mword n) `{ArithFact (m >=? n)} : mword m := zero_extend v m. + +Definition zero_reg : regtype := EXTZ 64 (Ox"0" : mword 4). +Hint Unfold zero_reg : sail. +Definition regval_from_reg (r : mword 64) : mword 64 := r. + +Definition regval_into_reg (v : mword 64) : mword 64 := v. + +Definition rX (r : Z) `{ArithFact ((0 <=? r) && (r <? 32))} : M (mword 64) := + let l__32 := r in + (if sumbool_of_bool (Z.eqb l__32 0) then returnm zero_reg + else if sumbool_of_bool (Z.eqb l__32 1) then ((read_reg x1_ref) : M (mword 64)) : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 2) then ((read_reg x2_ref) : M (mword 64)) : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 3) then ((read_reg x3_ref) : M (mword 64)) : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 4) then ((read_reg x4_ref) : M (mword 64)) : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 5) then ((read_reg x5_ref) : M (mword 64)) : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 6) then ((read_reg x6_ref) : M (mword 64)) : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 7) then ((read_reg x7_ref) : M (mword 64)) : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 8) then ((read_reg x8_ref) : M (mword 64)) : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 9) then ((read_reg x9_ref) : M (mword 64)) : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 10) then + ((read_reg x10_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 11) then + ((read_reg x11_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 12) then + ((read_reg x12_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 13) then + ((read_reg x13_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 14) then + ((read_reg x14_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 15) then + ((read_reg x15_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 16) then + ((read_reg x16_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 17) then + ((read_reg x17_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 18) then + ((read_reg x18_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 19) then + ((read_reg x19_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 20) then + ((read_reg x20_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 21) then + ((read_reg x21_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 22) then + ((read_reg x22_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 23) then + ((read_reg x23_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 24) then + ((read_reg x24_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 25) then + ((read_reg x25_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 26) then + ((read_reg x26_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 27) then + ((read_reg x27_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 28) then + ((read_reg x28_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 29) then + ((read_reg x29_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 30) then + ((read_reg x30_ref) : M (mword 64)) + : M (mword 64) + else if sumbool_of_bool (Z.eqb l__32 31) then + ((read_reg x31_ref) : M (mword 64)) + : M (mword 64) + else assert_exp' false "invalid register number" >>= fun _ => exit tt) >>= fun v : regtype => + returnm (regval_from_reg v). + +Definition wX (r : Z) (in_v : mword 64) `{ArithFact ((0 <=? r) && (r <? 32))} : M (unit) := + let v := regval_into_reg in_v in + let l__0 := r in + (if sumbool_of_bool (Z.eqb l__0 0) then returnm tt + else if sumbool_of_bool (Z.eqb l__0 1) then write_reg x1_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 2) then write_reg x2_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 3) then write_reg x3_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 4) then write_reg x4_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 5) then write_reg x5_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 6) then write_reg x6_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 7) then write_reg x7_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 8) then write_reg x8_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 9) then write_reg x9_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 10) then write_reg x10_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 11) then write_reg x11_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 12) then write_reg x12_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 13) then write_reg x13_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 14) then write_reg x14_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 15) then write_reg x15_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 16) then write_reg x16_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 17) then write_reg x17_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 18) then write_reg x18_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 19) then write_reg x19_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 20) then write_reg x20_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 21) then write_reg x21_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 22) then write_reg x22_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 23) then write_reg x23_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 24) then write_reg x24_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 25) then write_reg x25_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 26) then write_reg x26_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 27) then write_reg x27_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 28) then write_reg x28_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 29) then write_reg x29_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 30) then write_reg x30_ref v : M (unit) + else if sumbool_of_bool (Z.eqb l__0 31) then write_reg x31_ref v : M (unit) + else assert_exp' false "invalid register number" >>= fun _ => exit tt) + : M (unit). + +Definition rX_bits (i : mword 5) : M (mword 64) := (rX (projT1 (uint i))) : M (mword 64). + +Definition wX_bits (i : mword 5) (data : mword 64) : M (unit) := + (wX (projT1 (uint i)) data) : M (unit). + +Definition reg_name_abi (r : mword 5) : M (string) := + let b__0 := r in + (if eq_vec b__0 ('b"00000" : mword 5) then returnm "zero" + else if eq_vec b__0 ('b"00001" : mword 5) then returnm "ra" + else if eq_vec b__0 ('b"00010" : mword 5) then returnm "sp" + else if eq_vec b__0 ('b"00011" : mword 5) then returnm "gp" + else if eq_vec b__0 ('b"00100" : mword 5) then returnm "tp" + else if eq_vec b__0 ('b"00101" : mword 5) then returnm "t0" + else if eq_vec b__0 ('b"00110" : mword 5) then returnm "t1" + else if eq_vec b__0 ('b"00111" : mword 5) then returnm "t2" + else if eq_vec b__0 ('b"01000" : mword 5) then returnm "fp" + else if eq_vec b__0 ('b"01001" : mword 5) then returnm "s1" + else if eq_vec b__0 ('b"01010" : mword 5) then returnm "a0" + else if eq_vec b__0 ('b"01011" : mword 5) then returnm "a1" + else if eq_vec b__0 ('b"01100" : mword 5) then returnm "a2" + else if eq_vec b__0 ('b"01101" : mword 5) then returnm "a3" + else if eq_vec b__0 ('b"01110" : mword 5) then returnm "a4" + else if eq_vec b__0 ('b"01111" : mword 5) then returnm "a5" + else if eq_vec b__0 ('b"10000" : mword 5) then returnm "a6" + else if eq_vec b__0 ('b"10001" : mword 5) then returnm "a7" + else if eq_vec b__0 ('b"10010" : mword 5) then returnm "s2" + else if eq_vec b__0 ('b"10011" : mword 5) then returnm "s3" + else if eq_vec b__0 ('b"10100" : mword 5) then returnm "s4" + else if eq_vec b__0 ('b"10101" : mword 5) then returnm "s5" + else if eq_vec b__0 ('b"10110" : mword 5) then returnm "s6" + else if eq_vec b__0 ('b"10111" : mword 5) then returnm "s7" + else if eq_vec b__0 ('b"11000" : mword 5) then returnm "s8" + else if eq_vec b__0 ('b"11001" : mword 5) then returnm "s9" + else if eq_vec b__0 ('b"11010" : mword 5) then returnm "s10" + else if eq_vec b__0 ('b"11011" : mword 5) then returnm "s11" + else if eq_vec b__0 ('b"11100" : mword 5) then returnm "t3" + else if eq_vec b__0 ('b"11101" : mword 5) then returnm "t4" + else if eq_vec b__0 ('b"11110" : mword 5) then returnm "t5" + else if eq_vec b__0 ('b"11111" : mword 5) then returnm "t6" + else + assert_exp' false "Pattern match failure at riscv_regs.sail 160:2 - 193:3" >>= fun _ => + exit tt) + : M (string). + +Definition init_base_regs '(tt : unit) : M (unit) := + write_reg x1_ref zero_reg >> + write_reg x2_ref zero_reg >> + write_reg x3_ref zero_reg >> + write_reg x4_ref zero_reg >> + write_reg x5_ref zero_reg >> + write_reg x6_ref zero_reg >> + write_reg x7_ref zero_reg >> + write_reg x8_ref zero_reg >> + write_reg x9_ref zero_reg >> + write_reg x10_ref zero_reg >> + write_reg x11_ref zero_reg >> + write_reg x12_ref zero_reg >> + write_reg x13_ref zero_reg >> + write_reg x14_ref zero_reg >> + write_reg x15_ref zero_reg >> + write_reg x16_ref zero_reg >> + write_reg x17_ref zero_reg >> + write_reg x18_ref zero_reg >> + write_reg x19_ref zero_reg >> + write_reg x20_ref zero_reg >> + write_reg x21_ref zero_reg >> + write_reg x22_ref zero_reg >> + write_reg x23_ref zero_reg >> + write_reg x24_ref zero_reg >> + write_reg x25_ref zero_reg >> + write_reg x26_ref zero_reg >> + write_reg x27_ref zero_reg >> + write_reg x28_ref zero_reg >> + write_reg x29_ref zero_reg >> + write_reg x30_ref zero_reg >> write_reg x31_ref zero_reg : M (unit). + +Definition initial_regstate : regstate := +{| x31 := (Ox"0000000000000000" : mword 64); + x30 := (Ox"0000000000000000" : mword 64); + x29 := (Ox"0000000000000000" : mword 64); + x28 := (Ox"0000000000000000" : mword 64); + x27 := (Ox"0000000000000000" : mword 64); + x26 := (Ox"0000000000000000" : mword 64); + x25 := (Ox"0000000000000000" : mword 64); + x24 := (Ox"0000000000000000" : mword 64); + x23 := (Ox"0000000000000000" : mword 64); + x22 := (Ox"0000000000000000" : mword 64); + x21 := (Ox"0000000000000000" : mword 64); + x20 := (Ox"0000000000000000" : mword 64); + x19 := (Ox"0000000000000000" : mword 64); + x18 := (Ox"0000000000000000" : mword 64); + x17 := (Ox"0000000000000000" : mword 64); + x16 := (Ox"0000000000000000" : mword 64); + x15 := (Ox"0000000000000000" : mword 64); + x14 := (Ox"0000000000000000" : mword 64); + x13 := (Ox"0000000000000000" : mword 64); + x12 := (Ox"0000000000000000" : mword 64); + x11 := (Ox"0000000000000000" : mword 64); + x10 := (Ox"0000000000000000" : mword 64); + x9 := (Ox"0000000000000000" : mword 64); + x8 := (Ox"0000000000000000" : mword 64); + x7 := (Ox"0000000000000000" : mword 64); + x6 := (Ox"0000000000000000" : mword 64); + x5 := (Ox"0000000000000000" : mword 64); + x4 := (Ox"0000000000000000" : mword 64); + x3 := (Ox"0000000000000000" : mword 64); + x2 := (Ox"0000000000000000" : mword 64); + x1 := (Ox"0000000000000000" : mword 64); + instbits := (Ox"0000000000000000" : mword 64); + nextPC := (Ox"0000000000000000" : mword 64); + PC := (Ox"0000000000000000" : mword 64) |}. +Hint Unfold initial_regstate : sail. + + |