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

Compare commits

base: M-Labs:9e530bc7299e56b4721aa342562ed774e76c2662
Branches Tags
M-Labs:master
..
compare: M-Labs:1a38b37473c6b359661d02f4d3b4826fb535d15c
Branches Tags
M-Labs:master

No commits in common. "9e530bc7299e56b4721aa342562ed774e76c2662" and "1a38b37473c6b359661d02f4d3b4826fb535d15c" have entirely different histories.
9e530bc729 ... 1a38b37473

55 changed files with 1978 additions and 401 deletions
Show Stats Expand all files Collapse all files

4
README.md
View File

@ -4,14 +4,14 @@ A port of [riscv-formal](https://github.com/SymbioticEDA/riscv-formal) to nMigen
## Breakdown ## Breakdown
| File/Directory | Description | | Directory | Description |
| --- | --- | | --- | --- |
| `shell.nix` | [nix-shell](https://nixos.wiki/wiki/Development_environment_with_nix-shell) configuration file | | `shell.nix` | [nix-shell](https://nixos.wiki/wiki/Development_environment_with_nix-shell) configuration file |
| `rvfi` | RISC-V Formal Verification Framework (nMigen port) | | `rvfi` | RISC-V Formal Verification Framework (nMigen port) |
| `rvfi/insns` | Supported RISC-V instructions and ISAs | | `rvfi/insns` | Supported RISC-V instructions and ISAs |
| `rvfi/checks` | Checks for RISC-V compliant cores | | `rvfi/checks` | Checks for RISC-V compliant cores |
| `rvfi/cores` | Cores currently tested against this port of riscv-formal | | `rvfi/cores` | Cores currently tested against this port of riscv-formal |
| `rvfi/cores/minerva/verify.py` | Verification tasks for the Minerva core | | `rvfi/cores/minerva` | Tests for the Minerva core |
## Running the Verification ## Running the Verification

2
rvfi/checks/causal_check.py
View File

@ -15,7 +15,6 @@ class CausalCheck(Elaboratable):
self.rvfi_order = Signal(64) self.rvfi_order = Signal(64)
self.rvfi_rs1_addr = Signal(5) self.rvfi_rs1_addr = Signal(5)
self.rvfi_rs2_addr = Signal(5) self.rvfi_rs2_addr = Signal(5)
def ports(self): def ports(self):
input_ports = [ input_ports = [
self.reset, self.reset,
@ -27,7 +26,6 @@ class CausalCheck(Elaboratable):
self.rvfi_rs2_addr self.rvfi_rs2_addr
] ]
return input_ports return input_ports
def elaborate(self, platform): def elaborate(self, platform):
m = Module() m = Module()

137
rvfi/checks/insn_check.py
View File

@ -6,9 +6,13 @@ Instruction Check
""" """
class InsnCheck(Elaboratable): class InsnCheck(Elaboratable):
def __init__(self, params, insn_model, rvformal_addr_valid): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, RISCV_FORMAL_ALIGNED_MEM, insn_model, rvformal_addr_valid):
# Core-specific parameters # Core-specific constants
self.params = params self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN
self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
self.RISCV_FORMAL_CSR_MISA = RISCV_FORMAL_CSR_MISA
self.RISCV_FORMAL_COMPRESSED = RISCV_FORMAL_COMPRESSED
self.RISCV_FORMAL_ALIGNED_MEM = RISCV_FORMAL_ALIGNED_MEM
# Instruction under test # Instruction under test
self.insn_model = insn_model self.insn_model = insn_model
@ -22,7 +26,7 @@ class InsnCheck(Elaboratable):
self.check = Signal(1) self.check = Signal(1)
self.rvfi_valid = Signal(1) self.rvfi_valid = Signal(1)
self.rvfi_order = Signal(64) self.rvfi_order = Signal(64)
self.rvfi_insn = Signal(self.params.ilen) self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN)
self.rvfi_trap = Signal(1) self.rvfi_trap = Signal(1)
self.rvfi_halt = Signal(1) self.rvfi_halt = Signal(1)
self.rvfi_intr = Signal(1) self.rvfi_intr = Signal(1)
@ -30,23 +34,22 @@ class InsnCheck(Elaboratable):
self.rvfi_ixl = Signal(2) self.rvfi_ixl = Signal(2)
self.rvfi_rs1_addr = Signal(5) self.rvfi_rs1_addr = Signal(5)
self.rvfi_rs2_addr = Signal(5) self.rvfi_rs2_addr = Signal(5)
self.rvfi_rs1_rdata = Signal(self.params.xlen) self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
self.rvfi_rs2_rdata = Signal(self.params.xlen) self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
self.rvfi_rd_addr = Signal(5) self.rvfi_rd_addr = Signal(5)
self.rvfi_rd_wdata = Signal(self.params.xlen) self.rvfi_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
self.rvfi_pc_rdata = Signal(self.params.xlen) self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
self.rvfi_pc_wdata = Signal(self.params.xlen) self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
self.rvfi_mem_addr = Signal(self.params.xlen) self.rvfi_mem_addr = Signal(self.RISCV_FORMAL_XLEN)
self.rvfi_mem_rmask = Signal(int(self.params.xlen // 8)) self.rvfi_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
self.rvfi_mem_wmask = Signal(int(self.params.xlen // 8)) self.rvfi_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
self.rvfi_mem_rdata = Signal(self.params.xlen) self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN)
self.rvfi_mem_wdata = Signal(self.params.xlen) self.rvfi_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
self.rvfi_csr_misa_rmask = Signal(self.params.xlen) self.rvfi_csr_misa_rmask = Signal(self.RISCV_FORMAL_XLEN)
self.rvfi_csr_misa_wmask = Signal(self.params.xlen) self.rvfi_csr_misa_wmask = Signal(self.RISCV_FORMAL_XLEN)
self.rvfi_csr_misa_rdata = Signal(self.params.xlen) self.rvfi_csr_misa_rdata = Signal(self.RISCV_FORMAL_XLEN)
self.rvfi_csr_misa_wdata = Signal(self.params.xlen) self.rvfi_csr_misa_wdata = Signal(self.RISCV_FORMAL_XLEN)
def ports(self): def ports(self):
input_ports = [ input_ports = [
self.reset, self.reset,
@ -73,7 +76,7 @@ class InsnCheck(Elaboratable):
self.rvfi_mem_rdata, self.rvfi_mem_rdata,
self.rvfi_mem_wdata self.rvfi_mem_wdata
] ]
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
input_ports.extend([ input_ports.extend([
self.rvfi_csr_misa_rmask, self.rvfi_csr_misa_rmask,
self.rvfi_csr_misa_wmask, self.rvfi_csr_misa_wmask,
@ -81,54 +84,78 @@ class InsnCheck(Elaboratable):
self.rvfi_csr_misa_wdata self.rvfi_csr_misa_wdata
]) ])
return input_ports return input_ports
def elaborate(self, platform): def elaborate(self, platform):
m = Module() m = Module()
valid = Signal(1) valid = Signal(1)
m.d.comb += valid.eq((~self.reset) & self.rvfi_valid) m.d.comb += valid.eq((~self.reset) & self.rvfi_valid)
insn = self.rvfi_insn insn = Signal(self.RISCV_FORMAL_ILEN)
trap = self.rvfi_trap m.d.comb += insn.eq(self.rvfi_insn)
halt = self.rvfi_halt trap = Signal(1)
intr = self.rvfi_intr m.d.comb += trap.eq(self.rvfi_trap)
rs1_addr = self.rvfi_rs1_addr halt = Signal(1)
rs2_addr = self.rvfi_rs2_addr m.d.comb += halt.eq(self.rvfi_halt)
rs1_rdata = self.rvfi_rs1_rdata intr = Signal(1)
rs2_rdata = self.rvfi_rs2_rdata m.d.comb += intr.eq(self.rvfi_intr)
rd_addr = self.rvfi_rd_addr rs1_addr = Signal(5)
rd_wdata = self.rvfi_rd_wdata m.d.comb += rs1_addr.eq(self.rvfi_rs1_addr)
pc_rdata = self.rvfi_pc_rdata rs2_addr = Signal(5)
pc_wdata = self.rvfi_pc_wdata 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 = self.rvfi_mem_addr mem_addr = Signal(self.RISCV_FORMAL_XLEN)
mem_rmask = self.rvfi_mem_rmask m.d.comb += mem_addr.eq(self.rvfi_mem_addr)
mem_wmask = self.rvfi_mem_wmask mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
mem_rdata = self.rvfi_mem_rdata m.d.comb += mem_rmask.eq(self.rvfi_mem_rmask)
mem_wdata = self.rvfi_mem_wdata 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)
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
csr_misa_rdata = self.rvfi_csr_misa_rdata csr_misa_rdata = Signal(self.RISCV_FORMAL_XLEN)
csr_misa_rmask = self.rvfi_csr_misa_rmask m.d.comb += csr_misa_rdata.eq(self.rvfi_csr_misa_rdata)
spec_csr_misa_rmask = Signal(self.params.xlen) csr_misa_rmask = Signal(self.RISCV_FORMAL_XLEN)
m.d.comb += csr_misa_rmask.eq(self.rvfi_csr_misa_rmask)
spec_csr_misa_rmask = Signal(self.RISCV_FORMAL_XLEN)
spec_valid = Signal(1) spec_valid = Signal(1)
spec_trap = Signal(1) spec_trap = Signal(1)
spec_rs1_addr = Signal(5) spec_rs1_addr = Signal(5)
spec_rs2_addr = Signal(5) spec_rs2_addr = Signal(5)
spec_rd_addr = Signal(5) spec_rd_addr = Signal(5)
spec_rd_wdata = Signal(self.params.xlen) spec_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
spec_pc_wdata = Signal(self.params.xlen) spec_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
spec_mem_addr = Signal(self.params.xlen) spec_mem_addr = Signal(self.RISCV_FORMAL_XLEN)
spec_mem_rmask = Signal(int(self.params.xlen // 8)) spec_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
spec_mem_wmask = Signal(int(self.params.xlen // 8)) spec_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
spec_mem_wdata = Signal(self.params.xlen) spec_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
rs1_rdata_or_zero = Signal(self.params.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)) m.d.comb += rs1_rdata_or_zero.eq(Mux(spec_rs1_addr != 0, rs1_rdata, 0))
rs2_rdata_or_zero = Signal(self.params.xlen) 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)) m.d.comb += rs2_rdata_or_zero.eq(Mux(spec_rs2_addr != 0, rs2_rdata, 0))
m.submodules.insn_spec = insn_spec = self.insn_model(self.params) try:
m.submodules.insn_spec = insn_spec = self.insn_model(RISCV_FORMAL_ILEN=self.RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN=self.RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA=self.RISCV_FORMAL_CSR_MISA)
except:
try:
m.submodules.insn_spec = insn_spec = self.insn_model(RISCV_FORMAL_ILEN=self.RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN=self.RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA=self.RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED=self.RISCV_FORMAL_COMPRESSED)
except:
m.submodules.insn_spec = insn_spec = self.insn_model(RISCV_FORMAL_ILEN=self.RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN=self.RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA=self.RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM=self.RISCV_FORMAL_ALIGNED_MEM)
m.d.comb += insn_spec.rvfi_valid.eq(valid) m.d.comb += insn_spec.rvfi_valid.eq(valid)
m.d.comb += insn_spec.rvfi_insn.eq(insn) m.d.comb += insn_spec.rvfi_insn.eq(insn)
@ -137,7 +164,7 @@ class InsnCheck(Elaboratable):
m.d.comb += insn_spec.rvfi_rs2_rdata.eq(rs2_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 += insn_spec.rvfi_mem_rdata.eq(mem_rdata)
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
m.d.comb += insn_spec.rvfi_csr_misa_rdata.eq(csr_misa_rdata) m.d.comb += insn_spec.rvfi_csr_misa_rdata.eq(csr_misa_rdata)
m.d.comb += spec_csr_misa_rmask.eq(insn_spec.spec_csr_misa_rmask) m.d.comb += spec_csr_misa_rmask.eq(insn_spec.spec_csr_misa_rmask)
@ -181,7 +208,7 @@ class InsnCheck(Elaboratable):
m.d.comb += Assert(rd_wdata == 0) m.d.comb += Assert(rd_wdata == 0)
m.d.comb += Assert(mem_wmask == 0) m.d.comb += Assert(mem_wmask == 0)
with m.Else(): with m.Else():
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
m.d.comb += Assert((spec_csr_misa_rmask & csr_misa_rmask) == spec_csr_misa_rmask) m.d.comb += Assert((spec_csr_misa_rmask & csr_misa_rmask) == spec_csr_misa_rmask)
with m.If(rs1_addr == 0): with m.If(rs1_addr == 0):
@ -204,7 +231,7 @@ class InsnCheck(Elaboratable):
with m.If(spec_mem_wmask | spec_mem_rmask): with m.If(spec_mem_wmask | spec_mem_rmask):
m.d.comb += Assert(self.rvformal_addr_eq(spec_mem_addr, mem_addr)) m.d.comb += Assert(self.rvformal_addr_eq(spec_mem_addr, mem_addr))
for i in range(int(self.params.xlen // 8)): for i in range(int(self.RISCV_FORMAL_XLEN // 8)):
with m.If(spec_mem_wmask[i]): with m.If(spec_mem_wmask[i]):
m.d.comb += Assert(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]) m.d.comb += Assert(spec_mem_wdata[i*8:i*8+8] == mem_wdata[i*8:i*8+8])

16
rvfi/checks/pc_bwd_check.py
View File

@ -6,9 +6,9 @@ PC Backward Check
""" """
class PcBwdCheck(Elaboratable): class PcBwdCheck(Elaboratable):
def __init__(self, params, rvformal_addr_valid): def __init__(self, RISCV_FORMAL_XLEN, rvformal_addr_valid):
# Core-specific parameters # Core-specific constants
self.params = params self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
# Address validity and equality # Address validity and equality
self.rvformal_addr_valid = rvformal_addr_valid self.rvformal_addr_valid = rvformal_addr_valid
@ -19,9 +19,8 @@ class PcBwdCheck(Elaboratable):
self.check = Signal(1) self.check = Signal(1)
self.rvfi_valid = Signal(1) self.rvfi_valid = Signal(1)
self.rvfi_order = Signal(64) self.rvfi_order = Signal(64)
self.rvfi_pc_rdata = Signal(self.params.xlen) self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
self.rvfi_pc_wdata = Signal(self.params.xlen) self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
def ports(self): def ports(self):
input_ports = [ input_ports = [
self.reset, self.reset,
@ -32,15 +31,14 @@ class PcBwdCheck(Elaboratable):
self.rvfi_pc_wdata self.rvfi_pc_wdata
] ]
return input_ports return input_ports
def elaborate(self, platform): def elaborate(self, platform):
m = Module() m = Module()
insn_order = AnyConst(64) insn_order = AnyConst(64)
expect_pc = Signal(self.params.xlen) expect_pc = Signal(self.RISCV_FORMAL_XLEN)
expect_pc_valid = Signal(1, reset=0) expect_pc_valid = Signal(1, reset=0)
pc_wdata = Signal(self.params.xlen) pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
m.d.comb += pc_wdata.eq(self.rvfi_pc_wdata) m.d.comb += pc_wdata.eq(self.rvfi_pc_wdata)
with m.If(self.reset): with m.If(self.reset):

16
rvfi/checks/pc_fwd_check.py
View File

@ -6,9 +6,9 @@ PC Forward Check
""" """
class PcFwdCheck(Elaboratable): class PcFwdCheck(Elaboratable):
def __init__(self, params, rvformal_addr_valid): def __init__(self, RISCV_FORMAL_XLEN, rvformal_addr_valid):
# Core-specific parameters # Core-specific constants
self.params = params self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
# Address validity and equality # Address validity and equality
self.rvformal_addr_valid = rvformal_addr_valid self.rvformal_addr_valid = rvformal_addr_valid
@ -19,9 +19,8 @@ class PcFwdCheck(Elaboratable):
self.check = Signal(1) self.check = Signal(1)
self.rvfi_valid = Signal(1) self.rvfi_valid = Signal(1)
self.rvfi_order = Signal(64) self.rvfi_order = Signal(64)
self.rvfi_pc_rdata = Signal(self.params.xlen) self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
self.rvfi_pc_wdata = Signal(self.params.xlen) self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
def ports(self): def ports(self):
input_ports = [ input_ports = [
self.reset, self.reset,
@ -32,15 +31,14 @@ class PcFwdCheck(Elaboratable):
self.rvfi_pc_wdata self.rvfi_pc_wdata
] ]
return input_ports return input_ports
def elaborate(self, platform): def elaborate(self, platform):
m = Module() m = Module()
insn_order = AnyConst(64) insn_order = AnyConst(64)
expect_pc = Signal(self.params.xlen) expect_pc = Signal(self.RISCV_FORMAL_XLEN)
expect_pc_valid = Signal(1, reset=0) expect_pc_valid = Signal(1, reset=0)
pc_rdata = Signal(self.params.xlen) pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
m.d.comb += pc_rdata.eq(self.rvfi_pc_rdata) m.d.comb += pc_rdata.eq(self.rvfi_pc_rdata)
with m.If(self.reset): with m.If(self.reset):

16
rvfi/checks/reg_check.py
View File

@ -6,9 +6,9 @@ Register Check
""" """
class RegCheck(Elaboratable): class RegCheck(Elaboratable):
def __init__(self, params): def __init__(self, RISCV_FORMAL_XLEN):
# Core-specific parameters # Core-specific constants
self.params = params self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
# Input ports # Input ports
self.reset = Signal(1) self.reset = Signal(1)
@ -16,12 +16,11 @@ class RegCheck(Elaboratable):
self.rvfi_valid = Signal(1) self.rvfi_valid = Signal(1)
self.rvfi_order = Signal(64) self.rvfi_order = Signal(64)
self.rvfi_rs1_addr = Signal(5) self.rvfi_rs1_addr = Signal(5)
self.rvfi_rs1_rdata = Signal(self.params.xlen) self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
self.rvfi_rs2_addr = Signal(5) self.rvfi_rs2_addr = Signal(5)
self.rvfi_rs2_rdata = Signal(self.params.xlen) self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
self.rvfi_rd_addr = Signal(5) self.rvfi_rd_addr = Signal(5)
self.rvfi_rd_wdata = Signal(self.params.xlen) self.rvfi_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
def ports(self): def ports(self):
input_ports = [ input_ports = [
self.reset, self.reset,
@ -36,13 +35,12 @@ class RegCheck(Elaboratable):
self.rvfi_rd_wdata self.rvfi_rd_wdata
] ]
return input_ports return input_ports
def elaborate(self, platform): def elaborate(self, platform):
m = Module() m = Module()
insn_order = AnyConst(64) insn_order = AnyConst(64)
register_index = AnyConst(5) register_index = AnyConst(5)
register_shadow = Signal(self.params.xlen, reset=0) register_shadow = Signal(self.RISCV_FORMAL_XLEN, reset=0)
register_written = Signal(1, reset=0) register_written = Signal(1, reset=0)
with m.If(self.reset): with m.If(self.reset):

1700
rvfi/cores/minerva/verify.py
View File

File diff suppressed because it is too large Load Diff

18
rvfi/insns/README.md
View File

@ -89,14 +89,14 @@ Below is a list of instructions currently supported by this port of the riscv-fo
- `IsaRV32I`: RV32I Base ISA - `IsaRV32I`: RV32I Base ISA
## Core-specific parameters ## Core-specific constants
The following core-specific parameters are currently supported: The following core-specific constants are currently supported:
| Parameter | Description | Valid value(s) | | Constant | Description | Valid value(s) | Supported by instruction(s) | Supported by ISA(s) |
| --- | --- | --- | | --- | --- | --- | --- | --- |
| `params.ilen` | Max length of instruction retired by core | `32` | | `RISCV_FORMAL_ILEN` | Max length of instruction retired by core | `32` | LUI, AUIPC, JAL, JALR, BEQ, BNE, BLT, BGE, BLTU, BGEU, LB, LH, LW, LBU, LHU, SB, SH, SW, ADDI, SLTI, SLTIU, XORI, ORI, ANDI, SLLI, SRLI, SRAI, ADD, SUB, SLL, SLT, SLTU, XOR, SRL, SRA, OR, AND | RV32I |
| `params.xlen` | Width of integer registers | `32` | | `RISCV_FORMAL_XLEN` | Width of integer registers | `32` | LUI, AUIPC, JAL, JALR, BEQ, BNE, BLT, BGE, BLTU, BGEU, LB, LH, LW, LBU, LHU, SB, SH, SW, ADDI, SLTI, SLTIU, XORI, ORI, ANDI, SLLI, SRLI, SRAI, ADD, SUB, SLL, SLT, SLTU, XOR, SRL, SRA, OR, AND | RV32I |
| `params.csr_misa` | Support for MISA CSRs enabled | `True`, `False` | | `RISCV_FORMAL_CSR_MISA` | Support for MISA CSRs enabled | `True`, `False` | LUI, AUIPC, JAL, JALR, BEQ, BNE, BLT, BGE, BLTU, BGEU, LB, LH, LW, LBU, LHU, SB, SH, SW, ADDI, SLTI, SLTIU, XORI, ORI, ANDI, SLLI, SRLI, SRAI, ADD, SUB, SLL, SLT, SLTU, XOR, SRL, SRA, OR, AND | RV32I |
| `params.compressed` | Support for compressed instructions | `True`, `False` | | `RISCV_FORMAL_COMPRESSED` | Support for compressed instructions | `True`, `False` | JAL, JALR, BEQ, BNE, BLT, BGE, BLTU, BGEU | RV32I |
| `params.aligned_mem` | Require aligned memory accesses | `True`, `False` | | `RISCV_FORMAL_ALIGNED_MEM` | Require aligned memory accesses | `True`, `False` | LB, LH, LW, LBU, LHU, SB, SH, SW | RV32I |

51
rvfi/insns/insn.py
View File

@ -1,42 +1,45 @@
from nmigen import * from nmigen import *
""" """
General RISC-V Instruction Insn.py
Class for generic RISC-V instructions
""" """
class Insn(Elaboratable): class Insn(Elaboratable):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
# Core-specific parameters # Core-specific constants
self.params = params self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN
self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
self.RISCV_FORMAL_CSR_MISA = RISCV_FORMAL_CSR_MISA
# RVFI input ports # RVFI input ports
self.rvfi_valid = Signal(1) self.rvfi_valid = Signal(1)
self.rvfi_insn = Signal(self.params.ilen) self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN)
self.rvfi_pc_rdata = Signal(self.params.xlen) self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
self.rvfi_rs1_rdata = Signal(self.params.xlen) self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
self.rvfi_rs2_rdata = Signal(self.params.xlen) self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
self.rvfi_mem_rdata = Signal(self.params.xlen) self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN)
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
self.rvfi_csr_misa_rdata = Signal(self.params.xlen) self.rvfi_csr_misa_rdata = Signal(self.RISCV_FORMAL_XLEN)
# RVFI output ports # RVFI output ports
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
self.spec_csr_misa_rmask = Signal(self.params.xlen) self.spec_csr_misa_rmask = Signal(self.RISCV_FORMAL_XLEN)
self.spec_valid = Signal(1) self.spec_valid = Signal(1)
self.spec_trap = Signal(1) self.spec_trap = Signal(1)
self.spec_rs1_addr = Signal(5) self.spec_rs1_addr = Signal(5)
self.spec_rs2_addr = Signal(5) self.spec_rs2_addr = Signal(5)
self.spec_rd_addr = Signal(5) self.spec_rd_addr = Signal(5)
self.spec_rd_wdata = Signal(self.params.xlen) self.spec_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
self.spec_pc_wdata = Signal(self.params.xlen) self.spec_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
self.spec_mem_addr = Signal(self.params.xlen) self.spec_mem_addr = Signal(self.RISCV_FORMAL_XLEN)
self.spec_mem_rmask = Signal(int(self.params.xlen // 8)) self.spec_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
self.spec_mem_wmask = Signal(int(self.params.xlen // 8)) self.spec_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
self.spec_mem_wdata = Signal(self.params.xlen) self.spec_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
# Additional wires and registers # Additional wires and registers
self.insn_padding = Signal(self.params.ilen) self.insn_padding = Signal(self.RISCV_FORMAL_ILEN)
self.insn_imm = Signal(self.params.xlen) self.insn_imm = Signal(self.RISCV_FORMAL_XLEN)
self.insn_funct7 = Signal(7) self.insn_funct7 = Signal(7)
self.insn_funct6 = Signal(6) self.insn_funct6 = Signal(6)
self.insn_shamt = Signal(6) self.insn_shamt = Signal(6)
@ -47,7 +50,6 @@ class Insn(Elaboratable):
self.insn_opcode = Signal(7) self.insn_opcode = Signal(7)
self.misa_ok = Signal(1) self.misa_ok = Signal(1)
self.ialign16 = Signal(1) self.ialign16 = Signal(1)
def ports(self): def ports(self):
input_ports = [ input_ports = [
self.rvfi_valid, self.rvfi_valid,
@ -57,7 +59,7 @@ class Insn(Elaboratable):
self.rvfi_rs2_rdata, self.rvfi_rs2_rdata,
self.rvfi_mem_rdata self.rvfi_mem_rdata
] ]
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
input_ports.append(self.rvfi_csr_misa_rdata) input_ports.append(self.rvfi_csr_misa_rdata)
output_ports = [ output_ports = [
self.spec_valid, self.spec_valid,
@ -72,10 +74,9 @@ class Insn(Elaboratable):
self.spec_mem_wmask, self.spec_mem_wmask,
self.spec_mem_wdata self.spec_mem_wdata
] ]
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
output_ports.append(self.spec_csr_misa_rmask) output_ports.append(self.spec_csr_misa_rmask)
return input_ports + output_ports return input_ports + output_ports
def elaborate(self, platform): def elaborate(self, platform):
m = Module() m = Module()

5
rvfi/insns/insn_add.py
View File

@ -5,9 +5,8 @@ ADD instruction
""" """
class InsnAdd(InsnRV32IRType): class InsnAdd(InsnRV32IRType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b0000000, 0b000, 0b0110011) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b000, 0b0110011)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)

5
rvfi/insns/insn_addi.py
View File

@ -5,9 +5,8 @@ ADDI instruction
""" """
class InsnAddi(InsnRV32IITypeArith): class InsnAddi(InsnRV32IITypeArith):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b000) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b000)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)

5
rvfi/insns/insn_and.py
View File

@ -5,9 +5,8 @@ AND instruction
""" """
class InsnAnd(InsnRV32IRType): class InsnAnd(InsnRV32IRType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b0000000, 0b111, 0b0110011) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b111, 0b0110011)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)

