diff options
| author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-06-24 12:22:47 -0700 |
|---|---|---|
| committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-06-24 13:13:37 -0700 |
| commit | 0e589ae548b5326afd085bf176ef5914a326cd8b (patch) | |
| tree | e20ff0369c36632b838f680af6601d7ae69519d4 /model/riscv_duopod.sail | |
| parent | a2e5c0283e57e585f479d9713952b47eb21cd8fd (diff) | |
| download | sail-riscv-0e589ae548b5326afd085bf176ef5914a326cd8b.zip sail-riscv-0e589ae548b5326afd085bf176ef5914a326cd8b.tar.gz sail-riscv-0e589ae548b5326afd085bf176ef5914a326cd8b.tar.bz2 | |
Starting cleaning up physical memory bits for pmp integration.
. convert duopod to directly use Sail lib/regfp functions
. put lib/regfp wrappers in prelude, and avoid calling them directly in riscv_mem
. remove mmio assumption in page-table walks, making read/write calls symmetric
. prune obsolete functions from prelude_mem
Diffstat (limited to 'model/riscv_duopod.sail')
| -rw-r--r-- | model/riscv_duopod.sail | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/model/riscv_duopod.sail b/model/riscv_duopod.sail index 99dbbba..f611f52 100644 --- a/model/riscv_duopod.sail +++ b/model/riscv_duopod.sail @@ -32,13 +32,11 @@ function wX (r, v) = overload X = {rX, wX} /* Accessors for memory */ - -val MEMr : forall 'n, 'n >= 0. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem} -function MEMr (addr, width) = - match __RISCV_read(addr, width, false, false, false) { - Some(v) => v, - None() => zeros(8 * width) - } +val MEMr = { lem: "MEMr", coq: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0. + (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} +val read_mem : forall 'n, 'n >= 0. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem} +function read_mem(addr, width) = + MEMr(sizeof(xlen), width, EXTZ(0x0), addr) /* Instruction decode and execute */ enum iop = {RISCV_ADDI, RISCV_SLTI, RISCV_SLTIU, RISCV_XORI, RISCV_ORI, RISCV_ANDI} @@ -73,7 +71,7 @@ function clause decode imm : bits(12) @ rs1 : regbits @ 0b011 @ rd : regbits @ 0 function clause execute(LOAD(imm, rs1, rd)) = let addr : xlenbits = X(rs1) + EXTS(imm) in - let result : xlenbits = MEMr(addr, xlen_bytes) in + let result : xlenbits = read_mem(addr, sizeof(xlen_bytes)) in X(rd) = result /* ****************************************************************** */ |