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

Begin re-organization of project structure

Browse Source
This commit is contained in:
Donald Sebastian Leung 2020-08-06 12:36:01 +08:00
parent 1d315b4735
commit 3eaed129c2
74 changed files with 1 additions and 5438 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
README.md
View File

@ -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

81
checks/rvfi_causal_check.py
View File

@ -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

103
checks/rvfi_channel.py
View File

@ -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

82
checks/rvfi_dmem_check.py
View File

@ -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

77
checks/rvfi_hang_check.py
View File

@ -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

109
checks/rvfi_ill_check.py
View File

@ -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

88
checks/rvfi_imem_check.py
View File

@ -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

205
checks/rvfi_insn_check.py
View File

@ -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

79
checks/rvfi_liveness_check.py
View File

@ -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

82
checks/rvfi_pc_bwd_check.py
View File

@ -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

82
checks/rvfi_pc_fwd_check.py
View File

@ -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

84
checks/rvfi_reg_check.py
View File

@ -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

78
checks/rvfi_unique_check.py
View File

@ -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

28
insns/README.md
View File

@ -1,28 +0,0 @@
# 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\*.
| 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 |
\* 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.
## Caveats
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:
| 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 |

51
insns/insn.py
View File

@ -1,51 +0,0 @@
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)
# Output ports
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)
def ports(self):
input_ports = [
self.rvfi_valid,
self.rvfi_insn,
self.rvfi_pc_rdata,
self.rvfi_rs1_rdata,
self.rvfi_rs2_rdata,
self.rvfi_mem_rdata
]
output_ports = [
self.spec_valid,
self.spec_trap,
self.spec_rs1_addr,
self.spec_rs2_addr,
self.spec_rd_addr,
self.spec_rd_wdata,
self.spec_pc_wdata,
self.spec_mem_addr,
self.spec_mem_rmask,
self.spec_mem_wmask,
self.spec_mem_wdata
]
return input_ports + output_ports
def elaborate(self, platform):
m = Module()
return m

38
insns/insn_I.py
View File

@ -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

38
insns/insn_I_shift.py
View File

@ -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

37
insns/insn_R.py
View File

@ -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

32
insns/insn_S.py
View File

@ -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

38
insns/insn_SB.py
View File

@ -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

33
insns/insn_U.py
View File

@ -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

34
insns/insn_UJ.py
View File

@ -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

21
insns/insn_add.py
View File

@ -1,21 +0,0 @@
from insn_R 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()
def elaborate(self, platform):
m = super(rvfi_insn_add, self).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)
return m

20
insns/insn_addi.py
View File

@ -1,20 +0,0 @@
from insn_I 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()
def elaborate(self, platform):
m = super(rvfi_insn_addi, self).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)
return m

21
insns/insn_and.py
View File

@ -1,21 +0,0 @@
from insn_R 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()
def elaborate(self, platform):
m = super(rvfi_insn_and, self).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)
return m

20
insns/insn_andi.py
View File

@ -1,20 +0,0 @@
from insn_I 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()
def elaborate(self, platform):
m = super(rvfi_insn_andi, self).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)
return m

17
insns/insn_auipc.py
View File

@ -1,17 +0,0 @@
from insn_U 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()
def elaborate(self, platform):
m = super(rvfi_insn_auipc, self).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

22
insns/insn_beq.py
View File

@ -1,22 +0,0 @@
from insn_SB 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()
def elaborate(self, platform):
m = super(rvfi_insn_beq, self).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)
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)
return m

22
insns/insn_bge.py
View File

@ -1,22 +0,0 @@
from insn_SB 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()
def elaborate(self, platform):
m = super(rvfi_insn_bge, self).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)
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)
return m

22
insns/insn_bgeu.py
View File

@ -1,22 +0,0 @@
from insn_SB 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()
def elaborate(self, platform):
m = super(rvfi_insn_bgeu, self).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)
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)
return m

22
insns/insn_blt.py
View File

@ -1,22 +0,0 @@
from insn_SB 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()
def elaborate(self, platform):
m = super(rvfi_insn_blt, self).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)
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)
return m

22
insns/insn_bltu.py
View File

@ -1,22 +0,0 @@
from insn_SB 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()
def elaborate(self, platform):
m = super(rvfi_insn_bltu, self).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)
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)
return m

22
insns/insn_bne.py
View File

@ -1,22 +0,0 @@
from insn_SB 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()
def elaborate(self, platform):
m = super(rvfi_insn_bne, self).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)
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)
return m

23
insns/insn_div.py
View File

@ -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

23
insns/insn_divu.py
View File

@ -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

20
insns/insn_jal.py
View File

@ -1,20 +0,0 @@
from insn_UJ 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()
def elaborate(self, platform):
m = super(rvfi_insn_jal, self).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.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))
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)
return m

21
insns/insn_jalr.py
View File