5
rvfi/insns/insn_andi.py
View File

@ -5,9 +5,8 @@ ANDI instruction
""" """
class InsnAndi(InsnRV32IITypeArith): class InsnAndi(InsnRV32IITypeArith):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b111) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b111)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)

5
rvfi/insns/insn_auipc.py
View File

@ -5,9 +5,8 @@ AUIPC instruction
""" """
class InsnAuipc(InsnRV32IUType): class InsnAuipc(InsnRV32IUType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b0010111) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0010111)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)

7
rvfi/insns/insn_beq.py
View File

@ -5,13 +5,12 @@ BEQ instruction
""" """
class InsnBeq(InsnRV32ISBType): class InsnBeq(InsnRV32ISBType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
super().__init__(params, 0b000) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b000)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)
next_pc = Signal(self.params.xlen) next_pc = Signal(self.RISCV_FORMAL_XLEN)
m.d.comb += next_pc.eq(Mux(self.rvfi_rs1_rdata == self.rvfi_rs2_rdata, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4)) m.d.comb += next_pc.eq(Mux(self.rvfi_rs1_rdata == self.rvfi_rs2_rdata, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4))
m.d.comb += self.spec_pc_wdata.eq(next_pc) m.d.comb += self.spec_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) m.d.comb += self.spec_trap.eq(Mux(self.ialign16, next_pc[0] != 0, next_pc[:2] != 0) | ~self.misa_ok)

