diff options
Diffstat (limited to 'risc-v')
| -rw-r--r-- | risc-v/hgen/herdtools_ast_to_shallow_ast.hgen | 4 | ||||
| -rw-r--r-- | risc-v/hgen/shallow_ast_to_herdtools_ast.hgen | 4 | ||||
| -rw-r--r-- | risc-v/riscv.sail | 12 | ||||
| -rw-r--r-- | risc-v/riscv_regfp.sail | 4 |
4 files changed, 12 insertions, 12 deletions
diff --git a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen index e66608e6..07c1d082 100644 --- a/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen +++ b/risc-v/hgen/herdtools_ast_to_shallow_ast.hgen @@ -3,10 +3,10 @@ translate_imm20 "imm" imm, translate_reg "rd" rd, translate_uop op) -| `RISCVJAL(imm, rd) -> JAL0( +| `RISCVJAL(imm, rd) -> RISCV_JAL( translate_imm21 "imm" imm, translate_reg "rd" rd) -| `RISCVJALR(imm, rs, rd) -> JALR0( +| `RISCVJALR(imm, rs, rd) -> RISCV_JALR( translate_imm12 "imm" imm, translate_reg "rs" rd, translate_reg "rd" rd) diff --git a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen index 23bcc4cb..3025992e 100644 --- a/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen +++ b/risc-v/hgen/shallow_ast_to_herdtools_ast.hgen @@ -1,7 +1,7 @@ | EBREAK -> `RISCVStopFetching | UTYPE( imm, rd, op) -> `RISCVUTYPE(translate_out_simm20 imm, translate_out_ireg rd, translate_out_uop op) -| JAL0( imm, rd) -> `RISCVJAL(translate_out_simm21 imm, translate_out_ireg rd) -| JALR0( imm, rs, rd) -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) +| RISCV_JAL( imm, rd) -> `RISCVJAL(translate_out_simm21 imm, translate_out_ireg rd) +| RISCV_JALR( imm, rs, rd) -> `RISCVJALR(translate_out_simm12 imm, translate_out_ireg rs, translate_out_ireg rd) | BTYPE( imm, rs2, rs1, op) -> `RISCVBType(translate_out_simm13 imm, translate_out_ireg rs2, translate_out_ireg rs1, translate_out_bop op) | ITYPE( imm, rs1, rd, op) -> `RISCVIType(translate_out_simm12 imm, translate_out_ireg rs1, translate_out_ireg rd, translate_out_iop op) | SHIFTIOP( imm, rs, rd, op) -> `RISCVShiftIop(translate_out_imm6 imm, translate_out_ireg rs, translate_out_ireg rd, translate_out_sop op) diff --git a/risc-v/riscv.sail b/risc-v/riscv.sail index 3a54e0c8..3d52d111 100644 --- a/risc-v/riscv.sail +++ b/risc-v/riscv.sail @@ -20,11 +20,11 @@ function clause execute (UTYPE(imm, rd, op)) = wGPR(rd, ret) (********************************************************************) -union ast member ((bit[21]), regno) JAL +union ast member ((bit[21]), regno) RISCV_JAL -function clause decode ((bit[20]) imm : (regno) rd : 0b1101111) = Some (JAL(imm[19] : imm[7..0] : imm[8] : imm[18..13] : imm[12..9] : 0b0, rd)) +function clause decode ((bit[20]) imm : (regno) rd : 0b1101111) = Some (RISCV_JAL(imm[19] : imm[7..0] : imm[8] : imm[18..13] : imm[12..9] : 0b0, rd)) -function clause execute (JAL(imm, rd)) = { +function clause execute (RISCV_JAL(imm, rd)) = { (bit[64]) pc := PC; wGPR(rd, pc + 4); (bit[64]) offset := EXTS(imm); @@ -32,12 +32,12 @@ function clause execute (JAL(imm, rd)) = { } (********************************************************************) -union ast member((bit[12]), regno, regno) JALR +union ast member((bit[12]), regno, regno) RISCV_JALR function clause decode ((bit[12]) imm : (regno) rs1 : 0b000 : (regno) rd : 0b1100111) = - Some(JALR(imm, rs1, rd)) + Some(RISCV_JALR(imm, rs1, rd)) -function clause execute (JALR(imm, rs1, rd)) = { +function clause execute (RISCV_JALR(imm, rs1, rd)) = { (* write rd before anything else to prevent unintended strength *) wGPR(rd, PC + 4); (bit[64]) newPC := rGPR(rs1) + EXTS(imm); diff --git a/risc-v/riscv_regfp.sail b/risc-v/riscv_regfp.sail index ad341c60..dee9cc8e 100644 --- a/risc-v/riscv_regfp.sail +++ b/risc-v/riscv_regfp.sail @@ -20,12 +20,12 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( case (UTYPE ( imm, rd, op)) -> { if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; } - case (JAL ( imm, rd)) -> { + case (RISCV_JAL ( imm, rd)) -> { if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; let (bit[64]) offset = EXTS(imm) in Nias := [|| NIAFP_concrete_address (PC + offset) ||] } - case (JALR ( imm, rs, rd)) -> { + case (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; let (bit[64]) offset = EXTS(imm) in |