Add minimal support for emulated Altera JTAG UART.

6 files changed, 127 insertions, 6 deletions

diff --git a/cheri/cheri_prelude.sail b/cheri/cheri_prelude.sail
index 9f39496f..23973782 100644
--- a/cheri/cheri_prelude.sail
+++ b/cheri/cheri_prelude.sail
@@ -431,6 +431,12 @@ function bool MEMw_tagged_conditional((bit[64]) addr, (bool) tag, (bit[cap_size_
 }
 
 function unit effect {wmem} MEMw_wrapper(addr, size, data) =
+  if (addr == 0x000000007f000000) then
+  {
+    UART_WDATA   := data[31..24];
+    UART_WRITTEN := 1;
+  }
+  else
   {
     (* On cheri non-capability writes must clear the corresponding tag*)
     TAGw((addr[63..5] : 0b00000), 0x00);
diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail
index f93309ed..e1f8d8e0 100644
--- a/mips/mips_insts.sail
+++ b/mips/mips_insts.sail
@@ -1118,7 +1118,7 @@ function clause execute (Load(width, signed, linked, base, rt, offset)) =
                   MEMr_reserve(pAddr, wordWidthBytes(width));
                 }
               else
-                MEMr(pAddr, wordWidthBytes(width));
+                MEMr_wrapper(pAddr, wordWidthBytes(width));
             if (signed) then
               wGPR(rt) := EXTS(memResult)
             else
@@ -1185,7 +1185,7 @@ function clause execute(LWL(base, rt, offset)) =
         (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, W);
         let pAddr = (TLBTranslate(vAddr, LoadData)) in
           {
-            mem_val   := MEMr (pAddr[63..2] : 0b00, 4); (* read word of interest *)
+            mem_val   := MEMr_wrapper (pAddr[63..2] : 0b00, 4); (* read word of interest *)
             reg_val   := rGPR(rt);
             wGPR(rt)  := EXTS(switch(vAddr[1..0])
               {
@@ -1205,7 +1205,7 @@ function clause execute(LWR(base, rt, offset)) =
         (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, W);
         let pAddr = (TLBTranslate(vAddr, LoadData)) in
           {
-            mem_val   := MEMr (pAddr[63..2] : 0b00, 4); (* read word of interest *)
+            mem_val   := MEMr_wrapper (pAddr[63..2] : 0b00, 4); (* read word of interest *)
             reg_val   := rGPR(rt);
             wGPR(rt)  := EXTS(switch(vAddr[1..0]) (* it is acceptable to sign extend in all cases *)
               {
@@ -1269,7 +1269,7 @@ function clause execute(LDL(base, rt, offset)) =
     (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, D);
     let pAddr = (TLBTranslate(vAddr, StoreData)) in
       {
-        mem_val   := MEMr (pAddr[63..3] : 0b000, 8); (* read double of interest *)
+        mem_val   := MEMr_wrapper (pAddr[63..3] : 0b000, 8); (* read double of interest *)
         reg_val   := rGPR(rt);
         wGPR(rt)  := switch(vAddr[2..0])
               {
@@ -1295,7 +1295,7 @@ function clause execute(LDR(base, rt, offset)) =
     (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, D);
     let pAddr = (TLBTranslate(vAddr, StoreData)) in
       {
-        mem_val   := MEMr (pAddr[63..3] : 0b000, 8); (* read double of interest *)
+        mem_val   := MEMr_wrapper (pAddr[63..3] : 0b000, 8); (* read double of interest *)
         reg_val   := rGPR(rt);
         wGPR(rt)  := switch(vAddr[2..0])
               {
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index a490efb9..5472ae84 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -221,6 +221,13 @@ let (vector <0, 32, inc, (register<(bit[64])>) >) GPR =
   GPR21, GPR22, GPR23, GPR24, GPR25, GPR26, GPR27, GPR28, GPR29, GPR30, GPR31
   ]
 
+(* JTAG Uart registers *)
+
+register (bit[8]) UART_WDATA
+register (bit[1]) UART_WRITTEN
+register (bit[8]) UART_RDATA
+register (bit[1]) UART_RVALID
+
 (* Check whether a given 64-bit vector is a properly sign extended 32-bit word *)
 val bit[64] -> bool effect pure NotWordVal
 function bool NotWordVal (word) = 
@@ -539,3 +546,16 @@ function bool isAddressAligned(addr, (WordType) wordType) =
     case D -> (addr[2..0] == 0b000)
   }
 
+function forall Nat 'n. (bit[8 * 'n]) effect { rmem } MEMr_wrapper ((bit[64]) addr, ([:'n:]) size) =
+    if (addr == 0x000000007f000000) then
+      {
+        let rvalid = (bit[1]) UART_RVALID in
+        {
+          UART_RVALID := [bitzero];
+          mask(0x00000000 : UART_RDATA : [rvalid] : 0b0000000 : 0x0000)
+        }
+      }
+    else if (addr == 0x000000007f000004) then
+      mask(0x000000000004ffff) (* Always plenty of write space available and jtag activity *)
+    else
+      MEMr(addr, size)
diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail
index e8b17a29..03d03cec 100644
--- a/mips/mips_wrappers.sail
+++ b/mips/mips_wrappers.sail
@@ -35,7 +35,15 @@
 (* mips_wrappers.sail: wrappers functions and hooks for CHERI extensibility 
    (mostly identity functions here) *)
 
-function unit effect {wmem} MEMw_wrapper(addr, size, data) = MEMw(addr, size, data)
+function unit effect {wmem} MEMw_wrapper(addr, size, data) = 
+    if (addr == 0x000000007f000000) then
+      {
+        UART_WDATA   := data[31..24];
+        UART_WRITTEN := 1;
+      }
+    else
+      MEMw(addr, size, data)
+
 function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) =
   MEMw_conditional(addr, size, data)
 
diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml
index 4a3625ed..5e238750 100644
--- a/src/lem_interp/run_with_elf.ml
+++ b/src/lem_interp/run_with_elf.ml
@@ -25,6 +25,7 @@ let data_mem = (ref Mem.empty : (memory_byte Run_interp_model.Mem.t) ref) ;;
 let prog_mem = (ref Mem.empty : (memory_byte Run_interp_model.Mem.t) ref) ;;
 let tag_mem  = (ref Mem.empty : (memory_byte Run_interp_model.Mem.t) ref);;
 let reg = ref Reg.empty ;;
+let input_buf = (ref [] : int list ref);;
 
 let add_mem byte addr mem =
   assert(byte >= 0 && byte < 256);
@@ -519,6 +520,11 @@ let mips_register_data_all =  [
   ("TLBEntry05" ,(D_decreasing, 117, 116));
   ("TLBEntry06" ,(D_decreasing, 117, 116));
   ("TLBEntry07" ,(D_decreasing, 117, 116));
+
+  ("UART_WDATA" ,(D_decreasing, 8, 7));
+  ("UART_RDATA" ,(D_decreasing, 8, 7));
+  ("UART_WRITTEN" ,(D_decreasing, 1, 0));
+  ("UART_RVALID" ,(D_decreasing, 1, 0));
 ]
 
 let initial_stack_and_reg_data_of_MIPS_elf_file e_entry all_data_memory =
@@ -1060,6 +1066,38 @@ let rec fde_loop count context model mode track_dependencies addr_trans =
                 reg := my_reg;
                 prog_mem := my_mem;
                 tag_mem := my_tags;
+                
+                (try
+                  let (pending, _, _)  = (Unix.select [(Unix.stdin)] [] [] 0.0) in
+                  (if (pending != []) then
+                    let char = (input_byte stdin) in (
+                    errorf "Input %x\n" char;
+                    input_buf := (!input_buf) @ [char]));
+                with
+                | _ -> ());
+
+                let uart_rvalid = option_int_of_reg "UART_RVALID" in
+                (match uart_rvalid with
+                | Some 0 ->
+                  (match !input_buf with
+                  | x :: xs -> (
+                      reg := Reg.add "UART_RDATA" (register_value_of_integer 8 7 Interp_interface.D_decreasing (Nat_big_num.of_int x)) !reg;
+                      reg := Reg.add "UART_RVALID" (register_value_of_integer 1 0 Interp_interface.D_decreasing (Nat_big_num.of_int 1)) !reg;
+                      input_buf := xs;
+                    )
+                  | [] -> ())
+                | _-> ());
+
+                let uart_written = option_int_of_reg "UART_WRITTEN" in
+                (match uart_written with 
+                | Some 1 ->
+                  (let uart_data = option_int_of_reg "UART_WDATA" in
+                  match uart_data with
+                  | Some b -> (printf "%c" (Char.chr b); printf "%!")
+                  | None   -> (errorf "UART_WDATA was undef" ; exit 1))
+                | _      -> ());
+                reg := Reg.add "UART_WRITTEN" (register_value_of_integer 1 0 Interp_interface.D_decreasing Nat_big_num.zero) !reg;
+                
                 reg := Reg.add "inBranchDelay" (Reg.find "branchPending" !reg) !reg;
                 reg := Reg.add "branchPending" (register_value_of_integer 1 0 Interp_interface.D_decreasing Nat_big_num.zero) !reg;
                 reg := Reg.add "PC" (Reg.find "nextPC" !reg) !reg;
@@ -1113,4 +1151,10 @@ let run () =
   let t = time_it (fun () -> fde_loop 0 context isa_model (Some Run) (ref false)  addr_trans) () in
   resultf "Execution time for file %s: %f seconds\n" name t;;
 
+(* Turn off line-buffering of standard input to allow responsive console input *)
+if Unix.isatty (Unix.stdin) then begin
+  let tattrs = Unix.tcgetattr (Unix.stdin) in
+  Unix.tcsetattr (Unix.stdin) (Unix.TCSANOW) ({tattrs with c_icanon=false})
+end ;;
+
 run () ;;
diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml
index 1ec6ecbe..56b9807b 100644
--- a/src/lem_interp/run_with_elf_cheri.ml
+++ b/src/lem_interp/run_with_elf_cheri.ml
@@ -25,6 +25,7 @@ let data_mem = (ref Mem.empty : (memory_byte Run_interp_model.Mem.t) ref) ;;
 let prog_mem = (ref Mem.empty : (memory_byte Run_interp_model.Mem.t) ref) ;;
 let tag_mem  = (ref Mem.empty : (memory_byte Run_interp_model.Mem.t) ref);;
 let reg = ref Reg.empty ;;
+let input_buf = (ref [] : int list ref);;
 
 let add_mem byte addr mem =
   assert(byte >= 0 && byte < 256);
@@ -519,6 +520,10 @@ let mips_register_data_all =  [
   ("TLBEntry05" ,(D_decreasing, 117, 116));
   ("TLBEntry06" ,(D_decreasing, 117, 116));
   ("TLBEntry07" ,(D_decreasing, 117, 116));
+  ("UART_WDATA" ,(D_decreasing, 8, 7));
+  ("UART_RDATA" ,(D_decreasing, 8, 7));
+  ("UART_WRITTEN" ,(D_decreasing, 1, 0));
+  ("UART_RVALID" ,(D_decreasing, 1, 0));
 ]
 
 let cheri_register_data_all = mips_register_data_all @ [
@@ -1151,6 +1156,38 @@ let rec fde_loop count context model mode track_dependencies addr_trans =
                 reg := my_reg;
                 prog_mem := my_mem;
                 tag_mem := my_tags;
+                
+                (try
+                  let (pending, _, _)  = (Unix.select [(Unix.stdin)] [] [] 0.0) in
+                  (if (pending != []) then
+                    let char = (input_byte stdin) in (
+                    errorf "Input %x\n" char;
+                    input_buf := (!input_buf) @ [char]));
+                with
+                | _ -> ());
+
+                let uart_rvalid = option_int_of_reg "UART_RVALID" in
+                (match uart_rvalid with
+                | Some 0 ->
+                  (match !input_buf with
+                  | x :: xs -> (
+                      reg := Reg.add "UART_RDATA" (register_value_of_integer 8 7 Interp_interface.D_decreasing (Nat_big_num.of_int x)) !reg;
+                      reg := Reg.add "UART_RVALID" (register_value_of_integer 1 0 Interp_interface.D_decreasing (Nat_big_num.of_int 1)) !reg;
+                      input_buf := xs;
+                    )
+                  | [] -> ())
+                | _-> ());
+
+                let uart_written = option_int_of_reg "UART_WRITTEN" in
+                (match uart_written with 
+                | Some 1 ->
+                  (let uart_data = option_int_of_reg "UART_WDATA" in
+                  match uart_data with
+                  | Some b -> (printf "%c" (Char.chr b); printf "%!")
+                  | None   -> (errorf "UART_WDATA was undef" ; exit 1))
+                | _      -> ());
+                reg := Reg.add "UART_WRITTEN" (register_value_of_integer 1 0 Interp_interface.D_decreasing Nat_big_num.zero) !reg;
+
                 reg := Reg.add "inBranchDelay" (Reg.find "branchPending" !reg) !reg;
                 reg := Reg.add "branchPending" (register_value_of_integer 1 0 Interp_interface.D_decreasing Nat_big_num.zero) !reg;
                 reg := Reg.add "PC" (Reg.find "nextPC" !reg) !reg;
@@ -1206,4 +1243,10 @@ let run () =
   let t = time_it (fun () -> fde_loop 0 context isa_model (Some Run) (ref false)  addr_trans) () in
   resultf "Execution time for file %s: %f seconds\n" name t;;
 
+(* Turn off line-buffering of standard input to allow responsive console input *)
+if Unix.isatty (Unix.stdin) then begin
+  let tattrs = Unix.tcgetattr (Unix.stdin) in
+  Unix.tcsetattr (Unix.stdin) (Unix.TCSANOW) ({tattrs with c_icanon=false})
+end ;;
+
 run () ;;