7
rvfi/insns/insn_bge.py
View File

@ -5,13 +5,12 @@ BGE instruction
""" """
class InsnBge(InsnRV32ISBType): class InsnBge(InsnRV32ISBType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
super().__init__(params, 0b101) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b101)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)
next_pc = Signal(self.params.xlen) next_pc = Signal(self.RISCV_FORMAL_XLEN)
m.d.comb += next_pc.eq(Mux(Value.as_signed(self.rvfi_rs1_rdata) >= Value.as_signed(self.rvfi_rs2_rdata), self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4)) m.d.comb += next_pc.eq(Mux(Value.as_signed(self.rvfi_rs1_rdata) >= Value.as_signed(self.rvfi_rs2_rdata), self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4))
m.d.comb += self.spec_pc_wdata.eq(next_pc) m.d.comb += self.spec_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) m.d.comb += self.spec_trap.eq(Mux(self.ialign16, next_pc[0] != 0, next_pc[:2] != 0) | ~self.misa_ok)

7
rvfi/insns/insn_bgeu.py
View File

@ -5,13 +5,12 @@ BGEU instruction
""" """
class InsnBgeu(InsnRV32ISBType): class InsnBgeu(InsnRV32ISBType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
super().__init__(params, 0b111) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b111)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)
next_pc = Signal(self.params.xlen) next_pc = Signal(self.RISCV_FORMAL_XLEN)
m.d.comb += next_pc.eq(Mux(self.rvfi_rs1_rdata >= self.rvfi_rs2_rdata, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4)) m.d.comb += next_pc.eq(Mux(self.rvfi_rs1_rdata >= self.rvfi_rs2_rdata, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4))
m.d.comb += self.spec_pc_wdata.eq(next_pc) m.d.comb += self.spec_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) m.d.comb += self.spec_trap.eq(Mux(self.ialign16, next_pc[0] != 0, next_pc[:2] != 0) | ~self.misa_ok)

