diff options
| -rw-r--r-- | lib/regfp.sail | 96 | ||||
| -rw-r--r-- | riscv/riscv.sail | 29 | ||||
| -rw-r--r-- | riscv/riscv_sys.sail | 6 |
3 files changed, 119 insertions, 12 deletions
diff --git a/lib/regfp.sail b/lib/regfp.sail new file mode 100644 index 00000000..b8cffb98 --- /dev/null +++ b/lib/regfp.sail @@ -0,0 +1,96 @@ +/* iR : input registers, + * oR : output registers, + * aR : registers feeding into the memory address */ + +/* branch instructions currently are not writing to NIA */ + +union regfp = { + RFull : string, + RSlice : (string,nat,nat), + RSliceBit : (string,nat), + RField : (string,string) +} + +type regfps = list(regfp) + +union niafp = { + NIAFP_successor : unit, + NIAFP_concrete_address : bits(64), + NIAFP_indirect_address : unit +} + +type niafps = list(niafp) + +/* only for MIPS */ +union diafp = { + DIAFP_none : unit, + DIAFP_concrete : bits(64), + DIAFP_reg : regfp +} + +enum read_kind = { + Read_plain, + Read_reserve, + Read_acquire, + Read_exclusive, + Read_exclusive_acquire, + Read_stream, + Read_RISCV_acquire, + Read_RISCV_strong_acquire, + Read_RISCV_reserved, + Read_RISCV_reserved_acquire, + Read_RISCV_reserved_strong_acquire, + Read_X86_locked +} + +enum write_kind = { + Write_plain, + Write_conditional, + Write_release, + Write_exclusive, + Write_exclusive_release, + Write_RISCV_release, + Write_RISCV_strong_release, + Write_RISCV_conditional, + Write_RISCV_conditional_release, + Write_RISCV_conditional_strong_release, + Write_X86_locked +} + +enum barrier_kind = { + Barrier_Sync, + Barrier_LwSync, + Barrier_Eieio, + Barrier_Isync, + Barrier_DMB, + Barrier_DMB_ST, + Barrier_DMB_LD, + Barrier_DSB, + Barrier_DSB_ST, + Barrier_DSB_LD, + Barrier_ISB, + Barrier_MIPS_SYNC, + Barrier_RISCV_rw_rw, + Barrier_RISCV_r_rw, + Barrier_RISCV_r_r, + Barrier_RISCV_rw_w, + Barrier_RISCV_w_w, + Barrier_RISCV_i, + Barrier_x86_MFENCE +} + +enum trans_kind = { + Transaction_start, + Transaction_commit, + Transaction_abort +} + +union instruction_kind = { + IK_barrier : barrier_kind, + IK_mem_read : read_kind, + IK_mem_write : write_kind, + IK_mem_rmw : (read_kind, write_kind), + IK_branch : unit, + IK_trans : trans_kind, + IK_simple : unit +} diff --git a/riscv/riscv.sail b/riscv/riscv.sail index 9175401c..4fd32126 100644 --- a/riscv/riscv.sail +++ b/riscv/riscv.sail @@ -1096,6 +1096,9 @@ function readCSR csr : csreg -> xlenbits = 0x343 => mtval, 0x344 => mip.bits(), + 0x3A0 => pmpcfg0, + 0x3B0 => pmpaddr0, + /* supervisor mode */ 0x100 => mstatus.bits(), /* FIXME: legalize view*/ 0x102 => sedeleg.bits(), @@ -1138,6 +1141,9 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = 0x343 => { mtval = value; Some(mtval) }, 0x344 => { mip = legalize_mip(mip, value); Some(mip.bits()) }, + 0x3A0 => { pmpcfg0 = value; Some(pmpcfg0) }, /* FIXME: legalize */ + 0x3B0 => { pmpaddr0 = value; Some(pmpaddr0) }, /* FIXME: legalize */ + /* supervisor mode */ 0x100 => { mstatus = legalize_sstatus(mstatus, value); Some(mstatus.bits()) }, 0x102 => { sedeleg = legalize_sedeleg(sedeleg, value); Some(sedeleg.bits()) }, @@ -1777,7 +1783,6 @@ end execute end print_insn end assembly end encdec -end encdec_compressed function decode bv = Some(encdec(bv)) @@ -1892,20 +1897,20 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR; if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR; }, - FENCE(pred, succ) -> { + FENCE(pred, succ) => { ik = - switch(pred, succ) { + match (pred, succ) { (0b0011, 0b0011) => IK_barrier (Barrier_RISCV_rw_rw), (0b0010, 0b0011) => IK_barrier (Barrier_RISCV_r_rw), - (0b0001, 0b0011) => IK_barrier (Barrier_RISCV_w_rw), +// (0b0001, 0b0011) => IK_barrier (Barrier_RISCV_w_rw), - (0b0011, 0b0010) => IK_barrier (Barrier_RISCV_rw_r), - (0b0010, 0b0010) => IK_barrier (Barrier_RISCV_r_r), - (0b0001, 0b0010) => IK_barrier (Barrier_RISCV_w_r), + // (0b0011, 0b0010) => IK_barrier (Barrier_RISCV_rw_r), + // (0b0010, 0b0010) => IK_barrier (Barrier_RISCV_r_r), + // (0b0001, 0b0010) => IK_barrier (Barrier_RISCV_w_r), - (0b0011, 0b0001) => IK_barrier (Barrier_RISCV_rw_w), - (0b0010, 0b0001) => IK_barrier (Barrier_RISCV_r_w), - (0b0001, 0b0001) => IK_barrier (Barrier_RISCV_w_w), + // (0b0011, 0b0001) => IK_barrier (Barrier_RISCV_rw_w), + // (0b0010, 0b0001) => IK_barrier (Barrier_RISCV_r_w), + // (0b0001, 0b0001) => IK_barrier (Barrier_RISCV_w_w), _ => internal_error("barrier type not implemented in initial_analysis") // case (FM_NORMAL, _, _) -> exit "not implemented" @@ -1913,10 +1918,10 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst // case (FM_TSO, 0b0011, 0b0011) -> IK_barrier (Barrier_RISCV_tso) // case (FM_TSO, _, _) -> exit "not implemented" }; - } + }, FENCEI() => { ik = IK_barrier (Barrier_RISCV_i); - } + }, // case (LOADRES ( aq, rl, rs1, width, rd)) -> { // if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR; // if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail index ab1afe87..3779d136 100644 --- a/riscv/riscv_sys.sail +++ b/riscv/riscv_sys.sail @@ -506,6 +506,9 @@ function csr_name(csr) = { 0x342 => "mcause", 0x343 => "mtval", 0x344 => "mip", + + 0x3A0 => "pmpcfg0", + 0x3B0 => "pmpaddr0", /* TODO: machine protection and translation */ /* machine counters/timers */ 0xB00 => "mcycle", @@ -609,6 +612,9 @@ function is_CSR_defined (csr : bits(12), p : Privilege) -> bool = 0x343 => p == Machine, // mtval 0x344 => p == Machine, // mip + 0x3A0 => p == Machine, // pmpcfg0 + 0x3B0 => p == Machine, // pmpaddr0 + /* supervisor mode: trap setup */ 0x100 => p == Machine | p == Supervisor, // sstatus 0x102 => p == Machine | p == Supervisor, // sedeleg |