Compare commits
110 Commits
1d315b4735
...
6459c71ac5
|
|
@ -12,7 +12,7 @@ TODO
|
|||
|
||||
## Scope
|
||||
|
||||
The full [RISC-V specification](https://riscv.org/specifications/) is hundreds of pages long including numerous possible extensions, some of which are still under active development at the time of writing. Therefore, this project does not aim to formalize the entire specification, but only the core parts of the specification, namely RV32I (except FENCE, ECALL and EBREAK) and perhaps RV32IM. Support for other extensions of the RISC-V specification may be added in the future.
|
||||
As with the original riscv-formal, support is planned for the RV32I and RV64I base ISAs, as well as the M and C extensions and combinations thereof (e.g. RV32IM, RV64IMC).
|
||||
|
||||
## License
|
||||
|
||||
|
|
|
|||
|
|
@ -1,81 +0,0 @@
|
|||
from nmigen import *
|
||||
from nmigen.hdl.ast import *
|
||||
|
||||
class rvfi_causal_check(Elaboratable):
|
||||
def __init__(self, RISCV_FORMAL_ILEN=32, RISCV_FORMAL_XLEN=32):
|
||||
self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN
|
||||
self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
|
||||
self.reset = Signal(1)
|
||||
self.check = Signal(1)
|
||||
self.rvfi_valid = Signal(1)
|
||||
self.rvfi_order = Signal(64)
|
||||
self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN)
|
||||
self.rvfi_trap = Signal(1)
|
||||
self.rvfi_halt = Signal(1)
|
||||
self.rvfi_intr = Signal(1)
|
||||
self.rvfi_mode = Signal(2)
|
||||
self.rvfi_ixl = Signal(2)
|
||||
self.rvfi_rs1_addr = Signal(5)
|
||||
self.rvfi_rs2_addr = Signal(5)
|
||||
self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rd_addr = Signal(5)
|
||||
self.rvfi_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
def ports(self):
|
||||
input_ports = [
|
||||
self.reset,
|
||||
self.check,
|
||||
self.rvfi_valid,
|
||||
self.rvfi_order,
|
||||
self.rvfi_insn,
|
||||
self.rvfi_trap,
|
||||
self.rvfi_halt,
|
||||
self.rvfi_intr,
|
||||
self.rvfi_mode,
|
||||
self.rvfi_ixl,
|
||||
self.rvfi_rs1_addr,
|
||||
self.rvfi_rs2_addr,
|
||||
self.rvfi_rs1_rdata,
|
||||
self.rvfi_rs2_rdata,
|
||||
self.rvfi_rd_addr,
|
||||
self.rvfi_rd_wdata,
|
||||
self.rvfi_pc_rdata,
|
||||
self.rvfi_pc_wdata,
|
||||
self.rvfi_mem_addr,
|
||||
self.rvfi_mem_rmask,
|
||||
self.rvfi_mem_wmask,
|
||||
self.rvfi_mem_rdata,
|
||||
self.rvfi_mem_wdata
|
||||
]
|
||||
output_ports = []
|
||||
return input_ports + output_ports
|
||||
def elaborate(self, platform):
|
||||
m = Module()
|
||||
|
||||
insn_order = AnyConst(64)
|
||||
register_index = AnyConst(5)
|
||||
found_non_causal = Signal(1, reset=0)
|
||||
|
||||
with m.If(self.reset):
|
||||
m.d.sync += found_non_causal.eq(0)
|
||||
with m.Else():
|
||||
with m.If(self.check):
|
||||
m.d.comb += Assume(register_index != 0)
|
||||
m.d.comb += Assume(self.rvfi_valid)
|
||||
m.d.comb += Assume(register_index == self.rvfi_rd_addr)
|
||||
m.d.comb += Assume(insn_order == self.rvfi_order)
|
||||
m.d.comb += Assert(~found_non_causal)
|
||||
with m.Else():
|
||||
with m.If(self.rvfi_valid & (self.rvfi_order > insn_order) & \
|
||||
((register_index == self.rvfi_rs1_addr) | \
|
||||
(register_index == self.rvfi_rs2_addr))):
|
||||
m.d.sync += found_non_causal.eq(1)
|
||||
|
||||
return m
|
||||
|
|
@ -1,103 +0,0 @@
|
|||
from nmigen import *
|
||||
from nmigen.hdl.ast import *
|
||||
|
||||
class rvfi_channel(Elaboratable):
|
||||
def __init__(self, RISCV_FORMAL_ILEN=32, RISCV_FORMAL_XLEN=32):
|
||||
self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN
|
||||
self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
|
||||
self.rvfi_valid = Signal(1)
|
||||
self.rvfi_order = Signal(64)
|
||||
self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN)
|
||||
self.rvfi_trap = Signal(1)
|
||||
self.rvfi_halt = Signal(1)
|
||||
self.rvfi_intr = Signal(1)
|
||||
self.rvfi_mode = Signal(2)
|
||||
self.rvfi_ixl = Signal(2)
|
||||
self.rvfi_rs1_addr = Signal(5)
|
||||
self.rvfi_rs2_addr = Signal(5)
|
||||
self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rd_addr = Signal(5)
|
||||
self.rvfi_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
def ports(self):
|
||||
input_ports = [
|
||||
self.rvfi_valid,
|
||||
self.rvfi_order,
|
||||
self.rvfi_insn,
|
||||
self.rvfi_trap,
|
||||
self.rvfi_halt,
|
||||
self.rvfi_intr,
|
||||
self.rvfi_mode,
|
||||
self.rvfi_ixl,
|
||||
self.rvfi_rs1_addr,
|
||||
self.rvfi_rs2_addr,
|
||||
self.rvfi_rs1_rdata,
|
||||
self.rvfi_rs2_rdata,
|
||||
self.rvfi_rd_addr,
|
||||
self.rvfi_rd_wdata,
|
||||
self.rvfi_pc_rdata,
|
||||
self.rvfi_pc_wdata,
|
||||
self.rvfi_mem_addr,
|
||||
self.rvfi_mem_rmask,
|
||||
self.rvfi_mem_wmask,
|
||||
self.rvfi_mem_rdata,
|
||||
self.rvfi_mem_wdata
|
||||
]
|
||||
output_ports = []
|
||||
return input_ports + output_ports
|
||||
def elaborate(self, platform):
|
||||
m = Module()
|
||||
|
||||
valid = Signal(1)
|
||||
m.d.comb += valid.eq(self.rvfi_valid)
|
||||
order = Signal(64)
|
||||
m.d.comb += order.eq(self.rvfi_order)
|
||||
insn = Signal(self.RISCV_FORMAL_ILEN)
|
||||
m.d.comb += insn.eq(self.rvfi_insn)
|
||||
trap = Signal(1)
|
||||
m.d.comb += trap.eq(self.rvfi_trap)
|
||||
halt = Signal(1)
|
||||
m.d.comb += halt.eq(self.rvfi_halt)
|
||||
intr = Signal(1)
|
||||
m.d.comb += intr.eq(self.rvfi_intr)
|
||||
mode = Signal(2)
|
||||
m.d.comb += mode.eq(self.rvfi_mode)
|
||||
ixl = Signal(2)
|
||||
m.d.comb += ixl.eq(self.rvfi_ixl)
|
||||
|
||||
rs1_addr = Signal(5)
|
||||
m.d.comb += rs1_addr.eq(self.rvfi_rs1_addr)
|
||||
rs2_addr = Signal(5)
|
||||
m.d.comb += rs2_addr.eq(self.rvfi_rs2_addr)
|
||||
rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += rs1_rdata.eq(self.rvfi_rs1_rdata)
|
||||
rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += rs2_rdata.eq(self.rvfi_rs2_rdata)
|
||||
rd_addr = Signal(5)
|
||||
m.d.comb += rd_addr.eq(self.rvfi_rd_addr)
|
||||
rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += rd_wdata.eq(self.rvfi_rd_wdata)
|
||||
pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += pc_rdata.eq(self.rvfi_pc_rdata)
|
||||
pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += pc_wdata.eq(self.rvfi_pc_wdata)
|
||||
|
||||
mem_addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += mem_addr.eq(self.rvfi_mem_addr)
|
||||
mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
m.d.comb += mem_rmask.eq(self.rvfi_mem_rmask)
|
||||
mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
m.d.comb += mem_wmask.eq(self.rvfi_mem_wmask)
|
||||
mem_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += mem_rdata.eq(self.rvfi_mem_rdata)
|
||||
mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += mem_wdata.eq(self.rvfi_mem_wdata)
|
||||
|
||||
return m
|
||||
|
|
@ -1,82 +0,0 @@
|
|||
from nmigen import *
|
||||
from nmigen.hdl.ast import *
|
||||
|
||||
class rvfi_dmem_check(Elaboratable):
|
||||
def __init__(self, RISCV_FORMAL_ILEN=32, RISCV_FORMAL_XLEN=32):
|
||||
self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN
|
||||
self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
|
||||
self.reset = Signal(1)
|
||||
self.enable = Signal(1)
|
||||
self.dmem_addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_valid = Signal(1)
|
||||
self.rvfi_order = Signal(64)
|
||||
self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN)
|
||||
self.rvfi_trap = Signal(1)
|
||||
self.rvfi_halt = Signal(1)
|
||||
self.rvfi_intr = Signal(1)
|
||||
self.rvfi_mode = Signal(2)
|
||||
self.rvfi_ixl = Signal(2)
|
||||
self.rvfi_rs1_addr = Signal(5)
|
||||
self.rvfi_rs2_addr = Signal(5)
|
||||
self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rd_addr = Signal(5)
|
||||
self.rvfi_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
def ports(self):
|
||||
input_ports = [
|
||||
self.reset,
|
||||
self.enable,
|
||||
self.rvfi_valid,
|
||||
self.rvfi_order,
|
||||
self.rvfi_insn,
|
||||
self.rvfi_trap,
|
||||
self.rvfi_halt,
|
||||
self.rvfi_intr,
|
||||
self.rvfi_mode,
|
||||
self.rvfi_ixl,
|
||||
self.rvfi_rs1_addr,
|
||||
self.rvfi_rs2_addr,
|
||||
self.rvfi_rs1_rdata,
|
||||
self.rvfi_rs2_rdata,
|
||||
self.rvfi_rd_addr,
|
||||
self.rvfi_rd_wdata,
|
||||
self.rvfi_pc_rdata,
|
||||
self.rvfi_pc_wdata,
|
||||
self.rvfi_mem_addr,
|
||||
self.rvfi_mem_rmask,
|
||||
self.rvfi_mem_wmask,
|
||||
self.rvfi_mem_rdata,
|
||||
self.rvfi_mem_wdata
|
||||
]
|
||||
output_ports = [
|
||||
self.dmem_addr
|
||||
]
|
||||
return input_ports + output_ports
|
||||
def elaborate(self, platform):
|
||||
m = Module()
|
||||
|
||||
dmem_addr_randval = AnyConst(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += self.dmem_addr.eq(dmem_addr_randval)
|
||||
|
||||
dmem_shadow = Signal(self.RISCV_FORMAL_XLEN)
|
||||
dmem_written = Signal(int(self.RISCV_FORMAL_XLEN // 8), reset=0)
|
||||
|
||||
with m.If(self.reset):
|
||||
m.d.sync += dmem_written.eq(0)
|
||||
with m.Else():
|
||||
with m.If(self.rvfi_valid & (self.rvfi_mem_addr == self.dmem_addr) & 1):
|
||||
for i in range(int(self.RISCV_FORMAL_XLEN // 8)):
|
||||
with m.If(self.enable & self.rvfi_mem_rmask[i] & dmem_written[i]):
|
||||
m.d.comb += Assert(dmem_shadow[i*8:i*8+8] == self.rvfi_mem_rdata[i*8:i*8+8])
|
||||
with m.If(self.rvfi_mem_wmask[i]):
|
||||
m.d.sync += dmem_shadow[i*8:i*8+8].eq(self.rvfi_mem_wdata[i*8:i*8+8])
|
||||
m.d.sync += dmem_written[i].eq(1)
|
||||
|
||||
return m
|
||||
|
|
@ -1,77 +0,0 @@
|
|||
from nmigen import *
|
||||
from nmigen.hdl.ast import *
|
||||
|
||||
class rvfi_hang_check(Elaboratable):
|
||||
def __init__(self, RISCV_FORMAL_ILEN=32, RISCV_FORMAL_XLEN=32):
|
||||
self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN
|
||||
self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
|
||||
self.reset = Signal(1)
|
||||
self.trig = Signal(1)
|
||||
self.check = Signal(1)
|
||||
self.rvfi_valid = Signal(1)
|
||||
self.rvfi_order = Signal(64)
|
||||
self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN)
|
||||
self.rvfi_trap = Signal(1)
|
||||
self.rvfi_halt = Signal(1)
|
||||
self.rvfi_intr = Signal(1)
|
||||
self.rvfi_mode = Signal(2)
|
||||
self.rvfi_ixl = Signal(2)
|
||||
self.rvfi_rs1_addr = Signal(5)
|
||||
self.rvfi_rs2_addr = Signal(5)
|
||||
self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rd_addr = Signal(5)
|
||||
self.rvfi_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
def ports(self):
|
||||
input_ports = [
|
||||
self.reset,
|
||||
self.trig,
|
||||
self.check,
|
||||
self.rvfi_valid,
|
||||
self.rvfi_order,
|
||||
self.rvfi_insn,
|
||||
self.rvfi_trap,
|
||||
self.rvfi_halt,
|
||||
self.rvfi_intr,
|
||||
self.rvfi_mode,
|
||||
self.rvfi_ixl,
|
||||
self.rvfi_rs1_addr,
|
||||
self.rvfi_rs2_addr,
|
||||
self.rvfi_rs1_rdata,
|
||||
self.rvfi_rs2_rdata,
|
||||
self.rvfi_rd_addr,
|
||||
self.rvfi_rd_wdata,
|
||||
self.rvfi_pc_rdata,
|
||||
self.rvfi_pc_wdata,
|
||||
self.rvfi_mem_addr,
|
||||
self.rvfi_mem_rmask,
|
||||
self.rvfi_mem_wmask,
|
||||
self.rvfi_mem_rdata,
|
||||
self.rvfi_mem_wdata
|
||||
]
|
||||
output_ports = []
|
||||
return input_ports + output_ports
|
||||
def elaborate(self, platform):
|
||||
m = Module()
|
||||
|
||||
okay = Signal(1, reset=0)
|
||||
|
||||
with m.If(self.reset):
|
||||
m.d.sync += okay.eq(0)
|
||||
with m.Else():
|
||||
with m.If(self.rvfi_valid):
|
||||
m.d.sync += okay.eq(1)
|
||||
with m.If(self.check):
|
||||
m.d.comb += Assert(okay)
|
||||
with m.If(self.rvfi_valid):
|
||||
m.d.comb += Assume(~self.rvfi_halt)
|
||||
m.d.comb += Assume(self.rvfi_insn != 0b00010000010100000000000001110011) # WFI
|
||||
|
||||
return m
|
||||
|
|
@ -1,109 +0,0 @@
|
|||
from nmigen import *
|
||||
from nmigen.hdl.ast import *
|
||||
|
||||
class rvfi_ill_check(Elaboratable):
|
||||
def __init__(self, RISCV_FORMAL_ILEN=32, RISCV_FORMAL_XLEN=32):
|
||||
self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN
|
||||
self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
|
||||
self.reset = Signal(1)
|
||||
self.check = Signal(1)
|
||||
self.rvfi_valid = Signal(1)
|
||||
self.rvfi_order = Signal(64)
|
||||
self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN)
|
||||
self.rvfi_trap = Signal(1)
|
||||
self.rvfi_halt = Signal(1)
|
||||
self.rvfi_intr = Signal(1)
|
||||
self.rvfi_mode = Signal(2)
|
||||
self.rvfi_ixl = Signal(2)
|
||||
self.rvfi_rs1_addr = Signal(5)
|
||||
self.rvfi_rs2_addr = Signal(5)
|
||||
self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rd_addr = Signal(5)
|
||||
self.rvfi_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
def ports(self):
|
||||
input_ports = [
|
||||
self.reset,
|
||||
self.check,
|
||||
self.rvfi_valid,
|
||||
self.rvfi_order,
|
||||
self.rvfi_insn,
|
||||
self.rvfi_trap,
|
||||
self.rvfi_halt,
|
||||
self.rvfi_intr,
|
||||
self.rvfi_mode,
|
||||
self.rvfi_ixl,
|
||||
self.rvfi_rs1_addr,
|
||||
self.rvfi_rs2_addr,
|
||||
self.rvfi_rs1_rdata,
|
||||
self.rvfi_rs2_rdata,
|
||||
self.rvfi_rd_addr,
|
||||
self.rvfi_rd_wdata,
|
||||
self.rvfi_pc_rdata,
|
||||
self.rvfi_pc_wdata,
|
||||
self.rvfi_mem_addr,
|
||||
self.rvfi_mem_rmask,
|
||||
self.rvfi_mem_wmask,
|
||||
self.rvfi_mem_rdata,
|
||||
self.rvfi_mem_wdata
|
||||
]
|
||||
output_ports = []
|
||||
return input_ports + output_ports
|
||||
def elaborate(self, platform):
|
||||
m = Module()
|
||||
|
||||
valid = Signal(1)
|
||||
m.d.comb += valid.eq((~self.reset) & self.rvfi_valid)
|
||||
insn = Signal(self.RISCV_FORMAL_ILEN)
|
||||
m.d.comb += insn.eq(self.rvfi_insn)
|
||||
trap = Signal(1)
|
||||
m.d.comb += trap.eq(self.rvfi_trap)
|
||||
halt = Signal(1)
|
||||
m.d.comb += halt.eq(self.rvfi_halt)
|
||||
intr = Signal(1)
|
||||
m.d.comb += intr.eq(self.rvfi_intr)
|
||||
rs1_addr = Signal(5)
|
||||
m.d.comb += rs1_addr.eq(self.rvfi_rs1_addr)
|
||||
rs2_addr = Signal(5)
|
||||
m.d.comb += rs2_addr.eq(self.rvfi_rs2_addr)
|
||||
rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += rs1_rdata.eq(self.rvfi_rs1_rdata)
|
||||
rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += rs2_rdata.eq(self.rvfi_rs2_rdata)
|
||||
rd_addr = Signal(5)
|
||||
m.d.comb += rd_addr.eq(self.rvfi_rd_addr)
|
||||
rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += rd_wdata.eq(self.rvfi_rd_wdata)
|
||||
pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += pc_rdata.eq(self.rvfi_pc_rdata)
|
||||
pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += pc_wdata.eq(self.rvfi_pc_wdata)
|
||||
|
||||
mem_addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += mem_addr.eq(self.rvfi_mem_addr)
|
||||
mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
m.d.comb += mem_rmask.eq(self.rvfi_mem_rmask)
|
||||
mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
m.d.comb += mem_wmask.eq(self.rvfi_mem_wmask)
|
||||
mem_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += mem_rdata.eq(self.rvfi_mem_rdata)
|
||||
mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += mem_wdata.eq(self.rvfi_mem_wdata)
|
||||
|
||||
m.d.comb += Cover((~self.reset) & self.check & valid & (insn == 0))
|
||||
with m.If((~self.reset) & self.check):
|
||||
m.d.comb += Assume(valid)
|
||||
m.d.comb += Assume(insn == 0)
|
||||
m.d.comb += Assert(trap)
|
||||
m.d.comb += Assert(rd_addr == 0)
|
||||
m.d.comb += Assert(rd_wdata == 0)
|
||||
m.d.comb += Assert(mem_wmask == 0)
|
||||
|
||||
return m
|
||||
|
|
@ -1,88 +0,0 @@
|
|||
from nmigen import *
|
||||
from nmigen.hdl.ast import *
|
||||
|
||||
class rvfi_imem_check(Elaboratable):
|
||||
def __init__(self, RISCV_FORMAL_ILEN=32, RISCV_FORMAL_XLEN=32):
|
||||
self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN
|
||||
self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
|
||||
self.reset = Signal(1)
|
||||
self.enable = Signal(1)
|
||||
self.imem_addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.imem_data = Signal(16)
|
||||
self.rvfi_valid = Signal(1)
|
||||
self.rvfi_order = Signal(64)
|
||||
self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN)
|
||||
self.rvfi_trap = Signal(1)
|
||||
self.rvfi_halt = Signal(1)
|
||||
self.rvfi_intr = Signal(1)
|
||||
self.rvfi_mode = Signal(2)
|
||||
self.rvfi_ixl = Signal(2)
|
||||
self.rvfi_rs1_addr = Signal(5)
|
||||
self.rvfi_rs2_addr = Signal(5)
|
||||
self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rd_addr = Signal(5)
|
||||
self.rvfi_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
def ports(self):
|
||||
input_ports = [
|
||||
self.reset,
|
||||
self.enable,
|
||||
self.rvfi_valid,
|
||||
self.rvfi_order,
|
||||
self.rvfi_insn,
|
||||
self.rvfi_trap,
|
||||
self.rvfi_halt,
|
||||
self.rvfi_intr,
|
||||
self.rvfi_mode,
|
||||
self.rvfi_ixl,
|
||||
self.rvfi_rs1_addr,
|
||||
self.rvfi_rs2_addr,
|
||||
self.rvfi_rs1_rdata,
|
||||
self.rvfi_rs2_rdata,
|
||||
self.rvfi_rd_addr,
|
||||
self.rvfi_rd_wdata,
|
||||
self.rvfi_pc_rdata,
|
||||
self.rvfi_pc_wdata,
|
||||
self.rvfi_mem_addr,
|
||||
self.rvfi_mem_rmask,
|
||||
self.rvfi_mem_wmask,
|
||||
self.rvfi_mem_rdata,
|
||||
self.rvfi_mem_wdata
|
||||
]
|
||||
output_ports = [
|
||||
self.imem_addr,
|
||||
self.imem_data
|
||||
]
|
||||
return input_ports + output_ports
|
||||
def elaborate(self, platform):
|
||||
m = Module()
|
||||
|
||||
imem_addr_randval = AnyConst(self.RISCV_FORMAL_XLEN)
|
||||
imem_data_randval = AnyConst(16)
|
||||
m.d.comb += self.imem_addr.eq(imem_addr_randval)
|
||||
m.d.comb += self.imem_data.eq(imem_data_randval)
|
||||
|
||||
pc = Signal(self.RISCV_FORMAL_XLEN)
|
||||
insn = Signal(self.RISCV_FORMAL_ILEN)
|
||||
|
||||
with m.If(self.reset):
|
||||
pass
|
||||
with m.Else():
|
||||
with m.If(self.enable & self.rvfi_valid):
|
||||
m.d.sync += pc.eq(self.rvfi_pc_rdata)
|
||||
m.d.sync += insn.eq(self.rvfi_insn)
|
||||
|
||||
with m.If(pc == self.imem_addr):
|
||||
m.d.comb += Assert(insn[:16] == self.imem_data)
|
||||
|
||||
with m.If((insn[:2] == 0b11) & (pc + 2 == self.imem_addr)):
|
||||
m.d.comb += Assert(insn[16:32] == self.imem_data)
|
||||
|
||||
return m
|
||||
|
|
@ -1,205 +0,0 @@
|
|||
from nmigen import *
|
||||
from nmigen.hdl.ast import *
|
||||
|
||||
# Ugly hack for now to get the insn_add import working
|
||||
import sys
|
||||
sys.path.append('../insns')
|
||||
from insn_add import *
|
||||
|
||||
class rvfi_insn_check(Elaboratable):
|
||||
def __init__(self, RISCV_FORMAL_ILEN=32, RISCV_FORMAL_XLEN=32):
|
||||
self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN
|
||||
self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
|
||||
self.reset = Signal(1)
|
||||
self.check = Signal(1)
|
||||
self.rvfi_valid = Signal(1)
|
||||
self.rvfi_order = Signal(64)
|
||||
self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN)
|
||||
self.rvfi_trap = Signal(1)
|
||||
self.rvfi_halt = Signal(1)
|
||||
self.rvfi_intr = Signal(1)
|
||||
self.rvfi_mode = Signal(2)
|
||||
self.rvfi_ixl = Signal(2)
|
||||
self.rvfi_rs1_addr = Signal(5)
|
||||
self.rvfi_rs2_addr = Signal(5)
|
||||
self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rd_addr = Signal(5)
|
||||
self.rvfi_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
def ports(self):
|
||||
input_ports = [
|
||||
self.reset,
|
||||
self.check,
|
||||
self.rvfi_valid,
|
||||
self.rvfi_order,
|
||||
self.rvfi_insn,
|
||||
self.rvfi_trap,
|
||||
self.rvfi_halt,
|
||||
self.rvfi_intr,
|
||||
self.rvfi_mode,
|
||||
self.rvfi_ixl,
|
||||
self.rvfi_rs1_addr,
|
||||
self.rvfi_rs2_addr,
|
||||
self.rvfi_rs1_rdata,
|
||||
self.rvfi_rs2_rdata,
|
||||
self.rvfi_rd_addr,
|
||||
self.rvfi_rd_wdata,
|
||||
self.rvfi_pc_rdata,
|
||||
self.rvfi_pc_wdata,
|
||||
self.rvfi_mem_addr,
|
||||
self.rvfi_mem_rmask,
|
||||
self.rvfi_mem_wmask,
|
||||
self.rvfi_mem_rdata,
|
||||
self.rvfi_mem_wdata
|
||||
]
|
||||
output_ports = []
|
||||
return input_ports + output_ports
|
||||
def elaborate(self, platform):
|
||||
m = Module()
|
||||
|
||||
valid = Signal(1)
|
||||
m.d.comb += valid.eq((~self.reset) & self.rvfi_valid)
|
||||
insn = Signal(self.RISCV_FORMAL_ILEN)
|
||||
m.d.comb += insn.eq(self.rvfi_insn)
|
||||
trap = Signal(1)
|
||||
m.d.comb += trap.eq(self.rvfi_trap)
|
||||
halt = Signal(1)
|
||||
m.d.comb += halt.eq(self.rvfi_halt)
|
||||
intr = Signal(1)
|
||||
m.d.comb += intr.eq(self.rvfi_intr)
|
||||
rs1_addr = Signal(5)
|
||||
m.d.comb += rs1_addr.eq(self.rvfi_rs1_addr)
|
||||
rs2_addr = Signal(5)
|
||||
m.d.comb += rs2_addr.eq(self.rvfi_rs2_addr)
|
||||
rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += rs1_rdata.eq(self.rvfi_rs1_rdata)
|
||||
rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += rs2_rdata.eq(self.rvfi_rs2_rdata)
|
||||
rd_addr = Signal(5)
|
||||
m.d.comb += rd_addr.eq(self.rvfi_rd_addr)
|
||||
rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += rd_wdata.eq(self.rvfi_rd_wdata)
|
||||
pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += pc_rdata.eq(self.rvfi_pc_rdata)
|
||||
pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += pc_wdata.eq(self.rvfi_pc_wdata)
|
||||
|
||||
mem_addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += mem_addr.eq(self.rvfi_mem_addr)
|
||||
mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
m.d.comb += mem_rmask.eq(self.rvfi_mem_rmask)
|
||||
mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
m.d.comb += mem_wmask.eq(self.rvfi_mem_wmask)
|
||||
mem_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += mem_rdata.eq(self.rvfi_mem_rdata)
|
||||
mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += mem_wdata.eq(self.rvfi_mem_wdata)
|
||||
|
||||
spec_valid = Signal(1)
|
||||
spec_trap = Signal(1)
|
||||
spec_rs1_addr = Signal(5)
|
||||
spec_rs2_addr = Signal(5)
|
||||
spec_rd_addr = Signal(5)
|
||||
spec_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
spec_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
spec_mem_addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
spec_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
spec_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
spec_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
|
||||
rs1_rdata_or_zero = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += rs1_rdata_or_zero.eq(Mux(spec_rs1_addr != 0, rs1_rdata, 0))
|
||||
rs2_rdata_or_zero = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += rs2_rdata_or_zero.eq(Mux(spec_rs2_addr != 0, rs2_rdata, 0))
|
||||
|
||||
# Change this submodule accordingly to test for different instructions(?)
|
||||
m.submodules.insn_spec = insn_spec = rvfi_insn_add(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN)
|
||||
|
||||
m.d.comb += insn_spec.rvfi_valid.eq(valid)
|
||||
m.d.comb += insn_spec.rvfi_insn.eq(insn)
|
||||
m.d.comb += insn_spec.rvfi_pc_rdata.eq(pc_rdata)
|
||||
m.d.comb += insn_spec.rvfi_rs1_rdata.eq(rs1_rdata_or_zero)
|
||||
m.d.comb += insn_spec.rvfi_rs2_rdata.eq(rs2_rdata_or_zero)
|
||||
m.d.comb += insn_spec.rvfi_mem_rdata.eq(mem_rdata)
|
||||
|
||||
m.d.comb += spec_valid.eq(insn_spec.spec_valid)
|
||||
m.d.comb += spec_trap.eq(insn_spec.spec_trap)
|
||||
m.d.comb += spec_rs1_addr.eq(insn_spec.spec_rs1_addr)
|
||||
m.d.comb += spec_rs2_addr.eq(insn_spec.spec_rs2_addr)
|
||||
m.d.comb += spec_rd_addr.eq(insn_spec.spec_rd_addr)
|
||||
m.d.comb += spec_rd_wdata.eq(insn_spec.spec_rd_wdata)
|
||||
m.d.comb += spec_pc_wdata.eq(insn_spec.spec_pc_wdata)
|
||||
m.d.comb += spec_mem_addr.eq(insn_spec.spec_mem_addr)
|
||||
m.d.comb += spec_mem_rmask.eq(insn_spec.spec_mem_rmask)
|
||||
m.d.comb += spec_mem_wmask.eq(insn_spec.spec_mem_wmask)
|
||||
m.d.comb += spec_mem_wdata.eq(insn_spec.spec_mem_wdata)
|
||||
|
||||
insn_pma_x = Signal(1)
|
||||
mem_pma_r = Signal(1)
|
||||
mem_pma_w = Signal(1)
|
||||
|
||||
mem_log2len = Signal(2)
|
||||
m.d.comb += mem_log2len.eq(Mux((spec_mem_rmask | spec_mem_wmask) & 0b11110000, 3, Mux((spec_mem_rmask | spec_mem_wmask) & 0b00001100, 2, Mux((spec_mem_rmask | spec_mem_wmask) & 0b00000010, 1, 0))))
|
||||
|
||||
m.d.comb += insn_pma_x.eq(1)
|
||||
m.d.comb += mem_pma_r.eq(1)
|
||||
m.d.comb += mem_pma_w.eq(1)
|
||||
|
||||
mem_access_fault = Signal(1)
|
||||
m.d.comb += mem_access_fault.eq((spec_mem_rmask & ~mem_pma_r) | (spec_mem_wmask & ~mem_pma_w) | (spec_mem_rmask | spec_mem_wmask))
|
||||
|
||||
with m.If(~self.reset):
|
||||
m.d.comb += Cover(spec_valid)
|
||||
m.d.comb += Cover(spec_valid & ~trap)
|
||||
m.d.comb += Cover(self.check & spec_valid)
|
||||
m.d.comb += Cover(self.check & spec_valid & ~trap)
|
||||
with m.If((~self.reset) & self.check):
|
||||
m.d.comb += Assume(spec_valid)
|
||||
|
||||
with m.If((~insn_pma_x) | mem_access_fault):
|
||||
m.d.comb += Assert(trap)
|
||||
m.d.comb += Assert(rd_addr == 0)
|
||||
m.d.comb += Assert(rd_wdata == 0)
|
||||
m.d.comb += Assert(mem_wmask == 0)
|
||||
with m.Else():
|
||||
with m.If(rs1_addr == 0):
|
||||
m.d.comb += Assert(rs1_rdata == 0)
|
||||
|
||||
with m.If(rs2_addr == 0):
|
||||
m.d.comb += Assert(rs2_rdata == 0)
|
||||
|
||||
with m.If(~spec_trap):
|
||||
with m.If(spec_rs1_addr != 0):
|
||||
m.d.comb += Assert(spec_rs1_addr == rs1_addr)
|
||||
|
||||
with m.If(spec_rs2_addr != 0):
|
||||
m.d.comb += Assert(spec_rs2_addr == rs2_addr)
|
||||
|
||||
m.d.comb += Assert(spec_rd_addr == rd_addr)
|
||||
m.d.comb += Assert(spec_rd_wdata == rd_wdata)
|
||||
m.d.comb += Assert(spec_pc_wdata == pc_wdata)
|
||||
|
||||
with m.If(spec_mem_wmask | spec_mem_rmask):
|
||||
m.d.comb += Assert(spec_mem_addr == mem_addr)
|
||||
|
||||
for i in range(int(self.RISCV_FORMAL_XLEN // 8)):
|
||||
with m.If(spec_mem_wmask[i]):
|
||||
m.d.comb += Assert(mem_wmask[i])
|
||||
m.d.comb += Assert(spec_mem_wdata[i*8:i*8+8] == mem_wdata[i*8:i*8+8])
|
||||
with m.Elif(mem_wmask[i]):
|
||||
m.d.comb += Assert(mem_rmask[i])
|
||||
m.d.comb += Assert(mem_rdata[i*8:i*8+8] == mem_wdata[i*8:i*8+8])
|
||||
with m.If(spec_mem_rmask[i]):
|
||||
m.d.comb += Assert(mem_rmask[i])
|
||||
|
||||
|
||||
m.d.comb += Assert(spec_trap == trap)
|
||||
|
||||
return m
|
||||
|
|
@ -1,79 +0,0 @@
|
|||
from nmigen import *
|
||||
from nmigen.hdl.ast import *
|
||||
|
||||
class rvfi_liveness_check(Elaboratable):
|
||||
def __init__(self, RISCV_FORMAL_ILEN=32, RISCV_FORMAL_XLEN=32):
|
||||
self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN
|
||||
self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
|
||||
self.reset = Signal(1)
|
||||
self.trig = Signal(1)
|
||||
self.check = Signal(1)
|
||||
self.rvfi_valid = Signal(1)
|
||||
self.rvfi_order = Signal(64)
|
||||
self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN)
|
||||
self.rvfi_trap = Signal(1)
|
||||
self.rvfi_halt = Signal(1)
|
||||
self.rvfi_intr = Signal(1)
|
||||
self.rvfi_mode = Signal(2)
|
||||
self.rvfi_ixl = Signal(2)
|
||||
self.rvfi_rs1_addr = Signal(5)
|
||||
self.rvfi_rs2_addr = Signal(5)
|
||||
self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rd_addr = Signal(5)
|
||||
self.rvfi_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
def ports(self):
|
||||
input_ports = [
|
||||
self.reset,
|
||||
self.trig,
|
||||
self.check,
|
||||
self.rvfi_valid,
|
||||
self.rvfi_order,
|
||||
self.rvfi_insn,
|
||||
self.rvfi_trap,
|
||||
self.rvfi_halt,
|
||||
self.rvfi_intr,
|
||||
self.rvfi_mode,
|
||||
self.rvfi_ixl,
|
||||
self.rvfi_rs1_addr,
|
||||
self.rvfi_rs2_addr,
|
||||
self.rvfi_rs1_rdata,
|
||||
self.rvfi_rs2_rdata,
|
||||
self.rvfi_rd_addr,
|
||||
self.rvfi_rd_wdata,
|
||||
self.rvfi_pc_rdata,
|
||||
self.rvfi_pc_wdata,
|
||||
self.rvfi_mem_addr,
|
||||
self.rvfi_mem_rmask,
|
||||
self.rvfi_mem_wmask,
|
||||
self.rvfi_mem_rdata,
|
||||
self.rvfi_mem_wdata
|
||||
]
|
||||
output_ports = []
|
||||
return input_ports + output_ports
|
||||
def elaborate(self, platform):
|
||||
m = Module()
|
||||
|
||||
insn_order = AnyConst(64)
|
||||
found_next_insn = Signal(1, reset=0)
|
||||
|
||||
with m.If(self.reset):
|
||||
m.d.sync += found_next_insn.eq(0)
|
||||
with m.Else():
|
||||
with m.If(self.rvfi_valid & (self.rvfi_order == insn_order + 1)):
|
||||
m.d.sync += found_next_insn.eq(1)
|
||||
with m.If(self.trig):
|
||||
m.d.comb += Assume(self.rvfi_valid)
|
||||
m.d.comb += Assume(~self.rvfi_halt)
|
||||
m.d.comb += Assume(insn_order == self.rvfi_order)
|
||||
with m.If(self.check):
|
||||
m.d.comb += Assert(found_next_insn)
|
||||
|
||||
return m
|
||||
|
|
@ -1,82 +0,0 @@
|
|||
from nmigen import *
|
||||
from nmigen.hdl.ast import *
|
||||
|
||||
class rvfi_pc_bwd_check(Elaboratable):
|
||||
def __init__(self, RISCV_FORMAL_ILEN=32, RISCV_FORMAL_XLEN=32):
|
||||
self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN
|
||||
self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
|
||||
self.reset = Signal(1)
|
||||
self.check = Signal(1)
|
||||
self.rvfi_valid = Signal(1)
|
||||
self.rvfi_order = Signal(64)
|
||||
self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN)
|
||||
self.rvfi_trap = Signal(1)
|
||||
self.rvfi_halt = Signal(1)
|
||||
self.rvfi_intr = Signal(1)
|
||||
self.rvfi_mode = Signal(2)
|
||||
self.rvfi_ixl = Signal(2)
|
||||
self.rvfi_rs1_addr = Signal(5)
|
||||
self.rvfi_rs2_addr = Signal(5)
|
||||
self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rd_addr = Signal(5)
|
||||
self.rvfi_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
def ports(self):
|
||||
input_ports = [
|
||||
self.reset,
|
||||
self.check,
|
||||
self.rvfi_valid,
|
||||
self.rvfi_order,
|
||||
self.rvfi_insn,
|
||||
self.rvfi_trap,
|
||||
self.rvfi_halt,
|
||||
self.rvfi_intr,
|
||||
self.rvfi_mode,
|
||||
self.rvfi_ixl,
|
||||
self.rvfi_rs1_addr,
|
||||
self.rvfi_rs2_addr,
|
||||
self.rvfi_rs1_rdata,
|
||||
self.rvfi_rs2_rdata,
|
||||
self.rvfi_rd_addr,
|
||||
self.rvfi_rd_wdata,
|
||||
self.rvfi_pc_rdata,
|
||||
self.rvfi_pc_wdata,
|
||||
self.rvfi_mem_addr,
|
||||
self.rvfi_mem_rmask,
|
||||
self.rvfi_mem_wmask,
|
||||
self.rvfi_mem_rdata,
|
||||
self.rvfi_mem_wdata
|
||||
]
|
||||
output_ports = []
|
||||
return input_ports + output_ports
|
||||
def elaborate(self, platform):
|
||||
m = Module()
|
||||
|
||||
insn_order = AnyConst(64)
|
||||
expect_pc = Signal(self.RISCV_FORMAL_XLEN)
|
||||
expect_pc_valid = Signal(1, reset=0)
|
||||
|
||||
pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += pc_wdata.eq(self.rvfi_pc_wdata)
|
||||
|
||||
with m.If(self.reset):
|
||||
m.d.sync += expect_pc_valid.eq(0)
|
||||
with m.Else():
|
||||
with m.If(self.check):
|
||||
m.d.comb += Assume(self.rvfi_valid)
|
||||
m.d.comb += Assume(insn_order == self.rvfi_order)
|
||||
with m.If(expect_pc_valid):
|
||||
m.d.comb += Assert(expect_pc == pc_wdata)
|
||||
with m.Else():
|
||||
with m.If(self.rvfi_valid & (self.rvfi_order == insn_order + 1)):
|
||||
m.d.sync += expect_pc.eq(self.rvfi_pc_rdata)
|
||||
m.d.sync += expect_pc_valid.eq(1)
|
||||
|
||||
return m
|
||||
|
|
@ -1,82 +0,0 @@
|
|||
from nmigen import *
|
||||
from nmigen.hdl.ast import *
|
||||
|
||||
class rvfi_pc_fwd_check(Elaboratable):
|
||||
def __init__(self, RISCV_FORMAL_ILEN=32, RISCV_FORMAL_XLEN=32):
|
||||
self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN
|
||||
self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
|
||||
self.reset = Signal(1)
|
||||
self.check = Signal(1)
|
||||
self.rvfi_valid = Signal(1)
|
||||
self.rvfi_order = Signal(64)
|
||||
self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN)
|
||||
self.rvfi_trap = Signal(1)
|
||||
self.rvfi_halt = Signal(1)
|
||||
self.rvfi_intr = Signal(1)
|
||||
self.rvfi_mode = Signal(2)
|
||||
self.rvfi_ixl = Signal(2)
|
||||
self.rvfi_rs1_addr = Signal(5)
|
||||
self.rvfi_rs2_addr = Signal(5)
|
||||
self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rd_addr = Signal(5)
|
||||
self.rvfi_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
def ports(self):
|
||||
input_ports = [
|
||||
self.reset,
|
||||
self.check,
|
||||
self.rvfi_valid,
|
||||
self.rvfi_order,
|
||||
self.rvfi_insn,
|
||||
self.rvfi_trap,
|
||||
self.rvfi_halt,
|
||||
self.rvfi_intr,
|
||||
self.rvfi_mode,
|
||||
self.rvfi_ixl,
|
||||
self.rvfi_rs1_addr,
|
||||
self.rvfi_rs2_addr,
|
||||
self.rvfi_rs1_rdata,
|
||||
self.rvfi_rs2_rdata,
|
||||
self.rvfi_rd_addr,
|
||||
self.rvfi_rd_wdata,
|
||||
self.rvfi_pc_rdata,
|
||||
self.rvfi_pc_wdata,
|
||||
self.rvfi_mem_addr,
|
||||
self.rvfi_mem_rmask,
|
||||
self.rvfi_mem_wmask,
|
||||
self.rvfi_mem_rdata,
|
||||
self.rvfi_mem_wdata
|
||||
]
|
||||
output_ports = []
|
||||
return input_ports + output_ports
|
||||
def elaborate(self, platform):
|
||||
m = Module()
|
||||
|
||||
insn_order = AnyConst(64)
|
||||
expect_pc = Signal(self.RISCV_FORMAL_XLEN)
|
||||
expect_pc_valid = Signal(1, reset=0)
|
||||
|
||||
pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += pc_rdata.eq(self.rvfi_pc_rdata)
|
||||
|
||||
with m.If(self.reset):
|
||||
m.d.sync += expect_pc_valid.eq(0)
|
||||
with m.Else():
|
||||
with m.If(self.check):
|
||||
m.d.comb += Assume(self.rvfi_valid)
|
||||
m.d.comb += Assume(insn_order == self.rvfi_order)
|
||||
with m.If(expect_pc_valid):
|
||||
m.d.comb += Assert(expect_pc == pc_rdata)
|
||||
with m.Else():
|
||||
with m.If(self.rvfi_valid & (self.rvfi_order == insn_order - 1)):
|
||||
m.d.sync += expect_pc.eq(self.rvfi_pc_wdata)
|
||||
m.d.sync += expect_pc_valid.eq(1)
|
||||
|
||||
return m
|
||||
|
|
@ -1,84 +0,0 @@
|
|||
from nmigen import *
|
||||
from nmigen.hdl.ast import *
|
||||
|
||||
class rvfi_reg_check(Elaboratable):
|
||||
def __init__(self, RISCV_FORMAL_ILEN=32, RISCV_FORMAL_XLEN=32):
|
||||
self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN
|
||||
self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
|
||||
self.reset = Signal(1)
|
||||
self.check = Signal(1)
|
||||
self.rvfi_valid = Signal(1)
|
||||
self.rvfi_order = Signal(64)
|
||||
self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN)
|
||||
self.rvfi_trap = Signal(1)
|
||||
self.rvfi_halt = Signal(1)
|
||||
self.rvfi_intr = Signal(1)
|
||||
self.rvfi_mode = Signal(2)
|
||||
self.rvfi_ixl = Signal(2)
|
||||
self.rvfi_rs1_addr = Signal(5)
|
||||
self.rvfi_rs2_addr = Signal(5)
|
||||
self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rd_addr = Signal(5)
|
||||
self.rvfi_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
def ports(self):
|
||||
input_ports = [
|
||||
self.reset,
|
||||
self.check,
|
||||
self.rvfi_valid,
|
||||
self.rvfi_order,
|
||||
self.rvfi_insn,
|
||||
self.rvfi_trap,
|
||||
self.rvfi_halt,
|
||||
self.rvfi_intr,
|
||||
self.rvfi_mode,
|
||||
self.rvfi_ixl,
|
||||
self.rvfi_rs1_addr,
|
||||
self.rvfi_rs2_addr,
|
||||
self.rvfi_rs1_rdata,
|
||||
self.rvfi_rs2_rdata,
|
||||
self.rvfi_rd_addr,
|
||||
self.rvfi_rd_wdata,
|
||||
self.rvfi_pc_rdata,
|
||||
self.rvfi_pc_wdata,
|
||||
self.rvfi_mem_addr,
|
||||
self.rvfi_mem_rmask,
|
||||
self.rvfi_mem_wmask,
|
||||
self.rvfi_mem_rdata,
|
||||
self.rvfi_mem_wdata
|
||||
]
|
||||
output_ports = []
|
||||
return input_ports + output_ports
|
||||
def elaborate(self, platform):
|
||||
m = Module()
|
||||
|
||||
insn_order = AnyConst(64)
|
||||
register_index = AnyConst(5)
|
||||
register_shadow = Signal(self.RISCV_FORMAL_XLEN, reset=0)
|
||||
register_written = Signal(1, reset=0)
|
||||
|
||||
with m.If(self.reset):
|
||||
m.d.sync += register_shadow.eq(0)
|
||||
m.d.sync += register_written.eq(0)
|
||||
with m.Else():
|
||||
with m.If(self.check):
|
||||
m.d.comb += Assume(self.rvfi_valid)
|
||||
m.d.comb += Assume(insn_order == self.rvfi_order)
|
||||
|
||||
with m.If(register_written & (register_index == self.rvfi_rs1_addr)):
|
||||
m.d.comb += Assert(register_shadow == self.rvfi_rs1_rdata)
|
||||
with m.If(register_written & (register_index == self.rvfi_rs2_addr)):
|
||||
m.d.comb += Assert(register_shadow == self.rvfi_rs2_rdata)
|
||||
with m.Else():
|
||||
with m.If(self.rvfi_valid & (self.rvfi_order < insn_order) & (register_index == self.rvfi_rd_addr)):
|
||||
m.d.sync += register_shadow.eq(self.rvfi_rd_wdata)
|
||||
m.d.sync += register_written.eq(1)
|
||||
|
||||
return m
|
||||
|
|
@ -1,78 +0,0 @@
|
|||
from nmigen import *
|
||||
from nmigen.hdl.ast import *
|
||||
|
||||
class rvfi_unique_check(Elaboratable):
|
||||
def __init__(self, RISCV_FORMAL_ILEN=32, RISCV_FORMAL_XLEN=32):
|
||||
self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN
|
||||
self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
|
||||
self.reset = Signal(1)
|
||||
self.trig = Signal(1)
|
||||
self.check = Signal(1)
|
||||
self.rvfi_valid = Signal(1)
|
||||
self.rvfi_order = Signal(64)
|
||||
self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN)
|
||||
self.rvfi_trap = Signal(1)
|
||||
self.rvfi_halt = Signal(1)
|
||||
self.rvfi_intr = Signal(1)
|
||||
self.rvfi_mode = Signal(2)
|
||||
self.rvfi_ixl = Signal(2)
|
||||
self.rvfi_rs1_addr = Signal(5)
|
||||
self.rvfi_rs2_addr = Signal(5)
|
||||
self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rd_addr = Signal(5)
|
||||
self.rvfi_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
def ports(self):
|
||||
input_ports = [
|
||||
self.reset,
|
||||
self.trig,
|
||||
self.check,
|
||||
self.rvfi_valid,
|
||||
self.rvfi_order,
|
||||
self.rvfi_insn,
|
||||
self.rvfi_trap,
|
||||
self.rvfi_halt,
|
||||
self.rvfi_intr,
|
||||
self.rvfi_mode,
|
||||
self.rvfi_ixl,
|
||||
self.rvfi_rs1_addr,
|
||||
self.rvfi_rs2_addr,
|
||||
self.rvfi_rs1_rdata,
|
||||
self.rvfi_rs2_rdata,
|
||||
self.rvfi_rd_addr,
|
||||
self.rvfi_rd_wdata,
|
||||
self.rvfi_pc_rdata,
|
||||
self.rvfi_pc_wdata,
|
||||
self.rvfi_mem_addr,
|
||||
self.rvfi_mem_rmask,
|
||||
self.rvfi_mem_wmask,
|
||||
self.rvfi_mem_rdata,
|
||||
self.rvfi_mem_wdata
|
||||
]
|
||||
output_ports = []
|
||||
return input_ports + output_ports
|
||||
def elaborate(self, platform):
|
||||
m = Module()
|
||||
|
||||
insn_order = AnyConst(64)
|
||||
found_other_insn = Signal(1, reset=0)
|
||||
|
||||
with m.If(self.reset):
|
||||
m.d.sync += found_other_insn.eq(0)
|
||||
with m.Else():
|
||||
with m.If(self.rvfi_valid & (self.rvfi_order == insn_order) & ~self.trig):
|
||||
m.d.sync += found_other_insn.eq(1)
|
||||
with m.If(self.trig):
|
||||
m.d.comb += Assume(self.rvfi_valid)
|
||||
m.d.comb += Assume(insn_order == self.rvfi_order)
|
||||
with m.If(self.check):
|
||||
m.d.comb += Assert(~found_other_insn)
|
||||
|
||||
return m
|
||||
112
insns/README.md
112
insns/README.md
|
|
@ -1,28 +1,102 @@
|
|||
# RISC-V Instructions
|
||||
|
||||
Refer to the table below for the instructions currently supported. At the time of writing, it covers the instructions in the RV32I base ISA except FENCE, ECALL and EBREAK, as well as the RV32M extension\*.
|
||||
## Instructions
|
||||
|
||||
Below is a table of RISC-V instructions supported by the original riscv-formal framework at the time of writing, categorized by instruction type.
|
||||
|
||||
| Instruction type | Instructions |
|
||||
| --- | --- |
|
||||
| U-type | lui, auipc |
|
||||
| UJ-type | jal |
|
||||
| I-type | jalr, lb, lh, lw, lbu, lhu, addi, slti, sltiu, xori, ori, andi |
|
||||
| SB-type | beq, bne, blt, bge, bltu, bgeu |
|
||||
| S-type | sb, sh, sw |
|
||||
| I-type (shift variation) | slli, srli, srai |
|
||||
| R-type | add, sub, sll, slt, sltu, xor, srl, sra, or, and, mul, mulh, mulhsu, mulhu, div, divu, rem, remu |
|
||||
| R-type | ADD, ADDW, AND, DIV, DIVU, DIVUW, DIVW, MUL, MULH, MULHSU, MULHU, MULW, OR, REM, REMU, REMUW, REMW, SLL, SLLW, SLT, SLTU, SRA, SRAW, SRL, SRLW, SUB, SUBW, XOR |
|
||||
| I-type | ADDI, ADDIW, ANDI, JALR, LB, LBU, LD, LH, LHU, LW, LWU, ORI, SLTI, SLTIU, XORI |
|
||||
| I-type (shift variation) | SLLI, SLLIW, SRAI, SRAIW, SRLI, SRLIW |
|
||||
| S-type | SB, SD, SH, SW |
|
||||
| SB-type | BEQ, BGE, BGEU, BLT, BLTU, BNE |
|
||||
| U-type | AUIPC, LUI |
|
||||
| UJ-type | JAL |
|
||||
| CI-type | C\_ADD, C\_ADDI, C\_ADDIW, C\_JALR, C\_JR, C\_LI, C\_MV |
|
||||
| CI-type (SP variation) | C\_ADDI16SP |
|
||||
| CI-type (ANDI variation) | C\_ANDI |
|
||||
| CI-type (LSP variation, 32 bit version) | C\_LWSP |
|
||||
| CI-type (LSP variation, 64 bit version) | C\_LDSP |
|
||||
| CI-type (LUI variation) | C\_LUI |
|
||||
| CI-type (SLI variation) | C\_SLLI |
|
||||
| CI-type (SRI variation) | C\_SRAI, C\_SRLI |
|
||||
| CIW-type | C\_ADDI4SPN |
|
||||
| CS-type (ALU version) | C\_ADDW, C\_AND, C\_OR, C\_SUB, C\_SUBW, C\_XOR |
|
||||
| CS-type (32 bit version) | C\_SW |
|
||||
| CS-type (64 bit version) | C\_SD |
|
||||
| CSS-type (32 bit version) | C\_SWSP |
|
||||
| CSS-type (64 bit version) | C\_SDSP |
|
||||
| CB-type | C\_BEQZ, C\_BNEZ |
|
||||
| CJ-type | C\_J, C\_JAL |
|
||||
| CL-type (32 bit version) | C\_LW |
|
||||
| CL-type (64 bit version) | C\_LD |
|
||||
|
||||
\* Due to limitations with modern solvers, they are sometimes unable to verify assertions involving multiplication and/or division; therefore, the core under test is expected to implement alternative operations for the RV32M extensions for the purposes of formal verification only, replacing multiplication/division operations with addition/subtraction and XORing with selected bitmasks.
|
||||
## Class Synopsis
|
||||
|
||||
## Caveats
|
||||
### Instructions
|
||||
|
||||
At the time of writing, the set of instructions supported in this port of riscv-formal is a mere subset of those supported in the original riscv-formal; for example, compressed instructions and 64-bit ISAs/extensions are not supported. Also note that the original riscv-formal contains tunable parameters that have been fixed to certain values in this translation:
|
||||
Below is a list of instructions currently supported by this port of the riscv-formal framework and is expected to grow over time. The instructions are roughly grouped by instruction type but sometimes with further specializations - the hierarchy of the lists reflects the hierarchy of inheritance in the classes used to represent various instructions.
|
||||
|
||||
| Parameter from riscv-formal | Fixed value in riscv-formal-nmigen |
|
||||
| --- | --- |
|
||||
| `RISCV_FORMAL_ILEN` | 32 |
|
||||
| `RISCV_FORMAL_XLEN` | 32 |
|
||||
| `RISCV_FORMAL_CSR_MISA` | undefined |
|
||||
| `RISCV_FORMAL_COMPRESSED` | undefined |
|
||||
| `RISCV_FORMAL_ALIGNED_MEM` | undefined |
|
||||
| `RISCV_FORMAL_ALTOPS` | defined |
|
||||
- `Insn`: General RISC-V instruction
|
||||
- `InsnRV32IRType`: RV32I R-Type Instruction
|
||||
- `InsnAdd`: ADD instruction
|
||||
- `InsnSub`: SUB instruction
|
||||
- `InsnSll`: SLL instruction
|
||||
- `InsnSlt`: SLT instruction
|
||||
- `InsnSltu`: SLTU instruction
|
||||
- `InsnXor`: XOR instruction
|
||||
- `InsnSrl`: SRL instruction
|
||||
- `InsnSra`: SRA instruction
|
||||
- `InsnOr`: OR instruction
|
||||
- `InsnAnd`: AND instruction
|
||||
- `InsnRV32IITypeShift`: RV32I I-Type Instruction (Shift Variation)
|
||||
- `InsnSlli`: SLLI instruction
|
||||
- `InsnSrli`: SRLI instruction
|
||||
- `InsnSrai`: SRAI instruction
|
||||
- `InsnRV32IIType`: RV32I I-Type Instruction
|
||||
- `InsnJalr`: JALR instruction
|
||||
- `InsnRV32IITypeLoad`: RV32I I-Type Instruction (Load Variation)
|
||||
- `InsnLb`: LB instruction
|
||||
- `InsnLh`: LH instruction
|
||||
- `InsnLw`: LW instruction
|
||||
- `InsnLbu`: LBU instruction
|
||||
- `InsnLhu`: LHU instruction
|
||||
- `InsnRV32IITypeArith`: RV32I I-Type Instruction (Arithmetic Variation)
|
||||
- `InsnAddi`: ADDI instruction
|
||||
- `InsnSlti`: SLTI instruction
|
||||
- `InsnSltiu`: SLTIU instruction
|
||||
- `InsnXori`: XORI instruction
|
||||
- `InsnOri`: ORI instruction
|
||||
- `InsnAndi`: ANDI instruction
|
||||
- `InsnRV32ISType`: RV32I S-Type Instruction
|
||||
- `InsnSb`: SB instruction
|
||||
- `InsnSh`: SH instruction
|
||||
- `InsnSw`: SW instruction
|
||||
- `InsnRV32ISBType`: RV32I SB-Type Instruction
|
||||
- `InsnBeq`: BEQ instruction
|
||||
- `InsnBne`: BNE instruction
|
||||
- `InsnBlt`: BLT instruction
|
||||
- `InsnBge`: BGE instruction
|
||||
- `InsnBltu`: BLTU instruction
|
||||
- `InsnBgeu`: BGEU instruction
|
||||
- `InsnJal`: JAL instruction
|
||||
- `InsnRV32IUType`: RV32I U-Type Instruction
|
||||
- `InsnLui`: LUI instruction
|
||||
- `InsnAuipc`: AUIPC instruction
|
||||
|
||||
### ISAs
|
||||
|
||||
- `IsaRV32I`: RV32I Base ISA
|
||||
|
||||
## Core-specific constants
|
||||
|
||||
The following core-specific constants are currently supported:
|
||||
|
||||
| Constant | Description | Valid value(s) | Supported by instruction(s) | Supported by ISA(s) |
|
||||
| --- | --- | --- | --- | --- |
|
||||
| `RISCV_FORMAL_ILEN` | Max length of instruction retired by core | `32` | 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 | RV32I |
|
||||
| `RISCV_FORMAL_XLEN` | Width of integer registers | `32` | 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 | RV32I |
|
||||
| `RISCV_FORMAL_CSR_MISA` | Support for MISA CSRs enabled | `True`, `False` | 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 | RV32I |
|
||||
| `RISCV_FORMAL_COMPRESSED` | Support for compressed instructions | `True`, `False` | JAL, JALR, BEQ, BNE, BLT, BGE, BLTU, BGEU | RV32I |
|
||||
| `RISCV_FORMAL_ALIGNED_MEM` | Require aligned memory accesses | `True`, `False` | LB, LH, LW, LBU, LHU, SB, SH, SW | RV32I |
|
||||
|
|
|
|||
|
|
@ -1,27 +1,55 @@
|
|||
from nmigen import *
|
||||
|
||||
class rvfi_insn(Elaboratable):
|
||||
def __init__(self):
|
||||
# Input ports
|
||||
self.rvfi_valid = Signal(1)
|
||||
self.rvfi_insn = Signal(32)
|
||||
self.rvfi_pc_rdata = Signal(32)
|
||||
self.rvfi_rs1_rdata = Signal(32)
|
||||
self.rvfi_rs2_rdata = Signal(32)
|
||||
self.rvfi_mem_rdata = Signal(32)
|
||||
"""
|
||||
Insn.py
|
||||
Class for generic RISC-V instructions
|
||||
"""
|
||||
|
||||
# Output ports
|
||||
class Insn(Elaboratable):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
# Core-specific constants
|
||||
self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN
|
||||
self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
|
||||
self.RISCV_FORMAL_CSR_MISA = RISCV_FORMAL_CSR_MISA
|
||||
|
||||
# RVFI input ports
|
||||
self.rvfi_valid = Signal(1)
|
||||
self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN)
|
||||
self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
if self.RISCV_FORMAL_CSR_MISA:
|
||||
self.rvfi_csr_misa_rdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
|
||||
# RVFI output ports
|
||||
if self.RISCV_FORMAL_CSR_MISA:
|
||||
self.spec_csr_misa_rmask = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.spec_valid = Signal(1)
|
||||
self.spec_trap = Signal(1)
|
||||
self.spec_rs1_addr = Signal(5)
|
||||
self.spec_rs2_addr = Signal(5)
|
||||
self.spec_rd_addr = Signal(5)
|
||||
self.spec_rd_wdata = Signal(32)
|
||||
self.spec_pc_wdata = Signal(32)
|
||||
self.spec_mem_addr = Signal(32)
|
||||
self.spec_mem_rmask = Signal(4)
|
||||
self.spec_mem_wmask = Signal(4)
|
||||
self.spec_mem_wdata = Signal(32)
|
||||
self.spec_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.spec_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.spec_mem_addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.spec_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.spec_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
|
||||
self.spec_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
|
||||
|
||||
# Additional wires and registers
|
||||
self.insn_padding = Signal(self.RISCV_FORMAL_ILEN)
|
||||
self.insn_imm = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.insn_funct7 = Signal(7)
|
||||
self.insn_funct6 = Signal(6)
|
||||
self.insn_shamt = Signal(6)
|
||||
self.insn_rs2 = Signal(5)
|
||||
self.insn_rs1 = Signal(5)
|
||||
self.insn_funct3 = Signal(3)
|
||||
self.insn_rd = Signal(5)
|
||||
self.insn_opcode = Signal(7)
|
||||
self.misa_ok = Signal(1)
|
||||
self.ialign16 = Signal(1)
|
||||
def ports(self):
|
||||
input_ports = [
|
||||
self.rvfi_valid,
|
||||
|
|
@ -31,6 +59,8 @@ class rvfi_insn(Elaboratable):
|
|||
self.rvfi_rs2_rdata,
|
||||
self.rvfi_mem_rdata
|
||||
]
|
||||
if self.RISCV_FORMAL_CSR_MISA:
|
||||
input_ports.append(self.rvfi_csr_misa_rdata)
|
||||
output_ports = [
|
||||
self.spec_valid,
|
||||
self.spec_trap,
|
||||
|
|
@ -44,8 +74,33 @@ class rvfi_insn(Elaboratable):
|
|||
self.spec_mem_wmask,
|
||||
self.spec_mem_wdata
|
||||
]
|
||||
if self.RISCV_FORMAL_CSR_MISA:
|
||||
output_ports.append(self.spec_csr_misa_rmask)
|
||||
return input_ports + output_ports
|
||||
def elaborate(self, platform):
|
||||
m = Module()
|
||||
|
||||
m.d.comb += self.insn_padding.eq(self.rvfi_insn >> 32)
|
||||
m.d.comb += self.insn_funct7.eq(self.rvfi_insn[25:32])
|
||||
m.d.comb += self.insn_funct6.eq(self.rvfi_insn[26:32])
|
||||
m.d.comb += self.insn_shamt.eq(self.rvfi_insn[20:26])
|
||||
m.d.comb += self.insn_rs2.eq(self.rvfi_insn[20:25])
|
||||
m.d.comb += self.insn_rs1.eq(self.rvfi_insn[15:20])
|
||||
m.d.comb += self.insn_funct3.eq(self.rvfi_insn[12:15])
|
||||
m.d.comb += self.insn_rd.eq(self.rvfi_insn[7:12])
|
||||
m.d.comb += self.insn_opcode.eq(self.rvfi_insn[:7])
|
||||
|
||||
# default assignments
|
||||
m.d.comb += self.spec_valid.eq(0)
|
||||
m.d.comb += self.spec_trap.eq(~self.misa_ok)
|
||||
m.d.comb += self.spec_rs1_addr.eq(0)
|
||||
m.d.comb += self.spec_rs2_addr.eq(0)
|
||||
m.d.comb += self.spec_rd_addr.eq(0)
|
||||
m.d.comb += self.spec_rd_wdata.eq(0)
|
||||
m.d.comb += self.spec_pc_wdata.eq(0)
|
||||
m.d.comb += self.spec_mem_addr.eq(0)
|
||||
m.d.comb += self.spec_mem_rmask.eq(0)
|
||||
m.d.comb += self.spec_mem_wmask.eq(0)
|
||||
m.d.comb += self.spec_mem_wdata.eq(0)
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,38 +0,0 @@
|
|||
from insn import *
|
||||
|
||||
class rvfi_insn_I(rvfi_insn):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_I, self).__init__()
|
||||
self.insn_padding = Signal(32)
|
||||
self.insn_imm = Signal(32)
|
||||
self.insn_rs1 = Signal(5)
|
||||
self.insn_funct3 = Signal(3)
|
||||
self.insn_rd = Signal(5)
|
||||
self.insn_opcode = Signal(7)
|
||||
self.misa_ok = Signal(1)
|
||||
self.ialign16 = Signal(1)
|
||||
def ports(self):
|
||||
return super(rvfi_insn_I, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_I, self).elaborate(platform)
|
||||
|
||||
# I-type instruction format
|
||||
m.d.comb += self.insn_padding.eq(self.rvfi_insn >> 32)
|
||||
m.d.comb += self.insn_imm.eq(Value.as_signed(self.rvfi_insn[20:32]))
|
||||
m.d.comb += self.insn_rs1.eq(self.rvfi_insn[15:20])
|
||||
m.d.comb += self.insn_funct3.eq(self.rvfi_insn[12:15])
|
||||
m.d.comb += self.insn_rd.eq(self.rvfi_insn[7:12])
|
||||
m.d.comb += self.insn_opcode.eq(self.rvfi_insn[:7])
|
||||
|
||||
m.d.comb += self.misa_ok.eq(1)
|
||||
m.d.comb += self.ialign16.eq(0)
|
||||
|
||||
# default assignments
|
||||
m.d.comb += self.spec_rs2_addr.eq(0)
|
||||
m.d.comb += self.spec_trap.eq(~self.misa_ok)
|
||||
m.d.comb += self.spec_mem_addr.eq(0)
|
||||
m.d.comb += self.spec_mem_rmask.eq(0)
|
||||
m.d.comb += self.spec_mem_wmask.eq(0)
|
||||
m.d.comb += self.spec_mem_wdata.eq(0)
|
||||
|
||||
return m
|
||||
|
|
@ -1,38 +0,0 @@
|
|||
from insn import *
|
||||
|
||||
class rvfi_insn_I_shift(rvfi_insn):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_I_shift, self).__init__()
|
||||
self.insn_padding = Signal(32)
|
||||
self.insn_funct6 = Signal(7)
|
||||
self.insn_shamt = Signal(6)
|
||||
self.insn_rs1 = Signal(5)
|
||||
self.insn_funct3 = Signal(3)
|
||||
self.insn_rd = Signal(5)
|
||||
self.insn_opcode = Signal(7)
|
||||
self.misa_ok = Signal(1)
|
||||
def ports(self):
|
||||
return super(rvfi_insn_I_shift, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_I_shift, self).elaborate(platform)
|
||||
|
||||
# I-type instruction format (shift variation)
|
||||
m.d.comb += self.insn_padding.eq(self.rvfi_insn >> 32)
|
||||
m.d.comb += self.insn_funct6.eq(self.rvfi_insn[26:32])
|
||||
m.d.comb += self.insn_shamt.eq(self.rvfi_insn[20:26])
|
||||
m.d.comb += self.insn_rs1.eq(self.rvfi_insn[15:20])
|
||||
m.d.comb += self.insn_funct3.eq(self.rvfi_insn[12:15])
|
||||
m.d.comb += self.insn_rd.eq(self.rvfi_insn[7:12])
|
||||
m.d.comb += self.insn_opcode.eq(self.rvfi_insn[:7])
|
||||
|
||||
m.d.comb += self.misa_ok.eq(1)
|
||||
|
||||
# default assignments
|
||||
m.d.comb += self.spec_rs2_addr.eq(0)
|
||||
m.d.comb += self.spec_trap.eq(~self.misa_ok)
|
||||
m.d.comb += self.spec_mem_addr.eq(0)
|
||||
m.d.comb += self.spec_mem_rmask.eq(0)
|
||||
m.d.comb += self.spec_mem_wmask.eq(0)
|
||||
m.d.comb += self.spec_mem_wdata.eq(0)
|
||||
|
||||
return m
|
||||
|
|
@ -1,37 +0,0 @@
|
|||
from insn import *
|
||||
|
||||
class rvfi_insn_R(rvfi_insn):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_R, self).__init__()
|
||||
self.insn_padding = Signal(32)
|
||||
self.insn_funct7 = Signal(7)
|
||||
self.insn_rs2 = Signal(5)
|
||||
self.insn_rs1 = Signal(5)
|
||||
self.insn_funct3 = Signal(3)
|
||||
self.insn_rd = Signal(5)
|
||||
self.insn_opcode = Signal(7)
|
||||
self.misa_ok = Signal(1)
|
||||
def ports(self):
|
||||
return super(rvfi_insn_R, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_R, self).elaborate(platform)
|
||||
|
||||
# R-type instruction format
|
||||
m.d.comb += self.insn_padding.eq(self.rvfi_insn >> 32)
|
||||
m.d.comb += self.insn_funct7.eq(self.rvfi_insn[25:32])
|
||||
m.d.comb += self.insn_rs2.eq(self.rvfi_insn[20:25])
|
||||
m.d.comb += self.insn_rs1.eq(self.rvfi_insn[15:20])
|
||||
m.d.comb += self.insn_funct3.eq(self.rvfi_insn[12:15])
|
||||
m.d.comb += self.insn_rd.eq(self.rvfi_insn[7:12])
|
||||
m.d.comb += self.insn_opcode.eq(self.rvfi_insn[:7])
|
||||
|
||||
m.d.comb += self.misa_ok.eq(1)
|
||||
|
||||
# default assignments
|
||||
m.d.comb += self.spec_trap.eq(~self.misa_ok)
|
||||
m.d.comb += self.spec_mem_addr.eq(0)
|
||||
m.d.comb += self.spec_mem_rmask.eq(0)
|
||||
m.d.comb += self.spec_mem_wmask.eq(0)
|
||||
m.d.comb += self.spec_mem_wdata.eq(0)
|
||||
|
||||
return m
|
||||
|
|
@ -1,32 +0,0 @@
|
|||
from insn import *
|
||||
class rvfi_insn_S(rvfi_insn):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_S, self).__init__()
|
||||
self.insn_padding = Signal(32)
|
||||
self.insn_imm = Signal(32)
|
||||
self.insn_rs2 = Signal(5)
|
||||
self.insn_rs1 = Signal(5)
|
||||
self.insn_funct3 = Signal(3)
|
||||
self.insn_opcode = Signal(7)
|
||||
self.misa_ok = Signal(1)
|
||||
def ports(self):
|
||||
return super(rvfi_insn_S, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_S, self).elaborate(platform)
|
||||
|
||||
# S-type instruction format
|
||||
m.d.comb += self.insn_padding.eq(self.rvfi_insn >> 32)
|
||||
m.d.comb += self.insn_imm.eq(Value.as_signed(Cat(self.rvfi_insn[7:12], self.rvfi_insn[25:32])))
|
||||
m.d.comb += self.insn_rs2.eq(self.rvfi_insn[20:25])
|
||||
m.d.comb += self.insn_rs1.eq(self.rvfi_insn[15:20])
|
||||
m.d.comb += self.insn_funct3.eq(self.rvfi_insn[12:15])
|
||||
m.d.comb += self.insn_opcode.eq(self.rvfi_insn[:7])
|
||||
|
||||
m.d.comb += self.misa_ok.eq(1)
|
||||
|
||||
# default assignments
|
||||
m.d.comb += self.spec_rd_addr.eq(0)
|
||||
m.d.comb += self.spec_rd_wdata.eq(0)
|
||||
m.d.comb += self.spec_mem_rmask.eq(0)
|
||||
|
||||
return m
|
||||
|
|
@ -1,38 +0,0 @@
|
|||
from insn import *
|
||||
|
||||
class rvfi_insn_SB(rvfi_insn):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_SB, self).__init__()
|
||||
self.insn_padding = Signal(32)
|
||||
self.insn_imm = Signal(32)
|
||||
self.insn_rs2 = Signal(5)
|
||||
self.insn_rs1 = Signal(5)
|
||||
self.insn_funct3 = Signal(3)
|
||||
self.insn_opcode = Signal(7)
|
||||
self.misa_ok = Signal(1)
|
||||
self.ialign16 = Signal(1)
|
||||
def ports(self):
|
||||
return super(rvfi_insn_SB, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_SB, self).elaborate(platform)
|
||||
|
||||
# SB-type instruction format
|
||||
m.d.comb += self.insn_padding.eq(self.rvfi_insn >> 32)
|
||||
m.d.comb += self.insn_imm.eq(Value.as_signed(Cat(self.rvfi_insn[8:12], self.rvfi_insn[25:31], self.rvfi_insn[7], self.rvfi_insn[31]) << 1))
|
||||
m.d.comb += self.insn_rs2.eq(self.rvfi_insn[20:25])
|
||||
m.d.comb += self.insn_rs1.eq(self.rvfi_insn[15:20])
|
||||
m.d.comb += self.insn_funct3.eq(self.rvfi_insn[12:15])
|
||||
m.d.comb += self.insn_opcode.eq(self.rvfi_insn[:7])
|
||||
|
||||
m.d.comb += self.misa_ok.eq(1)
|
||||
m.d.comb += self.ialign16.eq(0)
|
||||
|
||||
# default assignments
|
||||
m.d.comb += self.spec_rd_addr.eq(0)
|
||||
m.d.comb += self.spec_rd_wdata.eq(0)
|
||||
m.d.comb += self.spec_mem_addr.eq(0)
|
||||
m.d.comb += self.spec_mem_rmask.eq(0)
|
||||
m.d.comb += self.spec_mem_wmask.eq(0)
|
||||
m.d.comb += self.spec_mem_wdata.eq(0)
|
||||
|
||||
return m
|
||||
|
|
@ -1,33 +0,0 @@
|
|||
from insn import *
|
||||
|
||||
class rvfi_insn_U(rvfi_insn):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_U, self).__init__()
|
||||
self.insn_padding = Signal(32)
|
||||
self.insn_imm = Signal(32)
|
||||
self.insn_rd = Signal(5)
|
||||
self.insn_opcode = Signal(7)
|
||||
self.misa_ok = Signal(1)
|
||||
def ports(self):
|
||||
return super(rvfi_insn_U, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_U, self).elaborate(platform)
|
||||
|
||||
# U-type instruction format
|
||||
m.d.comb += self.insn_padding.eq(self.rvfi_insn >> 32)
|
||||
m.d.comb += self.insn_imm.eq(Value.as_signed(self.rvfi_insn[12:32] << 12))
|
||||
m.d.comb += self.insn_rd.eq(self.rvfi_insn[7:12])
|
||||
m.d.comb += self.insn_opcode.eq(self.rvfi_insn[:7])
|
||||
|
||||
m.d.comb += self.misa_ok.eq(1)
|
||||
|
||||
# Default assignments
|
||||
m.d.comb += self.spec_rs1_addr.eq(0)
|
||||
m.d.comb += self.spec_rs2_addr.eq(0)
|
||||
m.d.comb += self.spec_trap.eq(~self.misa_ok)
|
||||
m.d.comb += self.spec_mem_addr.eq(0)
|
||||
m.d.comb += self.spec_mem_rmask.eq(0)
|
||||
m.d.comb += self.spec_mem_wmask.eq(0)
|
||||
m.d.comb += self.spec_mem_wdata.eq(0)
|
||||
|
||||
return m
|
||||
|
|
@ -1,34 +0,0 @@
|
|||
from insn import *
|
||||
|
||||
class rvfi_insn_UJ(rvfi_insn):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_UJ, self).__init__()
|
||||
self.insn_padding = Signal(32)
|
||||
self.insn_imm = Signal(32)
|
||||
self.insn_rd = Signal(5)
|
||||
self.insn_opcode = Signal(7)
|
||||
self.misa_ok = Signal(1)
|
||||
self.ialign16 = Signal(1)
|
||||
def ports(self):
|
||||
return super(rvfi_insn_UJ, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_UJ, self).elaborate(platform)
|
||||
|
||||
# UJ-type instruction format
|
||||
m.d.comb += self.insn_padding.eq(self.rvfi_insn >> 32)
|
||||
m.d.comb += self.insn_imm.eq(Value.as_signed(Cat(self.rvfi_insn[21:31], self.rvfi_insn[20], self.rvfi_insn[12:20], self.rvfi_insn[31]) << 1))
|
||||
m.d.comb += self.insn_rd.eq(self.rvfi_insn[7:12])
|
||||
m.d.comb += self.insn_opcode.eq(self.rvfi_insn[:7])
|
||||
|
||||
m.d.comb += self.misa_ok.eq(1)
|
||||
m.d.comb += self.ialign16.eq(0)
|
||||
|
||||
# Default assignments
|
||||
m.d.comb += self.spec_rs1_addr.eq(0)
|
||||
m.d.comb += self.spec_rs2_addr.eq(0)
|
||||
m.d.comb += self.spec_mem_addr.eq(0)
|
||||
m.d.comb += self.spec_mem_rmask.eq(0)
|
||||
m.d.comb += self.spec_mem_wmask.eq(0)
|
||||
m.d.comb += self.spec_mem_wdata.eq(0)
|
||||
|
||||
return m
|
||||
|
|
@ -1,21 +1,15 @@
|
|||
from insn_R import *
|
||||
from insn_rv32i_r_type import *
|
||||
|
||||
class rvfi_insn_add(rvfi_insn_R):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_add, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_add, self).ports()
|
||||
"""
|
||||
ADD instruction
|
||||
"""
|
||||
|
||||
class InsnAdd(InsnRV32IRType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b000, 0b0110011)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_add, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# ADD instruction
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq(self.rvfi_rs1_rdata + self.rvfi_rs2_rdata)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct7 == 0b0000000) & (self.insn_funct3 == 0b000) & (self.insn_opcode == 0b0110011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata + self.rvfi_rs2_rdata, 0))
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,20 +1,15 @@
|
|||
from insn_I import *
|
||||
from insn_rv32i_i_type_arith import *
|
||||
|
||||
class rvfi_insn_addi(rvfi_insn_I):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_addi, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_addi, self).ports()
|
||||
"""
|
||||
ADDI instruction
|
||||
"""
|
||||
|
||||
class InsnAddi(InsnRV32IITypeArith):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b000)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_addi, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# ADDI instruction
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq(self.rvfi_rs1_rdata + self.insn_imm)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == 0b000) & (self.insn_opcode == 0b0010011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata + self.insn_imm, 0))
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,21 +1,15 @@
|
|||
from insn_R import *
|
||||
from insn_rv32i_r_type import *
|
||||
|
||||
class rvfi_insn_and(rvfi_insn_R):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_and, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_and, self).ports()
|
||||
"""
|
||||
AND instruction
|
||||
"""
|
||||
|
||||
class InsnAnd(InsnRV32IRType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b111, 0b0110011)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_and, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# AND instruction
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq(self.rvfi_rs1_rdata & self.rvfi_rs2_rdata)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct7 == 0b0000000) & (self.insn_funct3 == 0b111) & (self.insn_opcode == 0b0110011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata & self.rvfi_rs2_rdata, 0))
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,20 +1,15 @@
|
|||
from insn_I import *
|
||||
from insn_rv32i_i_type_arith import *
|
||||
|
||||
class rvfi_insn_andi(rvfi_insn_I):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_andi, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_andi, self).ports()
|
||||
"""
|
||||
ANDI instruction
|
||||
"""
|
||||
|
||||
class InsnAndi(InsnRV32IITypeArith):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b111)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_andi, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# ANDI instruction
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq(self.rvfi_rs1_rdata & self.insn_imm)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == 0b111) & (self.insn_opcode == 0b0010011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata & self.insn_imm, 0))
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,17 +1,15 @@
|
|||
from insn_U import *
|
||||
from insn_rv32i_u_type import *
|
||||
|
||||
class rvfi_insn_auipc(rvfi_insn_U):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_auipc, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_auipc, self).ports()
|
||||
"""
|
||||
AUIPC instruction
|
||||
"""
|
||||
|
||||
class InsnAuipc(InsnRV32IUType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0010111)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_auipc, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# AUIPC instruction
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_opcode == 0b0010111))
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_pc_rdata + self.insn_imm, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,21 +1,17 @@
|
|||
from insn_SB import *
|
||||
from insn_rv32i_sb_type import *
|
||||
|
||||
class rvfi_insn_beq(rvfi_insn_SB):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_beq, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_beq, self).ports()
|
||||
"""
|
||||
BEQ instruction
|
||||
"""
|
||||
|
||||
class InsnBeq(InsnRV32ISBType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b000)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_beq, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# BEQ instruction
|
||||
cond = Signal(1)
|
||||
m.d.comb += cond.eq(self.rvfi_rs1_rdata == self.rvfi_rs2_rdata)
|
||||
next_pc = Signal(32)
|
||||
m.d.comb += next_pc.eq(Mux(cond, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4))
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == 0b000) & (self.insn_opcode == 0b1100011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
next_pc = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += next_pc.eq(Mux(self.rvfi_rs1_rdata == self.rvfi_rs2_rdata, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4))
|
||||
m.d.comb += self.spec_pc_wdata.eq(next_pc)
|
||||
m.d.comb += self.spec_trap.eq(Mux(self.ialign16, next_pc[0] != 0, next_pc[:2] != 0) | ~self.misa_ok)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,21 +1,17 @@
|
|||
from insn_SB import *
|
||||
from insn_rv32i_sb_type import *
|
||||
|
||||
class rvfi_insn_bge(rvfi_insn_SB):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_bge, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_bge, self).ports()
|
||||
"""
|
||||
BGE instruction
|
||||
"""
|
||||
|
||||
class InsnBge(InsnRV32ISBType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b101)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_bge, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# BGE instruction
|
||||
cond = Signal(1)
|
||||
m.d.comb += cond.eq(Value.as_signed(self.rvfi_rs1_rdata) >= Value.as_signed(self.rvfi_rs2_rdata))
|
||||
next_pc = Signal(32)
|
||||
m.d.comb += next_pc.eq(Mux(cond, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4))
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == 0b101) & (self.insn_opcode == 0b1100011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
next_pc = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += next_pc.eq(Mux(Value.as_signed(self.rvfi_rs1_rdata) >= Value.as_signed(self.rvfi_rs2_rdata), self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4))
|
||||
m.d.comb += self.spec_pc_wdata.eq(next_pc)
|
||||
m.d.comb += self.spec_trap.eq(Mux(self.ialign16, next_pc[0] != 0, next_pc[:2] != 0) | ~self.misa_ok)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,21 +1,17 @@
|
|||
from insn_SB import *
|
||||
from insn_rv32i_sb_type import *
|
||||
|
||||
class rvfi_insn_bgeu(rvfi_insn_SB):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_bgeu, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_bgeu, self).ports()
|
||||
"""
|
||||
BGEU instruction
|
||||
"""
|
||||
|
||||
class InsnBgeu(InsnRV32ISBType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b111)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_bgeu, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# BGEU instruction
|
||||
cond = Signal(1)
|
||||
m.d.comb += cond.eq(self.rvfi_rs1_rdata >= self.rvfi_rs2_rdata)
|
||||
next_pc = Signal(32)
|
||||
m.d.comb += next_pc.eq(Mux(cond, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4))
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == 0b111) & (self.insn_opcode == 0b1100011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
next_pc = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += next_pc.eq(Mux(self.rvfi_rs1_rdata >= self.rvfi_rs2_rdata, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4))
|
||||
m.d.comb += self.spec_pc_wdata.eq(next_pc)
|
||||
m.d.comb += self.spec_trap.eq(Mux(self.ialign16, next_pc[0] != 0, next_pc[:2] != 0) | ~self.misa_ok)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,21 +1,17 @@
|
|||
from insn_SB import *
|
||||
from insn_rv32i_sb_type import *
|
||||
|
||||
class rvfi_insn_blt(rvfi_insn_SB):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_blt, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_blt, self).ports()
|
||||
"""
|
||||
BLT instruction
|
||||
"""
|
||||
|
||||
class InsnBlt(InsnRV32ISBType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b100)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_blt, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# BLT instruction
|
||||
cond = Signal(1)
|
||||
m.d.comb += cond.eq(Value.as_signed(self.rvfi_rs1_rdata) < Value.as_signed(self.rvfi_rs2_rdata))
|
||||
next_pc = Signal(32)
|
||||
m.d.comb += next_pc.eq(Mux(cond, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4))
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == 0b100) & (self.insn_opcode == 0b1100011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
next_pc = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += next_pc.eq(Mux(Value.as_signed(self.rvfi_rs1_rdata) < Value.as_signed(self.rvfi_rs2_rdata), self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4))
|
||||
m.d.comb += self.spec_pc_wdata.eq(next_pc)
|
||||
m.d.comb += self.spec_trap.eq(Mux(self.ialign16, next_pc[0] != 0, next_pc[:2] != 0) | ~self.misa_ok)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,21 +1,17 @@
|
|||
from insn_SB import *
|
||||
from insn_rv32i_sb_type import *
|
||||
|
||||
class rvfi_insn_bltu(rvfi_insn_SB):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_bltu, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_bltu, self).ports()
|
||||
"""
|
||||
BLTU instruction
|
||||
"""
|
||||
|
||||
class InsnBltu(InsnRV32ISBType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b110)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_bltu, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# BLTU instruction
|
||||
cond = Signal(1)
|
||||
m.d.comb += cond.eq(self.rvfi_rs1_rdata < self.rvfi_rs2_rdata)
|
||||
next_pc = Signal(32)
|
||||
m.d.comb += next_pc.eq(Mux(cond, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4))
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == 0b110) & (self.insn_opcode == 0b1100011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
next_pc = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += next_pc.eq(Mux(self.rvfi_rs1_rdata < self.rvfi_rs2_rdata, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4))
|
||||
m.d.comb += self.spec_pc_wdata.eq(next_pc)
|
||||
m.d.comb += self.spec_trap.eq(Mux(self.ialign16, next_pc[0] != 0, next_pc[:2] != 0) | ~self.misa_ok)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,21 +1,17 @@
|
|||
from insn_SB import *
|
||||
from insn_rv32i_sb_type import *
|
||||
|
||||
class rvfi_insn_bne(rvfi_insn_SB):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_bne, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_bne, self).ports()
|
||||
"""
|
||||
BNE instruction
|
||||
"""
|
||||
|
||||
class InsnBne(InsnRV32ISBType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b001)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_bne, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# BNE instruction
|
||||
cond = Signal(1)
|
||||
m.d.comb += cond.eq(self.rvfi_rs1_rdata != self.rvfi_rs2_rdata)
|
||||
next_pc = Signal(32)
|
||||
m.d.comb += next_pc.eq(Mux(cond, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4))
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == 0b001) & (self.insn_opcode == 0b1100011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
next_pc = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += next_pc.eq(Mux(self.rvfi_rs1_rdata != self.rvfi_rs2_rdata, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4))
|
||||
m.d.comb += self.spec_pc_wdata.eq(next_pc)
|
||||
m.d.comb += self.spec_trap.eq(Mux(self.ialign16, next_pc[0] != 0, next_pc[:2] != 0) | ~self.misa_ok)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,23 +0,0 @@
|
|||
from insn_R import *
|
||||
|
||||
class rvfi_insn_div(rvfi_insn_R):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_div, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_div, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_div, self).elaborate(platform)
|
||||
|
||||
# DIV instruction
|
||||
altops_bitmask = Signal(32)
|
||||
m.d.comb += altops_bitmask.eq(0x29bbf66f7f8529ec)
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq((self.rvfi_rs1_rdata - self.rvfi_rs2_rdata) ^ altops_bitmask)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct7 == 0b0000001) & (self.insn_funct3 == 0b100) & (self.insn_opcode == 0b0110011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
|
||||
return m
|
||||
|
|
@ -1,23 +0,0 @@
|
|||
from insn_R import *
|
||||
|
||||
class rvfi_insn_divu(rvfi_insn_R):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_divu, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_divu, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_divu, self).elaborate(platform)
|
||||
|
||||
# DIVU instruction
|
||||
altops_bitmask = Signal(32)
|
||||
m.d.comb += altops_bitmask.eq(0x8c629acb10e8fd70)
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq((self.rvfi_rs1_rdata - self.rvfi_rs2_rdata) ^ altops_bitmask)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct7 == 0b0000001) & (self.insn_funct3 == 0b101) & (self.insn_opcode == 0b0110011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
|
||||
return m
|
||||
|
|
@ -1,16 +1,31 @@
|
|||
from insn_UJ import *
|
||||
from insn import *
|
||||
|
||||
class rvfi_insn_jal(rvfi_insn_UJ):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_jal, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_jal, self).ports()
|
||||
"""
|
||||
JAL instruction
|
||||
"""
|
||||
|
||||
class InsnJal(Insn):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
|
||||
self.RISCV_FORMAL_COMPRESSED = RISCV_FORMAL_COMPRESSED
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_jal, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# JAL instruction
|
||||
next_pc = Signal(32)
|
||||
m.d.comb += next_pc.eq(self.rvfi_pc_rdata + self.insn_imm)
|
||||
m.d.comb += self.insn_imm.eq(Value.as_signed(Cat(self.rvfi_insn[21:31], self.rvfi_insn[20], self.rvfi_insn[12:20], self.rvfi_insn[31]) << 1))
|
||||
|
||||
if self.RISCV_FORMAL_CSR_MISA:
|
||||
m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
|
||||
m.d.comb += self.spec_csr_misa_rmask.eq(4)
|
||||
m.d.comb += self.ialign16.eq((self.rvfi_csr_misa_rdata & 4) != 0)
|
||||
else:
|
||||
m.d.comb += self.misa_ok.eq(1)
|
||||
if self.RISCV_FORMAL_COMPRESSED:
|
||||
m.d.comb += self.ialign16.eq(1)
|
||||
else:
|
||||
m.d.comb += self.ialign16.eq(0)
|
||||
|
||||
next_pc = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += next_pc.eq(self.rvfi_rs1_rdata + self.insn_imm)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_opcode == 0b1101111))
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_pc_rdata + 4, 0))
|
||||
|
|
|
|||
|
|
@ -1,15 +1,28 @@
|
|||
from insn_I import *
|
||||
from insn_rv32i_i_type import *
|
||||
|
||||
class rvfi_insn_jalr(rvfi_insn_I):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_jalr, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_jalr, self).ports()
|
||||
"""
|
||||
JALR instruction
|
||||
"""
|
||||
|
||||
class InsnJalr(InsnRV32IIType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
|
||||
self.RISCV_FORMAL_COMPRESSED = RISCV_FORMAL_COMPRESSED
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_jalr, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# JALR instruction
|
||||
next_pc = Signal(32)
|
||||
if self.RISCV_FORMAL_CSR_MISA:
|
||||
m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
|
||||
m.d.comb += self.spec_csr_misa_rmask.eq(4)
|
||||
m.d.comb += self.ialign16.eq((self.rvfi_csr_misa_rdata & 4) != 0)
|
||||
else:
|
||||
m.d.comb += self.misa_ok.eq(1)
|
||||
if self.RISCV_FORMAL_COMPRESSED:
|
||||
m.d.comb += self.ialign16.eq(1)
|
||||
else:
|
||||
m.d.comb += self.ialign16.eq(0)
|
||||
|
||||
next_pc = Signal(self.RISCV_FORMAL_XLEN)
|
||||
m.d.comb += next_pc.eq((self.rvfi_rs1_rdata + self.insn_imm) & ~1)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == 0b000) & (self.insn_opcode == 0b1100111))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
|
|
|
|||
|
|
@ -1,25 +1,9 @@
|
|||
from insn_I import *
|
||||
from insn_rv32i_i_type_load import *
|
||||
|
||||
class rvfi_insn_lb(rvfi_insn_I):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_lb, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_lb, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_lb, self).elaborate(platform)
|
||||
"""
|
||||
LB instruction
|
||||
"""
|
||||
|
||||
# LB instruction
|
||||
addr = Signal(32)
|
||||
m.d.comb += addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
|
||||
result = Signal(8)
|
||||
m.d.comb += result.eq(self.rvfi_mem_rdata)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (self.insn_funct3 == 0b000) & (self.insn_opcode == 0b0000011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_mem_addr.eq(addr)
|
||||
m.d.comb += self.spec_mem_rmask.eq((1 << 1) - 1)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, Value.as_signed(result), 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_trap.eq(~self.misa_ok)
|
||||
|
||||
return m
|
||||
class InsnLb(InsnRV32IITypeLoad):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b000, 1, True)
|
||||
|
|
|
|||
|
|
@ -1,25 +1,9 @@
|
|||
from insn_I import *
|
||||
from insn_rv32i_i_type_load import *
|
||||
|
||||
class rvfi_insn_lbu(rvfi_insn_I):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_lbu, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_lbu, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_lbu, self).elaborate(platform)
|
||||
"""
|
||||
LBU instruction
|
||||
"""
|
||||
|
||||
# LBU instruction
|
||||
addr = Signal(32)
|
||||
m.d.comb += addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
|
||||
result = Signal(8)
|
||||
m.d.comb += result.eq(self.rvfi_mem_rdata)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (self.insn_funct3 == 0b100) & (self.insn_opcode == 0b0000011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_mem_addr.eq(addr)
|
||||
m.d.comb += self.spec_mem_rmask.eq((1 << 1) - 1)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_trap.eq(~self.misa_ok)
|
||||
|
||||
return m
|
||||
class InsnLbu(InsnRV32IITypeLoad):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b100, 1, False)
|
||||
|
|
|
|||
|
|
@ -1,25 +1,9 @@
|
|||
from insn_I import *
|
||||
from insn_rv32i_i_type_load import *
|
||||
|
||||
class rvfi_insn_lh(rvfi_insn_I):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_lh, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_lh, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_lh, self).elaborate(platform)
|
||||
"""
|
||||
LH instruction
|
||||
"""
|
||||
|
||||
# LH instruction
|
||||
addr = Signal(32)
|
||||
m.d.comb += addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
|
||||
result = Signal(16)
|
||||
m.d.comb += result.eq(self.rvfi_mem_rdata)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (self.insn_funct3 == 0b001) & (self.insn_opcode == 0b0000011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_mem_addr.eq(addr)
|
||||
m.d.comb += self.spec_mem_rmask.eq((1 << 2) - 1)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, Value.as_signed(result), 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_trap.eq(~self.misa_ok)
|
||||
|
||||
return m
|
||||
class InsnLh(InsnRV32IITypeLoad):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b001, 2, True)
|
||||
|
|
|
|||
|
|
@ -1,25 +1,9 @@
|
|||
from insn_I import *
|
||||
from insn_rv32i_i_type_load import *
|
||||
|
||||
class rvfi_insn_lhu(rvfi_insn_I):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_lhu, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_lhu, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_lhu, self).elaborate(platform)
|
||||
"""
|
||||
LHU instruction
|
||||
"""
|
||||
|
||||
# LHU instruction
|
||||
addr = Signal(32)
|
||||
m.d.comb += addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
|
||||
result = Signal(16)
|
||||
m.d.comb += result.eq(self.rvfi_mem_rdata)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (self.insn_funct3 == 0b101) & (self.insn_opcode == 0b0000011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_mem_addr.eq(addr)
|
||||
m.d.comb += self.spec_mem_rmask.eq((1 << 2) - 1)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_trap.eq(~self.misa_ok)
|
||||
|
||||
return m
|
||||
class InsnLhu(InsnRV32IITypeLoad):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b101, 2, False)
|
||||
|
|
|
|||
|
|
@ -1,17 +1,15 @@
|
|||
from insn_U import *
|
||||
from insn_rv32i_u_type import *
|
||||
|
||||
class rvfi_insn_lui(rvfi_insn_U):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_lui, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_lui, self).ports()
|
||||
"""
|
||||
LUI instruction
|
||||
"""
|
||||
|
||||
class InsnLui(InsnRV32IUType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0110111)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_lui, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# LUI instruction
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_opcode == 0b0110111))
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.insn_imm, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,25 +1,9 @@
|
|||
from insn_I import *
|
||||
from insn_rv32i_i_type_load import *
|
||||
|
||||
class rvfi_insn_lw(rvfi_insn_I):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_lw, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_lw, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_lw, self).elaborate(platform)
|
||||
"""
|
||||
LW instruction
|
||||
"""
|
||||
|
||||
# LW instruction
|
||||
addr = Signal(32)
|
||||
m.d.comb += addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq(self.rvfi_mem_rdata)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (self.insn_funct3 == 0b010) & (self.insn_opcode == 0b0000011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_mem_addr.eq(addr)
|
||||
m.d.comb += self.spec_mem_rmask.eq((1 << 4) - 1)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, Value.as_signed(result), 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_trap.eq(~self.misa_ok)
|
||||
|
||||
return m
|
||||
class InsnLw(InsnRV32IITypeLoad):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b010, 4, True)
|
||||
|
|
|
|||
|
|
@ -1,23 +0,0 @@
|
|||
from insn_R import *
|
||||
|
||||
class rvfi_insn_mul(rvfi_insn_R):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_mul, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_mul, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_mul, self).elaborate(platform)
|
||||
|
||||
# MUL instruction
|
||||
altops_bitmask = Signal(32)
|
||||
m.d.comb += altops_bitmask.eq(0x2cdf52a55876063e)
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq((self.rvfi_rs1_rdata + self.rvfi_rs2_rdata) ^ altops_bitmask)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct7 == 0b0000001) & (self.insn_funct3 == 0b000) & (self.insn_opcode == 0b0110011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
|
||||
return m
|
||||
|
|
@ -1,23 +0,0 @@
|
|||
from insn_R import *
|
||||
|
||||
class rvfi_insn_mulh(rvfi_insn_R):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_mulh, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_mulh, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_mulh, self).elaborate(platform)
|
||||
|
||||
# MULH instruction
|
||||
altops_bitmask = Signal(32)
|
||||
m.d.comb += altops_bitmask.eq(0x15d01651f6583fb7)
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq((self.rvfi_rs1_rdata + self.rvfi_rs2_rdata) ^ altops_bitmask)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct7 == 0b0000001) & (self.insn_funct3 == 0b001) & (self.insn_opcode == 0b0110011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
|
||||
return m
|
||||
|
|
@ -1,23 +0,0 @@
|
|||
from insn_R import *
|
||||
|
||||
class rvfi_insn_mulhsu(rvfi_insn_R):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_mulhsu, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_mulhsu, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_mulhsu, self).elaborate(platform)
|
||||
|
||||
# MULHSU instruction
|
||||
altops_bitmask = Signal(32)
|
||||
m.d.comb += altops_bitmask.eq(0xea3969edecfbe137)
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq((self.rvfi_rs1_rdata - self.rvfi_rs2_rdata) ^ altops_bitmask)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct7 == 0b0000001) & (self.insn_funct3 == 0b010) & (self.insn_opcode == 0b0110011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
|
||||
return m
|
||||
|
|
@ -1,23 +0,0 @@
|
|||
from insn_R import *
|
||||
|
||||
class rvfi_insn_mulhu(rvfi_insn_R):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_mulhu, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_mulhu, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_mulhu, self).elaborate(platform)
|
||||
|
||||
# MULHU instruction
|
||||
altops_bitmask = Signal(32)
|
||||
m.d.comb += altops_bitmask.eq(0xd13db50d949ce5e8)
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq((self.rvfi_rs1_rdata + self.rvfi_rs2_rdata) ^ altops_bitmask)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct7 == 0b0000001) & (self.insn_funct3 == 0b011) & (self.insn_opcode == 0b0110011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
|
||||
return m
|
||||
|
|
@ -1,21 +1,15 @@
|
|||
from insn_R import *
|
||||
from insn_rv32i_r_type import *
|
||||
|
||||
class rvfi_insn_or(rvfi_insn_R):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_or, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_or, self).ports()
|
||||
"""
|
||||
OR instruction
|
||||
"""
|
||||
|
||||
class InsnOr(InsnRV32IRType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b110, 0b0110011)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_or, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# OR instruction
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq(self.rvfi_rs1_rdata | self.rvfi_rs2_rdata)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct7 == 0b0000000) & (self.insn_funct3 == 0b110) & (self.insn_opcode == 0b0110011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata | self.rvfi_rs2_rdata, 0))
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,20 +1,15 @@
|
|||
from insn_I import *
|
||||
from insn_rv32i_i_type_arith import *
|
||||
|
||||
class rvfi_insn_ori(rvfi_insn_I):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_ori, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_ori, self).ports()
|
||||
"""
|
||||
ORI instruction
|
||||
"""
|
||||
|
||||
class InsnOri(InsnRV32IITypeArith):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b110)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_ori, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# ORI instruction
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq(self.rvfi_rs1_rdata | self.insn_imm)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == 0b110) & (self.insn_opcode == 0b0010011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata | self.insn_imm, 0))
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,23 +0,0 @@
|
|||
from insn_R import *
|
||||
|
||||
class rvfi_insn_rem(rvfi_insn_R):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_rem, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_rem, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_rem, self).elaborate(platform)
|
||||
|
||||
# REM instruction
|
||||
altops_bitmask = Signal(32)
|
||||
m.d.comb += altops_bitmask.eq(0xf5b7d8538da68fa5)
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq((self.rvfi_rs1_rdata - self.rvfi_rs2_rdata) ^ altops_bitmask)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct7 == 0b0000001) & (self.insn_funct3 == 0b110) & (self.insn_opcode == 0b0110011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
|
||||
return m
|
||||
|
|
@ -1,23 +0,0 @@
|
|||
from insn_R import *
|
||||
|
||||
class rvfi_insn_remu(rvfi_insn_R):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_remu, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_remu, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_remu, self).elaborate(platform)
|
||||
|
||||
# REMU instruction
|
||||
altops_bitmask = Signal(32)
|
||||
m.d.comb += altops_bitmask.eq(0xbc4402413138d0e1)
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq((self.rvfi_rs1_rdata - self.rvfi_rs2_rdata) ^ altops_bitmask)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct7 == 0b0000001) & (self.insn_funct3 == 0b111) & (self.insn_opcode == 0b0110011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
|
||||
return m
|
||||
|
|
@ -0,0 +1,13 @@
|
|||
from insn import *
|
||||
|
||||
"""
|
||||
RV32I I-Type Instruction
|
||||
"""
|
||||
|
||||
class InsnRV32IIType(Insn):
|
||||
def elaborate(self, platform):
|
||||
m = super().elaborate(platform)
|
||||
|
||||
m.d.comb += self.insn_imm.eq(Value.as_signed(self.rvfi_insn[20:32]))
|
||||
|
||||
return m
|
||||
|
|
@ -0,0 +1,25 @@
|
|||
from insn_rv32i_i_type import *
|
||||
|
||||
"""
|
||||
RV32I I-Type Instruction (Arithmetic Variation)
|
||||
"""
|
||||
|
||||
class InsnRV32IITypeArith(InsnRV32IIType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, funct3):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
|
||||
self.funct3 = funct3
|
||||
def elaborate(self, platform):
|
||||
m = super().elaborate(platform)
|
||||
|
||||
if self.RISCV_FORMAL_CSR_MISA:
|
||||
m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
|
||||
m.d.comb += self.spec_csr_misa_rmask.eq(0)
|
||||
else:
|
||||
m.d.comb += self.misa_ok.eq(1)
|
||||
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == self.funct3) & (self.insn_opcode == 0b0010011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
|
||||
return m
|
||||
|
|
@ -0,0 +1,48 @@
|
|||
from insn_rv32i_i_type import *
|
||||
|
||||
"""
|
||||
RV32I I-Type Instruction (Load Variation)
|
||||
"""
|
||||
|
||||
class InsnRV32IITypeLoad(InsnRV32IIType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, funct3, mask_shift, is_signed):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
|
||||
self.RISCV_FORMAL_ALIGNED_MEM = RISCV_FORMAL_ALIGNED_MEM
|
||||
self.funct3 = funct3
|
||||
self.mask_shift = mask_shift
|
||||
self.is_signed = is_signed
|
||||
self.addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
self.result = Signal(8 * self.mask_shift)
|
||||
def elaborate(self, platform):
|
||||
m = super().elaborate(platform)
|
||||
|
||||
if self.RISCV_FORMAL_CSR_MISA:
|
||||
m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
|
||||
m.d.comb += self.spec_csr_misa_rmask.eq(0)
|
||||
else:
|
||||
m.d.comb += self.misa_ok.eq(1)
|
||||
|
||||
if self.RISCV_FORMAL_ALIGNED_MEM:
|
||||
m.d.comb += self.addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
|
||||
m.d.comb += self.result.eq(self.rvfi_mem_rdata >> (8 * (self.addr - self.spec_mem_addr)))
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == self.funct3) & (self.insn_opcode == 0b0000011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_mem_addr.eq(self.addr & ~(int(self.RISCV_FORMAL_XLEN // 8) - 1))
|
||||
m.d.comb += self.spec_mem_rmask.eq(((1 << self.mask_shift) - 1) << (self.addr - self.spec_mem_addr))
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, Value.as_signed(self.result) if self.is_signed else self.result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_trap.eq(((self.addr & (self.mask_shift - 1)) != 0) | ~self.misa_ok)
|
||||
else:
|
||||
m.d.comb += self.addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
|
||||
m.d.comb += self.result.eq(self.rvfi_mem_rdata)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (self.insn_funct3 == self.funct3) & (self.insn_opcode == 0b0000011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_mem_addr.eq(self.addr)
|
||||
m.d.comb += self.spec_mem_rmask.eq((1 << self.mask_shift) - 1)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, Value.as_signed(self.result) if self.is_signed else self.result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_trap.eq(~self.misa_ok)
|
||||
|
||||
return m
|
||||
|
|
@ -0,0 +1,26 @@
|
|||
from insn import *
|
||||
|
||||
"""
|
||||
RV32I I-Type Instruction (Shift Variation)
|
||||
"""
|
||||
|
||||
class InsnRV32IITypeShift(Insn):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, funct6, funct3):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
|
||||
self.funct6 = funct6
|
||||
self.funct3 = funct3
|
||||
def elaborate(self, platform):
|
||||
m = super().elaborate(platform)
|
||||
|
||||
if self.RISCV_FORMAL_CSR_MISA:
|
||||
m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
|
||||
m.d.comb += self.spec_csr_misa_rmask.eq(0)
|
||||
else:
|
||||
m.d.comb += self.misa_ok.eq(1)
|
||||
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct6 == self.funct6) & (self.insn_funct3 == self.funct3) & (self.insn_opcode == 0b0010011) & ((~self.insn_shamt[5]) | (self.RISCV_FORMAL_XLEN == 64)))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
|
||||
return m
|
||||
|
|
@ -0,0 +1,28 @@
|
|||
from insn import *
|
||||
|
||||
"""
|
||||
RV32I R-Type Instruction
|
||||
"""
|
||||
|
||||
class InsnRV32IRType(Insn):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, funct7, funct3, opcode):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
|
||||
self.funct7 = funct7
|
||||
self.funct3 = funct3
|
||||
self.opcode = opcode
|
||||
def elaborate(self, platform):
|
||||
m = super().elaborate(platform)
|
||||
|
||||
if self.RISCV_FORMAL_CSR_MISA:
|
||||
m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
|
||||
m.d.comb += self.spec_csr_misa_rmask.eq(0)
|
||||
else:
|
||||
m.d.comb += self.misa_ok.eq(1)
|
||||
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct7 == self.funct7) & (self.insn_funct3 == self.funct3) & (self.insn_opcode == self.opcode))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
|
||||
return m
|
||||
|
|
@ -0,0 +1,46 @@
|
|||
from insn import *
|
||||
|
||||
"""
|
||||
RV32I S-Type Instruction
|
||||
"""
|
||||
|
||||
class InsnRV32ISType(Insn):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, funct3, mask_shift):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
|
||||
self.RISCV_FORMAL_ALIGNED_MEM = RISCV_FORMAL_ALIGNED_MEM
|
||||
self.funct3 = funct3
|
||||
self.mask_shift = mask_shift
|
||||
self.addr = Signal(self.RISCV_FORMAL_XLEN)
|
||||
def elaborate(self, platform):
|
||||
m = super().elaborate(platform)
|
||||
|
||||
m.d.comb += self.insn_imm.eq(Value.as_signed(Cat(self.rvfi_insn[7:12], self.rvfi_insn[25:32])))
|
||||
|
||||
if self.RISCV_FORMAL_CSR_MISA:
|
||||
m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
|
||||
m.d.comb += self.spec_csr_misa_rmask.eq(0)
|
||||
else:
|
||||
m.d.comb += self.misa_ok.eq(1)
|
||||
|
||||
if self.RISCV_FORMAL_ALIGNED_MEM:
|
||||
m.d.comb += self.addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == self.funct3) & (self.insn_opcode == 0b0100011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_mem_addr.eq(self.addr & ~(int(self.RISCV_FORMAL_XLEN // 8) - 1))
|
||||
m.d.comb += self.spec_mem_wmask.eq(((1 << self.mask_shift) - 1) << (self.addr - self.spec_mem_addr))
|
||||
m.d.comb += self.spec_mem_wdata.eq(self.rvfi_rs2_rdata << (8 * (self.addr - self.spec_mem_addr)))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_trap.eq(((self.addr & (self.mask_shift - 1)) != 0) | ~self.misa_ok)
|
||||
else:
|
||||
m.d.comb += self.addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == self.funct3) & (self.insn_opcode == 0b0100011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_mem_addr.eq(self.addr)
|
||||
m.d.comb += self.spec_mem_wmask.eq((1 << self.mask_shift) - 1)
|
||||
m.d.comb += self.spec_mem_wdata.eq(self.rvfi_rs2_rdata)
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_trap.eq(~self.misa_ok)
|
||||
|
||||
return m
|
||||
|
|
@ -0,0 +1,32 @@
|
|||
from insn import *
|
||||
|
||||
"""
|
||||
RV32I SB-Type Instruction
|
||||
"""
|
||||
|
||||
class InsnRV32ISBType(Insn):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, funct3):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
|
||||
self.RISCV_FORMAL_COMPRESSED = RISCV_FORMAL_COMPRESSED
|
||||
self.funct3 = funct3
|
||||
def elaborate(self, platform):
|
||||
m = super().elaborate(platform)
|
||||
|
||||
m.d.comb += self.insn_imm.eq(Value.as_signed(Cat(self.rvfi_insn[8:12], self.rvfi_insn[25:31], self.rvfi_insn[7], self.rvfi_insn[31]) << 1))
|
||||
|
||||
if self.RISCV_FORMAL_CSR_MISA:
|
||||
m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
|
||||
m.d.comb += self.spec_csr_misa_rmask.eq(4)
|
||||
m.d.comb += self.ialign16.eq((self.rvfi_csr_misa_rdata & 4) != 0)
|
||||
else:
|
||||
m.d.comb += self.misa_ok.eq(1)
|
||||
if self.RISCV_FORMAL_COMPRESSED:
|
||||
m.d.comb += self.ialign16.eq(1)
|
||||
else:
|
||||
m.d.comb += self.ialign16.eq(0)
|
||||
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == self.funct3) & (self.insn_opcode == 0b1100011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
|
||||
return m
|
||||
|
|
@ -0,0 +1,26 @@
|
|||
from insn import *
|
||||
|
||||
"""
|
||||
RV32I U-Type Instruction
|
||||
"""
|
||||
|
||||
class InsnRV32IUType(Insn):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, opcode):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
|
||||
self.opcode = opcode
|
||||
def elaborate(self, platform):
|
||||
m = super().elaborate(platform)
|
||||
|
||||
m.d.comb += self.insn_imm.eq(Value.as_signed(self.rvfi_insn[12:32] << 12))
|
||||
|
||||
if self.RISCV_FORMAL_CSR_MISA:
|
||||
m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
|
||||
m.d.comb += self.spec_csr_misa_rmask.eq(0)
|
||||
else:
|
||||
m.d.comb += self.misa_ok.eq(1)
|
||||
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_opcode == self.opcode))
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
|
||||
return m
|
||||
|
|
@ -1,23 +1,9 @@
|
|||
from insn_S import *
|
||||
from insn_rv32i_s_type import *
|
||||
|
||||
class rvfi_insn_sb(rvfi_insn_S):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_sb, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_sb, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_sb, self).elaborate(platform)
|
||||
"""
|
||||
SB instruction
|
||||
"""
|
||||
|
||||
# SB instruction
|
||||
addr = Signal(32)
|
||||
m.d.comb += addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == 0b000) & (self.insn_opcode == 0b0100011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_mem_addr.eq(addr)
|
||||
m.d.comb += self.spec_mem_wmask.eq((1 << 1) - 1)
|
||||
m.d.comb += self.spec_mem_wdata.eq(self.rvfi_rs2_rdata)
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_trap.eq(~self.misa_ok)
|
||||
|
||||
return m
|
||||
class InsnSb(InsnRV32ISType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b000, 1)
|
||||
|
|
|
|||
|
|
@ -1,23 +1,9 @@
|
|||
from insn_S import *
|
||||
from insn_rv32i_s_type import *
|
||||
|
||||
class rvfi_insn_sh(rvfi_insn_S):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_sh, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_sh, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_sh, self).elaborate(platform)
|
||||
"""
|
||||
SH instruction
|
||||
"""
|
||||
|
||||
# SH instruction
|
||||
addr = Signal(32)
|
||||
m.d.comb += addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == 0b001) & (self.insn_opcode == 0b0100011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_mem_addr.eq(addr)
|
||||
m.d.comb += self.spec_mem_wmask.eq((1 << 2) - 1)
|
||||
m.d.comb += self.spec_mem_wdata.eq(self.rvfi_rs2_rdata)
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_trap.eq(~self.misa_ok)
|
||||
|
||||
return m
|
||||
class InsnSh(InsnRV32ISType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b001, 2)
|
||||
|
|
|
|||
|
|
@ -1,23 +1,15 @@
|
|||
from insn_R import *
|
||||
from insn_rv32i_r_type import *
|
||||
|
||||
class rvfi_insn_sll(rvfi_insn_R):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_sll, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_sll, self).ports()
|
||||
"""
|
||||
SLL instruction
|
||||
"""
|
||||
|
||||
class InsnSll(InsnRV32IRType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b001, 0b0110011)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_sll, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# SLL instruction
|
||||
shamt = Signal(6)
|
||||
m.d.comb += shamt.eq(self.rvfi_rs2_rdata[:5])
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq(self.rvfi_rs1_rdata << shamt)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct7 == 0b0000000) & (self.insn_funct3 == 0b001) & (self.insn_opcode == 0b0110011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata << Mux(self.RISCV_FORMAL_XLEN == 64, self.rvfi_rs2_rdata[:6], self.rvfi_rs2_rdata[:5]), 0))
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,20 +1,15 @@
|
|||
from insn_I_shift import *
|
||||
from insn_rv32i_i_type_shift import *
|
||||
|
||||
class rvfi_insn_slli(rvfi_insn_I_shift):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_slli, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_slli, self).ports()
|
||||
"""
|
||||
SLLI instruction
|
||||
"""
|
||||
|
||||
class InsnSlli(InsnRV32IITypeShift):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b000000, 0b001)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_slli, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# SLLI instruction
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq(self.rvfi_rs1_rdata << self.insn_shamt)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct6 == 0b000000) & (self.insn_funct3 == 0b001) & (self.insn_opcode == 0b0010011) & (~self.insn_shamt[5]))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata << self.insn_shamt, 0))
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,21 +1,15 @@
|
|||
from insn_R import *
|
||||
from insn_rv32i_r_type import *
|
||||
|
||||
class rvfi_insn_slt(rvfi_insn_R):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_slt, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_slt, self).ports()
|
||||
"""
|
||||
SLT instruction
|
||||
"""
|
||||
|
||||
class InsnSlt(InsnRV32IRType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b010, 0b0110011)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_slt, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# SLT instruction
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq(Value.as_signed(self.rvfi_rs1_rdata) < Value.as_signed(self.rvfi_rs2_rdata))
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct7 == 0b0000000) & (self.insn_funct3 == 0b010) & (self.insn_opcode == 0b0110011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, Value.as_signed(self.rvfi_rs1_rdata) < Value.as_signed(self.rvfi_rs2_rdata), 0))
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,20 +1,15 @@
|
|||
from insn_I import *
|
||||
from insn_rv32i_i_type_arith import *
|
||||
|
||||
class rvfi_insn_slti(rvfi_insn_I):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_slti, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_slti, self).ports()
|
||||
"""
|
||||
SLTI instruction
|
||||
"""
|
||||
|
||||
class InsnSlti(InsnRV32IITypeArith):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b010)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_slti, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# SLTI instruction
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq(Value.as_signed(self.rvfi_rs1_rdata) < Value.as_signed(self.insn_imm))
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == 0b010) & (self.insn_opcode == 0b0010011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, Value.as_signed(self.rvfi_rs1_rdata) < Value.as_signed(self.insn_imm), 0))
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,20 +1,15 @@
|
|||
from insn_I import *
|
||||
from insn_rv32i_i_type_arith import *
|
||||
|
||||
class rvfi_insn_sltiu(rvfi_insn_I):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_sltiu, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_sltiu, self).ports()
|
||||
"""
|
||||
SLTIU instruction
|
||||
"""
|
||||
|
||||
class InsnSltiu(InsnRV32IITypeArith):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b011)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_sltiu, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# SLTIU instruction
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq(self.rvfi_rs1_rdata < self.insn_imm)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == 0b011) & (self.insn_opcode == 0b0010011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata < self.insn_imm, 0))
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,21 +1,15 @@
|
|||
from insn_R import *
|
||||
from insn_rv32i_r_type import *
|
||||
|
||||
class rvfi_insn_sltu(rvfi_insn_R):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_sltu, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_sltu, self).ports()
|
||||
"""
|
||||
SLTU instruction
|
||||
"""
|
||||
|
||||
class InsnSltu(InsnRV32IRType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b011, 0b0110011)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_sltu, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# SLTU instruction
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq(self.rvfi_rs1_rdata < self.rvfi_rs2_rdata)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct7 == 0b0000000) & (self.insn_funct3 == 0b011) & (self.insn_opcode == 0b0110011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata < self.rvfi_rs2_rdata, 0))
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,23 +1,15 @@
|
|||
from insn_R import *
|
||||
from insn_rv32i_r_type import *
|
||||
|
||||
class rvfi_insn_sra(rvfi_insn_R):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_sra, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_sra, self).ports()
|
||||
"""
|
||||
SRA instruction
|
||||
"""
|
||||
|
||||
class InsnSra(InsnRV32IRType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0100000, 0b101, 0b0110011)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_sra, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# SRA instruction
|
||||
shamt = Signal(6)
|
||||
m.d.comb += shamt.eq(self.rvfi_rs2_rdata[:5])
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq((self.rvfi_rs1_rdata >> shamt) | (-(self.rvfi_rs1_rdata < 0) << (32 - shamt))) # https://stackoverflow.com/a/25207042
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct7 == 0b0100000) & (self.insn_funct3 == 0b101) & (self.insn_opcode == 0b0110011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, (Value.as_signed(self.rvfi_rs1_rdata) >> Mux(self.RISCV_FORMAL_XLEN == 64, self.rvfi_rs2_rdata[:6], self.rvfi_rs2_rdata[:5])) | (-(Value.as_signed(self.rvfi_rs1_rdata) < 0) << (self.RISCV_FORMAL_XLEN - Mux(self.RISCV_FORMAL_XLEN == 64, self.rvfi_rs2_rdata[:6], self.rvfi_rs2_rdata[:5]))), 0)) # https://stackoverflow.com/a/25207042
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,20 +1,15 @@
|
|||
from insn_I_shift import *
|
||||
from insn_rv32i_i_type_shift import *
|
||||
|
||||
class rvfi_insn_srai(rvfi_insn_I_shift):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_srai, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_srai, self).ports()
|
||||
"""
|
||||
SRAI instruction
|
||||
"""
|
||||
|
||||
class InsnSrai(InsnRV32IITypeShift):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b010000, 0b101)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_srai, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# SRAI instruction
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq((self.rvfi_rs1_rdata >> self.insn_shamt) | (-(self.rvfi_rs1_rdata < 0) << (32 - self.insn_shamt))) # https://stackoverflow.com/a/25207042
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct6 == 0b010000) & (self.insn_funct3 == 0b101) & (self.insn_opcode == 0b0010011) & (~self.insn_shamt[5]))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, (Value.as_signed(self.rvfi_rs1_rdata) >> self.insn_shamt) | (-(Value.as_signed(self.rvfi_rs1_rdata) < 0) << (self.RISCV_FORMAL_XLEN - self.insn_shamt)), 0))
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,23 +1,15 @@
|
|||
from insn_R import *
|
||||
from insn_rv32i_r_type import *
|
||||
|
||||
class rvfi_insn_srl(rvfi_insn_R):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_srl, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_srl, self).ports()
|
||||
"""
|
||||
SRL instruction
|
||||
"""
|
||||
|
||||
class InsnSrl(InsnRV32IRType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b100, 0b0110011)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_srl, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# SRL instruction
|
||||
shamt = Signal(6)
|
||||
m.d.comb += shamt.eq(self.rvfi_rs2_rdata[:5])
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq(self.rvfi_rs1_rdata >> shamt)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct7 == 0b0000000) & (self.insn_funct3 == 0b101) & (self.insn_opcode == 0b0110011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata >> Mux(self.RISCV_FORMAL_XLEN == 64, self.rvfi_rs2_rdata[:6], self.rvfi_rs2_rdata[:5]), 0))
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,20 +1,15 @@
|
|||
from insn_I_shift import *
|
||||
from insn_rv32i_i_type_shift import *
|
||||
|
||||
class rvfi_insn_srli(rvfi_insn_I_shift):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_srli, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_srli, self).ports()
|
||||
"""
|
||||
SRLI instruction
|
||||
"""
|
||||
|
||||
class InsnSrli(InsnRV32IITypeShift):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b000000, 0b101)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_srli, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# SRLI instruction
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq(self.rvfi_rs1_rdata >> self.insn_shamt)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct6 == 0b000000) & (self.insn_funct3 == 0b101) & (self.insn_opcode == 0b0010011) & (~self.insn_shamt[5]))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata >> self.insn_shamt, 0))
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,21 +1,15 @@
|
|||
from insn_R import *
|
||||
from insn_rv32i_r_type import *
|
||||
|
||||
class rvfi_insn_sub(rvfi_insn_R):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_sub, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_sub, self).ports()
|
||||
"""
|
||||
SUB instruction
|
||||
"""
|
||||
|
||||
class InsnSub(InsnRV32IRType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0100000, 0b000, 0b0110011)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_sub, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# SUB instruction
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq(self.rvfi_rs1_rdata - self.rvfi_rs2_rdata)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct7 == 0b0100000) & (self.insn_funct3 == 0b000) & (self.insn_opcode == 0b0110011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata - self.rvfi_rs2_rdata, 0))
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,23 +1,9 @@
|
|||
from insn_S import *
|
||||
from insn_rv32i_s_type import *
|
||||
|
||||
class rvfi_insn_sw(rvfi_insn_S):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_sw, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_sw, self).ports()
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_sw, self).elaborate(platform)
|
||||
"""
|
||||
SW instruction
|
||||
"""
|
||||
|
||||
# SW instruction
|
||||
addr = Signal(32)
|
||||
m.d.comb += addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == 0b010) & (self.insn_opcode == 0b0100011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_mem_addr.eq(addr)
|
||||
m.d.comb += self.spec_mem_wmask.eq((1 << 4) - 1)
|
||||
m.d.comb += self.spec_mem_wdata.eq(self.rvfi_rs2_rdata)
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_trap.eq(~self.misa_ok)
|
||||
|
||||
return m
|
||||
class InsnSw(InsnRV32ISType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b010, 4)
|
||||
|
|
|
|||
|
|
@ -1,11 +0,0 @@
|
|||
# RV32IM Instruction Types
|
||||
|
||||
| Instruction type | Instructions |
|
||||
| --- | --- |
|
||||
| U-type | lui, auipc |
|
||||
| UJ-type | jal |
|
||||
| I-type | jalr, lb, lh, lw, lbu, lhu, addi, slti, sltiu, xori, ori, andi |
|
||||
| SB-type | beq, bne, blt, bge, bltu, bgeu |
|
||||
| S-type | sb, sh, sw |
|
||||
| I-type (shift variation) | slli, srli, srai |
|
||||
| R-type | add, sub, sll, slt, sltu, xor, srl, sra, or, and, mul, mulh, mulhsu, mulhu, div, divu, rem, remu |
|
||||
|
|
@ -1,21 +1,15 @@
|
|||
from insn_R import *
|
||||
from insn_rv32i_r_type import *
|
||||
|
||||
class rvfi_insn_xor(rvfi_insn_R):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_xor, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_xor, self).ports()
|
||||
"""
|
||||
XOR instruction
|
||||
"""
|
||||
|
||||
class InsnXor(InsnRV32IRType):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b100, 0b0110011)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_xor, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# XOR instruction
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq(self.rvfi_rs1_rdata ^ self.rvfi_rs2_rdata)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct7 == 0b0000000) & (self.insn_funct3 == 0b100) & (self.insn_opcode == 0b0110011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata ^ self.rvfi_rs2_rdata, 0))
|
||||
|
||||
return m
|
||||
|
|
|
|||
|
|
@ -1,20 +1,15 @@
|
|||
from insn_I import *
|
||||
from insn_rv32i_i_type_arith import *
|
||||
|
||||
class rvfi_insn_xori(rvfi_insn_I):
|
||||
def __init__(self):
|
||||
super(rvfi_insn_xori, self).__init__()
|
||||
def ports(self):
|
||||
return super(rvfi_insn_xori, self).ports()
|
||||
"""
|
||||
XORI instruction
|
||||
"""
|
||||
|
||||
class InsnXori(InsnRV32IITypeArith):
|
||||
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
|
||||
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b100)
|
||||
def elaborate(self, platform):
|
||||
m = super(rvfi_insn_xori, self).elaborate(platform)
|
||||
m = super().elaborate(platform)
|
||||
|
||||
# XORI instruction
|
||||
result = Signal(32)
|
||||
m.d.comb += result.eq(self.rvfi_rs1_rdata ^ self.insn_imm)
|
||||
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == 0b100) & (self.insn_opcode == 0b0010011))
|
||||
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
|
||||
m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, result, 0))
|
||||
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
|
||||
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata ^ self.insn_imm, 0))
|
||||
|
||||
return m
|
||||
|
|
|
|||
1228
insns/isa_rv32i.py
1228
insns/isa_rv32i.py
File diff suppressed because it is too large
Load Diff
|
|
@ -1,37 +0,0 @@
|
|||
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
|
||||
|
|
@ -1,107 +0,0 @@
|
|||
with open('isa_rv32i.py', 'w') as isa_rv32i:
|
||||
def fprint(strng):
|
||||
print(strng, file=isa_rv32i)
|
||||
fprint("# Generated by isa_rv32i_gen.py")
|
||||
fprint("from nmigen import *")
|
||||
with open('isa_rv32i.txt', 'r') as isa_rv32i_txt_file:
|
||||
isa_rv32i_insns = isa_rv32i_txt_file.read().split('\n')[:-1]
|
||||
for isa_rv32i_insn in isa_rv32i_insns:
|
||||
fprint("from insn_%s import *" % isa_rv32i_insn)
|
||||
fprint("")
|
||||
fprint("class rvfi_isa_rv32i(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_rv32i_insn in isa_rv32i_insns:
|
||||
fprint(" spec_insn_%s_valid = Signal(1)" % isa_rv32i_insn)
|
||||
fprint(" spec_insn_%s_trap = Signal(1)" % isa_rv32i_insn)
|
||||
fprint(" spec_insn_%s_rs1_addr = Signal(5)" % isa_rv32i_insn)
|
||||
fprint(" spec_insn_%s_rs2_addr = Signal(5)" % isa_rv32i_insn)
|
||||
fprint(" spec_insn_%s_rd_addr = Signal(5)" % isa_rv32i_insn)
|
||||
fprint(" spec_insn_%s_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)" % isa_rv32i_insn)
|
||||
fprint(" spec_insn_%s_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)" % isa_rv32i_insn)
|
||||
fprint(" spec_insn_%s_mem_addr = Signal(self.RISCV_FORMAL_XLEN)" % isa_rv32i_insn)
|
||||
fprint(" spec_insn_%s_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))" % isa_rv32i_insn)
|
||||
fprint(" spec_insn_%s_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))" % isa_rv32i_insn)
|
||||
fprint(" spec_insn_%s_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)" % isa_rv32i_insn)
|
||||
fprint(" m.submodules.insn_%s = insn_%s = rvfi_insn_%s()" % (isa_rv32i_insn, isa_rv32i_insn, isa_rv32i_insn))
|
||||
fprint(" m.d.comb += insn_%s.rvfi_valid.eq(self.rvfi_valid)" % isa_rv32i_insn)
|
||||
fprint(" m.d.comb += insn_%s.rvfi_insn.eq(self.rvfi_insn)" % isa_rv32i_insn)
|
||||
fprint(" m.d.comb += insn_%s.rvfi_pc_rdata.eq(self.rvfi_pc_rdata)" % isa_rv32i_insn)
|
||||
fprint(" m.d.comb += insn_%s.rvfi_rs1_rdata.eq(self.rvfi_rs1_rdata)" % isa_rv32i_insn)
|
||||
fprint(" m.d.comb += insn_%s.rvfi_rs2_rdata.eq(self.rvfi_rs2_rdata)" % isa_rv32i_insn)
|
||||
fprint(" m.d.comb += insn_%s.rvfi_mem_rdata.eq(self.rvfi_mem_rdata)" % isa_rv32i_insn)
|
||||
fprint(" m.d.comb += spec_insn_%s_valid.eq(insn_%s.spec_valid)" % (isa_rv32i_insn, isa_rv32i_insn))
|
||||
fprint(" m.d.comb += spec_insn_%s_trap.eq(insn_%s.spec_trap)" % (isa_rv32i_insn, isa_rv32i_insn))
|
||||
fprint(" m.d.comb += spec_insn_%s_rs1_addr.eq(insn_%s.spec_rs1_addr)" % (isa_rv32i_insn, isa_rv32i_insn))
|
||||
fprint(" m.d.comb += spec_insn_%s_rs2_addr.eq(insn_%s.spec_rs2_addr)" % (isa_rv32i_insn, isa_rv32i_insn))
|
||||
fprint(" m.d.comb += spec_insn_%s_rd_addr.eq(insn_%s.spec_rd_addr)" % (isa_rv32i_insn, isa_rv32i_insn))
|
||||
fprint(" m.d.comb += spec_insn_%s_rd_wdata.eq(insn_%s.spec_rd_wdata)" % (isa_rv32i_insn, isa_rv32i_insn))
|
||||
fprint(" m.d.comb += spec_insn_%s_pc_wdata.eq(insn_%s.spec_pc_wdata)" % (isa_rv32i_insn, isa_rv32i_insn))
|
||||
fprint(" m.d.comb += spec_insn_%s_mem_addr.eq(insn_%s.spec_mem_addr)" % (isa_rv32i_insn, isa_rv32i_insn))
|
||||
fprint(" m.d.comb += spec_insn_%s_mem_rmask.eq(insn_%s.spec_mem_rmask)" % (isa_rv32i_insn, isa_rv32i_insn))
|
||||
fprint(" m.d.comb += spec_insn_%s_mem_wmask.eq(insn_%s.spec_mem_wmask)" % (isa_rv32i_insn, isa_rv32i_insn))
|
||||
fprint(" m.d.comb += spec_insn_%s_mem_wdata.eq(insn_%s.spec_mem_wdata)" % (isa_rv32i_insn, isa_rv32i_insn))
|
||||
fprint("")
|
||||
def gen_spec(strng):
|
||||
result = "0"
|
||||
for isa_rv32i_insn in isa_rv32i_insns:
|
||||
result = "Mux(spec_insn_%s_valid, spec_insn_%s_%s, %s)" % (isa_rv32i_insn, isa_rv32i_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")
|
||||
1459
insns/isa_rv32im.py
1459
insns/isa_rv32im.py
File diff suppressed because it is too large
Load Diff
|
|
@ -1,45 +0,0 @@
|
|||
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
|
||||
|
|
@ -1,107 +0,0 @@
|
|||
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")
|
||||
Loading…
Reference in New Issue