7
rvfi/insns/insn_blt.py
View File

@ -5,13 +5,12 @@ BLT instruction
""" """
class InsnBlt(InsnRV32ISBType): class InsnBlt(InsnRV32ISBType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
super().__init__(params, 0b100) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b100)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)
next_pc = Signal(self.params.xlen) next_pc = Signal(self.RISCV_FORMAL_XLEN)
m.d.comb += next_pc.eq(Mux(Value.as_signed(self.rvfi_rs1_rdata) < Value.as_signed(self.rvfi_rs2_rdata), self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4)) m.d.comb += next_pc.eq(Mux(Value.as_signed(self.rvfi_rs1_rdata) < Value.as_signed(self.rvfi_rs2_rdata), self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4))
m.d.comb += self.spec_pc_wdata.eq(next_pc) m.d.comb += self.spec_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) m.d.comb += self.spec_trap.eq(Mux(self.ialign16, next_pc[0] != 0, next_pc[:2] != 0) | ~self.misa_ok)

7
rvfi/insns/insn_bltu.py
View File

@ -5,13 +5,12 @@ BLTU instruction
""" """
class InsnBltu(InsnRV32ISBType): class InsnBltu(InsnRV32ISBType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
super().__init__(params, 0b110) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b110)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)
next_pc = Signal(self.params.xlen) next_pc = Signal(self.RISCV_FORMAL_XLEN)
m.d.comb += next_pc.eq(Mux(self.rvfi_rs1_rdata < self.rvfi_rs2_rdata, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4)) m.d.comb += next_pc.eq(Mux(self.rvfi_rs1_rdata < self.rvfi_rs2_rdata, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4))
m.d.comb += self.spec_pc_wdata.eq(next_pc) m.d.comb += self.spec_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) m.d.comb += self.spec_trap.eq(Mux(self.ialign16, next_pc[0] != 0, next_pc[:2] != 0) | ~self.misa_ok)

7
rvfi/insns/insn_bne.py
View File

@ -5,13 +5,12 @@ BNE instruction
""" """
class InsnBne(InsnRV32ISBType): class InsnBne(InsnRV32ISBType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
super().__init__(params, 0b001) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b001)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)
next_pc = Signal(self.params.xlen) next_pc = Signal(self.RISCV_FORMAL_XLEN)
m.d.comb += next_pc.eq(Mux(self.rvfi_rs1_rdata != self.rvfi_rs2_rdata, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4)) m.d.comb += next_pc.eq(Mux(self.rvfi_rs1_rdata != self.rvfi_rs2_rdata, self.rvfi_pc_rdata + self.insn_imm, self.rvfi_pc_rdata + 4))
m.d.comb += self.spec_pc_wdata.eq(next_pc) m.d.comb += self.spec_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) m.d.comb += self.spec_trap.eq(Mux(self.ialign16, next_pc[0] != 0, next_pc[:2] != 0) | ~self.misa_ok)

9
rvfi/insns/insn_jal.py
View File