@ -1,21 +0,0 @@
from insn_I 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()
def elaborate(self, platform):
m = super(rvfi_insn_jalr, self).elaborate(platform)
# JALR instruction
next_pc = Signal(32)
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)
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))
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)
return m

25
insns/insn_lb.py
View File

@ -1,25 +0,0 @@
from insn_I 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
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

25
insns/insn_lbu.py
View File

@ -1,25 +0,0 @@
from insn_I 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
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

25
insns/insn_lh.py
View File

@ -1,25 +0,0 @@
from insn_I 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
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

25
insns/insn_lhu.py
View File

@ -1,25 +0,0 @@
from insn_I 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
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

17
insns/insn_lui.py
View File

@ -1,17 +0,0 @@
from insn_U 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()
def elaborate(self, platform):
m = super(rvfi_insn_lui, self).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

25
insns/insn_lw.py
View File

@ -1,25 +0,0 @@
from insn_I 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
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

23
insns/insn_mul.py
View File

@ -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

23
insns/insn_mulh.py
View File

@ -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

23
insns/insn_mulhsu.py
View File

@ -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

23
insns/insn_mulhu.py
View File

@ -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

21
insns/insn_or.py
View File

@ -1,21 +0,0 @@
from insn_R 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()
def elaborate(self, platform):
m = super(rvfi_insn_or, self).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)
return m

20
insns/insn_ori.py
View File

@ -1,20 +0,0 @@
from insn_I 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()
def elaborate(self, platform):
m = super(rvfi_insn_ori, self).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)
return m

23
insns/insn_rem.py
View File

@ -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

23
insns/insn_remu.py
View File

@ -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

23
insns/insn_sb.py
View File

@ -1,23 +0,0 @@
from insn_S 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
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

23
insns/insn_sh.py
View File

@ -1,23 +0,0 @@
from insn_S 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
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

23
insns/insn_sll.py
View File

@ -1,23 +0,0 @@
from insn_R 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()
def elaborate(self, platform):
m = super(rvfi_insn_sll, self).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)
return m

20
insns/insn_slli.py
View File

@ -1,20 +0,0 @@
from insn_I_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()
def elaborate(self, platform):
m = super(rvfi_insn_slli, self).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)
return m

21
insns/insn_slt.py
View File

@ -1,21 +0,0 @@
from insn_R 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()
def elaborate(self, platform):
m = super(rvfi_insn_slt, self).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)
return m

20
insns/insn_slti.py
View File

@ -1,20 +0,0 @@
from insn_I 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()
def elaborate(self, platform):
m = super(rvfi_insn_slti, self).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)
return m

20
insns/insn_sltiu.py
View File

@ -1,20 +0,0 @@
from insn_I 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()
def elaborate(self, platform):
m = super(rvfi_insn_sltiu, self).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)
return m

21
insns/insn_sltu.py
View File

@ -1,21 +0,0 @@
from insn_R 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()
def elaborate(self, platform):
m = super(rvfi_insn_sltu, self).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)
return m

23
insns/insn_sra.py
View File

@ -1,23 +0,0 @@
from insn_R 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()
def elaborate(self, platform):
m = super(rvfi_insn_sra, self).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)
return m

20
insns/insn_srai.py
View File

@ -1,20 +0,0 @@
from insn_I_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()
def elaborate(self, platform):
m = super(rvfi_insn_srai, self).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)
return m

23
insns/insn_srl.py
View File

@ -1,23 +0,0 @@
from insn_R 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()
def elaborate(self, platform):
m = super(rvfi_insn_srl, self).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)
return m

20
insns/insn_srli.py
View File

@ -1,20 +0,0 @@
from insn_I_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()
def elaborate(self, platform):
m = super(rvfi_insn_srli, self).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)
return m

21
insns/insn_sub.py
View File

@ -1,21 +0,0 @@
from insn_R 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()
def elaborate(self, platform):
m = super(rvfi_insn_sub, self).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)
return m

23
insns/insn_sw.py
View File

@ -1,23 +0,0 @@
from insn_S 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
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

11
insns/insn_types.md
View File

@ -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 |

21
insns/insn_xor.py
View File

@ -1,21 +0,0 @@
from insn_R 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()
def elaborate(self, platform):
m = super(rvfi_insn_xor, self).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)
return m

20
insns/insn_xori.py
View File

@ -1,20 +0,0 @@
from insn_I 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()
def elaborate(self, platform):
m = super(rvfi_insn_xori, self).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)
return m

1211
insns/isa_rv32i.py
View File

File diff suppressed because it is too large Load Diff

37
insns/isa_rv32i.txt
View File

@ -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

107
insns/isa_rv32i_gen.py
View File

@ -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
View File

File diff suppressed because it is too large Load Diff

45
insns/isa_rv32im.txt
View File

@ -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

107
insns/isa_rv32im_gen.py
View File

@ -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")