aboutsummaryrefslogtreecommitdiff
path: root/model
diff options
context:
space:
mode:
Diffstat (limited to 'model')
-rw-r--r--model/riscv_analysis.sail176
-rw-r--r--model/riscv_fetch_rvfi.sail2
-rw-r--r--model/riscv_insts_base.sail46
-rw-r--r--model/riscv_pc_access.sail10
-rw-r--r--model/riscv_platform.sail9
-rw-r--r--model/riscv_step_rvfi.sail2
6 files changed, 240 insertions, 5 deletions
diff --git a/model/riscv_analysis.sail b/model/riscv_analysis.sail
index 34572f8..ec8c96f 100644
--- a/model/riscv_analysis.sail
+++ b/model/riscv_analysis.sail
@@ -10,6 +10,8 @@ let GPRstr : vector(32, dec, string) = [ "x31", "x30", "x29", "x28", "x27", "x26
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;
@@ -180,3 +182,177 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
};
(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 == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+ },
+ RISCV_JAL(imm, rd) => {
+ if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+ let offset : bits(64) = EXTS(imm) in
+ Nias = [| NIAFP_concrete_address (PC + offset) |];
+ ik = IK_branch();
+ },
+ RISCV_JALR(imm, rs, rd) => {
+ if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
+ if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+ let offset : bits(64) = EXTS(imm) in
+ Nias = [| NIAFP_indirect_address() |];
+ ik = IK_branch();
+ },
+ BTYPE(imm, rs2, rs1, op) => {
+ if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
+ if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
+ ik = IK_branch();
+ let offset : bits(64) = EXTS(imm) in
+ Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |];
+ },
+ ITYPE(imm, rs, rd, op) => {
+ if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
+ if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+ },
+ SHIFTIOP(imm, rs, rd, op) => {
+ if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
+ if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+ },
+ RTYPE(rs2, rs1, rd, op) => {
+ if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
+ if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
+ if (rd == 0) 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 ~(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 == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
+ if (rd == 0) 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("LOAD type not implemented in initial_analysis")
+ }
+ },
+ STORE(imm, rs2, rs1, width, aq, rl) => {
+ if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
+ if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
+ if (rs1 == 0) 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("STORE type not implemented in initial_analysis")
+ }
+ },
+ ADDIW(imm, rs, rd) => {
+ if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
+ if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+ },
+ SHIFTW(imm, rs, rd, op) => {
+ if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
+ if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+ },
+ RTYPEW(rs2, rs1, rd, op) => {
+ if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
+ if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
+ if (rd == 0) 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("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("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 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
+ if (rd == 0) 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("LOADRES type not implemented in initial_analysis")
+ };
+ },
+ STORECON(aq, rl, rs2, rs1, width, rd) => {
+ if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
+ if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
+ if (rs1 == 0) then () else aR = RFull(GPRstr[rs1]) :: aR;
+ if (rd == 0) 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("STORECON type not implemented in initial_analysis")
+ };
+ },
+ AMO(op, aq, rl, rs2, rs1, width, rd) => {
+ if (rs2 == 0) then () else iR = RFull(GPRstr[rs2]) :: iR;
+ if (rs1 == 0) then () else iR = RFull(GPRstr[rs1]) :: iR;
+ if (rs1 == 0) then () else aR = RFull(GPRstr[rs1]) :: aR;
+ if (rd == 0) 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
diff --git a/model/riscv_fetch_rvfi.sail b/model/riscv_fetch_rvfi.sail
index 03b6010..c2a5e74 100644
--- a/model/riscv_fetch_rvfi.sail
+++ b/model/riscv_fetch_rvfi.sail
@@ -5,7 +5,7 @@ function fetch() -> FetchResult =
else {
let i = rvfi_instruction.rvfi_insn();
rvfi_exec->rvfi_order() = minstret;
- rvfi_exec->rvfi_pc_rdata() = EXTZ(PC);
+ rvfi_exec->rvfi_pc_rdata() = EXTZ(get_arch_pc());
rvfi_exec->rvfi_insn() = EXTZ(i);
/* TODO: should we write these even if they're not really registers? */
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index 0df5ce8..10f3117 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -17,7 +17,7 @@ function clause execute UTYPE(imm, rd, op) = {
let off : xlenbits = EXTS(imm @ 0x000);
let ret : xlenbits = match op {
RISCV_LUI => off,
- RISCV_AUIPC => PC + off
+ RISCV_AUIPC => get_arch_pc() + off
};
X(rd) = ret;
RETIRE_SUCCESS
@@ -564,6 +564,31 @@ union clause ast = FENCE : (bits(4), bits(4))
mapping clause encdec = FENCE(pred, succ)
<-> 0b0000 @ pred @ succ @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111
+/* For future versions of Sail where barriers can be parameterised */
+$ifdef FEATURE_UNION_BARRIER
+
+function clause execute (FENCE(pred, succ)) = {
+ match (pred, succ) {
+ (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_rw_rw()),
+ (_ : bits(2) @ 0b10, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_r_rw()),
+ (_ : bits(2) @ 0b10, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_r_r()),
+ (_ : bits(2) @ 0b11, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_rw_w()),
+ (_ : bits(2) @ 0b01, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_w_w()),
+ (_ : bits(2) @ 0b01, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_w_rw()),
+ (_ : bits(2) @ 0b11, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_rw_r()),
+ (_ : bits(2) @ 0b10, _ : bits(2) @ 0b01) => __barrier(Barrier_RISCV_r_w()),
+ (_ : bits(2) @ 0b01, _ : bits(2) @ 0b10) => __barrier(Barrier_RISCV_w_r()),
+
+ (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (),
+
+ _ => { print("FIXME: unsupported fence");
+ () }
+ };
+ RETIRE_SUCCESS
+}
+
+$else
+
function clause execute (FENCE(pred, succ)) = {
match (pred, succ) {
(_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_rw_rw),
@@ -584,6 +609,8 @@ function clause execute (FENCE(pred, succ)) = {
RETIRE_SUCCESS
}
+$endif
+
mapping bit_maybe_r : bits(1) <-> string = {
0b1 <-> "r",
0b0 <-> ""
@@ -617,6 +644,21 @@ union clause ast = FENCE_TSO : (bits(4), bits(4))
mapping clause encdec = FENCE_TSO(pred, succ)
<-> 0b1000 @ pred @ succ @ 0b00000 @ 0b000 @ 0b00000 @ 0b0001111
+$ifdef FEATURE_UNION_BARRIER
+
+function clause execute (FENCE_TSO(pred, succ)) = {
+ match (pred, succ) {
+ (_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_tso()),
+ (_ : bits(2) @ 0b00, _ : bits(2) @ 0b00) => (),
+
+ _ => { print("FIXME: unsupported fence");
+ () }
+ };
+ RETIRE_SUCCESS
+}
+
+$else
+
function clause execute (FENCE_TSO(pred, succ)) = {
match (pred, succ) {
(_ : bits(2) @ 0b11, _ : bits(2) @ 0b11) => __barrier(Barrier_RISCV_tso),
@@ -628,6 +670,8 @@ function clause execute (FENCE_TSO(pred, succ)) = {
RETIRE_SUCCESS
}
+$endif
+
mapping clause assembly = FENCE_TSO(pred, succ)
<-> "fence.tso" ^ spc() ^ fence_bits(pred) ^ sep() ^ fence_bits(succ)
diff --git a/model/riscv_pc_access.sail b/model/riscv_pc_access.sail
index a51e627..2de44ba 100644
--- a/model/riscv_pc_access.sail
+++ b/model/riscv_pc_access.sail
@@ -1,5 +1,13 @@
/* accessors for default architectural addresses, for use from within instructions */
-/* FIXME: see note in cheri_addr_checks.sail */
+
+/*!
+ Retrieves the architectural PC value. This is not necessarily the value
+ found in the PC register as extensions may choose to override this function.
+ The value in the PC register is the absolute virtual address of the instruction
+ to fetch.
+ */
+val get_arch_pc : unit -> xlenbits effect {rreg}
+function get_arch_pc() = PC
val get_next_pc : unit -> xlenbits effect {rreg}
function get_next_pc() = nextPC
diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail
index 9184f02..52511a9 100644
--- a/model/riscv_platform.sail
+++ b/model/riscv_platform.sail
@@ -337,12 +337,19 @@ function htif_tick() = {
}
/* Top-level MMIO dispatch */
-
+$ifndef RVFI_DII
function within_mmio_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool =
within_clint(addr, width) | (within_htif_readable(addr, width) & 1 <= 'n)
+$else
+function within_mmio_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = false
+$endif
+$ifndef RVFI_DII
function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool =
within_clint(addr, width) | (within_htif_writable(addr, width) & 'n <= 8)
+$else
+function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> bool = false
+$endif
function mmio_read forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : atom('n)) -> MemoryOpResult(bits(8 * 'n)) =
if within_clint(addr, width)
diff --git a/model/riscv_step_rvfi.sail b/model/riscv_step_rvfi.sail
index 0efcdce..0ab482a 100644
--- a/model/riscv_step_rvfi.sail
+++ b/model/riscv_step_rvfi.sail
@@ -6,7 +6,7 @@ function ext_pre_step_hook() -> unit = ()
function ext_post_step_hook() -> unit = {
/* record the next pc */
- rvfi_exec->rvfi_pc_wdata() = EXTZ(PC)
+ rvfi_exec->rvfi_pc_wdata() = EXTZ(get_arch_pc())
}
val ext_init : unit -> unit effect {wreg}
generated by cgit v1.1 at 2024-11-06 00:51:16 +0000