@ -5,23 +5,26 @@ JAL instruction
""" """
class InsnJal(Insn): class InsnJal(Insn):
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
self.RISCV_FORMAL_COMPRESSED = RISCV_FORMAL_COMPRESSED
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)
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_imm.eq(Value.as_signed(Cat(self.rvfi_insn[21:31], self.rvfi_insn[20], self.rvfi_insn[12:20], self.rvfi_insn[31]) << 1))
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0) m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
m.d.comb += self.spec_csr_misa_rmask.eq(4) m.d.comb += self.spec_csr_misa_rmask.eq(4)
m.d.comb += self.ialign16.eq((self.rvfi_csr_misa_rdata & 4) != 0) m.d.comb += self.ialign16.eq((self.rvfi_csr_misa_rdata & 4) != 0)
else: else:
m.d.comb += self.misa_ok.eq(1) m.d.comb += self.misa_ok.eq(1)
if self.params.compressed: if self.RISCV_FORMAL_COMPRESSED:
m.d.comb += self.ialign16.eq(1) m.d.comb += self.ialign16.eq(1)
else: else:
m.d.comb += self.ialign16.eq(0) m.d.comb += self.ialign16.eq(0)
next_pc = Signal(self.params.xlen) next_pc = Signal(self.RISCV_FORMAL_XLEN)
m.d.comb += next_pc.eq(self.rvfi_rs1_rdata + self.insn_imm) m.d.comb += next_pc.eq(self.rvfi_rs1_rdata + self.insn_imm)
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_opcode == 0b1101111)) m.d.comb += self.spec_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_addr.eq(self.insn_rd)

9
rvfi/insns/insn_jalr.py
View File

@ -5,21 +5,24 @@ JALR instruction
""" """
class InsnJalr(InsnRV32IIType): class InsnJalr(InsnRV32IIType):
def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
self.RISCV_FORMAL_COMPRESSED = RISCV_FORMAL_COMPRESSED
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0) m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
m.d.comb += self.spec_csr_misa_rmask.eq(4) m.d.comb += self.spec_csr_misa_rmask.eq(4)
m.d.comb += self.ialign16.eq((self.rvfi_csr_misa_rdata & 4) != 0) m.d.comb += self.ialign16.eq((self.rvfi_csr_misa_rdata & 4) != 0)
else: else:
m.d.comb += self.misa_ok.eq(1) m.d.comb += self.misa_ok.eq(1)
if self.params.compressed: if self.RISCV_FORMAL_COMPRESSED:
m.d.comb += self.ialign16.eq(1) m.d.comb += self.ialign16.eq(1)
else: else:
m.d.comb += self.ialign16.eq(0) m.d.comb += self.ialign16.eq(0)
next_pc = Signal(self.params.xlen) next_pc = Signal(self.RISCV_FORMAL_XLEN)
m.d.comb += next_pc.eq((self.rvfi_rs1_rdata + self.insn_imm) & ~1) 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_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_rs1_addr.eq(self.insn_rs1)

4
rvfi/insns/insn_lb.py
View File

@ -5,5 +5,5 @@ LB instruction
""" """
class InsnLb(InsnRV32IITypeLoad): class InsnLb(InsnRV32IITypeLoad):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
super().__init__(params, 0b000, 1, True) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b000, 1, True)

4
rvfi/insns/insn_lbu.py
View File

@ -5,5 +5,5 @@ LBU instruction
""" """
class InsnLbu(InsnRV32IITypeLoad): class InsnLbu(InsnRV32IITypeLoad):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
super().__init__(params, 0b100, 1, False) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b100, 1, False)

4
rvfi/insns/insn_lh.py
View File

@ -5,5 +5,5 @@ LH instruction
""" """
class InsnLh(InsnRV32IITypeLoad): class InsnLh(InsnRV32IITypeLoad):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
super().__init__(params, 0b001, 2, True) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b001, 2, True)

4
rvfi/insns/insn_lhu.py
View File

@ -5,5 +5,5 @@ LHU instruction
""" """
class InsnLhu(InsnRV32IITypeLoad): class InsnLhu(InsnRV32IITypeLoad):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
super().__init__(params, 0b101, 2, False) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b101, 2, False)

5
rvfi/insns/insn_lui.py
View File

@ -5,9 +5,8 @@ LUI instruction
""" """
class InsnLui(InsnRV32IUType): class InsnLui(InsnRV32IUType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b0110111) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0110111)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)

4
rvfi/insns/insn_lw.py
View File

@ -5,5 +5,5 @@ LW instruction
""" """
class InsnLw(InsnRV32IITypeLoad): class InsnLw(InsnRV32IITypeLoad):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
super().__init__(params, 0b010, 4, True) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b010, 4, True)

5
rvfi/insns/insn_or.py
View File

@ -5,9 +5,8 @@ OR instruction
""" """
class InsnOr(InsnRV32IRType): class InsnOr(InsnRV32IRType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b0000000, 0b110, 0b0110011) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b110, 0b0110011)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)

5
rvfi/insns/insn_ori.py
View File

@ -5,9 +5,8 @@ ORI instruction
""" """
class InsnOri(InsnRV32IITypeArith): class InsnOri(InsnRV32IITypeArith):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b110) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b110)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)

7
rvfi/insns/insn_rv32i_i_type_arith.py
View File

@ -5,14 +5,13 @@ RV32I I-Type Instruction (Arithmetic Variation)
""" """
class InsnRV32IITypeArith(InsnRV32IIType): class InsnRV32IITypeArith(InsnRV32IIType):
def __init__(self, params, funct3): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, funct3):
super().__init__(params) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
self.funct3 = funct3 self.funct3 = funct3
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0) m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
m.d.comb += self.spec_csr_misa_rmask.eq(0) m.d.comb += self.spec_csr_misa_rmask.eq(0)
else: else:

14
rvfi/insns/insn_rv32i_i_type_load.py
View File

@ -5,30 +5,30 @@ RV32I I-Type Instruction (Load Variation)
""" """
class InsnRV32IITypeLoad(InsnRV32IIType): class InsnRV32IITypeLoad(InsnRV32IIType):
def __init__(self, params, funct3, mask_shift, is_signed): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, funct3, mask_shift, is_signed):
super().__init__(params) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
self.RISCV_FORMAL_ALIGNED_MEM = RISCV_FORMAL_ALIGNED_MEM
self.funct3 = funct3 self.funct3 = funct3
self.mask_shift = mask_shift self.mask_shift = mask_shift
self.is_signed = is_signed self.is_signed = is_signed
self.addr = Signal(self.params.xlen) self.addr = Signal(self.RISCV_FORMAL_XLEN)
self.result = Signal(8 * self.mask_shift) self.result = Signal(8 * self.mask_shift)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0) m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
m.d.comb += self.spec_csr_misa_rmask.eq(0) m.d.comb += self.spec_csr_misa_rmask.eq(0)
else: else:
m.d.comb += self.misa_ok.eq(1) m.d.comb += self.misa_ok.eq(1)
if self.params.aligned_mem: if self.RISCV_FORMAL_ALIGNED_MEM:
m.d.comb += self.addr.eq(self.rvfi_rs1_rdata + self.insn_imm) m.d.comb += self.addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
m.d.comb += self.result.eq(self.rvfi_mem_rdata >> (8 * (self.addr - self.spec_mem_addr))) m.d.comb += self.result.eq(self.rvfi_mem_rdata >> (8 * (self.addr - self.spec_mem_addr)))
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == self.funct3) & (self.insn_opcode == 0b0000011)) m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == self.funct3) & (self.insn_opcode == 0b0000011))
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1) m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
m.d.comb += self.spec_rd_addr.eq(self.insn_rd) m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
m.d.comb += self.spec_mem_addr.eq(self.addr & ~(int(self.params.xlen // 8) - 1)) m.d.comb += self.spec_mem_addr.eq(self.addr & ~(int(self.RISCV_FORMAL_XLEN // 8) - 1))
m.d.comb += self.spec_mem_rmask.eq(((1 << self.mask_shift) - 1) << (self.addr - self.spec_mem_addr)) m.d.comb += self.spec_mem_rmask.eq(((1 << self.mask_shift) - 1) << (self.addr - self.spec_mem_addr))
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, Value.as_signed(self.result) if self.is_signed else self.result, 0)) m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, Value.as_signed(self.result) if self.is_signed else self.result, 0))
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4) m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)

9
rvfi/insns/insn_rv32i_i_type_shift.py
View File

