Skip to content

Instantly share code, notes, and snippets.

@WildCryptoFox
Last active August 27, 2022 20:00
Show Gist options
  • Save WildCryptoFox/4d56511885f5b44514b0fcf006a5546a to your computer and use it in GitHub Desktop.
Save WildCryptoFox/4d56511885f5b44514b0fcf006a5546a to your computer and use it in GitHub Desktop.
import logic.basic
structure misa := (extensions : list (string × list nat))
namespace misa
private def gc : list (string × list nat) :=
[⟨"M", [2]⟩, ⟨"A", [2, 1]⟩, ⟨"F", [2, 2]⟩, ⟨"D", [2, 2]⟩, ⟨"C", [2]⟩,
⟨"Zicsr", [2]⟩, ⟨"Zifencei", [2]⟩]
def rv32gc : misa := ⟨⟨"32I", [2, 1]⟩ :: gc⟩
def rv64gc : misa := ⟨⟨"64I", [2, 1]⟩ :: gc⟩
def rv64gqcv : misa := ⟨⟨"Q", [2, 2]⟩ :: ⟨"V", [0, 7]⟩ :: rv64gc.extensions⟩
def xlen : misa → ℕ | ⟨e⟩ :=
if "64I" ∈ e.map prod.fst then 64 else 32
def flen : misa → ℕ | ⟨e⟩ :=
if "D" ∈ e.map prod.fst then 64
else if "F" ∈ e.map prod.fst then 32
else 0
def ilen := 32
def ialign : misa → ℕ | ⟨e⟩ :=
if "C" ∈ e.map prod.fst then 16 else 32
end misa
-- @[pattern] def n := v
meta def mk_pat (n : name) (v : expr) :=
tactic.infer_type v >>= λ t,
tactic.add_decl (declaration.defn n [] t v reducibility_hints.abbrev tt)
>> tactic.set_basic_attribute `pattern n
run_cmd [
[`load, `load_fp, `custom_0, `misc_mem, `op_imm, `auipc, `op_imm_32],
[`store, `store_fp, `custom_1, `amo, `op, `lui, `op_32 ],
[`madd, `msub, `nmsub, `nmadd, `op_fp, `reserved_0, `custom_2 ],
[`branch, `jalr, `reserved, `jal, `system, `reserved_1, `custom_3 ]
].enum.mmap' $ λ ⟨row, ns⟩, ns.enum.mmap' $ λ ⟨col, n⟩,
let opc := 3 + col.shiftl 2 + row.shiftl 5 in
mk_pat (`opcode ++ n) `(fin.of_nat opc : fin 128)
run_cmd [
(0xC00, [`cycle, `time, `instret]),
(0xC80, [`cycleh, `timeh, `instreth]),
(0x001, [`fflags, `frm, `fcsr])
].mmap' $ λ ⟨base, ns⟩, ns.enum.mmap' $ λ ⟨offset, n⟩,
mk_pat (`csr ++ n) (reflect $ base + offset)
structure regnum :=
(num : ℕ)
instance : has_zero regnum := ⟨⟨0⟩⟩
@[derive decidable_eq]
inductive reg_type | integer | float
open reg_type
structure reg (rtype : reg_type) :=
(register : regnum)
instance (rtype) : has_coe (reg rtype) regnum := ⟨reg.register⟩
inductive fmt : Type
| R (opcode7 : fin 128) (funct3 : fin 8) (rd rs1 rs2 : regnum) (funct7 : fin 128)
| R4 (opcode7 : fin 128) (funct3 : fin 8) (rd rs1 rs2 rs3 : regnum) (funct2 : fin 4)
-- 12-bit signed immediate
| I (opcode7 : fin 128) (funct3 : fin 8) (rd rs1 : regnum) (imm : ℤ)
-- 12-bit signed immediate
| S (opcode7 : fin 128) (funct3 : fin 8) ( rs1 rs2 : regnum) (imm : ℤ)
-- high 12 of 13-bit signed immediate
| B (opcode7 : fin 128) (funct3 : fin 8) ( rs1 rs2 : regnum) (imm : ℤ)
-- high 20 of 32-bit signed immediate
| U (opcode7 : fin 128) (rd : regnum) (imm : ℤ)
-- high 20 of 33-bit signed immediate
| J (opcode7 : fin 128) (rd : regnum) (imm : ℤ)
namespace fmt
private def regs (rd rs1 rs2 rs3 : regnum := 0) :=
(rd.num.land 31).shiftl 7 + (rs1.num.land 31).shiftl 15
+ (rs2.num.land 31).shiftl 20 + (rs3.num.land 31).shiftl 27
private def bits (a : ℤ) (b c) :=
(a.to_nat.shiftr c).land (2^(b - c) - 1)
-- encoding truncates out-of-range registers and immediates
-- fixme: immediates should be encoded in 2's complement
def encode : fmt → ℕ
| (R opcode7 funct3 rd rs1 rs2 funct7) :=
opcode7.val + regs rd rs1 rs2 + funct3.val.shiftl 12 + funct7.val.shiftl 25
| (R4 opcode7 funct3 rd rs1 rs2 rs3 funct2) :=
opcode7.val + regs rd rs1 rs2 rs3 + funct3.val.shiftl 12
+ funct2.val.shiftl 25
| (I opcode7 funct3 rd rs1 imm) :=
opcode7.val + regs rd rs1 + funct3.val.shiftl 12 + imm.sign.to_nat.shiftl 31
+ (bits imm.to_nat 10 0).shiftl 20
| (S opcode7 funct3 rs1 rs2 imm) :=
opcode7.val + regs 0 rs1 rs2 + funct3.val.shiftl 12
+ imm.sign.to_nat.shiftl 31 + (bits imm.to_nat 10 5).shiftl 25
+ (bits imm.to_nat 4 0).shiftl 7
| (B opcode7 funct3 rs1 rs2 imm) :=
opcode7.val + regs 0 rs1 rs2 + funct3.val.shiftl 12
+ imm.sign.to_nat.shiftl 31 + (bits imm.to_nat 10 5).shiftl 25
+ (bits imm 4 1).shiftl 8 + (bits imm 11 11).shiftl 7
| (U opcode7 rd imm) :=
opcode7.val + regs rd + imm.sign.to_nat.shiftl 31
+ (bits imm.to_nat 20 12).shiftl 12
| (J opcode7 rd imm) :=
opcode7.val + regs rd + imm.sign.to_nat.shiftl 31 + (bits imm 10 1).shiftl 21
+ (bits imm 11 11).shiftl 20 + (bits imm 19 12).shiftl 12
structure decoded :=
(opcode rd funct3 rs1 rs2 funct7 : ℕ)
(I_imm S_imm B_imm U_imm J_imm : ℤ)
private def decode_sign (n) : ℤ := if bits n 31 31 = 1 then -1 else 1
-- fixme: immediates are encoded in 2's complement
def decode (n : ℕ) : decoded :=
{
opcode := bits n 6 0,
rd := bits n 11 7,
funct3 := bits n 14 12,
rs1 := bits n 19 15,
rs2 := bits n 24 20,
funct7 := bits n 31 20,
I_imm := decode_sign n * bits n 30 20,
S_imm := decode_sign n * ((bits n 30 25).shiftl 5 + bits n 11 7),
B_imm := decode_sign n * ((bits n 30 25).shiftl 5 + (bits n 11 8).shiftl 1
+ (bits n 11 11).shiftl 11),
U_imm := decode_sign n * (bits n 30 12).shiftl 12,
J_imm := decode_sign n * ((bits n 10 1).shiftl 21 + (bits n 11 11).shiftl 20
+ (bits n 19 12).shiftl 12),
}
end fmt
def reg_imm (rtype) := reg rtype ⊕ ℤ
instance has_coe_reg (rtype) : has_coe (reg rtype) (reg_imm rtype) := ⟨λ r, sum.inl r⟩
instance has_coe_int (rtype) : has_coe ℤ (reg_imm rtype) := ⟨λ r, sum.inr r⟩
inductive compare | eq | ne | lt | le
inductive csr_mode | swap | set | clear
inductive rounding_mode | even | zero | down | up | max_magnitude | dyn
@[derive decidable_eq]
inductive sign_inj_mode | copy | not | xor
@[derive decidable_eq]
inductive arith
| xor | or | and | shiftl | shiftr
| add | sub | mul | mulh | div | rem
@[derive decidable_eq]
inductive arith_f
| add | sub | mul | div | rem
| sqrt | min | max
| sign_inj (mode : sign_inj_mode)
| fmadd | fmsub | fnmadd | fnmsub
inductive atomic_op | swap | add | and | or | xor | max | min
namespace arith
abbreviation has_imm (op : arith) : Prop :=
op ∈ [xor, or, and, shiftl, shiftr, add, sub]
end arith
namespace arith_f
abbreviation has_rs3 (op : arith_f) : Prop :=
op ∈ [fnmadd, fnmsub]
end arith_f
inductive inst
-- arithmetic operations
| arith (op : arith) (rd rs1 : reg integer)
(rs2_imm : if op.has_imm then reg_imm integer else reg integer)
| arith_f (op : arith_f) (rd rs1 rs2 : reg float)
(rs3 : if op.has_rs3 then reg float else opt_param unit ())
-- load upper immediate
| lui (rd : reg integer) (offset : ℤ) (apc : opt_param bool ff)
-- comparisons, classifications, and conversions
| compare {rtype} (c : compare) (rd : reg integer) (rs1 : reg rtype)
(rs2 : if rtype = integer then reg_imm integer else reg float)
| classify (rd : reg integer) (rs1 : reg float)
| convert {rtype} (rd : reg rtype)
(rs1 : reg (if rtype = integer then float else integer))
(mv : opt_param bool ff)
-- control flow
| jump (rd : reg integer) (base : option (reg integer)) (offset : ℤ)
| branch (c : compare) (rs1 rs2 : reg integer) (offset : ℤ)
-- memory
| load {rtype} (dest : reg rtype) (base : reg integer) (offset : ℤ)
| store {rtype} (src : reg rtype) (base : reg integer) (offset : ℤ)
| fence (mode pred succ : fin 16)
| fencei
| load_reserved (rd addr : reg integer) (acquire release : bool)
| store_conditional (rd addr src : reg integer) (acquire release : bool)
| atomic (op : atomic_op) (rd rs1 rs2 : reg integer) (acquire release : bool)
-- system
| ecall
| ebreak
-- "Zicsr"
| csr (mode : csr_mode) (rd : reg integer) (rs2_imm : reg_imm integer) (addr : ℤ)
namespace inst
open fmt arith arith_f sign_inj_mode
private def fmt_reg_imm {rtype} (funct3 : fin 8) (funct7 : fin 128) (rd rs1 : regnum)
: reg_imm rtype → fmt
| (sum.inl rs2) := R opcode.op funct3 rd rs1 rs2 funct7
| (sum.inr imm) := I opcode.op_imm funct3 rd rs1 imm
def to_fmt : inst → fmt
-- arithmetic operations
| (arith add rd rs1 rs2_imm) := fmt_reg_imm 0b000 0 rd rs1 rs2_imm
| (arith sub rd rs1 (sum.inl rs2)) := R opcode.op 0b000 rd rs1 rs2 0100000
| (arith sub rd rs1 (sum.inr imm)) := I opcode.op_imm 0b000 rd rs1 (-imm)
| (arith xor rd rs1 rs2_imm) := fmt_reg_imm 0b100 0 rd rs1 rs2_imm
| (arith or rd rs1 rs2_imm) := fmt_reg_imm 0b110 0 rd rs1 rs2_imm
| (arith and rd rs1 rs2_imm) := fmt_reg_imm 0b111 0 rd rs1 rs2_imm
| (arith shiftl rd rs1 rs2_imm) := fmt_reg_imm 0b001 0 rd rs1 rs2_imm
-- fixme signed rs1 -> funct7 = 0100000
| (arith shiftr rd rs1 rs2_imm) := fmt_reg_imm 0b101 0 rd rs1 rs2_imm
| (arith mul rd rs1 (rs2 : reg integer)) := R opcode.op 0b000 rd rs1 rs2 0b0000001
-- fixme signed/unsigned pairs of rs1/rs2
| (arith mulh rd rs1 (rs2 : reg integer)) := R opcode.op 0b001 rd rs1 rs2 0b0000001
-- fixme signed rs1 -> funct3 = 101
| (arith div rd rs1 (rs2 : reg integer)) := R opcode.op 0b100 rd rs1 rs2 0b0000001
-- fixme signed rs1 -> funct3 = 111
| (arith rem rd rs1 (rs2 : reg integer)) := R opcode.op 0b110 rd rs1 rs2 0b0000001
| (arith_f add rd rs1 rs2 ()) := R opcode.op_fp 0b000 rd rs1 rs2 0b0000001
| (arith_f sub rd rs1 rs2 ()) := R opcode.op_fp 0b000 rd rs1 rs2 0b0000001
| (arith_f mul rd rs1 rs2 ()) := R opcode.op_fp 0b000 rd rs1 rs2 0b0000001
| (arith_f div rd rs1 rs2 ()) := R opcode.op_fp 0b000 rd rs1 rs2 0b0000001
| (arith_f rem rd rs1 rs2 ()) := R opcode.op_fp 0b000 rd rs1 rs2 0b0000001
| (arith_f min rd rs1 rs2 ()) := R opcode.op_fp 0b110 rd rs1 rs2 0b0000001
| (arith_f max rd rs1 rs2 ()) := R opcode.op_fp 0b110 rd rs1 rs2 0b0000001
| (arith_f sqrt rd rs1 rs2 ()) := R opcode.op_fp 0b110 rd rs1 rs2 0b0000001
| (arith_f (sign_inj copy) rd rs1 rs2 ()) := R opcode.op_fp 0b110 rd rs1 rs2 0b0000001
| (arith_f (sign_inj not) rd rs1 rs2 ()) := R opcode.op_fp 0b110 rd rs1 rs2 0b0000001
| (arith_f (sign_inj xor) rd rs1 rs2 ()) := R opcode.op_fp 0b110 rd rs1 rs2 0b0000001
| (arith_f fmadd rd rs1 rs2 rs3) := R opcode.op_fp 0b110 rd rs1 rs2 0b0000001
| (arith_f fmsub rd rs1 rs2 rs3) := R opcode.op_fp 0b110 rd rs1 rs2 0b0000001
| (arith_f fnmadd rd rs1 rs2 rs3) := R opcode.op_fp 0b110 rd rs1 rs2 0b0000001
| (arith_f fnmsub rd rs1 rs2 rs3) := R opcode.op_fp 0b110 rd rs1 rs2 0b0000001
-- load upper immediate
| (lui rd offset apc) := R 0 0 0 0 0 0
-- comparisons, classifications, and conversions
| (compare c rd rs1 rs2) := R 0 0 0 0 0 0
| (classify rd rs1) := R 0 0 0 0 0 0
| (convert rd rs1 mv) := R 0 0 0 0 0 0
-- control flow
| (jump rd base offset) := R 0 0 0 0 0 0
| (branch c rs1 rs2 offset) := R 0 0 0 0 0 0
-- memory
| (load dest base offset) := R 0 0 0 0 0 0
| (store src base offset) := R 0 0 0 0 0 0
| (fence mode pred succ) := R 0 0 0 0 0 0
| fencei := R 0 0 0 0 0 0
| (load_reserved rd addr acquire release) := R 0 0 0 0 0 0
| (store_conditional rd addr src acquire release) := R 0 0 0 0 0 0
| (atomic op rd rs1 rs2 acquire release) := R 0 0 0 0 0 0
-- system
| ecall := R 0 0 0 0 0 0
| ebreak := R 0 0 0 0 0 0
-- "Zicsr"
| (csr mode rd rs2_imm addr) := R 0 0 0 0 0 0
def encode : inst → ℕ := fmt.encode ∘ to_fmt
end inst
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment