Merge pull request #458 from Alasdair/interface

RVWMO support via Sail concurrency interface

1 files changed, 0 insertions, 367 deletions

diff --git a/model/riscv_analysis.sail b/model/riscv_analysis.sail
deleted file mode 100644
index 0d72bed..0000000
--- a/model/riscv_analysis.sail
+++ /dev/null
@@ -1,367 +0,0 @@
-/*=======================================================================================*/
-/*  This Sail RISC-V architecture model, comprising all files and                        */
-/*  directories except where otherwise noted is subject the BSD                          */
-/*  two-clause license in the LICENSE file.                                              */
-/*                                                                                       */
-/*  SPDX-License-Identifier: BSD-2-Clause                                                */
-/*=======================================================================================*/
-
-$include <regfp.sail>
-
-/* in reverse order because inc vectors don't seem to work (bug) */
-let GPRstrs : 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"
-  ]
-
-function GPRstr(i: bits(5)) -> string = GPRstrs[unsigned(i)]
-
-let CIA_fp = RFull("CIA")
-let NIA_fp = RFull("NIA")
-
-$ifndef FEATURE_UNION_BARRIER
-
-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 == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-     },
-     RISCV_JAL(imm, rd) => {
-            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-            let offset : bits(64) = sign_extend(imm) in
-            Nias = [| NIAFP_concrete_address (PC + offset) |];
-            ik = IK_branch();
-     },
-     RISCV_JALR(imm, rs, rd) => {
-            if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-            let offset : bits(64) = sign_extend(imm) in
-            Nias = [| NIAFP_indirect_address() |];
-            ik = IK_branch();
-     },
-     BTYPE(imm, rs2, rs1, op) => {
-            if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-            if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-            ik = IK_branch();
-            let offset : bits(64) = sign_extend(imm) in
-            Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |];
-      },
-      ITYPE(imm, rs, rd, op) => {
-            if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-      },
-      SHIFTIOP(imm, rs, rd, op) => {
-             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-      },
-      RTYPE(rs2, rs1, rd, op) => {
-             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-             if (rd == 0b00000) 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 not(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 == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-             if (rd == 0b00000) 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(__FILE__, __LINE__, "LOAD type not implemented in initial_analysis")
-               }
-      },
-      STORE(imm, rs2, rs1, width, aq, rl) => {
-             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-             if (rs1 == 0b00000) 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(__FILE__, __LINE__, "STORE type not implemented in initial_analysis")
-               }
-      },
-      ADDIW(imm, rs, rd) => {
-             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-      },
-      SHIFTIWOP(imm, rs, rd, op) => {
-             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-      },
-      RTYPEW(rs2, rs1, rd, op) => {
-             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-             if (rd == 0b00000) 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(__FILE__, __LINE__, "barrier type not implemented in initial_analysis")
-               };
-      },
-      FENCE_TSO(pred, succ) => {
-             ik =
-               match (pred, succ) {
-                 (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_tso),
-                 _ => internal_error(__FILE__, __LINE__, "barrier type not implemented in initial_analysis")
-               };
-      },
-     FENCEI() => {
-              ik = IK_simple (); // for RMEM, should morally be Barrier_RISCV_i
-     },
-     LOADRES(aq, rl, rs1, width, rd) => {
-            if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-            if (rd == 0b00000) 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(__FILE__, __LINE__, "LOADRES type not implemented in initial_analysis")
-            };
-     },
-     STORECON(aq, rl, rs2, rs1, width, rd) => {
-            if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-            if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-            if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR;
-            if (rd == 0b00000) 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(__FILE__, __LINE__, "STORECON type not implemented in initial_analysis")
-             };
-      },
-      AMO(op, aq, rl, rs2, rs1, width, rd) => {
-             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-             if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR;
-             if (rd == 0b00000) 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)
-}
-
-$else
-
-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 == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-     },
-     RISCV_JAL(imm, rd) => {
-	    if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-            let offset : bits(64) = sign_extend(imm) in
-            Nias = [| NIAFP_concrete_address (PC + offset) |];
-            ik = IK_branch();
-     },
-     RISCV_JALR(imm, rs, rd) => {
-            if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-            let offset : bits(64) = sign_extend(imm) in
-            Nias = [| NIAFP_indirect_address() |];
-            ik = IK_branch();
-     },
-     BTYPE(imm, rs2, rs1, op) => {
-            if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-            if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-            ik = IK_branch();
-            let offset : bits(64) = sign_extend(imm) in
-            Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |];
-      },
-      ITYPE(imm, rs, rd, op) => {
-            if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-            if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-      },
-      SHIFTIOP(imm, rs, rd, op) => {
-             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-      },
-      RTYPE(rs2, rs1, rd, op) => {
-             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-             if (rd == 0b00000) 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 not(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 == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-             if (rd == 0b00000) 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(__FILE__, __LINE__, "LOAD type not implemented in initial_analysis")
-               }
-      },
-      STORE(imm, rs2, rs1, width, aq, rl) => {
-             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-             if (rs1 == 0b00000) 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(__FILE__, __LINE__, "STORE type not implemented in initial_analysis")
-               }
-      },
-      ADDIW(imm, rs, rd) => {
-             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-      },
-      SHIFTIWOP(imm, rs, rd, op) => {
-             if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
-             if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
-      },
-      RTYPEW(rs2, rs1, rd, op) => {
-             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-             if (rd == 0b00000) 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(__FILE__, __LINE__, "barrier type not implemented in initial_analysis")
-               };
-      },
-      FENCE_TSO(pred, succ) => {
-             ik =
-               match (pred, succ) {
-		 (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => IK_barrier (Barrier_RISCV_tso ()),
-                 _ => internal_error(__FILE__, __LINE__, "barrier type not implemented in initial_analysis")
-               };
-      },
-     FENCEI() => {
-              ik = IK_simple (); // for RMEM, should morally be Barrier_RISCV_i
-     },
-     LOADRES(aq, rl, rs1, width, rd) => {
-            if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-            if (rd == 0b00000) 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(__FILE__, __LINE__, "LOADRES type not implemented in initial_analysis")
-            };
-     },
-     STORECON(aq, rl, rs2, rs1, width, rd) => {
-            if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-            if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-            if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR;
-            if (rd == 0b00000) 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(__FILE__, __LINE__, "STORECON type not implemented in initial_analysis")
-             };
-      },
-      AMO(op, aq, rl, rs2, rs1, width, rd) => {
-             if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR;
-             if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR;
-             if (rs1 == 0b00000) then () else aR = RFull(GPRstr(rs1)) :: aR;
-             if (rd == 0b00000) 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)
-}
-
-$endif