@ -5,21 +5,20 @@ RV32I I-Type Instruction (Shift Variation)
""" """
class InsnRV32IITypeShift(Insn): class InsnRV32IITypeShift(Insn):
def __init__(self, params, funct6, funct3): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, funct6, funct3):
super().__init__(params) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
self.funct6 = funct6 self.funct6 = funct6
self.funct3 = funct3 self.funct3 = funct3
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0) m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
m.d.comb += self.spec_csr_misa_rmask.eq(0) m.d.comb += self.spec_csr_misa_rmask.eq(0)
else: else:
m.d.comb += self.misa_ok.eq(1) m.d.comb += self.misa_ok.eq(1)
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct6 == self.funct6) & (self.insn_funct3 == self.funct3) & (self.insn_opcode == 0b0010011) & ((~self.insn_shamt[5]) | (self.params.xlen == 64))) m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct6 == self.funct6) & (self.insn_funct3 == self.funct3) & (self.insn_opcode == 0b0010011) & ((~self.insn_shamt[5]) | (self.RISCV_FORMAL_XLEN == 64)))
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1) m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
m.d.comb += self.spec_rd_addr.eq(self.insn_rd) m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4) m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)

7
rvfi/insns/insn_rv32i_r_type.py
View File

@ -5,16 +5,15 @@ RV32I R-Type Instruction
""" """
class InsnRV32IRType(Insn): class InsnRV32IRType(Insn):
def __init__(self, params, funct7, funct3, opcode): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, funct7, funct3, opcode):
super().__init__(params) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
self.funct7 = funct7 self.funct7 = funct7
self.funct3 = funct3 self.funct3 = funct3
self.opcode = opcode self.opcode = opcode
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0) m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
m.d.comb += self.spec_csr_misa_rmask.eq(0) m.d.comb += self.spec_csr_misa_rmask.eq(0)
else: else:

14
rvfi/insns/insn_rv32i_s_type.py
View File

@ -5,29 +5,29 @@ RV32I S-Type Instruction
""" """
class InsnRV32ISType(Insn): class InsnRV32ISType(Insn):
def __init__(self, params, funct3, mask_shift): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, funct3, mask_shift):
super().__init__(params) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
self.RISCV_FORMAL_ALIGNED_MEM = RISCV_FORMAL_ALIGNED_MEM
self.funct3 = funct3 self.funct3 = funct3
self.mask_shift = mask_shift self.mask_shift = mask_shift
self.addr = Signal(self.params.xlen) self.addr = Signal(self.RISCV_FORMAL_XLEN)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)
m.d.comb += self.insn_imm.eq(Value.as_signed(Cat(self.rvfi_insn[7:12], self.rvfi_insn[25:32]))) m.d.comb += self.insn_imm.eq(Value.as_signed(Cat(self.rvfi_insn[7:12], self.rvfi_insn[25:32])))
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0) m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
m.d.comb += self.spec_csr_misa_rmask.eq(0) m.d.comb += self.spec_csr_misa_rmask.eq(0)
else: else:
m.d.comb += self.misa_ok.eq(1) m.d.comb += self.misa_ok.eq(1)
if self.params.aligned_mem: if self.RISCV_FORMAL_ALIGNED_MEM:
m.d.comb += self.addr.eq(self.rvfi_rs1_rdata + self.insn_imm) m.d.comb += self.addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == self.funct3) & (self.insn_opcode == 0b0100011)) m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == self.funct3) & (self.insn_opcode == 0b0100011))
m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1) m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2) m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
m.d.comb += self.spec_mem_addr.eq(self.addr & ~(int(self.params.xlen // 8) - 1)) m.d.comb += self.spec_mem_addr.eq(self.addr & ~(int(self.RISCV_FORMAL_XLEN // 8) - 1))
m.d.comb += self.spec_mem_wmask.eq(((1 << self.mask_shift) - 1) << (self.addr - self.spec_mem_addr)) m.d.comb += self.spec_mem_wmask.eq(((1 << self.mask_shift) - 1) << (self.addr - self.spec_mem_addr))
m.d.comb += self.spec_mem_wdata.eq(self.rvfi_rs2_rdata << (8 * (self.addr - self.spec_mem_addr))) m.d.comb += self.spec_mem_wdata.eq(self.rvfi_rs2_rdata << (8 * (self.addr - self.spec_mem_addr)))
m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4) m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)

10
rvfi/insns/insn_rv32i_sb_type.py
View File

@ -5,22 +5,22 @@ RV32I SB-Type Instruction
""" """
class InsnRV32ISBType(Insn): class InsnRV32ISBType(Insn):
def __init__(self, params, funct3): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, funct3):
super().__init__(params) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
self.RISCV_FORMAL_COMPRESSED = RISCV_FORMAL_COMPRESSED
self.funct3 = funct3 self.funct3 = funct3
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)
m.d.comb += self.insn_imm.eq(Value.as_signed(Cat(self.rvfi_insn[8:12], self.rvfi_insn[25:31], self.rvfi_insn[7], self.rvfi_insn[31]) << 1)) m.d.comb += self.insn_imm.eq(Value.as_signed(Cat(self.rvfi_insn[8:12], self.rvfi_insn[25:31], self.rvfi_insn[7], self.rvfi_insn[31]) << 1))
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0) m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
m.d.comb += self.spec_csr_misa_rmask.eq(4) m.d.comb += self.spec_csr_misa_rmask.eq(4)
m.d.comb += self.ialign16.eq((self.rvfi_csr_misa_rdata & 4) != 0) m.d.comb += self.ialign16.eq((self.rvfi_csr_misa_rdata & 4) != 0)
else: else:
m.d.comb += self.misa_ok.eq(1) m.d.comb += self.misa_ok.eq(1)
if self.params.compressed: if self.RISCV_FORMAL_COMPRESSED:
m.d.comb += self.ialign16.eq(1) m.d.comb += self.ialign16.eq(1)
else: else:
m.d.comb += self.ialign16.eq(0) m.d.comb += self.ialign16.eq(0)

7
rvfi/insns/insn_rv32i_u_type.py
View File

@ -5,16 +5,15 @@ RV32I U-Type Instruction
""" """
class InsnRV32IUType(Insn): class InsnRV32IUType(Insn):
def __init__(self, params, opcode): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, opcode):
super().__init__(params) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
self.opcode = opcode self.opcode = opcode
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)
m.d.comb += self.insn_imm.eq(Value.as_signed(self.rvfi_insn[12:32] << 12)) m.d.comb += self.insn_imm.eq(Value.as_signed(self.rvfi_insn[12:32] << 12))
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0) m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
m.d.comb += self.spec_csr_misa_rmask.eq(0) m.d.comb += self.spec_csr_misa_rmask.eq(0)
else: else:

4
rvfi/insns/insn_sb.py
View File

@ -5,5 +5,5 @@ SB instruction
""" """
class InsnSb(InsnRV32ISType): class InsnSb(InsnRV32ISType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
super().__init__(params, 0b000, 1) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b000, 1)

4
rvfi/insns/insn_sh.py
View File

@ -5,5 +5,5 @@ SH instruction
""" """
class InsnSh(InsnRV32ISType): class InsnSh(InsnRV32ISType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
super().__init__(params, 0b001, 2) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b001, 2)

7
rvfi/insns/insn_sll.py
View File

@ -5,12 +5,11 @@ SLL instruction
""" """
class InsnSll(InsnRV32IRType): class InsnSll(InsnRV32IRType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b0000000, 0b001, 0b0110011) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b001, 0b0110011)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata << Mux(self.params.xlen == 64, self.rvfi_rs2_rdata[:6], self.rvfi_rs2_rdata[:5]), 0)) m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata << Mux(self.RISCV_FORMAL_XLEN == 64, self.rvfi_rs2_rdata[:6], self.rvfi_rs2_rdata[:5]), 0))
return m return m

5
rvfi/insns/insn_slli.py
View File

@ -5,9 +5,8 @@ SLLI instruction
""" """
class InsnSlli(InsnRV32IITypeShift): class InsnSlli(InsnRV32IITypeShift):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b000000, 0b001) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b000000, 0b001)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)

5
rvfi/insns/insn_slt.py
View File

@ -5,9 +5,8 @@ SLT instruction
""" """
class InsnSlt(InsnRV32IRType): class InsnSlt(InsnRV32IRType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b0000000, 0b010, 0b0110011) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b010, 0b0110011)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)

5
rvfi/insns/insn_slti.py
View File

@ -5,9 +5,8 @@ SLTI instruction
""" """
class InsnSlti(InsnRV32IITypeArith): class InsnSlti(InsnRV32IITypeArith):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b010) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b010)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)

