diff options
| -rw-r--r-- | riscv/platform.ml | 9 | ||||
| -rw-r--r-- | riscv/platform_impl.ml | 11 | ||||
| -rw-r--r-- | riscv/riscv_extras.lem | 8 | ||||
| -rw-r--r-- | riscv/riscv_platform.sail | 12 |
4 files changed, 36 insertions, 4 deletions
diff --git a/riscv/platform.ml b/riscv/platform.ml index 919900f4..485acb76 100644 --- a/riscv/platform.ml +++ b/riscv/platform.ml @@ -74,6 +74,15 @@ let rom_size () = bits_of_int !rom_size_ref let dram_base () = bits_of_int64 P.dram_base let dram_size () = bits_of_int64 P.dram_size +(* 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)) + +let term_read () = + let c = P.term_read () in + bits_of_int (int_of_char c) + (* returns starting value for PC, i.e. start of reset vector *) let init elf_file = Elf.load_elf elf_file; diff --git a/riscv/platform_impl.ml b/riscv/platform_impl.ml index 1d2037a6..9b063404 100644 --- a/riscv/platform_impl.ml +++ b/riscv/platform_impl.ml @@ -143,6 +143,17 @@ let make_dtb dts = (* Call the dtc compiler, assumed to be at /usr/bin/dtc *) (Printf.printf "%s\n" ("Error executing dtc: " ^ fn ^ ": " ^ Unix.error_message e); exit 1) +(* Terminal I/O *) + +let term_write char = + ignore (Unix.write_substring Unix.stdout (String.make 1 char) 0 1) + +let rec term_read () = + let buf = Bytes.make 1 '\000' in + let nbytes = Unix.read Unix.stdin buf 0 1 in + (* todo: handle nbytes == 0 *) + buf.[0] + (* let save_string_to_file s fname = let out = open_out fname in diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem index 7e217d74..553b7508 100644 --- a/riscv/riscv_extras.lem +++ b/riscv/riscv_extras.lem @@ -68,6 +68,14 @@ val plat_clint_size : forall 'a. Size 'a => unit -> bitvector 'a let plat_clint_size () = wordFromInteger 0 declare ocaml target_rep function plat_clint_size = `Platform.clint_size` +val plat_term_write : forall 'a. Size 'a => bitvector 'a -> unit +let plat_term_write _ = () +declare ocaml target_rep function plat_term_write = `Platform.term_write` + +val plat_term_read : forall 'a. Size 'a => unit -> bitvector 'a +let plat_term_read () = wordFromInteger 0 +declare ocaml target_rep function plat_term_read = `Platform.term_read` + val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a let shift_bits_right v m = shiftr v (uint m) val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail index f3911ba9..a002341a 100644 --- a/riscv/riscv_platform.sail +++ b/riscv/riscv_platform.sail @@ -70,7 +70,12 @@ function clint_store(addr, width, data) = { } else MemException(E_SAMO_Access_Fault) } -/* Spike's HTIF device interface. */ +/* Basic terminal character I/O. */ + +val plat_term_write = {ocaml: "Platform.term_write", lem: "plat_term_write"} : bits(8) -> unit +val plat_term_read = {ocaml: "Platform.term_read", lem: "plat_term_read"} : unit -> bits(8) + +/* Spike's HTIF device interface, which multiplexes the above MMIO devices. */ bitfield htif_cmd : bits(64) = { device : 63 .. 56, @@ -81,7 +86,6 @@ bitfield htif_cmd : bits(64) = { register htif_done : bool register htif_exit_code : xlenbits -// no support yet for terminal input val htif_load : forall 'n, 0 < 'n <= 64. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) function htif_load(addr, width) = MemValue(EXTZ(0b0)) @@ -103,8 +107,8 @@ function htif_store(addr, width, data) = { }, 0x01 => { /* terminal */ match cmd.cmd() { - 0x00 => /* input */ (), - 0x01 => /* TODO: output data */ (), + 0x00 => /* TODO: terminal input handling */ (), + 0x01 => plat_term_write(cmd.payload()[7..0]), c => print("Unknown term cmd: " ^ BitStr(c)) } }, |