diff options
| -rw-r--r-- | Makefile | 14 | ||||
| -rw-r--r-- | model/riscv_fdext_regs.sail | 8 | ||||
| -rw-r--r-- | model/riscv_insts_fdext.sail | 308 |
3 files changed, 194 insertions, 136 deletions
@@ -17,7 +17,8 @@ endif # Instruction sources, depending on target SAIL_CHECK_SRCS = riscv_addr_checks_common.sail riscv_addr_checks.sail riscv_misa_ext.sail -SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_aext.sail riscv_insts_cext.sail riscv_insts_mext.sail riscv_insts_zicsr.sail riscv_insts_next.sail +SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_aext.sail riscv_insts_cext.sail riscv_insts_mext.sail riscv_insts_zicsr.sail riscv_insts_next.sail riscv_insts_fdext.sail + SAIL_SEQ_INST = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail SAIL_RMEM_INST = $(SAIL_DEFAULT_INST) riscv_jalr_rmem.sail riscv_insts_rmem.sail @@ -50,10 +51,15 @@ SAIL_REGS_SRCS = riscv_reg_type.sail riscv_regs.sail riscv_pc_access.sail riscv_ SAIL_REGS_SRCS += riscv_pmp_regs.sail riscv_pmp_control.sail SAIL_REGS_SRCS += riscv_ext_regs.sail $(SAIL_CHECK_SRCS) +SAIL_FD_SRCS = riscv_flen_D.sail +SAIL_FD_SRCS += riscv_freg_type.sail +SAIL_FD_SRCS += riscv_fdext_regs.sail + SAIL_ARCH_SRCS = $(PRELUDE) SAIL_ARCH_SRCS += riscv_types_ext.sail riscv_types.sail SAIL_ARCH_SRCS += riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail SAIL_ARCH_SRCS += riscv_mem.sail $(SAIL_VM_SRCS) +SAIL_ARCH_SRCS += $(SAIL_FD_SRCS) SAIL_ARCH_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail $(SAIL_VM_SRCS) SAIL_STEP_SRCS = riscv_step_common.sail riscv_step_ext.sail riscv_decode_ext.sail riscv_fetch.sail riscv_step.sail RVFI_STEP_SRCS = riscv_step_common.sail riscv_step_rvfi.sail riscv_decode_ext.sail riscv_fetch_rvfi.sail riscv_step.sail @@ -139,6 +145,12 @@ else RISCV_EXTRAS_LEM = riscv_extras.lem endif +.PHONY: test +test: + touch model/riscv_insts_base.sail + make ocaml_emulator/riscv_ocaml_sim_$(ARCH) + ./ocaml_emulator/riscv_ocaml_sim_RV64 test/riscv-tests/rv64ui-p-add.elf + all: ocaml_emulator/riscv_ocaml_sim_$(ARCH) c_emulator/riscv_sim_$(ARCH) riscv_isa riscv_coq riscv_hol riscv_rmem .PHONY: all diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail index e7163ac..6ce6403 100644 --- a/model/riscv_fdext_regs.sail +++ b/model/riscv_fdext_regs.sail @@ -121,7 +121,13 @@ function wF (r, in_v) = { print_reg("f" ^ string_of_int(r) ^ " <- " ^ FRegStr(v)); } -overload F = {rF, wF} +function rF_bits(i: bits(5)) -> xlenbits = rF(unsigned(i)) + +function wF_bits(i: bits(5), data: xlenbits) -> unit = { + wF(unsigned(i)) = data +} + +overload F = {rF_bits, wF_bits, rF, wF} /* register names */ diff --git a/model/riscv_insts_fdext.sail b/model/riscv_insts_fdext.sail index 014dbff..a09c21a 100644 --- a/model/riscv_insts_fdext.sail +++ b/model/riscv_insts_fdext.sail @@ -11,7 +11,7 @@ enum rounding_mode = {RM_RNE, RM_RTZ, RM_RDN, RM_RUP, RM_RMM, RM_DYN} -mapping encdec_rounding_mode : rounding_mode <-> bits(3) = { +mapping rounding_mode_bits : rounding_mode <-> bits(3) = { RM_RNE <-> 0b000, RM_RTZ <-> 0b001, RM_RDN <-> 0b010, @@ -26,71 +26,72 @@ mapping frm_mnemonic : rounding_mode <-> string = { RM_RDN <-> "rdn", RM_RUP <-> "rup", RM_RMM <-> "rmm", - RM_DYN <-> "dyn", + RM_DYN <-> "dyn" } /* **************************************************************** */ /* Help-functions for 'encdec()' to restrict to certain */ /* combinations of {F,D} x {RV32,RV64} */ -function is_RV32F_or_RV64F () -> bool = (haveFExt & (sizeof(xlen)=32 | sizeof(xlen)=64)) -function is_RV64F () -> bool = (haveFExt & sizeof(xlen)=64) +function is_RV32F_or_RV64F () -> bool = (haveFExt() & (sizeof(xlen) == 32 | sizeof(xlen) == 64)) +function is_RV64F () -> bool = (haveFExt() & sizeof(xlen) == 64) -function is_RV32D_or_RV64D () -> bool = (haveDExt & (sizeof(xlen)=32 | sizeof(xlen)=64)) -function is_RV64D () -> bool = (haveDExt & sizeof(xlen)=64) +function is_RV32D_or_RV64D () -> bool = (haveDExt() & (sizeof(xlen) == 32 | sizeof(xlen) == 64)) +function is_RV64D () -> bool = (haveDExt() & sizeof(xlen) == 64) /* ****************************************************************** */ /* Floating-point loads */ /* AST */ -/* FLW and FLD; W/D is encoded in 'width' */ +/* FLW and FLD; W/D is encoded in 'word_width' */ union clause ast = LOAD_FP : (bits(12), regidx, regidx, word_width) /* AST <-> Binary encoding ================================ */ -mapping clause encdec = LOAD_FP(imm, rs1, rd, WORD) if is_RV32F_or_RV64F - <-> imm @ rs1 @ 3b010 @ rd @ 0b000_0111 if is_RV32F_or_RV64F +mapping clause encdec = LOAD_FP(imm, rs1, rd, WORD) if is_RV32F_or_RV64F() + <-> imm @ rs1 @ 0b010 @ rd @ 0b000_0111 if is_RV32F_or_RV64F() -mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE) if is_RV32D_or_RV64D - <-> imm @ rs1 @ 3b011 @ rd @ 0b000_0111 if is_RV32D_or_RV64D +mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE) if is_RV32D_or_RV64D() + <-> imm @ rs1 @ 0b011 @ rd @ 0b000_0111 if is_RV32D_or_RV64D() /* Execution semantics ================================ */ -function clause execute(LOAD_FP(imm, rs1, rd, width) = { +val process_fload : forall 'n, 0 < 'n <= xlen_bytes. + (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) + -> Retired effect {escape, rreg, wreg} +function process_fload(rd, addr, value, is_unsigned) = + match extend_value(is_unsigned, value) { + MemValue(result) => { F(rd) = result; RETIRE_SUCCESS }, + MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } + } + +function clause execute(LOAD_FP(imm, rs1, rd, width)) = { let offset : xlenbits = EXTS(imm); /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ - match ext_data_get_addr(rs1, offset, Read, width) { + match ext_data_get_addr(rs1, offset, Read(Data), width) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width) - then { handle_mem_exception(vaddr, E_Load_Addr_Align); RETIRE_FAIL } - else match translateAddr(vaddr, Read) { - TR_Failure(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, - TR_Address(addr) => - let (aq, rl, res, is_unsigned) = (false, false, false, false) + then { handle_mem_exception(vaddr, E_Load_Addr_Align()); RETIRE_FAIL } + else match translateAddr(vaddr, Read(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Address(addr, _) => { + let (aq, rl, res, is_unsigned) = (false, false, false, false); match (width, sizeof(xlen)) { - (BYTE, _) => { handle_illegal(); RETIRE_FAIL } - (HALF, _) => { handle_illegal(); RETIRE_FAIL } + (BYTE, _) => { handle_illegal(); RETIRE_FAIL }, + (HALF, _) => { handle_illegal(); RETIRE_FAIL }, (WORD, _) => - process_fload(rd, vaddr, mem_read(Read, addr, 4, aq, rl, res), is_unsigned), + process_fload(rd, vaddr, mem_read(Read(Data), addr, 4, aq, rl, res), is_unsigned), (DOUBLE, 64) => - process_fload(rd, vaddr, mem_read(Read, addr, 8, aq, rl, res), is_unsigned) + process_fload(rd, vaddr, mem_read(Read(Data), addr, 8, aq, rl, res), is_unsigned) } + } } } } -val process_fload : forall 'n, 0 < 'n <= xlen_bytes. - (regidx, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) - -> Retired effect {escape, rreg, wreg} -function process_fload(rd, addr, value, is_unsigned) = - match extend_value(is_unsigned, value) { - MemValue(result) => { F(rd) = result; RETIRE_SUCCESS }, - MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } - } - /* AST -> Assembly notation ================================ */ mapping clause assembly = LOAD_FP(imm, rs1, rd, width) @@ -105,20 +106,29 @@ mapping clause assembly = LOAD_FP(imm, rs1, rd, width) /* AST */ /* FLW and FLD; W/D is encoded in 'width' */ -union clause ast = STORE_FP : (bits(12), regidx, regidx, width) +union clause ast = STORE_FP : (bits(12), regidx, regidx, word_width) /* AST <-> Binary encoding ================================ */ -mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, WORD) if is_RV32F_or_RV64F - <-> imm7 : bits(7) @ rs2 @ rs1 @ 3b010 @ imm5 : bits(5) @ 0b010_0111 if is_RV32F_or_RV64F +mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, WORD) if is_RV32F_or_RV64F() + <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b010 @ imm5 : bits(5) @ 0b010_0111 if is_RV32F_or_RV64F() -mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, DOUBLE) if is_RV32D_or_RV64D - <-> imm7 : bits(7) @ rs2 @ rs1 @ 3b011 @ imm5 : bits(5) @ 0b010_0111 if is_RV32D_or_RV64D +mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, DOUBLE) if is_RV32D_or_RV64D() + <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b011 @ imm5 : bits(5) @ 0b010_0111 if is_RV32D_or_RV64D() /* Execution semantics ================================ */ -function clause execute (STORE_FP(imm, rs2, rs1, width) = { +val process_fstore : (xlenbits, MemoryOpResult(bool)) -> Retired effect {escape, rreg, wreg} +function process_fstore(vaddr, value) = + match value { + MemValue(true) => { RETIRE_SUCCESS }, + MemValue(false) => { internal_error("store got false from mem_write_value") }, + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + } + +function clause execute (STORE_FP(imm, rs2, rs1, width)) = { let offset : xlenbits = EXTS(imm); + let (aq, rl, con) = (false, false, false); /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ match ext_data_get_addr(rs1, offset, Write(Data), width) { @@ -130,8 +140,8 @@ function clause execute (STORE_FP(imm, rs2, rs1, width) = { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, TR_Address(addr, _) => { let eares : MemoryOpResult(unit) = match width { - BYTE => { /* no action */ } - HALF => { /* no action */ } + BYTE => MemValue () /* bogus placeholder for illegal size */, + HALF => MemValue () /* bogus placeholder for illegal size */, WORD => mem_write_ea(addr, 4, aq, rl, false), DOUBLE => mem_write_ea(addr, 8, aq, rl, false) }; @@ -139,10 +149,9 @@ function clause execute (STORE_FP(imm, rs2, rs1, width) = { MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL }, MemValue(_) => { let rs2_val = F(rs2); - let (aq, rl, con) = (false, false, false) match (width, sizeof(xlen)) { - (BYTE, _) => { handle_illegal(); RETIRE_FAIL } - (HALF, _) => { handle_illegal(); RETIRE_FAIL } + (BYTE, _) => { handle_illegal(); RETIRE_FAIL }, + (HALF, _) => { handle_illegal(); RETIRE_FAIL }, (WORD, _) => process_fstore (vaddr, mem_write_value(addr, 4, rs2_val[31..0], aq, rl, con)), (DOUBLE, 64) => process_fstore (vaddr, mem_write_value(addr, 8, rs2_val, aq, rl, con)) }; @@ -153,15 +162,6 @@ function clause execute (STORE_FP(imm, rs2, rs1, width) = { } } -val process_fstore : forall 'n, 0 < 'n <= xlen_bytes. - (xlenbits, MemoryOpResult(bool) -> Retired effect {escape, rreg, wreg} -function process_fstore(vaddr, value) = - match value { - MemValue(true) => { RETIRE_SUCCESS }, - MemValue(false) => { internal_error("store got false from mem_write_value") }, - MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } - } - /* AST -> Assembly notation ================================ */ mapping clause assembly = STORE_FP(imm, rs2, rs1, width) @@ -184,31 +184,39 @@ union clause ast = F_MADD_TYPE : (regidx, regidx, regidx, rounding_mode, regidx, /* F instructions */ -mapping clause encdec = F_MADD_TYPE(rs3, rs2, rs1, rm, rd, FMADD_S) if is_RV32F_or_RV64F - <-> rs3 @ 0b00 @ rs2 @ rs1 @ rm @ rd @ 0b100_0011 if is_RV32F_or_RV64F +mapping clause encdec = + F_MADD_TYPE(rs3, rs2, rs1, rm, rd, FMADD_S) if is_RV32F_or_RV64F() +<-> rs3 @ 0b00 @ rs2 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b100_0011 if is_RV32F_or_RV64F() -mapping clause encdec = F_MADD_TYPE(rs3, rs2, rs1, rm, rd, FMSUB_S) if is_RV32F_or_RV64F - <-> rs3 @ 0b00 @ rs2 @ rs1 @ rm @ rd @ 0b100_0111 if is_RV32F_or_RV64F +mapping clause encdec = + F_MADD_TYPE(rs3, rs2, rs1, rm, rd, FMSUB_S) if is_RV32F_or_RV64F() +<-> rs3 @ 0b00 @ rs2 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b100_0111 if is_RV32F_or_RV64F() -mapping clause encdec = F_MADD_TYPE(rs3, rs2, rs1, rm, rd, FNMSUB_S) if is_RV32F_or_RV64F - <-> rs3 @ 0b00 @ rs2 @ rs1 @ rm @ rd @ 0b100_1011 if is_RV32F_or_RV64F +mapping clause encdec = + F_MADD_TYPE(rs3, rs2, rs1, rm, rd, FNMSUB_S) if is_RV32F_or_RV64F() +<-> rs3 @ 0b00 @ rs2 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b100_1011 if is_RV32F_or_RV64F() -mapping clause encdec = F_MADD_TYPE(rs3, rs2, rs1, rm, rd, FNMADD_S) if is_RV32F_or_RV64F - <-> rs3 @ 0b00 @ rs2 @ rs1 @ rm @ rd @ 0b100_1111 if is_RV32F_or_RV64F +mapping clause encdec = + F_MADD_TYPE(rs3, rs2, rs1, rm, rd, FNMADD_S) if is_RV32F_or_RV64F() +<-> rs3 @ 0b00 @ rs2 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b100_1111 if is_RV32F_or_RV64F() /* D instructions */ -mapping clause encdec = F_MADD_TYPE(rs3, rs2, rs1, rm, rd, FMADD_D) if is_RV32D_or_RV64D() - <-> rs3 @ 0b01 @ rs2 @ rs1 @ rm @ rd @ 0b100_0011 if is_RV32D_or_RV64D() +mapping clause encdec = + F_MADD_TYPE(rs3, rs2, rs1, rm, rd, FMADD_D) if is_RV32D_or_RV64D() +<-> rs3 @ 0b01 @ rs2 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b100_0011 if is_RV32D_or_RV64D() -mapping clause encdec = F_MADD_TYPE(rs3, rs2, rs1, rm, rd, FMSUB_D) if is_RV32D_or_RV64D() - <-> rs3 @ 0b01 @ rs2 @ rs1 @ rm @ rd @ 0b100_0111 if is_RV32D_or_RV64D() +mapping clause encdec = + F_MADD_TYPE(rs3, rs2, rs1, rm, rd, FMSUB_D) if is_RV32D_or_RV64D() +<-> rs3 @ 0b01 @ rs2 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b100_0111 if is_RV32D_or_RV64D() -mapping clause encdec = F_MADD_TYPE(rs3, rs2, rs1, rm, rd, FNMSUB_D) if is_RV32D_or_RV64D() - <-> rs3 @ 0b01 @ rs2 @ rs1 @ rm @ rd @ 0b100_1011 if is_RV32D_or_RV64D() +mapping clause encdec = + F_MADD_TYPE(rs3, rs2, rs1, rm, rd, FNMSUB_D) if is_RV32D_or_RV64D() +<-> rs3 @ 0b01 @ rs2 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b100_1011 if is_RV32D_or_RV64D() -mapping clause encdec = F_MADD_TYPE(rs3, rs2, rs1, rm, rd, FNMADD_D) if is_RV32D_or_RV64D() - <-> rs3 @ 0b01 @ rs2 @ rs1 @ rm @ rd @ 0b100_1111 if is_RV32D_or_RV64D() +mapping clause encdec = + F_MADD_TYPE(rs3, rs2, rs1, rm, rd, FNMADD_D) if is_RV32D_or_RV64D() +<-> rs3 @ 0b01 @ rs2 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b100_1111 if is_RV32D_or_RV64D() /* Execution semantics ================================ */ @@ -256,45 +264,59 @@ union clause ast = F_BIN_RM_TYPE : (regidx, regidx, rounding_mode, regidx, f_bin /* F instructions */ -mapping clause encdec = F_BIN_RM_TYPE(rs2, rs1, rm, rd, FADD_S) if is_RV32F_or_RV64F - <-> 0b000_0000 @ rs2 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV32F_or_RV64F +mapping clause encdec = + F_BIN_RM_TYPE(rs2, rs1, rm, rd, FADD_S) if is_RV32F_or_RV64F() +<-> 0b000_0000 @ rs2 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F() -mapping clause encdec = F_BIN_RM_TYPE(rs2, rs1, rm, rd, FSUB_S) if is_RV32F_or_RV64F - <-> 0b000_0100 @ rs2 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV32F_or_RV64F +mapping clause encdec = + F_BIN_RM_TYPE(rs2, rs1, rm, rd, FSUB_S) if is_RV32F_or_RV64F() +<-> 0b000_0100 @ rs2 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F() -mapping clause encdec = F_BIN_RM_TYPE(rs2, rs1, rm, rd, FMUL_S) if is_RV32F_or_RV64F - <-> 0b000_1000 @ rs2 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV32F_or_RV64F +mapping clause encdec = + F_BIN_RM_TYPE(rs2, rs1, rm, rd, FMUL_S) if is_RV32F_or_RV64F() +<-> 0b000_1000 @ rs2 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F() -mapping clause encdec = F_BIN_RM_TYPE(rs2, rs1, rm, rd, FDIV_S) if is_RV32F_or_RV64F - <-> 0b000_1100 @ rs2 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV32F_or_RV64F +mapping clause encdec = + F_BIN_RM_TYPE(rs2, rs1, rm, rd, FDIV_S) if is_RV32F_or_RV64F() +<-> 0b000_1100 @ rs2 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F() /* D instructions */ -mapping clause encdec = F_BIN_RM_TYPE(rs2, rs1, rm, rd, FADD_D) if is_RV32D_or_RV64D - <-> 0b000_0001 @ rs2 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV32D_or_RV64D +mapping clause encdec = + F_BIN_RM_TYPE(rs2, rs1, rm, rd, FADD_D) if is_RV32D_or_RV64D() +<-> 0b000_0001 @ rs2 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() -mapping clause encdec = F_BIN_RM_TYPE(rs2, rs1, rm, rd, FSUB_D) if is_RV32D_or_RV64D - <-> 0b000_0101 @ rs2 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV32D_or_RV64D +mapping clause encdec = + F_BIN_RM_TYPE(rs2, rs1, rm, rd, FSUB_D) if is_RV32D_or_RV64D() +<-> 0b000_0101 @ rs2 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() -mapping clause encdec = F_BIN_RM_TYPE(rs2, rs1, rm, rd, FMUL_D) if is_RV32D_or_RV64D - <-> 0b000_1001 @ rs2 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV32D_or_RV64D +mapping clause encdec = + F_BIN_RM_TYPE(rs2, rs1, rm, rd, FMUL_D) if is_RV32D_or_RV64D() +<-> 0b000_1001 @ rs2 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() -mapping clause encdec = F_BIN_RM_TYPE(rs2, rs1, rm, rd, FDIV_D) if is_RV32D_or_RV64D - <-> 0b000_1101 @ rs2 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV32D_or_RV64D +mapping clause encdec = + F_BIN_RM_TYPE(rs2, rs1, rm, rd, FDIV_D) if is_RV32D_or_RV64D() +<-> 0b000_1101 @ rs2 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() /* Execution semantics ================================ */ function clause execute (F_BIN_RM_TYPE(rs2, rs1, rm, rd, op)) = { + /* TODO */ + handle_illegal(); + RETIRE_FAIL + + /* fill in primitive op using soft-float let rs1_val = F(rs1); let rs2_val = F(rs2); let result : xlenbits = match op { - FADD_S => prim_fadd_s (rs1_val, rs2_val) /* TODO: fill in primitive op using soft-float */ - FSUB_S => prim_fsub_s (rs1_val, rs2_val) - FMUL_S => prim_fmul_s (rs1_val, rs2_val) + FADD_S => prim_fadd_s (rs1_val, rs2_val), + FSUB_S => prim_fsub_s (rs1_val, rs2_val), + FMUL_S => prim_fmul_s (rs1_val, rs2_val), FDIV_S => prim_fdiv_s (rs1_val, rs2_val) }; F(rd) = result; RETIRE_SUCCESS + */ } /* AST -> Assembly notation ================================ */ @@ -329,69 +351,87 @@ union clause ast = F_UN_RM_TYPE : (regidx, rounding_mode, regidx, f_un_rm_op) /* F instructions */ -mapping clause encdec = F_UN_RM_TYPE(rs1, rm, rd, FSQRT_S) if is_RV32F_or_RV64F() - <-> 0b010_1100 @ 0b00000 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV32F_or_RV64F() +mapping clause encdec = + F_UN_RM_TYPE(rs1, rm, rd, FSQRT_S) if is_RV32F_or_RV64F() +<-> 0b010_1100 @ 0b00000 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F() -mapping clause encdec = F_UN_RM_TYPE(rs1, rm, rd, FCVT_W_S) if is_RV32F_or_RV64F() - <-> 0b110_0000 @ 0b00000 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV32F_or_RV64F() +mapping clause encdec = + F_UN_RM_TYPE(rs1, rm, rd, FCVT_W_S) if is_RV32F_or_RV64F() +<-> 0b110_0000 @ 0b00000 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F() -mapping clause encdec = F_UN_RM_TYPE(rs1, rm, rd, FCVT_WU_S) if is_RV32F_or_RV64F() - <-> 0b110_0000 @ 0b00001 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV32F_or_RV64F() +mapping clause encdec = + F_UN_RM_TYPE(rs1, rm, rd, FCVT_WU_S) if is_RV32F_or_RV64F() +<-> 0b110_0000 @ 0b00001 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F() -mapping clause encdec = F_UN_RM_TYPE(rs1, rm, rd, FCVT_S_W) if is_RV32F_or_RV64F() - <-> 0b110_1000 @ 0b00000 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV32F_or_RV64F() +mapping clause encdec = + F_UN_RM_TYPE(rs1, rm, rd, FCVT_S_W) if is_RV32F_or_RV64F() +<-> 0b110_1000 @ 0b00000 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F() -mapping clause encdec = F_UN_RM_TYPE(rs1, rm, rd, FCVT_S_WU) if is_RV32F_or_RV64F() - <-> 0b110_1000 @ 0b00001 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV32F_or_RV64F() +mapping clause encdec = + F_UN_RM_TYPE(rs1, rm, rd, FCVT_S_WU) if is_RV32F_or_RV64F() +<-> 0b110_1000 @ 0b00001 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV32F_or_RV64F() /* D instructions */ -mapping clause encdec = F_UN_RM_TYPE(rs1, rm, rd, FSQRT_D) if is_RV32D_or_RV64D() - <-> 0b010_1101 @ 0b00000 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV32D_or_RV64D() +mapping clause encdec = + F_UN_RM_TYPE(rs1, rm, rd, FSQRT_D) if is_RV32D_or_RV64D() +<-> 0b010_1101 @ 0b00000 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() -mapping clause encdec = F_UN_RM_TYPE(rs1, rm, rd, FCVT_W_D) if is_RV32D_or_RV64D() - <-> 0b110_0001 @ 0b00000 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV32D_or_RV64D() +mapping clause encdec = + F_UN_RM_TYPE(rs1, rm, rd, FCVT_W_D) if is_RV32D_or_RV64D() +<-> 0b110_0001 @ 0b00000 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() -mapping clause encdec = F_UN_RM_TYPE(rs1, rm, rd, FCVT_WU_D) if is_RV32D_or_RV64D() - <-> 0b110_0001 @ 0b00001 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV32D_or_RV64D() +mapping clause encdec = + F_UN_RM_TYPE(rs1, rm, rd, FCVT_WU_D) if is_RV32D_or_RV64D() +<-> 0b110_0001 @ 0b00001 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() -mapping clause encdec = F_UN_RM_TYPE(rs1, rm, rd, FCVT_D_W) if is_RV32D_or_RV64D() - <-> 0b110_1001 @ 0b00000 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV32D_or_RV64D() +mapping clause encdec = + F_UN_RM_TYPE(rs1, rm, rd, FCVT_D_W) if is_RV32D_or_RV64D() +<-> 0b110_1001 @ 0b00000 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() -mapping clause encdec = F_UN_RM_TYPE(rs1, rm, rd, FCVT_D_WU) if is_RV32D_or_RV64D() - <-> 0b110_1001 @ 0b00001 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV32D_or_RV64D() +mapping clause encdec = + F_UN_RM_TYPE(rs1, rm, rd, FCVT_D_WU) if is_RV32D_or_RV64D() +<-> 0b110_1001 @ 0b00001 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV32D_or_RV64D() /* F instructions, RV64 only */ -mapping clause encdec = F_UN_RM_TYPE(rs1, rm, rd, FCVT_L_S) if is_RV64F() - <-> 0b110_0000 @ 0b00010 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV64F() +mapping clause encdec = + F_UN_RM_TYPE(rs1, rm, rd, FCVT_L_S) if is_RV64F() +<-> 0b110_0000 @ 0b00010 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV64F() -mapping clause encdec = F_UN_RM_TYPE(rs1, rm, rd, FCVT_LU_S) if is_RV64F() - <-> 0b110_0000 @ 0b00011 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV64F() +mapping clause encdec = + F_UN_RM_TYPE(rs1, rm, rd, FCVT_LU_S) if is_RV64F() +<-> 0b110_0000 @ 0b00011 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV64F() -mapping clause encdec = F_UN_RM_TYPE(rs1, rm, rd, FCVT_S_L) if is_RV64F() - <-> 0b110_1000 @ 0b00010 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV64F() +mapping clause encdec = + F_UN_RM_TYPE(rs1, rm, rd, FCVT_S_L) if is_RV64F() +<-> 0b110_1000 @ 0b00010 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV64F() -mapping clause encdec = F_UN_RM_TYPE(rs1, rm, rd, FCVT_S_LU) if is_RV64F() - <-> 0b110_1000 @ 0b00011 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV64F() +mapping clause encdec = + F_UN_RM_TYPE(rs1, rm, rd, FCVT_S_LU) if is_RV64F() +<-> 0b110_1000 @ 0b00011 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV64F() /* D instructions, RV64 only */ -mapping clause encdec = F_UN_RM_TYPE(rs1, rm, rd, FCVT_L_D) if is_RV64D() - <-> 0b110_0001 @ 0b00010 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV64D() +mapping clause encdec = + F_UN_RM_TYPE(rs1, rm, rd, FCVT_L_D) if is_RV64D() +<-> 0b110_0001 @ 0b00010 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV64D() -mapping clause encdec = F_UN_RM_TYPE(rs1, rm, rd, FCVT_LU_D) if is_RV64D() - <-> 0b110_0001 @ 0b00011 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV64D() +mapping clause encdec = + F_UN_RM_TYPE(rs1, rm, rd, FCVT_LU_D) if is_RV64D() +<-> 0b110_0001 @ 0b00011 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV64D() -mapping clause encdec = F_UN_RM_TYPE(rs1, rm, rd, FCVT_D_L) if is_RV64D() - <-> 0b110_1001 @ 0b00010 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV64D() +mapping clause encdec = + F_UN_RM_TYPE(rs1, rm, rd, FCVT_D_L) if is_RV64D() +<-> 0b110_1001 @ 0b00010 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV64D() -mapping clause encdec = F_UN_RM_TYPE(rs1, rm, rd, FCVT_D_LU) if is_RV64D() - <-> 0b110_1001 @ 0b00011 @ rs1 @ rm @ rd @ 0b101_0011 if is_RV64D() +mapping clause encdec = + F_UN_RM_TYPE(rs1, rm, rd, FCVT_D_LU) if is_RV64D() +<-> 0b110_1001 @ 0b00011 @ rs1 @ rounding_mode_bits (rm) @ rd @ 0b101_0011 if is_RV64D() /* Execution semantics ================================ */ -function clause execute (F_UN_RM_TYPE(rs1, rm, rd, op) = { +function clause execute (F_UN_RM_TYPE(rs1, rm, rd, op)) = { /* TODO */ handle_illegal(); RETIRE_FAIL @@ -497,7 +537,7 @@ mapping clause encdec = F_BIN_TYPE(rs2, rs1, rd, FLE_D) if is_ /* Execution semantics ================================ */ -function clause execute (F_BIN_TYPE(rs2, rs1, rd, op) = { +function clause execute (F_BIN_TYPE(rs2, rs1, rd, op)) = { /* TODO */ handle_illegal(); RETIRE_FAIL @@ -542,26 +582,26 @@ union clause ast = F_UN_TYPE : ( regidx, regidx, f_un_ /* F instructions, RV32 and RV64 */ -mapping clause encdec = F_UN_TYPE(rs1, rm, rd, FMV_X_W) if haveFExt() & sizeof(xlen)=32 - <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveFExt() & sizeof(xlen)=32 +mapping clause encdec = F_UN_TYPE(rs1, rd, FMV_X_W) if haveFExt() & sizeof(xlen) == 32 + <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveFExt() & sizeof(xlen) == 32 -mapping clause encdec = F_UN_TYPE(rs1, rm, rd, FCLASS_S) if haveFExt() & sizeof(xlen)=32 - <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveFExt() & sizeof(xlen)=32 +mapping clause encdec = F_UN_TYPE(rs1, rd, FCLASS_S) if haveFExt() & sizeof(xlen) == 32 + <-> 0b111_0000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveFExt() & sizeof(xlen) == 32 -mapping clause encdec = F_UN_TYPE(rs1, rm, rd, FMV_W_X) if haveFExt() & sizeof(xlen)=32 - <-> 0b111_1000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveFExt() & sizeof(xlen)=32 +mapping clause encdec = F_UN_TYPE(rs1, rd, FMV_W_X) if haveFExt() & sizeof(xlen) == 32 + <-> 0b111_1000 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveFExt() & sizeof(xlen) == 32 /* D instructions, RV64 only */ -mapping clause encdec = F_UN_TYPE(rs1, rm, rd, FMV_X_D) if is_RV64D() +mapping clause encdec = F_UN_TYPE(rs1, rd, FMV_X_D) if is_RV64D() <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV64D() -mapping clause encdec = F_UN_TYPE(rs1, rm, rd, FMV_D_X) if is_RV64D() +mapping clause encdec = F_UN_TYPE(rs1, rd, FMV_D_X) if is_RV64D() <-> 0b111_1001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if is_RV64D() /* Execution semantics ================================ */ -function clause execute (F_UN_TYPE(rs1, rd, op) = { +function clause execute (F_UN_TYPE(rs1, rd, op)) = { /* TODO */ handle_illegal(); RETIRE_FAIL @@ -578,7 +618,7 @@ mapping f_un_type_mnemonic : f_un_op <-> string = { FMV_D_X <-> "fmv.d.x" } -mapping clause assembly = F_UN_TYPE(rs1, rd, op +mapping clause assembly = F_UN_TYPE(rs1, rd, op) <-> f_un_type_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) |