5
rvfi/insns/insn_sltiu.py
View File

@ -5,9 +5,8 @@ SLTIU instruction
""" """
class InsnSltiu(InsnRV32IITypeArith): class InsnSltiu(InsnRV32IITypeArith):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b011) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b011)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)

5
rvfi/insns/insn_sltu.py
View File

@ -5,9 +5,8 @@ SLTU instruction
""" """
class InsnSltu(InsnRV32IRType): class InsnSltu(InsnRV32IRType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b0000000, 0b011, 0b0110011) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b011, 0b0110011)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)

7
rvfi/insns/insn_sra.py
View File

@ -5,12 +5,11 @@ SRA instruction
""" """
class InsnSra(InsnRV32IRType): class InsnSra(InsnRV32IRType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b0100000, 0b101, 0b0110011) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0100000, 0b101, 0b0110011)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, (Value.as_signed(self.rvfi_rs1_rdata) >> Mux(self.params.xlen == 64, self.rvfi_rs2_rdata[:6], self.rvfi_rs2_rdata[:5])) | (-(Value.as_signed(self.rvfi_rs1_rdata) < 0) << (self.params.xlen - Mux(self.params.xlen == 64, self.rvfi_rs2_rdata[:6], self.rvfi_rs2_rdata[:5]))), 0)) # https://stackoverflow.com/a/25207042 m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, (Value.as_signed(self.rvfi_rs1_rdata) >> Mux(self.RISCV_FORMAL_XLEN == 64, self.rvfi_rs2_rdata[:6], self.rvfi_rs2_rdata[:5])) | (-(Value.as_signed(self.rvfi_rs1_rdata) < 0) << (self.RISCV_FORMAL_XLEN - Mux(self.RISCV_FORMAL_XLEN == 64, self.rvfi_rs2_rdata[:6], self.rvfi_rs2_rdata[:5]))), 0)) # https://stackoverflow.com/a/25207042
return m return m

7
rvfi/insns/insn_srai.py
View File

@ -5,12 +5,11 @@ SRAI instruction
""" """
class InsnSrai(InsnRV32IITypeShift): class InsnSrai(InsnRV32IITypeShift):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b010000, 0b101) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b010000, 0b101)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, (Value.as_signed(self.rvfi_rs1_rdata) >> self.insn_shamt) | (-(Value.as_signed(self.rvfi_rs1_rdata) < 0) << (self.params.xlen - self.insn_shamt)), 0)) m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, (Value.as_signed(self.rvfi_rs1_rdata) >> self.insn_shamt) | (-(Value.as_signed(self.rvfi_rs1_rdata) < 0) << (self.RISCV_FORMAL_XLEN - self.insn_shamt)), 0))
return m return m

7
rvfi/insns/insn_srl.py
View File

@ -5,12 +5,11 @@ SRL instruction
""" """
class InsnSrl(InsnRV32IRType): class InsnSrl(InsnRV32IRType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b0000000, 0b100, 0b0110011) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b100, 0b0110011)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)
m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata >> Mux(self.params.xlen == 64, self.rvfi_rs2_rdata[:6], self.rvfi_rs2_rdata[:5]), 0)) m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata >> Mux(self.RISCV_FORMAL_XLEN == 64, self.rvfi_rs2_rdata[:6], self.rvfi_rs2_rdata[:5]), 0))
return m return m

5
rvfi/insns/insn_srli.py
View File

@ -5,9 +5,8 @@ SRLI instruction
""" """
class InsnSrli(InsnRV32IITypeShift): class InsnSrli(InsnRV32IITypeShift):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b000000, 0b101) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b000000, 0b101)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)

5
rvfi/insns/insn_sub.py
View File

@ -5,9 +5,8 @@ SUB instruction
""" """
class InsnSub(InsnRV32IRType): class InsnSub(InsnRV32IRType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b0100000, 0b000, 0b0110011) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0100000, 0b000, 0b0110011)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)

4
rvfi/insns/insn_sw.py
View File

@ -5,5 +5,5 @@ SW instruction
""" """
class InsnSw(InsnRV32ISType): class InsnSw(InsnRV32ISType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
super().__init__(params, 0b010, 4) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b010, 4)

5
rvfi/insns/insn_xor.py
View File

@ -5,9 +5,8 @@ XOR instruction
""" """
class InsnXor(InsnRV32IRType): class InsnXor(InsnRV32IRType):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b0000000, 0b100, 0b0110011) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b100, 0b0110011)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)

5
rvfi/insns/insn_xori.py
View File

@ -5,9 +5,8 @@ XORI instruction
""" """
class InsnXori(InsnRV32IITypeArith): class InsnXori(InsnRV32IITypeArith):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
super().__init__(params, 0b100) super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b100)
def elaborate(self, platform): def elaborate(self, platform):
m = super().elaborate(platform) m = super().elaborate(platform)

124
rvfi/insns/isa_rv32i.py
View File

