Skip to content

Commit

Permalink
Merge branch 'master' into Zacas_v4
Browse files Browse the repository at this point in the history 
Signed-off-by: ved-rivos <91900059+ved-rivos@users.noreply.github.com>
  • Loading branch information
@ved-rivos
ved-rivos authored Aug 18, 2023
2 parents a6af6d8 + 58cac61 commit 1032cba
Show file tree
Hide file tree
Showing 42 changed files with 250 additions and 251 deletions.
12 changes: 6 additions & 6 deletions model/prelude.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -187,11 +187,11 @@ function get_config_print_reg () = false
function get_config_print_mem () = false
function get_config_print_platform () = false

val EXTS : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
val EXTZ : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
val sign_extend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
val zero_extend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)

function EXTS(m, v) = sail_sign_extend(v, m)
function EXTZ(m, v) = sail_zero_extend(v, m)
function sign_extend(m, v) = sail_sign_extend(v, m)
function zero_extend(m, v) = sail_zero_extend(v, m)

val zeros_implicit : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
function zeros_implicit (n) = sail_zeros(n)
Expand Down Expand Up @@ -245,11 +245,11 @@ overload operator << = {shift_bits_left, shiftl}
/* Ideally these would be sail builtin */

function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) =
let v128 : bits(128) = EXTS(v) in
let v128 : bits(128) = sign_extend(v) in
(v128 >> shift)[63..0]

function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) =
let v64 : bits(64) = EXTS(v) in
let v64 : bits(64) = sign_extend(v) in
(v64 >> shift)[31..0]

