diff options
Diffstat (limited to 'model')
34 files changed, 2331 insertions, 1663 deletions
diff --git a/model/main.sail b/model/main.sail index a72eb3f..c349b3f 100644 --- a/model/main.sail +++ b/model/main.sail @@ -3,11 +3,10 @@ val main : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wre function main () = { // PC = __GetSlice_int(64, elf_entry(), 0); - PC = zero_extend(0x1000, 64); + PC = sail_zero_extend(0x1000, sizeof(xlen)); print_bits("PC = ", PC); try { - init_platform(); - init_sys(); + init_model(); loop() } catch { Error_not_implemented(s) => print_string("Error: Not implemented: ", s), diff --git a/model/main_rvfi.sail b/model/main_rvfi.sail index 0ba4acf..10b5428 100644 --- a/model/main_rvfi.sail +++ b/model/main_rvfi.sail @@ -4,19 +4,19 @@ val rvfi_fetch : unit -> FetchResult effect {escape, rmem, rreg, wmv, wreg} function rvfi_fetch() = /* check for legal PC */ - if (PC[0] != 0b0 | (PC[1] != 0b0 & (~ (haveRVC())))) + if (PC[0] != 0b0 | (PC[1] != 0b0 & (~ (haveRVC())))) then F_Error(E_Fetch_Addr_Align, PC) else { let i = rvfi_instruction.rvfi_insn(); rvfi_exec->rvfi_order() = minstret; rvfi_exec->rvfi_pc_rdata() = PC; - rvfi_exec->rvfi_insn() = zero_extend(i,64); + rvfi_exec->rvfi_insn() = sail_zero_extend(i,64); /* TODO: should we write these even if they're not really registers? */ rvfi_exec->rvfi_rs1_data() = X(i[19 .. 15]); rvfi_exec->rvfi_rs2_data() = X(i[24 .. 20]); - rvfi_exec->rvfi_rs1_addr() = zero_extend(i[19 .. 15],8); - rvfi_exec->rvfi_rs2_addr() = zero_extend(i[24 .. 20],8); - if (i[1 .. 0] == 0b11) + rvfi_exec->rvfi_rs1_addr() = sail_zero_extend(i[19 .. 15],8); + rvfi_exec->rvfi_rs2_addr() = sail_zero_extend(i[24 .. 20],8); + if (i[1 .. 0] == 0b11) then F_Base(i) else F_RVC(i[15 .. 0]) } @@ -29,7 +29,7 @@ val rvfi_step : int -> bool effect {barr, eamem, escape, exmem, rmem, rreg, wmv, function rvfi_step(step_no) = { minstret_written = false; /* see note for minstret */ let (retired, stepped) : (bool, bool) = - match curInterrupt(cur_privilege, mip, mie, mideleg) { + match dispatchInterrupt(cur_privilege) { Some(intr, priv) => { print_bits("Handling interrupt: ", intr); handle_interrupt(intr, priv); @@ -51,8 +51,13 @@ function rvfi_step(step_no) = { }, Some(ast) => { print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ ast); - nextPC = PC + 2; - (execute(ast), true) + /* check for RVC once here instead of every RVC execute clause. */ + if haveRVC() then { + nextPC = PC + 2; + (execute(ast), true) + } else { + (false, true) + } } } }, @@ -95,11 +100,10 @@ function main () = { rvfi_zero_exec_packet(); rvfi_halt_exec_packet(); let _ = rvfi_get_exec_packet(); - PC = zero_extend(0x1000, 64); + PC = sail_zero_extend(0x1000, 64); print_bits("PC = ", PC); try { - init_platform(); - init_sys(); + init_model(); loop() } catch { Error_not_implemented(s) => print_string("Error: Not implemented: ", s), diff --git a/model/prelude.sail b/model/prelude.sail index 806562c..73f96b0 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -1,779 +1,37 @@ default Order dec -$include <flow.sail> - -type bits ('n : Int) = vector('n, dec, bit) -union option ('a : Type) = {None : unit, Some : 'a} - +$include <option.sail> +$include <arith.sail> +$include <string.sail> +$include <vector_dec.sail> $include <regfp.sail> -val spc : unit <-> string -val opt_spc : unit <-> string -val def_spc : unit <-> string - -val hex_bits : forall 'n . (atom('n), bits('n)) <-> string - val string_startswith = "string_startswith" : (string, string) -> bool val string_drop = "string_drop" : (string, nat) -> string val string_take = "string_take" : (string, nat) -> string val string_length = "string_length" : string -> nat val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string -val maybe_int_of_prefix = "maybe_int_of_prefix" : string -> option((int, nat)) -val maybe_nat_of_prefix = "maybe_nat_of_prefix" : string -> option((nat, nat)) -val maybe_int_of_string = "maybe_int_of_string" : string -> option(int) - -/* Python: -f = """val hex_bits_{0} : bits({0}) <-> string -val hex_bits_{0}_forwards = "decimal_string_of_bits" : bits({0}) -> string -val hex_bits_{0}_forwards_matches : bits({0}) -> bool -function hex_bits_{0}_forwards_matches bv = true -val "hex_bits_{0}_matches_prefix" : string -> option((bits({0}), nat)) -val hex_bits_{0}_backwards_matches : string -> bool -function hex_bits_{0}_backwards_matches s = match s {{ - s if match hex_bits_{0}_matches_prefix(s) {{ - Some (_, n) if n == string_length(s) => true, - _ => false - }} => true, - _ => false -}} -val hex_bits_{0}_backwards : string -> bits({0}) -function hex_bits_{0}_backwards s = - match hex_bits_{0}_matches_prefix(s) {{ - Some (bv, n) if n == string_length(s) => bv - }} -""" - -for i in list(range(1, 34)) + [48, 64]: - print(f.format(i)) - -*/ -val hex_bits_1 : bits(1) <-> string -val hex_bits_1_forwards = "decimal_string_of_bits" : bits(1) -> string -val hex_bits_1_forwards_matches : bits(1) -> bool -function hex_bits_1_forwards_matches bv = true -val "hex_bits_1_matches_prefix" : string -> option((bits(1), nat)) -val hex_bits_1_backwards_matches : string -> bool -function hex_bits_1_backwards_matches s = match s { - s if match hex_bits_1_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_1_backwards : string -> bits(1) -function hex_bits_1_backwards s = - match hex_bits_1_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_2 : bits(2) <-> string -val hex_bits_2_forwards = "decimal_string_of_bits" : bits(2) -> string -val hex_bits_2_forwards_matches : bits(2) -> bool -function hex_bits_2_forwards_matches bv = true -val "hex_bits_2_matches_prefix" : string -> option((bits(2), nat)) -val hex_bits_2_backwards_matches : string -> bool -function hex_bits_2_backwards_matches s = match s { - s if match hex_bits_2_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_2_backwards : string -> bits(2) -function hex_bits_2_backwards s = - match hex_bits_2_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_3 : bits(3) <-> string -val hex_bits_3_forwards = "decimal_string_of_bits" : bits(3) -> string -val hex_bits_3_forwards_matches : bits(3) -> bool -function hex_bits_3_forwards_matches bv = true -val "hex_bits_3_matches_prefix" : string -> option((bits(3), nat)) -val hex_bits_3_backwards_matches : string -> bool -function hex_bits_3_backwards_matches s = match s { - s if match hex_bits_3_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_3_backwards : string -> bits(3) -function hex_bits_3_backwards s = - match hex_bits_3_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_4 : bits(4) <-> string -val hex_bits_4_forwards = "decimal_string_of_bits" : bits(4) -> string -val hex_bits_4_forwards_matches : bits(4) -> bool -function hex_bits_4_forwards_matches bv = true -val "hex_bits_4_matches_prefix" : string -> option((bits(4), nat)) -val hex_bits_4_backwards_matches : string -> bool -function hex_bits_4_backwards_matches s = match s { - s if match hex_bits_4_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_4_backwards : string -> bits(4) -function hex_bits_4_backwards s = - match hex_bits_4_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_5 : bits(5) <-> string -val hex_bits_5_forwards = "decimal_string_of_bits" : bits(5) -> string -val hex_bits_5_forwards_matches : bits(5) -> bool -function hex_bits_5_forwards_matches bv = true -val "hex_bits_5_matches_prefix" : string -> option((bits(5), nat)) -val hex_bits_5_backwards_matches : string -> bool -function hex_bits_5_backwards_matches s = match s { - s if match hex_bits_5_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_5_backwards : string -> bits(5) -function hex_bits_5_backwards s = - match hex_bits_5_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_6 : bits(6) <-> string -val hex_bits_6_forwards = "decimal_string_of_bits" : bits(6) -> string -val hex_bits_6_forwards_matches : bits(6) -> bool -function hex_bits_6_forwards_matches bv = true -val "hex_bits_6_matches_prefix" : string -> option((bits(6), nat)) -val hex_bits_6_backwards_matches : string -> bool -function hex_bits_6_backwards_matches s = match s { - s if match hex_bits_6_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_6_backwards : string -> bits(6) -function hex_bits_6_backwards s = - match hex_bits_6_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_7 : bits(7) <-> string -val hex_bits_7_forwards = "decimal_string_of_bits" : bits(7) -> string -val hex_bits_7_forwards_matches : bits(7) -> bool -function hex_bits_7_forwards_matches bv = true -val "hex_bits_7_matches_prefix" : string -> option((bits(7), nat)) -val hex_bits_7_backwards_matches : string -> bool -function hex_bits_7_backwards_matches s = match s { - s if match hex_bits_7_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_7_backwards : string -> bits(7) -function hex_bits_7_backwards s = - match hex_bits_7_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_8 : bits(8) <-> string -val hex_bits_8_forwards = "decimal_string_of_bits" : bits(8) -> string -val hex_bits_8_forwards_matches : bits(8) -> bool -function hex_bits_8_forwards_matches bv = true -val "hex_bits_8_matches_prefix" : string -> option((bits(8), nat)) -val hex_bits_8_backwards_matches : string -> bool -function hex_bits_8_backwards_matches s = match s { - s if match hex_bits_8_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_8_backwards : string -> bits(8) -function hex_bits_8_backwards s = - match hex_bits_8_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_9 : bits(9) <-> string -val hex_bits_9_forwards = "decimal_string_of_bits" : bits(9) -> string -val hex_bits_9_forwards_matches : bits(9) -> bool -function hex_bits_9_forwards_matches bv = true -val "hex_bits_9_matches_prefix" : string -> option((bits(9), nat)) -val hex_bits_9_backwards_matches : string -> bool -function hex_bits_9_backwards_matches s = match s { - s if match hex_bits_9_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_9_backwards : string -> bits(9) -function hex_bits_9_backwards s = - match hex_bits_9_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_10 : bits(10) <-> string -val hex_bits_10_forwards = "decimal_string_of_bits" : bits(10) -> string -val hex_bits_10_forwards_matches : bits(10) -> bool -function hex_bits_10_forwards_matches bv = true -val "hex_bits_10_matches_prefix" : string -> option((bits(10), nat)) -val hex_bits_10_backwards_matches : string -> bool -function hex_bits_10_backwards_matches s = match s { - s if match hex_bits_10_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_10_backwards : string -> bits(10) -function hex_bits_10_backwards s = - match hex_bits_10_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_11 : bits(11) <-> string -val hex_bits_11_forwards = "decimal_string_of_bits" : bits(11) -> string -val hex_bits_11_forwards_matches : bits(11) -> bool -function hex_bits_11_forwards_matches bv = true -val "hex_bits_11_matches_prefix" : string -> option((bits(11), nat)) -val hex_bits_11_backwards_matches : string -> bool -function hex_bits_11_backwards_matches s = match s { - s if match hex_bits_11_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_11_backwards : string -> bits(11) -function hex_bits_11_backwards s = - match hex_bits_11_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_12 : bits(12) <-> string -val hex_bits_12_forwards = "decimal_string_of_bits" : bits(12) -> string -val hex_bits_12_forwards_matches : bits(12) -> bool -function hex_bits_12_forwards_matches bv = true -val "hex_bits_12_matches_prefix" : string -> option((bits(12), nat)) -val hex_bits_12_backwards_matches : string -> bool -function hex_bits_12_backwards_matches s = match s { - s if match hex_bits_12_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_12_backwards : string -> bits(12) -function hex_bits_12_backwards s = - match hex_bits_12_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_13 : bits(13) <-> string -val hex_bits_13_forwards = "decimal_string_of_bits" : bits(13) -> string -val hex_bits_13_forwards_matches : bits(13) -> bool -function hex_bits_13_forwards_matches bv = true -val "hex_bits_13_matches_prefix" : string -> option((bits(13), nat)) -val hex_bits_13_backwards_matches : string -> bool -function hex_bits_13_backwards_matches s = match s { - s if match hex_bits_13_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_13_backwards : string -> bits(13) -function hex_bits_13_backwards s = - match hex_bits_13_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_14 : bits(14) <-> string -val hex_bits_14_forwards = "decimal_string_of_bits" : bits(14) -> string -val hex_bits_14_forwards_matches : bits(14) -> bool -function hex_bits_14_forwards_matches bv = true -val "hex_bits_14_matches_prefix" : string -> option((bits(14), nat)) -val hex_bits_14_backwards_matches : string -> bool -function hex_bits_14_backwards_matches s = match s { - s if match hex_bits_14_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_14_backwards : string -> bits(14) -function hex_bits_14_backwards s = - match hex_bits_14_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_15 : bits(15) <-> string -val hex_bits_15_forwards = "decimal_string_of_bits" : bits(15) -> string -val hex_bits_15_forwards_matches : bits(15) -> bool -function hex_bits_15_forwards_matches bv = true -val "hex_bits_15_matches_prefix" : string -> option((bits(15), nat)) -val hex_bits_15_backwards_matches : string -> bool -function hex_bits_15_backwards_matches s = match s { - s if match hex_bits_15_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_15_backwards : string -> bits(15) -function hex_bits_15_backwards s = - match hex_bits_15_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_16 : bits(16) <-> string -val hex_bits_16_forwards = "decimal_string_of_bits" : bits(16) -> string -val hex_bits_16_forwards_matches : bits(16) -> bool -function hex_bits_16_forwards_matches bv = true -val "hex_bits_16_matches_prefix" : string -> option((bits(16), nat)) -val hex_bits_16_backwards_matches : string -> bool -function hex_bits_16_backwards_matches s = match s { - s if match hex_bits_16_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_16_backwards : string -> bits(16) -function hex_bits_16_backwards s = - match hex_bits_16_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_17 : bits(17) <-> string -val hex_bits_17_forwards = "decimal_string_of_bits" : bits(17) -> string -val hex_bits_17_forwards_matches : bits(17) -> bool -function hex_bits_17_forwards_matches bv = true -val "hex_bits_17_matches_prefix" : string -> option((bits(17), nat)) -val hex_bits_17_backwards_matches : string -> bool -function hex_bits_17_backwards_matches s = match s { - s if match hex_bits_17_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_17_backwards : string -> bits(17) -function hex_bits_17_backwards s = - match hex_bits_17_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_18 : bits(18) <-> string -val hex_bits_18_forwards = "decimal_string_of_bits" : bits(18) -> string -val hex_bits_18_forwards_matches : bits(18) -> bool -function hex_bits_18_forwards_matches bv = true -val "hex_bits_18_matches_prefix" : string -> option((bits(18), nat)) -val hex_bits_18_backwards_matches : string -> bool -function hex_bits_18_backwards_matches s = match s { - s if match hex_bits_18_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_18_backwards : string -> bits(18) -function hex_bits_18_backwards s = - match hex_bits_18_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_19 : bits(19) <-> string -val hex_bits_19_forwards = "decimal_string_of_bits" : bits(19) -> string -val hex_bits_19_forwards_matches : bits(19) -> bool -function hex_bits_19_forwards_matches bv = true -val "hex_bits_19_matches_prefix" : string -> option((bits(19), nat)) -val hex_bits_19_backwards_matches : string -> bool -function hex_bits_19_backwards_matches s = match s { - s if match hex_bits_19_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_19_backwards : string -> bits(19) -function hex_bits_19_backwards s = - match hex_bits_19_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_20 : bits(20) <-> string -val hex_bits_20_forwards = "decimal_string_of_bits" : bits(20) -> string -val hex_bits_20_forwards_matches : bits(20) -> bool -function hex_bits_20_forwards_matches bv = true -val "hex_bits_20_matches_prefix" : string -> option((bits(20), nat)) -val hex_bits_20_backwards_matches : string -> bool -function hex_bits_20_backwards_matches s = match s { - s if match hex_bits_20_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_20_backwards : string -> bits(20) -function hex_bits_20_backwards s = - match hex_bits_20_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_21 : bits(21) <-> string -val hex_bits_21_forwards = "decimal_string_of_bits" : bits(21) -> string -val hex_bits_21_forwards_matches : bits(21) -> bool -function hex_bits_21_forwards_matches bv = true -val "hex_bits_21_matches_prefix" : string -> option((bits(21), nat)) -val hex_bits_21_backwards_matches : string -> bool -function hex_bits_21_backwards_matches s = match s { - s if match hex_bits_21_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_21_backwards : string -> bits(21) -function hex_bits_21_backwards s = - match hex_bits_21_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_22 : bits(22) <-> string -val hex_bits_22_forwards = "decimal_string_of_bits" : bits(22) -> string -val hex_bits_22_forwards_matches : bits(22) -> bool -function hex_bits_22_forwards_matches bv = true -val "hex_bits_22_matches_prefix" : string -> option((bits(22), nat)) -val hex_bits_22_backwards_matches : string -> bool -function hex_bits_22_backwards_matches s = match s { - s if match hex_bits_22_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_22_backwards : string -> bits(22) -function hex_bits_22_backwards s = - match hex_bits_22_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_23 : bits(23) <-> string -val hex_bits_23_forwards = "decimal_string_of_bits" : bits(23) -> string -val hex_bits_23_forwards_matches : bits(23) -> bool -function hex_bits_23_forwards_matches bv = true -val "hex_bits_23_matches_prefix" : string -> option((bits(23), nat)) -val hex_bits_23_backwards_matches : string -> bool -function hex_bits_23_backwards_matches s = match s { - s if match hex_bits_23_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_23_backwards : string -> bits(23) -function hex_bits_23_backwards s = - match hex_bits_23_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_24 : bits(24) <-> string -val hex_bits_24_forwards = "decimal_string_of_bits" : bits(24) -> string -val hex_bits_24_forwards_matches : bits(24) -> bool -function hex_bits_24_forwards_matches bv = true -val "hex_bits_24_matches_prefix" : string -> option((bits(24), nat)) -val hex_bits_24_backwards_matches : string -> bool -function hex_bits_24_backwards_matches s = match s { - s if match hex_bits_24_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_24_backwards : string -> bits(24) -function hex_bits_24_backwards s = - match hex_bits_24_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_25 : bits(25) <-> string -val hex_bits_25_forwards = "decimal_string_of_bits" : bits(25) -> string -val hex_bits_25_forwards_matches : bits(25) -> bool -function hex_bits_25_forwards_matches bv = true -val "hex_bits_25_matches_prefix" : string -> option((bits(25), nat)) -val hex_bits_25_backwards_matches : string -> bool -function hex_bits_25_backwards_matches s = match s { - s if match hex_bits_25_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_25_backwards : string -> bits(25) -function hex_bits_25_backwards s = - match hex_bits_25_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_26 : bits(26) <-> string -val hex_bits_26_forwards = "decimal_string_of_bits" : bits(26) -> string -val hex_bits_26_forwards_matches : bits(26) -> bool -function hex_bits_26_forwards_matches bv = true -val "hex_bits_26_matches_prefix" : string -> option((bits(26), nat)) -val hex_bits_26_backwards_matches : string -> bool -function hex_bits_26_backwards_matches s = match s { - s if match hex_bits_26_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_26_backwards : string -> bits(26) -function hex_bits_26_backwards s = - match hex_bits_26_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_27 : bits(27) <-> string -val hex_bits_27_forwards = "decimal_string_of_bits" : bits(27) -> string -val hex_bits_27_forwards_matches : bits(27) -> bool -function hex_bits_27_forwards_matches bv = true -val "hex_bits_27_matches_prefix" : string -> option((bits(27), nat)) -val hex_bits_27_backwards_matches : string -> bool -function hex_bits_27_backwards_matches s = match s { - s if match hex_bits_27_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_27_backwards : string -> bits(27) -function hex_bits_27_backwards s = - match hex_bits_27_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_28 : bits(28) <-> string -val hex_bits_28_forwards = "decimal_string_of_bits" : bits(28) -> string -val hex_bits_28_forwards_matches : bits(28) -> bool -function hex_bits_28_forwards_matches bv = true -val "hex_bits_28_matches_prefix" : string -> option((bits(28), nat)) -val hex_bits_28_backwards_matches : string -> bool -function hex_bits_28_backwards_matches s = match s { - s if match hex_bits_28_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_28_backwards : string -> bits(28) -function hex_bits_28_backwards s = - match hex_bits_28_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_29 : bits(29) <-> string -val hex_bits_29_forwards = "decimal_string_of_bits" : bits(29) -> string -val hex_bits_29_forwards_matches : bits(29) -> bool -function hex_bits_29_forwards_matches bv = true -val "hex_bits_29_matches_prefix" : string -> option((bits(29), nat)) -val hex_bits_29_backwards_matches : string -> bool -function hex_bits_29_backwards_matches s = match s { - s if match hex_bits_29_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_29_backwards : string -> bits(29) -function hex_bits_29_backwards s = - match hex_bits_29_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_30 : bits(30) <-> string -val hex_bits_30_forwards = "decimal_string_of_bits" : bits(30) -> string -val hex_bits_30_forwards_matches : bits(30) -> bool -function hex_bits_30_forwards_matches bv = true -val "hex_bits_30_matches_prefix" : string -> option((bits(30), nat)) -val hex_bits_30_backwards_matches : string -> bool -function hex_bits_30_backwards_matches s = match s { - s if match hex_bits_30_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_30_backwards : string -> bits(30) -function hex_bits_30_backwards s = - match hex_bits_30_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_31 : bits(31) <-> string -val hex_bits_31_forwards = "decimal_string_of_bits" : bits(31) -> string -val hex_bits_31_forwards_matches : bits(31) -> bool -function hex_bits_31_forwards_matches bv = true -val "hex_bits_31_matches_prefix" : string -> option((bits(31), nat)) -val hex_bits_31_backwards_matches : string -> bool -function hex_bits_31_backwards_matches s = match s { - s if match hex_bits_31_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_31_backwards : string -> bits(31) -function hex_bits_31_backwards s = - match hex_bits_31_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_32 : bits(32) <-> string -val hex_bits_32_forwards = "decimal_string_of_bits" : bits(32) -> string -val hex_bits_32_forwards_matches : bits(32) -> bool -function hex_bits_32_forwards_matches bv = true -val "hex_bits_32_matches_prefix" : string -> option((bits(32), nat)) -val hex_bits_32_backwards_matches : string -> bool -function hex_bits_32_backwards_matches s = match s { - s if match hex_bits_32_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_32_backwards : string -> bits(32) -function hex_bits_32_backwards s = - match hex_bits_32_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_33 : bits(33) <-> string -val hex_bits_33_forwards = "decimal_string_of_bits" : bits(33) -> string -val hex_bits_33_forwards_matches : bits(33) -> bool -function hex_bits_33_forwards_matches bv = true -val "hex_bits_33_matches_prefix" : string -> option((bits(33), nat)) -val hex_bits_33_backwards_matches : string -> bool -function hex_bits_33_backwards_matches s = match s { - s if match hex_bits_33_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_33_backwards : string -> bits(33) -function hex_bits_33_backwards s = - match hex_bits_33_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_48 : bits(48) <-> string -val hex_bits_48_forwards = "decimal_string_of_bits" : bits(48) -> string -val hex_bits_48_forwards_matches : bits(48) -> bool -function hex_bits_48_forwards_matches bv = true -val "hex_bits_48_matches_prefix" : string -> option((bits(48), nat)) -val hex_bits_48_backwards_matches : string -> bool -function hex_bits_48_backwards_matches s = match s { - s if match hex_bits_48_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_48_backwards : string -> bits(48) -function hex_bits_48_backwards s = - match hex_bits_48_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_64 : bits(64) <-> string -val hex_bits_64_forwards = "decimal_string_of_bits" : bits(64) -> string -val hex_bits_64_forwards_matches : bits(64) -> bool -function hex_bits_64_forwards_matches bv = true -val "hex_bits_64_matches_prefix" : string -> option((bits(64), nat)) -val hex_bits_64_backwards_matches : string -> bool -function hex_bits_64_backwards_matches s = match s { - s if match hex_bits_64_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_64_backwards : string -> bits(64) -function hex_bits_64_backwards s = - match hex_bits_64_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val eq_vec = {ocaml: "eq_list", interpreter: "eq_list", lem: "eq_vec", coq: "eq_vec", c: "eq_bits"} : forall 'n. (bits('n), bits('n)) -> bool - -val eq_string = {c: "eq_string", ocaml: "eq_string", interpreter: "eq_string", lem: "eq", coq: "generic_eq"} : (string, string) -> bool - -val eq_real = {ocaml: "eq_real", interpreter: "eq_real", lem: "eq"} : (real, real) -> bool val eq_anything = {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", lem: "eq", coq: "generic_eq"} : forall ('a : Type). ('a, 'a) -> bool -val bitvector_length = {ocaml: "length", interpreter: "length", lem: "length", coq: "length_mword"} : forall 'n. bits('n) -> atom('n) -val vector_length = {ocaml: "length", interpreter: "length", lem: "length_list", coq: "vec_length"} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n) -val list_length = {ocaml: "length", interpreter: "length", lem: "length_list", coq: "length_list"} : forall ('a : Type). list('a) -> int - -overload length = {bitvector_length, vector_length, list_length} +overload operator == = {eq_string, eq_anything} val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} /* sneaky deref with no effect necessary for bitfield writes */ val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a -overload operator == = {eq_vec, eq_string, eq_real, eq_anything} - -val vector_subrange = { - ocaml: "subrange", - interpreter: "subrange", - lem: "subrange_vec_dec", - c: "vector_subrange", - coq: "subrange_vec_dec" -} : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n. - (bits('n), atom('m), atom('o)) -> bits('m - 'o + 1) -/* -val vector_subrange = {ocaml: "subrange", interpreter: "subrange", lem: "subrange_vec_dec", coq: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n. - (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) -*/ - -val bitvector_access = {c: "bitvector_access", ocaml: "access", interpreter: "access", lem: "access_vec_dec", coq: "access_vec_dec"} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n. - (bits('n), atom('m)) -> bit - -val any_vector_access = {ocaml: "access", interpreter: "access", lem: "access_list_dec", coq: "vec_access_dec"} : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. - (vector('n, dec, 'a), atom('m)) -> 'a - -overload vector_access = {bitvector_access, any_vector_access} - -val bitvector_update = {ocaml: "update", interpreter: "update", lem: "update_vec_dec", coq: "update_vec_dec"} : forall 'n. - (bits('n), int, bit) -> bits('n) - -val any_vector_update = {ocaml: "update", interpreter: "update", lem: "update_list_dec", coq: "vector_update"} : forall 'n ('a : Type). +val any_vector_update = {ocaml: "update", lem: "update_list_dec", coq: "vector_update"} : forall 'n ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a) -overload vector_update = {bitvector_update, any_vector_update} +overload vector_update = {any_vector_update} val update_subrange = {ocaml: "update_subrange", interpreter: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) -val vcons = {lem: "cons_vec"} : forall ('n : Int) ('a : Type). - ('a, vector('n, dec, 'a)) -> vector('n + 1, dec, 'a) - -val bitvector_concat = {c: "append", ocaml: "append", interpreter: "append", lem: "concat_vec", coq: "concat_vec"} : forall ('n : Int) ('m : Int). - (bits('n), bits('m)) -> bits('n + 'm) - -val vector_concat = {ocaml: "append", interpreter: "append", lem: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type). +val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type). (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a) -overload append = {bitvector_concat, vector_concat} +overload append = {vector_concat} val not_vec = {c: "not_bits", _: "not_vec"} : forall 'n. bits('n) -> bits('n) @@ -781,7 +39,7 @@ overload ~ = {not_bool, not_vec} val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool -function neq_vec (x, y) = not_bool(eq_vec(x, y)) +function neq_vec (x, y) = not_bool(eq_bits(x, y)) val neq_anything = {lem: "neq", coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool @@ -797,38 +55,9 @@ val or_vec = {lem: "or_vec", c: "or_bits", coq: "or_vec", ocaml: "or_vec", inter overload operator | = {or_vec} -val unsigned = {ocaml: "uint", interpreter: "uint", lem: "uint", coq: "uint", c: "sail_unsigned"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) - -val signed = {ocaml: "sint", interpreter: "sint", lem: "sint", coq: "sint", c: "sail_signed"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) - -val hex_slice = "hex_slice" : forall 'n 'm, 'n >= 'm. (string, atom('n), atom('m)) -> bits('n - 'm) - -val __SetSlice_bits = "set_slice" : forall 'n 'm. - (atom('n), atom('m), bits('n), int, bits('m)) -> bits('n) - -val __SetSlice_int = "set_slice_int" : forall 'w. (atom('w), int, int, bits('w)) -> int - -val __raw_SetSlice_int : forall 'w. (atom('w), int, int, bits('w)) -> int - -val __raw_GetSlice_int = "get_slice_int" : forall 'w, 'w >= 0. (atom('w), int, int) -> bits('w) - -val __GetSlice_int : forall 'n, 'n >= 0. (atom('n), int, int) -> bits('n) - -function __GetSlice_int (n, m, o) = __raw_GetSlice_int(n, m, o) - -val __raw_SetSlice_bits : forall 'n 'w. - (atom('n), atom('w), bits('n), int, bits('w)) -> bits('n) - -val __raw_GetSlice_bits : forall 'n 'w, 'w >= 0. - (atom('n), atom('w), bits('n), int) -> bits('w) - val "shiftl" : forall 'm. (bits('m), int) -> bits('m) val "shiftr" : forall 'm. (bits('m), int) -> bits('m) -val __SignExtendSlice = {lem: "exts_slice"} : forall 'm. (bits('m), int, int) -> bits('m) - -val __ZeroExtendSlice = {lem: "extz_slice"} : forall 'm. (bits('m), int, int) -> bits('m) - val cast cast_unit_vec : bit -> bits(1) function cast_unit_vec b = match b { @@ -836,120 +65,30 @@ function cast_unit_vec b = match b { bitone => 0b1 } -val putchar = "putchar" : forall ('a : Type). 'a -> unit - -val concat_str = {c: "concat_str", ocaml: "concat_str", interpreter: "concat_str", lem: "stringAppend", coq: "String.append"} : (string, string) -> string - -val string_of_int = {c: "string_of_int", ocaml: "string_of_int", interpreter: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string - -val DecStr : int -> string - -val HexStr : int -> string +val string_of_int = {c: "string_of_int", ocaml: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string val BitStr = "string_of_bits" : forall 'n. bits('n) -> string -val "decimal_string_of_bits" : forall 'n. bits('n) -> string val xor_vec = {c: "xor_bits", _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) val int_power = {ocaml: "int_power", interpreter: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int -val real_power = {ocaml: "real_power", interpreter: "real_power", lem: "realPowInteger"} : (real, int) -> real - -overload operator ^ = {xor_vec, int_power, real_power, concat_str} - -val add_int = {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm. - (int('n), int('m)) -> int('n + 'm) - -val add_vec = {c: "add_bits", _: "add_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) - -val add_vec_int = {c: "add_bits_int", _: "add_vec_int"} : forall 'n. (bits('n), int) -> bits('n) - -val add_real = {ocaml: "add_real", interpreter: "add_real", lem: "realAdd"} : (real, real) -> real - -overload operator + = {add_int, add_vec, add_vec_int, add_real} - -val sub_int = {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : forall 'n 'm. - (int('n), int('m)) -> int('n - 'm) - -val sub_nat = {ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)", - interpreter: "sub_nat", lem: "integerMinus", coq: "sub_nat", c: "sub_nat"} - : (nat, nat) -> nat +overload operator ^ = {xor_vec, int_power, concat_str} val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) val sub_vec_int = {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits('n), int) -> bits('n) -val sub_real = {ocaml: "sub_real", interpreter: "sub_real", lem: "realMinus"} : (real, real) -> real - -val negate_int = {ocaml: "negate", interpreter: "negate", lem: "integerNegate", coq: "Z.opp"} : forall 'n. int('n) -> int(- 'n) - -val negate_real = {ocaml: "Num.minus_num", interpreter: "neg_real", lem: "realNegate"} : real -> real - -overload operator - = {sub_int, sub_vec, sub_vec_int, sub_real} - -overload negate = {negate_int, negate_real} - -val mult_atom = {ocaml: "mult", interpreter: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : forall 'n 'm. - (atom('n), atom('m)) -> atom('n * 'm) - -val mult_int = {ocaml: "mult", interpreter: "mult", lem: "integerMult", coq: "Z.mul"} : (int, int) -> int - -val mult_real = {ocaml: "mult_real", interpreter: "mult_real", lem: "realMult"} : (real, real) -> real - -overload operator * = {mult_atom, mult_int, mult_real} - -val Sqrt = {ocaml: "sqrt_real", interpreter: "sqrt_real", lem: "realSqrt"} : real -> real - -val gteq_real = {ocaml: "gteq_real", interpreter: "gteq_real", lem: "gteq"} : (real, real) -> bool - -overload operator >= = {gteq_real} - -val lteq_real = {ocaml: "lteq_real", interpreter: "lteq_real", lem: "lteq"} : (real, real) -> bool - -overload operator <= = {lteq_real} - -val gt_real = {ocaml: "gt_real", interpreter: "gt_real", lem: "gt"} : (real, real) -> bool - -overload operator > = {gt_real} - -val lt_real = {ocaml: "lt_real", interpreter: "lt_real", lem: "lt"} : (real, real) -> bool - -overload operator < = {lt_real} - -val RoundDown = {ocaml: "round_down", interpreter: "round_down", lem: "realFloor"} : real -> int - -val RoundUp = {ocaml: "round_up", interpreter: "round_up", lem: "realCeiling"} : real -> int - -val abs_int = {ocaml: "abs_int", interpreter: "abs_int", lem: "abs", coq: "Z.abs"} : int -> int - -val abs_real = {ocaml: "abs_real", interpreter: "abs_real", lem: "abs"} : real -> real - -overload abs = {abs_int, abs_real} - -val quotient_nat = {ocaml: "quotient", interpreter: "quotient", lem: "integerDiv"} : (nat, nat) -> nat - -val quotient_real = {ocaml: "quotient_real", interpreter: "quotient_real", lem: "realDiv"} : (real, real) -> real - -val quotient = {ocaml: "quotient", interpreter: "quotient", lem: "integerDiv"} : (int, int) -> int - -overload operator / = {quotient_nat, quotient, quotient_real} +overload operator - = {sub_vec, sub_vec_int} val quot_round_zero = {ocaml: "quot_round_zero", interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int"} : (int, int) -> int val rem_round_zero = {ocaml: "rem_round_zero", interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int -val modulus = {ocaml: "modulus", interpreter: "modulus", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int +val modulus = {lem: "hardware_mod"} : (int, int) -> int overload operator % = {modulus} -val Real = {ocaml: "Num.num_of_big_int", interpreter: "to_real", lem: "realFromInteger"} : int -> real - -val shl_int = "shl_int" : (int, int) -> int -val shr_int = "shr_int" : (int, int) -> int -val lor_int = "lor_int" : (int, int) -> int -val land_int = "land_int" : (int, int) -> int -val lxor_int = "lxor_int" : (int, int) -> int - -val min_nat = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "min_nat", c: "min_int"} : (nat, nat) -> nat +val min_nat = {ocaml: "min_int", lem: "min", coq: "min_nat", c: "min_int"} : (nat, nat) -> nat val min_int = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "Z.min", c: "min_int"} : (int, int) -> int @@ -961,42 +100,9 @@ overload min = {min_nat, min_int} overload max = {max_nat, max_int} -val __TraceMemoryWrite : forall 'n 'm. - (atom('n), bits('m), bits(8 * 'n)) -> unit - -val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit - -val replicate_bits = "replicate_bits" : forall 'n 'm, 'm >= 0. (bits('n), atom('m)) -> bits('n * 'm) - -val cast ex_nat : nat -> {'n, 'n >= 0. atom('n)} - -function ex_nat 'n = n - -val cast ex_int : int -> {'n, true. atom('n)} - -function ex_int 'n = n - -/* -val cast ex_range : forall 'n 'm. range('n, 'm) -> {'o, 'n <= 'o <= 'm. atom('o)} - -function ex_range (n as 'N) = n -*/ - -val coerce_int_nat : int -> nat effect {escape} - -function coerce_int_nat 'x = { - assert(constraint('x >= 0)); - x -} - -val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0. - (bits('m), int, atom('n)) -> bits('n) - val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) val print = "print_endline" : string -> unit -val print_int = "print_int" : (string, int) -> unit -val print_bits = "print_bits" : forall 'n. (string, bits('n)) -> unit val print_string = "print_string" : (string, string) -> unit val print_instr = {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", _: "print_endline"} : string -> unit @@ -1004,23 +110,32 @@ val print_reg = {ocaml: "Platform.print_reg", interpreter: "print_endline", val print_mem = {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", _: "print_endline"} : string -> unit val print_platform = {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", _: "print_endline"} : string -> unit -val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) -val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) - $ifndef FEATURE_IMPLICITS val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) val EXTZ : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) -function EXTS v = sign_extend(v, sizeof('m)) -function EXTZ v = zero_extend(v, sizeof('m)) +function EXTS v = sail_sign_extend(v, sizeof('m)) +function EXTZ v = sail_zero_extend(v, sizeof('m)) $else val EXTS : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) val EXTZ : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) -function EXTS(m, v) = sign_extend(v, m) -function EXTZ(m, v) = zero_extend(v, m) +function EXTS(m, v) = sail_sign_extend(v, m) +function EXTZ(m, v) = sail_zero_extend(v, m) $endif +val cast bool_to_bits : bool -> bits(1) +function bool_to_bits x = if x then 0b1 else 0b0 + +val cast bit_to_bool : bit -> bool +function bit_to_bool b = match b { + bitone => true, + bitzero => false +} + +val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l) +function to_bits (l, n) = get_slice_int(l, n, 0) + infix 4 <_s infix 4 >=_s infix 4 <_u @@ -1039,36 +154,12 @@ function operator <_u (x, y) = unsigned(x) < unsigned(y) function operator >=_u (x, y) = unsigned(x) >= unsigned(y) function operator <=_u (x, y) = unsigned(x) <= unsigned(y) -val cast bool_to_bits : bool -> bits(1) -function bool_to_bits x = if x then 0b1 else 0b0 - -val cast bit_to_bool : bit -> bool -function bit_to_bool b = match b { - bitone => true, - bitzero => false -} - infix 7 >> infix 7 << val operator >> = "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) val operator << = "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) -val vector64 : int -> bits(64) - -function vector64 n = __raw_GetSlice_int(64, n, 0) - -val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l) -function to_bits (l, n) = __raw_GetSlice_int(l, n, 0) - -val vector_update_subrange_dec = {ocaml: "update_subrange", interpreter: "update_subrange", c: "vector_update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o. - (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) - -val vector_update_subrange_inc = {ocaml: "update_subrange", interpreter: "update_subrange", lem: "update_subrange_vec_inc"} : forall 'n 'm 'o. - (vector('n, inc, bit), atom('m), atom('o), vector('o - ('m - 1), inc, bit)) -> vector('n, inc, bit) - -overload vector_update_subrange = {vector_update_subrange_dec, vector_update_subrange_inc} - /* Ideally these would be sail builtin */ function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) = @@ -1079,6 +170,14 @@ function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) = let v64 : bits(64) = EXTS(v) in (v64 >> shift)[31..0] +/* helpers for mappings */ + +val spc : unit <-> string +val opt_spc : unit <-> string +val def_spc : unit <-> string + +val "decimal_string_of_bits" : forall 'n. bits('n) -> string +val hex_bits : forall 'n . (atom('n), bits('n)) <-> string val n_leading_spaces : string -> nat function n_leading_spaces s = diff --git a/model/prelude_mapping.sail b/model/prelude_mapping.sail new file mode 100644 index 0000000..4826084 --- /dev/null +++ b/model/prelude_mapping.sail @@ -0,0 +1,690 @@ +/* Python: +f = """val hex_bits_{0} : bits({0}) <-> string +val hex_bits_{0}_forwards = "decimal_string_of_bits" : bits({0}) -> string +val hex_bits_{0}_forwards_matches : bits({0}) -> bool +function hex_bits_{0}_forwards_matches bv = true +val "hex_bits_{0}_matches_prefix" : string -> option((bits({0}), nat)) +val hex_bits_{0}_backwards_matches : string -> bool +function hex_bits_{0}_backwards_matches s = match s {{ + s if match hex_bits_{0}_matches_prefix(s) {{ + Some (_, n) if n == string_length(s) => true, + _ => false + }} => true, + _ => false +}} +val hex_bits_{0}_backwards : string -> bits({0}) +function hex_bits_{0}_backwards s = + match hex_bits_{0}_matches_prefix(s) {{ + Some (bv, n) if n == string_length(s) => bv + }} +""" + +for i in list(range(1, 34)) + [48, 64]: + print(f.format(i)) + +*/ +val hex_bits_1 : bits(1) <-> string +val hex_bits_1_forwards = "decimal_string_of_bits" : bits(1) -> string +val hex_bits_1_forwards_matches : bits(1) -> bool +function hex_bits_1_forwards_matches bv = true +val "hex_bits_1_matches_prefix" : string -> option((bits(1), nat)) +val hex_bits_1_backwards_matches : string -> bool +function hex_bits_1_backwards_matches s = match s { + s if match hex_bits_1_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_1_backwards : string -> bits(1) +function hex_bits_1_backwards s = + match hex_bits_1_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_2 : bits(2) <-> string +val hex_bits_2_forwards = "decimal_string_of_bits" : bits(2) -> string +val hex_bits_2_forwards_matches : bits(2) -> bool +function hex_bits_2_forwards_matches bv = true +val "hex_bits_2_matches_prefix" : string -> option((bits(2), nat)) +val hex_bits_2_backwards_matches : string -> bool +function hex_bits_2_backwards_matches s = match s { + s if match hex_bits_2_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_2_backwards : string -> bits(2) +function hex_bits_2_backwards s = + match hex_bits_2_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_3 : bits(3) <-> string +val hex_bits_3_forwards = "decimal_string_of_bits" : bits(3) -> string +val hex_bits_3_forwards_matches : bits(3) -> bool +function hex_bits_3_forwards_matches bv = true +val "hex_bits_3_matches_prefix" : string -> option((bits(3), nat)) +val hex_bits_3_backwards_matches : string -> bool +function hex_bits_3_backwards_matches s = match s { + s if match hex_bits_3_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_3_backwards : string -> bits(3) +function hex_bits_3_backwards s = + match hex_bits_3_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_4 : bits(4) <-> string +val hex_bits_4_forwards = "decimal_string_of_bits" : bits(4) -> string +val hex_bits_4_forwards_matches : bits(4) -> bool +function hex_bits_4_forwards_matches bv = true +val "hex_bits_4_matches_prefix" : string -> option((bits(4), nat)) +val hex_bits_4_backwards_matches : string -> bool +function hex_bits_4_backwards_matches s = match s { + s if match hex_bits_4_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_4_backwards : string -> bits(4) +function hex_bits_4_backwards s = + match hex_bits_4_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_5 : bits(5) <-> string +val hex_bits_5_forwards = "decimal_string_of_bits" : bits(5) -> string +val hex_bits_5_forwards_matches : bits(5) -> bool +function hex_bits_5_forwards_matches bv = true +val "hex_bits_5_matches_prefix" : string -> option((bits(5), nat)) +val hex_bits_5_backwards_matches : string -> bool +function hex_bits_5_backwards_matches s = match s { + s if match hex_bits_5_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_5_backwards : string -> bits(5) +function hex_bits_5_backwards s = + match hex_bits_5_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_6 : bits(6) <-> string +val hex_bits_6_forwards = "decimal_string_of_bits" : bits(6) -> string +val hex_bits_6_forwards_matches : bits(6) -> bool +function hex_bits_6_forwards_matches bv = true +val "hex_bits_6_matches_prefix" : string -> option((bits(6), nat)) +val hex_bits_6_backwards_matches : string -> bool +function hex_bits_6_backwards_matches s = match s { + s if match hex_bits_6_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_6_backwards : string -> bits(6) +function hex_bits_6_backwards s = + match hex_bits_6_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_7 : bits(7) <-> string +val hex_bits_7_forwards = "decimal_string_of_bits" : bits(7) -> string +val hex_bits_7_forwards_matches : bits(7) -> bool +function hex_bits_7_forwards_matches bv = true +val "hex_bits_7_matches_prefix" : string -> option((bits(7), nat)) +val hex_bits_7_backwards_matches : string -> bool +function hex_bits_7_backwards_matches s = match s { + s if match hex_bits_7_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_7_backwards : string -> bits(7) +function hex_bits_7_backwards s = + match hex_bits_7_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_8 : bits(8) <-> string +val hex_bits_8_forwards = "decimal_string_of_bits" : bits(8) -> string +val hex_bits_8_forwards_matches : bits(8) -> bool +function hex_bits_8_forwards_matches bv = true +val "hex_bits_8_matches_prefix" : string -> option((bits(8), nat)) +val hex_bits_8_backwards_matches : string -> bool +function hex_bits_8_backwards_matches s = match s { + s if match hex_bits_8_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_8_backwards : string -> bits(8) +function hex_bits_8_backwards s = + match hex_bits_8_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_9 : bits(9) <-> string +val hex_bits_9_forwards = "decimal_string_of_bits" : bits(9) -> string +val hex_bits_9_forwards_matches : bits(9) -> bool +function hex_bits_9_forwards_matches bv = true +val "hex_bits_9_matches_prefix" : string -> option((bits(9), nat)) +val hex_bits_9_backwards_matches : string -> bool +function hex_bits_9_backwards_matches s = match s { + s if match hex_bits_9_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_9_backwards : string -> bits(9) +function hex_bits_9_backwards s = + match hex_bits_9_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_10 : bits(10) <-> string +val hex_bits_10_forwards = "decimal_string_of_bits" : bits(10) -> string +val hex_bits_10_forwards_matches : bits(10) -> bool +function hex_bits_10_forwards_matches bv = true +val "hex_bits_10_matches_prefix" : string -> option((bits(10), nat)) +val hex_bits_10_backwards_matches : string -> bool +function hex_bits_10_backwards_matches s = match s { + s if match hex_bits_10_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_10_backwards : string -> bits(10) +function hex_bits_10_backwards s = + match hex_bits_10_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_11 : bits(11) <-> string +val hex_bits_11_forwards = "decimal_string_of_bits" : bits(11) -> string +val hex_bits_11_forwards_matches : bits(11) -> bool +function hex_bits_11_forwards_matches bv = true +val "hex_bits_11_matches_prefix" : string -> option((bits(11), nat)) +val hex_bits_11_backwards_matches : string -> bool +function hex_bits_11_backwards_matches s = match s { + s if match hex_bits_11_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_11_backwards : string -> bits(11) +function hex_bits_11_backwards s = + match hex_bits_11_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_12 : bits(12) <-> string +val hex_bits_12_forwards = "decimal_string_of_bits" : bits(12) -> string +val hex_bits_12_forwards_matches : bits(12) -> bool +function hex_bits_12_forwards_matches bv = true +val "hex_bits_12_matches_prefix" : string -> option((bits(12), nat)) +val hex_bits_12_backwards_matches : string -> bool +function hex_bits_12_backwards_matches s = match s { + s if match hex_bits_12_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_12_backwards : string -> bits(12) +function hex_bits_12_backwards s = + match hex_bits_12_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_13 : bits(13) <-> string +val hex_bits_13_forwards = "decimal_string_of_bits" : bits(13) -> string +val hex_bits_13_forwards_matches : bits(13) -> bool +function hex_bits_13_forwards_matches bv = true +val "hex_bits_13_matches_prefix" : string -> option((bits(13), nat)) +val hex_bits_13_backwards_matches : string -> bool +function hex_bits_13_backwards_matches s = match s { + s if match hex_bits_13_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_13_backwards : string -> bits(13) +function hex_bits_13_backwards s = + match hex_bits_13_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_14 : bits(14) <-> string +val hex_bits_14_forwards = "decimal_string_of_bits" : bits(14) -> string +val hex_bits_14_forwards_matches : bits(14) -> bool +function hex_bits_14_forwards_matches bv = true +val "hex_bits_14_matches_prefix" : string -> option((bits(14), nat)) +val hex_bits_14_backwards_matches : string -> bool +function hex_bits_14_backwards_matches s = match s { + s if match hex_bits_14_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_14_backwards : string -> bits(14) +function hex_bits_14_backwards s = + match hex_bits_14_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_15 : bits(15) <-> string +val hex_bits_15_forwards = "decimal_string_of_bits" : bits(15) -> string +val hex_bits_15_forwards_matches : bits(15) -> bool +function hex_bits_15_forwards_matches bv = true +val "hex_bits_15_matches_prefix" : string -> option((bits(15), nat)) +val hex_bits_15_backwards_matches : string -> bool +function hex_bits_15_backwards_matches s = match s { + s if match hex_bits_15_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_15_backwards : string -> bits(15) +function hex_bits_15_backwards s = + match hex_bits_15_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_16 : bits(16) <-> string +val hex_bits_16_forwards = "decimal_string_of_bits" : bits(16) -> string +val hex_bits_16_forwards_matches : bits(16) -> bool +function hex_bits_16_forwards_matches bv = true +val "hex_bits_16_matches_prefix" : string -> option((bits(16), nat)) +val hex_bits_16_backwards_matches : string -> bool +function hex_bits_16_backwards_matches s = match s { + s if match hex_bits_16_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_16_backwards : string -> bits(16) +function hex_bits_16_backwards s = + match hex_bits_16_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_17 : bits(17) <-> string +val hex_bits_17_forwards = "decimal_string_of_bits" : bits(17) -> string +val hex_bits_17_forwards_matches : bits(17) -> bool +function hex_bits_17_forwards_matches bv = true +val "hex_bits_17_matches_prefix" : string -> option((bits(17), nat)) +val hex_bits_17_backwards_matches : string -> bool +function hex_bits_17_backwards_matches s = match s { + s if match hex_bits_17_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_17_backwards : string -> bits(17) +function hex_bits_17_backwards s = + match hex_bits_17_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_18 : bits(18) <-> string +val hex_bits_18_forwards = "decimal_string_of_bits" : bits(18) -> string +val hex_bits_18_forwards_matches : bits(18) -> bool +function hex_bits_18_forwards_matches bv = true +val "hex_bits_18_matches_prefix" : string -> option((bits(18), nat)) +val hex_bits_18_backwards_matches : string -> bool +function hex_bits_18_backwards_matches s = match s { + s if match hex_bits_18_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_18_backwards : string -> bits(18) +function hex_bits_18_backwards s = + match hex_bits_18_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_19 : bits(19) <-> string +val hex_bits_19_forwards = "decimal_string_of_bits" : bits(19) -> string +val hex_bits_19_forwards_matches : bits(19) -> bool +function hex_bits_19_forwards_matches bv = true +val "hex_bits_19_matches_prefix" : string -> option((bits(19), nat)) +val hex_bits_19_backwards_matches : string -> bool +function hex_bits_19_backwards_matches s = match s { + s if match hex_bits_19_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_19_backwards : string -> bits(19) +function hex_bits_19_backwards s = + match hex_bits_19_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_20 : bits(20) <-> string +val hex_bits_20_forwards = "decimal_string_of_bits" : bits(20) -> string +val hex_bits_20_forwards_matches : bits(20) -> bool +function hex_bits_20_forwards_matches bv = true +val "hex_bits_20_matches_prefix" : string -> option((bits(20), nat)) +val hex_bits_20_backwards_matches : string -> bool +function hex_bits_20_backwards_matches s = match s { + s if match hex_bits_20_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_20_backwards : string -> bits(20) +function hex_bits_20_backwards s = + match hex_bits_20_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_21 : bits(21) <-> string +val hex_bits_21_forwards = "decimal_string_of_bits" : bits(21) -> string +val hex_bits_21_forwards_matches : bits(21) -> bool +function hex_bits_21_forwards_matches bv = true +val "hex_bits_21_matches_prefix" : string -> option((bits(21), nat)) +val hex_bits_21_backwards_matches : string -> bool +function hex_bits_21_backwards_matches s = match s { + s if match hex_bits_21_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_21_backwards : string -> bits(21) +function hex_bits_21_backwards s = + match hex_bits_21_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_22 : bits(22) <-> string +val hex_bits_22_forwards = "decimal_string_of_bits" : bits(22) -> string +val hex_bits_22_forwards_matches : bits(22) -> bool +function hex_bits_22_forwards_matches bv = true +val "hex_bits_22_matches_prefix" : string -> option((bits(22), nat)) +val hex_bits_22_backwards_matches : string -> bool +function hex_bits_22_backwards_matches s = match s { + s if match hex_bits_22_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_22_backwards : string -> bits(22) +function hex_bits_22_backwards s = + match hex_bits_22_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_23 : bits(23) <-> string +val hex_bits_23_forwards = "decimal_string_of_bits" : bits(23) -> string +val hex_bits_23_forwards_matches : bits(23) -> bool +function hex_bits_23_forwards_matches bv = true +val "hex_bits_23_matches_prefix" : string -> option((bits(23), nat)) +val hex_bits_23_backwards_matches : string -> bool +function hex_bits_23_backwards_matches s = match s { + s if match hex_bits_23_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_23_backwards : string -> bits(23) +function hex_bits_23_backwards s = + match hex_bits_23_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_24 : bits(24) <-> string +val hex_bits_24_forwards = "decimal_string_of_bits" : bits(24) -> string +val hex_bits_24_forwards_matches : bits(24) -> bool +function hex_bits_24_forwards_matches bv = true +val "hex_bits_24_matches_prefix" : string -> option((bits(24), nat)) +val hex_bits_24_backwards_matches : string -> bool +function hex_bits_24_backwards_matches s = match s { + s if match hex_bits_24_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_24_backwards : string -> bits(24) +function hex_bits_24_backwards s = + match hex_bits_24_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_25 : bits(25) <-> string +val hex_bits_25_forwards = "decimal_string_of_bits" : bits(25) -> string +val hex_bits_25_forwards_matches : bits(25) -> bool +function hex_bits_25_forwards_matches bv = true +val "hex_bits_25_matches_prefix" : string -> option((bits(25), nat)) +val hex_bits_25_backwards_matches : string -> bool +function hex_bits_25_backwards_matches s = match s { + s if match hex_bits_25_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_25_backwards : string -> bits(25) +function hex_bits_25_backwards s = + match hex_bits_25_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_26 : bits(26) <-> string +val hex_bits_26_forwards = "decimal_string_of_bits" : bits(26) -> string +val hex_bits_26_forwards_matches : bits(26) -> bool +function hex_bits_26_forwards_matches bv = true +val "hex_bits_26_matches_prefix" : string -> option((bits(26), nat)) +val hex_bits_26_backwards_matches : string -> bool +function hex_bits_26_backwards_matches s = match s { + s if match hex_bits_26_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_26_backwards : string -> bits(26) +function hex_bits_26_backwards s = + match hex_bits_26_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_27 : bits(27) <-> string +val hex_bits_27_forwards = "decimal_string_of_bits" : bits(27) -> string +val hex_bits_27_forwards_matches : bits(27) -> bool +function hex_bits_27_forwards_matches bv = true +val "hex_bits_27_matches_prefix" : string -> option((bits(27), nat)) +val hex_bits_27_backwards_matches : string -> bool +function hex_bits_27_backwards_matches s = match s { + s if match hex_bits_27_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_27_backwards : string -> bits(27) +function hex_bits_27_backwards s = + match hex_bits_27_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_28 : bits(28) <-> string +val hex_bits_28_forwards = "decimal_string_of_bits" : bits(28) -> string +val hex_bits_28_forwards_matches : bits(28) -> bool +function hex_bits_28_forwards_matches bv = true +val "hex_bits_28_matches_prefix" : string -> option((bits(28), nat)) +val hex_bits_28_backwards_matches : string -> bool +function hex_bits_28_backwards_matches s = match s { + s if match hex_bits_28_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_28_backwards : string -> bits(28) +function hex_bits_28_backwards s = + match hex_bits_28_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_29 : bits(29) <-> string +val hex_bits_29_forwards = "decimal_string_of_bits" : bits(29) -> string +val hex_bits_29_forwards_matches : bits(29) -> bool +function hex_bits_29_forwards_matches bv = true +val "hex_bits_29_matches_prefix" : string -> option((bits(29), nat)) +val hex_bits_29_backwards_matches : string -> bool +function hex_bits_29_backwards_matches s = match s { + s if match hex_bits_29_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_29_backwards : string -> bits(29) +function hex_bits_29_backwards s = + match hex_bits_29_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_30 : bits(30) <-> string +val hex_bits_30_forwards = "decimal_string_of_bits" : bits(30) -> string +val hex_bits_30_forwards_matches : bits(30) -> bool +function hex_bits_30_forwards_matches bv = true +val "hex_bits_30_matches_prefix" : string -> option((bits(30), nat)) +val hex_bits_30_backwards_matches : string -> bool +function hex_bits_30_backwards_matches s = match s { + s if match hex_bits_30_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_30_backwards : string -> bits(30) +function hex_bits_30_backwards s = + match hex_bits_30_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_31 : bits(31) <-> string +val hex_bits_31_forwards = "decimal_string_of_bits" : bits(31) -> string +val hex_bits_31_forwards_matches : bits(31) -> bool +function hex_bits_31_forwards_matches bv = true +val "hex_bits_31_matches_prefix" : string -> option((bits(31), nat)) +val hex_bits_31_backwards_matches : string -> bool +function hex_bits_31_backwards_matches s = match s { + s if match hex_bits_31_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_31_backwards : string -> bits(31) +function hex_bits_31_backwards s = + match hex_bits_31_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_32 : bits(32) <-> string +val hex_bits_32_forwards = "decimal_string_of_bits" : bits(32) -> string +val hex_bits_32_forwards_matches : bits(32) -> bool +function hex_bits_32_forwards_matches bv = true +val "hex_bits_32_matches_prefix" : string -> option((bits(32), nat)) +val hex_bits_32_backwards_matches : string -> bool +function hex_bits_32_backwards_matches s = match s { + s if match hex_bits_32_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_32_backwards : string -> bits(32) +function hex_bits_32_backwards s = + match hex_bits_32_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_33 : bits(33) <-> string +val hex_bits_33_forwards = "decimal_string_of_bits" : bits(33) -> string +val hex_bits_33_forwards_matches : bits(33) -> bool +function hex_bits_33_forwards_matches bv = true +val "hex_bits_33_matches_prefix" : string -> option((bits(33), nat)) +val hex_bits_33_backwards_matches : string -> bool +function hex_bits_33_backwards_matches s = match s { + s if match hex_bits_33_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_33_backwards : string -> bits(33) +function hex_bits_33_backwards s = + match hex_bits_33_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_48 : bits(48) <-> string +val hex_bits_48_forwards = "decimal_string_of_bits" : bits(48) -> string +val hex_bits_48_forwards_matches : bits(48) -> bool +function hex_bits_48_forwards_matches bv = true +val "hex_bits_48_matches_prefix" : string -> option((bits(48), nat)) +val hex_bits_48_backwards_matches : string -> bool +function hex_bits_48_backwards_matches s = match s { + s if match hex_bits_48_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_48_backwards : string -> bits(48) +function hex_bits_48_backwards s = + match hex_bits_48_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + +val hex_bits_64 : bits(64) <-> string +val hex_bits_64_forwards = "decimal_string_of_bits" : bits(64) -> string +val hex_bits_64_forwards_matches : bits(64) -> bool +function hex_bits_64_forwards_matches bv = true +val "hex_bits_64_matches_prefix" : string -> option((bits(64), nat)) +val hex_bits_64_backwards_matches : string -> bool +function hex_bits_64_backwards_matches s = match s { + s if match hex_bits_64_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_64_backwards : string -> bits(64) +function hex_bits_64_backwards s = + match hex_bits_64_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } + diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail new file mode 100644 index 0000000..8e483f8 --- /dev/null +++ b/model/prelude_mem.sail @@ -0,0 +1,70 @@ +/* These functions define the primitives for physical memory access. + * They depend on the XLEN of the architecture. + */ + +val __WriteRAM = {lem: "MEMw", _: "write_ram"} : forall 'n 'm. + (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} + +val __WriteRAM_release = {lem: "MEMw_release", _: "write_ram"} : forall 'n 'm. + (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} + +val __WriteRAM_strong_release = {lem: "MEMw_strong_release", _: "write_ram"} : forall 'n 'm. + (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} + +val __WriteRAM_conditional = {lem: "MEMw_conditional", _: "write_ram"} : forall 'n 'm. + (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} + +val __WriteRAM_conditional_release = {lem: "MEMw_conditional_release", _: "write_ram"} : forall 'n 'm. + (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} + +val __WriteRAM_conditional_strong_release = {lem: "MEMw_conditional_strong_release", _: "write_ram"} : forall 'n 'm. + (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} + +val __RISCV_write : forall 'n. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> bool effect {wmv} +function __RISCV_write (addr, width, data, aq, rl, con) = + match (aq, rl, con) { + (false, false, false) => __WriteRAM(sizeof(xlen), width, EXTZ(0x0), addr, data), + (false, true, false) => __WriteRAM_release(sizeof(xlen), width, EXTZ(0x0), addr, data), + (false, false, true) => __WriteRAM_conditional(sizeof(xlen), width, EXTZ(0x0), addr, data), + (false, true, true) => __WriteRAM_conditional_release(sizeof(xlen), width, EXTZ(0x0), addr, data), + (true, true, false) => __WriteRAM_strong_release(sizeof(xlen), width, EXTZ(0x0), addr, data), + (true, true, true) => __WriteRAM_conditional_strong_release(sizeof(xlen), width, EXTZ(0x0), addr, data), + (true, false, false) => false, + (true, false, true) => false + } + +val __TraceMemoryWrite : forall 'n 'm. + (atom('n), bits('m), bits(8 * 'n)) -> unit + +val __ReadRAM = { lem: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0. + (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} + +val __ReadRAM_acquire = { lem: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0. + (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} + +val __ReadRAM_strong_acquire = { lem: "MEMr_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0. + (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} + +val __ReadRAM_reserved = { lem: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm, 'n >= 0. + (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} + +val __ReadRAM_reserved_acquire = { lem: "MEMr_reserved_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0. + (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} + +val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0. + (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} + +val __RISCV_read : forall 'n, 'n >= 0. (xlenbits, atom('n), bool, bool, bool) -> option(bits(8 * 'n)) effect {rmem} +function __RISCV_read (addr, width, aq, rl, res) = + match (aq, rl, res) { + (false, false, false) => Some(__ReadRAM(sizeof(xlen), width, EXTZ(0x0), addr)), + (true, false, false) => Some(__ReadRAM_acquire(sizeof(xlen), width, EXTZ(0x0), addr)), + (true, true, false) => Some(__ReadRAM_strong_acquire(sizeof(xlen), width, EXTZ(0x0), addr)), + (false, false, true) => Some(__ReadRAM_reserved(sizeof(xlen), width, EXTZ(0x0), addr)), + (true, false, true) => Some(__ReadRAM_reserved_acquire(sizeof(xlen), width, EXTZ(0x0), addr)), + (true, true, true) => Some(__ReadRAM_reserved_strong_acquire(sizeof(xlen), width, EXTZ(0x0), addr)), + (false, true, false) => None(), + (false, true, true) => None() + } + +val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit diff --git a/model/riscv_duopod.sail b/model/riscv_duopod.sail index f7a7712..99dbbba 100644 --- a/model/riscv_duopod.sail +++ b/model/riscv_duopod.sail @@ -1,6 +1,4 @@ - -type xlen = atom(64) -type xlen_t = bits(64) +// This file depends on the xlen definitions in riscv_xlen.sail. type regno ('n : Int), 0 <= 'n < 32 = atom('n) type regbits = bits(5) @@ -13,18 +11,18 @@ function regbits_to_regno b = let r as atom(_) = unsigned(b) in r /* Architectural state */ -register PC : xlen_t -register nextPC : xlen_t +register PC : xlenbits +register nextPC : xlenbits -register Xs : vector(32, dec, xlen_t) +register Xs : vector(32, dec, xlenbits) /* Getters and setters for X registers (special case for zeros register, x0) */ -val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlen_t effect {rreg} +val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg} -function rX 0 = 0x0000000000000000 +function rX 0 = EXTZ(0x0) and rX (r if r > 0) = Xs[r] -val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlen_t) -> unit effect {wreg} +val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg} function wX (r, v) = if r != 0 then { @@ -35,7 +33,7 @@ overload X = {rX, wX} /* Accessors for memory */ -val MEMr : forall 'n, 'n >= 0. (xlen_t, atom('n)) -> bits(8 * 'n) effect {rmem} +val MEMr : forall 'n, 'n >= 0. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem} function MEMr (addr, width) = match __RISCV_read(addr, width, false, false, false) { Some(v) => v, @@ -61,7 +59,7 @@ function clause decode imm : bits(12) @ rs1 : regbits @ 0b000 @ rd : regbits @ 0 function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) = let rs1_val = X(rs1) in - let imm_ext : xlen_t = EXTS(imm) in + let imm_ext : xlenbits = EXTS(imm) in let result = rs1_val + imm_ext in X(rd) = result @@ -74,8 +72,8 @@ function clause decode imm : bits(12) @ rs1 : regbits @ 0b011 @ rd : regbits @ 0 = Some(LOAD(imm, rs1, rd)) function clause execute(LOAD(imm, rs1, rd)) = - let addr : xlen_t = X(rs1) + EXTS(imm) in - let result : xlen_t = MEMr(addr, 8) in + let addr : xlenbits = X(rs1) + EXTS(imm) in + let result : xlenbits = MEMr(addr, xlen_bytes) in X(rd) = result /* ****************************************************************** */ diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 2f93cc5..7042583 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -32,7 +32,7 @@ mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) * call to load_reservation in LR and cancel_reservation in SC. */ -val process_loadres : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> bool effect {escape, rreg, wreg} +val process_loadres : forall 'n, 0 < 'n <= xlen_bytes. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> bool effect {escape, rreg, wreg} function process_loadres(rd, addr, value, is_unsigned) = match extend_value(is_unsigned, value) { MemValue(result) => { load_reservation(addr); X(rd) = result; true }, @@ -53,17 +53,17 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = { DOUBLE => vaddr[2..0] == 0b000 }; /* "LR faults like a normal load, even though it's in the AMO major opcode space." - - Andrew Waterman, isa-dev, 10 Jul 2018. + * - Andrew Waterman, isa-dev, 10 Jul 2018. */ if (~ (aligned)) then { handle_mem_exception(vaddr, E_Load_Addr_Align); false } else match translateAddr(vaddr, Read, Data) { TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, TR_Address(addr) => - match width { - WORD => process_loadres(rd, vaddr, mem_read(addr, 4, aq, rl, true), false), - DOUBLE => process_loadres(rd, vaddr, mem_read(addr, 8, aq, rl, true), false), - _ => internal_error("LOADRES expected WORD or DOUBLE") + match (width, sizeof(xlen)) { + (WORD, _) => process_loadres(rd, vaddr, mem_read(addr, 4, aq, rl, true), false), + (DOUBLE, 64) => process_loadres(rd, vaddr, mem_read(addr, 8, aq, rl, true), false), + _ => internal_error("LOADRES expected WORD or DOUBLE") } } } else { @@ -109,24 +109,24 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { else { if match_reservation(vaddr) == false then { /* cannot happen in rmem */ - X(rd) = EXTZ(0b1); true + X(rd) = EXTZ(0b1); cancel_reservation(); true } else { match translateAddr(vaddr, Write, Data) { TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, TR_Address(addr) => { - let eares : MemoryOpResult(unit) = match width { - WORD => mem_write_ea(addr, 4, aq, rl, true), - DOUBLE => mem_write_ea(addr, 8, aq, rl, true), - _ => internal_error("STORECON expected word or double") + let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) { + (WORD, _) => mem_write_ea(addr, 4, aq, rl, true), + (DOUBLE, 64) => mem_write_ea(addr, 8, aq, rl, true), + _ => internal_error("STORECON expected word or double") }; match (eares) { MemException(e) => { handle_mem_exception(addr, e); false }, MemValue(_) => { rs2_val = X(rs2); - let res : MemoryOpResult(bool) = match width { - WORD => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true), - DOUBLE => mem_write_value(addr, 8, rs2_val, aq, rl, true), - _ => internal_error("STORECON expected word or double") + let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) { + (WORD, _) => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true), + (DOUBLE, 64) => mem_write_value(addr, 8, rs2_val, aq, rl, true), + _ => internal_error("STORECON expected word or double") }; match (res) { MemValue(true) => { X(rd) = EXTZ(0b0); cancel_reservation(); true }, @@ -175,19 +175,19 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { match translateAddr(vaddr, ReadWrite, Data) { TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, TR_Address(addr) => { - let eares : MemoryOpResult(unit) = match width { - WORD => mem_write_ea(addr, 4, aq & rl, rl, true), - DOUBLE => mem_write_ea(addr, 8, aq & rl, rl, true), - _ => internal_error ("AMO expected WORD or DOUBLE") + let eares : MemoryOpResult(unit) = match (width, sizeof(xlen)) { + (WORD, _) => mem_write_ea(addr, 4, aq & rl, rl, true), + (DOUBLE, 64) => mem_write_ea(addr, 8, aq & rl, rl, true), + _ => internal_error ("AMO expected WORD or DOUBLE") }; rs2_val : xlenbits = X(rs2); match (eares) { MemException(e) => { handle_mem_exception(addr, e); false }, MemValue(_) => { - let rval : MemoryOpResult(xlenbits) = match width { - WORD => extend_value(false, mem_read(addr, 4, aq, aq & rl, true)), - DOUBLE => extend_value(false, mem_read(addr, 8, aq, aq & rl, true)), - _ => internal_error ("AMO expected WORD or DOUBLE") + let rval : MemoryOpResult(xlenbits) = match (width, sizeof(xlen)) { + (WORD, _) => extend_value(false, mem_read(addr, 4, aq, aq & rl, true)), + (DOUBLE, 64) => extend_value(false, mem_read(addr, 8, aq, aq & rl, true)), + _ => internal_error ("AMO expected WORD or DOUBLE") }; match (rval) { MemException(e) => { handle_mem_exception(addr, e); false }, @@ -200,17 +200,19 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { AMOAND => rs2_val & loaded, AMOOR => rs2_val | loaded, - /* Have to convert number to vector here. Check this */ - AMOMIN => vector64(min(signed(rs2_val), signed(loaded))), - AMOMAX => vector64(max(signed(rs2_val), signed(loaded))), - AMOMINU => vector64(min(unsigned(rs2_val), unsigned(loaded))), - AMOMAXU => vector64(max(unsigned(rs2_val), unsigned(loaded))) + /* These operations convert bitvectors to integer values using [un]signed, + * and back using to_bits(). + */ + AMOMIN => to_bits(sizeof(xlen), min(signed(rs2_val), signed(loaded))), + AMOMAX => to_bits(sizeof(xlen), max(signed(rs2_val), signed(loaded))), + AMOMINU => to_bits(sizeof(xlen), min(unsigned(rs2_val), unsigned(loaded))), + AMOMAXU => to_bits(sizeof(xlen), max(unsigned(rs2_val), unsigned(loaded))) }; - let wval : MemoryOpResult(bool) = match width { - WORD => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true), - DOUBLE => mem_write_value(addr, 8, result, aq & rl, rl, true), - _ => internal_error("AMO expected WORD or DOUBLE") + let wval : MemoryOpResult(bool) = match (width, sizeof(xlen)) { + (WORD, _) => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true), + (DOUBLE, 64) => mem_write_value(addr, 8, result, aq & rl, rl, true), + _ => internal_error("AMO expected WORD or DOUBLE") }; match (wval) { MemValue(true) => { X(rd) = loaded; true }, diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 3f8eac8..8ae4923 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -179,16 +179,23 @@ mapping encdec_sop : sop <-> bits(3) = { RISCV_SRAI <-> 0b101 } -mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SLLI) <-> 0b000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 -mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRLI) <-> 0b000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 -mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRAI) <-> 0b010000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 +mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SLLI) <-> 0b000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == false +mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRLI) <-> 0b000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == false +mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRAI) <-> 0b010000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == false function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = { let rs1_val = X(rs1); + /* the decoder guard should ensure that shamt[5] = 0 for RV32 */ let result : xlenbits = match op { - RISCV_SLLI => rs1_val << shamt, - RISCV_SRLI => rs1_val >> shamt, - RISCV_SRAI => shift_right_arith64(rs1_val, shamt) + RISCV_SLLI => if sizeof(xlen) == 32 + then rs1_val << shamt[4..0] + else rs1_val << shamt, + RISCV_SRLI => if sizeof(xlen) == 32 + then rs1_val >> shamt[4..0] + else rs1_val >> shamt, + RISCV_SRAI => if sizeof(xlen) == 32 + then shift_right_arith32(rs1_val, shamt[4..0]) + else shift_right_arith64(rs1_val, shamt) }; X(rd) = result; true @@ -227,10 +234,16 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) = { RISCV_AND => rs1_val & rs2_val, RISCV_OR => rs1_val | rs2_val, RISCV_XOR => rs1_val ^ rs2_val, - RISCV_SLL => rs1_val << (rs2_val[5..0]), - RISCV_SRL => rs1_val >> (rs2_val[5..0]), + RISCV_SLL => if sizeof(xlen) == 32 + then rs1_val << (rs2_val[4..0]) + else rs1_val << (rs2_val[5..0]), + RISCV_SRL => if sizeof(xlen) == 32 + then rs1_val >> (rs2_val[4..0]) + else rs1_val >> (rs2_val[5..0]), RISCV_SUB => rs1_val - rs2_val, - RISCV_SRA => shift_right_arith64(rs1_val, rs2_val[5..0]) + RISCV_SRA => if sizeof(xlen) == 32 + then shift_right_arith32(rs1_val, rs2_val[4..0]) + else shift_right_arith64(rs1_val, rs2_val[5..0]) }; X(rd) = result; true @@ -260,13 +273,13 @@ union clause ast = LOAD : (bits(12), regbits, regbits, bool, word_width, bool, b mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if size_bits(size) != 0b11 | not_bool(is_unsigned) <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_bits(size) @ rd @ 0b0000011 if size_bits(size) != 0b11 | not_bool(is_unsigned) -val extend_value : forall 'n, 0 < 'n <= 8. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits) +val extend_value : forall 'n, 0 < 'n <= xlen_bytes. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits) function extend_value(is_unsigned, value) = match (value) { MemValue(v) => MemValue(if is_unsigned then EXTZ(v) else EXTS(v) : xlenbits), MemException(e) => MemException(e) } -val process_load : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> bool effect {escape, rreg, wreg} +val process_load : forall 'n, 0 < 'n <= xlen_bytes. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> bool effect {escape, rreg, wreg} function process_load(rd, addr, value, is_unsigned) = match extend_value(is_unsigned, value) { MemValue(result) => { X(rd) = result; true }, @@ -289,14 +302,14 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = { else match translateAddr(vaddr, Read, Data) { TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, TR_Address(addr) => - match width { - BYTE => + match (width, sizeof(xlen)) { + (BYTE, _) => process_load(rd, vaddr, mem_read(addr, 1, aq, rl, false), is_unsigned), - HALF => + (HALF, _) => process_load(rd, vaddr, mem_read(addr, 2, aq, rl, false), is_unsigned), - WORD => + (WORD, _) => process_load(rd, vaddr, mem_read(addr, 4, aq, rl, false), is_unsigned), - DOUBLE => + (DOUBLE, 64) => process_load(rd, vaddr, mem_read(addr, 8, aq, rl, false), is_unsigned) } } @@ -349,11 +362,11 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = { MemException(e) => { handle_mem_exception(addr, e); false }, MemValue(_) => { let rs2_val = X(rs2); - let res : MemoryOpResult(bool) = match width { - BYTE => mem_write_value(addr, 1, rs2_val[7..0], aq, rl, false), - HALF => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false), - WORD => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false), - DOUBLE => mem_write_value(addr, 8, rs2_val, aq, rl, false) + let res : MemoryOpResult(bool) = match (width, sizeof(xlen)) { + (BYTE, _) => mem_write_value(addr, 1, rs2_val[7..0], aq, rl, false), + (HALF, _) => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false), + (WORD, _) => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false), + (DOUBLE, 64) => mem_write_value(addr, 8, rs2_val, aq, rl, false) }; match (res) { MemValue(true) => true, @@ -373,7 +386,9 @@ mapping clause assembly = STORE(imm, rs1, rd, size, aq, rl) union clause ast = ADDIW : (bits(12), regbits, regbits) mapping clause encdec = ADDIW(imm, rs1, rd) + if sizeof(xlen) == 64 <-> imm @ rs1 @ 0b000 @ rd @ 0b0011011 + if sizeof(xlen) == 64 function clause execute (ADDIW(imm, rs1, rd)) = { let result : xlenbits = EXTS(imm) + X(rs1); @@ -382,14 +397,25 @@ function clause execute (ADDIW(imm, rs1, rd)) = { } mapping clause assembly = ADDIW(imm, rs1, rd) + if sizeof(xlen) == 64 <-> "addiw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm) + if sizeof(xlen) == 64 /* ****************************************************************** */ union clause ast = SHIFTW : (bits(5), regbits, regbits, sop) -mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SLLI) <-> 0b0000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011 -mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SRLI) <-> 0b0000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 -mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SRAI) <-> 0b0100000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 +mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SLLI) + if sizeof(xlen) == 64 + <-> 0b0000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011 + if sizeof(xlen) == 64 +mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SRLI) + if sizeof(xlen) == 64 + <-> 0b0000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 + if sizeof(xlen) == 64 +mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SRAI) + if sizeof(xlen) == 64 + <-> 0b0100000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 + if sizeof(xlen) == 64 function clause execute (SHIFTW(shamt, rs1, rd, op)) = { let rs1_val = (X(rs1))[31..0]; @@ -409,16 +435,33 @@ mapping shiftw_mnemonic : sop <-> string = { } mapping clause assembly = SHIFTW(shamt, rs1, rd, op) + if sizeof(xlen) == 64 <-> shiftw_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_5(shamt) + if sizeof(xlen) == 64 /* ****************************************************************** */ union clause ast = RTYPEW : (regbits, regbits, regbits, ropw) -mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_ADDW) <-> 0b0000000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 -mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SUBW) <-> 0b0100000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 -mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SLLW) <-> 0b0000000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011 -mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SRLW) <-> 0b0000000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 -mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SRAW) <-> 0b0100000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 +mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_ADDW) + if sizeof(xlen) == 64 + <-> 0b0000000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 + if sizeof(xlen) == 64 +mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SUBW) + if sizeof(xlen) == 64 + <-> 0b0100000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 + if sizeof(xlen) == 64 +mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SLLW) + if sizeof(xlen) == 64 + <-> 0b0000000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011 + if sizeof(xlen) == 64 +mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SRLW) + if sizeof(xlen) == 64 + <-> 0b0000000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 + if sizeof(xlen) == 64 +mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SRAW) + if sizeof(xlen) == 64 + <-> 0b0100000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 + if sizeof(xlen) == 64 function clause execute (RTYPEW(rs2, rs1, rd, op)) = { let rs1_val = (X(rs1))[31..0]; @@ -443,23 +486,34 @@ mapping rtypew_mnemonic : ropw <-> string = { } mapping clause assembly = RTYPEW(rs2, rs1, rd, op) + if sizeof(xlen) == 64 <-> rtypew_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) + if sizeof(xlen) == 64 /* ****************************************************************** */ union clause ast = SHIFTIWOP : (bits(5), regbits, regbits, sopw) -mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SLLIW) <-> 0b0000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011 -mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SRLIW) <-> 0b0000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 -mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SRAIW) <-> 0b0100000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 +mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SLLIW) + if sizeof(xlen) == 64 + <-> 0b0000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011 + if sizeof(xlen) == 64 +mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SRLIW) + if sizeof(xlen) == 64 + <-> 0b0000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 + if sizeof(xlen) == 64 +mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SRAIW) + if sizeof(xlen) == 64 + <-> 0b0100000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 + if sizeof(xlen) == 64 function clause execute (SHIFTIWOP(shamt, rs1, rd, op)) = { let rs1_val = X(rs1); - let result : xlenbits = match op { - RISCV_SLLIW => EXTS(rs1_val[31..0] << shamt), - RISCV_SRLIW => EXTS(rs1_val[31..0] >> shamt), - RISCV_SRAIW => EXTS(shift_right_arith32(rs1_val[31..0], shamt)) + let result : bits(32) = match op { + RISCV_SLLIW => rs1_val[31..0] << shamt, + RISCV_SRLIW => rs1_val[31..0] >> shamt, + RISCV_SRAIW => shift_right_arith32(rs1_val[31..0], shamt) }; - X(rd) = result; + X(rd) = EXTS(result); true } @@ -470,7 +524,9 @@ mapping shiftiwop_mnemonic : sopw <-> string = { } mapping clause assembly = SHIFTIWOP(shamt, rs1, rd, op) + if sizeof(xlen) == 64 <-> shiftiwop_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_5(shamt) + if sizeof(xlen) == 64 /* ****************************************************************** */ union clause ast = FENCE : (bits(4), bits(4)) @@ -649,18 +705,16 @@ mapping clause encdec = SFENCE_VMA(rs1, rs2) <-> 0b0001001 @ rs2 @ rs1 @ 0b000 @ 0b00000 @ 0b1110011 function clause execute SFENCE_VMA(rs1, rs2) = { - /* TODO: handle PMP/TLB synchronization when executed in M-mode. */ - if cur_privilege == User - then { handle_illegal(); false } - else match (architecture(mstatus.SXL()), mstatus.TVM()) { - (Some(RV64), true) => { handle_illegal(); false }, - (Some(RV64), false) => { - let addr : option(vaddr39) = if rs1 == 0 then None() else Some(X(rs1)[38 .. 0]); - let asid : option(asid64) = if rs2 == 0 then None() else Some(X(rs2)[15 .. 0]); - flushTLB(asid, addr); - true - }, - (_, _) => internal_error("unimplemented sfence architecture") + let addr : option(xlenbits) = if rs1 == 0 then None() else Some(X(rs1)); + let asid : option(xlenbits) = if rs2 == 0 then None() else Some(X(rs2)); + match cur_privilege { + User => { handle_illegal(); false }, + Supervisor => match (architecture(get_mstatus_SXL(mstatus)), mstatus.TVM()) { + (Some(_), true) => { handle_illegal(); false }, + (Some(_), false) => { flush_TLB(asid, addr); true }, + (_, _) => internal_error("unimplemented sfence architecture") + }, + Machine => { flush_TLB(asid, addr); true } } } diff --git a/model/riscv_insts_cext.sail b/model/riscv_insts_cext.sail index 9feced0..70d4978 100644 --- a/model/riscv_insts_cext.sail +++ b/model/riscv_insts_cext.sail @@ -56,7 +56,9 @@ mapping clause assembly = C_LW(uimm, rsc, rdc) union clause ast = C_LD : (bits(5), cregbits, cregbits) mapping clause encdec_compressed = C_LD(ui76 @ ui53, rs1, rd) + if sizeof(xlen) == 64 <-> 0b011 @ ui53 : bits(3) @ rs1 : cregbits @ ui76 : bits(2) @ rd : cregbits @ 0b00 + if sizeof(xlen) == 64 function clause execute (C_LD(uimm, rsc, rdc)) = { let imm : bits(12) = EXTZ(uimm @ 0b000); @@ -66,7 +68,9 @@ function clause execute (C_LD(uimm, rsc, rdc)) = { } mapping clause assembly = C_LD(uimm, rsc, rdc) + if sizeof(xlen) == 64 <-> "c.ld" ^ spc() ^ creg_name(rdc) ^ sep() ^ creg_name(rsc) ^ sep() ^ hex_bits_8(uimm @ 0b000) + if sizeof(xlen) == 64 /* ****************************************************************** */ union clause ast = C_SW : (bits(5), cregbits, cregbits) @@ -88,7 +92,9 @@ mapping clause assembly = C_SW(uimm, rsc1, rsc2) union clause ast = C_SD : (bits(5), cregbits, cregbits) mapping clause encdec_compressed = C_SD(ui76 @ ui53, rs1, rs2) + if sizeof(xlen) == 64 <-> 0b111 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00 + if sizeof(xlen) == 64 function clause execute (C_SD(uimm, rsc1, rsc2)) = { let imm : bits(12) = EXTZ(uimm @ 0b000); @@ -98,7 +104,9 @@ function clause execute (C_SD(uimm, rsc1, rsc2)) = { } mapping clause assembly = C_SD(uimm, rsc1, rsc2) + if sizeof(xlen) == 64 <-> "c.sd" ^ spc() ^ creg_name(rsc1) ^ sep() ^ creg_name(rsc2) ^ sep() ^ hex_bits_8(uimm @ 0b000) + if sizeof(xlen) == 64 /* ****************************************************************** */ union clause ast = C_ADDI : (bits(6), regbits) @@ -120,19 +128,28 @@ mapping clause assembly = C_ADDI(nzi, rsd) /* ****************************************************************** */ union clause ast = C_JAL : (bits(11)) -union clause ast = C_ADDIW : (bits(6), regbits) -/* FIXME: decoding differs for RVC32/RVC64. Below, we are assuming - * RV64, and C_JAL is RV32 only. */ - -mapping clause encdec_compressed = C_ADDIW(imm5 @ imm40, rsd) - if rsd != zreg - <-> 0b001 @ imm5 : bits(1) @ rsd : regbits @ imm40 : bits(5) @ 0b01 - if rsd != zreg +mapping clause encdec_compressed = C_JAL(i11 @ i10 @ i98 @ i7 @ i6 @ i5 @ i4 @ i31) + if sizeof(xlen) == 32 + <-> 0b001 @ i11 : bits(1) @ i4 : bits(1) @ i98 : bits(2) @ i10 : bits(1) @ i6 : bits(1) @ i7 : bits(1) @ i31 : bits(3) @ i5 : bits(1) @ 0b01 + if sizeof(xlen) == 32 function clause execute (C_JAL(imm)) = execute(RISCV_JAL(EXTS(imm @ 0b0), ra)) +mapping clause assembly = C_JAL(imm) + if sizeof(xlen) == 32 + <-> "c.jal" ^ spc() ^ hex_bits_12(imm @ 0b0) + if sizeof(xlen) == 32 + +/* ****************************************************************** */ +union clause ast = C_ADDIW : (bits(6), regbits) + +mapping clause encdec_compressed = C_ADDIW(imm5 @ imm40, rsd) + if rsd != zreg & sizeof(xlen) == 64 + <-> 0b001 @ imm5 : bits(1) @ rsd : regbits @ imm40 : bits(5) @ 0b01 + if rsd != zreg & sizeof(xlen) == 64 + function clause execute (C_ADDIW(imm, rsd)) = { let imm : bits(32) = EXTS(imm); let rs_val = X(rsd); @@ -141,11 +158,10 @@ function clause execute (C_ADDIW(imm, rsd)) = { true } -mapping clause assembly = C_JAL(imm) - <-> "c.jal" ^ spc() ^ hex_bits_12(imm @ 0b0) - mapping clause assembly = C_ADDIW(imm, rsd) + if sizeof(xlen) == 64 <-> "c.addiw" ^ spc() ^ reg_name(rsd) ^ sep() ^ hex_bits_6(imm) + if sizeof(xlen) == 64 /* ****************************************************************** */ union clause ast = C_LI : (bits(6), regbits) @@ -316,7 +332,9 @@ union clause ast = C_SUBW : (cregbits, cregbits) /* TODO: invalid on RV32 */ mapping clause encdec_compressed = C_SUBW(rsd, rs2) + if sizeof(xlen) == 64 <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b00 @ rs2 : cregbits @ 0b01 + if sizeof(xlen) == 64 function clause execute (C_SUBW(rsd, rs2)) = { let rsd = creg2reg_bits(rsd); @@ -325,14 +343,18 @@ function clause execute (C_SUBW(rsd, rs2)) = { } mapping clause assembly = C_SUBW(rsd, rs2) + if sizeof(xlen) == 64 <-> "c.subw" ^ spc() ^ creg_name(rsd) ^ sep() ^ creg_name(rs2) + if sizeof(xlen) == 64 /* ****************************************************************** */ union clause ast = C_ADDW : (cregbits, cregbits) /* TODO: invalid on RV32 */ mapping clause encdec_compressed = C_ADDW(rsd, rs2) + if sizeof(xlen) == 64 <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b01 @ rs2 : cregbits @ 0b01 + if sizeof(xlen) == 64 function clause execute (C_ADDW(rsd, rs2)) = { let rsd = creg2reg_bits(rsd); @@ -341,7 +363,9 @@ function clause execute (C_ADDW(rsd, rs2)) = { } mapping clause assembly = C_ADDW(rsd, rs2) + if sizeof(xlen) == 64 <-> "c.addw" ^ spc() ^ creg_name(rsd) ^ sep() ^ creg_name(rs2) + if sizeof(xlen) == 64 /* ****************************************************************** */ union clause ast = C_J : (bits(11)) @@ -412,9 +436,9 @@ mapping clause assembly = C_LWSP(uimm, rd) union clause ast = C_LDSP : (bits(6), regbits) mapping clause encdec_compressed = C_LDSP(ui86 @ ui5 @ ui43, rd) - if rd != zreg + if rd != zreg & sizeof(xlen) == 64 <-> 0b011 @ ui5 : bits(1) @ rd : regbits @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10 - if rd != zreg + if rd != zreg & sizeof(xlen) == 64 function clause execute (C_LDSP(uimm, rd)) = { let imm : bits(12) = EXTZ(uimm @ 0b000); @@ -422,9 +446,9 @@ function clause execute (C_LDSP(uimm, rd)) = { } mapping clause assembly = C_LDSP(uimm, rd) - if rd != zreg + if rd != zreg & sizeof(xlen) == 64 <-> "c.ldsp" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_6(uimm) - if rd != zreg + if rd != zreg & sizeof(xlen) == 64 /* ****************************************************************** */ union clause ast = C_SWSP : (bits(6), regbits) @@ -444,7 +468,9 @@ mapping clause assembly = C_SWSP(uimm, rd) union clause ast = C_SDSP : (bits(6), regbits) mapping clause encdec_compressed = C_SDSP(ui86 @ ui53, rs2) + if sizeof(xlen) == 64 <-> 0b111 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regbits @ 0b10 + if sizeof(xlen) == 64 function clause execute (C_SDSP(uimm, rs2)) = { let imm : bits(12) = EXTZ(uimm @ 0b000); @@ -452,7 +478,9 @@ function clause execute (C_SDSP(uimm, rs2)) = { } mapping clause assembly = C_SDSP(uimm, rs2) + if sizeof(xlen) == 64 <-> "c.sdsp" ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_6(uimm) + if sizeof(xlen) == 64 /* ****************************************************************** */ union clause ast = C_JR : (regbits) diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail index 0908a7b..cab8d9c 100644 --- a/model/riscv_insts_mext.sail +++ b/model/riscv_insts_mext.sail @@ -22,8 +22,10 @@ function clause execute (MUL(rs2, rs1, rd, high, signed1, signed2)) = { let rs2_val = X(rs2); let rs1_int : int = if signed1 then signed(rs1_val) else unsigned(rs1_val); let rs2_int : int = if signed2 then signed(rs2_val) else unsigned(rs2_val); - let result128 = to_bits(128, rs1_int * rs2_int); - let result = if high then result128[127..64] else result128[63..0]; + let result_wide = to_bits(2 * sizeof(xlen), rs1_int * rs2_int); + let result = if high + then result_wide[(2 * sizeof(xlen) - 1) .. sizeof(xlen)] + else result_wide[(sizeof(xlen) - 1) .. 0]; X(rd) = result; true } else { @@ -57,7 +59,7 @@ function clause execute (DIV(rs2, rs1, rd, s)) = { let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int); /* check for signed overflow */ let q': int = if s & q > xlen_max_signed then xlen_min_signed else q; - X(rd) = to_bits(xlen, q'); + X(rd) = to_bits(sizeof(xlen), q'); true } else { handle_illegal(); @@ -87,7 +89,7 @@ function clause execute (REM(rs2, rs1, rd, s)) = { let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val); let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int); /* signed overflow case returns zero naturally as required due to -1 divisor */ - X(rd) = to_bits(xlen, r); + X(rd) = to_bits(sizeof(xlen), r); true } else { handle_illegal(); @@ -101,7 +103,10 @@ mapping clause assembly = REM(rs2, rs1, rd, s) /* ****************************************************************** */ union clause ast = MULW : (regbits, regbits, regbits) -mapping clause encdec = MULW(rs2, rs1, rd) <-> 0b0000001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 +mapping clause encdec = MULW(rs2, rs1, rd) + if sizeof(xlen) == 64 + <-> 0b0000001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 + if sizeof(xlen) == 64 function clause execute (MULW(rs2, rs1, rd)) = { if haveMulDiv() then { @@ -121,13 +126,17 @@ function clause execute (MULW(rs2, rs1, rd)) = { } mapping clause assembly = MULW(rs2, rs1, rd) + if sizeof(xlen) == 64 <-> "mulw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) + if sizeof(xlen) == 64 /* ****************************************************************** */ union clause ast = DIVW : (regbits, regbits, regbits, bool) mapping clause encdec = DIVW(rs2, rs1, rd, s) + if sizeof(xlen) == 64 <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0111011 + if sizeof(xlen) == 64 function clause execute (DIVW(rs2, rs1, rd, s)) = { if haveMulDiv() then { @@ -147,13 +156,17 @@ function clause execute (DIVW(rs2, rs1, rd, s)) = { } mapping clause assembly = DIVW(rs2, rs1, rd, s) + if sizeof(xlen) == 64 <-> "div" ^ maybe_not_u(s) ^ "w" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) + if sizeof(xlen) == 64 /* ****************************************************************** */ union clause ast = REMW : (regbits, regbits, regbits, bool) mapping clause encdec = REMW(rs2, rs1, rd, s) + if sizeof(xlen) == 64 <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0111011 + if sizeof(xlen) == 64 function clause execute (REMW(rs2, rs1, rd, s)) = { if haveMulDiv() then { @@ -172,4 +185,6 @@ function clause execute (REMW(rs2, rs1, rd, s)) = { } mapping clause assembly = REMW(rs2, rs1, rd, s) + if sizeof(xlen) == 64 <-> "rem" ^ maybe_not_u(s) ^ "w" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) + if sizeof(xlen) == 64 diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index aac2266..749f20c 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -15,56 +15,65 @@ mapping clause encdec = CSR(csr, rs1, rd, is_imm, op) function readCSR csr : csreg -> xlenbits = { let res : xlenbits = - match csr { + match (csr, sizeof(xlen)) { /* machine mode */ - 0xF11 => mvendorid, - 0xF12 => marchid, - 0xF13 => mimpid, - 0xF14 => mhartid, - 0x300 => mstatus.bits(), - 0x301 => misa.bits(), - 0x302 => medeleg.bits(), - 0x303 => mideleg.bits(), - 0x304 => mie.bits(), - 0x305 => mtvec.bits(), - 0x306 => EXTZ(mcounteren.bits()), - 0x340 => mscratch, - 0x341 => mepc & pc_alignment_mask(), - 0x342 => mcause.bits(), - 0x343 => mtval, - 0x344 => mip.bits(), - - 0x3A0 => pmpcfg0, - 0x3B0 => pmpaddr0, - - /* supervisor mode */ - 0x100 => lower_mstatus(mstatus).bits(), - 0x102 => sedeleg.bits(), - 0x103 => sideleg.bits(), - 0x104 => lower_mie(mie, mideleg).bits(), - 0x105 => stvec.bits(), - 0x106 => EXTZ(scounteren.bits()), - 0x140 => sscratch, - 0x141 => sepc & pc_alignment_mask(), - 0x142 => scause.bits(), - 0x143 => stval, - 0x144 => lower_mip(mip, mideleg).bits(), - 0x180 => satp, - - /* others */ - 0xC00 => mcycle, - 0xC01 => mtime, - 0xC02 => minstret, + (0xF11, _) => EXTZ(mvendorid), + (0xF12, _) => marchid, + (0xF13, _) => mimpid, + (0xF14, _) => mhartid, + (0x300, _) => mstatus.bits(), + (0x301, _) => misa.bits(), + (0x302, _) => medeleg.bits(), + (0x303, _) => mideleg.bits(), + (0x304, _) => mie.bits(), + (0x305, _) => mtvec.bits(), + (0x306, _) => EXTZ(mcounteren.bits()), + (0x340, _) => mscratch, + (0x341, _) => mepc & pc_alignment_mask(), + (0x342, _) => mcause.bits(), + (0x343, _) => mtval, + (0x344, _) => mip.bits(), + + (0x3A0, _) => pmpcfg0, + (0x3B0, _) => pmpaddr0, + + /* machine mode counters */ + (0xB00, _) => mcycle[(sizeof(xlen) - 1) .. 0], + (0xB02, _) => minstret[(sizeof(xlen) - 1) .. 0], + (0xB80, 32) => mcycle[63 .. 32], + (0xB82, 32) => minstret[63 .. 32], /* trigger/debug */ - 0x7a0 => ~(tselect), /* this indicates we don't have any trigger support */ - - _ => /* check extensions */ - match read_UExt_CSR(csr) { - Some(res) => res, - None() => { print_bits("unhandled read to CSR ", csr); - 0x0000_0000_0000_0000 } - } + (0x7a0, _) => ~(tselect), /* this indicates we don't have any trigger support */ + + /* supervisor mode */ + (0x100, _) => lower_mstatus(mstatus).bits(), + (0x102, _) => sedeleg.bits(), + (0x103, _) => sideleg.bits(), + (0x104, _) => lower_mie(mie, mideleg).bits(), + (0x105, _) => stvec.bits(), + (0x106, _) => EXTZ(scounteren.bits()), + (0x140, _) => sscratch, + (0x141, _) => sepc & pc_alignment_mask(), + (0x142, _) => scause.bits(), + (0x143, _) => stval, + (0x144, _) => lower_mip(mip, mideleg).bits(), + (0x180, _) => satp, + + /* user mode counters */ + (0xC00, _) => mcycle[(sizeof(xlen) - 1) .. 0], + (0xC01, _) => mtime[(sizeof(xlen) - 1) .. 0], + (0xC02, _) => minstret[(sizeof(xlen) - 1) .. 0], + (0xC80, 32) => mcycle[63 .. 32], + (0xC81, 32) => mtime[63 .. 32], + (0xC82, 32) => minstret[63 .. 32], + + _ => /* check extensions */ + match read_UExt_CSR(csr) { + Some(res) => res, + None() => { print_bits("unhandled read to CSR ", csr); + EXTZ(0x0) } + } }; print_reg("CSR " ^ csr ^ " -> " ^ BitStr(res)); res @@ -72,52 +81,53 @@ function readCSR csr : csreg -> xlenbits = { function writeCSR (csr : csreg, value : xlenbits) -> unit = { let res : option(xlenbits) = - match csr { + match (csr, sizeof(xlen)) { /* machine mode */ - 0x300 => { mstatus = legalize_mstatus(mstatus, value); Some(mstatus.bits()) }, - 0x301 => { misa = legalize_misa(misa, value); Some(misa.bits()) }, - 0x302 => { medeleg = legalize_medeleg(medeleg, value); Some(medeleg.bits()) }, - 0x303 => { mideleg = legalize_mideleg(mideleg, value); Some(mideleg.bits()) }, - 0x304 => { mie = legalize_mie(mie, value); Some(mie.bits()) }, - 0x305 => { mtvec = legalize_tvec(mtvec, value); Some(mtvec.bits()) }, - 0x306 => { mcounteren = legalize_mcounteren(mcounteren, value); Some(EXTZ(mcounteren.bits())) }, - 0x340 => { mscratch = value; Some(mscratch) }, - 0x341 => { mepc = legalize_xepc(value); Some(mepc) }, - 0x342 => { mcause->bits() = value; Some(mcause.bits()) }, - 0x343 => { mtval = value; Some(mtval) }, - 0x344 => { mip = legalize_mip(mip, value); Some(mip.bits()) }, - - 0x3A0 => { pmpcfg0 = value; Some(pmpcfg0) }, /* FIXME: legalize */ - 0x3B0 => { pmpaddr0 = value; Some(pmpaddr0) }, /* FIXME: legalize */ - - /* supervisor mode */ - 0x100 => { mstatus = legalize_sstatus(mstatus, value); Some(mstatus.bits()) }, - 0x102 => { sedeleg = legalize_sedeleg(sedeleg, value); Some(sedeleg.bits()) }, - 0x103 => { sideleg->bits() = value; Some(sideleg.bits()) }, /* TODO: does this need legalization? */ - 0x104 => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits()) }, - 0x105 => { stvec = legalize_tvec(stvec, value); Some(stvec.bits()) }, - 0x106 => { scounteren = legalize_scounteren(scounteren, value); Some(EXTZ(scounteren.bits())) }, - 0x140 => { sscratch = value; Some(sscratch) }, - 0x141 => { sepc = legalize_xepc(value); Some(sepc) }, - 0x142 => { scause->bits() = value; Some(scause.bits()) }, - 0x143 => { stval = value; Some(stval) }, - 0x144 => { mip = legalize_sip(mip, mideleg, value); Some(mip.bits()) }, - 0x180 => { satp = legalize_satp(cur_Architecture(), satp, value); Some(satp) }, + (0x300, _) => { mstatus = legalize_mstatus(mstatus, value); Some(mstatus.bits()) }, + (0x301, _) => { misa = legalize_misa(misa, value); Some(misa.bits()) }, + (0x302, _) => { medeleg = legalize_medeleg(medeleg, value); Some(medeleg.bits()) }, + (0x303, _) => { mideleg = legalize_mideleg(mideleg, value); Some(mideleg.bits()) }, + (0x304, _) => { mie = legalize_mie(mie, value); Some(mie.bits()) }, + (0x305, _) => { mtvec = legalize_tvec(mtvec, value); Some(mtvec.bits()) }, + (0x306, _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(EXTZ(mcounteren.bits())) }, + (0x340, _) => { mscratch = value; Some(mscratch) }, + (0x341, _) => { mepc = legalize_xepc(value); Some(mepc) }, + (0x342, _) => { mcause->bits() = value; Some(mcause.bits()) }, + (0x343, _) => { mtval = value; Some(mtval) }, + (0x344, _) => { mip = legalize_mip(mip, value); Some(mip.bits()) }, + + (0x3A0, _) => { pmpcfg0 = value; Some(pmpcfg0) }, /* FIXME: legalize */ + (0x3B0, _) => { pmpaddr0 = value; Some(pmpaddr0) }, /* FIXME: legalize */ + + /* machine mode counters */ + (0xB00, _) => { mcycle[(sizeof(xlen) - 1) .. 0] = value; Some(value) }, + (0xB02, _) => { minstret[(sizeof(xlen) - 1) .. 0] = value; minstret_written = true; Some(value) }, + (0xB80, 32) => { mcycle[63 .. 32] = value; Some(value) }, + (0xB82, 32) => { minstret[63 .. 32] = value; minstret_written = true; Some(value) }, /* trigger/debug */ - 0x7a0 => { tselect = value; Some(tselect) }, + (0x7a0, _) => { tselect = value; Some(tselect) }, - /* counters */ - 0xC00 => { mcycle = value; Some(mcycle) }, - /* FIXME: it is not clear whether writable mtime is platform-dependent. */ - 0xC02 => { minstret = value; minstret_written = true; Some(minstret) }, - - _ => None() + /* supervisor mode */ + (0x100, _) => { mstatus = legalize_sstatus(mstatus, value); Some(mstatus.bits()) }, + (0x102, _) => { sedeleg = legalize_sedeleg(sedeleg, value); Some(sedeleg.bits()) }, + (0x103, _) => { sideleg->bits() = value; Some(sideleg.bits()) }, /* TODO: does this need legalization? */ + (0x104, _) => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits()) }, + (0x105, _) => { stvec = legalize_tvec(stvec, value); Some(stvec.bits()) }, + (0x106, _) => { scounteren = legalize_scounteren(scounteren, value); Some(EXTZ(scounteren.bits())) }, + (0x140, _) => { sscratch = value; Some(sscratch) }, + (0x141, _) => { sepc = legalize_xepc(value); Some(sepc) }, + (0x142, _) => { scause->bits() = value; Some(scause.bits()) }, + (0x143, _) => { stval = value; Some(stval) }, + (0x144, _) => { mip = legalize_sip(mip, mideleg, value); Some(mip.bits()) }, + (0x180, _) => { satp = legalize_satp(cur_Architecture(), satp, value); Some(satp) }, + + _ => None() }; match res { Some(v) => print_reg("CSR " ^ csr ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")"), None() => { /* check extensions */ - if write_UExt_CSR(csr, value) + if write_UExt_CSR(csr, value) then () else print_bits("unhandled write to CSR ", csr) } @@ -162,6 +172,3 @@ mapping clause assembly = CSR(csr, rs1, rd, true, op) <-> csr_mnemonic(op) ^ "i" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_5(rs1) ^ sep() ^ csr_name_map(csr) mapping clause assembly = CSR(csr, rs1, rd, false, op) <-> csr_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ csr_name_map(csr) - - - diff --git a/model/riscv_jalr_rmem.sail b/model/riscv_jalr_rmem.sail index daf4bb0..cd8174e 100644 --- a/model/riscv_jalr_rmem.sail +++ b/model/riscv_jalr_rmem.sail @@ -5,6 +5,6 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = { /* write rd before anything else to prevent unintended strength */ X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */ let newPC : xlenbits = X(rs1) + EXTS(imm); - nextPC = newPC[63..1] @ 0b0; + nextPC = newPC[(sizeof(xlen) - 1) .. 1] @ 0b0; true } diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail index fcf9526..25b9dbb 100644 --- a/model/riscv_jalr_seq.sail +++ b/model/riscv_jalr_seq.sail @@ -7,7 +7,7 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = { some manner, but for now, we just keep a reordered definition to improve simulator performance. */ - let newPC : xlenbits = (X(rs1) + EXTS(imm))[63..1] @ 0b0; + let newPC : xlenbits = (X(rs1) + EXTS(imm))[(sizeof(xlen) - 1) .. 1] @ 0b0; if newPC[1] & (~ (haveRVC())) then { handle_mem_exception(newPC, E_Fetch_Addr_Align); false; diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 9ffb713..7e31659 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -45,7 +45,7 @@ function rvfi_read (addr, width, result) = { MemValue(v) => if width <= 8 then { - rvfi_exec->rvfi_mem_wdata() = zero_extend(v,64); + rvfi_exec->rvfi_mem_wdata() = sail_zero_extend(v,64); rvfi_exec->rvfi_mem_wmask() = to_bits(8,width) } else (), MemException(_) => () @@ -67,7 +67,11 @@ function mem_read (addr, width, aq, rl, res) = { let result : MemoryOpResult(bits(8 * 'n)) = if (aq | res) & (~ (is_aligned_addr(addr, width))) then MemException(E_Load_Addr_Align) - else checked_mem_read(Data, addr, width, aq, rl, res); + else match (aq, rl, res) { + (false, true, false) => throw(Error_not_implemented("load.rl")), + (false, true, true) => throw(Error_not_implemented("lr.rl")), + (_, _, _) => checked_mem_read(Data, addr, width, aq, rl, res) + }; rvfi_read(addr, width, result); result } @@ -120,7 +124,7 @@ val rvfi_write : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> unit e function rvfi_write (addr, width, value) = { rvfi_exec->rvfi_mem_addr() = addr; if width <= 8 then { - rvfi_exec->rvfi_mem_wdata() = zero_extend(value,64); + rvfi_exec->rvfi_mem_wdata() = sail_zero_extend(value,64); rvfi_exec->rvfi_mem_wmask() = to_bits(8,width); } } @@ -136,5 +140,9 @@ function mem_write_value (addr, width, value, aq, rl, con) = { rvfi_write(addr, width, value); if (rl | con) & (~ (is_aligned_addr(addr, width))) then MemException(E_SAMO_Addr_Align) - else checked_mem_write(addr, width, value, aq, rl, con) + else match (aq, rl, con) { + (true, false, false) => throw(Error_not_implemented("store.aq")), + (true, false, true) => throw(Error_not_implemented("sc.aq")), + (_, _, _) => checked_mem_write(addr, width, value, aq, rl, con) + } } diff --git a/model/riscv_next_regs.sail b/model/riscv_next_regs.sail index a8cc38c..5a3fb58 100644 --- a/model/riscv_next_regs.sail +++ b/model/riscv_next_regs.sail @@ -1,7 +1,7 @@ /* Architectural state for the 'N' user-level interrupts standard extension. */ /* ustatus reveals a subset of mstatus */ -bitfield Ustatus : bits(64) = { +bitfield Ustatus : xlenbits = { UPIE : 4, UIE : 0 } @@ -28,7 +28,7 @@ function legalize_ustatus(m : Mstatus, v : xlenbits) -> Mstatus = { m } -bitfield Uinterrupts : bits(64) = { +bitfield Uinterrupts : xlenbits = { UEI : 8, /* external interrupt */ UTI : 4, /* timer interrupt */ USI : 0 /* software interrupt */ diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 0ac77da..437c41d 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -64,17 +64,26 @@ function phys_mem_segments() = /* Physical memory map predicates */ function within_phys_mem forall 'n. (addr : xlenbits, width : atom('n)) -> bool = { - let ram_base = plat_ram_base (); - let rom_base = plat_rom_base (); - let ram_size = plat_ram_size (); - let rom_size = plat_rom_size (); + /* To avoid overflow issues when physical memory extends to the end + * of the addressable range, we need to perform address bound checks + * with a wider bitwidth. + * + * But since this is a hot function, we use only 64-bit width even for + * 64-bit mode to reduce impact on emulator performance. + */ + + let ext_addr : bits(64) = EXTZ(addr); + let ram_base : bits(64) = EXTZ(plat_ram_base ()); + let rom_base : bits(64) = EXTZ(plat_rom_base ()); + let ram_size : bits(64) = EXTZ(plat_ram_size ()); + let rom_size : bits(64) = EXTZ(plat_rom_size ()); /* todo: iterate over segment list */ - if ( ram_base <=_u addr - & (addr + sizeof('n)) <=_u (ram_base + ram_size)) + if ( ram_base <=_u ext_addr + & (ext_addr + sizeof('n)) <=_u (ram_base + ram_size)) then true - else if ( rom_base <=_u addr - & (addr + sizeof('n)) <=_u (rom_base + rom_size)) + else if ( rom_base <=_u ext_addr + & (ext_addr + sizeof('n)) <=_u (rom_base + rom_size)) then true else { print_platform("within_phys_mem: " ^ BitStr(addr) ^ " not within phys-mem:"); @@ -91,17 +100,17 @@ function within_clint forall 'n. (addr : xlenbits, width : atom('n)) -> bool = & (addr + sizeof('n)) <=_u (plat_clint_base() + plat_clint_size()) function within_htif_writable forall 'n. (addr : xlenbits, width : atom('n)) -> bool = - plat_htif_tohost() == addr + plat_htif_tohost() == addr | (plat_htif_tohost() + 4 == addr & width == 4) function within_htif_readable forall 'n. (addr : xlenbits, width : atom('n)) -> bool = - plat_htif_tohost() == addr + plat_htif_tohost() == addr | (plat_htif_tohost() + 4 == addr & width == 4) /* CLINT (Core Local Interruptor), based on Spike. */ val plat_insns_per_tick = {ocaml: "Platform.insns_per_tick", interpreter: "Platform.insns_per_tick", c: "plat_insns_per_tick", lem: "plat_insns_per_tick"} : unit -> int // assumes a single hart, since this typically is a vector of per-hart registers. -register mtimecmp : xlenbits // memory-mapped internal clint register. +register mtimecmp : bits(64) // memory-mapped internal clint register. /* CLINT memory-mapped IO */ @@ -117,9 +126,11 @@ register mtimecmp : xlenbits // memory-mapped internal clint register. * bffc mtime hi */ -let MSIP_BASE : xlenbits = 0x0000000000000000 -let MTIMECMP_BASE : xlenbits = 0x0000000000004000 -let MTIME_BASE : xlenbits = 0x000000000000bff8 +let MSIP_BASE : xlenbits = EXTZ(0x00000) +let MTIMECMP_BASE : xlenbits = EXTZ(0x04000) +let MTIMECMP_BASE_HI : xlenbits = EXTZ(0x04004) +let MTIME_BASE : xlenbits = EXTZ(0x0bff8) +let MTIME_BASE_HI : xlenbits = EXTZ(0x0bffc) val clint_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} function clint_load(addr, width) = { @@ -128,17 +139,40 @@ function clint_load(addr, width) = { if addr == MSIP_BASE & ('n == 8 | 'n == 4) then { print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mip.MSI())); - MemValue(zero_extend(mip.MSI(), sizeof(8 * 'n))) + MemValue(sail_zero_extend(mip.MSI(), sizeof(8 * 'n))) + } + else if addr == MTIMECMP_BASE & ('n == 4) + then { + print_platform("clint<4>[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtimecmp[31..0])); + /* FIXME: Redundant zero_extend currently required by Lem backend */ + MemValue(sail_zero_extend(mtimecmp[31..0], 32)) } else if addr == MTIMECMP_BASE & ('n == 8) then { - print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtimecmp)); - MemValue(zero_extend(mtimecmp, 64)) /* FIXME: Redundant zero_extend currently required by Lem backend */ + print_platform("clint<8>[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtimecmp)); + /* FIXME: Redundant zero_extend currently required by Lem backend */ + MemValue(sail_zero_extend(mtimecmp, 64)) + } + else if addr == MTIMECMP_BASE_HI & ('n == 4) + then { + print_platform("clint-hi<4>[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtimecmp[63..32])); + /* FIXME: Redundant zero_extend currently required by Lem backend */ + MemValue(sail_zero_extend(mtimecmp[63..32], 32)) + } + else if addr == MTIME_BASE & ('n == 4) + then { + print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtime)); + MemValue(sail_zero_extend(mtime[31..0], 32)) } else if addr == MTIME_BASE & ('n == 8) then { print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtime)); - MemValue(zero_extend(mtime, 64)) + MemValue(sail_zero_extend(mtime, 64)) + } + else if addr == MTIME_BASE_HI & ('n == 4) + then { + print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtime)); + MemValue(sail_zero_extend(mtime[63..32], 32)) } else { print_platform("clint[" ^ BitStr(addr) ^ "] -> <not-mapped>"); @@ -165,8 +199,18 @@ function clint_store(addr, width, data) = { clint_dispatch(); MemValue(true) } else if addr == MTIMECMP_BASE & 'n == 8 then { - print_platform("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mtimecmp)"); - mtimecmp = zero_extend(data, 64); /* FIXME: Redundant zero_extend currently required by Lem backend */ + print_platform("clint<8>[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mtimecmp)"); + mtimecmp = sail_zero_extend(data, 64); /* FIXME: Redundant zero_extend currently required by Lem backend */ + clint_dispatch(); + MemValue(true) + } else if addr == MTIMECMP_BASE & 'n == 4 then { + print_platform("clint<4>[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mtimecmp)"); + mtimecmp = vector_update_subrange(mtimecmp, 31, 0, sail_zero_extend(data, 32)); /* FIXME: Redundant zero_extend currently required by Lem backend */ + clint_dispatch(); + MemValue(true) + } else if addr == MTIMECMP_BASE_HI & 'n == 4 then { + print_platform("clint<4>[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mtimecmp)"); + mtimecmp = vector_update_subrange(mtimecmp, 63, 32, sail_zero_extend(data, 32)); /* FIXME: Redundant zero_extend currently required by Lem backend */ clint_dispatch(); MemValue(true) } else { @@ -195,9 +239,9 @@ bitfield htif_cmd : bits(64) = { payload : 47 .. 0 } -register htif_tohost : xlenbits +register htif_tohost : bits(64) register htif_done : bool -register htif_exit_code : xlenbits +register htif_exit_code : bits(64) /* Since the htif tohost port is only available at a single address, @@ -209,27 +253,37 @@ val htif_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 function htif_load(addr, width) = { print_platform("htif[" ^ BitStr(addr) ^ "] -> " ^ BitStr(htif_tohost)); /* FIXME: For now, only allow the expected access widths. */ - if width == 8 - then MemValue(zero_extend(htif_tohost, 64)) /* FIXME: Redundant zero_extend currently required by Lem backend */ - else MemException(E_Load_Access_Fault) + if width == 8 & (addr == plat_htif_tohost()) + then MemValue(sail_zero_extend(htif_tohost, 64)) /* FIXME: Redundant zero_extend currently required by Lem backend */ + else if width == 4 & addr == plat_htif_tohost() + then MemValue(sail_zero_extend(htif_tohost[31..0], 32)) /* FIXME: Redundant zero_extend currently required by Lem backend */ + else if width == 4 & addr == plat_htif_tohost() + 4 + then MemValue(sail_zero_extend(htif_tohost[63..32], 32)) /* FIXME: Redundant zero_extend currently required by Lem backend */ + else MemException(E_Load_Access_Fault) } -/* The wreg effect is an artifact of using 'register' to implement device state. */ -val htif_store: forall 'n, 0 < 'n <= 8. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wreg} +/* The rreg,wreg effects are an artifact of using 'register' to implement device state. */ +val htif_store: forall 'n, 0 < 'n <= 8. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {rreg,wreg} function htif_store(addr, width, data) = { print_platform("htif[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data)); /* Store the written value so that we can ack it later. */ - let cbits : xlenbits = EXTZ(data); - htif_tohost = cbits; + if width == 8 + then { htif_tohost = EXTZ(data) } + else if width == 4 & addr == plat_htif_tohost() + then { htif_tohost = vector_update_subrange(htif_tohost, 31, 0, data) } + else if width == 4 & addr == plat_htif_tohost() + 4 + then { htif_tohost = vector_update_subrange(htif_tohost, 63, 32, data) } + else { htif_tohost = EXTZ(data) }; + /* Process the cmd immediately; this is needed for terminal output. */ - let cmd = Mk_htif_cmd(cbits); + let cmd = Mk_htif_cmd(htif_tohost); match cmd.device() { 0x00 => { /* syscall-proxy */ print_platform("htif-syscall-proxy cmd: " ^ BitStr(cmd.payload())); if cmd.payload()[0] == 0b1 then { htif_done = true; - htif_exit_code = (zero_extend(cmd.payload(), xlen) >> 0b01) : xlenbits + htif_exit_code = (sail_zero_extend(cmd.payload(), 64) >> 0b01) } else () }, diff --git a/model/riscv_step.sail b/model/riscv_step.sail index 78369a8..ca2ca76 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -128,3 +128,10 @@ function loop () = { } } } + +/* initialize model state */ +function init_model () -> unit = { + init_platform (); /* devices */ + init_sys (); /* processor */ + init_vmem () /* virtual memory */ +} diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index df84733..2f02839 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -29,8 +29,17 @@ function is_CSR_defined (csr : bits(12), p : Privilege) -> bool = 0x344 => p == Machine, // mip 0x3A0 => p == Machine, // pmpcfg0 - 0x3B0 => false, // (Disabled for Spike compatibility) -// 0x3B0 => p == Machine, // pmpaddr0 + 0x3B0 => p == Machine, // pmpaddr0 + + /* counters */ + 0xB00 => p == Machine, // mcycle + 0xB02 => p == Machine, // minstret + + 0xB80 => p == Machine & (sizeof(xlen) == 32), // mcycleh + 0xB82 => p == Machine & (sizeof(xlen) == 32), // minstreth + + /* disabled trigger/debug module */ + 0x7a0 => p == Machine, /* supervisor mode: trap setup */ 0x100 => haveSupMode() & (p == Machine | p == Supervisor), // sstatus @@ -50,8 +59,14 @@ function is_CSR_defined (csr : bits(12), p : Privilege) -> bool = /* supervisor mode: address translation */ 0x180 => haveSupMode() & (p == Machine | p == Supervisor), // satp - /* disabled trigger/debug module */ - 0x7a0 => p == Machine, + /* user mode: counters */ + 0xC00 => p == User, // cycle + 0xC01 => p == User, // time + 0xC02 => p == User, // instret + + 0xC80 => p == User & (sizeof(xlen) == 32), // cycleh + 0xC81 => p == User & (sizeof(xlen) == 32), // timeh + 0xC82 => p == User & (sizeof(xlen) == 32), // instreth /* check extensions */ _ => is_UExt_CSR_defined(csr, p) // 'N' extension @@ -71,9 +86,9 @@ function check_Counteren(csr : csreg, p : Privilege) -> bool = (0xC01, Supervisor) => mcounteren.TM() == true, (0xC02, Supervisor) => mcounteren.IR() == true, - (0xC00, User) => scounteren.CY() == true, - (0xC01, User) => scounteren.TM() == true, - (0xC02, User) => scounteren.IR() == true, + (0xC00, User) => mcounteren.CY() == true & ((~ (haveSupMode())) | scounteren.CY() == true), + (0xC01, User) => mcounteren.TM() == true & ((~ (haveSupMode())) | scounteren.TM() == true), + (0xC02, User) => mcounteren.IR() == true & ((~ (haveSupMode())) | scounteren.IR() == true), (_, _) => /* no HPM counters for now */ if 0xC03 <=_u csr & csr <=_u 0xC1F @@ -405,7 +420,7 @@ function init_sys() -> unit = { mhartid = EXTZ(0b0); - misa->MXL() = arch_to_bits(RV64); + misa->MXL() = arch_to_bits(if sizeof(xlen) == 32 then RV32 else RV64); misa->A() = true; /* atomics */ misa->C() = true; /* RVC */ misa->I() = true; /* base integer ISA */ @@ -413,9 +428,8 @@ function init_sys() -> unit = { misa->U() = true; /* user-mode */ misa->S() = true; /* supervisor-mode */ - /* 64-bit only mode with no extensions */ - mstatus->SXL() = misa.MXL(); - mstatus->UXL() = misa.MXL(); + mstatus = set_mstatus_SXL(mstatus, misa.MXL()); + mstatus = set_mstatus_UXL(mstatus, misa.MXL()); mstatus->SD() = false; mip->bits() = EXTZ(0b0); diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index e39331f..439d12d 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -38,8 +38,8 @@ register cur_inst : xlenbits /* M-mode registers */ -bitfield Misa : bits(64) = { - MXL : 63 .. 62, +bitfield Misa : xlenbits = { + MXL : xlen - 1 .. xlen - 2, Z : 25, Y : 24, @@ -88,11 +88,13 @@ function haveSupMode() -> bool = misa.S() == true function haveUsrMode() -> bool = misa.U() == true function haveNExt() -> bool = misa.N() == true -bitfield Mstatus : bits(64) = { - SD : 63, +bitfield Mstatus : xlenbits = { + SD : xlen - 1, - SXL : 35 .. 34, - UXL : 33 .. 32, + // The SXL and UXL fields don't exist on RV32, so they are modelled + // via explicit getters and setters; see below. + // SXL : 35 .. 34, + // UXL : 33 .. 32, TSR : 22, TW : 21, @@ -117,6 +119,36 @@ bitfield Mstatus : bits(64) = { } register mstatus : Mstatus +function get_mstatus_SXL(m : Mstatus) -> arch_xlen = { + if sizeof(xlen) == 32 + then arch_to_bits(RV32) + else m.bits()[35 .. 34] +} + +function set_mstatus_SXL(m : Mstatus, a : arch_xlen) -> Mstatus = { + if sizeof(xlen) == 32 + then m + else { + let m = vector_update_subrange(m.bits(), 35, 34, a); + Mk_Mstatus(m) + } +} + +function get_mstatus_UXL(m : Mstatus) -> arch_xlen = { + if sizeof(xlen) == 32 + then arch_to_bits(RV32) + else m.bits()[33 .. 32] +} + +function set_mstatus_UXL(m : Mstatus, a : arch_xlen) -> Mstatus = { + if sizeof(xlen) == 32 + then m + else { + let m = vector_update_subrange(m.bits(), 33, 32, a); + Mk_Mstatus(m) + } +} + function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { let m : Mstatus = Mk_Mstatus(v); @@ -131,9 +163,9 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { let m = update_SD(m, extStatus_of_bits(m.FS()) == Dirty | extStatus_of_bits(m.XS()) == Dirty); - /* For now, we don't allow SXL and UXL to be changed, for Spike compatibility. */ - let m = update_SXL(m, o.SXL()); - let m = update_UXL(m, o.UXL()); + /* We don't support dynamic changes to SXL and UXL. */ + let m = set_mstatus_SXL(m, get_mstatus_SXL(o)); + let m = set_mstatus_UXL(m, get_mstatus_UXL(o)); /* Hardwired to zero in the absence of 'N'. */ let m = update_UPIE(m, false); @@ -147,8 +179,8 @@ function cur_Architecture() -> Architecture = { let a : arch_xlen = match (cur_privilege) { Machine => misa.MXL(), - Supervisor => mstatus.SXL(), - User => mstatus.UXL() + Supervisor => get_mstatus_SXL(mstatus), + User => get_mstatus_UXL(mstatus) }; match architecture(a) { Some(a) => a, @@ -162,7 +194,7 @@ function in32BitMode() -> bool = { /* interrupt processing state */ -bitfield Minterrupts : bits(64) = { +bitfield Minterrupts : xlenbits = { MEI : 11, /* external interrupts */ SEI : 9, UEI : 8, @@ -223,7 +255,7 @@ function legalize_mideleg(o : Minterrupts, v : xlenbits) -> Minterrupts = { /* exception processing state */ -bitfield Medeleg : bits(64) = { +bitfield Medeleg : xlenbits = { SAMO_Page_Fault : 15, Load_Page_Fault : 13, Fetch_Page_Fault : 12, @@ -250,9 +282,9 @@ function legalize_medeleg(o : Medeleg, v : xlenbits) -> Medeleg = { /* registers for trap handling */ -bitfield Mtvec : bits(64) = { - Base : 63 .. 2, - Mode : 1 .. 0 +bitfield Mtvec : xlenbits = { + Base : xlen - 1 .. 2, + Mode : 1 .. 0 } register mtvec : Mtvec /* Trap Vector */ @@ -265,9 +297,9 @@ function legalize_tvec(o : Mtvec, v : xlenbits) -> Mtvec = { } } -bitfield Mcause : bits(64) = { - IsInterrupt : 63, - Cause : 62 .. 0 +bitfield Mcause : xlenbits = { + IsInterrupt : xlen - 1, + Cause : xlen - 2 .. 0 } register mcause : Mcause @@ -329,8 +361,8 @@ function legalize_scounteren(c : Counteren, v : xlenbits) -> Counteren = { c } -register mcycle : xlenbits -register mtime : xlenbits +register mcycle : bits(64) +register mtime : bits(64) /* minstret * @@ -343,7 +375,7 @@ register mtime : xlenbits * written to, we track writes to it in a separate model-internal * register. */ -register minstret : xlenbits +register minstret : bits(64) register minstret_written : bool function retire_instruction() -> unit = { @@ -353,7 +385,7 @@ function retire_instruction() -> unit = { } /* informational registers */ -register mvendorid : xlenbits +register mvendorid : bits(32) register mimpid : xlenbits register marchid : xlenbits /* TODO: this should be readonly, and always 0 for now */ @@ -367,9 +399,11 @@ register pmpcfg0 : xlenbits /* S-mode registers */ /* sstatus reveals a subset of mstatus */ -bitfield Sstatus : bits(64) = { - SD : 63, - UXL : 33 .. 32, +bitfield Sstatus : xlenbits = { + SD : xlen - 1, + // The UXL field does not exist on RV32, so we define an explicit + // getter and setter below. + // UXL : 30 .. 29, MXR : 19, SUM : 18, XS : 16 .. 15, @@ -380,12 +414,23 @@ bitfield Sstatus : bits(64) = { SIE : 1, UIE : 0 } +/* sstatus is a view of mstatus, so there is no register defined. */ + +function get_sstatus_UXL(s : Sstatus) -> arch_xlen = { + let m = Mk_Mstatus(s.bits()); + get_mstatus_UXL(m) +} + +function set_sstatus_UXL(s : Sstatus, a : arch_xlen) -> Sstatus = { + let m = Mk_Mstatus(s.bits()); + let m = set_mstatus_UXL(m, a); + Mk_Sstatus(m.bits()) +} -/* This is a view, so there is no register defined. */ function lower_mstatus(m : Mstatus) -> Sstatus = { let s = Mk_Sstatus(EXTZ(0b0)); let s = update_SD(s, m.SD()); - let s = update_UXL(s, m.UXL()); + let s = set_sstatus_UXL(s, get_mstatus_UXL(m)); let s = update_MXR(s, m.MXR()); let s = update_SUM(s, m.SUM()); let s = update_XS(s, m.XS()); @@ -420,7 +465,7 @@ function legalize_sstatus(m : Mstatus, v : xlenbits) -> Mstatus = { lift_sstatus(m, Mk_Sstatus(v)) } -bitfield Sedeleg : bits(64) = { +bitfield Sedeleg : xlenbits = { UEnvCall : 8, SAMO_Access_Fault : 7, SAMO_Addr_Align : 6, @@ -437,7 +482,7 @@ function legalize_sedeleg(s : Sedeleg, v : xlenbits) -> Sedeleg = { Mk_Sedeleg(EXTZ(v[8..0])) } -bitfield Sinterrupts : bits(64) = { +bitfield Sinterrupts : xlenbits = { SEI : 9, /* external interrupts */ UEI : 8, @@ -508,30 +553,43 @@ function legalize_sie(m : Minterrupts, d : Minterrupts, v : xlenbits) -> Minterr register sideleg : Sinterrupts -/* s-mode address translation and protection (satp) */ +/* other non-VM related supervisor state */ +register stvec : Mtvec +register sscratch : xlenbits +register sepc : xlenbits +register scause : Mcause +register stval : xlenbits + +/* + * S-mode address translation and protection (satp) layout. + * The actual satp register is defined in an architecture-specific file. + */ + bitfield Satp64 : bits(64) = { Mode : 63 .. 60, Asid : 59 .. 44, PPN : 43 .. 0 } -register satp : xlenbits -function legalize_satp(a : Architecture, o : xlenbits, v : xlenbits) -> xlenbits = { +function legalize_satp64(a : Architecture, o : bits(64), v : bits(64)) -> bits(64) = { let s = Mk_Satp64(v); - match satpMode_of_bits(a, s.Mode()) { + match satp64Mode_of_bits(a, s.Mode()) { None() => o, Some(Sv32) => o, /* Sv32 is unsupported for now */ Some(_) => s.bits() } } -/* other supervisor state */ -register stvec : Mtvec -register sscratch : xlenbits -register sepc : xlenbits -register scause : Mcause -register stval : xlenbits +bitfield Satp32 : bits(32) = { + Mode : 31, + Asid : 30 .. 22, + PPN : 21 .. 0 +} + +function legalize_satp32(a : Architecture, o : bits(32), v : bits(32)) -> bits(32) = { + /* all 32-bit satp modes are valid */ + v +} /* disabled trigger/debug module */ register tselect : xlenbits - diff --git a/model/riscv_termination.sail b/model/riscv_termination_common.sail index 6da4896..e38cd19 100644 --- a/model/riscv_termination.sail +++ b/model/riscv_termination_common.sail @@ -1,5 +1,4 @@ termination_measure n_leading_spaces s = string_length(s) -termination_measure walk39(_,_,_,_,_,_,level,_) = level val compressed_measure : ast -> int function compressed_measure(instr) = match instr { diff --git a/model/riscv_termination_rv32.sail b/model/riscv_termination_rv32.sail new file mode 100644 index 0000000..7cf8cb8 --- /dev/null +++ b/model/riscv_termination_rv32.sail @@ -0,0 +1 @@ +termination_measure walk32(_,_,_,_,_,_,level,_) = level diff --git a/model/riscv_termination_rv64.sail b/model/riscv_termination_rv64.sail new file mode 100644 index 0000000..18005b8 --- /dev/null +++ b/model/riscv_termination_rv64.sail @@ -0,0 +1,2 @@ +termination_measure walk39(_,_,_,_,_,_,level,_) = level +termination_measure walk48(_,_,_,_,_,_,level,_) = level diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 4d012e0..634cd83 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -1,11 +1,13 @@ /* Basic type and function definitions used pervasively in the model. */ -let xlen = 64 -type xlenbits = bits(64) +/* this value is only defined for the runtime platform for ELF loading + * checks, and not used in the model. + */ +let xlen_val = sizeof(xlen) -let xlen_max_unsigned = 2 ^ xlen - 1 -let xlen_max_signed = 2 ^ (xlen - 1) - 1 -let xlen_min_signed = 0 - 2 ^ (xlen - 1) +let xlen_max_unsigned = 2 ^ sizeof(xlen) - 1 +let xlen_max_signed = 2 ^ (sizeof(xlen) - 1) - 1 +let xlen_min_signed = 0 - 2 ^ (sizeof(xlen) - 1) type half = bits(16) type word = bits(32) @@ -80,7 +82,7 @@ val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg} /*function rX 0 = 0x0000000000000000 and rX (r if r > 0) = Xs[r]*/ function rX r = match r { - 0 => 0x0000000000000000, + 0 => EXTZ(0x0), 1 => x1, 2 => x2, 3 => x3, @@ -438,13 +440,14 @@ function extStatus_of_bits(e) = /* supervisor-level address translation modes */ type satp_mode = bits(4) -enum SATPMode = {Sbare, Sv32, Sv39} +enum SATPMode = {Sbare, Sv32, Sv39, Sv48} -function satpMode_of_bits(a : Architecture, m : satp_mode) -> option(SATPMode) = +function satp64Mode_of_bits(a : Architecture, m : satp_mode) -> option(SATPMode) = match (a, m) { (_, 0x0) => Some(Sbare), (RV32, 0x1) => Some(Sv32), (RV64, 0x8) => Some(Sv39), + (RV64, 0x9) => Some(Sv48), (_, _) => None() } diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail deleted file mode 100644 index ef56108..0000000 --- a/model/riscv_vmem.sail +++ /dev/null @@ -1,406 +0,0 @@ -/* Supervisor-mode address translation and page-table walks. */ - -/* PageSize */ - -let PAGESIZE_BITS = 12 - -/* PTE attributes, permission checks and updates */ - -type pteAttribs = bits(8) - -bitfield PTE_Bits : pteAttribs = { - D : 7, - A : 6, - G : 5, - U : 4, - X : 3, - W : 2, - R : 1, - V : 0 -} - -function isPTEPtr(p : pteAttribs) -> bool = { - let a = Mk_PTE_Bits(p); - a.R() == false & a.W() == false & a.X() == false -} - -function isInvalidPTE(p : pteAttribs) -> bool = { - let a = Mk_PTE_Bits(p); - a.V() == false | (a.W() == true & a.R() == false) -} - -function checkPTEPermission(ac : AccessType, priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits) -> bool = { - match (ac, priv) { - (Read, User) => p.U() == true & (p.R() == true | (p.X() == true & mxr)), - (Write, User) => p.U() == true & p.W() == true, - (ReadWrite, User) => p.U() == true & p.W() == true & (p.R() == true | (p.X() == true & mxr)), - (Execute, User) => p.U() == true & p.X() == true, - - (Read, Supervisor) => (p.U() == false | do_sum) & (p.R() == true | (p.X() == true & mxr)), - (Write, Supervisor) => (p.U() == false | do_sum) & p.W() == true, - (ReadWrite, Supervisor) => (p.U() == false | do_sum) & p.W() == true & (p.R() == true | (p.X() == true & mxr)), - (Execute, Supervisor) => p.U() == false & p.X() == true, - - (_, Machine) => internal_error("m-mode mem perm check") - } -} - -function update_PTE_Bits(p : PTE_Bits, a : AccessType) -> option(PTE_Bits) = { - let update_d = (a == Write | a == ReadWrite) & p.D() == false; // dirty-bit - let update_a = p.A() == false; // accessed-bit - if update_d | update_a then { - let np = update_A(p, true); - let np = if update_d then update_D(np, true) else np; - Some(np) - } else None() -} - -/* failure modes for address-translation/page-table-walks */ -enum PTW_Error = { - PTW_Access, /* physical memory access error for a PTE */ - PTW_Invalid_PTE, - PTW_No_Permission, - PTW_Misaligned, /* misaligned superpage */ - PTW_PTE_Update /* PTE update needed but not enabled */ -} -val cast ptw_error_to_str : PTW_Error -> string -function ptw_error_to_str(e) = - match (e) { - PTW_Access => "mem-access-error", - PTW_Invalid_PTE => "invalid-pte", - PTW_No_Permission => "no-permission", - PTW_Misaligned => "misaligned-superpage", - PTW_PTE_Update => "pte-update-needed" - } - -/* conversion of these translation/PTW failures into architectural exceptions */ -function translationException(a : AccessType, f : PTW_Error) -> ExceptionType = { - let e : ExceptionType = - match (a, f) { - (ReadWrite, PTW_Access) => E_SAMO_Access_Fault, - (ReadWrite, _) => E_SAMO_Page_Fault, - (Read, PTW_Access) => E_Load_Access_Fault, - (Read, _) => E_Load_Page_Fault, - (Write, PTW_Access) => E_SAMO_Access_Fault, - (Write, _) => E_SAMO_Page_Fault, - (Fetch, PTW_Access) => E_Fetch_Access_Fault, - (Fetch, _) => E_Fetch_Page_Fault - } in { -/* print("translationException(" ^ a ^ ", " ^ f ^ ") -> " ^ e); */ - e - } -} -/* address translation: Sv39 */ - -let SV39_LEVEL_BITS = 9 -let SV39_LEVELS = 3 -let PTE39_LOG_SIZE = 3 -let PTE39_SIZE = 8 - -type vaddr39 = bits(39) -type paddr39 = bits(56) -type pte39 = xlenbits - -bitfield SV39_Vaddr : vaddr39 = { - VPNi : 38 .. 12, - PgOfs : 11 .. 0 -} - -bitfield SV39_Paddr : paddr39 = { - PPNi : 55 .. 12, - PgOfs : 11 .. 0 -} - -bitfield SV39_PTE : pte39 = { - PPNi : 53 .. 10, - RSW : 9 .. 8, - BITS : 7 .. 0 -} - -/* ASID */ - -type asid64 = bits(16) - -function curAsid64() -> asid64 = { - let satp64 = Mk_Satp64(satp); - satp64.Asid() -} - -/* Current page table base from satp */ -function curPTB39() -> paddr39 = { - let satp64 = Mk_Satp64(satp); - EXTZ(shiftl(satp64.PPN(), PAGESIZE_BITS)) -} - -/* Page-table walk. */ - -union PTW_Result = { - PTW_Success: (paddr39, SV39_PTE, paddr39, nat, bool), - PTW_Failure: PTW_Error -} - -val walk39 : (vaddr39, AccessType, Privilege, bool, bool, paddr39, nat, bool) -> PTW_Result effect {rmem, escape} -function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) -> PTW_Result = { - let va = Mk_SV39_Vaddr(vaddr); - let pt_ofs : paddr39 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]), - PTE39_LOG_SIZE); - let pte_addr = ptb + pt_ofs; - /* FIXME: we assume here that walks only access physical-memory-backed addresses, and not MMIO regions. */ - match (phys_mem_read(Data, EXTZ(pte_addr), 8, false, false, false)) { - MemException(_) => { -/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) - ^ " pt_base=" ^ BitStr(ptb) - ^ " pt_ofs=" ^ BitStr(pt_ofs) - ^ " pte_addr=" ^ BitStr(pte_addr) - ^ ": invalid pte address"); */ - PTW_Failure(PTW_Access) - }, - MemValue(v) => { - let pte = Mk_SV39_PTE(v); - let pbits = pte.BITS(); - let pattr = Mk_PTE_Bits(pbits); - let is_global = global | (pattr.G() == true); -/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) - ^ " pt_base=" ^ BitStr(ptb) - ^ " pt_ofs=" ^ BitStr(pt_ofs) - ^ " pte_addr=" ^ BitStr(pte_addr) - ^ " pte=" ^ BitStr(v)); */ - if isInvalidPTE(pbits) then { -/* print("walk39: invalid pte"); */ - PTW_Failure(PTW_Invalid_PTE) - } else { - if isPTEPtr(pbits) then { - if level == 0 then { - /* last-level PTE contains a pointer instead of a leaf */ -/* print("walk39: last-level pte contains a ptr"); */ - PTW_Failure(PTW_Invalid_PTE) - } else { - /* walk down the pointer to the next level */ - walk39(vaddr, ac, priv, mxr, do_sum, EXTZ(shiftl(pte.PPNi(), PAGESIZE_BITS)), level - 1, is_global) - } - } else { /* leaf PTE */ - if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pattr)) then { -/* print("walk39: pte permission check failure"); */ - PTW_Failure(PTW_No_Permission) - } else { - if level > 0 then { /* superpage */ - /* fixme hack: to get a mask of appropriate size */ - let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ EXTZ(0b1), level * SV39_LEVEL_BITS) - 1; - if (pte.PPNi() & mask) != EXTZ(0b0) then { - /* misaligned superpage mapping */ -/* print("walk39: misaligned superpage mapping"); */ - PTW_Failure(PTW_Misaligned) - } else { - /* add the appropriate bits of the VPN to the superpage PPN */ - let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & mask); -/* let res = append(ppn, va.PgOfs()); - print("walk39: using superpage: pte.ppn=" ^ BitStr(pte.PPNi()) - ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global) - } - } else { - /* normal leaf PTE */ -/* let res = append(pte.PPNi(), va.PgOfs()); - print("walk39: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(pte.PPNi()) ^ " res=" ^ BitStr(res)); */ - PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global) - } - } - } - } - } - } -} - -/* idealized TLB to model fence.vm and also speed up simulation. */ - -struct TLB39_Entry = { - asid : asid64, - global : bool, - vAddr : vaddr39, /* VPN */ - pAddr : paddr39, /* PPN */ - vMatchMask : vaddr39, /* matching mask for superpages */ - vAddrMask : vaddr39, /* selection mask for superpages */ - pte : SV39_PTE, /* permissions */ - pteAddr : paddr39, /* for dirty writeback */ - age : xlenbits -} - -/* the rreg effect is an artifact of using the cycle counter to provide the age */ -val make_TLB39_Entry : (asid64, bool, vaddr39, paddr39, SV39_PTE, nat, paddr39) -> TLB39_Entry effect {rreg} - -function make_TLB39_Entry(asid, global, vAddr, pAddr, pte, level, pteAddr) = { - let shift : nat = PAGESIZE_BITS + (level * SV39_LEVEL_BITS); - /* fixme hack: use a better idiom for masks */ - let vAddrMask : vaddr39 = shiftl(vAddr ^ vAddr ^ EXTZ(0b1), shift) - 1; - let vMatchMask : vaddr39 = ~ (vAddrMask); - struct { - asid = asid, - global = global, - pte = pte, - pteAddr = pteAddr, - vAddrMask = vAddrMask, - vMatchMask = vMatchMask, - vAddr = vAddr & vMatchMask, - pAddr = shiftl(shiftr(pAddr, shift), shift), - age = mcycle - } -} - -/* TODO: make this a vector or array of entries */ -register tlb39 : option(TLB39_Entry) - -val lookupTLB39 : (asid64, vaddr39) -> option((int, TLB39_Entry)) effect {rreg} -function lookupTLB39(asid, vaddr) = { - match tlb39 { - None() => None(), - Some(e) => if (e.global | (e.asid == asid)) - & (e.vAddr == (e.vMatchMask & vaddr)) - then Some((0, e)) - else None() - } -} - -val addToTLB39 : (asid64, vaddr39, paddr39, SV39_PTE, paddr39, nat, bool) -> unit effect {wreg, rreg} -function addToTLB39(asid, vAddr, pAddr, pte, pteAddr, level, global) = { - let ent = make_TLB39_Entry(asid, global, vAddr, pAddr, pte, level, pteAddr); - tlb39 = Some(ent) -} - -function writeTLB39(idx : int, ent : TLB39_Entry) -> unit = - tlb39 = Some(ent) - -val flushTLB : (option(asid64), option(vaddr39)) -> unit effect {rreg, wreg} -function flushTLB(asid, addr) = { - let ent : option(TLB39_Entry) = - match (tlb39, asid, addr) { - (None(), _, _) => None(), - (Some(e), None(), None()) => None(), - (Some(e), None(), Some(a)) => if e.vAddr == (e.vMatchMask & a) - then None() else Some(e), - (Some(e), Some(i), None()) => if (e.asid == i) & (~ (e.global)) - then None() else Some(e), - (Some(e), Some(i), Some(a)) => if (e.asid == i) & (e.vAddr == (a & e.vMatchMask)) - & (~ (e.global)) - then None() else Some(e) - }; - tlb39 = ent -} - -union TR39_Result = { - TR39_Address : paddr39, - TR39_Failure : PTW_Error -} - -val translate39 : (vaddr39, AccessType, Privilege, bool, bool, nat) -> TR39_Result effect {rreg, wreg, wmv, escape, rmem} -function translate39(vAddr, ac, priv, mxr, do_sum, level) = { - let asid = curAsid64(); - match lookupTLB39(asid, vAddr) { - Some(idx, ent) => { - let pteBits = Mk_PTE_Bits(ent.pte.BITS()); - if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pteBits)) - then TR39_Failure(PTW_No_Permission) - else { - match update_PTE_Bits(pteBits, ac) { - None() => TR39_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)), - Some(pbits) => { - if ~ (plat_enable_dirty_update ()) - then { - /* pte needs dirty/accessed update but that is not enabled */ - TR39_Failure(PTW_PTE_Update) - } else { - /* update PTE entry and TLB */ - n_ent : TLB39_Entry = ent; - n_ent.pte = update_BITS(ent.pte, pbits.bits()); - writeTLB39(idx, n_ent); - /* update page table */ - match checked_mem_write(EXTZ(ent.pteAddr), 8, ent.pte.bits(), false, false, false) { - MemValue(_) => (), - MemException(e) => internal_error("invalid physical address in TLB") - }; - TR39_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)) - } - } - } - } - }, - None() => { - match walk39(vAddr, ac, priv, mxr, do_sum, curPTB39(), level, false) { - PTW_Failure(f) => TR39_Failure(f), - PTW_Success(pAddr, pte, pteAddr, level, global) => { - match update_PTE_Bits(Mk_PTE_Bits(pte.BITS()), ac) { - None() => { - addToTLB39(asid, vAddr, pAddr, pte, pteAddr, level, global); - TR39_Address(pAddr) - }, - Some(pbits) => - if ~ (plat_enable_dirty_update ()) - then { - /* pte needs dirty/accessed update but that is not enabled */ - TR39_Failure(PTW_PTE_Update) - } else { - w_pte : SV39_PTE = update_BITS(pte, pbits.bits()); - match checked_mem_write(EXTZ(pteAddr), 8, w_pte.bits(), false, false, false) { - MemValue(_) => { - addToTLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global); - TR39_Address(pAddr) - }, - MemException(e) => { - /* pte is not in valid memory */ - TR39_Failure(PTW_Access) - } - } - } - } - } - } - } - } -} - -/* Address translation mode */ - -val translationMode : (Privilege) -> SATPMode effect {rreg, escape} -function translationMode(priv) = { - if priv == Machine then Sbare - else { - let arch = architecture(mstatus.SXL()); - match arch { - Some(RV64) => { - let mbits : satp_mode = Mk_Satp64(satp).Mode(); - match satpMode_of_bits(RV64, mbits) { - Some(m) => m, - None() => internal_error("invalid RV64 translation mode in satp") - } - }, - _ => internal_error("unsupported address translation arch") - } - } -} - -union TR_Result = { - TR_Address : xlenbits, - TR_Failure : ExceptionType -} - -/* Top-level address translation dispatcher */ - -val translateAddr : (xlenbits, AccessType, ReadType) -> TR_Result effect {escape, rmem, rreg, wmv, wreg} -function translateAddr(vAddr, ac, rt) = { - let effPriv : Privilege = match rt { - Instruction => cur_privilege, - Data => if mstatus.MPRV() == true - then privLevel_of_bits(mstatus.MPP()) - else cur_privilege - }; - let mxr : bool = mstatus.MXR() == true; - let do_sum : bool = mstatus.SUM() == true; - let mode : SATPMode = translationMode(effPriv); - match mode { - Sbare => TR_Address(vAddr), - SV39 => match translate39(vAddr[38 .. 0], ac, effPriv, mxr, do_sum, SV39_LEVELS - 1) { - TR39_Address(pa) => TR_Address(EXTZ(pa)), - TR39_Failure(f) => TR_Failure(translationException(ac, f)) - }, - _ => internal_error("unsupported address translation scheme") - } -} diff --git a/model/riscv_vmem_common.sail b/model/riscv_vmem_common.sail new file mode 100644 index 0000000..c153579 --- /dev/null +++ b/model/riscv_vmem_common.sail @@ -0,0 +1,239 @@ +/* Shared definitions for supervisor-mode page-table-entries and permission checks. + * + * These definitions are independent of xlen and do not involve + * accessing physical memory. + */ + +/* PageSize */ + +let PAGESIZE_BITS = 12 + +/* PTE attributes, permission checks and updates */ + +type pteAttribs = bits(8) + +bitfield PTE_Bits : pteAttribs = { + D : 7, + A : 6, + G : 5, + U : 4, + X : 3, + W : 2, + R : 1, + V : 0 +} + +function isPTEPtr(p : pteAttribs) -> bool = { + let a = Mk_PTE_Bits(p); + a.R() == false & a.W() == false & a.X() == false +} + +function isInvalidPTE(p : pteAttribs) -> bool = { + let a = Mk_PTE_Bits(p); + a.V() == false | (a.W() == true & a.R() == false) +} + +function checkPTEPermission(ac : AccessType, priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits) -> bool = { + match (ac, priv) { + (Read, User) => p.U() == true & (p.R() == true | (p.X() == true & mxr)), + (Write, User) => p.U() == true & p.W() == true, + (ReadWrite, User) => p.U() == true & p.W() == true & (p.R() == true | (p.X() == true & mxr)), + (Execute, User) => p.U() == true & p.X() == true, + + (Read, Supervisor) => (p.U() == false | do_sum) & (p.R() == true | (p.X() == true & mxr)), + (Write, Supervisor) => (p.U() == false | do_sum) & p.W() == true, + (ReadWrite, Supervisor) => (p.U() == false | do_sum) & p.W() == true & (p.R() == true | (p.X() == true & mxr)), + (Execute, Supervisor) => p.U() == false & p.X() == true, + + (_, Machine) => internal_error("m-mode mem perm check") + } +} + +function update_PTE_Bits(p : PTE_Bits, a : AccessType) -> option(PTE_Bits) = { + let update_d = (a == Write | a == ReadWrite) & p.D() == false; // dirty-bit + let update_a = p.A() == false; // accessed-bit + if update_d | update_a then { + let np = update_A(p, true); + let np = if update_d then update_D(np, true) else np; + Some(np) + } else None() +} + +/* failure modes for address-translation/page-table-walks */ +enum PTW_Error = { + PTW_Access, /* physical memory access error for a PTE */ + PTW_Invalid_PTE, + PTW_No_Permission, + PTW_Misaligned, /* misaligned superpage */ + PTW_PTE_Update /* PTE update needed but not enabled */ +} +val cast ptw_error_to_str : PTW_Error -> string +function ptw_error_to_str(e) = + match (e) { + PTW_Access => "mem-access-error", + PTW_Invalid_PTE => "invalid-pte", + PTW_No_Permission => "no-permission", + PTW_Misaligned => "misaligned-superpage", + PTW_PTE_Update => "pte-update-needed" + } + +/* conversion of these translation/PTW failures into architectural exceptions */ +function translationException(a : AccessType, f : PTW_Error) -> ExceptionType = { + let e : ExceptionType = + match (a, f) { + (ReadWrite, PTW_Access) => E_SAMO_Access_Fault, + (ReadWrite, _) => E_SAMO_Page_Fault, + (Read, PTW_Access) => E_Load_Access_Fault, + (Read, _) => E_Load_Page_Fault, + (Write, PTW_Access) => E_SAMO_Access_Fault, + (Write, _) => E_SAMO_Page_Fault, + (Fetch, PTW_Access) => E_Fetch_Access_Fault, + (Fetch, _) => E_Fetch_Page_Fault + } in { +/* print("translationException(" ^ a ^ ", " ^ f ^ ") -> " ^ e); */ + e + } +} + +/* + * Definitions for RV32, which has a single address translation mode: Sv32. + */ + +type vaddr32 = bits(32) +type paddr32 = bits(34) +type pte32 = bits(32) + +/* asid */ +type asid32 = bits(9) + +function curAsid32(satp : bits(32)) -> asid32 = { + let s = Mk_Satp32(satp); + s.Asid() +} + +/* page table base from satp */ +function curPTB32(satp : bits(32)) -> paddr32 = { + let s : Satp32 = Mk_Satp32(satp); + shiftl(EXTZ(s.PPN()), PAGESIZE_BITS) +} + +/* Sv32 parameters and bitfield layouts */ + +let SV32_LEVEL_BITS = 10 +let SV32_LEVELS = 2 +let PTE32_LOG_SIZE = 2 +let PTE32_SIZE = 4 + +bitfield SV32_Vaddr : vaddr32 = { + VPNi : 31 .. 12, + PgOfs : 11 .. 0 +} + +bitfield SV32_Paddr : paddr32 = { + PPNi : 33 .. 12, + PgOfs : 11 .. 0 +} + +bitfield SV32_PTE : pte32 = { + PPNi : 31 .. 10, + RSW : 9 .. 8, + BITS : 7 .. 0 +} + +/* + * Definitions for RV64, which has two defined address translation modes: Sv39 and Sv48. + */ + +/* Sv48 and Sv64 are reserved but not defined. The size of the VPN + * increases by 9 bits through Sv39, Sv48 and Sv57, but not for Sv64. + * Also, the 45-bit size of the VPN for Sv57 exceeds the 44-bit size + * of the PPN in satp64. Due to these corner cases, it is unlikely + * that definitions can be shared across all four schemes, so separate + * definitions might eventually be needed for each translation mode. + * + * But to keep things simple for now, since Sv39 and Sv48 have the + * same PPN size, we share some definitions. + */ + +type paddr64 = bits(56) +type pte64 = bits(64) + +/* asid */ + +type asid64 = bits(16) + +function curAsid64(satp : bits(64)) -> asid64 = { + let s = Mk_Satp64(satp); + s.Asid() +} + +/* page table base from satp */ +function curPTB64(satp : bits(64)) -> paddr64 = { + let s = Mk_Satp64(satp); + shiftl(EXTZ(s.PPN()), PAGESIZE_BITS) +} + +/* Sv39 parameters and bitfield layouts */ + +let SV39_LEVEL_BITS = 9 +let SV39_LEVELS = 3 +let PTE39_LOG_SIZE = 3 +let PTE39_SIZE = 8 + +type vaddr39 = bits(39) + +bitfield SV39_Vaddr : vaddr39 = { + VPNi : 38 .. 12, + PgOfs : 11 .. 0 +} + +bitfield SV39_Paddr : paddr64 = { + PPNi : 55 .. 12, + PgOfs : 11 .. 0 +} + +bitfield SV39_PTE : pte64 = { + PPNi : 53 .. 10, + RSW : 9 .. 8, + BITS : 7 .. 0 +} + +/* Sv48 parameters and bitfield layouts */ + +let SV48_LEVEL_BITS = 9 +let SV48_LEVELS = 4 +let PTE48_LOG_SIZE = 3 +let PTE48_SIZE = 8 + +type vaddr48 = bits(48) +type pte48 = bits(64) + +bitfield SV48_Vaddr : vaddr48 = { + VPNi : 38 .. 12, + PgOfs : 11 .. 0 +} + +bitfield SV48_Paddr : paddr64 = { + PPNi : 55 .. 12, + PgOfs : 11 .. 0 +} + +bitfield SV48_PTE : pte48 = { + PPNi : 53 .. 10, + RSW : 9 .. 8, + BITS : 7 .. 0 +} + +/* Result of a page-table walk. */ + +union PTW_Result('paddr : Type, 'pte : Type) = { + PTW_Success: ('paddr, 'pte, 'paddr, nat, bool), + PTW_Failure: PTW_Error +} + +/* Result of address translation */ + +union TR_Result('paddr : Type, 'failure : Type) = { + TR_Address : 'paddr, + TR_Failure : 'failure +} diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail new file mode 100644 index 0000000..ff5443f --- /dev/null +++ b/model/riscv_vmem_rv32.sail @@ -0,0 +1,66 @@ +/* RV32 Supervisor-mode address translation and page-table walks. */ + +/* Define the architectural satp and its legalizer. */ + +register satp : xlenbits + +function legalize_satp(a : Architecture, o : xlenbits, v : xlenbits) -> xlenbits = + legalize_satp32(a, o, v) + +/* Compute the address translation mode. */ + +val translationMode : (Privilege) -> SATPMode effect {rreg, escape} +function translationMode(priv) = { + if priv == Machine then Sbare + else { + let arch = architecture(get_mstatus_SXL(mstatus)); + match arch { + Some(RV32) => { + let s = Mk_Satp32(satp[31..0]); + if s.Mode() == false then Sbare else Sv32 + }, + _ => internal_error("unsupported address translation arch") + } + } +} + +/* Top-level address translation dispatcher */ + +val translateAddr : (xlenbits, AccessType, ReadType) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rreg, wmv, wreg} +function translateAddr(vAddr, ac, rt) = { + let effPriv : Privilege = match rt { + Instruction => cur_privilege, + Data => if mstatus.MPRV() == true + then privLevel_of_bits(mstatus.MPP()) + else cur_privilege + }; + let mxr : bool = mstatus.MXR() == true; + let do_sum : bool = mstatus.SUM() == true; + let mode : SATPMode = translationMode(effPriv); + + let asid = curAsid32(satp); + let ptb = curPTB32(satp); + + match mode { + Sbare => TR_Address(vAddr), + Sv32 => match translate32(asid, ptb, vAddr, ac, effPriv, mxr, do_sum, SV32_LEVELS - 1) { + TR_Address(pa) => TR_Address(to_phys_addr(pa)), + TR_Failure(f) => TR_Failure(translationException(ac, f)) + }, + _ => internal_error("unsupported address translation scheme") + } +} + +val flush_TLB : (option(xlenbits), option(xlenbits)) -> unit effect {rreg, wreg} +function flush_TLB(asid_xlen, addr_xlen) -> unit = { + let asid : option(asid32) = + match (asid_xlen) { + None() => None(), + Some(a) => Some(a[8 .. 0]) + }; + flush_TLB32(asid, addr_xlen) +} + +function init_vmem () -> unit = { + init_vmem_sv32() +} diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail new file mode 100644 index 0000000..58d187e --- /dev/null +++ b/model/riscv_vmem_rv64.sail @@ -0,0 +1,85 @@ +/* RV64 Supervisor-mode address translation and page-table walks. */ + +/* Define the architectural satp and its legalizer. */ + +register satp : xlenbits + +function legalize_satp(a : Architecture, o : xlenbits, v : xlenbits) -> xlenbits = + legalize_satp64(a, o, v) + +/* Compute the address translation mode. */ + +val translationMode : (Privilege) -> SATPMode effect {rreg, escape} +function translationMode(priv) = { + if priv == Machine then Sbare + else { + let arch = architecture(get_mstatus_SXL(mstatus)); + match arch { + Some(RV64) => { + let mbits : satp_mode = Mk_Satp64(satp).Mode(); + match satp64Mode_of_bits(RV64, mbits) { + Some(m) => m, + None() => internal_error("invalid RV64 translation mode in satp") + } + }, + Some(RV32) => { + let s = Mk_Satp32(satp[31..0]); + if s.Mode() == false then Sbare else Sv32 + }, + _ => internal_error("unsupported address translation arch") + } + } +} + +/* Top-level address translation dispatcher */ + +val translateAddr : (xlenbits, AccessType, ReadType) -> TR_Result(xlenbits, ExceptionType) effect {escape, rmem, rreg, wmv, wreg} +function translateAddr(vAddr, ac, rt) = { + let effPriv : Privilege = match rt { + Instruction => cur_privilege, + Data => if mstatus.MPRV() == true + then privLevel_of_bits(mstatus.MPP()) + else cur_privilege + }; + let mxr : bool = mstatus.MXR() == true; + let do_sum : bool = mstatus.SUM() == true; + let mode : SATPMode = translationMode(effPriv); + + let asid = curAsid64(satp); + let ptb = curPTB64(satp); + + match mode { + Sbare => TR_Address(vAddr), + Sv39 => match translate39(asid, ptb, vAddr[38 .. 0], ac, effPriv, mxr, do_sum, SV39_LEVELS - 1) { + TR_Address(pa) => TR_Address(EXTZ(pa)), + TR_Failure(f) => TR_Failure(translationException(ac, f)) + }, + Sv48 => match translate48(asid, ptb, vAddr[47 .. 0], ac, effPriv, mxr, do_sum, SV48_LEVELS - 1) { + TR_Address(pa) => TR_Address(EXTZ(pa)), + TR_Failure(f) => TR_Failure(translationException(ac, f)) + }, + _ => internal_error("unsupported address translation scheme") + } +} + +val flush_TLB : (option(xlenbits), option(xlenbits)) -> unit effect {rreg, wreg} +function flush_TLB(asid_xlen, addr_xlen) -> unit = { + /* Flush both Sv39 and Sv48 TLBs. */ + let (addr39, addr48) : (option(vaddr39), option(vaddr48)) = + match addr_xlen { + None() => (None(), None()), + Some(a) => (Some(a[38 .. 0]), Some(a[47 .. 0])) + }; + let asid : option(asid64) = + match asid_xlen { + None() => None(), + Some(a) => Some(a[15 .. 0]) + }; + flush_TLB39(asid, addr39); + flush_TLB48(asid, addr48) +} + +function init_vmem() -> unit = { + init_vmem_sv39(); + init_vmem_sv48() +} diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail new file mode 100644 index 0000000..437851c --- /dev/null +++ b/model/riscv_vmem_sv32.sail @@ -0,0 +1,185 @@ +/* Sv32 address translation for RV32. */ + +/* FIXME: paddr32 is 34-bits, but phys_mem accesses in riscv_mem take 32-bit (xlenbits) addresses. + * Define a converter for now. + */ + +function to_phys_addr(a : paddr32) -> xlenbits = a[31..0] + +val walk32 : (vaddr32, AccessType, Privilege, bool, bool, paddr32, nat, bool) -> PTW_Result(paddr32, SV32_PTE) effect {rmem, escape} +function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = { + let va = Mk_SV32_Vaddr(vaddr); + let pt_ofs : paddr32 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV32_LEVEL_BITS))[(SV32_LEVEL_BITS - 1) .. 0]), + PTE32_LOG_SIZE); + let pte_addr = ptb + pt_ofs; + /* FIXME: we assume here that walks only access physical-memory-backed addresses, and not MMIO regions. */ + match (phys_mem_read(Data, to_phys_addr(pte_addr), 4, false, false, false)) { + MemException(_) => { +/* print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) + ^ " pt_base=" ^ BitStr(to_phys_addr(ptb)) + ^ " pt_ofs=" ^ BitStr(to_phys_addr(pt_ofs)) + ^ " pte_addr=" ^ BitStr(to_phys_addr(pte_addr)) + ^ ": invalid pte address"); */ + PTW_Failure(PTW_Access) + }, + MemValue(v) => { + let pte = Mk_SV32_PTE(v); + let pbits = pte.BITS(); + let pattr = Mk_PTE_Bits(pbits); + let is_global = global | (pattr.G() == true); +/* print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) + ^ " pt_base=" ^ BitStr(to_phys_addr(ptb)) + ^ " pt_ofs=" ^ BitStr(to_phys_addr(pt_ofs)) + ^ " pte_addr=" ^ BitStr(to_phys_addr(pte_addr)) + ^ " pte=" ^ BitStr(v)); */ + if isInvalidPTE(pbits) then { +/* print("walk32: invalid pte"); */ + PTW_Failure(PTW_Invalid_PTE) + } else { + if isPTEPtr(pbits) then { + if level == 0 then { + /* last-level PTE contains a pointer instead of a leaf */ +/* print("walk32: last-level pte contains a ptr"); */ + PTW_Failure(PTW_Invalid_PTE) + } else { + /* walk down the pointer to the next level */ + walk32(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global) + } + } else { /* leaf PTE */ + if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pattr)) then { +/* print("walk32: pte permission check failure"); */ + PTW_Failure(PTW_No_Permission) + } else { + if level > 0 then { /* superpage */ + /* fixme hack: to get a mask of appropriate size */ + let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ EXTZ(0b1), level * SV32_LEVEL_BITS) - 1; + if (pte.PPNi() & mask) != EXTZ(0b0) then { + /* misaligned superpage mapping */ +/* print("walk32: misaligned superpage mapping"); */ + PTW_Failure(PTW_Misaligned) + } else { + /* add the appropriate bits of the VPN to the superpage PPN */ + let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & mask); +/* let res = append(ppn, va.PgOfs()); + print("walk32: using superpage: pte.ppn=" ^ BitStr(pte.PPNi()) + ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ + PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global) + } + } else { + /* normal leaf PTE */ +/* let res = append(pte.PPNi(), va.PgOfs()); + print("walk32: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(pte.PPNi()) ^ " res=" ^ BitStr(res)); */ + PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global) + } + } + } + } + } + } +} + +/* TLB management: single entry for now */ + +// ideally we would use the below form: +// type TLB32_Entry = TLB_Entry(sizeof(asid32), sizeof(vaddr32), sizeof(paddr32), sizeof(pte32)) +type TLB32_Entry = TLB_Entry(9, 32, 34, 32) +register tlb32 : option(TLB32_Entry) + +val lookup_TLB32 : (asid32, vaddr32) -> option((nat, TLB32_Entry)) effect {rreg} +function lookup_TLB32(asid, vaddr) = + match tlb32 { + None() => None(), + Some(e) => if match_TLB_Entry(e, asid, vaddr) then Some((0, e)) else None() + } + +val add_to_TLB32 : (asid32, vaddr32, paddr32, SV32_PTE, paddr32, nat, bool) -> unit effect {wreg, rreg} +function add_to_TLB32(asid, vAddr, pAddr, pte, pteAddr, level, global) = { + let ent : TLB32_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits(), level, pteAddr, SV32_LEVEL_BITS); + tlb32 = Some(ent) +} + +function write_TLB32(idx : nat, ent : TLB32_Entry) -> unit = + tlb32 = Some(ent) + +val flush_TLB32 : (option(asid32), option(vaddr32)) -> unit effect {rreg, wreg} +function flush_TLB32(asid, addr) = + match (tlb32) { + None() => (), + Some(e) => if flush_TLB_Entry(e, asid, addr) + then tlb32 = None() + else () + } + +/* address translation */ + +val translate32 : (asid32, paddr32, vaddr32, AccessType, Privilege, bool, bool, nat) -> TR_Result(paddr32, PTW_Error) effect {rreg, wreg, wmv, escape, rmem} +function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = { + match lookup_TLB32(asid, vAddr) { + Some(idx, ent) => { +/* print("translate32: TLB32 hit for " ^ BitStr(vAddr)); */ + let pte = Mk_SV32_PTE(ent.pte); + let pteBits = Mk_PTE_Bits(pte.BITS()); + if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pteBits)) + then TR_Failure(PTW_No_Permission) + else { + match update_PTE_Bits(pteBits, ac) { + None() => TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)), + Some(pbits) => { + if ~ (plat_enable_dirty_update ()) + then { + /* pte needs dirty/accessed update but that is not enabled */ + TR_Failure(PTW_PTE_Update) + } else { + /* update PTE entry and TLB */ + n_pte = update_BITS(pte, pbits.bits()); + n_ent : TLB32_Entry = ent; + n_ent.pte = n_pte.bits(); + write_TLB32(idx, n_ent); + /* update page table */ + match checked_mem_write(to_phys_addr(EXTZ(ent.pteAddr)), 4, n_pte.bits(), false, false, false) { + MemValue(_) => (), + MemException(e) => internal_error("invalid physical address in TLB") + }; + TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)) + } + } + } + } + }, + None() => { + match walk32(vAddr, ac, priv, mxr, do_sum, ptb, level, false) { + PTW_Failure(f) => TR_Failure(f), + PTW_Success(pAddr, pte, pteAddr, level, global) => { + match update_PTE_Bits(Mk_PTE_Bits(pte.BITS()), ac) { + None() => { + add_to_TLB32(asid, vAddr, pAddr, pte, pteAddr, level, global); + TR_Address(pAddr) + }, + Some(pbits) => + if ~ (plat_enable_dirty_update ()) + then { + /* pte needs dirty/accessed update but that is not enabled */ + TR_Failure(PTW_PTE_Update) + } else { + w_pte : SV32_PTE = update_BITS(pte, pbits.bits()); + match checked_mem_write(to_phys_addr(pteAddr), 4, w_pte.bits(), false, false, false) { + MemValue(_) => { + add_to_TLB32(asid, vAddr, pAddr, w_pte, pteAddr, level, global); + TR_Address(pAddr) + }, + MemException(e) => { + /* pte is not in valid memory */ + TR_Failure(PTW_Access) + } + } + } + } + } + } + } + } +} + +function init_vmem_sv32() -> unit = { + tlb32 = None() +} diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail new file mode 100644 index 0000000..b349783 --- /dev/null +++ b/model/riscv_vmem_sv39.sail @@ -0,0 +1,179 @@ +/* Sv39 address translation for RV64. */ + +val walk39 : (vaddr39, AccessType, Privilege, bool, bool, paddr64, nat, bool) -> PTW_Result(paddr64, SV39_PTE) effect {rmem, escape} +function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = { + let va = Mk_SV39_Vaddr(vaddr); + let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]), + PTE39_LOG_SIZE); + let pte_addr = ptb + pt_ofs; + /* FIXME: we assume here that walks only access physical-memory-backed addresses, and not MMIO regions. */ + match (phys_mem_read(Data, EXTZ(pte_addr), 8, false, false, false)) { + MemException(_) => { +/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) + ^ " pt_base=" ^ BitStr(ptb) + ^ " pt_ofs=" ^ BitStr(pt_ofs) + ^ " pte_addr=" ^ BitStr(pte_addr) + ^ ": invalid pte address"); */ + PTW_Failure(PTW_Access) + }, + MemValue(v) => { + let pte = Mk_SV39_PTE(v); + let pbits = pte.BITS(); + let pattr = Mk_PTE_Bits(pbits); + let is_global = global | (pattr.G() == true); +/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) + ^ " pt_base=" ^ BitStr(ptb) + ^ " pt_ofs=" ^ BitStr(pt_ofs) + ^ " pte_addr=" ^ BitStr(pte_addr) + ^ " pte=" ^ BitStr(v)); */ + if isInvalidPTE(pbits) then { +/* print("walk39: invalid pte"); */ + PTW_Failure(PTW_Invalid_PTE) + } else { + if isPTEPtr(pbits) then { + if level == 0 then { + /* last-level PTE contains a pointer instead of a leaf */ +/* print("walk39: last-level pte contains a ptr"); */ + PTW_Failure(PTW_Invalid_PTE) + } else { + /* walk down the pointer to the next level */ + walk39(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global) + } + } else { /* leaf PTE */ + if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pattr)) then { +/* print("walk39: pte permission check failure"); */ + PTW_Failure(PTW_No_Permission) + } else { + if level > 0 then { /* superpage */ + /* fixme hack: to get a mask of appropriate size */ + let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ EXTZ(0b1), level * SV39_LEVEL_BITS) - 1; + if (pte.PPNi() & mask) != EXTZ(0b0) then { + /* misaligned superpage mapping */ +/* print("walk39: misaligned superpage mapping"); */ + PTW_Failure(PTW_Misaligned) + } else { + /* add the appropriate bits of the VPN to the superpage PPN */ + let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & mask); +/* let res = append(ppn, va.PgOfs()); + print("walk39: using superpage: pte.ppn=" ^ BitStr(pte.PPNi()) + ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ + PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global) + } + } else { + /* normal leaf PTE */ +/* let res = append(pte.PPNi(), va.PgOfs()); + print("walk39: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(pte.PPNi()) ^ " res=" ^ BitStr(res)); */ + PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global) + } + } + } + } + } + } +} + +/* TLB management: single entry for now */ + +// ideally we would use the below form: +// type TLB39_Entry = TLB_Entry(sizeof(asid64), sizeof(vaddr39), sizeof(paddr64), sizeof(pte64)) +type TLB39_Entry = TLB_Entry(16, 39, 56, 64) +register tlb39 : option(TLB39_Entry) + +val lookup_TLB39 : (asid64, vaddr39) -> option((nat, TLB39_Entry)) effect {rreg} +function lookup_TLB39(asid, vaddr) = + match tlb39 { + None() => None(), + Some(e) => if match_TLB_Entry(e, asid, vaddr) then Some((0, e)) else None() + } + +val add_to_TLB39 : (asid64, vaddr39, paddr64, SV39_PTE, paddr64, nat, bool) -> unit effect {wreg, rreg} +function add_to_TLB39(asid, vAddr, pAddr, pte, pteAddr, level, global) = { + let ent : TLB39_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits(), level, pteAddr, SV39_LEVEL_BITS); + tlb39 = Some(ent) +} + +function write_TLB39(idx : nat, ent : TLB39_Entry) -> unit = + tlb39 = Some(ent) + +val flush_TLB39 : (option(asid64), option(vaddr39)) -> unit effect {rreg, wreg} +function flush_TLB39(asid, addr) = + match (tlb39) { + None() => (), + Some(e) => if flush_TLB_Entry(e, asid, addr) + then tlb39 = None() + else () + } + +/* address translation */ + +val translate39 : (asid64, paddr64, vaddr39, AccessType, Privilege, bool, bool, nat) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, escape, rmem} +function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = { + match lookup_TLB39(asid, vAddr) { + Some(idx, ent) => { +/* print("translate39: TLB39 hit for " ^ BitStr(vAddr)); */ + let pte = Mk_SV39_PTE(ent.pte); + let pteBits = Mk_PTE_Bits(pte.BITS()); + if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pteBits)) + then TR_Failure(PTW_No_Permission) + else { + match update_PTE_Bits(pteBits, ac) { + None() => TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)), + Some(pbits) => { + if ~ (plat_enable_dirty_update ()) + then { + /* pte needs dirty/accessed update but that is not enabled */ + TR_Failure(PTW_PTE_Update) + } else { + /* update PTE entry and TLB */ + n_pte = update_BITS(pte, pbits.bits()); + n_ent : TLB39_Entry = ent; + n_ent.pte = n_pte.bits(); + write_TLB39(idx, n_ent); + /* update page table */ + match checked_mem_write(EXTZ(ent.pteAddr), 8, n_pte.bits(), false, false, false) { + MemValue(_) => (), + MemException(e) => internal_error("invalid physical address in TLB") + }; + TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)) + } + } + } + } + }, + None() => { + match walk39(vAddr, ac, priv, mxr, do_sum, ptb, level, false) { + PTW_Failure(f) => TR_Failure(f), + PTW_Success(pAddr, pte, pteAddr, level, global) => { + match update_PTE_Bits(Mk_PTE_Bits(pte.BITS()), ac) { + None() => { + add_to_TLB39(asid, vAddr, pAddr, pte, pteAddr, level, global); + TR_Address(pAddr) + }, + Some(pbits) => + if ~ (plat_enable_dirty_update ()) + then { + /* pte needs dirty/accessed update but that is not enabled */ + TR_Failure(PTW_PTE_Update) + } else { + w_pte : SV39_PTE = update_BITS(pte, pbits.bits()); + match checked_mem_write(EXTZ(pteAddr), 8, w_pte.bits(), false, false, false) { + MemValue(_) => { + add_to_TLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global); + TR_Address(pAddr) + }, + MemException(e) => { + /* pte is not in valid memory */ + TR_Failure(PTW_Access) + } + } + } + } + } + } + } + } +} + +function init_vmem_sv39() -> unit = { + tlb39 = None() +} diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail new file mode 100644 index 0000000..b3bd47e --- /dev/null +++ b/model/riscv_vmem_sv48.sail @@ -0,0 +1,144 @@ +/* Sv48 address translation for RV64. */ + +val walk48 : (vaddr48, AccessType, Privilege, bool, bool, paddr64, nat, bool) -> PTW_Result(paddr64, SV48_PTE) effect {rmem, escape} +function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = { + let va = Mk_SV48_Vaddr(vaddr); + let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV48_LEVEL_BITS))[(SV48_LEVEL_BITS - 1) .. 0]), + PTE48_LOG_SIZE); + let pte_addr = ptb + pt_ofs; + /* FIXME: we assume here that walks only access physical-memory-backed addresses, and not MMIO regions. */ + match (phys_mem_read(Data, EXTZ(pte_addr), 8, false, false, false)) { + MemException(_) => { +/* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) + ^ " pt_base=" ^ BitStr(ptb) + ^ " pt_ofs=" ^ BitStr(pt_ofs) + ^ " pte_addr=" ^ BitStr(pte_addr) + ^ ": invalid pte address"); */ + PTW_Failure(PTW_Access) + }, + MemValue(v) => { + let pte = Mk_SV48_PTE(v); + let pbits = pte.BITS(); + let pattr = Mk_PTE_Bits(pbits); + let is_global = global | (pattr.G() == true); +/* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) + ^ " pt_base=" ^ BitStr(ptb) + ^ " pt_ofs=" ^ BitStr(pt_ofs) + ^ " pte_addr=" ^ BitStr(pte_addr) + ^ " pte=" ^ BitStr(v)); */ + if isInvalidPTE(pbits) then { +/* print("walk48: invalid pte"); */ + PTW_Failure(PTW_Invalid_PTE) + } else { + if isPTEPtr(pbits) then { + if level == 0 then { + /* last-level PTE contains a pointer instead of a leaf */ +/* print("walk48: last-level pte contains a ptr"); */ + PTW_Failure(PTW_Invalid_PTE) + } else { + /* walk down the pointer to the next level */ + walk48(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global) + } + } else { /* leaf PTE */ + if ~ (checkPTEPermission(ac, priv, mxr, do_sum, pattr)) then { +/* print("walk48: pte permission check failure"); */ + PTW_Failure(PTW_No_Permission) + } else { + if level > 0 then { /* superpage */ + /* fixme hack: to get a mask of appropriate size */ + let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ EXTZ(0b1), level * SV48_LEVEL_BITS) - 1; + if (pte.PPNi() & mask) != EXTZ(0b0) then { + /* misaligned superpage mapping */ +/* print("walk48: misaligned superpage mapping"); */ + PTW_Failure(PTW_Misaligned) + } else { + /* add the appropriate bits of the VPN to the superpage PPN */ + let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & mask); +/* let res = append(ppn, va.PgOfs()); + print("walk48: using superpage: pte.ppn=" ^ BitStr(pte.PPNi()) + ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ + PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global) + } + } else { + /* normal leaf PTE */ +/* let res = append(pte.PPNi(), va.PgOfs()); + print("walk48: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(pte.PPNi()) ^ " res=" ^ BitStr(res)); */ + PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global) + } + } + } + } + } + } +} + +/* TLB management: single entry for now */ + +// ideally we would use the below form: +// type TLB48_Entry = TLB_Entry(sizeof(asid64), sizeof(vaddr48), sizeof(paddr64), sizeof(pte64)) +type TLB48_Entry = TLB_Entry(16, 48, 56, 64) +register tlb48 : option(TLB48_Entry) + +val lookup_TLB48 : (asid64, vaddr48) -> option((nat, TLB48_Entry)) effect {rreg} +function lookup_TLB48(asid, vaddr) = + match tlb48 { + None() => None(), + Some(e) => if match_TLB_Entry(e, asid, vaddr) then Some((0, e)) else None() + } + +val add_to_TLB48 : (asid64, vaddr48, paddr64, SV48_PTE, paddr64, nat, bool) -> unit effect {wreg, rreg} +function add_to_TLB48(asid, vAddr, pAddr, pte, pteAddr, level, global) = { + let ent : TLB48_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits(), level, pteAddr, SV48_LEVEL_BITS); + tlb48 = Some(ent) +} + +function write_TLB48(idx : nat, ent : TLB48_Entry) -> unit = + tlb48 = Some(ent) + +val flush_TLB48 : (option(asid64), option(vaddr48)) -> unit effect {rreg, wreg} +function flush_TLB48(asid, addr) = + match (tlb48) { + None() => (), + Some(e) => if flush_TLB_Entry(e, asid, addr) + then tlb48 = None() + else () + } + +/* address translation */ + +val translate48 : (asid64, paddr64, vaddr48, AccessType, Privilege, bool, bool, nat) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, escape, rmem} +function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level) = { + match walk48(vAddr, ac, priv, mxr, do_sum, ptb, level, false) { + PTW_Failure(f) => TR_Failure(f), + PTW_Success(pAddr, pte, pteAddr, level, global) => { + match update_PTE_Bits(Mk_PTE_Bits(pte.BITS()), ac) { + None() => { + add_to_TLB48(asid, vAddr, pAddr, pte, pteAddr, level, global); + TR_Address(pAddr) + }, + Some(pbits) => + if ~ (plat_enable_dirty_update ()) + then { + /* pte needs dirty/accessed update but that is not enabled */ + TR_Failure(PTW_PTE_Update) + } else { + w_pte : SV48_PTE = update_BITS(pte, pbits.bits()); + match checked_mem_write(EXTZ(pteAddr), 8, w_pte.bits(), false, false, false) { + MemValue(_) => { + add_to_TLB48(asid, vAddr, pAddr, w_pte, pteAddr, level, global); + TR_Address(pAddr) + }, + MemException(e) => { + /* pte is not in valid memory */ + TR_Failure(PTW_Access) + } + } + } + } + } + } +} + +function init_vmem_sv48() -> unit = { + tlb48 = None() +} diff --git a/model/riscv_vmem_tlb.sail b/model/riscv_vmem_tlb.sail new file mode 100644 index 0000000..5d9831c --- /dev/null +++ b/model/riscv_vmem_tlb.sail @@ -0,0 +1,54 @@ +/* idealized generic TLB entry to model fence.vm and also speed up simulation. */ + +struct TLB_Entry('asidlen: Int, 'valen: Int, 'palen: Int, 'ptelen: Int) = { + asid : bits('asidlen), + global : bool, + vAddr : bits('valen), /* VPN */ + pAddr : bits('palen), /* PPN */ + vMatchMask : bits('valen), /* matching mask for superpages */ + vAddrMask : bits('valen), /* selection mask for superpages */ + pte : bits('ptelen), /* PTE */ + pteAddr : bits('palen), /* for dirty writeback */ + age : bits(64) +} + + +val make_TLB_Entry : forall 'asidlen 'valen 'palen 'ptelen, 'valen > 0. + (bits('asidlen), bool, bits('valen), bits('palen), bits('ptelen), nat, bits('palen), nat) + -> TLB_Entry('asidlen, 'valen, 'palen, 'ptelen) effect {rreg} +function make_TLB_Entry(asid, global, vAddr, pAddr, pte, level, pteAddr, levelBitSize) = { + let shift : nat = PAGESIZE_BITS + (level * levelBitSize); + /* fixme hack: use a better idiom for masks */ + let vAddrMask : bits('valen) = shiftl(vAddr ^ vAddr ^ EXTZ(0b1), shift) - 1; + let vMatchMask : bits('valen) = ~ (vAddrMask); + struct { + asid = asid, + global = global, + pte = pte, + pteAddr = pteAddr, + vAddrMask = vAddrMask, + vMatchMask = vMatchMask, + vAddr = vAddr & vMatchMask, + pAddr = shiftl(shiftr(pAddr, shift), shift), + age = mcycle + } +} + +val match_TLB_Entry : forall 'asidlen 'valen 'palen 'ptelen. + (TLB_Entry('asidlen, 'valen, 'palen, 'ptelen), bits('asidlen), bits('valen)) + -> bool +function match_TLB_Entry(ent, asid, vaddr) = + (ent.global | (ent.asid == asid)) & (ent.vAddr == (ent.vMatchMask & vaddr)) + +val flush_TLB_Entry : forall 'asidlen 'valen 'palen 'ptelen. + (TLB_Entry('asidlen, 'valen, 'palen, 'ptelen), option(bits('asidlen)), option(bits('valen))) + -> bool +function flush_TLB_Entry(e, asid, addr) = { + match(asid, addr) { + ( None(), None()) => true, + ( None(), Some(a)) => e.vAddr == (e.vMatchMask & a), + (Some(i), None()) => (e.asid == i) & (~ (e.global)), + (Some(i), Some(a)) => ( (e.asid == i) & (e.vAddr == (a & e.vMatchMask)) + & (~ (e.global))) + } +} diff --git a/model/riscv_xlen32.sail b/model/riscv_xlen32.sail new file mode 100644 index 0000000..3722e85 --- /dev/null +++ b/model/riscv_xlen32.sail @@ -0,0 +1,5 @@ +/* Define the XLEN value for the architecture. */ + +type xlen : Int = 32 +type xlen_bytes : Int = 4 +type xlenbits = bits(xlen) diff --git a/model/riscv_xlen64.sail b/model/riscv_xlen64.sail new file mode 100644 index 0000000..7abf5dd --- /dev/null +++ b/model/riscv_xlen64.sail @@ -0,0 +1,5 @@ +/* Define the XLEN value for the architecture. */ + +type xlen : Int = 64 +type xlen_bytes : Int = 8 +type xlenbits = bits(xlen) diff --git a/model/rvfi_dii.sail b/model/rvfi_dii.sail index 9680ab4..b0e3a06 100644 --- a/model/rvfi_dii.sail +++ b/model/rvfi_dii.sail @@ -63,7 +63,7 @@ register rvfi_exec : RVFI_DII_Execution_Packet val rvfi_zero_exec_packet : unit -> unit effect {wreg} function rvfi_zero_exec_packet () = - rvfi_exec = Mk_RVFI_DII_Execution_Packet(zero_extend(0b0,704)) + rvfi_exec = Mk_RVFI_DII_Execution_Packet(sail_zero_extend(0b0,704)) val rvfi_halt_exec_packet : unit -> unit effect {wreg} |