@ -41,35 +41,38 @@ RV32I Base ISA
""" """
class IsaRV32I(Elaboratable): class IsaRV32I(Elaboratable):
def __init__(self, params): def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, RISCV_FORMAL_ALIGNED_MEM):
# Core-specific parameters # Core-specific constants
self.params = params self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN
self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
self.RISCV_FORMAL_CSR_MISA = RISCV_FORMAL_CSR_MISA
self.RISCV_FORMAL_COMPRESSED = RISCV_FORMAL_COMPRESSED
self.RISCV_FORMAL_ALIGNED_MEM = RISCV_FORMAL_ALIGNED_MEM
# Input ports # Input ports
self.rvfi_valid = Signal(1) self.rvfi_valid = Signal(1)
self.rvfi_insn = Signal(self.params.ilen) self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN)
self.rvfi_pc_rdata = Signal(self.params.xlen) self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
self.rvfi_rs1_rdata = Signal(self.params.xlen) self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
self.rvfi_rs2_rdata = Signal(self.params.xlen) self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
self.rvfi_mem_rdata = Signal(self.params.xlen) self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN)
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
self.rvfi_csr_misa_rdata = Signal(self.params.xlen) self.rvfi_csr_misa_rdata = Signal(self.RISCV_FORMAL_XLEN)
# Output ports # Output ports
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
self.spec_csr_misa_rmask = Signal(self.params.xlen) self.spec_csr_misa_rmask = Signal(self.RISCV_FORMAL_XLEN)
self.spec_valid = Signal(1) self.spec_valid = Signal(1)
self.spec_trap = Signal(1) self.spec_trap = Signal(1)
self.spec_rs1_addr = Signal(5) self.spec_rs1_addr = Signal(5)
self.spec_rs2_addr = Signal(5) self.spec_rs2_addr = Signal(5)
self.spec_rd_addr = Signal(5) self.spec_rd_addr = Signal(5)
self.spec_rd_wdata = Signal(self.params.xlen) self.spec_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
self.spec_pc_wdata = Signal(self.params.xlen) self.spec_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
self.spec_mem_addr = Signal(self.params.xlen) self.spec_mem_addr = Signal(self.RISCV_FORMAL_XLEN)
self.spec_mem_rmask = Signal(int(self.params.xlen // 8)) self.spec_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
self.spec_mem_wmask = Signal(int(self.params.xlen // 8)) self.spec_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
self.spec_mem_wdata = Signal(self.params.xlen) self.spec_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
def ports(self): def ports(self):
input_ports = [ input_ports = [
self.rvfi_valid, self.rvfi_valid,
@ -79,7 +82,7 @@ class IsaRV32I(Elaboratable):
self.rvfi_rs2_rdata, self.rvfi_rs2_rdata,
self.rvfi_mem_rdata self.rvfi_mem_rdata
] ]
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
input_ports.append(self.rvfi_csr_misa_rdata) input_ports.append(self.rvfi_csr_misa_rdata)
output_ports = [ output_ports = [
self.spec_valid, self.spec_valid,
@ -94,52 +97,51 @@ class IsaRV32I(Elaboratable):
self.spec_mem_wmask, self.spec_mem_wmask,
self.spec_mem_wdata self.spec_mem_wdata
] ]
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
output_ports.append(self.spec_csr_misa_rmask) output_ports.append(self.spec_csr_misa_rmask)
return input_ports + output_ports return input_ports + output_ports
def elaborate(self, platform): def elaborate(self, platform):
m = Module() m = Module()
insn_submodules = {} insn_submodules = {}
m.submodules._lui = insn_submodules['lui'] = InsnLui(self.params) m.submodules._lui = insn_submodules['lui'] = InsnLui(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
m.submodules._auipc = insn_submodules['auipc'] = InsnAuipc(self.params) m.submodules._auipc = insn_submodules['auipc'] = InsnAuipc(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
m.submodules._jal = insn_submodules['jal'] = InsnJal(self.params) m.submodules._jal = insn_submodules['jal'] = InsnJal(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED)
m.submodules._jalr = insn_submodules['jalr'] = InsnJalr(self.params) m.submodules._jalr = insn_submodules['jalr'] = InsnJalr(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED)
m.submodules._beq = insn_submodules['beq'] = InsnBeq(self.params) m.submodules._beq = insn_submodules['beq'] = InsnBeq(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED)
m.submodules._bne = insn_submodules['bne'] = InsnBne(self.params) m.submodules._bne = insn_submodules['bne'] = InsnBne(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED)
m.submodules._blt = insn_submodules['blt'] = InsnBlt(self.params) m.submodules._blt = insn_submodules['blt'] = InsnBlt(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED)
m.submodules._bge = insn_submodules['bge'] = InsnBge(self.params) m.submodules._bge = insn_submodules['bge'] = InsnBge(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED)
m.submodules._bltu = insn_submodules['bltu'] = InsnBltu(self.params) m.submodules._bltu = insn_submodules['bltu'] = InsnBltu(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED)
m.submodules._bgeu = insn_submodules['bgeu'] = InsnBgeu(self.params) m.submodules._bgeu = insn_submodules['bgeu'] = InsnBgeu(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED)
m.submodules._lb = insn_submodules['lb'] = InsnLb(self.params) m.submodules._lb = insn_submodules['lb'] = InsnLb(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED)
m.submodules._lh = insn_submodules['lh'] = InsnLh(self.params) m.submodules._lh = insn_submodules['lh'] = InsnLh(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED)
m.submodules._lw = insn_submodules['lw'] = InsnLw(self.params) m.submodules._lw = insn_submodules['lw'] = InsnLw(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED)
m.submodules._lbu = insn_submodules['lbu'] = InsnLbu(self.params) m.submodules._lbu = insn_submodules['lbu'] = InsnLbu(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED)
m.submodules._lhu = insn_submodules['lhu'] = InsnLhu(self.params) m.submodules._lhu = insn_submodules['lhu'] = InsnLhu(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED)
m.submodules._sb = insn_submodules['sb'] = InsnSb(self.params) m.submodules._sb = insn_submodules['sb'] = InsnSb(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED)
m.submodules._sh = insn_submodules['Sh'] = InsnSh(self.params) m.submodules._sh = insn_submodules['Sh'] = InsnSh(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED)
m.submodules._sw = insn_submodules['sw'] = InsnSw(self.params) m.submodules._sw = insn_submodules['sw'] = InsnSw(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA, self.RISCV_FORMAL_COMPRESSED)
m.submodules._addi = insn_submodules['addi'] = InsnAddi(self.params) m.submodules._addi = insn_submodules['addi'] = InsnAddi(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
m.submodules._slti = insn_submodules['slti'] = InsnSlti(self.params) m.submodules._slti = insn_submodules['slti'] = InsnSlti(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
m.submodules._sltiu = insn_submodules['sltiu'] = InsnSltiu(self.params) m.submodules._sltiu = insn_submodules['sltiu'] = InsnSltiu(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
m.submodules._xori = insn_submodules['xori'] = InsnXori(self.params) m.submodules._xori = insn_submodules['xori'] = InsnXori(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
m.submodules._ori = insn_submodules['ori'] = InsnOri(self.params) m.submodules._ori = insn_submodules['ori'] = InsnOri(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
m.submodules._andi = insn_submodules['andi'] = InsnAndi(self.params) m.submodules._andi = insn_submodules['andi'] = InsnAndi(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
m.submodules._slli = insn_submodules['slli'] = InsnSlli(self.params) m.submodules._slli = insn_submodules['slli'] = InsnSlli(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
m.submodules._srli = insn_submodules['srli'] = InsnSrli(self.params) m.submodules._srli = insn_submodules['srli'] = InsnSrli(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
m.submodules._srai = insn_submodules['srai'] = InsnSrai(self.params) m.submodules._srai = insn_submodules['srai'] = InsnSrai(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
m.submodules._add = insn_submodules['add'] = InsnAdd(self.params) m.submodules._add = insn_submodules['add'] = InsnAdd(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
m.submodules._sub = insn_submodules['sub'] = InsnSub(self.params) m.submodules._sub = insn_submodules['sub'] = InsnSub(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
m.submodules._sll = insn_submodules['sll'] = InsnSll(self.params) m.submodules._sll = insn_submodules['sll'] = InsnSll(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
m.submodules._slt = insn_submodules['slt'] = InsnSlt(self.params) m.submodules._slt = insn_submodules['slt'] = InsnSlt(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
m.submodules._sltu = insn_submodules['sltu'] = InsnSltu(self.params) m.submodules._sltu = insn_submodules['sltu'] = InsnSltu(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
m.submodules._xor = insn_submodules['xor'] = InsnXor(self.params) m.submodules._xor = insn_submodules['xor'] = InsnXor(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
m.submodules._srl = insn_submodules['srl'] = InsnSrl(self.params) m.submodules._srl = insn_submodules['srl'] = InsnSrl(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
m.submodules._sra = insn_submodules['sra'] = InsnSra(self.params) m.submodules._sra = insn_submodules['sra'] = InsnSra(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
m.submodules._or = insn_submodules['or'] = InsnOr(self.params) m.submodules._or = insn_submodules['or'] = InsnOr(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
m.submodules._and = insn_submodules['and'] = InsnAnd(self.params) m.submodules._and = insn_submodules['and'] = InsnAnd(self.RISCV_FORMAL_ILEN, self.RISCV_FORMAL_XLEN, self.RISCV_FORMAL_CSR_MISA)
for _, insn in insn_submodules.items(): for _, insn in insn_submodules.items():
m.d.comb += insn.rvfi_valid.eq(self.rvfi_valid) m.d.comb += insn.rvfi_valid.eq(self.rvfi_valid)
@ -148,7 +150,7 @@ class IsaRV32I(Elaboratable):
m.d.comb += insn.rvfi_rs1_rdata.eq(self.rvfi_rs1_rdata) m.d.comb += insn.rvfi_rs1_rdata.eq(self.rvfi_rs1_rdata)
m.d.comb += insn.rvfi_rs2_rdata.eq(self.rvfi_rs2_rdata) m.d.comb += insn.rvfi_rs2_rdata.eq(self.rvfi_rs2_rdata)
m.d.comb += insn.rvfi_mem_rdata.eq(self.rvfi_mem_rdata) m.d.comb += insn.rvfi_mem_rdata.eq(self.rvfi_mem_rdata)
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
m.d.comb += insn.rvfi_csr_misa_rdata.eq(self.rvfi_csr_misa_rdata) m.d.comb += insn.rvfi_csr_misa_rdata.eq(self.rvfi_csr_misa_rdata)
spec_valid = 0 spec_valid = 0
@ -206,7 +208,7 @@ class IsaRV32I(Elaboratable):
spec_mem_wdata = Mux(insn.spec_valid, insn.spec_mem_wdata, spec_mem_wdata) spec_mem_wdata = Mux(insn.spec_valid, insn.spec_mem_wdata, spec_mem_wdata)
m.d.comb += self.spec_mem_wdata.eq(spec_mem_wdata) m.d.comb += self.spec_mem_wdata.eq(spec_mem_wdata)
if self.params.csr_misa: if self.RISCV_FORMAL_CSR_MISA:
spec_csr_misa_rmask = 0 spec_csr_misa_rmask = 0
for _, insn in insn_submodules.items(): for _, insn in insn_submodules.items():
spec_csr_misa_rmask = Mux(insn.spec_valid, insn.spec_csr_misa_rmask, spec_csr_misa_rmask) spec_csr_misa_rmask = Mux(insn.spec_valid, insn.spec_csr_misa_rmask, spec_csr_misa_rmask)

4
rvfi/riscv_formal_parameters.py
View File

@ -1,4 +0,0 @@
from collections import namedtuple
RISCVFormalParameters = namedtuple('RISCVFormalParameters',
['ilen', 'xlen', 'csr_misa', 'compressed', 'aligned_mem'])