infix 7 >>>
Expand Down
12 changes: 6 additions & 6 deletions model/riscv_analysis.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -98,22 +98,22 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
},
RISCV_JAL(imm, rd) => {
if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
let offset : bits(64) = EXTS(imm) in
let offset : bits(64) = sign_extend(imm) in
Nias = [| NIAFP_concrete_address (PC + offset) |];
ik = IK_branch();
},
RISCV_JALR(imm, rs, rd) => {
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
let offset : bits(64) = sign_extend(imm) in
Nias = [| NIAFP_indirect_address() |];
ik = IK_branch();
},
BTYPE(imm, rs2, rs1, op) => {
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
let offset : bits(64) = sign_extend(imm) in
Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |];
},
ITYPE(imm, rs, rd, op) => {
Expand Down Expand Up @@ -271,22 +271,22 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst
},
RISCV_JAL(imm, rd) => {
if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR;
let offset : bits(64) = EXTS(imm) in
let offset : bits(64) = sign_extend(imm) in
Nias = [| NIAFP_concrete_address (PC + offset) |];
ik = IK_branch();
},
RISCV_JALR(imm, rs, rd) => {
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
let offset : bits(64) = sign_extend(imm) in
Nias = [| NIAFP_indirect_address() |];
ik = IK_branch();
},
BTYPE(imm, rs2, rs1, op) => {
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
let offset : bits(64) = sign_extend(imm) in
Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |];
},
ITYPE(imm, rs, rd, op) => {
Expand Down
12 changes: 6 additions & 6 deletions model/riscv_fdext_control.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,12 +83,12 @@ function clause ext_is_CSR_defined (0x001, _) = haveFExt() | haveZfinx()
function clause ext_is_CSR_defined (0x002, _) = haveFExt() | haveZfinx()
function clause ext_is_CSR_defined (0x003, _) = haveFExt() | haveZfinx()

function clause ext_read_CSR (0x001) = Some (EXTZ (fcsr.FFLAGS()))
function clause ext_read_CSR (0x002) = Some (EXTZ (fcsr.FRM()))
function clause ext_read_CSR (0x003) = Some (EXTZ (fcsr.bits()))
function clause ext_read_CSR (0x001) = Some (zero_extend (fcsr.FFLAGS()))
function clause ext_read_CSR (0x002) = Some (zero_extend (fcsr.FRM()))
function clause ext_read_CSR (0x003) = Some (zero_extend (fcsr.bits()))

function clause ext_write_CSR (0x001, value) = { ext_write_fcsr (fcsr.FRM(), value [4..0]); Some(EXTZ(fcsr.FFLAGS())) }
function clause ext_write_CSR (0x002, value) = { ext_write_fcsr (value [2..0], fcsr.FFLAGS()); Some(EXTZ(fcsr.FRM())) }
function clause ext_write_CSR (0x003, value) = { ext_write_fcsr (value [7..5], value [4..0]); Some(EXTZ(fcsr.bits())) }
function clause ext_write_CSR (0x001, value) = { ext_write_fcsr (fcsr.FRM(), value [4..0]); Some(zero_extend(fcsr.FFLAGS())) }
function clause ext_write_CSR (0x002, value) = { ext_write_fcsr (value [2..0], fcsr.FFLAGS()); Some(zero_extend(fcsr.FRM())) }
function clause ext_write_CSR (0x003, value) = { ext_write_fcsr (value [7..5], value [4..0]); Some(zero_extend(fcsr.bits())) }

/* **************************************************************** */
6 changes: 3 additions & 3 deletions model/riscv_fdext_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -356,7 +356,7 @@ function wF_or_X_H(i, data) = {
assert(sys_enable_fdext() != sys_enable_zfinx());
if sys_enable_fdext()
then F_H(i) = data
else X(i) = EXTS(data)
else X(i) = sign_extend(data)
}

val wF_or_X_S : (bits(5), bits(32)) -> unit effect {escape, wreg}
Expand All @@ -365,7 +365,7 @@ function wF_or_X_S(i, data) = {
assert(sys_enable_fdext() != sys_enable_zfinx());
if sys_enable_fdext()
then F_S(i) = data
else X(i) = EXTS(data)
else X(i) = sign_extend(data)
}

val wF_or_X_D : (bits(5), bits(64)) -> unit effect {escape, wreg}
Expand All @@ -375,7 +375,7 @@ function wF_or_X_D(i, data) = {
if sys_enable_fdext()
then F_D(i) = data
else if sizeof(xlen) >= 64
then X(i) = EXTS(data)
then X(i) = sign_extend(data)
else {
assert (i[0] == bitzero);
if i != zeros() then {
Expand Down
8 changes: 4 additions & 4 deletions model/riscv_fetch_rvfi.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -70,9 +70,9 @@

function fetch() -> FetchResult = {
rvfi_inst_data->rvfi_order() = minstret;
rvfi_pc_data->rvfi_pc_rdata() = EXTZ(get_arch_pc());
rvfi_inst_data->rvfi_mode() = EXTZ(privLevel_to_bits(cur_privilege));
rvfi_inst_data->rvfi_ixl() = EXTZ(misa.MXL());
rvfi_pc_data->rvfi_pc_rdata() = zero_extend(get_arch_pc());
rvfi_inst_data->rvfi_mode() = zero_extend(privLevel_to_bits(cur_privilege));
rvfi_inst_data->rvfi_ixl() = zero_extend(misa.MXL());

/* First allow extensions to check pc */
match ext_fetch_check_pc(PC, PC) {
Expand All @@ -85,7 +85,7 @@ function fetch() -> FetchResult = {
TR_Failure(e, _) => F_Error(e, PC),
TR_Address(_, _) => {
let i = rvfi_instruction.rvfi_insn();
rvfi_inst_data->rvfi_insn() = EXTZ(i);
rvfi_inst_data->rvfi_insn() = zero_extend(i);
if (i[1 .. 0] != 0b11)
then F_RVC(i[15 .. 0])
else {
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_freg_type.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@
type fregtype = flenbits

/* default zero register */
let zero_freg : fregtype = EXTZ(0x0)
let zero_freg : fregtype = zero_extend(0x0)

/* default register printer */
val FRegStr : fregtype -> string
Expand Down
9 changes: 4 additions & 5 deletions model/riscv_insts_aext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -179,7 +179,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
/* should only happen in rmem
* rmem: allow SC to fail very early
*/
X(rd) = EXTZ(0b1); RETIRE_SUCCESS
X(rd) = zero_extend(0b1); RETIRE_SUCCESS
} else {
if haveAtomics() then {
/* normal non-rmem case
Expand All @@ -206,7 +206,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
else {
if match_reservation(vaddr) == false then {
/* cannot happen in rmem */
X(rd) = EXTZ(0b1); cancel_reservation(); RETIRE_SUCCESS
X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS
} else {
match translateAddr(vaddr, Write(Data)) { /* Write and ReadWrite are equivalent here:
* both result in a SAMO exception */
Expand All @@ -231,8 +231,8 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
_ => internal_error(__FILE__, __LINE__, "STORECON expected word or double")
};
match (res) {
MemValue(true) => { X(rd) = EXTZ(0b0); cancel_reservation(); RETIRE_SUCCESS },
MemValue(false) => { X(rd) = EXTZ(0b1); cancel_reservation(); RETIRE_SUCCESS },
MemValue(true) => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS },
MemValue(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS },
MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }
}
}
Expand Down Expand Up @@ -387,7 +387,6 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
AMOAND => rs2_val & loaded,
AMOOR => rs2_val | loaded,
AMOCAS => rs2_val,

/* These operations convert bitvectors to integer values using [un]signed,
* and back using to_bits().
*/
Expand Down
32 changes: 16 additions & 16 deletions model/riscv_insts_base.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ mapping clause encdec = UTYPE(imm, rd, op)
<-> imm @ rd @ encdec_uop(op)

function clause execute UTYPE(imm, rd, op) = {
let off : xlenbits = EXTS(imm @ 0x000);
let off : xlenbits = sign_extend(imm @ 0x000);
let ret : xlenbits = match op {
RISCV_LUI => off,
RISCV_AUIPC => get_arch_pc() + off
Expand Down Expand Up @@ -120,7 +120,7 @@ but this is difficult
*/

function clause execute (RISCV_JAL(imm, rd)) = {
let t : xlenbits = PC + EXTS(imm);
let t : xlenbits = PC + sign_extend(imm);
/* Extensions get the first checks on the prospective target address. */
match ext_control_check_pc(t) {
Ext_ControlAddr_Error(e) => {
Expand Down Expand Up @@ -184,7 +184,7 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = {
RISCV_BLTU => rs1_val <_u rs2_val,
RISCV_BGEU => rs1_val >=_u rs2_val
};
let t : xlenbits = PC + EXTS(imm);
let t : xlenbits = PC + sign_extend(imm);
if taken then {
/* Extensions get the first checks on the prospective target address. */
match ext_control_check_pc(t) {
Expand Down Expand Up @@ -234,11 +234,11 @@ mapping clause encdec = ITYPE(imm, rs1, rd, op)

function clause execute (ITYPE (imm, rs1, rd, op)) = {
let rs1_val = X(rs1);
let immext : xlenbits = EXTS(imm);
let immext : xlenbits = sign_extend(imm);
let result : xlenbits = match op {
RISCV_ADDI => rs1_val + immext,
RISCV_SLTI => EXTZ(bool_to_bits(rs1_val <_s immext)),
RISCV_SLTIU => EXTZ(bool_to_bits(rs1_val <_u immext)),
RISCV_SLTI => zero_extend(bool_to_bits(rs1_val <_s immext)),
RISCV_SLTIU => zero_extend(bool_to_bits(rs1_val <_u immext)),
RISCV_ANDI => rs1_val & immext,
RISCV_ORI => rs1_val | immext,
RISCV_XORI => rs1_val ^ immext
Expand Down Expand Up @@ -318,8 +318,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(bool_to_bits(rs1_val <_s rs2_val)),
RISCV_SLTU => EXTZ(bool_to_bits(rs1_val <_u 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_AND => rs1_val & rs2_val,
RISCV_OR => rs1_val | rs2_val,
RISCV_XOR => rs1_val ^ rs2_val,
Expand Down Expand Up @@ -364,7 +364,7 @@ mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if (

val extend_value : forall 'n, 0 < 'n <= xlen_bytes. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits)
function extend_value(is_unsigned, value) = match (value) {
MemValue(v) => MemValue(if is_unsigned then EXTZ(v) else EXTS(v) : xlenbits),
MemValue(v) => MemValue(if is_unsigned then zero_extend(v) else sign_extend(v) : xlenbits),
MemException(e) => MemException(e)
}

Expand All @@ -385,7 +385,7 @@ function check_misaligned(vaddr : xlenbits, width : word_width) -> bool =
}

function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
let offset : xlenbits = EXTS(imm);
let offset : xlenbits = sign_extend(imm);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Read(Data), width) {
Expand Down Expand Up @@ -441,7 +441,7 @@ mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false)
/* NOTE: Currently, we only EA if address translation is successful.
This may need revisiting. */
function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
let offset : xlenbits = EXTS(imm);
let offset : xlenbits = sign_extend(imm);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Write(Data), width) {
Expand Down Expand Up @@ -494,8 +494,8 @@ mapping clause encdec = ADDIW(imm, rs1, rd)
if sizeof(xlen) == 64

function clause execute (ADDIW(imm, rs1, rd)) = {
let result : xlenbits = EXTS(imm) + X(rs1);
X(rd) = EXTS(result[31..0]);
let result : xlenbits = sign_extend(imm) + X(rs1);
X(rd) = sign_extend(result[31..0]);
RETIRE_SUCCESS
}

Expand Down Expand Up @@ -527,7 +527,7 @@ function clause execute (SHIFTW(shamt, rs1, rd, op)) = {
RISCV_SRLI => rs1_val >> shamt,
RISCV_SRAI => shift_right_arith32(rs1_val, shamt)
};
X(rd) = EXTS(result);
X(rd) = sign_extend(result);
RETIRE_SUCCESS
}

Expand Down Expand Up @@ -576,7 +576,7 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) = {
RISCV_SRLW => rs1_val >> (rs2_val[4..0]),
RISCV_SRAW => shift_right_arith32(rs1_val, rs2_val[4..0])
};
X(rd) = EXTS(result);
X(rd) = sign_extend(result);
RETIRE_SUCCESS
}

Expand Down Expand Up @@ -616,7 +616,7 @@ function clause execute (SHIFTIWOP(shamt, rs1, rd, op)) = {
RISCV_SRLIW => rs1_val[31..0] >> shamt,
RISCV_SRAIW => shift_right_arith32(rs1_val[31..0], shamt)
};
X(rd) = EXTS(result);
X(rd) = sign_extend(result);
RETIRE_SUCCESS
}

Expand Down
8 changes: 4 additions & 4 deletions model/riscv_insts_cdext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ mapping clause encdec_compressed = C_FLDSP(ui86 @ ui5 @ ui43, rd)
if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()

function clause execute (C_FLDSP(uimm, rd)) = {
let imm : bits(12) = EXTZ(uimm @ 0b000);
let imm : bits(12) = zero_extend(uimm @ 0b000);
execute(LOAD_FP(imm, sp, rd, DOUBLE))
}

Expand All @@ -102,7 +102,7 @@ mapping clause encdec_compressed = C_FSDSP(ui86 @ ui53, rs2)
if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()

function clause execute (C_FSDSP(uimm, rs2)) = {
let imm : bits(12) = EXTZ(uimm @ 0b000);
let imm : bits(12) = zero_extend(uimm @ 0b000);
execute(STORE_FP(imm, rs2, sp, DOUBLE))
}

Expand All @@ -120,7 +120,7 @@ mapping clause encdec_compressed = C_FLD(ui76 @ ui53, rs1, rd)
if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()

function clause execute (C_FLD(uimm, rsc, rdc)) = {
let imm : bits(12) = EXTZ(uimm @ 0b000);
let imm : bits(12) = zero_extend(uimm @ 0b000);
let rd = creg2reg_idx(rdc);
let rs = creg2reg_idx(rsc);
execute(LOAD_FP(imm, rs, rd, DOUBLE))
Expand All @@ -140,7 +140,7 @@ mapping clause encdec_compressed = C_FSD(ui76 @ ui53, rs1, rs2)
if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()

function clause execute (C_FSD(uimm, rsc1, rsc2)) = {
let imm : bits(12) = EXTZ(uimm @ 0b000);
let imm : bits(12) = zero_extend(uimm @ 0b000);
let rs1 = creg2reg_idx(rsc1);
let rs2 = creg2reg_idx(rsc2);
execute(STORE_FP(imm, rs2, rs1, DOUBLE))
Expand Down
Loading

0 comments on commit 1032cba

Please sign in to comment.