M-Labs
/
riscv-formal-nmigen
6
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Add RV32IM ISA

pull/3/head
Donald Sebastian Leung 2020-07-24 13:51:04 +08:00
parent 5bce84836c
commit 2421f1f6b6
3 changed files with 1611 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1459
insns/isa_rv32im.py Normal file
View File

File diff suppressed because it is too large Load Diff

45
insns/isa_rv32im.txt Normal file
View File

@ -0,0 +1,45 @@
lui
auipc
jal
jalr
beq
bne
blt
bge
bltu
bgeu
lb
lh
lw
lbu
lhu
sb
sh
sw
addi
slti
sltiu
xori
ori
andi
slli
srli
srai
add
sub
sll
slt
sltu
xor
srl
sra
or
and
mul
mulh
mulhsu
mulhu
div
divu
rem
remu

107
insns/isa_rv32im_gen.py Normal file
View File

@ -0,0 +1,107 @@
with open('isa_rv32im.py', 'w') as isa_rv32im:
def fprint(strng):
print(strng, file=isa_rv32im)
fprint("# Generated by isa_rv32im_gen.py")
fprint("from nmigen import *")
with open('isa_rv32im.txt', 'r') as isa_rv32im_txt_file:
isa_rv32im_insns = isa_rv32im_txt_file.read().split('\n')[:-1]
for isa_rv32im_insn in isa_rv32im_insns:
fprint("from insn_%s import *" % isa_rv32im_insn)
fprint("")
fprint("class rvfi_isa_rv32im(Elaboratable):")
fprint(" def __init__(self, RISCV_FORMAL_ILEN=32, RISCV_FORMAL_XLEN=32):")
fprint(" self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN")
fprint(" self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN")
fprint(" self.rvfi_valid = Signal(1)")
fprint(" self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN)")
fprint(" self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)")
fprint(" self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)")
fprint(" self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)")
fprint(" self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN)")
fprint("")
fprint(" self.spec_valid = Signal(1)")
fprint(" self.spec_trap = Signal(1)")
fprint(" self.spec_rs1_addr = Signal(5)")
fprint(" self.spec_rs2_addr = Signal(5)")
fprint(" self.spec_rd_addr = Signal(5)")
fprint(" self.spec_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)")
fprint(" self.spec_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)")
fprint(" self.spec_mem_addr = Signal(self.RISCV_FORMAL_XLEN)")
fprint(" self.spec_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))")
fprint(" self.spec_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))")
fprint(" self.spec_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)")
fprint(" def ports(self):")
fprint(" input_ports = [")
fprint(" self.rvfi_valid,")
fprint(" self.rvfi_insn,")
fprint(" self.rvfi_pc_rdata,")
fprint(" self.rvfi_rs1_rdata,")
fprint(" self.rvfi_rs2_rdata,")
fprint(" self.rvfi_mem_rdata")
fprint(" ]")
fprint(" output_ports = [")
fprint(" self.spec_valid,")
fprint(" self.spec_trap,")
fprint(" self.spec_rs1_addr,")
fprint(" self.spec_rs2_addr,")
fprint(" self.spec_rd_addr,")
fprint(" self.spec_rd_wdata,")
fprint(" self.spec_pc_wdata,")
fprint(" self.spec_mem_addr,")
fprint(" self.spec_mem_rmask,")
fprint(" self.spec_mem_wmask,")
fprint(" self.spec_mem_wdata")
fprint(" ]")
fprint(" return input_ports + output_ports")
fprint(" def elaborate(self, platform):")
fprint(" m = Module()")
fprint("")
for isa_rv32im_insn in isa_rv32im_insns:
fprint(" spec_insn_%s_valid = Signal(1)" % isa_rv32im_insn)
fprint(" spec_insn_%s_trap = Signal(1)" % isa_rv32im_insn)
fprint(" spec_insn_%s_rs1_addr = Signal(5)" % isa_rv32im_insn)
fprint(" spec_insn_%s_rs2_addr = Signal(5)" % isa_rv32im_insn)
fprint(" spec_insn_%s_rd_addr = Signal(5)" % isa_rv32im_insn)
fprint(" spec_insn_%s_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)" % isa_rv32im_insn)
fprint(" spec_insn_%s_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)" % isa_rv32im_insn)
fprint(" spec_insn_%s_mem_addr = Signal(self.RISCV_FORMAL_XLEN)" % isa_rv32im_insn)
fprint(" spec_insn_%s_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))" % isa_rv32im_insn)
fprint(" spec_insn_%s_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))" % isa_rv32im_insn)
fprint(" spec_insn_%s_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)" % isa_rv32im_insn)
fprint(" m.submodules.insn_%s = insn_%s = rvfi_insn_%s()" % (isa_rv32im_insn, isa_rv32im_insn, isa_rv32im_insn))
fprint(" m.d.comb += insn_%s.rvfi_valid.eq(self.rvfi_valid)" % isa_rv32im_insn)
fprint(" m.d.comb += insn_%s.rvfi_insn.eq(self.rvfi_insn)" % isa_rv32im_insn)
fprint(" m.d.comb += insn_%s.rvfi_pc_rdata.eq(self.rvfi_pc_rdata)" % isa_rv32im_insn)
fprint(" m.d.comb += insn_%s.rvfi_rs1_rdata.eq(self.rvfi_rs1_rdata)" % isa_rv32im_insn)
fprint(" m.d.comb += insn_%s.rvfi_rs2_rdata.eq(self.rvfi_rs2_rdata)" % isa_rv32im_insn)
fprint(" m.d.comb += insn_%s.rvfi_mem_rdata.eq(self.rvfi_mem_rdata)" % isa_rv32im_insn)
fprint(" m.d.comb += spec_insn_%s_valid.eq(insn_%s.spec_valid)" % (isa_rv32im_insn, isa_rv32im_insn))
fprint(" m.d.comb += spec_insn_%s_trap.eq(insn_%s.spec_trap)" % (isa_rv32im_insn, isa_rv32im_insn))
fprint(" m.d.comb += spec_insn_%s_rs1_addr.eq(insn_%s.spec_rs1_addr)" % (isa_rv32im_insn, isa_rv32im_insn))
fprint(" m.d.comb += spec_insn_%s_rs2_addr.eq(insn_%s.spec_rs2_addr)" % (isa_rv32im_insn, isa_rv32im_insn))
fprint(" m.d.comb += spec_insn_%s_rd_addr.eq(insn_%s.spec_rd_addr)" % (isa_rv32im_insn, isa_rv32im_insn))
fprint(" m.d.comb += spec_insn_%s_rd_wdata.eq(insn_%s.spec_rd_wdata)" % (isa_rv32im_insn, isa_rv32im_insn))
fprint(" m.d.comb += spec_insn_%s_pc_wdata.eq(insn_%s.spec_pc_wdata)" % (isa_rv32im_insn, isa_rv32im_insn))
fprint(" m.d.comb += spec_insn_%s_mem_addr.eq(insn_%s.spec_mem_addr)" % (isa_rv32im_insn, isa_rv32im_insn))
fprint(" m.d.comb += spec_insn_%s_mem_rmask.eq(insn_%s.spec_mem_rmask)" % (isa_rv32im_insn, isa_rv32im_insn))
fprint(" m.d.comb += spec_insn_%s_mem_wmask.eq(insn_%s.spec_mem_wmask)" % (isa_rv32im_insn, isa_rv32im_insn))
fprint(" m.d.comb += spec_insn_%s_mem_wdata.eq(insn_%s.spec_mem_wdata)" % (isa_rv32im_insn, isa_rv32im_insn))
fprint("")
def gen_spec(strng):
result = "0"
for isa_rv32im_insn in isa_rv32im_insns:
result = "Mux(spec_insn_%s_valid, spec_insn_%s_%s, %s)" % (isa_rv32im_insn, isa_rv32im_insn, strng, result)
fprint(" m.d.comb += self.spec_%s.eq(%s)" % (strng, result))
gen_spec("valid")
gen_spec("trap")
gen_spec("rs1_addr")
gen_spec("rs2_addr")
gen_spec("rd_addr")
gen_spec("rd_wdata")
gen_spec("pc_wdata")
gen_spec("mem_addr")
gen_spec("mem_rmask")
gen_spec("mem_wmask")
gen_spec("mem_wdata")
fprint("")
fprint(" return m")