aboutsummaryrefslogtreecommitdiff
path: root/model
diff options
context:
space:
mode:
Diffstat (limited to 'model')
-rw-r--r--model/prelude.sail19
-rw-r--r--model/riscv_analysis.sail151
-rw-r--r--model/riscv_duopod.sail24
-rw-r--r--model/riscv_fetch.sail2
-rw-r--r--model/riscv_insts_aext.sail4
-rw-r--r--model/riscv_insts_base.sail36
-rw-r--r--model/riscv_insts_cext.sail4
-rw-r--r--model/riscv_jalr_seq.sail5
-rw-r--r--model/riscv_next_regs.sail8
-rw-r--r--model/riscv_platform.sail8
-rw-r--r--model/riscv_pmp_control.sail10
-rw-r--r--model/riscv_pmp_regs.sail10
-rw-r--r--model/riscv_regs.sail8
-rw-r--r--model/riscv_step.sail2
-rw-r--r--model/riscv_sys_control.sail90
-rw-r--r--model/riscv_sys_regs.sail70
-rw-r--r--model/riscv_types.sail16
-rw-r--r--model/riscv_vmem_common.sail28
-rw-r--r--model/riscv_vmem_rv32.sail6
-rw-r--r--model/riscv_vmem_rv64.sail6
-rw-r--r--model/riscv_vmem_sv32.sail2
-rw-r--r--model/riscv_vmem_sv39.sail2
-rw-r--r--model/riscv_vmem_sv48.sail2
23 files changed, 260 insertions, 253 deletions
diff --git a/model/prelude.sail b/model/prelude.sail
index c67ec3c..a8faf3d 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -50,16 +50,17 @@ overload operator & = {and_vec}
overload operator | = {or_vec}
-val cast cast_unit_vec : bit -> bits(1)
+val string_of_int = {c: "string_of_int", ocaml: "string_of_int", interpreter: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string
-function cast_unit_vec b = match b {
- bitzero => 0b0,
- bitone => 0b1
-}
+val "string_of_bits" : forall 'n. bits('n) -> string
-val string_of_int = {c: "string_of_int", ocaml: "string_of_int", interpreter: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string
+function string_of_bit(b: bit) -> string =
+ match b {
+ bitzero => "0b0",
+ bitone => "0b1"
+ }
-val BitStr = "string_of_bits" : forall 'n. bits('n) -> string
+overload BitStr = {string_of_bits, string_of_bit}
val xor_vec = {c: "xor_bits", _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
@@ -125,10 +126,10 @@ overload zeros = {zeros_implicit}
val ones : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
function ones (n) = sail_ones (n)
-val cast bool_to_bits : bool -> bits(1)
+val bool_to_bits : bool -> bits(1)
function bool_to_bits x = if x then 0b1 else 0b0
-val cast bit_to_bool : bit -> bool
+val bit_to_bool : bit -> bool
function bit_to_bool b = match b {
bitone => true,
bitzero => false
diff --git a/model/riscv_analysis.sail b/model/riscv_analysis.sail
index ec8c96f..5b55e6e 100644
--- a/model/riscv_analysis.sail
+++ b/model/riscv_analysis.sail
@@ -1,11 +1,12 @@
$include <regfp.sail>
/* in reverse order because inc vectors don't seem to work (bug) */
-let GPRstr : vector(32, dec, string) = [ "x31", "x30", "x29", "x28", "x27", "x26", "x25", "x24", "x23", "x22", "x21",
+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")
@@ -23,40 +24,40 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
match instr {
EBREAK() => (),
UTYPE(imm, rd, op) => {
- if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+ if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
},
RISCV_JAL(imm, rd) => {
- if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+ if (rd == 0b00000) 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;
+ if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
+ if (rd == 0b00000) 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;
+ 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) = 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;
+ 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 == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
- if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+ 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 == 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;
+ 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 {
@@ -65,16 +66,16 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
};
iR = RFull(csr_name(csr)) :: iR;
if ~(is_imm) then {
- iR = RFull(GPRstr[rs1]) :: iR;
+ iR = RFull(GPRstr(rs1)) :: iR;
};
if isWrite then {
oR = RFull(csr_name(csr)) :: oR;
};
- oR = RFull(GPRstr[rd]) :: 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;
+ 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) {
@@ -86,9 +87,9 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
}
},
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;
+ 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),
@@ -99,17 +100,17 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
}
},
ADDIW(imm, rs, rd) => {
- if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
- if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+ if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
+ if (rd == 0b00000) 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;
+ 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 == 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;
+ 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 =
@@ -141,8 +142,8 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
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;
+ 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),
@@ -152,10 +153,10 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
};
},
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;
+ 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),
@@ -165,10 +166,10 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
};
},
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;
+ 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),
@@ -196,40 +197,40 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
match instr {
EBREAK() => (),
UTYPE(imm, rd, op) => {
- if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+ if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
},
RISCV_JAL(imm, rd) => {
- if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+ if (rd == 0b00000) 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;
+ if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
+ if (rd == 0b00000) 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;
+ 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) = 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;
+ 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 == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
- if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+ 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 == 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;
+ 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 {
@@ -238,16 +239,16 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
};
iR = RFull(csr_name(csr)) :: iR;
if ~(is_imm) then {
- iR = RFull(GPRstr[rs1]) :: iR;
+ iR = RFull(GPRstr(rs1)) :: iR;
};
if isWrite then {
oR = RFull(csr_name(csr)) :: oR;
};
- oR = RFull(GPRstr[rd]) :: 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;
+ 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) {
@@ -259,9 +260,9 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
}
},
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;
+ 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),
@@ -272,17 +273,17 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
}
},
ADDIW(imm, rs, rd) => {
- if (rs == 0) then () else iR = RFull(GPRstr[rs]) :: iR;
- if (rd == 0) then () else oR = RFull(GPRstr[rd]) :: oR;
+ if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR;
+ if (rd == 0b00000) 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;
+ 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 == 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;
+ 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 =
@@ -313,8 +314,8 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
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;
+ 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),
@@ -324,10 +325,10 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
};
},
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;
+ 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),
@@ -337,10 +338,10 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
};
},
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;
+ 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),
diff --git a/model/riscv_duopod.sail b/model/riscv_duopod.sail
index f611f52..395a332 100644
--- a/model/riscv_duopod.sail
+++ b/model/riscv_duopod.sail
@@ -1,14 +1,10 @@
// This file depends on the xlen definitions in riscv_xlen.sail.
-type regno ('n : Int), 0 <= 'n < 32 = atom('n)
type regbits = bits(5)
val zeros : forall 'n, 'n >= 0. atom('n) -> bits('n)
function zeros n = replicate_bits(0b0, n)
-val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
-function regbits_to_regno b = let r as atom(_) = unsigned(b) in r
-
/* Architectural state */
register PC : xlenbits
@@ -17,24 +13,28 @@ register nextPC : xlenbits
register Xs : vector(32, dec, xlenbits)
/* Getters and setters for X registers (special case for zeros register, x0) */
-val rX : forall 'n, 0 <= 'n < 32. regno('n) -> xlenbits effect {rreg}
+val rX : regbits -> xlenbits effect {rreg}
-function rX 0 = EXTZ(0x0)
-and rX (r if r > 0) = Xs[r]
+function rX(r) =
+ match r {
+ 0b00000 => EXTZ(0x0),
+ _ => Xs[unsigned(r)]
+ }
-val wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg}
+val wX : (regbits, xlenbits) -> unit effect {wreg}
function wX (r, v) =
- if r != 0 then {
- Xs[r] = v;
+ if r != 0b00000 then {
+ Xs[unsigned(r)] = v;
}
overload X = {rX, wX}
/* Accessors for memory */
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}
+ (atom('m), int('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
+
+val read_mem : forall 'n, 'n >= 0. (xlenbits, int('n)) -> bits(8 * 'n) effect {rmem}
function read_mem(addr, width) =
MEMr(sizeof(xlen), width, EXTZ(0x0), addr)
diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail
index ae8748c..c52a70d 100644
--- a/model/riscv_fetch.sail
+++ b/model/riscv_fetch.sail
@@ -12,7 +12,7 @@ function fetch() -> FetchResult =
match ext_fetch_check_pc(PC, PC) {
Ext_FetchAddr_Error(e) => F_Ext_Error(e),
Ext_FetchAddr_OK(use_pc) => {
- if (use_pc[0] != 0b0 | (use_pc[1] != 0b0 & (~ (haveRVC()))))
+ if (use_pc[0] != bitzero | (use_pc[1] != bitzero & (~ (haveRVC()))))
then F_Error(E_Fetch_Addr_Align, PC)
else match translateAddr(use_pc, Execute) {
TR_Failure(e) => F_Error(e, PC),
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
index cd2f069..d2cbd38 100644
--- a/model/riscv_insts_aext.sail
+++ b/model/riscv_insts_aext.sail
@@ -53,7 +53,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
*/
match width {
BYTE => true,
- HALF => vaddr[0] == 0b0,
+ HALF => vaddr[0..0] == 0b0,
WORD => vaddr[1..0] == 0b00,
DOUBLE => vaddr[2..0] == 0b000
};
@@ -112,7 +112,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
*/
match width {
BYTE => true,
- HALF => vaddr[0] == 0b0,
+ HALF => vaddr[0..0] == 0b0,
WORD => vaddr[1..0] == 0b00,
DOUBLE => vaddr[2..0] == 0b000
};
diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
index a435786..a0858bf 100644
--- a/model/riscv_insts_base.sail
+++ b/model/riscv_insts_base.sail
@@ -59,7 +59,7 @@ function clause execute (RISCV_JAL(imm, rd)) = {
},
Ext_ControlAddr_OK(target) => {
/* Perform standard alignment check */
- if target[1] & (~ (haveRVC()))
+ if bit_to_bool(target[1]) & (~ (haveRVC()))
then {
handle_mem_exception(target, E_Fetch_Addr_Align);
RETIRE_FAIL
@@ -123,7 +123,7 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = {
RETIRE_FAIL
},
Ext_ControlAddr_OK(target) => {
- if target[1] & (~ (haveRVC())) then {
+ if bit_to_bool(target[1]) & (~ (haveRVC())) then {
handle_mem_exception(target, E_Fetch_Addr_Align);
RETIRE_FAIL;
} else {
@@ -167,8 +167,8 @@ function clause execute (ITYPE (imm, rs1, rd, op)) = {
let immext : xlenbits = EXTS(imm);
let result : xlenbits = match op {
RISCV_ADDI => rs1_val + immext,
- RISCV_SLTI => EXTZ(rs1_val <_s immext),
- RISCV_SLTIU => EXTZ(rs1_val <_u immext),
+ RISCV_SLTI => EXTZ(bool_to_bits(rs1_val <_s immext)),
+ RISCV_SLTIU => EXTZ(bool_to_bits(rs1_val <_u immext)),
RISCV_ANDI => rs1_val & immext,
RISCV_ORI => rs1_val | immext,
RISCV_XORI => rs1_val ^ immext
@@ -198,9 +198,9 @@ mapping encdec_sop : sop <-> bits(3) = {
RISCV_SRAI <-> 0b101
}
-mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SLLI) <-> 0b000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == false
-mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRLI) <-> 0b000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == false
-mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRAI) <-> 0b010000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == false
+mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SLLI) <-> 0b000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == bitzero
+mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRLI) <-> 0b000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == bitzero
+mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRAI) <-> 0b010000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == bitzero
function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = {
let rs1_val = X(rs1);
@@ -248,8 +248,8 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) = {
let rs2_val = X(rs2);
let result : xlenbits = match op {
RISCV_ADD => rs1_val + rs2_val,
- RISCV_SLT => EXTZ(rs1_val <_s rs2_val),
- RISCV_SLTU => EXTZ(rs1_val <_u rs2_val),
+ RISCV_SLT => EXTZ(bool_to_bits(rs1_val <_s rs2_val)),
+ RISCV_SLTU => EXTZ(bool_to_bits(rs1_val <_u rs2_val)),
RISCV_AND => rs1_val & rs2_val,
RISCV_OR => rs1_val | rs2_val,
RISCV_XOR => rs1_val ^ rs2_val,
@@ -309,9 +309,9 @@ function check_misaligned(vaddr : xlenbits, width : word_width) -> bool =
if plat_enable_misaligned_access() then false
else match width {
BYTE => false,
- HALF => vaddr[0] == true,
- WORD => vaddr[0] == true | vaddr[1] == true,
- DOUBLE => vaddr[0] == true | vaddr[1] == true | vaddr[2] == true
+ HALF => vaddr[0] == bitone,
+ WORD => vaddr[0] == bitone | vaddr[1] == bitone,
+ DOUBLE => vaddr[0] == bitone | vaddr[1] == bitone | vaddr[2] == bitone
}
function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
@@ -731,7 +731,7 @@ mapping clause encdec = SRET()
function clause execute SRET() = {
match cur_privilege {
User => handle_illegal(),
- Supervisor => if (~ (haveSupMode ())) | mstatus.TSR() == true
+ Supervisor => if (~ (haveSupMode ())) | mstatus.TSR() == 0b1
then handle_illegal()
else set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC)),
Machine => if (~ (haveSupMode ()))
@@ -765,7 +765,7 @@ mapping clause encdec = WFI()
function clause execute WFI() =
match cur_privilege {
Machine => { platform_wfi(); RETIRE_SUCCESS },
- Supervisor => if mstatus.TW() == true
+ Supervisor => if mstatus.TW() == 0b1
then { handle_illegal(); RETIRE_FAIL }
else { platform_wfi(); RETIRE_SUCCESS },
User => { handle_illegal(); RETIRE_FAIL }
@@ -780,13 +780,13 @@ mapping clause encdec = SFENCE_VMA(rs1, rs2)
<-> 0b0001001 @ rs2 @ rs1 @ 0b000 @ 0b00000 @ 0b1110011
function clause execute SFENCE_VMA(rs1, rs2) = {
- let addr : option(xlenbits) = if rs1 == 0 then None() else Some(X(rs1));
- let asid : option(xlenbits) = if rs2 == 0 then None() else Some(X(rs2));
+ let addr : option(xlenbits) = if rs1 == 0b00000 then None() else Some(X(rs1));
+ let asid : option(xlenbits) = if rs2 == 0b00000 then None() else Some(X(rs2));
match cur_privilege {
User => { handle_illegal(); RETIRE_FAIL },
Supervisor => match (architecture(get_mstatus_SXL(mstatus)), mstatus.TVM()) {
- (Some(_), true) => { handle_illegal(); RETIRE_FAIL },
- (Some(_), false) => { flush_TLB(asid, addr); RETIRE_SUCCESS },
+ (Some(_), 0b1) => { handle_illegal(); RETIRE_FAIL },
+ (Some(_), 0b0) => { flush_TLB(asid, addr); RETIRE_SUCCESS },
(_, _) => internal_error("unimplemented sfence architecture")
},
Machine => { flush_TLB(asid, addr); RETIRE_SUCCESS }
diff --git a/model/riscv_insts_cext.sail b/model/riscv_insts_cext.sail
index c58c636..4f3d0c6 100644
--- a/model/riscv_insts_cext.sail
+++ b/model/riscv_insts_cext.sail
@@ -400,9 +400,9 @@ mapping clause assembly = C_BNEZ(imm, rs)
union clause ast = C_SLLI : (bits(6), regidx)
mapping clause encdec_compressed = C_SLLI(nzui5 @ nzui40, rsd)
- if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == false)
+ if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == 0b0)
<-> 0b000 @ nzui5 : bits(1) @ rsd : regidx @ nzui40 : bits(5) @ 0b10
- if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == false)
+ if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == 0b0)
function clause execute (C_SLLI(shamt, rsd)) =
execute(SHIFTIOP(shamt, rsd, rsd, RISCV_SLLI))
diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail
index 5b37c78..884820f 100644
--- a/model/riscv_jalr_seq.sail
+++ b/model/riscv_jalr_seq.sail
@@ -15,9 +15,8 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = {
RETIRE_FAIL
},
Ext_ControlAddr_OK(addr) => {
- let target = [addr with 0 = bitzero]; /* clear addr[0] */
- if target[1] & (~ (haveRVC()))
- then {
+ let target = [addr with 0 = bitzero]; /* clear addr[0] */
+ if bit_to_bool(target[1]) & ~(haveRVC()) then {
handle_mem_exception(target, E_Fetch_Addr_Align);
RETIRE_FAIL
} else {
diff --git a/model/riscv_next_regs.sail b/model/riscv_next_regs.sail
index 5a3fb58..b9c9c59 100644
--- a/model/riscv_next_regs.sail
+++ b/model/riscv_next_regs.sail
@@ -55,7 +55,7 @@ function lower_sie(s : Sinterrupts, d : Sinterrupts) -> Uinterrupts = {
/* Returns the new value of sip from the previous sip (o) and the written uip (u) as delegated by sideleg (d). */
function lift_uip(o : Sinterrupts, d : Sinterrupts, u : Uinterrupts) -> Sinterrupts = {
let s : Sinterrupts = o;
- let s = if d.USI() == true then update_USI(s, u.USI()) else s;
+ let s = if d.USI() == 0b1 then update_USI(s, u.USI()) else s;
s
}
@@ -66,9 +66,9 @@ function legalize_uip(s : Sinterrupts, d : Sinterrupts, v : xlenbits) -> Sinterr
/* Returns the new value of sie from the previous sie (o) and the written uie (u) as delegated by sideleg (d). */
function lift_uie(o : Sinterrupts, d : Sinterrupts, u : Uinterrupts) -> Sinterrupts = {
let s : Sinterrupts = o;
- let s = if d.UEI() == true then update_UEI(s, u.UEI()) else s;
- let s = if d.UTI() == true then update_UTI(s, u.UTI()) else s;
- let s = if d.USI() == true then update_USI(s, u.USI()) else s;
+ let s = if d.UEI() == 0b1 then update_UEI(s, u.UEI()) else s;
+ let s = if d.UTI() == 0b1 then update_UTI(s, u.UTI()) else s;
+ let s = if d.USI() == 0b1 then update_USI(s, u.USI()) else s;
s
}
diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail
index 52511a9..9639592 100644
--- a/model/riscv_platform.sail
+++ b/model/riscv_platform.sail
@@ -201,11 +201,11 @@ function clint_load(addr, width) = {
function clint_dispatch() -> unit = {
if get_config_print_platform()
then print_platform("clint::tick mtime <- " ^ BitStr(mtime));
- mip->MTI() = false;
+ mip->MTI() = 0b0;
if mtimecmp <=_u mtime then {
if get_config_print_platform()
then print_platform(" clint timer pending at mtime " ^ BitStr(mtime));
- mip->MTI() = true
+ mip->MTI() = 0b1
}
}
@@ -216,7 +216,7 @@ function clint_store(addr, width, data) = {
if addr == MSIP_BASE & ('n == 8 | 'n == 4) then {
if get_config_print_platform()
then print_platform("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mip.MSI <- " ^ BitStr(data[0]) ^ ")");
- mip->MSI() = data[0] == 0b1;
+ mip->MSI() = [data[0]];
clint_dispatch();
MemValue(true)
} else if addr == MTIMECMP_BASE & 'n == 8 then {
@@ -308,7 +308,7 @@ function htif_store(addr, width, data) = {
0x00 => { /* syscall-proxy */
if get_config_print_platform()
then print_platform("htif-syscall-proxy cmd: " ^ BitStr(cmd.payload()));
- if cmd.payload()[0] == 0b1
+ if cmd.payload()[0] == bitone
then {
htif_done = true;
htif_exit_code = (sail_zero_extend(cmd.payload(), 64) >> 1)
diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail
index 4c65f7d..233602f 100644
--- a/model/riscv_pmp_control.sail
+++ b/model/riscv_pmp_control.sail
@@ -29,10 +29,10 @@ function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits
val pmpCheckRWX: (Pmpcfg_ent, AccessType) -> bool
function pmpCheckRWX(ent, acc) = {
match acc {
- Read => ent.R() == true,
- Write => ent.W() == true,
- ReadWrite => ent.R() == true & ent.W() == true,
- Execute => ent.X() == true
+ Read => ent.R() == 0b1,
+ Write => ent.W() == 0b1,
+ ReadWrite => ent.R() == 0b1 & ent.W() == 0b1,
+ Execute => ent.X() == 0b1
}
}
@@ -40,7 +40,7 @@ function pmpCheckRWX(ent, acc) = {
val pmpCheckPerms: (Pmpcfg_ent, AccessType, Privilege) -> bool
function pmpCheckPerms(ent, acc, priv) = {
match priv {
- Machine => if ent.L() == true
+ Machine => if ent.L() == 0b1
then pmpCheckRWX(ent, acc)
else true,
_ => pmpCheckRWX(ent, acc)
diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail
index fcc6901..978ef18 100644
--- a/model/riscv_pmp_regs.sail
+++ b/model/riscv_pmp_regs.sail
@@ -2,7 +2,7 @@
enum PmpAddrMatchType = {OFF, TOR, NA4, NAPOT}
-val cast pmpAddrMatchType_of_bits : bits(2) -> PmpAddrMatchType
+val pmpAddrMatchType_of_bits : bits(2) -> PmpAddrMatchType
function pmpAddrMatchType_of_bits(bs) = {
match bs {
0b00 => OFF,
@@ -12,7 +12,7 @@ function pmpAddrMatchType_of_bits(bs) = {
}
}
-val cast pmpAddrMatchType_to_bits : PmpAddrMatchType -> bits(2)
+val pmpAddrMatchType_to_bits : PmpAddrMatchType -> bits(2)
function pmpAddrMatchType_to_bits(bs) = {
match bs {
OFF => 0b00,
@@ -87,7 +87,7 @@ function pmpReadCfgReg(n) = {
/* Helper to handle locked entries */
function pmpWriteCfg(cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent =
- if cfg.L() == true then cfg else Mk_Pmpcfg_ent(v)
+ if cfg.L() == 0b1 then cfg else Mk_Pmpcfg_ent(v)
val pmpWriteCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n), xlenbits) -> unit effect {rreg, wreg}
function pmpWriteCfgReg(n, v) = {
@@ -139,5 +139,5 @@ function pmpWriteCfgReg(n, v) = {
function pmpWriteAddr(cfg: Pmpcfg_ent, reg: xlenbits, v: xlenbits) -> xlenbits =
if sizeof(xlen) == 32
- then { if cfg.L() == true then reg else v }
- else { if cfg.L() == true then reg else EXTZ(v[53..0]) }
+ then { if cfg.L() == 0b1 then reg else v }
+ else { if cfg.L() == 0b1 then reg else EXTZ(v[53..0]) }
diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail
index c852677..4b4a1ea 100644
--- a/model/riscv_regs.sail
+++ b/model/riscv_regs.sail
@@ -139,7 +139,13 @@ function wX (r, in_v) = {
}
}
-overload X = {rX, wX}
+function rX_bits(i: bits(5)) -> xlenbits = rX(unsigned(i))
+
+function wX_bits(i: bits(5), data: xlenbits) -> unit = {
+ wX(unsigned(i)) = data
+}
+
+overload X = {rX_bits, wX_bits, rX, wX}
/* register names */
diff --git a/model/riscv_step.sail b/model/riscv_step.sail
index 4e81fe9..ed27c84 100644
--- a/model/riscv_step.sail
+++ b/model/riscv_step.sail
@@ -10,7 +10,7 @@ function step(step_no : int) -> bool = {
match dispatchInterrupt(cur_privilege) {
Some(intr, priv) => {
if get_config_print_instr()
- then print_bits("Handling interrupt: ", intr);
+ then print_bits("Handling interrupt: ", interruptType_to_bits(intr));
handle_interrupt(intr, priv);
(RETIRE_FAIL, false)
},
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index a8029a4..14e5d99 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -97,17 +97,17 @@ function check_CSR_access(csrrw, csrpr, p, isWrite) =
& (privLevel_to_bits(p) >=_u csrpr) /* privilege */
function check_TVM_SATP(csr : csreg, p : Privilege) -> bool =
- ~ (csr == 0x180 & p == Supervisor & mstatus.TVM() == true)
+ ~ (csr == 0x180 & p == Supervisor & mstatus.TVM() == 0b1)
function check_Counteren(csr : csreg, p : Privilege) -> bool =
match(csr, p) {
- (0xC00, Supervisor) => mcounteren.CY() == true,
- (0xC01, Supervisor) => mcounteren.TM() == true,
- (0xC02, Supervisor) => mcounteren.IR() == true,
+ (0xC00, Supervisor) => mcounteren.CY() == 0b1,
+ (0xC01, Supervisor) => mcounteren.TM() == 0b1,
+ (0xC02, Supervisor) => mcounteren.IR() == 0b1,
- (0xC00, User) => mcounteren.CY() == true & ((~ (haveSupMode())) | scounteren.CY() == true),
- (0xC01, User) => mcounteren.TM() == true & ((~ (haveSupMode())) | scounteren.TM() == true),
- (0xC02, User) => mcounteren.IR() == true & ((~ (haveSupMode())) | scounteren.IR() == true),
+ (0xC00, User) => mcounteren.CY() == 0b1 & ((~ (haveSupMode())) | scounteren.CY() == 0b1),
+ (0xC01, User) => mcounteren.TM() == 0b1 & ((~ (haveSupMode())) | scounteren.TM() == 0b1),
+ (0xC02, User) => mcounteren.IR() == 0b1 & ((~ (haveSupMode())) | scounteren.IR() == 0b1),
(_, _) => /* no HPM counters for now */
if 0xC03 <=_u csr & csr <=_u 0xC1F
@@ -144,10 +144,10 @@ val cancel_reservation = {ocaml: "Platform.cancel_reservation", interpreter: "Pl
*/
function exception_delegatee(e : ExceptionType, p : Privilege) -> Privilege = {
let idx = num_of_ExceptionType(e);
- let super = medeleg.bits()[idx];
+ let super = bit_to_bool(medeleg.bits()[idx]);
/* if S-mode is absent, medeleg delegates to U-mode if 'N' is supported. */
let user = if haveSupMode()
- then super & haveNExt() & sedeleg.bits()[idx]
+ then super & haveNExt() & bit_to_bool(sedeleg.bits()[idx])
else super & haveNExt();
let deleg = if haveUsrMode() & user then User
else if haveSupMode() & super then Supervisor
@@ -162,16 +162,16 @@ function exception_delegatee(e : ExceptionType, p : Privilege) -> Privilege = {
*/
function findPendingInterrupt(ip : xlenbits) -> option(InterruptType) = {
let ip = Mk_Minterrupts(ip);
- if ip.MEI() == true then Some(I_M_External)
- else if ip.MSI() == true then Some(I_M_Software)
- else if ip.MTI() == true then Some(I_M_Timer)
- else if ip.SEI() == true then Some(I_S_External)
- else if ip.SSI() == true then Some(I_S_Software)
- else if ip.STI() == true then Some(I_S_Timer)
- else if ip.UEI() == true then Some(I_U_External)
- else if ip.USI() == true then Some(I_U_Software)
- else if ip.UTI() == true then Some(I_U_Timer)
- else None()
+ if ip.MEI() == 0b1 then Some(I_M_External)
+ else if ip.MSI() == 0b1 then Some(I_M_Software)
+ else if ip.MTI() == 0b1 then Some(I_M_Timer)
+ else if ip.SEI() == 0b1 then Some(I_S_External)
+ else if ip.SSI() == 0b1 then Some(I_S_Software)
+ else if ip.STI() == 0b1 then Some(I_S_Timer)
+ else if ip.UEI() == 0b1 then Some(I_U_External)
+ else if ip.USI() == 0b1 then Some(I_U_Software)
+ else if ip.UTI() == 0b1 then Some(I_U_Timer)
+ else None()
}
/* Process the pending interrupts xip at a privilege according to
@@ -214,9 +214,9 @@ function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = {
* while lower privileges are blocked. An unsupported privilege is
* considered blocked.
*/
- let mIE = priv != Machine | (priv == Machine & mstatus.MIE() == true);
- let sIE = haveSupMode() & (priv == User | (priv == Supervisor & mstatus.SIE() == true));
- let uIE = haveNExt() & (priv == User & mstatus.UIE() == true);
+ let mIE = priv != Machine | (priv == Machine & mstatus.MIE() == 0b1);
+ let sIE = haveSupMode() & (priv == User | (priv == Supervisor & mstatus.SIE() == 0b1));
+ let uIE = haveNExt() & (priv == User & mstatus.UIE() == 0b1);
match processPending(mip, mie, mideleg.bits(), mIE) {
Ints_Empty() => None(),
Ints_Pending(p) => let r = (p, Machine) in Some(r),
@@ -304,11 +304,11 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
match (del_priv) {
Machine => {
- mcause->IsInterrupt() = intr;
+ mcause->IsInterrupt() = bool_to_bits(intr);
mcause->Cause() = EXTZ(c);
mstatus->MPIE() = mstatus.MIE();
- mstatus->MIE() = false;
+ mstatus->MIE() = 0b0;
mstatus->MPP() = privLevel_to_bits(cur_privilege);
mtval = tval(info);
mepc = pc;
@@ -325,14 +325,14 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
Supervisor => {
assert (haveSupMode(), "no supervisor mode present for delegation");
- scause->IsInterrupt() = intr;
+ scause->IsInterrupt() = bool_to_bits(intr);
scause->Cause() = EXTZ(c);
mstatus->SPIE() = mstatus.SIE();
- mstatus->SIE() = false;
- mstatus->SPP() = match (cur_privilege) {
- User => false,
- Supervisor => true,
+ mstatus->SIE() = 0b0;
+ mstatus->SPP() = match cur_privilege {
+ User => 0b0,
+ Supervisor => 0b1,
Machine => internal_error("invalid privilege for s-mode trap")
};
stval = tval(info);
@@ -350,11 +350,11 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
User => {
assert(haveUsrMode(), "no user mode present for delegation");
- ucause->IsInterrupt() = intr;
+ ucause->IsInterrupt() = bool_to_bits(intr);
ucause->Cause() = EXTZ(c);
mstatus->UPIE() = mstatus.UIE();
- mstatus->UIE() = false;
+ mstatus->UIE() = 0b0;
utval = tval(info);
uepc = pc;
@@ -378,12 +378,12 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
if get_config_print_platform()
then print_platform("trapping from " ^ to_str(cur_priv) ^ " to " ^ to_str(del_priv)
^ " to handle " ^ to_str(e.trap));
- trap_handler(del_priv, false, e.trap, pc, e.excinfo, e.ext)
+ trap_handler(del_priv, false, exceptionType_to_bits(e.trap), pc, e.excinfo, e.ext)
},
(_, CTL_MRET()) => {
let prev_priv = cur_privilege;
mstatus->MIE() = mstatus.MPIE();
- mstatus->MPIE() = true;
+ mstatus->MPIE() = 0b1;
cur_privilege = privLevel_of_bits(mstatus.MPP());
mstatus->MPP() = privLevel_to_bits(if haveUsrMode() then User else Machine);
@@ -398,10 +398,10 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
(_, CTL_SRET()) => {
let prev_priv = cur_privilege;
mstatus->SIE() = mstatus.SPIE();
- mstatus->SPIE() = true;
- cur_privilege = if mstatus.SPP() == true then Supervisor else User;
+ mstatus->SPIE() = 0b1;
+ cur_privilege = if mstatus.SPP() == 0b1 then Supervisor else User;
/* S-mode implies that U-mode is supported (issue 331 on riscv-isa-manual). */
- mstatus->SPP() = false;
+ mstatus->SPP() = 0b0;
if get_config_print_reg()
then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
@@ -415,7 +415,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
(_, CTL_URET()) => {
let prev_priv = cur_privilege;
mstatus->UIE() = mstatus.UPIE();
- mstatus->UPIE() = true;
+ mstatus->UPIE() = 0b1;
cur_privilege = User;
if get_config_print_reg()
@@ -437,7 +437,7 @@ function handle_mem_exception(addr : xlenbits, e : ExceptionType) -> unit = {
}
function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit =
- set_next_pc(trap_handler(del_priv, true, i, PC, None(), None()))
+ set_next_pc(trap_handler(del_priv, true, interruptType_to_bits(i), PC, None(), None()))
/* state state initialization */
@@ -447,16 +447,16 @@ function init_sys() -> unit = {
mhartid = EXTZ(0b0);
misa->MXL() = arch_to_bits(if sizeof(xlen) == 32 then RV32 else RV64);
- misa->A() = true; /* atomics */
- misa->C() = sys_enable_rvc (); /* RVC */
- misa->I() = true; /* base integer ISA */
- misa->M() = true; /* integer multiply/divide */
- misa->U() = true; /* user-mode */
- misa->S() = true; /* supervisor-mode */
+ misa->A() = 0b1; /* atomics */
+ misa->C() = bool_to_bits(sys_enable_rvc()); /* RVC */
+ misa->I() = 0b1; /* base integer ISA */
+ misa->M() = 0b1; /* integer multiply/divide */
+ misa->U() = 0b1; /* user-mode */
+ misa->S() = 0b1; /* supervisor-mode */
mstatus = set_mstatus_SXL(mstatus, misa.MXL());
mstatus = set_mstatus_UXL(mstatus, misa.MXL());
- mstatus->SD() = false;
+ mstatus->SD() = 0b0;
mip->bits() = EXTZ(0b0);
mie->bits() = EXTZ(0b0);
diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 27e0c00..25da335 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -81,7 +81,7 @@ function legalize_misa(m : Misa, v : xlenbits) -> Misa = {
then { /* Allow modifications to C only for now. */
let v = Mk_Misa(v);
/* Suppress changing C if nextPC would become misaligned. */
- if v.C() == false & nextPC[1] == true
+ if v.C() == 0b0 & nextPC[1] == bitone
then m
else update_C(m, v.C())
}
@@ -90,12 +90,12 @@ function legalize_misa(m : Misa, v : xlenbits) -> Misa = {
/* helpers to check support for various extensions. */
/* we currently don't model 'E', so always assume 'I'. */
-function haveAtomics() -> bool = misa.A() == true
-function haveRVC() -> bool = misa.C() == true
-function haveMulDiv() -> bool = misa.M() == true
-function haveSupMode() -> bool = misa.S() == true
-function haveUsrMode() -> bool = misa.U() == true
-function haveNExt() -> bool = misa.N() == true
+function haveAtomics() -> bool = misa.A() == 0b1
+function haveRVC() -> bool = misa.C() == 0b1
+function haveMulDiv() -> bool = misa.M() == 0b1
+function haveSupMode() -> bool = misa.S() == 0b1
+function haveUsrMode() -> bool = misa.U() == 0b1
+function haveNExt() -> bool = misa.N() == 0b1
bitfield Mstatus : xlenbits = {
SD : xlen - 1,
@@ -129,7 +129,7 @@ bitfield Mstatus : xlenbits = {
register mstatus : Mstatus
function effectivePrivilege(m : Mstatus, priv : Privilege) -> Privilege =
- if m.MPRV() == true
+ if m.MPRV() == 0b1
then privLevel_of_bits(mstatus.MPP())
else cur_privilege
@@ -174,16 +174,16 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
*/
// let m = update_FS(m, extStatus_to_bits(Off));
- let m = update_SD(m, extStatus_of_bits(m.FS()) == Dirty
- | extStatus_of_bits(m.XS()) == Dirty);
+ let dirty = extStatus_of_bits(m.FS()) == Dirty | extStatus_of_bits(m.XS()) == Dirty;
+ let m = update_SD(m, bool_to_bits(dirty));
/* We don't support dynamic changes to SXL and UXL. */
let m = set_mstatus_SXL(m, get_mstatus_SXL(o));
let m = set_mstatus_UXL(m, get_mstatus_UXL(o));
/* Hardwired to zero in the absence of 'N'. */
- let m = update_UPIE(m, false);
- let m = update_UIE(m, false);
+ let m = update_UPIE(m, 0b0);
+ let m = update_UIE(m, 0b0);
m
}
@@ -261,9 +261,9 @@ function legalize_mideleg(o : Minterrupts, v : xlenbits) -> Minterrupts = {
/* M-mode interrupt delegation bits "should" be hardwired to 0. */
/* FIXME: needs verification against eventual spec language. */
let m = Mk_Minterrupts(v);
- let m = update_MEI(m, false);
- let m = update_MTI(m, false);
- let m = update_MSI(m, false);
+ let m = update_MEI(m, 0b0);
+ let m = update_MTI(m, 0b0);
+ let m = update_MSI(m, 0b0);
m
}
@@ -290,7 +290,7 @@ register medeleg : Medeleg /* Delegation to S-mode */
function legalize_medeleg(o : Medeleg, v : xlenbits) -> Medeleg = {
let m = Mk_Medeleg(v);
/* M-EnvCalls delegation is not supported */
- let m = update_MEnvCall(m, false);
+ let m = update_MEnvCall(m, 0b0);
m
}
@@ -322,7 +322,7 @@ function tvec_addr(m : Mtvec, c : Mcause) -> option(xlenbits) = {
let base : xlenbits = m.Base() @ 0b00;
match (trapVectorMode_of_bits(m.Mode())) {
TV_Direct => Some(base),
- TV_Vector => if c.IsInterrupt() == true
+ TV_Vector => if c.IsInterrupt() == 0b1
then Some(base + (EXTZ(c.Cause()) << 2))
else Some(base),
TV_Reserved => None()
@@ -337,13 +337,13 @@ register mepc : xlenbits
* When misa.C is writable, it zeroes only xepc[0].
*/
function legalize_xepc(v : xlenbits) -> xlenbits =
- if sys_enable_writable_misa () | misa.C() == true
+ if sys_enable_writable_misa () | misa.C() == 0b1
then [v with 0 = bitzero]
else v & EXTS(0b100)
/* masking for reads to xepc */
function pc_alignment_mask() -> xlenbits =
- ~(EXTZ(if misa.C() == true then 0b00 else 0b10))
+ ~(EXTZ(if misa.C() == 0b1 then 0b00 else 0b10))
/* auxiliary exception registers */
@@ -364,17 +364,17 @@ register scounteren : Counteren
function legalize_mcounteren(c : Counteren, v : xlenbits) -> Counteren = {
/* no HPM counters yet */
- let c = update_IR(c, v[2]);
- let c = update_TM(c, v[1]);
- let c = update_CY(c, v[0]);
+ let c = update_IR(c, [v[2]]);
+ let c = update_TM(c, [v[1]]);
+ let c = update_CY(c, [v[0]]);
c
}
function legalize_scounteren(c : Counteren, v : xlenbits) -> Counteren = {
/* no HPM counters yet */
- let c = update_IR(c, v[2]);
- let c = update_TM(c, v[1]);
- let c = update_CY(c, v[0]);
+ let c = update_IR(c, [v[2]]);
+ let c = update_TM(c, [v[1]]);
+ let c = update_CY(c, [v[0]]);
c
}
@@ -462,8 +462,8 @@ function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = {
let m = update_XS(m, s.XS());
// See comment for mstatus.FS.
let m = update_FS(m, s.FS());
- let m = update_SD(m, extStatus_of_bits(m.FS()) == Dirty
- | extStatus_of_bits(m.XS()) == Dirty);
+ let dirty = extStatus_of_bits(m.FS()) == Dirty | extStatus_of_bits(m.XS()) == Dirty;
+ let m = update_SD(m, bool_to_bits(dirty));
let m = update_SPP(m, s.SPP());
let m = update_SPIE(m, s.SPIE());
@@ -535,8 +535,8 @@ function lift_sip(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterru
let m : Minterrupts = o;
let m = update_SSI(m, s.SSI() & d.SSI());
if haveNExt() then {
- let m = if d.UEI() == true then update_UEI(m, s.UEI()) else m;
- let m = if d.USI() == true then update_USI(m, s.USI()) else m;
+ let m = if d.UEI() == 0b1 then update_UEI(m, s.UEI()) else m;
+ let m = if d.USI() == 0b1 then update_USI(m, s.USI()) else m;
m
} else m
}
@@ -548,13 +548,13 @@ function legalize_sip(m : Minterrupts, d : Minterrupts, v : xlenbits) -> Minterr
/* Returns the new value of mie from the previous mie (o) and the written sie (s) as delegated by mideleg (d). */
function lift_sie(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = {
let m : Minterrupts = o;
- let m = if d.SEI() == true then update_SEI(m, s.SEI()) else m;
- let m = if d.STI() == true then update_STI(m, s.STI()) else m;
- let m = if d.SSI() == true then update_SSI(m, s.SSI()) else m;
+ let m = if d.SEI() == 0b1 then update_SEI(m, s.SEI()) else m;
+ let m = if d.STI() == 0b1 then update_STI(m, s.STI()) else m;
+ let m = if d.SSI() == 0b1 then update_SSI(m, s.SSI()) else m;
if haveNExt() then {
- let m = if d.UEI() == true then update_UEI(m, s.UEI()) else m;
- let m = if d.UTI() == true then update_UTI(m, s.UTI()) else m;
- let m = if d.USI() == true then update_USI(m, s.USI()) else m;
+ let m = if d.UEI() == 0b1 then update_UEI(m, s.UEI()) else m;
+ let m = if d.UTI() == 0b1 then update_UTI(m, s.UTI()) else m;
+ let m = if d.USI() == 0b1 then update_USI(m, s.USI()) else m;
m
} else m
}
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index a47afc3..d8d6de0 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -22,7 +22,7 @@ type csreg = bits(12) /* CSR addressing */
type regno ('n : Int), 0 <= 'n < 32 = atom('n)
-val cast regidx_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
+val regidx_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
function regidx_to_regno b = let 'r = unsigned(b) in r
/* mapping RVC register indices into normal indices */
@@ -65,7 +65,7 @@ function arch_to_bits(a : Architecture) -> arch_xlen =
type priv_level = bits(2)
enum Privilege = {User, Supervisor, Machine}
-val cast privLevel_to_bits : Privilege -> priv_level
+val privLevel_to_bits : Privilege -> priv_level
function privLevel_to_bits (p) =
match (p) {
User => 0b00,
@@ -73,7 +73,7 @@ function privLevel_to_bits (p) =
Machine => 0b11
}
-val cast privLevel_of_bits : priv_level -> Privilege
+val privLevel_of_bits : priv_level -> Privilege
function privLevel_of_bits (p) =
match (p) {
0b00 => User,
@@ -128,7 +128,7 @@ enum InterruptType = {
I_M_External
}
-val cast interruptType_to_bits : InterruptType -> exc_code
+val interruptType_to_bits : InterruptType -> exc_code
function interruptType_to_bits (i) =
match (i) {
I_U_Software => 0x00,
@@ -166,7 +166,7 @@ enum ExceptionType = {
E_CHERI
}
-val cast exceptionType_to_bits : ExceptionType -> exc_code
+val exceptionType_to_bits : ExceptionType -> exc_code
function exceptionType_to_bits(e) =
match (e) {
E_Fetch_Addr_Align => 0x00,
@@ -237,7 +237,7 @@ function internal_error(s) = {
type tv_mode = bits(2)
enum TrapVectorMode = {TV_Direct, TV_Vector, TV_Reserved}
-val cast trapVectorMode_of_bits : tv_mode -> TrapVectorMode
+val trapVectorMode_of_bits : tv_mode -> TrapVectorMode
function trapVectorMode_of_bits (m) =
match (m) {
0b00 => TV_Direct,
@@ -250,7 +250,7 @@ function trapVectorMode_of_bits (m) =
type ext_status = bits(2)
enum ExtStatus = {Off, Initial, Clean, Dirty}
-val cast extStatus_to_bits : ExtStatus -> ext_status
+val extStatus_to_bits : ExtStatus -> ext_status
function extStatus_to_bits(e) =
match (e) {
Off => 0b00,
@@ -259,7 +259,7 @@ function extStatus_to_bits(e) =
Dirty => 0b11
}
-val cast extStatus_of_bits : ext_status -> ExtStatus
+val extStatus_of_bits : ext_status -> ExtStatus
function extStatus_of_bits(e) =
match (e) {
0b00 => Off,
diff --git a/model/riscv_vmem_common.sail b/model/riscv_vmem_common.sail
index c8808f7..690a3c7 100644
--- a/model/riscv_vmem_common.sail
+++ b/model/riscv_vmem_common.sail
@@ -25,36 +25,36 @@ bitfield PTE_Bits : pteAttribs = {
function isPTEPtr(p : pteAttribs) -> bool = {
let a = Mk_PTE_Bits(p);
- a.R() == false & a.W() == false & a.X() == false
+ a.R() == 0b0 & a.W() == 0b0 & a.X() == 0b0
}
function isInvalidPTE(p : pteAttribs) -> bool = {
let a = Mk_PTE_Bits(p);
- a.V() == false | (a.W() == true & a.R() == false)
+ a.V() == 0b0 | (a.W() == 0b1 & a.R() == 0b0)
}
function checkPTEPermission(ac : AccessType, priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits) -> bool = {
match (ac, priv) {
- (Read, User) => p.U() == true & (p.R() == true | (p.X() == true & mxr)),
- (Write, User) => p.U() == true & p.W() == true,
- (ReadWrite, User) => p.U() == true & p.W() == true & (p.R() == true | (p.X() == true & mxr)),
- (Execute, User) => p.U() == true & p.X() == true,
+ (Read, User) => p.U() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr)),
+ (Write, User) => p.U() == 0b1 & p.W() == 0b1,
+ (ReadWrite, User) => p.U() == 0b1 & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr)),
+ (Execute, User) => p.U() == 0b1 & p.X() == 0b1,
- (Read, Supervisor) => (p.U() == false | do_sum) & (p.R() == true | (p.X() == true & mxr)),
- (Write, Supervisor) => (p.U() == false | do_sum) & p.W() == true,
- (ReadWrite, Supervisor) => (p.U() == false | do_sum) & p.W() == true & (p.R() == true | (p.X() == true & mxr)),
- (Execute, Supervisor) => p.U() == false & p.X() == true,
+ (Read, Supervisor) => (p.U() == 0b0 | do_sum) & (p.R() == 0b1 | (p.X() == 0b1 & mxr)),
+ (Write, Supervisor) => (p.U() == 0b0 | do_sum) & p.W() == 0b1,
+ (ReadWrite, Supervisor) => (p.U() == 0b0 | do_sum) & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr)),
+ (Execute, Supervisor) => p.U() == 0b0 & p.X() == 0b1,
(_, Machine) => internal_error("m-mode mem perm check")
}
}
function update_PTE_Bits(p : PTE_Bits, a : AccessType) -> option(PTE_Bits) = {
- let update_d = (a == Write | a == ReadWrite) & p.D() == false; // dirty-bit
- let update_a = p.A() == false; // accessed-bit
+ let update_d = (a == Write | a == ReadWrite) & p.D() == 0b0; // dirty-bit
+ let update_a = p.A() == 0b0; // accessed-bit
if update_d | update_a then {
- let np = update_A(p, true);
- let np = if update_d then update_D(np, true) else np;
+ let np = update_A(p, 0b1);
+ let np = if update_d then update_D(np, 0b1) else np;
Some(np)
} else None()
}
diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail
index 5b640b1..02f8141 100644
--- a/model/riscv_vmem_rv32.sail
+++ b/model/riscv_vmem_rv32.sail
@@ -17,7 +17,7 @@ function translationMode(priv) = {
match arch {
Some(RV32) => {
let s = Mk_Satp32(satp[31..0]);
- if s.Mode() == false then Sbare else Sv32
+ if s.Mode() == 0b0 then Sbare else Sv32
},
_ => internal_error("unsupported address translation arch")
}
@@ -32,8 +32,8 @@ function translateAddr(vAddr, ac) = {
Execute => cur_privilege,
_ => effectivePrivilege(mstatus, cur_privilege)
};
- let mxr : bool = mstatus.MXR() == true;
- let do_sum : bool = mstatus.SUM() == true;
+ let mxr : bool = mstatus.MXR() == 0b1;
+ let do_sum : bool = mstatus.SUM() == 0b1;
let mode : SATPMode = translationMode(effPriv);
let asid = curAsid32(satp);
diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail
index e3cca0b..3153983 100644
--- a/model/riscv_vmem_rv64.sail
+++ b/model/riscv_vmem_rv64.sail
@@ -24,7 +24,7 @@ function translationMode(priv) = {
},
Some(RV32) => {
let s = Mk_Satp32(satp[31..0]);
- if s.Mode() == false then Sbare else Sv32
+ if s.Mode() == 0b0 then Sbare else Sv32
},
_ => internal_error("unsupported address translation arch")
}
@@ -39,8 +39,8 @@ function translateAddr(vAddr, ac) = {
Execute => cur_privilege,
_ => effectivePrivilege(mstatus, cur_privilege)
};
- let mxr : bool = mstatus.MXR() == true;
- let do_sum : bool = mstatus.SUM() == true;
+ let mxr : bool = mstatus.MXR() == 0b1;
+ let do_sum : bool = mstatus.SUM() == 0b1;
let mode : SATPMode = translationMode(effPriv);
let asid = curAsid64(satp);
diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail
index 49d7ec1..23404e3 100644
--- a/model/riscv_vmem_sv32.sail
+++ b/model/riscv_vmem_sv32.sail
@@ -25,7 +25,7 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
let pte = Mk_SV32_PTE(v);
let pbits = pte.BITS();
let pattr = Mk_PTE_Bits(pbits);
- let is_global = global | (pattr.G() == true);
+ let is_global = global | (pattr.G() == 0b1);
/* print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
^ " pt_base=" ^ BitStr(to_phys_addr(ptb))
^ " pt_ofs=" ^ BitStr(to_phys_addr(pt_ofs))
diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail
index a575a07..50a52f0 100644
--- a/model/riscv_vmem_sv39.sail
+++ b/model/riscv_vmem_sv39.sail
@@ -19,7 +19,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
let pte = Mk_SV39_PTE(v);
let pbits = pte.BITS();
let pattr = Mk_PTE_Bits(pbits);
- let is_global = global | (pattr.G() == true);
+ let is_global = global | (pattr.G() == 0b1);
/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
^ " pt_base=" ^ BitStr(ptb)
^ " pt_ofs=" ^ BitStr(pt_ofs)
diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail
index a898ac7..18abafd 100644
--- a/model/riscv_vmem_sv48.sail
+++ b/model/riscv_vmem_sv48.sail
@@ -19,7 +19,7 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global) = {
let pte = Mk_SV48_PTE(v);
let pbits = pte.BITS();
let pattr = Mk_PTE_Bits(pbits);
- let is_global = global | (pattr.G() == true);
+ let is_global = global | (pattr.G() == 0b1);
/* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
^ " pt_base=" ^ BitStr(ptb)
^ " pt_ofs=" ^ BitStr(pt_ofs)
generated by cgit v1.1 at 2024-11-06 00:57:11 +0000