Add terminal output to riscv platform, with incomplete handling of input.

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))
       }
     },