aboutsummaryrefslogtreecommitdiff
path: root/model/riscv_analysis.sail
diff options
context:
space:
mode:
Diffstat (limited to 'model/riscv_analysis.sail')
-rw-r--r--model/riscv_analysis.sail367
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
generated by cgit v1.1 at 2024-07-24 03:12:14 +0000