Skip to content

Commit

Permalink
Use bool <-> bit mappings from riscv_types.sail everywhere
Browse files Browse the repository at this point in the history 
A minor refactor to use these mapping types everywhere instead of functions.
  • Loading branch information
@Timmmm
Timmmm committed Jun 11, 2024
1 parent 7ff6d94 commit 5075064
Show file tree
Hide file tree
Showing 17 changed files with 83 additions and 90 deletions.
19 changes: 11 additions & 8 deletions model/prelude.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -99,16 +99,19 @@ overload zeros = {zeros_implicit}
val ones : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
function ones (n) = sail_ones (n)

val bool_to_bit : bool -> bit
function bool_to_bit x = if x then bitone else bitzero
mapping bool_bit : bool <-> bit = {
true <-> bitone,
false <-> bitzero,
}

val bool_to_bits : bool -> bits(1)
function bool_to_bits x = [bool_to_bit(x)]
mapping bool_bits : bool <-> bits(1) = {
true <-> 0b1,
false <-> 0b0,
}

val bit_to_bool : bit -> bool
function bit_to_bool b = match b {
bitone => true,
bitzero => false
mapping bool_not_bits : bool <-> bits(1) = {
true <-> 0b0,
false <-> 0b1,
}

val to_bits : forall 'l, 'l >= 0.(int('l), int) -> bits('l)
Expand Down
12 changes: 6 additions & 6 deletions model/riscv_insts_base.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ function clause execute (RISCV_JAL(imm, rd)) = {
},
Ext_ControlAddr_OK(target) => {
/* Perform standard alignment check */
if bit_to_bool(target[1]) & not(haveRVC())
if bool_bit(target[1]) & not(haveRVC())
then {
handle_mem_exception(target, E_Fetch_Addr_Align());
RETIRE_FAIL
Expand Down Expand Up @@ -131,7 +131,7 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = {
RETIRE_FAIL
},
Ext_ControlAddr_OK(target) => {
if bit_to_bool(target[1]) & not(haveRVC()) then {
if bool_bit(target[1]) & not(haveRVC()) then {
handle_mem_exception(target, E_Fetch_Addr_Align());
RETIRE_FAIL;
} else {
Expand Down Expand Up @@ -175,8 +175,8 @@ function clause execute (ITYPE (imm, rs1, rd, op)) = {
let immext : xlenbits = sign_extend(imm);
let result : xlenbits = match op {
RISCV_ADDI => rs1_val + immext,
RISCV_SLTI => zero_extend(bool_to_bits(rs1_val <_s immext)),
RISCV_SLTIU => zero_extend(bool_to_bits(rs1_val <_u immext)),
RISCV_SLTI => zero_extend(bool_bits(rs1_val <_s immext)),
RISCV_SLTIU => zero_extend(bool_bits(rs1_val <_u immext)),
RISCV_ANDI => rs1_val & immext,
RISCV_ORI => rs1_val | immext,
RISCV_XORI => rs1_val ^ immext
Expand Down Expand Up @@ -256,8 +256,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 => zero_extend(bool_to_bits(rs1_val <_s rs2_val)),
RISCV_SLTU => zero_extend(bool_to_bits(rs1_val <_u rs2_val)),
RISCV_SLT => zero_extend(bool_bits(rs1_val <_s rs2_val)),
RISCV_SLTU => zero_extend(bool_bits(rs1_val <_u rs2_val)),
RISCV_AND => rs1_val & rs2_val,
RISCV_OR => rs1_val | rs2_val,
RISCV_XOR => rs1_val ^ rs2_val,
Expand Down
6 changes: 3 additions & 3 deletions model/riscv_insts_dext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -801,7 +801,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = {
riscv_f64Eq (rs1_val_D, rs2_val_D);

accrue_fflags(fflags);
X(rd) = zero_extend(bool_to_bits(rd_val));
X(rd) = zero_extend(bool_bits(rd_val));
RETIRE_SUCCESS
}

Expand All @@ -813,7 +813,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)) = {
riscv_f64Lt (rs1_val_D, rs2_val_D);

accrue_fflags(fflags);
X(rd) = zero_extend(bool_to_bits(rd_val));
X(rd) = zero_extend(bool_bits(rd_val));
RETIRE_SUCCESS
}

Expand All @@ -825,7 +825,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLE_D)) = {
riscv_f64Le (rs1_val_D, rs2_val_D);

accrue_fflags(fflags);
X(rd) = zero_extend(bool_to_bits(rd_val));
X(rd) = zero_extend(bool_bits(rd_val));
RETIRE_SUCCESS
}

Expand Down
6 changes: 3 additions & 3 deletions model/riscv_insts_fext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -925,7 +925,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)) = {
riscv_f32Eq (rs1_val_S, rs2_val_S);

accrue_fflags(fflags);
X(rd) = zero_extend(bool_to_bits(rd_val));
X(rd) = zero_extend(bool_bits(rd_val));
RETIRE_SUCCESS
}

Expand All @@ -937,7 +937,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)) = {
riscv_f32Lt (rs1_val_S, rs2_val_S);

accrue_fflags(fflags);
X(rd) = zero_extend(bool_to_bits(rd_val));
X(rd) = zero_extend(bool_bits(rd_val));
RETIRE_SUCCESS
}

Expand All @@ -949,7 +949,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLE_S)) = {
riscv_f32Le (rs1_val_S, rs2_val_S);

accrue_fflags(fflags);
X(rd) = zero_extend(bool_to_bits(rd_val));
X(rd) = zero_extend(bool_bits(rd_val));
RETIRE_SUCCESS
}

