diff options
| author | Alasdair Armstrong | 2018-07-24 18:09:18 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-07-24 18:09:18 +0100 |
| commit | 6b4f407ad34ca7d4d8a89a5a4d401ac80c7413b0 (patch) | |
| tree | ed09b22b7ea4ca20fbcc89b761f1955caea85041 /riscv | |
| parent | dafb09e7c26840dce3d522fef3cf359729ca5b61 (diff) | |
| parent | 8114501b7b956ee4a98fa8599c7efee62fc19206 (diff) | |
Merge remote-tracking branch 'origin/sail2' into c_fixes
Diffstat (limited to 'riscv')
| -rw-r--r-- | riscv/Makefile | 22 | ||||
| -rw-r--r-- | riscv/_tags.bisect | 3 | ||||
| -rw-r--r-- | riscv/platform.ml | 17 | ||||
| -rw-r--r-- | riscv/platform_impl.ml | 19 | ||||
| -rw-r--r-- | riscv/platform_main.ml | 30 | ||||
| -rw-r--r-- | riscv/prelude.sail | 44 | ||||
| -rw-r--r-- | riscv/riscv.sail | 1219 | ||||
| -rw-r--r-- | riscv/riscv_analysis.sail | 179 | ||||
| -rw-r--r-- | riscv/riscv_duopod.sail | 2 | ||||
| -rw-r--r-- | riscv/riscv_extras.lem | 38 | ||||
| -rw-r--r-- | riscv/riscv_extras_sequential.lem | 38 | ||||
| -rw-r--r-- | riscv/riscv_mem.sail | 81 | ||||
| -rw-r--r-- | riscv/riscv_platform.sail | 84 | ||||
| -rw-r--r-- | riscv/riscv_step.sail | 31 | ||||
| -rw-r--r-- | riscv/riscv_sys.sail | 199 | ||||
| -rw-r--r-- | riscv/riscv_types.sail | 262 | ||||
| -rw-r--r-- | riscv/riscv_vmem.sail | 94 | ||||
| -rw-r--r-- | riscv/tracecmp.ml | 69 |
18 files changed, 1340 insertions, 1091 deletions
diff --git a/riscv/Makefile b/riscv/Makefile index 22f80338..4a396048 100644 --- a/riscv/Makefile +++ b/riscv/Makefile @@ -1,4 +1,4 @@ -SAIL_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail riscv_mem.sail riscv_vmem.sail riscv.sail riscv_step.sail +SAIL_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv_platform.sail riscv_mem.sail riscv_vmem.sail riscv.sail riscv_step.sail riscv_analysis.sail PLATFORM_OCAML_SRCS = platform.ml platform_impl.ml platform_main.ml SAIL_DIR ?= $(realpath ..) SAIL ?= $(SAIL_DIR)/sail @@ -17,9 +17,24 @@ _sbuild/platform_main.native: _sbuild/riscv.ml _tags $(PLATFORM_OCAML_SRCS) Make cp _tags $(PLATFORM_OCAML_SRCS) _sbuild cd _sbuild && ocamlbuild -use-ocamlfind platform_main.native +_sbuild/coverage.native: _sbuild/riscv.ml _tags.bisect $(PLATFORM_OCAML_SRCS) Makefile + cp $(PLATFORM_OCAML_SRCS) _sbuild + cp _tags.bisect _sbuild/_tags + cd _sbuild && ocamlbuild -use-ocamlfind platform_main.native && cp -L platform_main.native coverage.native + platform: _sbuild/platform_main.native rm -f $@ && ln -s $^ $@ +coverage: _sbuild/coverage.native + rm -f platform && ln -s $^ platform # since the test scripts runs this file + rm -rf bisect*.out bisect coverage + ../test/riscv/run_tests.sh # this will generate bisect*.out files in this directory + mkdir bisect && mv bisect*.out bisect/ + mkdir coverage && bisect-ppx-report -html coverage/ -I _sbuild/ bisect/bisect*.out + +riscv.c: $(SAIL_SRCS) Makefile + $(SAIL) -O -memo_z3 -c $(SAIL_SRCS) 1> $@ + tracecmp: tracecmp.ml ocamlfind ocamlopt -annot -linkpkg -package unix $^ -o $@ @@ -50,7 +65,8 @@ riscv_sequential.lem: $(SAIL_SRCS) Makefile $(SAIL_DIR)/sail -lem -lem_sequential -o riscv_sequential -lem_mwords -lem_lib Riscv_extras_sequential $(SAIL_SRCS) riscvScript.sml : riscv.lem riscv_extras.lem - lem -hol -outdir . -lib ../lib/hol -lib ../src/lem_interp -lib ../src/gen_lib \ + lem -hol -outdir . -lib ../lib/hol -i ../lib/hol/sail2_prompt_monad.lem -i ../lib/hol/sail2_prompt.lem \ + -lib ../src/lem_interp -lib ../src/gen_lib \ riscv_extras.lem \ riscv_types.lem \ riscv.lem @@ -69,6 +85,6 @@ clean: Riscv_extras.thy -rm -f Riscv_duopod.thy Riscv_duopod_types.thy riscv_duopod.lem riscv_duopod_types.lem -rm -f riscvScript.sml riscv_typesScript.sml riscv_extrasScript.sml - -rm -f platform_main.native platform + -rm -f platform_main.native platform coverage.native -Holmake cleanAll ocamlbuild -clean diff --git a/riscv/_tags.bisect b/riscv/_tags.bisect new file mode 100644 index 00000000..d3b996f2 --- /dev/null +++ b/riscv/_tags.bisect @@ -0,0 +1,3 @@ +<**/*.ml>: bin_annot, annot +<*.m{l,li}>: package(lem), package(linksem), package(zarith), package(bisect_ppx) +<platform_main.native>: package(lem), package(linksem), package(zarith), package(bisect_ppx) diff --git a/riscv/platform.ml b/riscv/platform.ml index 0366e601..092df80f 100644 --- a/riscv/platform.ml +++ b/riscv/platform.ml @@ -97,7 +97,24 @@ let clint_size () = bits_of_int64 P.clint_size let insns_per_tick () = Big_int.of_int P.insns_per_tick +(* load reservation *) + +let reservation = ref "none" (* shouldn't match any valid address *) + +let load_reservation addr = + Printf.eprintf "reservation <- %s\n" (string_of_bits addr); + reservation := string_of_bits addr + +let match_reservation addr = + Printf.eprintf "reservation: %s, key=%s\n" (!reservation) (string_of_bits addr); + string_of_bits addr = !reservation + +let cancel_reservation () = + Printf.eprintf "reservation <- none\n"; + reservation := "none" + (* terminal I/O *) + let term_write char_bits = let big_char = Big_int.bitwise_and (uint char_bits) (Big_int.of_int 255) in P.term_write (char_of_int (Big_int.to_int big_char)) diff --git a/riscv/platform_impl.ml b/riscv/platform_impl.ml index aab272f8..e593dce9 100644 --- a/riscv/platform_impl.ml +++ b/riscv/platform_impl.ml @@ -107,16 +107,29 @@ let cpu_hz = 1000000000;; let insns_per_tick = 100;; let mems = [ { addr = dram_base; - size = dram_size } ];; + size = dram_size } ];; let dts = spike_dts "rv64imac" cpu_hz insns_per_tick mems;; let bytes_to_string bytes = String.init (List.length bytes) (fun i -> Char.chr (List.nth bytes i)) +let dtc_path = ref "/usr/bin/dtc" + +let set_dtc path = + try let st = Unix.stat path in + if st.Unix.st_kind = Unix.S_REG && st.Unix.st_perm != 0 + then dtc_path := path + else ( Printf.eprintf "%s doesn't seem like a valid executable.\n%!" path; + exit 1) + with Unix.Unix_error (e, _, _) -> + ( Printf.eprintf "Error accessing %s: %s\n%!" path (Unix.error_message e); + exit 1) + let make_dtb dts = (* Call the dtc compiler, assumed to be at /usr/bin/dtc *) try + let cmd = Printf.sprintf "%s -I dts" !dtc_path in let (cfrom, cto, cerr) = - Unix.open_process_full "/usr/bin/dtc -I dts" [||] + Unix.open_process_full cmd [||] in ( output_string cto dts; (* print_endline " sent dts to dtc ..."; *) @@ -136,7 +149,7 @@ let make_dtb dts = (* Call the dtc compiler, assumed to be at /usr/bin/dtc *) let emsg = bytes_to_string (accum_bytes cerr []) in match Unix.close_process_full (cfrom, cto, cerr) with | Unix.WEXITED 0 -> dtb - | _ -> (Printf.printf "%s\n" ("Error executing dtc: " ^ emsg); + | _ -> (Printf.printf "%s\n%!" ("Error executing dtc: " ^ emsg); exit 1) ) with Unix.Unix_error (e, fn, _) -> diff --git a/riscv/platform_main.ml b/riscv/platform_main.ml index 8dd47547..e204daee 100644 --- a/riscv/platform_main.ml +++ b/riscv/platform_main.ml @@ -72,7 +72,10 @@ let options = Arg.align ([("-dump-dts", " enable dirty-bit update during page-table walks"); ("-enable-misaligned-access", Arg.Set P.config_enable_misaligned_access, - " enable misaligned accesses without M-mode traps") + " enable misaligned accesses without M-mode traps"); + ("-with-dtc", + Arg.String PI.set_dtc, + " full path to dtc to use") ]) let usage_msg = "RISC-V platform options:" @@ -87,11 +90,7 @@ let elf_arg = | _ -> (prerr_endline "Please provide an ELF file."; exit 0) ) -let () = - Random.self_init (); - - let pc = Platform.init elf_arg in - +let run pc = sail_call (fun r -> try ( zinit_platform (); (* devices *) @@ -105,3 +104,22 @@ let () = | ZError_internal_error (_) -> prerr_endline "Error: internal error" ) + +let show_times init_s init_e run_e insts = + let init_time = init_e.Unix.tms_utime -. init_s.Unix.tms_utime in + let exec_time = run_e.Unix.tms_utime -. init_e.Unix.tms_utime in + Printf.eprintf "\nInitialization: %g secs\n" init_time; + Printf.eprintf "Execution: %g secs\n" exec_time; + Printf.eprintf "Instructions retired: %Ld\n" insts; + Printf.eprintf "Perf: %g ips\n" ((Int64.to_float insts) /. exec_time) + +let () = + Random.self_init (); + + let init_start = Unix.times () in + let pc = Platform.init elf_arg in + let init_end = Unix.times () in + let _ = run pc in + let run_end = Unix.times () in + let insts = Big_int.to_int64 (uint (!Riscv.zminstret)) in + show_times init_start init_end run_end insts diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 412dcfc7..6eeda601 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -217,7 +217,7 @@ function cast_unit_vec b = match b { bitone => 0b1 } -val print = "prerr_endline" : string -> unit +val print = "print_endline" : string -> unit val putchar = "putchar" : forall ('a : Type). 'a -> unit @@ -355,22 +355,46 @@ overload min = {min_nat, min_int} overload max = {max_nat, max_int} val __WriteRAM = "write_ram" : forall 'n 'm. - (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> unit effect {wmv} + (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} val __RISCV_write : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> bool effect {wmv} function __RISCV_write (addr, width, data) = { - __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data); - true + __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data) } val __TraceMemoryWrite : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit -val __ReadRAM = "read_ram" : forall 'n 'm. +val __ReadRAM = { lem: "MEMr", _ : "read_ram" } : forall 'n 'm. (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} -val __RISCV_read : forall 'n. (bits(64), atom('n)) -> option(bits(8 * 'n)) effect {rmem} -function __RISCV_read (addr, width) = Some(__ReadRAM(64, width, 0x0000_0000_0000_0000, addr)) +val __ReadRAM_acquire = { lem: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm. + (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. + (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} + +val __ReadRAM_reserved = { lem: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm. + (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. + (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. + (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} + +val __RISCV_read : forall 'n. (bits(64), 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(64, width, 0x0000_0000_0000_0000, addr)), + (true, false, false) => Some(__ReadRAM_acquire(64, width, 0x0000_0000_0000_0000, addr)), + (true, true, false) => Some(__ReadRAM_strong_acquire(64, width, 0x0000_0000_0000_0000, addr)), + (false, false, true) => Some(__ReadRAM_reserved(64, width, 0x0000_0000_0000_0000, addr)), + (true, false, true) => Some(__ReadRAM_reserved_acquire(64, width, 0x0000_0000_0000_0000, addr)), + (true, true, true) => Some(__ReadRAM_reserved_strong_acquire(64, width, 0x0000_0000_0000_0000, addr)), + (false, true, false) => None(), + (false, true, true) => None() + } val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit @@ -402,9 +426,9 @@ val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0. val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) -val print_int = "prerr_int" : (string, int) -> unit -val print_bits = "prerr_bits" : forall 'n. (string, bits('n)) -> unit -val print_string = "prerr_string" : (string, 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 "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) diff --git a/riscv/riscv.sail b/riscv/riscv.sail index 87f1b7ca..f81de3e9 100644 --- a/riscv/riscv.sail +++ b/riscv/riscv.sail @@ -1,3 +1,8 @@ +/* Instruction definitions. + * + * This includes decoding, execution, and assembly parsing and printing. + */ + scattered union ast val decode : bits(32) -> option(ast) effect pure @@ -28,28 +33,23 @@ mapping encdec_uop : uop <-> bits(7) = { mapping clause encdec = UTYPE(imm, rd, op) <-> imm @ rd @ encdec_uop(op) -function clause execute UTYPE(imm, rd, op) = - let off : xlenbits = EXTS(imm @ 0x000) in - let ret : xlenbits = match op { - RISCV_LUI => off, - RISCV_AUIPC => PC + off - } in { - X(rd) = ret; - true - } - -function clause print_insn UTYPE(imm, rd, op) = - match (op) { - RISCV_LUI => "lui " ^ rd ^ ", " ^ BitStr(imm), - RISCV_AUIPC => "auipc " ^ rd ^ ", " ^ BitStr(imm) - } +function clause execute UTYPE(imm, rd, op) = { + let off : xlenbits = EXTS(imm @ 0x000); + let ret : xlenbits = match op { + RISCV_LUI => off, + RISCV_AUIPC => PC + off + }; + X(rd) = ret; + true +} mapping utype_mnemonic : uop <-> string = { RISCV_LUI <-> "lui", RISCV_AUIPC <-> "auipc" } -mapping clause assembly = UTYPE(imm, rd, op) <-> utype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_20(imm) +mapping clause assembly = UTYPE(imm, rd, op) + <-> utype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_20(imm) /* ****************************************************************** */ union clause ast = RISCV_JAL : (bits(21), regbits) @@ -70,16 +70,13 @@ but this is difficult */ function clause execute (RISCV_JAL(imm, rd)) = { - let pc : xlenbits = PC; - X(rd) = nextPC; /* compatible with JAL and C.JAL */ - let offset : xlenbits = EXTS(imm); - nextPC = pc + offset; - true + let pc : xlenbits = PC; + X(rd) = nextPC; /* compatible with JAL and C.JAL */ + let offset : xlenbits = EXTS(imm); + nextPC = pc + offset; + true } -function clause print_insn (RISCV_JAL(imm, rd)) = - "jal " ^ rd ^ ", " ^ BitStr(imm) - /* TODO: handle 2-byte-alignment in mappings */ mapping clause assembly = RISCV_JAL(imm, rd) <-> "jal" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_21(imm) @@ -90,26 +87,32 @@ union clause ast = RISCV_JALR : (bits(12), regbits, regbits) mapping clause encdec = RISCV_JALR(imm, rs1, rd) <-> imm @ rs1 @ 0b000 @ rd @ 0b1100111 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; - true + /* 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); +/* RMEM FIXME: For the sequential model, the above definition doesn't work directly + if rs1 = rd. We would effectively have to keep a regfile for reads and another for + writes, and swap on instruction fetch. This could perhaps be optimized in + some manner, but for now, we just reorder the previous two lines to improve simulator + performance in the sequential model, as below: + let newPC : xlenbits = X(rs1) + EXTS(imm); + X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */ +*/ + nextPC = newPC[63..1] @ 0b0; + true } -function clause print_insn (RISCV_JALR(imm, rs1, rd)) = - "jalr " ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(imm) - -mapping clause assembly = RISCV_JALR(imm, rs1, rd) <-> "jalr" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm) +mapping clause assembly = RISCV_JALR(imm, rs1, rd) + <-> "jalr" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm) /* ****************************************************************** */ union clause ast = BTYPE : (bits(13), regbits, regbits, bop) mapping encdec_bop : bop <-> bits(3) = { - RISCV_BEQ <-> 0b000, - RISCV_BNE <-> 0b001, - RISCV_BLT <-> 0b100, - RISCV_BGE <-> 0b101, + RISCV_BEQ <-> 0b000, + RISCV_BNE <-> 0b001, + RISCV_BLT <-> 0b100, + RISCV_BGE <-> 0b101, RISCV_BLTU <-> 0b110, RISCV_BGEU <-> 0b111 } @@ -117,9 +120,9 @@ mapping encdec_bop : bop <-> bits(3) = { mapping clause encdec = BTYPE(imm7_6 @ imm5_0 @ imm7_5_0 @ imm5_4_1 @ 0b0, rs2, rs1, op) <-> imm7_6 : bits(1) @ imm7_5_0 : bits(6) @ rs2 @ rs1 @ encdec_bop(op) @ imm5_4_1 : bits(4) @ imm5_0 : bits(1) @ 0b1100011 -function clause execute (BTYPE(imm, rs2, rs1, op)) = - let rs1_val = X(rs1) in - let rs2_val = X(rs2) in +function clause execute (BTYPE(imm, rs2, rs1, op)) = { + let rs1_val = X(rs1); + let rs2_val = X(rs2); let taken : bool = match op { RISCV_BEQ => rs1_val == rs2_val, RISCV_BNE => rs1_val != rs2_val, @@ -127,22 +130,10 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = RISCV_BGE => rs1_val >=_s rs2_val, RISCV_BLTU => rs1_val <_u rs2_val, RISCV_BGEU => rs1_val >=_u rs2_val - } in { - if taken then nextPC = PC + EXTS(imm); - true - } - -function clause print_insn (BTYPE(imm, rs2, rs1, op)) = - let insn : string = - match (op) { - RISCV_BEQ => "beq ", - RISCV_BNE => "bne ", - RISCV_BLT => "blt ", - RISCV_BGE => "bge ", - RISCV_BLTU => "bltu ", - RISCV_BGEU => "bgeu " - } in - insn ^ rs1 ^ ", " ^ rs2 ^ ", " ^ BitStr(imm) + }; + if taken then nextPC = PC + EXTS(imm); + true +} mapping btype_mnemonic : bop <-> string = { RISCV_BEQ <-> "beq", @@ -153,8 +144,8 @@ mapping btype_mnemonic : bop <-> string = { RISCV_BGEU <-> "bgeu" } -mapping clause assembly = BTYPE(imm, rs2, rs1, op) <-> btype_mnemonic(op) ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_13(imm) - +mapping clause assembly = BTYPE(imm, rs2, rs1, op) + <-> btype_mnemonic(op) ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_13(imm) /* ****************************************************************** */ union clause ast = ITYPE : (bits(12), regbits, regbits, iop) @@ -170,9 +161,9 @@ mapping encdec_iop : iop <-> bits(3) = { mapping clause encdec = ITYPE(imm, rs1, rd, op) <-> imm @ rs1 @ encdec_iop(op) @ rd @ 0b0010011 -function clause execute (ITYPE (imm, rs1, rd, op)) = - let rs1_val = X(rs1) in - let immext : xlenbits = EXTS(imm) in +function clause execute (ITYPE (imm, rs1, rd, op)) = { + let rs1_val = X(rs1); + let immext : xlenbits = EXTS(imm); let result : xlenbits = match op { RISCV_ADDI => rs1_val + immext, RISCV_SLTI => EXTZ(rs1_val <_s immext), @@ -180,22 +171,10 @@ function clause execute (ITYPE (imm, rs1, rd, op)) = RISCV_XORI => rs1_val ^ immext, RISCV_ORI => rs1_val | immext, RISCV_ANDI => rs1_val & immext - } in { - X(rd) = result; - true - } - -function clause print_insn (ITYPE(imm, rs1, rd, op)) = - let insn : string = - match (op) { - RISCV_ADDI => "addi ", - RISCV_SLTI => "slti ", - RISCV_SLTIU => "sltiu ", - RISCV_XORI => "xori ", - RISCV_ORI => "ori ", - RISCV_ANDI => "andi " - } in - insn ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(imm) + }; + X(rd) = result; + true +} mapping itype_mnemonic : iop <-> string = { RISCV_ADDI <-> "addi", @@ -206,7 +185,8 @@ mapping itype_mnemonic : iop <-> string = { RISCV_ANDI <-> "andi" } -mapping clause assembly = ITYPE(imm, rs1, rd, op) <-> itype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm) +mapping clause assembly = ITYPE(imm, rs1, rd, op) + <-> itype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm) /* ****************************************************************** */ union clause ast = SHIFTIOP : (bits(6), regbits, regbits, sop) @@ -221,25 +201,16 @@ mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SLLI) <-> 0b000000 @ sham 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 -function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = - let rs1_val = X(rs1) in - let result : xlenbits = match op { - RISCV_SLLI => rs1_val << shamt, - RISCV_SRLI => rs1_val >> shamt, - RISCV_SRAI => shift_right_arith64(rs1_val, shamt) - } in { - X(rd) = result; - true - } - -function clause print_insn (SHIFTIOP(shamt, rs1, rd, op)) = - let insn : string = - match (op) { - RISCV_SLLI => "slli ", - RISCV_SRLI => "srli ", - RISCV_SRAI => "srai " - } in - insn ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(shamt) +function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = { + let rs1_val = X(rs1); + let result : xlenbits = match op { + RISCV_SLLI => rs1_val << shamt, + RISCV_SRLI => rs1_val >> shamt, + RISCV_SRAI => shift_right_arith64(rs1_val, shamt) + }; + X(rd) = result; + true +} mapping shiftiop_mnemonic : sop <-> string = { RISCV_SLLI <-> "slli", @@ -247,7 +218,8 @@ mapping shiftiop_mnemonic : sop <-> string = { RISCV_SRAI <-> "srai" } -mapping clause assembly = SHIFTIOP(shamt, rs1, rd, op) <-> shiftiop_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ hex_bits_6(shamt) +mapping clause assembly = SHIFTIOP(shamt, rs1, rd, op) + <-> shiftiop_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ hex_bits_6(shamt) /* ****************************************************************** */ union clause ast = RTYPE : (regbits, regbits, regbits, rop) @@ -263,9 +235,9 @@ mapping clause encdec = RTYPE(rs2, rs1, rd, RISCV_SRA) <-> 0b0100000 @ rs2 @ rs mapping clause encdec = RTYPE(rs2, rs1, rd, RISCV_OR) <-> 0b0000000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0110011 mapping clause encdec = RTYPE(rs2, rs1, rd, RISCV_AND) <-> 0b0000000 @ rs2 @ rs1 @ 0b111 @ rd @ 0b0110011 -function clause execute (RTYPE(rs2, rs1, rd, op)) = - let rs1_val = X(rs1) in - let rs2_val = X(rs2) in +function clause execute (RTYPE(rs2, rs1, rd, op)) = { + let rs1_val = X(rs1); + let rs2_val = X(rs2); let result : xlenbits = match op { RISCV_ADD => rs1_val + rs2_val, RISCV_SUB => rs1_val - rs2_val, @@ -277,26 +249,10 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) = RISCV_SRA => shift_right_arith64(rs1_val, rs2_val[5..0]), RISCV_OR => rs1_val | rs2_val, RISCV_AND => rs1_val & rs2_val - } in { - X(rd) = result; - true - } - -function clause print_insn (RTYPE(rs2, rs1, rd, op)) = - let insn : string = - match (op) { - RISCV_ADD => "add ", - RISCV_SUB => "sub ", - RISCV_SLL => "sll ", - RISCV_SLT => "slt ", - RISCV_SLTU => "sltu ", - RISCV_XOR => "xor ", - RISCV_SRL => "srl ", - RISCV_SRA => "sra ", - RISCV_OR => "or ", - RISCV_AND => "and " - } in - insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2 + }; + X(rd) = result; + true +} mapping rtype_mnemonic : rop <-> string = { RISCV_ADD <-> "add", @@ -311,14 +267,16 @@ mapping rtype_mnemonic : rop <-> string = { RISCV_AND <-> "and" } -mapping clause assembly = RTYPE(rs2, rs1, rd, op) <-> rtype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) +mapping clause assembly = RTYPE(rs2, rs1, rd, op) + <-> rtype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) /* ****************************************************************** */ union clause ast = LOAD : (bits(12), regbits, regbits, bool, word_width, bool, bool) /* I am assuming that load unsigned double wasn't meant to be missing here? */ /* TODO: aq/rl */ -mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_bits(size) @ rd @ 0b0000011 +mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) + <-> imm @ rs1 @ bool_bits(is_unsigned) @ size_bits(size) @ rd @ 0b0000011 val extend_value : forall 'n, 0 < 'n <= 8. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits) function extend_value(is_unsigned, value) = match (value) { @@ -328,13 +286,13 @@ function extend_value(is_unsigned, value) = match (value) { val process_load : forall 'n, 0 < 'n <= 8. (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)) { + match extend_value(is_unsigned, value) { MemValue(result) => { X(rd) = result; true }, MemException(e) => { handle_mem_exception(addr, e); false } } function check_misaligned(vaddr : xlenbits, width : word_width) -> bool = - if plat_enable_misaligned_access() then false + if plat_enable_misaligned_access() then false else match width { BYTE => false, HALF => vaddr[0] == true, @@ -343,34 +301,19 @@ function check_misaligned(vaddr : xlenbits, width : word_width) -> bool = } function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = - let vaddr : xlenbits = X(rs1) + EXTS(imm) in - if check_misaligned(vaddr, width) - 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 { - BYTE => process_load(rd, vaddr, mem_read(addr, 1, aq, rl, false), is_unsigned), - HALF => process_load(rd, vaddr, mem_read(addr, 2, aq, rl, false), is_unsigned), - WORD => process_load(rd, vaddr, mem_read(addr, 4, aq, rl, false), is_unsigned), - DOUBLE => process_load(rd, vaddr, mem_read(addr, 8, aq, rl, false), is_unsigned) - } - } - -/* FIXME: aq/rl are getting dropped */ -function clause print_insn (LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = - let insn : string = - match (width, is_unsigned) { - (BYTE, false) => "lb ", - (BYTE, true) => "lbu ", - (HALF, false) => "lh ", - (HALF, true) => "lhu ", - (WORD, false) => "lw ", - (WORD, true) => "lwu ", - (DOUBLE, false) => "ld ", - (DOUBLE, true) => "ldu " - } in - insn ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(imm) + let vaddr : xlenbits = X(rs1) + EXTS(imm) in + if check_misaligned(vaddr, width) + 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 { + BYTE => process_load(rd, vaddr, mem_read(addr, 1, aq, rl, false), is_unsigned), + HALF => process_load(rd, vaddr, mem_read(addr, 2, aq, rl, false), is_unsigned), + WORD => process_load(rd, vaddr, mem_read(addr, 4, aq, rl, false), is_unsigned), + DOUBLE => process_load(rd, vaddr, mem_read(addr, 8, aq, rl, false), is_unsigned) + } + } /* TODO FIXME: is this the actual aq/rl syntax? */ val maybe_aq : bool <-> string @@ -392,59 +335,53 @@ mapping maybe_u = { } -mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned, size, aq, rl) <-> "l" ^ size_mnemonic(size) ^ maybe_u(is_unsigned) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm) +mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned, size, aq, rl) + <-> "l" ^ size_mnemonic(size) ^ maybe_u(is_unsigned) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm) /* ****************************************************************** */ union clause ast = STORE : (bits(12), regbits, regbits, word_width, bool, bool) /* TODO: aq/rl */ -mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false) <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ imm5 : bits(5) @ 0b0100011 +mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false) + <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ imm5 : bits(5) @ 0b0100011 /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = - let vaddr : xlenbits = X(rs1) + EXTS(imm) in - if check_misaligned(vaddr, width) - then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); false } - else match translateAddr(vaddr, Write, Data) { - TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, - TR_Address(addr) => - let eares : MemoryOpResult(unit) = match width { - BYTE => mem_write_ea(addr, 1, aq, rl, false), - HALF => mem_write_ea(addr, 2, aq, rl, false), - WORD => mem_write_ea(addr, 4, aq, rl, false), - DOUBLE => mem_write_ea(addr, 8, aq, rl, false) - } in - match (eares) { - MemException(e) => { handle_mem_exception(addr, e); false }, - MemValue(_) => { - let rs2_val = X(rs2) in - let res : MemoryOpResult(unit) = 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) - } in - match (res) { - MemValue(_) => true, - MemException(e) => { handle_mem_exception(addr, e); false } - } + let vaddr : xlenbits = X(rs1) + EXTS(imm) in + if check_misaligned(vaddr, width) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); false } + else match translateAddr(vaddr, Write, Data) { + TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, + TR_Address(addr) => { + let eares : MemoryOpResult(unit) = match width { + BYTE => mem_write_ea(addr, 1, aq, rl, false), + HALF => mem_write_ea(addr, 2, aq, rl, false), + WORD => mem_write_ea(addr, 4, aq, rl, false), + DOUBLE => mem_write_ea(addr, 8, aq, rl, false) + }; + match (eares) { + 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) + }; + match (res) { + MemValue(true) => true, + MemValue(false) => internal_error("store got false from mem_write_value"), + MemException(e) => { handle_mem_exception(addr, e); false } } } + } } + } -/* FIXME: aq/rl are getting dropped */ -function clause print_insn (STORE(imm, rs2, rs1, width, aq, rl)) = - let insn : string = - match (width) { - BYTE => "sb ", - HALF => "sh ", - WORD => "sw ", - DOUBLE => "sd " - } in - insn ^ rs2 ^ ", " ^ rs1 ^ ", " ^ BitStr(imm) - -mapping clause assembly = STORE(imm, rs1, rd, size, aq, rl) <-> "s" ^ size_mnemonic(size) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm) +mapping clause assembly = STORE(imm, rs1, rd, size, aq, rl) + <-> "s" ^ size_mnemonic(size) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm) /* ****************************************************************** */ @@ -458,8 +395,6 @@ function clause execute (ADDIW(imm, rs1, rd)) = { true } -function clause print_insn (ADDIW(imm, rs1, rd)) = - "addiw " ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(imm) mapping clause assembly = ADDIW(imm, rs1, rd) <-> "addiw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm) @@ -470,25 +405,16 @@ mapping clause encdec = SHIFTW(shamt, rs1, rd, RISCV_SLLI) <-> 0b0000000 @ shamt 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 -function clause execute (SHIFTW(shamt, rs1, rd, op)) = - let rs1_val = (X(rs1))[31..0] in - let result : bits(32) = match op { - RISCV_SLLI => rs1_val << shamt, - RISCV_SRLI => rs1_val >> shamt, - RISCV_SRAI => shift_right_arith32(rs1_val, shamt) - } in { - X(rd) = EXTS(result); - true - } - -function clause print_insn (SHIFTW(shamt, rs1, rd, op)) = - let insn : string = - match (op) { - RISCV_SLLI => "slli ", - RISCV_SRLI => "srli ", - RISCV_SRAI => "srai " - } in - insn ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(shamt) +function clause execute (SHIFTW(shamt, rs1, rd, op)) = { + let rs1_val = (X(rs1))[31..0]; + let result : bits(32) = match op { + RISCV_SLLI => rs1_val << shamt, + RISCV_SRLI => rs1_val >> shamt, + RISCV_SRAI => shift_right_arith32(rs1_val, shamt) + }; + X(rd) = EXTS(result); + true +} mapping shiftw_mnemonic : sop <-> string = { RISCV_SLLI <-> "slli", @@ -496,7 +422,8 @@ mapping shiftw_mnemonic : sop <-> string = { RISCV_SRAI <-> "srai" } -mapping clause assembly = SHIFTW(shamt, rs1, rd, op) <-> shiftw_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_5(shamt) +mapping clause assembly = SHIFTW(shamt, rs1, rd, op) + <-> shiftw_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_5(shamt) /* ****************************************************************** */ union clause ast = RTYPEW : (regbits, regbits, regbits, ropw) @@ -507,30 +434,19 @@ mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SLLW) <-> 0b0000000 @ rs2 @ r 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 -function clause execute (RTYPEW(rs2, rs1, rd, op)) = - let rs1_val = (X(rs1))[31..0] in - let rs2_val = (X(rs2))[31..0] in +function clause execute (RTYPEW(rs2, rs1, rd, op)) = { + let rs1_val = (X(rs1))[31..0]; + let rs2_val = (X(rs2))[31..0]; let result : bits(32) = match op { RISCV_ADDW => rs1_val + rs2_val, RISCV_SUBW => rs1_val - rs2_val, RISCV_SLLW => rs1_val << (rs2_val[4..0]), RISCV_SRLW => rs1_val >> (rs2_val[4..0]), RISCV_SRAW => shift_right_arith32(rs1_val, rs2_val[4..0]) - } in { - X(rd) = EXTS(result); - true - } - -function clause print_insn (RTYPEW(rs2, rs1, rd, op)) = - let insn : string = - match (op) { - RISCV_ADDW => "addw ", - RISCV_SUBW => "subw ", - RISCV_SLLW => "sllw ", - RISCV_SRLW => "srlw ", - RISCV_SRAW => "sraw " - } in - insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2 + }; + X(rd) = EXTS(result); + true +} mapping rtypew_mnemonic : ropw <-> string = { RISCV_ADDW <-> "addw", @@ -540,7 +456,8 @@ mapping rtypew_mnemonic : ropw <-> string = { RISCV_SRAW <-> "sraw" } -mapping clause assembly = RTYPEW(rs2, rs1, rd, op) <-> rtypew_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) +mapping clause assembly = RTYPEW(rs2, rs1, rd, op) + <-> rtypew_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) /* ****************************************************************** */ /* FIXME: separate these out into separate ast variants */ @@ -554,28 +471,19 @@ mapping encdec_mul_op : (bool, bool, bool) <-> bits(3) = { } /* for some reason the : bits(3) here is still necessary - BUG */ -mapping clause encdec = MUL(rs2, rs1, rd, high, signed1, signed2) <-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(high, signed1, signed2) : bits(3) @ rd @ 0b0110011 - -function clause execute (MUL(rs2, rs1, rd, high, signed1, signed2)) = - let rs1_val = X(rs1) in - let rs2_val = X(rs2) in - let rs1_int : int = if signed1 then signed(rs1_val) else unsigned(rs1_val) in - let rs2_int : int = if signed2 then signed(rs2_val) else unsigned(rs2_val) in - let result128 = to_bits(128, rs1_int * rs2_int) in - let result = if high then result128[127..64] else result128[63..0] in { - X(rd) = result; - true - } - -function clause print_insn (MUL(rs2, rs1, rd, high, signed1, signed2)) = - let insn : string = - match (high, signed1, signed2) { - (false, true, true) => "mul ", - (true, true, true) => "mulh ", - (true, true, false) => "mulhsu ", - (true, false, false) => "mulhu" - } in - insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2 +mapping clause encdec = MUL(rs2, rs1, rd, high, signed1, signed2) + <-> 0b0000001 @ rs2 @ rs1 @ encdec_mul_op(high, signed1, signed2) : bits(3) @ rd @ 0b0110011 + +function clause execute (MUL(rs2, rs1, rd, high, signed1, signed2)) = { + let rs1_val = X(rs1); + 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]; + X(rd) = result; + true +} mapping mul_mnemonic : (bool, bool, bool) <-> string = { (false, true, true) <-> "mul", @@ -591,47 +499,40 @@ union clause ast = DIV : (regbits, regbits, regbits, bool) mapping clause encdec = DIV(rs2, rs1, rd, s) <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0110011 -function clause execute (DIV(rs2, rs1, rd, s)) = - let rs1_val = X(rs1) in - let rs2_val = X(rs2) in - let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val) in - let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val) in - let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int) in - let q': int = if s & q > xlen_max_signed then xlen_min_signed else q in /* check for signed overflow */ { - X(rd) = to_bits(xlen, q'); - true - } - -function clause print_insn (DIV(rs2, rs1, rd, s)) = - let insn : string = if s then "div " else "divu " in - insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2 +function clause execute (DIV(rs2, rs1, rd, s)) = { + let rs1_val = X(rs1); + let rs2_val = X(rs2); + let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val); + let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val); + let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int); + let q': int = if s & q > xlen_max_signed then xlen_min_signed else q; /* check for signed overflow */ + X(rd) = to_bits(xlen, q'); + true +} mapping maybe_not_u : bool <-> string = { false <-> "u", - true <-> "" + true <-> "" } -mapping clause assembly = DIV(rs2, rs1, rd, s) <-> "div" ^ maybe_not_u(s) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) +mapping clause assembly = DIV(rs2, rs1, rd, s) + <-> "div" ^ maybe_not_u(s) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) /* ****************************************************************** */ union clause ast = REM : (regbits, regbits, regbits, bool) mapping clause encdec = REM(rs2, rs1, rd, s) <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0110011 -function clause execute (REM(rs2, rs1, rd, s)) = - let rs1_val = X(rs1) in - let rs2_val = X(rs2) in - let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val) in - let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val) in - let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int) in { +function clause execute (REM(rs2, rs1, rd, s)) = { + let rs1_val = X(rs1); + let rs2_val = X(rs2); + let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val); + 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); - true - } - -function clause print_insn (REM(rs2, rs1, rd, s)) = - let insn : string = if s then "rem " else "remu " in - insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2 + X(rd) = to_bits(xlen, r); + true +} mapping clause assembly = REM(rs2, rs1, rd, s) <-> "rem" ^ maybe_not_u(s) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) @@ -640,63 +541,54 @@ union clause ast = MULW : (regbits, regbits, regbits) mapping clause encdec = MULW(rs2, rs1, rd) <-> 0b0000001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 -function clause execute (MULW(rs2, rs1, rd)) = - let rs1_val = X(rs1)[31..0] in - let rs2_val = X(rs2)[31..0] in - let rs1_int : int = signed(rs1_val) in - let rs2_int : int = signed(rs2_val) in - let result32 = to_bits(64, rs1_int * rs2_int)[31..0] in /* XXX surprising behaviour of to_bits requires exapnsion to 64 bits followed by truncation... */ - let result : xlenbits = EXTS(result32) in { - X(rd) = result; - true - } - -function clause print_insn (MULW(rs2, rs1, rd)) = - "mulw " ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2 +function clause execute (MULW(rs2, rs1, rd)) = { + let rs1_val = X(rs1)[31..0]; + let rs2_val = X(rs2)[31..0]; + let rs1_int : int = signed(rs1_val); + let rs2_int : int = signed(rs2_val); + let result32 = to_bits(64, rs1_int * rs2_int)[31..0]; /* XXX surprising behaviour of to_bits requires expansion to 64 bits followed by truncation... */ + let result : xlenbits = EXTS(result32); + X(rd) = result; + true +} -mapping clause assembly = MULW(rs2, rs1, rd) <-> "mulw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) +mapping clause assembly = MULW(rs2, rs1, rd) + <-> "mulw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) /* ****************************************************************** */ union clause ast = DIVW : (regbits, regbits, regbits, bool) mapping clause encdec = DIVW(rs2, rs1, rd, s) <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0111011 -function clause execute (DIVW(rs2, rs1, rd, s)) = - let rs1_val = X(rs1)[31..0] in - let rs2_val = X(rs2)[31..0] in - let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val) in - let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val) in - let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int) in - let q': int = if s & q > (2 ^ 31 - 1) then (0 - 2^31) else q in /* check for signed overflow */ { - X(rd) = EXTS(to_bits(32, q')); - true - } - -function clause print_insn (DIVW(rs2, rs1, rd, s)) = - let insn : string = if s then "divw " else "divuw " in - insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2 +function clause execute (DIVW(rs2, rs1, rd, s)) = { + let rs1_val = X(rs1)[31..0]; + let rs2_val = X(rs2)[31..0]; + let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val); + let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val); + let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int); + let q': int = if s & q > (2 ^ 31 - 1) then (0 - 2^31) else q; /* check for signed overflow */ + X(rd) = EXTS(to_bits(32, q')); + true +} -mapping clause assembly = DIVW(rs2, rs1, rd, s) <-> "div" ^ maybe_not_u(s) ^ "w" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) +mapping clause assembly = DIVW(rs2, rs1, rd, s) + <-> "div" ^ maybe_not_u(s) ^ "w" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) /* ****************************************************************** */ union clause ast = REMW : (regbits, regbits, regbits, bool) mapping clause encdec = REMW(rs2, rs1, rd, s) <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0111011 -function clause execute (REMW(rs2, rs1, rd, s)) = - let rs1_val = X(rs1)[31..0] in - let rs2_val = X(rs2)[31..0] in - let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val) in - let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val) in - let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int) in { - /* signed overflow case returns zero naturally as required due to -1 divisor */ - X(rd) = EXTS(to_bits(32, r)); - true - } - -function clause print_insn (REMW(rs2, rs1, rd, s)) = - let insn : string = if s then "remw " else "remuw " in - insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2 +function clause execute (REMW(rs2, rs1, rd, s)) = { + let rs1_val = X(rs1)[31..0]; + let rs2_val = X(rs2)[31..0]; + let rs1_int : int = if s then signed(rs1_val) else unsigned(rs1_val); + 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) = EXTS(to_bits(32, r)); + true +} mapping clause assembly = REMW(rs2, rs1, rd, s) <-> "rem" ^ maybe_not_u(s) ^ "w" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) @@ -707,19 +599,17 @@ mapping clause encdec = FENCE(pred, succ) <-> 0b0000 @ pred @ succ @ 0b00000 @ 0 function clause execute (FENCE(pred, succ)) = { match (pred, succ) { - (0b0011, 0b0011) => MEM_fence_rw_rw(), - (0b0010, 0b0011) => MEM_fence_r_rw(), - (0b0010, 0b0010) => MEM_fence_r_r(), - (0b0011, 0b0001) => MEM_fence_rw_w(), - (0b0001, 0b0001) => MEM_fence_w_w(), - - (0b1111, 0b1111) => MEM_fence_rw_rw(), - (0b1110, 0b1111) => MEM_fence_r_rw(), - (0b1110, 0b1110) => MEM_fence_r_r(), - (0b1111, 0b1101) => MEM_fence_rw_w(), - (0b1101, 0b1101) => MEM_fence_w_w(), - - (0b0000, 0b0000) => (), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => MEM_fence_rw_rw(), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => MEM_fence_r_rw(), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => MEM_fence_r_r(), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => MEM_fence_rw_w(), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => MEM_fence_w_w(), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => MEM_fence_w_rw(), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => MEM_fence_rw_r(), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => MEM_fence_r_w(), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => MEM_fence_w_r(), + + (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (), _ => { print("FIXME: unsupported fence"); () } @@ -727,10 +617,6 @@ function clause execute (FENCE(pred, succ)) = { true } -/* FIXME */ -function clause print_insn (FENCE(pred, succ)) = - "fence" - mapping bit_maybe_r : bits(1) <-> string = { 0b1 <-> "r", 0b0 <-> "" @@ -762,10 +648,9 @@ union clause ast = FENCEI : unit mapping clause encdec = FENCEI() <-> 0b000000000000 @ 0b00000 @ 0b001 @ 0b00000 @ 0b0001111 -function clause execute FENCEI() = { MEM_fence_i(); true } +/* fence.i is a nop for the memory model */ +function clause execute FENCEI() = { /* MEM_fence_i(); */ true } -function clause print_insn (FENCEI()) = - "fence.i" mapping clause assembly = FENCEI() <-> "fence.i" @@ -774,20 +659,17 @@ union clause ast = ECALL : unit mapping clause encdec = ECALL() <-> 0b000000000000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 -function clause execute ECALL() = +function clause execute ECALL() = { let t : sync_exception = struct { trap = match (cur_privilege) { - User => E_U_EnvCall, + User => E_U_EnvCall, Supervisor => E_S_EnvCall, - Machine => E_M_EnvCall + Machine => E_M_EnvCall }, - excinfo = (None() : option(xlenbits)) } in { - nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC); - false - } - -function clause print_insn (ECALL()) = - "ecall" + excinfo = (None() : option(xlenbits)) }; + nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC); + false +} mapping clause assembly = ECALL() <-> "ecall" @@ -797,16 +679,12 @@ union clause ast = MRET : unit mapping clause encdec = MRET() <-> 0b0011000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 function clause execute MRET() = { - if cur_privilege == Machine then - nextPC = handle_exception(cur_privilege, CTL_MRET(), PC) - else - handle_illegal(); + if cur_privilege == Machine + then nextPC = handle_exception(cur_privilege, CTL_MRET(), PC) + else handle_illegal(); false } -function clause print_insn (MRET()) = - "mret" - mapping clause assembly = MRET() <-> "mret" /* ****************************************************************** */ @@ -817,7 +695,7 @@ mapping clause encdec = SRET() <-> 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b000 function clause execute SRET() = { match cur_privilege { User => handle_illegal(), - Supervisor => if mstatus.TSR() == true + Supervisor => if mstatus.TSR() == true then handle_illegal() else nextPC = handle_exception(cur_privilege, CTL_SRET(), PC), Machine => nextPC = handle_exception(cur_privilege, CTL_SRET(), PC) @@ -825,9 +703,6 @@ function clause execute SRET() = { false } -function clause print_insn (SRET()) = - "sret" - mapping clause assembly = SRET() <-> "sret" /* ****************************************************************** */ @@ -840,9 +715,6 @@ function clause execute EBREAK() = { false } -function clause print_insn (EBREAK()) = - "ebreak" - mapping clause assembly = EBREAK() <-> "ebreak" /* ****************************************************************** */ @@ -853,15 +725,12 @@ mapping clause encdec = WFI() <-> 0b000100000101 @ 0b00000 @ 0b000 @ 0b00000 @ 0 function clause execute WFI() = match cur_privilege { Machine => true, - Supervisor => if mstatus.TW() == true + Supervisor => if mstatus.TW() == true then { handle_illegal(); false } else true, User => { handle_illegal(); false } } -function clause print_insn (WFI()) = - "wfi" - mapping clause assembly = WFI() <-> "wfi" /* ****************************************************************** */ @@ -870,10 +739,9 @@ union clause ast = SFENCE_VMA : (regbits, regbits) mapping clause encdec = SFENCE_VMA(rs1, rs2) <-> 0b0001001 @ rs2 @ rs1 @ 0b000 @ 0b00000 @ 0b1110011 function clause execute SFENCE_VMA(rs1, rs2) = { - /* FIXME: spec leaves unspecified what happens if this is executed in M-mode. - We assume it is the same as S-mode, which is definitely wrong. - */ - if cur_privilege == User then { handle_illegal(); false } + /* 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) => { @@ -886,75 +754,132 @@ function clause execute SFENCE_VMA(rs1, rs2) = { } } -function clause print_insn (SFENCE_VMA(rs1, rs2)) = - "sfence.vma " ^ rs1 ^ ", " ^ rs2 +mapping clause assembly = SFENCE_VMA(rs1, rs2) + <-> "sfence.vma" ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) -mapping clause assembly = SFENCE_VMA(rs1, rs2) <-> "sfence.vma" ^ spc() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) +/* ****************************************************************** */ +// Some print utils for lr/sc. + +function aqrl_str(aq : bool, rl : bool) -> string = + match (aq, rl) { + (false, false) => "", + (false, true) => ".rl", + (true, false) => ".aq", + (true, true) => ".aqrl" + } + +function lrsc_width_str(width : word_width) -> string = + match (width) { + BYTE => ".b", + HALF => ".h", + WORD => ".w", + DOUBLE => ".d" + } /* ****************************************************************** */ union clause ast = LOADRES : (bool, bool, regbits, word_width, regbits) mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 -val process_loadres : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> unit +/* We could set load-reservations on physical or virtual addresses. + * For now we set them on virtual addresses, since it makes the + * sequential model of SC a bit simpler, at the cost of an explicit + * call to load_reservation in LR and cancel_reservation in SC. + */ -function clause execute(LOADRES(aq, rl, rs1, width, rd)) = - let vaddr : xlenbits = X(rs1) in - match translateAddr(vaddr, Read, Data) { - TR_Failure(e) => { handle_mem_exception(vaddr, e); false }, - TR_Address(addr) => - match width { - WORD => process_load(rd, addr, mem_read(addr, 4, aq, rl, true), false), - DOUBLE => process_load(rd, addr, mem_read(addr, 8, aq, rl, true), false), - _ => internal_error("LOADRES expected WORD or DOUBLE") - } +val process_loadres : forall 'n, 0 < 'n <= 8. (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 }, + MemException(e) => { handle_mem_exception(addr, e); false } } -/* FIXME */ -function clause print_insn (LOADRES(aq, rl, rs1, width, rd)) = - let insn : string = - match (width) { - WORD => "lr.w ", - DOUBLE => "lr.d ", - _ => "lr.bad " +function clause execute(LOADRES(aq, rl, rs1, width, rd)) = + let vaddr : xlenbits = X(rs1) in + let aligned : bool = + /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt + * to treat them as valid here; otherwise we'd need to throw an internal_error. + * May need to revisit for latex output. + */ + match width { + BYTE => true, + HALF => vaddr[0] == 0b0, + WORD => vaddr[1..0] == 0b00, + DOUBLE => vaddr[2..0] == 0b000 } in - insn ^ rd ^ ", " ^ rs1 + /* "LR faults like a normal load, even though it's in the AMO major opcode space." + - 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") + } + } -mapping clause assembly = LOADRES(aq, rl, rs1, size, rd) <-> "lr." ^ maybe_aq(aq) ^ maybe_rl(rl) ^ size_mnemonic(size) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) +mapping clause assembly = LOADRES(aq, rl, rs1, size, rd) + <-> "lr." ^ maybe_aq(aq) ^ maybe_rl(rl) ^ size_mnemonic(size) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) /* ****************************************************************** */ union clause ast = STORECON : (bool, bool, regbits, regbits, word_width, regbits) -mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 +mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) + <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111 /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { - status : bits(1) = if speculate_conditional_success() then 0b0 else 0b1; - X(rd) = EXTZ(status); - - if status == 0b1 then true else { - vaddr : xlenbits = X(rs1); - 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") - }; - match (eares) { - MemException(e) => { handle_mem_exception(addr, e); false }, - MemValue(_) => { - rs2_val = X(rs2); - let res : MemoryOpResult(unit) = 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") - } in - match (res) { - MemValue(_) => true, - MemException(e) => { handle_mem_exception(addr, e); false } + /* RMEM FIXME: This definition differs from the Sail1 version: + * rs1 is read *before* speculate_conditional_success + * (called via match_reservation), partly due to the current api of + * match_reservation. Reverting back to the weaker Sail1 version + * will require changes to the API for the ghost reservation state. + */ + vaddr : xlenbits = X(rs1); + let aligned : bool = + /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt + * to treat them as valid here; otherwise we'd need to throw an internal_error. + * May need to revisit for latex output. + */ + match width { + BYTE => true, + HALF => vaddr[0] == 0b0, + WORD => vaddr[1..0] == 0b00, + DOUBLE => vaddr[2..0] == 0b000 + } in + if (~ (aligned)) + then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); false } + else { + if match_reservation(vaddr) == false + then { X(rd) = EXTZ(0b1); 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") + }; + 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") + }; + match (res) { + MemValue(true) => { X(rd) = EXTZ(0b0); cancel_reservation(); true }, + MemValue(false) => { X(rd) = EXTZ(0b1); cancel_reservation(); true }, + MemException(e) => { handle_mem_exception(addr, e); false } + } } } } @@ -963,16 +888,6 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { } } -/* FIXME */ -function clause print_insn (STORECON(aq, rl, rs2, rs1, width, rd)) = - let insn : string = - match (width) { - WORD => "sc.w ", - DOUBLE => "sc.d ", - _ => "sc.bad " - } in - insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2 - mapping clause assembly = STORECON(aq, rl, rs2, rs1, size, rd) <-> "sc." ^ maybe_aq(aq) ^ maybe_rl(rl) ^ size_mnemonic(size) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) /* ****************************************************************** */ @@ -1013,10 +928,10 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { _ => internal_error ("AMO expected WORD or DOUBLE") }; match (rval) { - MemException(e) => { handle_mem_exception(addr, e); false }, + MemException(e) => { handle_mem_exception(addr, e); false }, MemValue(loaded) => { rs2_val : xlenbits = X(rs2); - result : xlenbits = + result : xlenbits = match op { AMOSWAP => rs2_val, AMOADD => rs2_val + loaded, @@ -1031,13 +946,14 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { AMOMAXU => vector64(max(unsigned(rs2_val), unsigned(loaded))) }; - let wval : MemoryOpResult(unit) = match width { + 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") }; match (wval) { - MemValue(_) => { X(rd) = loaded; true }, + MemValue(true) => { X(rd) = loaded; true }, + MemValue(false) => { internal_error("AMO got false from mem_write_value") }, MemException(e) => { handle_mem_exception(addr, e); false } } } @@ -1048,30 +964,6 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { } } -function clause print_insn (AMO(op, aq, rl, rs2, rs1, width, rd)) = - let insn : string = - match (op, width) { - (AMOSWAP, WORD) => "amoswap.w ", - (AMOADD , WORD) => "amoadd.w ", - (AMOXOR , WORD) => "amoxor.w ", - (AMOAND , WORD) => "amoand.w ", - (AMOOR , WORD) => "amoor.w ", - (AMOMIN , WORD) => "amomin.w ", - (AMOMAX , WORD) => "amomax.w ", - (AMOMINU, WORD) => "amominu.w ", - (AMOMAXU, WORD) => "amomaxu.w ", - (AMOSWAP, DOUBLE) => "amoswap.d ", - (AMOADD , DOUBLE) => "amoadd.d ", - (AMOXOR , DOUBLE) => "amoxor.d ", - (AMOAND , DOUBLE) => "amoand.d ", - (AMOOR , DOUBLE) => "amoor.d ", - (AMOMIN , DOUBLE) => "amomin.d ", - (AMOMAX , DOUBLE) => "amomax.d ", - (AMOMINU, DOUBLE) => "amominu.d ", - (AMOMAXU, DOUBLE) => "amomaxu.d ", - (_, _) => "amo.bad " - } in - insn ^ rd ^ ", " ^ rs1 ^ ", " ^ rs2 mapping amo_mnemonic : amoop <-> string = { AMOSWAP <-> "amoswap", @@ -1085,7 +977,8 @@ mapping amo_mnemonic : amoop <-> string = { AMOMAXU <-> "amomaxu" } -mapping clause assembly = AMO(op, aq, rl, rs2, rs1, width, rd) <-> amo_mnemonic(op) ^ "." ^ size_mnemonic(width) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) +mapping clause assembly = AMO(op, aq, rl, rs2, rs1, width, rd) + <-> amo_mnemonic(op) ^ "." ^ size_mnemonic(width) ^ maybe_aq(aq) ^ maybe_rl(rl) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) /* ****************************************************************** */ union clause ast = CSR : (bits(12), regbits, regbits, bool, csrop) @@ -1114,7 +1007,7 @@ function readCSR csr : csreg -> xlenbits = 0x305 => mtvec.bits(), 0x306 => EXTZ(mcounteren.bits()), 0x340 => mscratch, - 0x341 => mepc, + 0x341 => mepc & pc_alignment_mask(), 0x342 => mcause.bits(), 0x343 => mtval, 0x344 => mip.bits(), @@ -1130,7 +1023,7 @@ function readCSR csr : csreg -> xlenbits = 0x105 => stvec.bits(), 0x106 => EXTZ(scounteren.bits()), 0x140 => sscratch, - 0x141 => sepc, + 0x141 => sepc & pc_alignment_mask(), 0x142 => scause.bits(), 0x143 => stval, 0x144 => lower_mip(mip, mideleg).bits(), @@ -1222,18 +1115,6 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) = true } -function clause print_insn (CSR(csr, rs1, rd, is_imm, op)) = - let insn : string = - match (op, is_imm) { - (CSRRW, true) => "csrrwi ", - (CSRRW, false) => "csrrw ", - (CSRRS, true) => "csrrsi ", - (CSRRS, false) => "csrrs ", - (CSRRC, true) => "csrrci ", - (CSRRC, false) => "csrrc " - } in - let rs1_str : string = if is_imm then BitStr(rs1) else reg_name_abi(rs1) in - insn ^ rd ^ ", " ^ rs1_str ^ ", " ^ csr_name(csr) mapping maybe_i : bool <-> string = { true <-> "i", @@ -1252,10 +1133,10 @@ mapping clause assembly = CSR(csr, rs1, rd, false, op) <-> csr_mnemonic(op) ^ sp /* ****************************************************************** */ union clause ast = NOP : unit -function clause decodeCompressed (0b000 @ nzi1 : bits(1) @ 0b00000 @ (nzi0 : bits(5)) @ 0b01) : bits(16) = { - if (nzi1 == 0b0) & (nzi0 == 0b00000) then Some(NOP()) +function clause decodeCompressed (0b000 @ nzi1 : bits(1) @ 0b00000 @ (nzi0 : bits(5)) @ 0b01) : bits(16) = + if (nzi1 == 0b0) & (nzi0 == 0b00000) + then Some(NOP()) else None() -} function clause execute NOP() = true @@ -1266,17 +1147,16 @@ function clause print_insn (NOP()) = union clause ast = C_ADDI4SPN : (cregbits, bits(8)) -function clause decodeCompressed (0b000 @ nz54 : bits(2) @ nz96 : bits(4) @ nz2 : bits(1) @ nz3 : bits(1) @ rd : cregbits @ 0b00) : bits(16) = { - let nzimm = (nz96 @ nz54 @ nz3 @ nz2) : bits(8) in - if nzimm == 0b00000000 then None() +function clause decodeCompressed (0b000 @ nz54 : bits(2) @ nz96 : bits(4) @ nz2 : bits(1) @ nz3 : bits(1) @ rd : cregbits @ 0b00) : bits(16) = + let nzimm = (nz96 @ nz54 @ nz3 @ nz2) : bits(8) in + if nzimm == 0b00000000 + then None() else Some(C_ADDI4SPN(rd, nzimm)) -} -function clause execute (C_ADDI4SPN(rdc, nzimm)) = { +function clause execute (C_ADDI4SPN(rdc, nzimm)) = let imm : bits(12) = (0b00 @ nzimm @ 0b00) in let rd = creg2reg_bits(rdc) in execute(ITYPE(imm, sp, rd, RISCV_ADDI)) -} function clause print_insn (C_ADDI4SPN(rdc, nzimm)) = "c.addi4spn " ^ creg2reg_bits(rdc) ^ ", " ^ BitStr(nzimm) @@ -1284,17 +1164,15 @@ function clause print_insn (C_ADDI4SPN(rdc, nzimm)) = /* ****************************************************************** */ union clause ast = C_LW : (bits(5), cregbits, cregbits) -function clause decodeCompressed (0b010 @ ui53 : bits(3) @ rs1 : cregbits @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregbits @ 0b00) : bits(16) = { +function clause decodeCompressed (0b010 @ ui53 : bits(3) @ rs1 : cregbits @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregbits @ 0b00) : bits(16) = let uimm = (ui6 @ ui53 @ ui2) : bits(5) in Some(C_LW(uimm, rs1, rd)) -} -function clause execute (C_LW(uimm, rsc, rdc)) = { +function clause execute (C_LW(uimm, rsc, rdc)) = let imm : bits(12) = EXTZ(uimm @ 0b00) in let rd = creg2reg_bits(rdc) in let rs = creg2reg_bits(rsc) in execute(LOAD(imm, rs, rd, false, WORD, false, false)) -} function clause print_insn (C_LW(uimm, rsc, rdc)) = "c.lw " ^ creg2reg_bits(rdc) ^ ", " ^ creg2reg_bits(rsc) ^ ", " ^ BitStr(uimm) @@ -1302,17 +1180,15 @@ function clause print_insn (C_LW(uimm, rsc, rdc)) = /* ****************************************************************** */ union clause ast = C_LD : (bits(5), cregbits, cregbits) -function clause decodeCompressed (0b011 @ ui53 : bits(3) @ rs1 : cregbits @ ui76 : bits(2) @ rd : cregbits @ 0b00) : bits(16) = { +function clause decodeCompressed (0b011 @ ui53 : bits(3) @ rs1 : cregbits @ ui76 : bits(2) @ rd : cregbits @ 0b00) : bits(16) = let uimm = (ui76 @ ui53) : bits(5) in Some(C_LD(uimm, rs1, rd)) -} -function clause execute (C_LD(uimm, rsc, rdc)) = { +function clause execute (C_LD(uimm, rsc, rdc)) = let imm : bits(12) = EXTZ(uimm @ 0b000) in let rd = creg2reg_bits(rdc) in let rs = creg2reg_bits(rsc) in execute(LOAD(imm, rs, rd, false, DOUBLE, false, false)) -} function clause print_insn (C_LD(uimm, rsc, rdc)) = "c.ld " ^ creg2reg_bits(rdc) ^ ", " ^ creg2reg_bits(rsc) ^ ", " ^ BitStr(uimm) @@ -1320,17 +1196,15 @@ function clause print_insn (C_LD(uimm, rsc, rdc)) = /* ****************************************************************** */ union clause ast = C_SW : (bits(5), cregbits, cregbits) -function clause decodeCompressed (0b110 @ ui53 : bits(3) @ rs1 : cregbits @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregbits @ 0b00) : bits(16) = { +function clause decodeCompressed (0b110 @ ui53 : bits(3) @ rs1 : cregbits @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregbits @ 0b00) : bits(16) = let uimm = (ui6 @ ui53 @ ui2) : bits(5) in Some(C_SW(uimm, rs1, rs2)) -} -function clause execute (C_SW(uimm, rsc1, rsc2)) = { +function clause execute (C_SW(uimm, rsc1, rsc2)) = let imm : bits(12) = EXTZ(uimm @ 0b00) in let rs1 = creg2reg_bits(rsc1) in let rs2 = creg2reg_bits(rsc2) in execute(STORE(imm, rs2, rs1, WORD, false, false)) -} function clause print_insn (C_SW(uimm, rsc1, rsc2)) = "c.sw " ^ creg2reg_bits(rsc1) ^ ", " ^ creg2reg_bits(rsc2) ^ ", " ^ BitStr(uimm) @@ -1338,17 +1212,15 @@ function clause print_insn (C_SW(uimm, rsc1, rsc2)) = /* ****************************************************************** */ union clause ast = C_SD : (bits(5), cregbits, cregbits) -function clause decodeCompressed (0b111 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00): bits(16) = { +function clause decodeCompressed (0b111 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00): bits(16) = let uimm = (ui76 @ ui53) : bits(5) in Some(C_SD(uimm, rs1, rs2)) -} -function clause execute (C_SD(uimm, rsc1, rsc2)) = { +function clause execute (C_SD(uimm, rsc1, rsc2)) = let imm : bits(12) = EXTZ(uimm @ 0b000) in let rs1 = creg2reg_bits(rsc1) in let rs2 = creg2reg_bits(rsc2) in execute(STORE(imm, rs2, rs1, DOUBLE, false, false)) -} function clause print_insn (C_SD(uimm, rsc1, rsc2)) = "c.sd " ^ creg2reg_bits(rsc1) ^ ", " ^ creg2reg_bits(rsc2) ^ ", " ^ BitStr(uimm) @@ -1356,16 +1228,14 @@ function clause print_insn (C_SD(uimm, rsc1, rsc2)) = /* ****************************************************************** */ union clause ast = C_ADDI : (bits(6), regbits) -function clause decodeCompressed (0b000 @ nzi5 : bits(1) @ rsd : regbits @ nzi40 : bits(5) @ 0b01) : bits(16) = { +function clause decodeCompressed (0b000 @ nzi5 : bits(1) @ rsd : regbits @ nzi40 : bits(5) @ 0b01) : bits(16) = let nzi = (nzi5 @ nzi40) : bits(6) in if (nzi == 0b000000) | (rsd == zreg) then None() else Some(C_ADDI(nzi, rsd)) -} -function clause execute (C_ADDI(nzi, rsd)) = { +function clause execute (C_ADDI(nzi, rsd)) = let imm : bits(12) = EXTS(nzi) in execute(ITYPE(imm, rsd, rsd, RISCV_ADDI)) -} function clause print_insn (C_ADDI(nzi, rsd)) = "c.addi " ^ rsd ^ ", " ^ BitStr(nzi) @@ -1380,9 +1250,8 @@ union clause ast = C_ADDIW : (bits(6), regbits) function clause decodeCompressed (0b001 @ imm5 : bits(1) @ rsd : regbits @ imm40 : bits(5) @ 0b01) = Some (C_ADDIW((imm5 @ imm40), rsd)) -function clause execute (C_JAL(imm)) = { +function clause execute (C_JAL(imm)) = execute(RISCV_JAL(EXTS(imm @ 0b0), ra)) -} function clause execute (C_ADDIW(imm, rsd)) = { let imm : bits(32) = EXTS(imm); @@ -1401,15 +1270,14 @@ function clause print_insn (C_ADDIW(imm, rsd)) = /* ****************************************************************** */ union clause ast = C_LI : (bits(6), regbits) -function clause decodeCompressed (0b010 @ imm5 : bits(1) @ rd : regbits @ imm40 : bits(5) @ 0b01) = { - if (rd == zreg) then None() +function clause decodeCompressed (0b010 @ imm5 : bits(1) @ rd : regbits @ imm40 : bits(5) @ 0b01) = + if rd == zreg + then None() else Some(C_LI(imm5 @ imm40, rd)) -} -function clause execute (C_LI(imm, rd)) = { +function clause execute (C_LI(imm, rd)) = let imm : bits(12) = EXTS(imm) in execute(ITYPE(imm, zreg, rd, RISCV_ADDI)) -} function clause print_insn (C_LI(imm, rd)) = "c.li " ^ rd ^ ", " ^ BitStr(imm) @@ -1417,16 +1285,15 @@ function clause print_insn (C_LI(imm, rd)) = /* ****************************************************************** */ union clause ast = C_ADDI16SP : (bits(6)) -function clause decodeCompressed (0b011 @ nzi9 : bits(1) @ /* x2 */ 0b00010 @ nzi4 : bits(1) @ nzi6 : bits(1) @ nzi87 : bits(2) @ nzi5 : bits(1) @ 0b01) = { - let nzimm = nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4 in - if (nzimm == 0b000000) then None() +function clause decodeCompressed (0b011 @ nzi9 : bits(1) @ /* x2 */ 0b00010 @ nzi4 : bits(1) @ nzi6 : bits(1) @ nzi87 : bits(2) @ nzi5 : bits(1) @ 0b01) = + let nzimm = nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4 in + if nzimm == 0b000000 + then None() else Some(C_ADDI16SP(nzimm)) -} -function clause execute (C_ADDI16SP(imm)) = { +function clause execute (C_ADDI16SP(imm)) = let imm : bits(12) = EXTS(imm @ 0x0) in execute(ITYPE(imm, sp, sp, RISCV_ADDI)) -} function clause print_insn (C_ADDI16SP(imm)) = "c.addi16sp " ^ BitStr(imm) @@ -1434,15 +1301,14 @@ function clause print_insn (C_ADDI16SP(imm)) = /* ****************************************************************** */ union clause ast = C_LUI : (bits(6), regbits) -function clause decodeCompressed (0b011 @ imm17 : bits(1) @ rd : regbits @ imm1612 : bits(5) @ 0b01) = { - if (rd == zreg) | (rd == sp) then None() +function clause decodeCompressed (0b011 @ imm17 : bits(1) @ rd : regbits @ imm1612 : bits(5) @ 0b01) = + if (rd == zreg) | (rd == sp) + then None() else Some(C_LUI(imm17 @ imm1612, rd)) -} -function clause execute (C_LUI(imm, rd)) = { +function clause execute (C_LUI(imm, rd)) = let res : bits(20) = EXTS(imm) in execute(UTYPE(res, rd, RISCV_LUI)) -} function clause print_insn (C_LUI(imm, rd)) = "c.lui " ^ rd ^ ", " ^ BitStr(imm) @@ -1450,17 +1316,15 @@ function clause print_insn (C_LUI(imm, rd)) = /* ****************************************************************** */ union clause ast = C_SRLI : (bits(6), cregbits) -function clause decodeCompressed (0b100 @ nzui5 : bits(1) @ 0b00 @ rsd : cregbits @ nzui40 : bits(5) @ 0b01) = { - let shamt : bits(6) = nzui5 @ nzui40 in - if shamt == 0b000000 /* TODO: On RV32, also need shamt[5] == 0 */ +function clause decodeCompressed (0b100 @ nzui5 : bits(1) @ 0b00 @ rsd : cregbits @ nzui40 : bits(5) @ 0b01) = + let shamt : bits(6) = nzui5 @ nzui40 in + if shamt == 0b000000 /* TODO: On RV32, also need shamt[5] == 0 */ then None() else Some(C_SRLI(shamt, rsd)) -} -function clause execute (C_SRLI(shamt, rsd)) = { +function clause execute (C_SRLI(shamt, rsd)) = let rsd = creg2reg_bits(rsd) in execute(SHIFTIOP(shamt, rsd, rsd, RISCV_SRLI)) -} function clause print_insn (C_SRLI(shamt, rsd)) = "c.srli " ^ creg2reg_bits(rsd) ^ ", " ^ BitStr(shamt) @@ -1468,17 +1332,15 @@ function clause print_insn (C_SRLI(shamt, rsd)) = /* ****************************************************************** */ union clause ast = C_SRAI : (bits(6), cregbits) -function clause decodeCompressed (0b100 @ nzui5 : bits(1) @ 0b01 @ rsd : cregbits @ nzui40 : bits(5) @ 0b01) = { - let shamt : bits(6) = nzui5 @ nzui40 in - if shamt == 0b000000 /* TODO: On RV32, also need shamt[5] == 0 */ +function clause decodeCompressed (0b100 @ nzui5 : bits(1) @ 0b01 @ rsd : cregbits @ nzui40 : bits(5) @ 0b01) = + let shamt : bits(6) = nzui5 @ nzui40 in + if shamt == 0b000000 /* TODO: On RV32, also need shamt[5] == 0 */ then None() else Some(C_SRAI(shamt, rsd)) -} -function clause execute (C_SRAI(shamt, rsd)) = { +function clause execute (C_SRAI(shamt, rsd)) = let rsd = creg2reg_bits(rsd) in execute(SHIFTIOP(shamt, rsd, rsd, RISCV_SRAI)) -} function clause print_insn (C_SRAI(shamt, rsd)) = "c.srai " ^ creg2reg_bits(rsd) ^ ", " ^ BitStr(shamt) @@ -1488,10 +1350,9 @@ union clause ast = C_ANDI : (bits(6), cregbits) function clause decodeCompressed (0b100 @ i5 : bits(1) @ 0b10 @ rsd : cregbits @ i40 : bits(5) @ 0b01) = Some(C_ANDI(i5 @ i40, rsd)) -function clause execute (C_ANDI(imm, rsd)) = { +function clause execute (C_ANDI(imm, rsd)) = let rsd = creg2reg_bits(rsd) in execute(ITYPE(EXTS(imm), rsd, rsd, RISCV_ANDI)) -} function clause print_insn (C_ANDI(imm, rsd)) = "c.andi " ^ creg2reg_bits(rsd) ^ ", " ^ BitStr(imm) @@ -1501,11 +1362,10 @@ union clause ast = C_SUB : (cregbits, cregbits) function clause decodeCompressed (0b100 @ 0b0 @ 0b11 @ rsd : cregbits @ 0b00 @ rs2 : cregbits @ 0b01) = Some(C_SUB(rsd, rs2)) -function clause execute (C_SUB(rsd, rs2)) = { +function clause execute (C_SUB(rsd, rs2)) = let rsd = creg2reg_bits(rsd) in let rs2 = creg2reg_bits(rs2) in execute(RTYPE(rs2, rsd, rsd, RISCV_SUB)) -} function clause print_insn (C_SUB(rsd, rs2)) = "c.sub " ^ creg2reg_bits(rsd) ^ ", " ^ creg2reg_bits(rs2) @@ -1515,11 +1375,10 @@ union clause ast = C_XOR : (cregbits, cregbits) function clause decodeCompressed (0b100 @ 0b0 @ 0b11 @ rsd : cregbits @ 0b01 @ rs2 : cregbits @ 0b01) = Some(C_XOR(rsd, rs2)) -function clause execute (C_XOR(rsd, rs2)) = { +function clause execute (C_XOR(rsd, rs2)) = let rsd = creg2reg_bits(rsd) in let rs2 = creg2reg_bits(rs2) in execute(RTYPE(rs2, rsd, rsd, RISCV_XOR)) -} function clause print_insn (C_XOR(rsd, rs2)) = "c.xor " ^ creg2reg_bits(rsd) ^ ", " ^ creg2reg_bits(rs2) @@ -1529,11 +1388,10 @@ union clause ast = C_OR : (cregbits, cregbits) function clause decodeCompressed (0b100 @ 0b0 @ 0b11 @ rsd : cregbits @ 0b10 @ rs2 : cregbits @ 0b01) = Some(C_OR(rsd, rs2)) -function clause execute (C_OR(rsd, rs2)) = { +function clause execute (C_OR(rsd, rs2)) = let rsd = creg2reg_bits(rsd) in let rs2 = creg2reg_bits(rs2) in execute(RTYPE(rs2, rsd, rsd, RISCV_OR)) -} function clause print_insn (C_OR(rsd, rs2)) = "c.or " ^ creg2reg_bits(rsd) ^ ", " ^ creg2reg_bits(rs2) @@ -1543,11 +1401,10 @@ union clause ast = C_AND : (cregbits, cregbits) function clause decodeCompressed (0b100 @ 0b0 @ 0b11 @ rsd : cregbits @ 0b11 @ rs2 : cregbits @ 0b01) = Some(C_AND(rsd, rs2)) -function clause execute (C_AND(rsd, rs2)) = { +function clause execute (C_AND(rsd, rs2)) = let rsd = creg2reg_bits(rsd) in let rs2 = creg2reg_bits(rs2) in execute(RTYPE(rs2, rsd, rsd, RISCV_AND)) -} function clause print_insn (C_AND(rsd, rs2)) = "c.and " ^ creg2reg_bits(rsd) ^ ", " ^ creg2reg_bits(rs2) @@ -1558,11 +1415,10 @@ union clause ast = C_SUBW : (cregbits, cregbits) /* TODO: invalid on RV32 */ function clause decodeCompressed (0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b00 @ rs2 : cregbits @ 0b01) = Some(C_SUBW(rsd, rs2)) -function clause execute (C_SUBW(rsd, rs2)) = { +function clause execute (C_SUBW(rsd, rs2)) = let rsd = creg2reg_bits(rsd) in let rs2 = creg2reg_bits(rs2) in execute(RTYPEW(rs2, rsd, rsd, RISCV_SUBW)) -} function clause print_insn (C_SUBW(rsd, rs2)) = "c.subw " ^ creg2reg_bits(rsd) ^ ", " ^ creg2reg_bits(rs2) @@ -1573,11 +1429,10 @@ union clause ast = C_ADDW : (cregbits, cregbits) /* TODO: invalid on RV32 */ function clause decodeCompressed (0b100 @ 0b1 @ 0b11 @ rsd : cregbits @ 0b01 @ rs2 : cregbits @ 0b01) = Some(C_ADDW(rsd, rs2)) -function clause execute (C_ADDW(rsd, rs2)) = { +function clause execute (C_ADDW(rsd, rs2)) = let rsd = creg2reg_bits(rsd) in let rs2 = creg2reg_bits(rs2) in execute(RTYPEW(rs2, rsd, rsd, RISCV_ADDW)) -} function clause print_insn (C_ADDW(rsd, rs2)) = "c.addw " ^ creg2reg_bits(rsd) ^ ", " ^ creg2reg_bits(rs2) @@ -1621,12 +1476,11 @@ function clause print_insn (C_BNEZ(imm, rs)) = /* ****************************************************************** */ union clause ast = C_SLLI : (bits(6), regbits) -function clause decodeCompressed (0b000 @ nzui5 : bits(1) @ rsd : regbits @ nzui40 : bits(5) @ 0b10) = { - let shamt : bits(6) = nzui5 @ nzui40 in - if shamt == 0b000000 | rsd == zreg /* TODO: On RV32, also need shamt[5] == 0 */ +function clause decodeCompressed (0b000 @ nzui5 : bits(1) @ rsd : regbits @ nzui40 : bits(5) @ 0b10) = + let shamt : bits(6) = nzui5 @ nzui40 in + if shamt == 0b000000 | rsd == zreg /* TODO: On RV32, also need shamt[5] == 0 */ then None() else Some(C_SLLI(shamt, rsd)) -} function clause execute (C_SLLI(shamt, rsd)) = execute(SHIFTIOP(shamt, rsd, rsd, RISCV_SLLI)) @@ -1637,17 +1491,15 @@ function clause print_insn (C_SLLI(shamt, rsd)) = /* ****************************************************************** */ union clause ast = C_LWSP : (bits(6), regbits) -function clause decodeCompressed (0b010 @ ui5 : bits(1) @ rd : regbits @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10) = { - let uimm : bits(6) = ui76 @ ui5 @ ui42 in - if rd == zreg +function clause decodeCompressed (0b010 @ ui5 : bits(1) @ rd : regbits @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10) = + let uimm : bits(6) = ui76 @ ui5 @ ui42 in + if rd == zreg then None() else Some(C_LWSP(uimm, rd)) -} -function clause execute (C_LWSP(uimm, rd)) = { +function clause execute (C_LWSP(uimm, rd)) = let imm : bits(12) = EXTZ(uimm @ 0b00) in execute(LOAD(imm, sp, rd, false, WORD, false, false)) -} function clause print_insn (C_LWSP(uimm, rd)) = "c.lwsp " ^ rd ^ ", " ^ BitStr(uimm) @@ -1655,17 +1507,15 @@ function clause print_insn (C_LWSP(uimm, rd)) = /* ****************************************************************** */ union clause ast = C_LDSP : (bits(6), regbits) -function clause decodeCompressed (0b011 @ ui5 : bits(1) @ rd : regbits @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10) = { - let uimm : bits(6) = ui86 @ ui5 @ ui43 in - if rd == zreg +function clause decodeCompressed (0b011 @ ui5 : bits(1) @ rd : regbits @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10) = + let uimm : bits(6) = ui86 @ ui5 @ ui43 in + if rd == zreg then None() else Some(C_LDSP(uimm, rd)) -} -function clause execute (C_LDSP(uimm, rd)) = { +function clause execute (C_LDSP(uimm, rd)) = let imm : bits(12) = EXTZ(uimm @ 0b000) in execute(LOAD(imm, sp, rd, false, DOUBLE, false, false)) -} function clause print_insn (C_LDSP(uimm, rd)) = "c.ldsp " ^ rd ^ ", " ^ BitStr(uimm) @@ -1673,15 +1523,13 @@ function clause print_insn (C_LDSP(uimm, rd)) = /* ****************************************************************** */ union clause ast = C_SWSP : (bits(6), regbits) -function clause decodeCompressed (0b110 @ ui52 : bits(4) @ ui76 : bits(2) @ rs2 : regbits @ 0b10) = { +function clause decodeCompressed (0b110 @ ui52 : bits(4) @ ui76 : bits(2) @ rs2 : regbits @ 0b10) = let uimm : bits(6) = ui76 @ ui52 in Some(C_SWSP(uimm, rs2)) -} -function clause execute (C_SWSP(uimm, rs2)) = { +function clause execute (C_SWSP(uimm, rs2)) = let imm : bits(12) = EXTZ(uimm @ 0b00) in execute(STORE(imm, rs2, sp, WORD, false, false)) -} function clause print_insn (C_SWSP(uimm, rd)) = "c.swsp " ^ rd ^ ", " ^ BitStr(uimm) @@ -1689,15 +1537,13 @@ function clause print_insn (C_SWSP(uimm, rd)) = /* ****************************************************************** */ union clause ast = C_SDSP : (bits(6), regbits) -function clause decodeCompressed (0b111 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regbits @ 0b10) = { +function clause decodeCompressed (0b111 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regbits @ 0b10) = let uimm : bits(6) = ui86 @ ui53 in Some(C_SDSP(uimm, rs2)) -} -function clause execute (C_SDSP(uimm, rs2)) = { +function clause execute (C_SDSP(uimm, rs2)) = let imm : bits(12) = EXTZ(uimm @ 0b000) in execute(STORE(imm, rs2, sp, DOUBLE, false, false)) -} function clause print_insn (C_SDSP(uimm, rd)) = "c.sdsp " ^ rd ^ ", " ^ BitStr(uimm) @@ -1705,11 +1551,10 @@ function clause print_insn (C_SDSP(uimm, rd)) = /* ****************************************************************** */ union clause ast = C_JR : (regbits) -function clause decodeCompressed (0b100 @ 0b0 @ rs1 : regbits @ 0b00000 @ 0b10) = { - if rs1 == zreg +function clause decodeCompressed (0b100 @ 0b0 @ rs1 : regbits @ 0b00000 @ 0b10) = + if rs1 == zreg then None() else Some(C_JR(rs1)) -} function clause execute (C_JR(rs1)) = execute(RISCV_JALR(EXTZ(0b0), rs1, zreg)) @@ -1720,11 +1565,10 @@ function clause print_insn (C_JR(rs1)) = /* ****************************************************************** */ union clause ast = C_JALR : (regbits) -function clause decodeCompressed (0b100 @ 0b1 @ rs1 : regbits @ 0b00000 @ 0b10) = { - if rs1 == zreg +function clause decodeCompressed (0b100 @ 0b1 @ rs1 : regbits @ 0b00000 @ 0b10) = + if rs1 == zreg then None() else Some(C_JALR(rs1)) -} function clause execute (C_JALR(rs1)) = execute(RISCV_JALR(EXTZ(0b0), rs1, ra)) @@ -1735,11 +1579,10 @@ function clause print_insn (C_JALR(rs1)) = /* ****************************************************************** */ union clause ast = C_MV : (regbits, regbits) -function clause decodeCompressed (0b100 @ 0b0 @ rd : regbits @ rs2 : regbits @ 0b10) = { - if rs2 == zreg | rd == zreg +function clause decodeCompressed (0b100 @ 0b0 @ rd : regbits @ rs2 : regbits @ 0b10) = + if rs2 == zreg | rd == zreg then None() else Some(C_MV(rd, rs2)) -} function clause execute (C_MV(rd, rs2)) = execute(RTYPE(rs2, zreg, rd, RISCV_ADD)) @@ -1750,11 +1593,10 @@ function clause print_insn (C_MV(rd, rs2)) = /* ****************************************************************** */ union clause ast = C_ADD : (regbits, regbits) -function clause decodeCompressed (0b100 @ 0b1 @ rsd : regbits @ rs2 : regbits @ 0b10) = { - if rsd == zreg | rs2 == zreg +function clause decodeCompressed (0b100 @ 0b1 @ rsd : regbits @ rs2 : regbits @ 0b10) = + if rsd == zreg | rs2 == zreg then None() else Some(C_ADD(rsd, rs2)) -} function clause execute (C_ADD(rsd, rs2)) = execute(RTYPE(rs2, rsd, rsd, RISCV_ADD)) @@ -1816,198 +1658,11 @@ function clause decodeCompressed _ = None() end ast end decodeCompressed end execute -end print_insn end assembly end encdec -function decode bv = Some(encdec(bv)) +function clause print_insn insn = assembly(insn) -$include <regfp.sail> - -/* in reverse order because inc vectors don't seem to work (bug) */ -let GPRstr : vector(32, dec, string) = [ "x31", "x30", "x29", "x28", "x27", "x26", "x25", "x24", "x23", "x22", "x21", - "x20", "x19", "x18", "x17", "x16", "x15", "x14", "x13", "x12", "x21", - "x10", "x9", "x8", "x7", "x6", "x5", "x4", "x3", "x2", "x1", "x0" - ] - - -let CIA_fp = RFull("CIA") -let NIA_fp = RFull("NIA") - -function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,instruction_kind) = { - iR = [| |] : regfps; - oR = [| |] : regfps; - aR = [| |] : regfps; - ik = IK_simple() : instruction_kind; - Nias = [| NIAFP_successor() |] : niafps; - Dia = DIAFP_none() : diafp; - - match instr { - EBREAK() => (), - UTYPE(imm, rd, op) => { - if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; - }, - RISCV_JAL(imm, rd) => { - if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; - let offset : bits(64) = EXTS(imm) in - Nias = [| NIAFP_concrete_address (PC + offset) |]; - ik = IK_branch(); - }, - RISCV_JALR(imm, rs, rd) => { - if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR; - if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; - let offset : bits(64) = EXTS(imm) in - Nias = [| NIAFP_indirect_address() |]; - ik = IK_branch(); - }, - BTYPE(imm, rs2, rs1, op) => { - if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR; - if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; - ik = IK_branch(); - let offset : bits(64) = EXTS(imm) in - Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |]; - }, - ITYPE(imm, rs, rd, op) => { - if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR; - if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; - }, - SHIFTIOP(imm, rs, rd, op) => { - if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR; - if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; - }, - RTYPE(rs2, rs1, rd, op) => { - if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR; - if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; - if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; - }, - CSR(csr, rs1, rd, is_imm, op) => { - let isWrite : bool = match op { - CSRRW => true, - _ => if is_imm then unsigned(rs1) != 0 else unsigned(rs1) != 0 - }; - iR = RFull(csr_name(csr)) :: iR; - if ~(is_imm) then { - iR = RFull(GPRstr[rs1]) :: iR; - }; - if isWrite then { - oR = RFull(csr_name(csr)) :: oR; - }; - oR = RFull(GPRstr[rd]) :: oR; - }, - LOAD(imm, rs, rd, unsign, width, aq, rl) => { /* XXX "unsigned" causes name conflict in lem shallow embedding... */ - if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR; - if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; - aR = iR; - ik = - match (aq, rl) { - (false, false) => IK_mem_read (Read_plain), - //(true, false) -> IK_mem_read (Read_RISCV_acquire_RCpc) - //(true, true) -> IK_mem_read (Read_RISCV_acquire_RCsc) - - _ => internal_error("LOAD type not implemented in initial_analysis") - } - }, - STORE(imm, rs2, rs1, width, aq, rl) => { - if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR; - if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; - if (rs1 == 0) then () else aR = RFull(GPRstr[rs1]) :: aR; - ik = - match (aq, rl) { - (false, false) => IK_mem_write (Write_plain), - //case (false, true) -> IK_mem_write (Write_RISCV_release_RCpc) - //case (true, true) -> IK_mem_write (Write_RISCV_release_RCsc) - - _ => internal_error("STORE type not implemented in initial_analysis") - } - }, - ADDIW(imm, rs, rd) => { - if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR; - if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; - }, - SHIFTW(imm, rs, rd, op) => { - if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR; - if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; - }, - RTYPEW(rs2, rs1, rd, op) => { - if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR; - if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; - if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; - }, - FENCE(pred, succ) => { - ik = - match (pred, succ) { - (0b0011, 0b0011) => IK_barrier (Barrier_RISCV_rw_rw), - (0b0010, 0b0011) => IK_barrier (Barrier_RISCV_r_rw), - (0b0010, 0b0010) => IK_barrier (Barrier_RISCV_r_r), - (0b0011, 0b0001) => IK_barrier (Barrier_RISCV_rw_w), - (0b0001, 0b0001) => IK_barrier (Barrier_RISCV_w_w), - - (0b1111, 0b1111) => IK_barrier (Barrier_RISCV_rw_rw), - (0b1110, 0b1111) => IK_barrier (Barrier_RISCV_r_rw), - (0b1110, 0b1110) => IK_barrier (Barrier_RISCV_r_r), - (0b1111, 0b1101) => IK_barrier (Barrier_RISCV_rw_w), - (0b1101, 0b1101) => IK_barrier (Barrier_RISCV_w_w), - - // (0b0001, 0b0011) => IK_barrier (Barrier_RISCV_w_rw), - // (0b0011, 0b0010) => IK_barrier (Barrier_RISCV_rw_r), - // (0b0010, 0b0001) => IK_barrier (Barrier_RISCV_r_w), - // (0b0001, 0b0010) => IK_barrier (Barrier_RISCV_w_r), - - - (0b0000, 0b0000) => IK_simple (), - - _ => internal_error("barrier type not implemented in initial_analysis") - // case (FM_NORMAL, _, _) -> exit "not implemented" - - // case (FM_TSO, 0b0011, 0b0011) -> IK_barrier (Barrier_RISCV_tso) - // case (FM_TSO, _, _) -> exit "not implemented" - }; - }, - FENCEI() => { - ik = IK_barrier (Barrier_RISCV_i); - }, - // LOADRES(aq, rl, rs1, width, rd) => { - // if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; - // if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; - // aR = iR; - // ik = match (aq, rl) { - // (false, false) => IK_mem_read (Read_RISCV_reserved) - // (true, false) => IK_mem_read (Read_RISCV_reserved_acquire_RCsc) - // (true, true) => IK_mem_read (Read_RISCV_reserved_acquire_release) - - // (false, true) => exit "not implemented" - // }; - // }, - // STORECON(aq, rl, rs2, rs1, width, rd) => { - // if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR; - // if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; - // if (rs1 == 0) then () else aR = RFull(GPRstr[rs1]) :: aR; - // if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; - - // ik = switch (aq, rl) { - // case (false, false) -> IK_mem_write (Write_RISCV_conditional) - // case (false, true) -> IK_mem_write (Write_RISCV_conditional_release_RCsc) - // case (true, true) -> IK_mem_write (Write_RISCV_conditional_acquire_release) - - // case (true, false) -> exit "not implemented" - // }; - // } - // AMO(op, aq, rl, rs2, rs1, width, rd) => { - // if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR; - // if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; - // if (rs1 == 0) then () else aR = RFull(GPRstr[rs1]) :: aR; - // if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; - - // ik = switch (aq, rl) { - // (false, false) => IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional) - // (false, true) => IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional_release_RCsc) - // (true, false) => IK_mem_rmw (Read_RISCV_reserved_acquire_RCsc, - // Write_RISCV_conditional) - // (true, true) => IK_mem_rmw (Read_RISCV_reserved_acquire_RCsc, - // Write_RISCV_conditional_release_RCsc) - // }; - // } - _ => () - }; - (iR,oR,aR,Nias,Dia,ik) -} +end print_insn + +function decode bv = Some(encdec(bv)) diff --git a/riscv/riscv_analysis.sail b/riscv/riscv_analysis.sail new file mode 100644 index 00000000..e374933a --- /dev/null +++ b/riscv/riscv_analysis.sail @@ -0,0 +1,179 @@ +$include <regfp.sail> + +/* in reverse order because inc vectors don't seem to work (bug) */ +let GPRstr : vector(32, dec, string) = [ "x31", "x30", "x29", "x28", "x27", "x26", "x25", "x24", "x23", "x22", "x21", + "x20", "x19", "x18", "x17", "x16", "x15", "x14", "x13", "x12", "x11", + "x10", "x9", "x8", "x7", "x6", "x5", "x4", "x3", "x2", "x1", "x0" + ] + + +let CIA_fp = RFull("CIA") +let NIA_fp = RFull("NIA") + +function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,instruction_kind) = { + iR = [| |] : regfps; + oR = [| |] : regfps; + aR = [| |] : regfps; + ik = IK_simple() : instruction_kind; + Nias = [| NIAFP_successor() |] : niafps; + Dia = DIAFP_none() : diafp; + + match instr { + EBREAK() => (), + UTYPE(imm, rd, op) => { + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + }, + RISCV_JAL(imm, rd) => { + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + let offset : bits(64) = EXTS(imm) in + Nias = [| NIAFP_concrete_address (PC + offset) |]; + ik = IK_branch(); + }, + RISCV_JALR(imm, rs, rd) => { + if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + let offset : bits(64) = EXTS(imm) in + Nias = [| NIAFP_indirect_address() |]; + ik = IK_branch(); + }, + BTYPE(imm, rs2, rs1, op) => { + if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR; + if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; + ik = IK_branch(); + let offset : bits(64) = EXTS(imm) in + Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |]; + }, + ITYPE(imm, rs, rd, op) => { + if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + }, + SHIFTIOP(imm, rs, rd, op) => { + if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + }, + RTYPE(rs2, rs1, rd, op) => { + if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR; + if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + }, + CSR(csr, rs1, rd, is_imm, op) => { + let isWrite : bool = match op { + CSRRW => true, + _ => if is_imm then unsigned(rs1) != 0 else unsigned(rs1) != 0 + }; + iR = RFull(csr_name(csr)) :: iR; + if ~(is_imm) then { + iR = RFull(GPRstr[rs1]) :: iR; + }; + if isWrite then { + oR = RFull(csr_name(csr)) :: oR; + }; + oR = RFull(GPRstr[rd]) :: oR; + }, + LOAD(imm, rs, rd, unsign, width, aq, rl) => { /* XXX "unsigned" causes name conflict in lem shallow embedding... */ + if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + aR = iR; + ik = + match (aq, rl) { + (false, false) => IK_mem_read (Read_plain), + (true, false) => IK_mem_read (Read_RISCV_acquire), + (true, true) => IK_mem_read (Read_RISCV_strong_acquire), + + _ => internal_error("LOAD type not implemented in initial_analysis") + } + }, + STORE(imm, rs2, rs1, width, aq, rl) => { + if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR; + if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; + if (rs1 == 0) then () else aR = RFull(GPRstr[rs1]) :: aR; + ik = + match (aq, rl) { + (false, false) => IK_mem_write (Write_plain), + (false, true) => IK_mem_write (Write_RISCV_release), + (true, true) => IK_mem_write (Write_RISCV_strong_release), + + _ => internal_error("STORE type not implemented in initial_analysis") + } + }, + ADDIW(imm, rs, rd) => { + if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + }, + SHIFTW(imm, rs, rd, op) => { + if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + }, + RTYPEW(rs2, rs1, rd, op) => { + if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR; + if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + }, + FENCE(pred, succ) => { + ik = + match (pred, succ) { + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_rw_rw), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_r_rw), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_r_r), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_rw_w), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_w_w), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_w_rw), + (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_rw_r), + (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => IK_barrier (Barrier_RISCV_r_w), + (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => IK_barrier (Barrier_RISCV_w_r), + + + (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => IK_simple (), + + _ => internal_error("barrier type not implemented in initial_analysis") + // case (FM_NORMAL, _, _) -> exit "not implemented" + + // case (FM_TSO, 0b0011, 0b0011) -> IK_barrier (Barrier_RISCV_tso) + // case (FM_TSO, _, _) -> exit "not implemented" + }; + }, + FENCEI() => { + ik = IK_simple (); // for RMEM, should morally be Barrier_RISCV_i + }, + LOADRES(aq, rl, rs1, width, rd) => { + if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + aR = iR; + ik = match (aq, rl) { + (false, false) => IK_mem_read (Read_RISCV_reserved), + (true, false) => IK_mem_read (Read_RISCV_reserved_acquire), + (true, true) => IK_mem_read (Read_RISCV_reserved_strong_acquire), + (false, true) => internal_error("LOADRES type not implemented in initial_analysis") + }; + }, + STORECON(aq, rl, rs2, rs1, width, rd) => { + if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR; + if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; + if (rs1 == 0) then () else aR = RFull(GPRstr[rs1]) :: aR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + ik = match (aq, rl) { + (false, false) => IK_mem_write (Write_RISCV_conditional), + (false, true) => IK_mem_write (Write_RISCV_conditional_release), + (true, true) => IK_mem_write (Write_RISCV_conditional_strong_release), + + (true, false) => internal_error("STORECON type not implemented in initial_analysis") + }; + }, + AMO(op, aq, rl, rs2, rs1, width, rd) => { + if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR; + if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; + if (rs1 == 0) then () else aR = RFull(GPRstr[rs1]) :: aR; + if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; + ik = match (aq, rl) { + (false, false) => IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional), + (false, true) => IK_mem_rmw (Read_RISCV_reserved, Write_RISCV_conditional_release), + (true, false) => IK_mem_rmw (Read_RISCV_reserved_acquire, + Write_RISCV_conditional), + (true, true) => IK_mem_rmw (Read_RISCV_reserved_acquire, + Write_RISCV_conditional_release) + }; + }, + _ => () + }; + (iR,oR,aR,Nias,Dia,ik) +} diff --git a/riscv/riscv_duopod.sail b/riscv/riscv_duopod.sail index ddb4f6e5..ff1e4065 100644 --- a/riscv/riscv_duopod.sail +++ b/riscv/riscv_duopod.sail @@ -37,7 +37,7 @@ overload X = {rX, wX} val MEMr : forall 'n. (xlen_t, atom('n)) -> bits(8 * 'n) effect {rmem} function MEMr (addr, width) = - match __RISCV_read(addr, width) { Some(v) => v, None() => zeros(8 * width) } + match __RISCV_read(addr, width, false, false, false) { Some(v) => v, None() => zeros(8 * width) } /* Instruction decode and execute */ enum iop = {RISCV_ADDI, RISCV_SLTI, RISCV_SLTIU, RISCV_XORI, RISCV_ORI, RISCV_ANDI} /* immediate ops */ diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem index 601f5008..a6fa1298 100644 --- a/riscv/riscv_extras.lem +++ b/riscv/riscv_extras.lem @@ -13,6 +13,10 @@ let MEM_fence_r_rw () = barrier Barrier_RISCV_r_rw let MEM_fence_r_r () = barrier Barrier_RISCV_r_r let MEM_fence_rw_w () = barrier Barrier_RISCV_rw_w let MEM_fence_w_w () = barrier Barrier_RISCV_w_w +let MEM_fence_w_rw () = barrier Barrier_RISCV_w_rw +let MEM_fence_rw_r () = barrier Barrier_RISCV_rw_r +let MEM_fence_r_w () = barrier Barrier_RISCV_r_w +let MEM_fence_w_r () = barrier Barrier_RISCV_w_r let MEM_fence_i () = barrier Barrier_RISCV_i val MEMea : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e @@ -30,18 +34,36 @@ let MEMea_conditional_release addr size = write_mem_ea Write_RISCV_conditional_ let MEMea_conditional_strong_release addr size = write_mem_ea Write_RISCV_conditional_strong_release addr size +val MEMr : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_reserved : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_reserved_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_reserved_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e + +let MEMr addrsize size hexRAM addr = read_mem Read_plain addr size +let MEMr_acquire addrsize size hexRAM addr = read_mem Read_RISCV_acquire addr size +let MEMr_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_strong_acquire addr size +let MEMr_reserved addrsize size hexRAM addr = read_mem Read_RISCV_reserved addr size +let MEMr_reserved_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_acquire addr size +let MEMr_reserved_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_strong_acquire addr size + val write_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => - integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv unit 'e + integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e let write_ram addrsize size hexRAM address value = - write_mem_val value >>= fun _ -> - return () + write_mem_val value val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e let read_ram addrsize size hexRAM address = read_mem Read_plain address size -let speculate_conditional_success () = excl_result () +val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit +let load_reservation addr = () + +let speculate_conditional_success _ = excl_result () + +let cancel_reservation () = () val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_ram_base () = wordFromInteger 0 @@ -97,7 +119,13 @@ val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvecto let shift_bits_left v m = shiftl v (uint m) val print_string : string -> string -> unit -let print_string msg s = prerr_endline (msg ^ s) +let print_string msg s = () (* print_endline (msg ^ s) *) + +val prerr_string : string -> string -> unit +let prerr_string msg s = prerr_endline (msg ^ s) val prerr_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit let prerr_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs))) + +val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit +let print_bits msg bs = () (* print_endline (msg ^ (show_bitlist (bits_of bs))) *) diff --git a/riscv/riscv_extras_sequential.lem b/riscv/riscv_extras_sequential.lem index 601f5008..a6fa1298 100644 --- a/riscv/riscv_extras_sequential.lem +++ b/riscv/riscv_extras_sequential.lem @@ -13,6 +13,10 @@ let MEM_fence_r_rw () = barrier Barrier_RISCV_r_rw let MEM_fence_r_r () = barrier Barrier_RISCV_r_r let MEM_fence_rw_w () = barrier Barrier_RISCV_rw_w let MEM_fence_w_w () = barrier Barrier_RISCV_w_w +let MEM_fence_w_rw () = barrier Barrier_RISCV_w_rw +let MEM_fence_rw_r () = barrier Barrier_RISCV_rw_r +let MEM_fence_r_w () = barrier Barrier_RISCV_r_w +let MEM_fence_w_r () = barrier Barrier_RISCV_w_r let MEM_fence_i () = barrier Barrier_RISCV_i val MEMea : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e @@ -30,18 +34,36 @@ let MEMea_conditional_release addr size = write_mem_ea Write_RISCV_conditional_ let MEMea_conditional_strong_release addr size = write_mem_ea Write_RISCV_conditional_strong_release addr size +val MEMr : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_reserved : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_reserved_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e +val MEMr_reserved_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e + +let MEMr addrsize size hexRAM addr = read_mem Read_plain addr size +let MEMr_acquire addrsize size hexRAM addr = read_mem Read_RISCV_acquire addr size +let MEMr_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_strong_acquire addr size +let MEMr_reserved addrsize size hexRAM addr = read_mem Read_RISCV_reserved addr size +let MEMr_reserved_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_acquire addr size +let MEMr_reserved_strong_acquire addrsize size hexRAM addr = read_mem Read_RISCV_reserved_strong_acquire addr size + val write_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => - integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv unit 'e + integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e let write_ram addrsize size hexRAM address value = - write_mem_val value >>= fun _ -> - return () + write_mem_val value val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e let read_ram addrsize size hexRAM address = read_mem Read_plain address size -let speculate_conditional_success () = excl_result () +val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit +let load_reservation addr = () + +let speculate_conditional_success _ = excl_result () + +let cancel_reservation () = () val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_ram_base () = wordFromInteger 0 @@ -97,7 +119,13 @@ val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvecto let shift_bits_left v m = shiftl v (uint m) val print_string : string -> string -> unit -let print_string msg s = prerr_endline (msg ^ s) +let print_string msg s = () (* print_endline (msg ^ s) *) + +val prerr_string : string -> string -> unit +let prerr_string msg s = prerr_endline (msg ^ s) val prerr_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit let prerr_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs))) + +val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit +let print_bits msg bs = () (* print_endline (msg ^ (show_bitlist (bits_of bs))) *) diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail index bdbb72bf..72b7e8da 100644 --- a/riscv/riscv_mem.sail +++ b/riscv/riscv_mem.sail @@ -1,11 +1,15 @@ -/* memory */ +/* Physical memory model. + * + * This assumes that the platform memory map has been defined, so that accesses + * to MMIO regions can be dispatched. + */ function is_aligned_addr (addr : xlenbits, width : atom('n)) -> forall 'n. bool = unsigned(addr) % width == 0 // only used for actual memory regions, to avoid MMIO effects -function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> forall 'n. MemoryOpResult(bits(8 * 'n)) = - match (t, __RISCV_read(addr, width)) { +function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl: bool, res : bool) -> forall 'n. MemoryOpResult(bits(8 * 'n)) = + match (t, __RISCV_read(addr, width, aq, rl, res)) { (Instruction, None()) => MemException(E_Fetch_Access_Fault), (Data, None()) => MemException(E_Load_Access_Fault), (_, Some(v)) => { print("mem[" ^ t ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v)); @@ -17,24 +21,24 @@ function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> fo if t == Data & within_mmio_readable(addr, width) then mmio_read(addr, width) else if within_phys_mem(addr, width) - then phys_mem_read(t, addr, width) + then phys_mem_read(t, addr, width, false, false, false) else MemException(E_Load_Access_Fault) -/* FIXME: We assume atomic accesses are only done to memory-backed regions. MMIO is not modeled. */ +/* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */ -val MEMr : forall 'n. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem} -val MEMr_acquire : forall 'n. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem} -val MEMr_strong_acquire : forall 'n. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem} -val MEMr_reserved : forall 'n. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem} -val MEMr_reserved_acquire : forall 'n. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem} -val MEMr_reserved_strong_acquire : forall 'n. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem} +val MEMr : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg} +val MEMr_acquire : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg} +val MEMr_strong_acquire : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg} +val MEMr_reserved : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg} +val MEMr_reserved_acquire : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg} +val MEMr_reserved_strong_acquire : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg} -function MEMr (addr, width) = phys_mem_read(Data, addr, width) -function MEMr_acquire (addr, width) = phys_mem_read(Data, addr, width) -function MEMr_strong_acquire (addr, width) = phys_mem_read(Data, addr, width) -function MEMr_reserved (addr, width) = phys_mem_read(Data, addr, width) -function MEMr_reserved_acquire (addr, width) = phys_mem_read(Data, addr, width) -function MEMr_reserved_strong_acquire (addr, width) = phys_mem_read(Data, addr, width) +function MEMr (addr, width) = checked_mem_read(Data, addr, width) +function MEMr_acquire (addr, width) = checked_mem_read(Data, addr, width) +function MEMr_strong_acquire (addr, width) = checked_mem_read(Data, addr, width) +function MEMr_reserved (addr, width) = checked_mem_read(Data, addr, width) +function MEMr_reserved_acquire (addr, width) = checked_mem_read(Data, addr, width) +function MEMr_reserved_strong_acquire (addr, width) = checked_mem_read(Data, addr, width) /* NOTE: The rreg effect is due to MMIO. */ val mem_read : forall 'n, 'n > 0. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg, escape} @@ -85,38 +89,37 @@ function mem_write_ea (addr, width, aq, rl, con) = { } // only used for actual memory regions, to avoid MMIO effects -function phys_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n. MemoryOpResult(unit) = { +function phys_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n. MemoryOpResult(bool) = { print("mem[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data)); - if __RISCV_write(addr, width, data) - then MemValue(()) - else MemException(E_SAMO_Access_Fault) + MemValue(__RISCV_write(addr, width, data)) } -function checked_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n, 'n > 0. MemoryOpResult(unit) = +// dispatches to MMIO regions or physical memory regions depending on physical memory map +function checked_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n, 'n > 0. MemoryOpResult(bool) = if within_mmio_writable(addr, width) then mmio_write(addr, width, data) else if within_phys_mem(addr, width) then phys_mem_write(addr, width, data) else MemException(E_SAMO_Access_Fault) -/* FIXME: We assume atomic accesses are only done to memory-backed regions. MMIO is not modeled. */ +/* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */ -val MEMval : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv} -val MEMval_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv} -val MEMval_strong_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv} -val MEMval_conditional : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv} -val MEMval_conditional_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv} -val MEMval_conditional_strong_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv} +val MEMval : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg} +val MEMval_release : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg} +val MEMval_strong_release : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg} +val MEMval_conditional : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg} +val MEMval_conditional_release : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg} +val MEMval_conditional_strong_release : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {wmv, rreg, wreg} -function MEMval (addr, width, data) = phys_mem_write(addr, width, data) -function MEMval_release (addr, width, data) = phys_mem_write(addr, width, data) -function MEMval_strong_release (addr, width, data) = phys_mem_write(addr, width, data) -function MEMval_conditional (addr, width, data) = phys_mem_write(addr, width, data) -function MEMval_conditional_release (addr, width, data) = phys_mem_write(addr, width, data) -function MEMval_conditional_strong_release (addr, width, data) = phys_mem_write(addr, width, data) +function MEMval (addr, width, data) = checked_mem_write(addr, width, data) +function MEMval_release (addr, width, data) = checked_mem_write(addr, width, data) +function MEMval_strong_release (addr, width, data) = checked_mem_write(addr, width, data) +function MEMval_conditional (addr, width, data) = checked_mem_write(addr, width, data) +function MEMval_conditional_release (addr, width, data) = checked_mem_write(addr, width, data) +function MEMval_conditional_strong_release (addr, width, data) = checked_mem_write(addr, width, data) /* NOTE: The wreg effect is due to MMIO, the rreg is due to checking mtime. */ -val mem_write_value : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(unit) effect {wmv, rreg, wreg, escape} +val mem_write_value : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, rreg, wreg, escape} function mem_write_value (addr, width, value, aq, rl, con) = { if (rl | con) & (~ (is_aligned_addr(addr, width))) @@ -133,11 +136,13 @@ function mem_write_value (addr, width, value, aq, rl, con) = { } } -val "speculate_conditional_success" : unit -> bool effect {exmem} - val MEM_fence_rw_rw = {ocaml: "skip", lem: "MEM_fence_rw_rw"} : unit -> unit effect {barr} val MEM_fence_r_rw = {ocaml: "skip", lem: "MEM_fence_r_rw"} : unit -> unit effect {barr} val MEM_fence_r_r = {ocaml: "skip", lem: "MEM_fence_r_r"} : unit -> unit effect {barr} val MEM_fence_rw_w = {ocaml: "skip", lem: "MEM_fence_rw_w"} : unit -> unit effect {barr} val MEM_fence_w_w = {ocaml: "skip", lem: "MEM_fence_w_w"} : unit -> unit effect {barr} +val MEM_fence_w_rw = {ocaml: "skip", lem: "MEM_fence_w_rw"} : unit -> unit effect {barr} +val MEM_fence_rw_r = {ocaml: "skip", lem: "MEM_fence_rw_r"} : unit -> unit effect {barr} +val MEM_fence_r_w = {ocaml: "skip", lem: "MEM_fence_r_w"} : unit -> unit effect {barr} +val MEM_fence_w_r = {ocaml: "skip", lem: "MEM_fence_w_r"} : unit -> unit effect {barr} val MEM_fence_i = {ocaml: "skip", lem: "MEM_fence_i"} : unit -> unit effect {barr} diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail index bf0e5020..7ab83aa6 100644 --- a/riscv/riscv_platform.sail +++ b/riscv/riscv_platform.sail @@ -1,4 +1,4 @@ -/* Platform and devices */ +/* Platform-specific definitions, and basic MMIO devices. */ /* Current constraints on this implementation are: - it cannot access memory directly, but instead provides definitions for the physical memory model @@ -21,8 +21,8 @@ val plat_enable_misaligned_access = {ocaml: "Platform.enable_misaligned_access", lem: "plat_enable_misaligned_access"} : unit -> bool /* ROM holding reset vector and device-tree DTB */ -val plat_rom_base = {ocaml: "Platform.rom_base", lem: "plat_rom_base"} : unit -> xlenbits -val plat_rom_size = {ocaml: "Platform.rom_size", lem: "plat_rom_size"} : unit -> xlenbits +val plat_rom_base = {ocaml: "Platform.rom_base", lem: "plat_rom_base"} : unit -> xlenbits +val plat_rom_size = {ocaml: "Platform.rom_size", lem: "plat_rom_size"} : unit -> xlenbits /* Location of clock-interface, which should match with the spec in the DTB */ val plat_clint_base = {ocaml: "Platform.clint_base", lem: "plat_clint_base"} : unit -> xlenbits @@ -57,9 +57,8 @@ function within_clint(addr : xlenbits, width : atom('n)) -> forall 'n. bool = function within_htif_writable(addr : xlenbits, width : atom('n)) -> forall 'n. bool = plat_htif_tohost() == addr -/* TODO */ function within_htif_readable(addr : xlenbits, width : atom('n)) -> forall 'n. bool = - false + plat_htif_tohost() == addr /* CLINT (Core Local Interruptor), based on Spike. */ @@ -70,11 +69,9 @@ register mtimecmp : xlenbits // memory-mapped internal clint register. /* CLINT memory-mapped IO */ -let MSIP_BASE : xlenbits = 0x0000000000000000 -let MTIMECMP_BASE : xlenbits = 0x0000000000004000 -let MTIME_BASE : xlenbits = 0x000000000000bff8 - -/* 0000 msip hart 0 -- memory-mapped software interrupt +/* relative address map: + * + * 0000 msip hart 0 -- memory-mapped software interrupt * 0004 msip hart 1 * 4000 mtimecmp hart 0 lo -- memory-mapped timer thresholds * 4004 mtimecmp hart 0 hi @@ -84,6 +81,10 @@ let MTIME_BASE : xlenbits = 0x000000000000bff8 * bffc mtime hi */ +let MSIP_BASE : xlenbits = 0x0000000000000000 +let MTIMECMP_BASE : xlenbits = 0x0000000000004000 +let MTIME_BASE : xlenbits = 0x000000000000bff8 + val clint_load : forall 'n. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} function clint_load(addr, width) = { let addr = addr - plat_clint_base (); @@ -119,19 +120,19 @@ function clint_dispatch() -> unit = { } /* The rreg effect is due to checking mtime. */ -val clint_store: forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {rreg,wreg} +val clint_store: forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {rreg,wreg} function clint_store(addr, width, data) = { let addr = addr - plat_clint_base (); if addr == MSIP_BASE & ('n == 8 | 'n == 4) then { print("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mip.MSI <- " ^ BitStr(data[0]) ^ ")"); mip->MSI() = data[0] == 0b1; clint_dispatch(); - MemValue(()) + MemValue(true) } else if addr == MTIMECMP_BASE & 'n == 8 then { print("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mtimecmp)"); mtimecmp = zero_extend(data, 64); /* FIXME: Redundant zero_extend currently required by Lem backend */ clint_dispatch(); - MemValue(()) + MemValue(true) } else { print("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (<unmapped>)"); MemException(E_SAMO_Access_Fault) @@ -158,22 +159,37 @@ bitfield htif_cmd : bits(64) = { payload : 47 .. 0 } -register htif_done : bool +register htif_tohost : xlenbits +register htif_done : bool register htif_exit_code : xlenbits -val htif_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) -function htif_load(addr, width) = MemValue(EXTZ(0b0)) -/* FIXME: 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(unit) effect {wreg} +/* Since the htif tohost port is only available at a single address, + * we'll assume here that physical memory model has correctly + * dispatched the address. + */ + +val htif_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} +function htif_load(addr, width) = { + print("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) +} + +/* 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} function htif_store(addr, width, data) = { - // since htif is only available at a single address, we'll assume here that physical memory - // model has correctly dispatched the address. + print("htif[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data)); + /* Store the written value so that we can ack it later. */ let cbits : xlenbits = EXTZ(data); + htif_tohost = cbits; + /* Process the cmd immediately; this is needed for terminal output. */ let cmd = Mk_htif_cmd(cbits); match cmd.device() { 0x00 => { /* syscall-proxy */ - print("htif-syscall-proxy[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data)); + print("htif-syscall-proxy cmd: " ^ BitStr(cmd.payload())); if cmd.payload()[0] == 0b1 then { htif_done = true; @@ -182,16 +198,22 @@ function htif_store(addr, width, data) = { else () }, 0x01 => { /* terminal */ - print("htif-term[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data)); + print("htif-term cmd: " ^ BitStr(cmd.payload())); match cmd.cmd() { 0x00 => /* TODO: terminal input handling */ (), 0x01 => plat_term_write(cmd.payload()[7..0]), c => print("Unknown term cmd: " ^ BitStr(c)) } }, - d => print("htif-????[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data)) + d => print("htif-???? cmd: " ^ BitStr(data)) }; - MemValue(()) + MemValue(true) +} + +val htif_tick : unit -> unit effect {rreg, wreg} +function htif_tick() = { + print("htif::tick " ^ BitStr(htif_tohost)); + htif_tohost = EXTZ(0b0) /* htif ack */ } /* Top-level MMIO dispatch */ @@ -209,16 +231,22 @@ function mmio_read(addr : xlenbits, width : atom('n)) -> forall 'n. MemoryOpResu then htif_load(addr, width) else MemException(E_Load_Access_Fault) -function mmio_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n, 'n > 0. MemoryOpResult(unit) = +function mmio_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n, 'n > 0. MemoryOpResult(bool) = if within_clint(addr, width) then clint_store(addr, width, data) else if within_htif_writable(addr, width) & 'n <= 8 then htif_store(addr, width, data) else MemException(E_SAMO_Access_Fault) -/* Platform initialization */ +/* Platform initialization and ticking. */ function init_platform() -> unit = { - htif_done = false; - htif_exit_code = EXTZ(0b0); + htif_tohost = EXTZ(0b0); + htif_done = false; + htif_exit_code = EXTZ(0b0) +} + +function tick_platform() -> unit = { + cancel_reservation(); + htif_tick(); } diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail index 2ac80cc6..2d074f27 100644 --- a/riscv/riscv_step.sail +++ b/riscv/riscv_step.sail @@ -1,6 +1,8 @@ +/* The emulator fetch-execute-interrupt dispatch loop. */ + union FetchResult = { - F_Base : word, /* Base ISA */ - F_RVC : half, /* Compressed ISA */ + F_Base : word, /* Base ISA */ + F_RVC : half, /* Compressed ISA */ F_Error : (ExceptionType, xlenbits) /* exception and PC */ } @@ -8,7 +10,7 @@ function isRVC(h : half) -> bool = ~ (h[1 .. 0] == 0b11) val fetch : unit -> FetchResult effect {escape, rmem, rreg, wmv, wreg} -function fetch() -> FetchResult = { +function fetch() -> FetchResult = /* check for legal PC */ if (PC[0] != 0b0 | (PC[1] != 0b0 & (~ (haveRVC())))) then F_Error(E_Fetch_Addr_Align, PC) @@ -39,11 +41,10 @@ function fetch() -> FetchResult = { } } } -} /* returns whether an instruction was retired, and whether to increment the step count in the trace */ val step : int -> (bool, bool) effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg} -function step(step_no) = { +function step(step_no) = match curInterrupt(cur_privilege, mip, mie, mideleg) { Some(intr, priv) => { print_bits("Handling interrupt: ", intr); @@ -87,14 +88,13 @@ function step(step_no) = { } } } -} val loop : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg} function loop () = { let insns_per_tick = plat_insns_per_tick(); i : int = 0; step_no : int = 0; - while true do { + while (~ (htif_done)) do { minstret_written = false; /* see note for minstret */ let (retired, stepped) = step(step_no); PC = nextPC; @@ -107,14 +107,15 @@ function loop () = { let exit_val = unsigned(htif_exit_code); if exit_val == 0 then print("SUCCESS") else print_int("FAILURE: ", exit_val); - exit(()); - }; - - /* update time */ - i = i + 1; - if i == insns_per_tick then { - tick_clock(); - i = 0; + } else { + /* update time */ + i = i + 1; + if i == insns_per_tick then { + tick_clock(); + /* for now, we drive the platform i/o at every clock tick. */ + tick_platform(); + i = 0; + } } } } diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail index bb3d13db..451ff9ec 100644 --- a/riscv/riscv_sys.sail +++ b/riscv/riscv_sys.sail @@ -1,3 +1,5 @@ +/* Machine-mode and supervisor-mode state definitions and operations. */ + /* privilege level */ register cur_privilege : Privilege @@ -6,6 +8,34 @@ register cur_privilege : Privilege register cur_inst : xlenbits +/* State projections + * + * Some machine state is processed via projections from machine-mode views to + * views from lower privilege levels. So, for e.g. when mstatus is read from + * lower privilege levels, we use 'lowering_' projections: + * + * mstatus -> sstatus -> ustatus + * + * Similarly, when machine state is written from lower privileges, that state is + * lifted into the appropriate value for the machine-mode state. + * + * ustatus -> sstatus -> mstatus + * + * In addition, several fields in machine state registers are WARL or WLRL, + * requiring that values written to the registers be legalized. For each such + * register, there will be an associated 'legalize_' function. These functions + * will need to be supplied externally, and will depend on the legal values + * supported by a platform/implementation (or misa). The legalize_ functions + * generate a legal value from the current value and the written value. In more + * complex cases, they will also implicitly read the current values of misa, + * mstatus, etc. + * + * Each register definition below is followed by custom projections + * and choice of legalizations if needed. For now, we typically + * implement the simplest legalize_ alternatives. + */ + + /* M-mode registers */ bitfield Misa : bits(64) = { @@ -40,9 +70,14 @@ bitfield Misa : bits(64) = { } register misa : Misa -function legalize_misa(m : Misa, v : xlenbits) -> Misa = - /* Ignore all writes for now. */ - m +function legalize_misa(m : Misa, v : xlenbits) -> Misa = { + /* Allow modifications to C. */ + let v = Mk_Misa(v); + // Suppress changing C if nextPC would become misaligned. + if v.C() == false & nextPC[1] == true + then m + else update_C(m, v.C()) +} bitfield Mstatus : bits(64) = { SD : 63, @@ -88,14 +123,14 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { m } -/* machine state utilities */ +/* architecture and extension checks */ function cur_Architecture() -> Architecture = { let a : arch_xlen = match (cur_privilege) { - Machine => misa.MXL(), + Machine => misa.MXL(), Supervisor => mstatus.SXL(), - User => mstatus.UXL() + User => mstatus.UXL() }; match architecture(a) { Some(a) => a, @@ -112,7 +147,7 @@ function haveRVC() -> bool = { misa.C() == true } function haveMulDiv() -> bool = { misa.M() == true } function haveFP() -> bool = { misa.F() == true | misa.D() == true } -/* interrupt registers */ +/* interrupt processing state */ bitfield Minterrupts : bits(64) = { MEI : 11, /* external interrupts */ @@ -163,7 +198,7 @@ function legalize_mideleg(o : Minterrupts, v : xlenbits) -> Minterrupts = { m } -/* exception registers */ +/* exception processing state */ bitfield Medeleg : bits(64) = { SAMO_Page_Fault : 15, @@ -225,14 +260,22 @@ function tvec_addr(m : Mtvec, c : Mcause) -> option(xlenbits) = { } } -/* auxiliary exception registers */ +/* Exception PC */ + register mepc : xlenbits +// legalizing writes to xepc function legalize_xepc(v : xlenbits) -> xlenbits = { v & EXTS(if haveRVC() then 0b110 else 0b100) } -register mtval : xlenbits +// masking for reads to xepc +function pc_alignment_mask() -> xlenbits = + ~(EXTZ(if misa.C() == true then 0b00 else 0b10)) + +/* auxiliary exception registers */ + +register mtval : xlenbits register mscratch : xlenbits /* counters */ @@ -266,15 +309,17 @@ function legalize_scounteren(c : Counteren, v : xlenbits) -> Counteren = { register mcycle : xlenbits register mtime : xlenbits -/* minstret is an architectural register, and can be written to. The - spec says that minstret increments on instruction retires need to - occur before any explicit writes to instret. However, in our - simulation loop, we need to execute an instruction to find out - whether it retired, and hence can only increment instret after - execution. To avoid doing this in the case minstret was explicitly - written to, we track writes to it in a separate model-internal - register. -*/ +/* minstret + * + * minstret is an architectural register, and can be written to. The + * spec says that minstret increments on instruction retires need to + * occur before any explicit writes to instret. However, in our + * simulation loop, we need to execute an instruction to find out + * whether it retired, and hence can only increment instret after + * execution. To avoid doing this in the case minstret was explicitly + * written to, we track writes to it in a separate model-internal + * register. + */ register minstret : xlenbits register minstret_written : bool @@ -295,8 +340,10 @@ register mhartid : xlenbits register pmpaddr0 : xlenbits register pmpcfg0 : xlenbits -/* supervisor mode registers */ +/* S-mode registers */ + +/* sstatus reveals a subset of mstatus */ bitfield Sstatus : bits(64) = { SD : 63, UXL : 33 .. 32, @@ -329,7 +376,8 @@ function lower_mstatus(m : Mstatus) -> Sstatus = { function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = { let m = update_SD(m, s.SD()); - // let m = update_UXL(m, s.UXL()); FIXME: This should be parameterized by a platform setting. For now, match spike. + // FIXME: This should be parameterized by a platform setting. For now, match spike. + // let m = update_UXL(m, s.UXL()); let m = update_MXR(m, s.MXR()); let m = update_SUM(m, s.SUM()); let m = update_XS(m, s.XS()); @@ -363,7 +411,6 @@ function legalize_sedeleg(s : Sedeleg, v : xlenbits) -> Sedeleg = { Mk_Sedeleg(EXTZ(v[8..0])) } -/* TODO: handle views for interrupt delegation */ bitfield Sinterrupts : bits(64) = { SEI : 9, /* external interrupts */ UEI : 8, @@ -426,6 +473,7 @@ function legalize_sie(m : Minterrupts, d : Minterrupts, v : xlenbits) -> Minterr register sideleg : Sinterrupts +/* s-mode address translation and protection (satp) */ bitfield Satp64 : bits(64) = { Mode : 63 .. 60, Asid : 59 .. 44, @@ -442,16 +490,17 @@ function legalize_satp(a : Architecture, o : xlenbits, v : xlenbits) -> xlenbits } } -register stvec : Mtvec +/* other supervisor state */ +register stvec : Mtvec register sscratch : xlenbits -register sepc : xlenbits -register scause : Mcause -register stval : xlenbits +register sepc : xlenbits +register scause : Mcause +register stval : xlenbits /* disabled trigger/debug module */ register tselect : xlenbits -/* csr name printer */ +/* CSR names */ val cast csr_name : csreg -> string function csr_name(csr) = { @@ -527,6 +576,12 @@ mapping csr_name_map : csreg <-> string = { 0x000 <-> "ustatus", 0x004 <-> "uie", 0x005 <-> "utvec", + /* user trap handling */ + 0x040 <-> "uscratch", + 0x041 <-> "uepc", + 0x042 <-> "ucause", + 0x043 <-> "utval", + 0x044 <-> "uip", /* user floating-point context */ 0x001 <-> "fflags", 0x002 <-> "frm", @@ -573,7 +628,27 @@ mapping csr_name_map : csreg <-> string = { 0x342 <-> "mcause", 0x343 <-> "mtval", 0x344 <-> "mip", - /* TODO: machine protection and translation */ + /* machine protection and translation */ + 0x3A0 <-> "pmpcfg0", + 0x3A1 <-> "pmpcfg1", + 0x3A2 <-> "pmpcfg2", + 0x3A3 <-> "pmpcfg3", + 0x3B0 <-> "pmpaddr0", + 0x3B1 <-> "pmpaddr1", + 0x3B2 <-> "pmpaddr2", + 0x3B3 <-> "pmpaddr3", + 0x3B4 <-> "pmpaddr4", + 0x3B5 <-> "pmpaddr5", + 0x3B6 <-> "pmpaddr6", + 0x3B7 <-> "pmpaddr7", + 0x3B8 <-> "pmpaddr8", + 0x3B9 <-> "pmpaddr9", + 0x3BA <-> "pmpaddr10", + 0x3BB <-> "pmpaddr11", + 0x3BC <-> "pmpaddr12", + 0x3BD <-> "pmpaddr13", + 0x3BE <-> "pmpaddr14", + 0x3BF <-> "pmpaddr15", /* machine counters/timers */ 0xB00 <-> "mcycle", 0xB02 <-> "minstret", @@ -581,11 +656,17 @@ mapping csr_name_map : csreg <-> string = { 0xB82 <-> "minstreth", /* TODO: other hpm counters and events */ /* trigger/debug */ - 0x7a0 <-> "tselect" + 0x7a0 <-> "tselect", + 0x7a1 <-> "tdata1", + 0x7a2 <-> "tdata2", + 0x7a3 <-> "tdata3" + + /* numeric fallback */ + /* reg <-> hex_bits_12(reg) */ } -/* csr access control */ +/* CSR access control */ function csrAccess(csr : csreg) -> csrRW = csr[11..10] function csrPriv(csr : csreg) -> priv_level = csr[9..8] @@ -670,6 +751,24 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool = & check_TVM_SATP(csr, p) & check_Counteren(csr, p) +/* Reservation handling for LR/SC. + * + * The reservation state is maintained external to the model since the + * reservation behavior is platform-specific anyway and maintaining + * this state outside the model simplifies the concurrency analysis. + * + * These are externs are defined here in the system module since + * we currently perform reservation cancellation on privilege level + * transition. Ideally, the platform should get more visibility into + * where cancellation can be performed. + */ + +val load_reservation = {ocaml: "Platform.load_reservation", lem: "load_reservation"} : xlenbits -> unit + +val match_reservation = {ocaml: "Platform.match_reservation", lem: "speculate_conditional_success"} : xlenbits -> bool effect {exmem} + +val cancel_reservation = {ocaml: "Platform.cancel_reservation", lem: "cancel_reservation"} : unit -> unit + /* Exception delegation: given an exception and the privilege at which * it occured, returns the privilege at which it should be handled. */ @@ -750,10 +849,10 @@ function curInterrupt(priv : Privilege, pend : Minterrupts, enbl : Minterrupts, } } -/* instruction control flow */ +/* privilege transitions due to exceptions and interrupts */ struct sync_exception = { - trap : ExceptionType, + trap : ExceptionType, excinfo : option(xlenbits) } @@ -776,6 +875,7 @@ union ctl_result = { function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits)) -> xlenbits = { print("handling " ^ (if intr then "int#" else "exc#") ^ BitStr(c) ^ " at priv " ^ del_priv ^ " with tval " ^ BitStr(tval(info))); + match (del_priv) { Machine => { mcause->IsInterrupt() = intr; @@ -791,6 +891,8 @@ function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenb print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log + cancel_reservation(); + match tvec_addr(mtvec, mcause) { Some(epc) => epc, None() => internal_error("Invalid mtvec mode") @@ -814,6 +916,8 @@ function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenb print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log + cancel_reservation(); + match tvec_addr(stvec, scause) { Some(epc) => epc, None() => internal_error("Invalid stvec mode") @@ -834,7 +938,7 @@ function handle_exception(cur_priv : Privilege, ctl : ctl_result, handle_trap(del_priv, false, e.trap, pc, e.excinfo) }, (_, CTL_MRET()) => { - let prev_priv = cur_privilege; + let prev_priv = cur_privilege; mstatus->MIE() = mstatus.MPIE(); mstatus->MPIE() = true; cur_privilege = privLevel_of_bits(mstatus.MPP()); @@ -842,10 +946,12 @@ function handle_exception(cur_priv : Privilege, ctl : ctl_result, print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log print("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege); - mepc + + cancel_reservation(); + mepc & pc_alignment_mask() }, (_, CTL_SRET()) => { - let prev_priv = cur_privilege; + let prev_priv = cur_privilege; mstatus->SIE() = mstatus.SPIE(); mstatus->SPIE() = true; cur_privilege = if mstatus.SPP() == true then Supervisor else User; @@ -853,7 +959,9 @@ function handle_exception(cur_priv : Privilege, ctl : ctl_result, print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log print("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege); - sepc + + cancel_reservation(); + sepc & pc_alignment_mask() } } } @@ -879,10 +987,12 @@ function handle_illegal() -> unit = { nextPC = handle_exception(cur_privilege, CTL_TRAP(t), PC) } +/* state state initialization */ + function init_sys() -> unit = { cur_privilege = Machine; - mhartid = EXTZ(0b0); + mhartid = EXTZ(0b0); misa->MXL() = arch_to_bits(RV64); misa->A() = true; /* atomics */ @@ -893,9 +1003,9 @@ function init_sys() -> unit = { misa->S() = true; /* supervisor-mode */ /* 64-bit only mode with no extensions */ - mstatus->SXL() = misa.MXL(); - mstatus->UXL() = misa.MXL(); - mstatus->SD() = false; + mstatus->SXL() = misa.MXL(); + mstatus->UXL() = misa.MXL(); + mstatus->SD() = false; mip->bits() = EXTZ(0b0); mie->bits() = EXTZ(0b0); @@ -911,8 +1021,9 @@ function init_sys() -> unit = { mtime = EXTZ(0b0); mcounteren->bits() = EXTZ(0b0); - minstret = EXTZ(0b0); - minstret_written = false; + + minstret = EXTZ(0b0); + minstret_written = false; // log compatibility with spike print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(EXTZ(0b0) : xlenbits) ^ ")") @@ -921,6 +1032,6 @@ function init_sys() -> unit = { /* memory access exceptions, defined here for use by the platform model. */ union MemoryOpResult ('a : Type) = { - MemValue : 'a, - MemException: ExceptionType + MemValue : 'a, + MemException : ExceptionType } diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail index 2991377d..77df74db 100644 --- a/riscv/riscv_types.sail +++ b/riscv/riscv_types.sail @@ -1,7 +1,8 @@ -/* basic types */ +/* Basic type and function definitions used pervasively in the model. */ let xlen = 64 type xlenbits = bits(64) + let xlen_max_unsigned = 2 ^ xlen - 1 let xlen_max_signed = 2 ^ (xlen - 1) - 1 let xlen_min_signed = 0 - 2 ^ (xlen - 1) @@ -9,24 +10,31 @@ let xlen_min_signed = 0 - 2 ^ (xlen - 1) type half = bits(16) type word = bits(32) +/* register identifiers */ + +type regbits = bits(5) +type cregbits = bits(3) /* identifiers in RVC instructions */ +type csreg = bits(12) /* CSR addressing */ + +/* register file indexing */ + type regno ('n : Int), 0 <= 'n < 32 = atom('n) -type regbits = bits(5) -type cregbits = bits(3) -type csreg = bits(12) val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)} function regbits_to_regno b = let 'r = unsigned(b) in r +/* mapping RVC register indices into normal indices */ val creg2reg_bits : cregbits -> regbits function creg2reg_bits(creg) = 0b01 @ creg -/* some arch and ABI relevant registers */ +/* some architecture and ABI relevant register identifiers */ +let zreg : regbits = 0b00000 /* x0, zero register */ +let ra : regbits = 0b00001 /* x1, return address */ +let sp : regbits = 0b00010 /* x2, stack pointer */ -let zreg : regbits = 0b00000 -let ra : regbits = 0b00001 /* x1 */ -let sp : regbits = 0b00010 /* x2 */ +/* program counter */ -register PC : xlenbits +register PC : xlenbits register nextPC : xlenbits /* register file and accessors */ @@ -147,7 +155,7 @@ function wX (r, v) = { overload X = {rX, wX} -/* register name printers */ +/* register names */ val cast reg_name_abi : regbits -> string @@ -191,11 +199,12 @@ function reg_name_abi(r) = { /* instruction fields */ type opcode = bits(7) -type imm12 = bits(12) -type imm20 = bits(20) -type amo = bits(1) +type imm12 = bits(12) +type imm20 = bits(20) +type amo = bits(1) /* amo opcode flags */ /* base architecture definitions */ + enum Architecture = {RV32, RV64, RV128} type arch_xlen = bits(2) function architecture(a : arch_xlen) -> option(Architecture) = @@ -216,14 +225,14 @@ function arch_to_bits(a : Architecture) -> arch_xlen = /* privilege levels */ type priv_level = bits(2) -enum Privilege = {User, Supervisor, Machine} +enum Privilege = {User, Supervisor, Machine} val cast privLevel_to_bits : Privilege -> priv_level function privLevel_to_bits (p) = match (p) { - User => 0b00, + User => 0b00, Supervisor => 0b01, - Machine => 0b11 + Machine => 0b11 } val cast privLevel_of_bits : priv_level -> Privilege @@ -237,35 +246,67 @@ function privLevel_of_bits (p) = val cast privLevel_to_str : Privilege -> string function privLevel_to_str (p) = match (p) { - User => "U", + User => "U", Supervisor => "S", - Machine => "M" + Machine => "M" } -/* access types */ +/* memory access types */ enum AccessType = {Read, Write, ReadWrite, Execute} + val cast accessType_to_str : AccessType -> string function accessType_to_str (a) = match (a) { - Read => "R", - Write => "W", + Read => "R", + Write => "W", ReadWrite => "RW", - Execute => "X" + Execute => "X" } enum ReadType = {Instruction, Data} + val cast readType_to_str : ReadType -> string function readType_to_str (r) = match (r) { Instruction => "I", - Data => "D" + Data => "D" } -/* architectural exception and interrupt definitions */ +enum word_width = {BYTE, HALF, WORD, DOUBLE} + +/* architectural interrupt definitions */ type exc_code = bits(4) +enum InterruptType = { + I_U_Software, + I_S_Software, + I_M_Software, + I_U_Timer, + I_S_Timer, + I_M_Timer, + I_U_External, + I_S_External, + I_M_External +} + +val cast interruptType_to_bits : InterruptType -> exc_code +function interruptType_to_bits (i) = + match (i) { + I_U_Software => 0x0, + I_S_Software => 0x1, + I_M_Software => 0x3, + I_U_Timer => 0x4, + I_S_Timer => 0x5, + I_M_Timer => 0x7, + I_U_External => 0x8, + I_S_External => 0x9, + I_M_External => 0xb + } + +/* architectural exception definitions */ + enum ExceptionType = { E_Fetch_Addr_Align, E_Fetch_Access_Fault, @@ -288,87 +329,50 @@ enum ExceptionType = { val cast exceptionType_to_bits : ExceptionType -> exc_code function exceptionType_to_bits(e) = match (e) { - E_Fetch_Addr_Align => 0x0, + E_Fetch_Addr_Align => 0x0, E_Fetch_Access_Fault => 0x1, - E_Illegal_Instr => 0x2, - E_Breakpoint => 0x3, - E_Load_Addr_Align => 0x4, - E_Load_Access_Fault => 0x5, - E_SAMO_Addr_Align => 0x6, - E_SAMO_Access_Fault => 0x7, - E_U_EnvCall => 0x8, - E_S_EnvCall => 0x9, - E_Reserved_10 => 0xa, - E_M_EnvCall => 0xb, - E_Fetch_Page_Fault => 0xc, - E_Load_Page_Fault => 0xd, - E_Reserved_14 => 0xe, - E_SAMO_Page_Fault => 0xf + E_Illegal_Instr => 0x2, + E_Breakpoint => 0x3, + E_Load_Addr_Align => 0x4, + E_Load_Access_Fault => 0x5, + E_SAMO_Addr_Align => 0x6, + E_SAMO_Access_Fault => 0x7, + E_U_EnvCall => 0x8, + E_S_EnvCall => 0x9, + E_Reserved_10 => 0xa, + E_M_EnvCall => 0xb, + E_Fetch_Page_Fault => 0xc, + E_Load_Page_Fault => 0xd, + E_Reserved_14 => 0xe, + E_SAMO_Page_Fault => 0xf } val cast exceptionType_to_str : ExceptionType -> string function exceptionType_to_str(e) = match (e) { - E_Fetch_Addr_Align => "fisaligned-fetch", + E_Fetch_Addr_Align => "misaligned-fetch", E_Fetch_Access_Fault => "fetch-access-fault", - E_Illegal_Instr => "illegal-instruction", - E_Breakpoint => "breakpoint", - E_Load_Addr_Align => "misaligned-load", - E_Load_Access_Fault => "load-access-fault", - E_SAMO_Addr_Align => "misaliged-store/amo", - E_SAMO_Access_Fault => "store/amo-access-fault", - E_U_EnvCall => "u-call", - E_S_EnvCall => "s-call", - E_Reserved_10 => "reserved-0", - E_M_EnvCall => "m-call", - E_Fetch_Page_Fault => "fetch-page-fault", - E_Load_Page_Fault => "load-page-fault", - E_Reserved_14 => "reserved-1", - E_SAMO_Page_Fault => "store/amo-page-fault" - } - -enum InterruptType = { - I_U_Software, - I_S_Software, - I_M_Software, - I_U_Timer, - I_S_Timer, - I_M_Timer, - I_U_External, - I_S_External, - I_M_External -} - -val cast interruptType_to_bits : InterruptType -> exc_code -function interruptType_to_bits (i) = - match (i) { - I_U_Software => 0x0, - I_S_Software => 0x1, - I_M_Software => 0x3, - I_U_Timer => 0x4, - I_S_Timer => 0x5, - I_M_Timer => 0x7, - I_U_External => 0x8, - I_S_External => 0x9, - I_M_External => 0xb - } - -type tv_mode = bits(2) -enum TrapVectorMode = {TV_Direct, TV_Vector, TV_Reserved} - -val cast trapVectorMode_of_bits : tv_mode -> TrapVectorMode -function trapVectorMode_of_bits (m) = - match (m) { - 0b00 => TV_Direct, - 0b01 => TV_Vector, - _ => TV_Reserved + E_Illegal_Instr => "illegal-instruction", + E_Breakpoint => "breakpoint", + E_Load_Addr_Align => "misaligned-load", + E_Load_Access_Fault => "load-access-fault", + E_SAMO_Addr_Align => "misaliged-store/amo", + E_SAMO_Access_Fault => "store/amo-access-fault", + E_U_EnvCall => "u-call", + E_S_EnvCall => "s-call", + E_Reserved_10 => "reserved-0", + E_M_EnvCall => "m-call", + E_Fetch_Page_Fault => "fetch-page-fault", + E_Load_Page_Fault => "load-page-fault", + E_Reserved_14 => "reserved-1", + E_SAMO_Page_Fault => "store/amo-page-fault" } -/* other exceptions */ +/* model-internal exceptions */ union exception = { Error_not_implemented : string, - Error_internal_error : unit + Error_internal_error : unit } val not_implemented : forall ('a : Type). string -> 'a effect {escape} @@ -380,6 +384,19 @@ function internal_error(s) = { throw Error_internal_error() } +/* trap modes */ + +type tv_mode = bits(2) +enum TrapVectorMode = {TV_Direct, TV_Vector, TV_Reserved} + +val cast trapVectorMode_of_bits : tv_mode -> TrapVectorMode +function trapVectorMode_of_bits (m) = + match (m) { + 0b00 => TV_Direct, + 0b01 => TV_Vector, + _ => TV_Reserved + } + /* extension context status */ type ext_status = bits(2) @@ -388,10 +405,10 @@ enum ExtStatus = {Off, Initial, Clean, Dirty} val cast extStatus_to_bits : ExtStatus -> ext_status function extStatus_to_bits(e) = match (e) { - Off => 0b00, + Off => 0b00, Initial => 0b01, - Clean => 0b10, - Dirty => 0b11 + Clean => 0b10, + Dirty => 0b11 } val cast extStatus_of_bits : ext_status -> ExtStatus @@ -410,24 +427,32 @@ enum SATPMode = {Sbare, Sv32, Sv39} function satpMode_of_bits(a : Architecture, m : satp_mode) -> option(SATPMode) = match (a, m) { - (_, 0x0) => Some(Sbare), + (_, 0x0) => Some(Sbare), (RV32, 0x1) => Some(Sv32), (RV64, 0x8) => Some(Sv39), (_, _) => None() } /* CSR access control bits (from CSR addresses) */ + type csrRW = bits(2) /* read/write */ -enum uop = {RISCV_LUI, RISCV_AUIPC} /* upper immediate ops */ -enum bop = {RISCV_BEQ, RISCV_BNE, RISCV_BLT, RISCV_BGE, RISCV_BLTU, RISCV_BGEU} /* branch ops */ -enum iop = {RISCV_ADDI, RISCV_SLTI, RISCV_SLTIU, RISCV_XORI, RISCV_ORI, RISCV_ANDI} /* immediate ops */ -enum sop = {RISCV_SLLI, RISCV_SRLI, RISCV_SRAI} /* shift ops */ -enum rop = {RISCV_ADD, RISCV_SUB, RISCV_SLL, RISCV_SLT, RISCV_SLTU, RISCV_XOR, RISCV_SRL, RISCV_SRA, RISCV_OR, RISCV_AND} /* reg-reg ops */ -enum ropw = {RISCV_ADDW, RISCV_SUBW, RISCV_SLLW, RISCV_SRLW, RISCV_SRAW} /* reg-reg 32-bit ops */ -enum amoop = {AMOSWAP, AMOADD, AMOXOR, AMOAND, AMOOR, AMOMIN, AMOMAX, AMOMINU, AMOMAXU} /* AMO ops */ -enum csrop = {CSRRW, CSRRS, CSRRC} -enum word_width = {BYTE, HALF, WORD, DOUBLE} +/* instruction opcode grouping */ +enum uop = {RISCV_LUI, RISCV_AUIPC} /* upper immediate ops */ +enum bop = {RISCV_BEQ, RISCV_BNE, RISCV_BLT, + RISCV_BGE, RISCV_BLTU, RISCV_BGEU} /* branch ops */ +enum iop = {RISCV_ADDI, RISCV_SLTI, RISCV_SLTIU, + RISCV_XORI, RISCV_ORI, RISCV_ANDI} /* immediate ops */ +enum sop = {RISCV_SLLI, RISCV_SRLI, RISCV_SRAI} /* shift ops */ +enum rop = {RISCV_ADD, RISCV_SUB, RISCV_SLL, RISCV_SLT, + RISCV_SLTU, RISCV_XOR, RISCV_SRL, RISCV_SRA, + RISCV_OR, RISCV_AND} /* reg-reg ops */ + +enum ropw = {RISCV_ADDW, RISCV_SUBW, RISCV_SLLW, + RISCV_SRLW, RISCV_SRAW} /* reg-reg 32-bit ops */ +enum amoop = {AMOSWAP, AMOADD, AMOXOR, AMOAND, AMOOR, + AMOMIN, AMOMAX, AMOMINU, AMOMAXU} /* AMO ops */ +enum csrop = {CSRRW, CSRRS, CSRRC} /* CSR ops */ /* mappings for assembly */ @@ -468,31 +493,30 @@ mapping reg_name = { } val sep : unit <-> string -mapping sep = { - () <-> opt_spc() ^ "," ^ def_spc() +mapping sep : unit <-> string = { + () <-> opt_spc() ^ "," ^ def_spc() } mapping bool_bits : bool <-> bits(1) = { - true <-> 0b1, - false <-> 0b0 + true <-> 0b1, + false <-> 0b0 } mapping bool_not_bits : bool <-> bits(1) = { - true <-> 0b0, - false <-> 0b1 + true <-> 0b0, + false <-> 0b1 } - mapping size_bits : word_width <-> bits(2) = { - BYTE <-> 0b00, - HALF <-> 0b01, - WORD <-> 0b10, + BYTE <-> 0b00, + HALF <-> 0b01, + WORD <-> 0b10, DOUBLE <-> 0b11 } mapping size_mnemonic : word_width <-> string = { - BYTE <-> "b", - HALF <-> "h", - WORD <-> "w", + BYTE <-> "b", + HALF <-> "h", + WORD <-> "w", DOUBLE <-> "d" } diff --git a/riscv/riscv_vmem.sail b/riscv/riscv_vmem.sail index 9d0f42d1..caafb131 100644 --- a/riscv/riscv_vmem.sail +++ b/riscv/riscv_vmem.sail @@ -1,3 +1,5 @@ +/* Supervisor-mode address translation and page-table walks. */ + /* PageSize */ let PAGESIZE_BITS = 12 @@ -29,23 +31,23 @@ function isInvalidPTE(p : pteAttribs) -> bool = { 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, 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, + (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, + (Execute, Supervisor) => p.U() == false & p.X() == true, - (_, Machine) => internal_error("m-mode mem perm check") + (_, 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; - let update_a = p.A() == false; + 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(p, true) else np; @@ -61,21 +63,33 @@ enum PTW_Error = { 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 = +function translationException(a : AccessType, f : PTW_Error) -> ExceptionType = { + let e : ExceptionType = match (a, f) { - (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, - /* atomics never raise Load exceptions */ (ReadWrite, PTW_Access) => E_SAMO_Access_Fault, - (ReadWrite, _) => E_SAMO_Page_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 @@ -131,20 +145,34 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) -> PTW_Result 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 memory-backed addresses. */ - match (phys_mem_read(Data, EXTZ(pte_addr), 8)) { - MemException(_) => PTW_Failure(PTW_Access), + /* 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 */ @@ -152,6 +180,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) -> PTW_Result } } 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 */ @@ -159,14 +188,20 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) -> PTW_Result 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) } } @@ -212,7 +247,6 @@ function make_TLB39_Entry(asid, global, vAddr, pAddr, pte, level, pteAddr) = { } /* TODO: make this a vector or array of entries */ -let TLBEntries = 32 register tlb39 : option(TLB39_Entry) val lookupTLB39 : (asid64, vaddr39) -> option((int, TLB39_Entry)) effect {rreg} @@ -229,7 +263,7 @@ function lookupTLB39(asid, vaddr) = { 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) + tlb39 = Some(ent) } function writeTLB39(idx : int, ent : TLB39_Entry) -> unit = @@ -354,12 +388,12 @@ val translateAddr : (xlenbits, AccessType, ReadType) -> TR_Result effect {escape 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 + 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 mxr : bool = mstatus.MXR() == true; + let do_sum : bool = mstatus.SUM() == true; let mode : SATPMode = translationMode(effPriv); match mode { Sbare => TR_Address(vAddr), diff --git a/riscv/tracecmp.ml b/riscv/tracecmp.ml index c4f718a2..64a918d5 100644 --- a/riscv/tracecmp.ml +++ b/riscv/tracecmp.ml @@ -27,6 +27,15 @@ type tick = { time : int64 } +type htif = { + tohost : int64 +} + +type ld_res = + | Res_make of int64 + | Res_match of int64 * int64 + | Res_cancel + type line = | L_none | L_inst of inst @@ -34,6 +43,8 @@ type line = | L_csr_read of csr_read | L_csr_write of csr_write | L_tick of tick + | L_htif of htif + | L_ld_res of ld_res let inst_count = ref 0 @@ -123,6 +134,57 @@ let parse_tick l = let sprint_tick t = Printf.sprintf "clint::tick mtime <- 0x%Lx" t.time +(* htif tick + htif::tick 0x1 + *) + +let parse_htif l = + try Scanf.sscanf l " htif::tick 0x%Lx" + (fun tohost -> L_htif { tohost }) + with + | Scanf.Scan_failure _ -> L_none + | End_of_file -> L_none + +let sprint_htif t = + Printf.sprintf "htif::tick 0x%Lx" t.tohost + +(* Load reservations: + make: reservation <- 0x80002008 + match: reservation: 0xffffffffffffffff, key=0x80002008 + cancel: reservation <- none + + *) +let parse_ldres_match l = + try Scanf.sscanf + l " reservation: 0x%Lx, key=0x%Lx" + (fun res key -> L_ld_res (Res_match (res, key))) + with + | Scanf.Scan_failure _ -> L_none + | End_of_file -> L_none + +let parse_ldres_match_sail l = + try Scanf.sscanf + l " reservation: none, key=0x%Lx" + (fun key -> L_ld_res (Res_match (Int64.minus_one, key))) + with + | Scanf.Scan_failure _ -> L_none + | End_of_file -> L_none + +let parse_ldres_change l = + try if l = "reservation <- none" + then L_ld_res Res_cancel + else Scanf.sscanf + l " reservation <- 0x%Lx" + (fun res -> L_ld_res (Res_make res)) + with + | Scanf.Scan_failure _ -> L_none + | End_of_file -> L_none + +let sprint_ldres = function + | Res_make res -> Printf.sprintf "reservation <- 0x%Lx" res + | Res_match (res, key) -> Printf.sprintf "reservation: 0x%Lx, key=0x%Lx" res key + | Res_cancel -> Printf.sprintf "reservation <- none" + (* scanners *) let popt p l = function @@ -131,10 +193,11 @@ let popt p l = function let parse_line l = parse_csr_read l |> popt parse_csr_write l - |> popt parse_reg_write l |> popt parse_tick l + |> popt parse_reg_write l |> popt parse_tick l |> popt parse_htif l + |> popt parse_ldres_change l |> popt parse_ldres_match l let parse_sail_line l = - parse_line l |> popt parse_sail_inst l + parse_line l |> popt parse_sail_inst l |> popt parse_ldres_match_sail l let parse_spike_line l = parse_line l |> popt parse_spike_inst l @@ -147,6 +210,8 @@ let sprint_line = function | L_csr_read r -> Printf.sprintf "<%d> %s" !inst_count (sprint_csr_read r) | L_csr_write r -> Printf.sprintf "<%d> %s" !inst_count (sprint_csr_write r) | L_tick t -> Printf.sprintf "<%d> %s" !inst_count (sprint_tick t) + | L_htif t -> Printf.sprintf "<%d> %s" !inst_count (sprint_htif t) + | L_ld_res r -> Printf.sprintf "<%d> %s" !inst_count (sprint_ldres r) (* file processing *) |