Initial top-level support for compression instructions.

- introduce the misa register
- check the appropriate instruction bits to decide whether it is compressed
- check misa.C to decide whether we can execute compressed instructions
- add a decodeCompressed function
- add two of the most basic RVC instructions: NOP and ILLEGAL

3 files changed, 84 insertions, 5 deletions

diff --git a/riscv/main.sail b/riscv/main.sail
index cc6bb90c..ce749d94 100644
--- a/riscv/main.sail
+++ b/riscv/main.sail
@@ -6,12 +6,29 @@ function fetch_and_execute () =
   let tohost = __GetSlice_int(64, elf_tohost(), 0) in
   while true do {
     print_bits("PC: ", PC);
+
+    /* for now, always fetch a 32-bit value.  this would need to
+       change with privileged mode, since we could cross a page
+       boundary with PC only 16-bit aligned in C mode.  */
     let instr = __RISCV_read(PC, 4);
-    nextPC = PC + 4;
-    let instr_ast = decode(instr);
-    match instr_ast {
-      Some(ast) => execute(ast),
-      None      => {print("Decode failed"); exit (())}
+
+    let (instr_ast, instr_sz) : (option(ast), int)=
+       match (instr[1 .. 0]) {
+         0b11 => (decode(instr), 4),
+	 _    => (decodeCompressed(instr[15 .. 0]), 2)
+       };
+    /* check whether a compressed instruction is legal. */
+    if (misa.C() == 0b0 & (instr_sz == 2)) then {
+      let t : sync_exception =
+      struct { trap = Illegal_Instr,
+               badaddr = Some (EXTZ(instr)) } in
+      nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
+    } else {
+      nextPC = PC + instr_sz;
+      match instr_ast {
+        Some(ast) => execute(ast),
+        None      => {print("Decode failed"); exit (())}
+      }
     };
     let tohost_val = __RISCV_read(tohost, 4);
     if unsigned(tohost_val) != 0 then {
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index 9ec5734e..acd4839d 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -3,6 +3,10 @@ scattered union ast
 val decode : bits(32) -> option(ast) effect pure
 scattered function decode
 
+val decodeCompressed : bits(16) -> option(ast) effect pure
+scattered function decodeCompressed
+
+
 val execute : ast -> unit effect {escape, wreg, rreg, wmv, eamem, rmem, barr, exmem}
 scattered function execute
 
@@ -503,8 +507,34 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) =
 
 /* ****************************************************************** */
 
+union clause ast = NOP
+
+function clause decodeCompressed (0b000 @ nzi1 : bits(1) @ 0b00000 @ (nzi0 : bits(5)) @ 0b01) : bits(16) = {
+  if (and_bool((nzi1 == 0b0), (nzi0 == 0b00000)))
+  then None
+  else Some(NOP)
+}
+
+function clause execute (NOP) = ()
+
+/* ****************************************************************** */
+
+union clause ast = ILLEGAL
+
+function clause decodeCompressed (0b0000 @ 0b00000 @ 0b00000 @ 0b01) : bits(16) = Some(ILLEGAL)
+
+function clause execute (ILLEGAL) = {
+  let t : sync_exception =
+  struct { trap = Illegal_Instr,
+           badaddr = Some (EXTZ(0b0)) } in
+  nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
+}
+
+/* ****************************************************************** */
+
 function clause decode _ = None
 
 end ast
 end decode
+end decodeCompressed
 end execute
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index 0eaadec4..bd37b297 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -68,6 +68,38 @@ function exc_to_bits e =
 
 /* FIXME: currently we have only those used by riscv-tests. */
 
+bitfield Misa : bits(64) = {
+  MXL  : 63 .. 62,
+
+  Z    : 25,
+  Y    : 24,
+  X    : 23,
+  W    : 22,
+  V    : 21,
+  U    : 20,
+  T    : 19,
+  S    : 18,
+  R    : 17,
+  Q    : 16,
+  P    : 15,
+  O    : 14,
+  N    : 13,
+  M    : 12,
+  L    : 11,
+  K    : 10,
+  J    : 9,
+  I    : 8,
+  H    : 7,
+  G    : 6,
+  F    : 5,
+  E    : 4,
+  D    : 3,
+  C    : 2,
+  B    : 1,
+  A    : 0
+}
+register misa : Misa
+
 bitfield Mstatus : bits(64) = {
   SD   : 63,