Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 5 additions & 3 deletions sail-impl/inst/32/rv_c/c_addi4spn
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
let imm : bits(12) = (0b00 @ nzimm @ 0b00);
let rd = creg2reg_idx(rdc);
X(rd) = X(sp) + imm;
let imm : bits(12) = (0b00 @ c_nzuimm10 @ 0b00);
let rd = creg2reg_idx(rd_p);
// 0b00010 represents sp
let sp_val = read_GPR(0b00010);
write_GPR(rd, sp_val + sign_extend(imm));
4 changes: 4 additions & 0 deletions sail-impl/inst/64/rv_c/c_add
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
let rd_val = read_GPR(rd_rs1_n0);
let rs2_val = read_GPR(c_rs2_n0);
write_GPR(rd_rs1_n0, rd_val + rs2_val);
nextPC = PC + 4;
4 changes: 4 additions & 0 deletions sail-impl/inst/64/rv_c/c_addi
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
let imm : bits(12) = sign_extend(c_nzimm6);
let rsd_val = read_GPR(rd_rs1_n0);
write_GPR(rd_rs1_n0, rsd_val + sign_extend(imm));
nextPC = PC + 4;
5 changes: 5 additions & 0 deletions sail-impl/inst/64/rv_c/c_addi16sp
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
let imm : bits(12) = sign_extend(c_nzimm10lo @ 0x0);
// 0b00010 represents sp
let sp_val = read_GPR(0b00010);
write_GPR(0b00010, sp_val + sign_extend(imm));
nextPC = PC + 4;
9 changes: 6 additions & 3 deletions sail-impl/inst/64/rv_c/c_addi4spn
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
let imm : bits(12) = (0b00 @ nzimm @ 0b00);
let rd = creg2reg_idx(rdc);
X(rd) = X(sp) + imm;
let imm : bits(12) = (0b00 @ c_nzuimm10 @ 0b00);
let rd = creg2reg_idx(rd_p);
// 0b00010 represents sp
let sp_val = read_GPR(0b00010);
write_GPR(rd, sp_val + sign_extend(imm));
nextPC = PC + 4;
6 changes: 6 additions & 0 deletions sail-impl/inst/64/rv_c/c_addiw
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
let imm : bits(6) = c_nzuimm10;
let rd = creg2reg_idx(rd_p);
// 0b00010 represents sp
let sp_val = read_GPR(0b00010);
write_GPR(rd, sp_val + sign_extend(imm));
nextPC = PC + 4;
6 changes: 6 additions & 0 deletions sail-impl/inst/64/rv_c/c_addw
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
let rsd = creg2reg_idx(rsd);
let rs2 = creg2reg_idx(rs2);
let rsd_val = read_GPR(rsd)[31..0];
let rs2_val = read_GPR(rs2)[31..0];
write_GPR(rsd, rs2_val + rsd_val);
nextPC = PC + 4;
6 changes: 6 additions & 0 deletions sail-impl/inst/64/rv_c/c_and
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
let rsd = creg2reg_idx(rd_rs1_p);
let rs2 = creg2reg_idx(rs2_p);
let rsd_val = read_GPR(rsd);
let rs2_val = read_GPR(rs2);
write_GPR(rsd, rs2_val & rsd_val);
nextPC = PC + 4;
3 changes: 3 additions & 0 deletions sail-impl/inst/64/rv_c/c_andi
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
let rsd = creg2reg_idx(rd_rs1_p);
write_GPR(rsd, read_GPR(rsd) & sign_extend(c_imm6lo));
nextPC = PC + 4;
7 changes: 7 additions & 0 deletions sail-impl/inst/64/rv_c/c_beqz
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
let rs = creg2reg_idx(rs1_p);
let rs_val = read_GPR(rs);
let taken : bool = rs_val == zero_extend(0b00);
if taken then {
let t : XLENBITS = PC + sign_extend(c_bimm9lo @ 0b0);
nextPC = t;
}
7 changes: 7 additions & 0 deletions sail-impl/inst/64/rv_c/c_bnez
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
let rs = creg2reg_idx(rs1_p);
let rs_val = read_GPR(rs);
let taken : bool = rs_val != zero_extend(0b00);
if taken then {
let t : XLENBITS = PC + sign_extend(c_bimm9lo @ 0b0);
nextPC = t;
}
58 changes: 58 additions & 0 deletions sail-impl/inst/64/rv_c/c_ebreak
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
// deal with delegation
let idx = num_of_ExceptionType(E_Breakpoint());
let super = bit_to_bool(medeleg.bits[idx]);
let deleg = if extensionEnabled(Ext_S) & super then Supervisor else Machine;