Expand Down
4 changes: 2 additions & 2 deletions model/riscv_insts_vext_utils.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -574,10 +574,10 @@ function get_fixed_rounding_incr(vec_elem, shift_amount) = {
let rounding_mode = vxrm[1 .. 0];
match rounding_mode {
0b00 => slice(vec_elem, shift_amount - 1, 1),
0b01 => bool_to_bits(
0b01 => bool_bits(
(slice(vec_elem, shift_amount - 1, 1) == 0b1) & (slice(vec_elem, 0, shift_amount - 1) != zeros() | slice(vec_elem, shift_amount, 1) == 0b1)),
0b10 => 0b0,
0b11 => bool_to_bits(
0b11 => bool_bits(
not(slice(vec_elem, shift_amount, 1) == 0b1) & (slice(vec_elem, 0, shift_amount) != zeros()))
}
}
Expand Down
20 changes: 10 additions & 10 deletions model/riscv_insts_vext_vm.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,8 +47,8 @@ function clause execute(VVMTYPE(funct6, vs2, vs1, vd)) = {
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
let res : bool = match funct6 {
VVM_VMADC => unsigned(vs2_val[i]) + unsigned(vs1_val[i]) + unsigned(bool_to_bits(vm_val[i])) > 2 ^ SEW - 1,
VVM_VMSBC => unsigned(vs2_val[i]) - unsigned(vs1_val[i]) - unsigned(bool_to_bits(vm_val[i])) < 0
VVM_VMADC => unsigned(vs2_val[i]) + unsigned(vs1_val[i]) + unsigned(bool_bits(vm_val[i])) > 2 ^ SEW - 1,
VVM_VMSBC => unsigned(vs2_val[i]) - unsigned(vs1_val[i]) - unsigned(bool_bits(vm_val[i])) < 0
};
result[i] = res
}
Expand Down Expand Up @@ -164,8 +164,8 @@ function clause execute(VVMSTYPE(funct6, vs2, vs1, vd)) = {
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
result[i] = match funct6 {
VVMS_VADC => to_bits(SEW, unsigned(vs2_val[i]) + unsigned(vs1_val[i]) + unsigned(bool_to_bits(vm_val[i]))),
VVMS_VSBC => to_bits(SEW, unsigned(vs2_val[i]) - unsigned(vs1_val[i]) - unsigned(bool_to_bits(vm_val[i])))
VVMS_VADC => to_bits(SEW, unsigned(vs2_val[i]) + unsigned(vs1_val[i]) + unsigned(bool_bits(vm_val[i]))),
VVMS_VSBC => to_bits(SEW, unsigned(vs2_val[i]) - unsigned(vs1_val[i]) - unsigned(bool_bits(vm_val[i])))
}
}
};
Expand Down Expand Up @@ -285,8 +285,8 @@ function clause execute(VXMTYPE(funct6, vs2, rs1, vd)) = {
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
let res : bool = match funct6 {
VXM_VMADC => unsigned(vs2_val[i]) + unsigned(rs1_val) + unsigned(bool_to_bits(vm_val[i])) > 2 ^ SEW - 1,
VXM_VMSBC => unsigned(vs2_val[i]) - unsigned(rs1_val) - unsigned(bool_to_bits(vm_val[i])) < 0
VXM_VMADC => unsigned(vs2_val[i]) + unsigned(rs1_val) + unsigned(bool_bits(vm_val[i])) > 2 ^ SEW - 1,
VXM_VMSBC => unsigned(vs2_val[i]) - unsigned(rs1_val) - unsigned(bool_bits(vm_val[i])) < 0
};
result[i] = res
}
Expand Down Expand Up @@ -402,8 +402,8 @@ function clause execute(VXMSTYPE(funct6, vs2, rs1, vd)) = {
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
result[i] = match funct6 {
VXMS_VADC => to_bits(SEW, unsigned(vs2_val[i]) + unsigned(rs1_val) + unsigned(bool_to_bits(vm_val[i]))),
VXMS_VSBC => to_bits(SEW, unsigned(vs2_val[i]) - unsigned(rs1_val) - unsigned(bool_to_bits(vm_val[i])))
VXMS_VADC => to_bits(SEW, unsigned(vs2_val[i]) + unsigned(rs1_val) + unsigned(bool_bits(vm_val[i]))),
VXMS_VSBC => to_bits(SEW, unsigned(vs2_val[i]) - unsigned(rs1_val) - unsigned(bool_bits(vm_val[i])))
}
}
};
Expand Down Expand Up @@ -528,7 +528,7 @@ function clause execute(VIMTYPE(funct6, vs2, simm, vd)) = {
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
let res : bool = match funct6 {
VIM_VMADC => unsigned(vs2_val[i]) + unsigned(imm_val) + unsigned(bool_to_bits(vm_val[i])) > 2 ^ SEW - 1
VIM_VMADC => unsigned(vs2_val[i]) + unsigned(imm_val) + unsigned(bool_bits(vm_val[i])) > 2 ^ SEW - 1
};
result[i] = res
}
Expand Down Expand Up @@ -639,7 +639,7 @@ function clause execute(VIMSTYPE(funct6, vs2, simm, vd)) = {
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
result[i] = match funct6 {
VIMS_VADC => to_bits(SEW, unsigned(vs2_val[i]) + unsigned(imm_val) + unsigned(bool_to_bits(vm_val[i])))
VIMS_VADC => to_bits(SEW, unsigned(vs2_val[i]) + unsigned(imm_val) + unsigned(bool_bits(vm_val[i])))
}
}
};
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_insts_zbs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ function clause execute (ZBS_IOP(shamt, rs1, rd, op)) = {
else zero_extend(0b1) << shamt;
let result : xlenbits = match op {
RISCV_BCLRI => rs1_val & ~(mask),
RISCV_BEXTI => zero_extend(bool_to_bits((rs1_val & mask) != zeros())),
RISCV_BEXTI => zero_extend(bool_bits((rs1_val & mask) != zeros())),
RISCV_BINVI => rs1_val ^ mask,
RISCV_BSETI => rs1_val | mask
};
Expand Down Expand Up @@ -79,7 +79,7 @@ function clause execute (ZBS_RTYPE(rs2, rs1, rd, op)) = {
else zero_extend(0b1) << rs2_val[5..0];
let result : xlenbits = match op {
RISCV_BCLR => rs1_val & ~(mask),
RISCV_BEXT => zero_extend(bool_to_bits((rs1_val & mask) != zeros())),
RISCV_BEXT => zero_extend(bool_bits((rs1_val & mask) != zeros())),
RISCV_BINV => rs1_val ^ mask,
RISCV_BSET => rs1_val | mask
};
Expand Down
12 changes: 6 additions & 6 deletions model/riscv_insts_zfa.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -566,7 +566,7 @@ function clause execute(RISCV_FLEQ_H(rs2, rs1, rd)) = {
riscv_f16Le_quiet (rs1_val_H, rs2_val_H);

accrue_fflags(fflags);
X(rd) = zero_extend(bool_to_bits(rd_val));
X(rd) = zero_extend(bool_bits(rd_val));
RETIRE_SUCCESS
}

Expand All @@ -590,7 +590,7 @@ function clause execute(RISCV_FLTQ_H(rs2, rs1, rd)) = {
riscv_f16Lt_quiet (rs1_val_H, rs2_val_H);

accrue_fflags(fflags);
X(rd) = zero_extend(bool_to_bits(rd_val));
X(rd) = zero_extend(bool_bits(rd_val));
RETIRE_SUCCESS
}

Expand All @@ -614,7 +614,7 @@ function clause execute(RISCV_FLEQ_S(rs2, rs1, rd)) = {
riscv_f32Le_quiet (rs1_val_S, rs2_val_S);

accrue_fflags(fflags);
X(rd) = zero_extend(bool_to_bits(rd_val));
X(rd) = zero_extend(bool_bits(rd_val));
RETIRE_SUCCESS
}

Expand All @@ -638,7 +638,7 @@ function clause execute(RISCV_FLTQ_S(rs2, rs1, rd)) = {
riscv_f32Lt_quiet (rs1_val_S, rs2_val_S);

accrue_fflags(fflags);
X(rd) = zero_extend(bool_to_bits(rd_val));
X(rd) = zero_extend(bool_bits(rd_val));
RETIRE_SUCCESS
}

Expand All @@ -663,7 +663,7 @@ function clause execute(RISCV_FLEQ_D(rs2, rs1, rd)) = {
riscv_f64Le_quiet (rs1_val_D, rs2_val_D);

accrue_fflags(fflags);
X(rd) = zero_extend(bool_to_bits(rd_val));
X(rd) = zero_extend(bool_bits(rd_val));
RETIRE_SUCCESS
}

Expand All @@ -687,7 +687,7 @@ function clause execute(RISCV_FLTQ_D(rs2, rs1, rd)) = {
riscv_f64Lt_quiet (rs1_val_D, rs2_val_D);

accrue_fflags(fflags);
X(rd) = zero_extend(bool_to_bits(rd_val));
X(rd) = zero_extend(bool_bits(rd_val));
RETIRE_SUCCESS
}

Expand Down
6 changes: 3 additions & 3 deletions model/riscv_insts_zfh.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -416,7 +416,7 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FEQ_H)) = {
riscv_f16Eq (rs1_val_H, rs2_val_H);

accrue_fflags(fflags);
X(rd) = zero_extend(bool_to_bits(rd_val));
X(rd) = zero_extend(bool_bits(rd_val));
RETIRE_SUCCESS
}

Expand All @@ -428,7 +428,7 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FLT_H)) = {
riscv_f16Lt (rs1_val_H, rs2_val_H);

accrue_fflags(fflags);
X(rd) = zero_extend(bool_to_bits(rd_val));
X(rd) = zero_extend(bool_bits(rd_val));
RETIRE_SUCCESS
}

Expand All @@ -440,7 +440,7 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FLE_H)) = {
riscv_f16Le (rs1_val_H, rs2_val_H);

accrue_fflags(fflags);
X(rd) = zero_extend(bool_to_bits(rd_val));
X(rd) = zero_extend(bool_bits(rd_val));
RETIRE_SUCCESS
}

Expand Down
2 changes: 1 addition & 1 deletion model/riscv_jalr_seq.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = {
},
Ext_ControlAddr_OK(addr) => {
let target = [addr with 0 = bitzero]; /* clear addr[0] */
if bit_to_bool(target[1]) & not(haveRVC()) then {
if bool_bit(target[1]) & not(haveRVC()) then {
handle_mem_exception(target, E_Fetch_Addr_Align());
RETIRE_FAIL
} else {
Expand Down
Loading

0 comments on commit 5075064

Please sign in to comment.