let del_priv = if privLevel_to_bits(deleg) <_u privLevel_to_bits(cur_privilege) then cur_privilege else deleg;

match (del_priv) {
Machine => {
mcause[IsInterrupt] = 0b0;
mcause[Cause] = zero_extend(exceptionType_to_bits(E_Breakpoint()));

mstatus[MPIE] = mstatus[MIE];
mstatus[MIE] = 0b0;
mstatus[MPP] = privLevel_to_bits(cur_privilege);
mtval.bits = PC;
mepc.bits = PC;

cur_privilege = del_priv;

let base : XLENBITS = mtvec[Base] @ 0b00;
nextPC = match (trapVectorMode_of_bits(mtvec[Mode])) {
TV_Direct => base,
TV_Vector => if mcause[IsInterrupt] == 0b1
then (base + (zero_extend(mcause[Cause] << 2)))
else base,
TV_Reserved => internal_error("Invalid mtvec mode")
}
},
Supervisor => {
assert(extensionEnabled(Ext_S), "no supervisor mode present for delegation");

scause[IsInterrupt] = 0b0;
scause[Cause] = zero_extend(exceptionType_to_bits(E_Breakpoint()));

mstatus[SPIE] = mstatus[SIE];
mstatus[SIE] = 0b0;
mstatus[SPP] = match cur_privilege {
User => 0b0,
Supervisor => 0b1,
Machine => internal_error("Invalid privilege for s-mode trap")
};
stval.bits = PC;
sepc.bits = PC;

cur_privilege = del_priv;

let base : XLENBITS = stvec[Base] @ 0b00;
nextPC = match (trapVectorMode_of_bits(stvec[Mode])) {
TV_Direct => base,
TV_Vector => if scause[IsInterrupt] == 0b1
then (base + (zero_extend(scause[Cause] << 2)))
else base,
TV_Reserved => internal_error("Invalid stvec mode")
}
},
User => internal_error("Invalid privilege level")
}
3 changes: 3 additions & 0 deletions sail-impl/inst/64/rv_c/c_j
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
write_GPR(0b00000, nextPC);
let newPC : XLENBITS = sign_extend(c_imm12);
nextPC = [newPC with 0 = bitzero];
4 changes: 4 additions & 0 deletions sail-impl/inst/64/rv_c/c_jalr
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
let ra_val = read_GPR(0b00001);
write_GPR(0b00000, ra_val);
let newPC : XLENBITS = read_GPR(c_rs1_n0);
nextPC = [newPC with 0 = bitzero];
3 changes: 3 additions & 0 deletions sail-impl/inst/64/rv_c/c_jr
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
write_GPR(0b00000, nextPC);
let newPC : XLENBITS = read_GPR(rs1_n0);
nextPC = [newPC with 0 = bitzero];
5 changes: 5 additions & 0 deletions sail-impl/inst/64/rv_c/c_ld
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
let imm : bits(12) = zero_extend(uimm @ 0b000);
let rd = creg2reg_idx(rdc);
let rs = creg2reg_idx(rsc);
write_GPR(rd, readmem(read_GPR(rs) + sign_extend(imm), satp.bits)[15..0]);
nextPC = PC + 4;
5 changes: 5 additions & 0 deletions sail-impl/inst/64/rv_c/c_ldsp
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
let imm : bits(12) = zero_extend(uimm @ 0b000);
let rd = creg2reg_idx(rdc);
// 0b00010 represents sp
write_GPR(rd, readmem(read_GPR(0b00010) + sign_extend(imm), satp.bits)[15..0]);
nextPC = PC + 4;
2 changes: 2 additions & 0 deletions sail-impl/inst/64/rv_c/c_li
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
write_GPR(rd_n0, sign_extend(c_imm6lo));
nextPC = PC + 4;
3 changes: 3 additions & 0 deletions sail-impl/inst/64/rv_c/c_lui
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
let off : XLENBITS = sign_extend(c_nzimm18lo @ 0x000);
write_GPR(rd_n2, off);
nextPC = PC + 4;
5 changes: 5 additions & 0 deletions sail-impl/inst/64/rv_c/c_lw
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
let imm : bits(12) = zero_extend(c_uimm7lo @ 0b00);
let rs = creg2reg_idx(rs1_p);
let rd = creg2reg_idx(rd_p);
write_GPR(rd, sign_extend(readmem(read_GPR(rs) + sign_extend(imm), satp.bits)[31..0]));
nextPC = PC + 4;
4 changes: 4 additions & 0 deletions sail-impl/inst/64/rv_c/c_lwsp
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
let imm : bits(12) = zero_extend(c_uimm8splo @ 0b000);
// 0b00010 represents sp
write_GPR(rd_n0, sign_extend(readmem(read_GPR(0b00010) + sign_extend(imm), satp.bits)[31..0]));
nextPC = PC + 4;
3 changes: 3 additions & 0 deletions sail-impl/inst/64/rv_c/c_mv
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
let rs2_val = read_GPR(c_rs2_n0);
write_GPR(rd_n0, rs2_val);
nextPC = PC + 4;
1 change: 1 addition & 0 deletions sail-impl/inst/64/rv_c/c_nop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
nextPC = PC + 4;
6 changes: 6 additions & 0 deletions sail-impl/inst/64/rv_c/c_or
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
let rsd = creg2reg_idx(rd_rs1_p);
let rs2 = creg2reg_idx(rs2_p);
let rsd_val = read_GPR(rsd);
let rs2_val = read_GPR(rs2);
write_GPR(rsd, rs2_val | rsd_val);
nextPC = PC + 4;
4 changes: 4 additions & 0 deletions sail-impl/inst/64/rv_c/c_sd
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
let imm : bits(12) = zero_extend(uimm @ 0b000);
let rs1 = creg2reg_idx(rsc1);
let rs2 = creg2reg_idx(rsc2);
writemem(read_GPR(rs1) + sign_extend(imm), read_GPR(rs2), satp.bits);
3 changes: 3 additions & 0 deletions sail-impl/inst/64/rv_c/c_sdsp
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
let imm : bits(12) = zero_extend(uimm @ 0b000);
let sp = creg2reg_idx(rsc2);
writemem(read_GPR(sp) + sign_extend(imm), read_GPR(rs2), satp.bits);
2 changes: 2 additions & 0 deletions sail-impl/inst/64/rv_c/c_slli
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
write_GPR(rd, read_GPR(rd) << uimm);
nextPC = PC + 4;
2 changes: 2 additions & 0 deletions sail-impl/inst/64/rv_c/c_srai
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
write_GPR(rd, shift_bits_right_arith(X(rs1), shamt));
nextPC = PC + 4;
2 changes: 2 additions & 0 deletions sail-impl/inst/64/rv_c/c_srli
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
write_GPR(rd, read_GPR(rd) >> uimm);
nextPC = PC + 4;
6 changes: 6 additions & 0 deletions sail-impl/inst/64/rv_c/c_sub
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
let rsd = creg2reg_idx(rd_rs1_p);
let rs2 = creg2reg_idx(rs2_p);
let rsd_val = read_GPR(rsd);
let rs2_val = read_GPR(rs2);
write_GPR(rsd, rs2_val - rsd_val);
nextPC = PC + 4;
6 changes: 6 additions & 0 deletions sail-impl/inst/64/rv_c/c_subw
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
let rsd = creg2reg_idx(rsd);
let rs2 = creg2reg_idx(rs2);
let rsd_val = read_GPR(rsd)[31..0];
let rs2_val = read_GPR(rs2)[31..0];
write_GPR(rsd, sign_extend(rs2_val - rsd_val));
nextPC = PC + 4;
4 changes: 4 additions & 0 deletions sail-impl/inst/64/rv_c/c_sw
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
let imm : bits(12) = zero_extend(c_uimm7lo @ 0b000);
let rs1 = creg2reg_idx(rs1_p);
let rs2 = creg2reg_idx(rs2_p);
writemem(read_GPR(rs1) + sign_extend(imm), read_GPR(rs2), zero_extend(0b10), satp.bits);
6 changes: 6 additions & 0 deletions sail-impl/inst/64/rv_c/c_xor
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
let rd = creg2reg_idx(rd_rs1_p);
let rs2 = creg2reg_idx(rs2_p);
let rd_val = read_GPR(rd);
let rs2_val = read_GPR(rs2);
write_GPR(rd, rd_val ^ rs2_val);
nextPC = PC + 4;
2 changes: 1 addition & 1 deletion sail-impl/sail-impl-meta.json
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
{
"march": "rv64i"
"march": "rv64ic"
}
64 changes: 52 additions & 12 deletions sailcodegen/src/SailCodeGen.scala
Original file line number Diff line number Diff line change
Expand Up @@ -156,7 +156,16 @@ class SailCodeGenerator(params: SailCodeGeneratorParams) {
case "jimm20lo" => s"bits(20)"
case "imm20lo" => s"bits(20)"
case "imm12lo" => s"bits(12)"
case "c_nzimm6lo" => s"bits(7)"
case "c_nzimm6lo" => s"bits(6)"
case "c_imm6lo" => s"bits(6)"
case "c_uimm7lo" => s"bits(5)"
case "c_nzimm18lo"=> s"bits(6)"
case "c_bimm9lo" => s"bits(8)"
case "c_uimm8splo"=> s"bits(6)"
case "c_nzimm10lo"=> s"bits(6)"
case "c_uimm8lo" => s"bits(5)"
case "c_nzuimm6lo"=> s"bits(6)"
case "c_uimm9splo"=> s"bits(6)"
case _ => s"bits(${arg.lsb - arg.msb + 1})"
}
} else {
Expand All @@ -180,12 +189,33 @@ class SailCodeGenerator(params: SailCodeGeneratorParams) {
val argBits = arg.lsb - arg.msb + 1
val newAcc = acc :+
(arg.name match {
case "bimm12hi" => "imm7_6 : bits(1) @ imm7_5_0 : bits(6)"
case "bimm12lo" => "imm5_4_1 : bits(4) @ imm5_0 : bits(1)"
case "jimm20" =>
case "bimm12hi" => "imm7_6 : bits(1) @ imm7_5_0 : bits(6)"
case "bimm12lo" => "imm5_4_1 : bits(4) @ imm5_0 : bits(1)"
case "jimm20" =>
"imm_19 : bits(1) @ imm_18_13 : bits(6) @ imm_12_9 : bits(4) @ imm_8 : bits(1) @ imm_7_0 : bits(8)"
case "imm12lo" => "imm12lo : bits(5)"
case "imm12hi" => "imm12hi : bits(7)"
case "imm12lo" => "imm12lo : bits(5)"
case "imm12hi" => "imm12hi : bits(7)"
case "c_nzimm6hi" => "nzi5 : bits(1)"
case "c_nzimm6lo" => "nzi40 : bits(5)"
case "c_nzuimm10" => "nz54 : bits(2) @ nz96 : bits(4) @ nz2 : bits(1) @ nz3 : bits(1)"
case "c_imm6hi" => "c_imm6hi : bits(1)"
case "c_imm6lo" => "c_imm6lo : bits(5)"
case "c_nzimm18hi" => "c_nzimm18hi : bits(1)"
case "c_nzimm18lo" => "c_nzimm18lo : bits(5)"
case "c_bimm9hi" => "i8 : bits(1) @ i43 : bits(2)"
case "c_bimm9lo" => "i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1)"
case "c_uimm8sphi" => "ui5 : bits(1)"
case "c_uimm8splo" => "ui42 : bits(3) @ ui76 : bits(2)"
case "c_nzimm10hi" => "nzi9 : bits(1)"
case "c_nzimm10lo" => "nzi4 : bits(1) @ nzi6 : bits(1) @ nzi87 : bits(2) @ nzi5 : bits(1)"
case "c_uimm7hi" => "ui53 : bits(3)"
case "c_uimm7lo" => "ui2 : bits(1) @ ui6 : bits(1)"
case "c_nzuimm6hi" => "nzui5 : bits(1)"
case "c_nzuimm6lo" => "nzui40 : bits(5)"
case "c_uimm9sphi" => "ui5 : bits(1)"
case "c_uimm9splo" => "ui43 : bits(2) @ ui86 : bits(3)"
case "c_uimm8hi" => "ui53 : bits(3)"
case "c_uimm8lo" => "ui76 : bits(2)"
case _ => arg.name
})

Expand Down Expand Up @@ -221,7 +251,17 @@ class SailCodeGenerator(params: SailCodeGeneratorParams) {
case "bimm12lo" => "imm7_6 @ imm5_0 @ imm7_5_0 @ imm5_4_1"
case "jimm20" => "imm_19 @ imm_7_0 @ imm_8 @ imm_18_13 @ imm_12_9"
case "imm12lo" => "imm12hi @ imm12lo"
case "c_nzimm6lo" => "nz96 @ nz54 @ nz3 @ nz2"
case "c_nzimm6lo" => "nzi5 @ nzi40"
case "c_nzuimm10" => "nz96 @ nz54 @ nz3 @ nz2"
case "c_imm6lo" => "c_imm6hi @ c_imm6lo"
case "c_nzimm18lo"=> "c_nzimm18hi @ c_nzimm18lo"
case "c_bimm9lo" => "i8 @ i76 @ i5 @ i43 @ i21"
case "c_uimm8splo"=> "ui76 @ ui5 @ ui42"
case "c_nzimm10lo"=> "nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4"
case "c_uimm7lo" => "ui6 @ ui53 @ ui2"
case "c_nzuimm6lo"=> "nzui5 @ nzui40"
case "c_uimm9splo"=> "ui86 @ ui5 @ ui43"
case "c_uimm8lo" => "ui76 @ ui53"
case _ => arg.toString
}
})
Expand All @@ -236,7 +276,6 @@ class SailCodeGenerator(params: SailCodeGeneratorParams) {
case "bimm12lo" => "imm7_6 @ imm5_0 @ imm7_5_0 @ imm5_4_1"
case "jimm20" => "imm_19 @ imm_7_0 @ imm_8 @ imm_18_13 @ imm_12_9"
case "imm12lo" => "imm12hi @ imm12lo"
case "c_nzimm6lo" => "nz96 @ nz54 @ nz3 @ nz2"
case _ => arg.toString
}
})
Expand All @@ -257,10 +296,11 @@ class SailCodeGenerator(params: SailCodeGeneratorParams) {
.filter(arg => !arg.toString.contains("hi"))
.map(arg => {
arg.name match {
case "bimm12lo" => arg.toString.stripSuffix("lo")
case "jimm20lo" => arg.toString.stripSuffix("lo")
case "imm12lo" => arg.toString.stripSuffix("lo")
case _ => arg.toString
case "bimm12lo" => arg.toString.stripSuffix("lo")
case "jimm20lo" => arg.toString.stripSuffix("lo")
case "imm12lo" => arg.toString.stripSuffix("lo")
case "c_nzimm6lo" => arg.toString.stripSuffix("lo")
case _ => arg.toString
}
})
.mkString(", ") + ")) = {" + os.read(path).split('\n').map(line => "\n\t" + line).mkString + "\n" + "}"
Expand Down
Empty file added z3_problems
Empty file.