Merge pull request 'Restructure insns directory contents' (#2) from restructuring into master

README.md

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

checks/rvfi_causal_check.py

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

checks/rvfi_channel.py

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

checks/rvfi_dmem_check.py

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

checks/rvfi_hang_check.py

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

checks/rvfi_ill_check.py

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

checks/rvfi_imem_check.py

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

checks/rvfi_insn_check.py

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

checks/rvfi_liveness_check.py

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

checks/rvfi_pc_bwd_check.py

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

checks/rvfi_pc_fwd_check.py

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

checks/rvfi_reg_check.py

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

checks/rvfi_unique_check.py

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

insns/README.md

@@ -1,28 +1,102 @@
 # RISC-V Instructions
 
-Refer to the table below for the instructions currently supported. At the time of writing, it covers the instructions in the RV32I base ISA except FENCE, ECALL and EBREAK, as well as the RV32M extension\*.
+## Instructions
+
+Below is a table of RISC-V instructions supported by the original riscv-formal framework at the time of writing, categorized by instruction type.
 
 | Instruction type | Instructions |
 | --- | --- |
-| U-type | lui, auipc |
+| R-type | ADD, ADDW, AND, DIV, DIVU, DIVUW, DIVW, MUL, MULH, MULHSU, MULHU, MULW, OR, REM, REMU, REMUW, REMW, SLL, SLLW, SLT, SLTU, SRA, SRAW, SRL, SRLW, SUB, SUBW, XOR |
-| UJ-type | jal |
+| I-type | ADDI, ADDIW, ANDI, JALR, LB, LBU, LD, LH, LHU, LW, LWU, ORI, SLTI, SLTIU, XORI |
-| I-type | jalr, lb, lh, lw, lbu, lhu, addi, slti, sltiu, xori, ori, andi |
+| I-type (shift variation) | SLLI, SLLIW, SRAI, SRAIW, SRLI, SRLIW |
-| SB-type | beq, bne, blt, bge, bltu, bgeu |
+| S-type | SB, SD, SH, SW |
-| S-type | sb, sh, sw |
+| SB-type | BEQ, BGE, BGEU, BLT, BLTU, BNE |
-| I-type (shift variation) | slli, srli, srai |
+| U-type | AUIPC, LUI |
-| R-type | add, sub, sll, slt, sltu, xor, srl, sra, or, and, mul, mulh, mulhsu, mulhu, div, divu, rem, remu |
+| UJ-type | JAL |
+| CI-type | C\_ADD, C\_ADDI, C\_ADDIW, C\_JALR, C\_JR, C\_LI, C\_MV |
+| CI-type (SP variation) | C\_ADDI16SP |
+| CI-type (ANDI variation) | C\_ANDI |
+| CI-type (LSP variation, 32 bit version) | C\_LWSP |
+| CI-type (LSP variation, 64 bit version) | C\_LDSP |
+| CI-type (LUI variation) | C\_LUI |
+| CI-type (SLI variation) | C\_SLLI |
+| CI-type (SRI variation) | C\_SRAI, C\_SRLI |
+| CIW-type | C\_ADDI4SPN |
+| CS-type (ALU version) | C\_ADDW, C\_AND, C\_OR, C\_SUB, C\_SUBW, C\_XOR |
+| CS-type (32 bit version) | C\_SW |
+| CS-type (64 bit version) | C\_SD |
+| CSS-type (32 bit version) | C\_SWSP |
+| CSS-type (64 bit version) | C\_SDSP |
+| CB-type | C\_BEQZ, C\_BNEZ |
+| CJ-type | C\_J, C\_JAL |
+| CL-type (32 bit version) | C\_LW |
+| CL-type (64 bit version) | C\_LD |
 
-\* Due to limitations with modern solvers, they are sometimes unable to verify assertions involving multiplication and/or division; therefore, the core under test is expected to implement alternative operations for the RV32M extensions for the purposes of formal verification only, replacing multiplication/division operations with addition/subtraction and XORing with selected bitmasks.
+## Class Synopsis
 
-## Caveats
+### Instructions
 
-At the time of writing, the set of instructions supported in this port of riscv-formal is a mere subset of those supported in the original riscv-formal; for example, compressed instructions and 64-bit ISAs/extensions are not supported. Also note that the original riscv-formal contains tunable parameters that have been fixed to certain values in this translation:
+Below is a list of instructions currently supported by this port of the riscv-formal framework and is expected to grow over time. The instructions are roughly grouped by instruction type but sometimes with further specializations - the hierarchy of the lists reflects the hierarchy of inheritance in the classes used to represent various instructions.
 
-| Parameter from riscv-formal | Fixed value in riscv-formal-nmigen |
+- `Insn`: General RISC-V instruction
-| --- | --- |
+  - `InsnRV32IRType`: RV32I R-Type Instruction
-| `RISCV_FORMAL_ILEN` | 32 |
+    - `InsnAdd`: ADD instruction
-| `RISCV_FORMAL_XLEN` | 32 |
+    - `InsnSub`: SUB instruction
-| `RISCV_FORMAL_CSR_MISA` | undefined |
+    - `InsnSll`: SLL instruction
-| `RISCV_FORMAL_COMPRESSED` | undefined |
+    - `InsnSlt`: SLT instruction
-| `RISCV_FORMAL_ALIGNED_MEM` | undefined |
+    - `InsnSltu`: SLTU instruction
-| `RISCV_FORMAL_ALTOPS` | defined |
+    - `InsnXor`: XOR instruction
+    - `InsnSrl`: SRL instruction
+    - `InsnSra`: SRA instruction
+    - `InsnOr`: OR instruction
+    - `InsnAnd`: AND instruction
+  - `InsnRV32IITypeShift`: RV32I I-Type Instruction (Shift Variation)
+    - `InsnSlli`: SLLI instruction
+    - `InsnSrli`: SRLI instruction
+    - `InsnSrai`: SRAI instruction
+  - `InsnRV32IIType`: RV32I I-Type Instruction
+    - `InsnJalr`: JALR instruction
+    - `InsnRV32IITypeLoad`: RV32I I-Type Instruction (Load Variation)
+      - `InsnLb`: LB instruction
+      - `InsnLh`: LH instruction
+      - `InsnLw`: LW instruction
+      - `InsnLbu`: LBU instruction
+      - `InsnLhu`: LHU instruction
+    - `InsnRV32IITypeArith`: RV32I I-Type Instruction (Arithmetic Variation)
+      - `InsnAddi`: ADDI instruction
+      - `InsnSlti`: SLTI instruction
+      - `InsnSltiu`: SLTIU instruction
+      - `InsnXori`: XORI instruction
+      - `InsnOri`: ORI instruction
+      - `InsnAndi`: ANDI instruction
+  - `InsnRV32ISType`: RV32I S-Type Instruction
+    - `InsnSb`: SB instruction
+    - `InsnSh`: SH instruction
+    - `InsnSw`: SW instruction
+  - `InsnRV32ISBType`: RV32I SB-Type Instruction
+    - `InsnBeq`: BEQ instruction
+    - `InsnBne`: BNE instruction
+    - `InsnBlt`: BLT instruction
+    - `InsnBge`: BGE instruction
+    - `InsnBltu`: BLTU instruction
+    - `InsnBgeu`: BGEU instruction
+  - `InsnJal`: JAL instruction
+  - `InsnRV32IUType`: RV32I U-Type Instruction
+    - `InsnLui`: LUI instruction
+    - `InsnAuipc`: AUIPC instruction
+
+### ISAs
+
+- `IsaRV32I`: RV32I Base ISA
+
+## Core-specific constants
+
+The following core-specific constants are currently supported:
+
+| Constant | Description | Valid value(s) | Supported by instruction(s) | Supported by ISA(s) |
+| --- | --- | --- | --- | --- |
+| `RISCV_FORMAL_ILEN` | Max length of instruction retired by core | `32` | LUI, AUIPC, JAL, JALR, BEQ, BNE, BLT, BGE, BLTU, BGEU, LB, LH, LW, LBU, LHU, SB, SH, SW, ADDI, SLTI, SLTIU, XORI, ORI, ANDI, SLLI, SRLI, SRAI, ADD, SUB, SLL, SLT, SLTU, XOR, SRL, SRA, OR, AND | RV32I |
+| `RISCV_FORMAL_XLEN` | Width of integer registers | `32` | LUI, AUIPC, JAL, JALR, BEQ, BNE, BLT, BGE, BLTU, BGEU, LB, LH, LW, LBU, LHU, SB, SH, SW, ADDI, SLTI, SLTIU, XORI, ORI, ANDI, SLLI, SRLI, SRAI, ADD, SUB, SLL, SLT, SLTU, XOR, SRL, SRA, OR, AND | RV32I |
+| `RISCV_FORMAL_CSR_MISA` | Support for MISA CSRs enabled | `True`, `False` | LUI, AUIPC, JAL, JALR, BEQ, BNE, BLT, BGE, BLTU, BGEU, LB, LH, LW, LBU, LHU, SB, SH, SW, ADDI, SLTI, SLTIU, XORI, ORI, ANDI, SLLI, SRLI, SRAI, ADD, SUB, SLL, SLT, SLTU, XOR, SRL, SRA, OR, AND | RV32I |
+| `RISCV_FORMAL_COMPRESSED` | Support for compressed instructions | `True`, `False` | JAL, JALR, BEQ, BNE, BLT, BGE, BLTU, BGEU | RV32I |
+| `RISCV_FORMAL_ALIGNED_MEM` | Require aligned memory accesses | `True`, `False` | LB, LH, LW, LBU, LHU, SB, SH, SW | RV32I |

insns/insn.py

@@ -1,27 +1,55 @@
 from nmigen import *
 
-class rvfi_insn(Elaboratable):
+"""
-    def __init__(self):
+Insn.py
-        # Input ports
+Class for generic RISC-V instructions
-        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
+class Insn(Elaboratable):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        # Core-specific constants
+        self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN
+        self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN
+        self.RISCV_FORMAL_CSR_MISA = RISCV_FORMAL_CSR_MISA
+
+        # RVFI input ports
+        self.rvfi_valid = Signal(1)
+        self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN)
+        self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN)
+        self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN)
+        self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN)
+        self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN)
+        if self.RISCV_FORMAL_CSR_MISA:
+            self.rvfi_csr_misa_rdata = Signal(self.RISCV_FORMAL_XLEN)
+
+        # RVFI output ports
+        if self.RISCV_FORMAL_CSR_MISA:
+            self.spec_csr_misa_rmask = Signal(self.RISCV_FORMAL_XLEN)
         self.spec_valid = Signal(1)
         self.spec_trap = Signal(1)
         self.spec_rs1_addr = Signal(5)
         self.spec_rs2_addr = Signal(5)
         self.spec_rd_addr = Signal(5)
-        self.spec_rd_wdata = Signal(32)
+        self.spec_rd_wdata = Signal(self.RISCV_FORMAL_XLEN)
-        self.spec_pc_wdata = Signal(32)
+        self.spec_pc_wdata = Signal(self.RISCV_FORMAL_XLEN)
-        self.spec_mem_addr = Signal(32)
+        self.spec_mem_addr = Signal(self.RISCV_FORMAL_XLEN)
-        self.spec_mem_rmask = Signal(4)
+        self.spec_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
-        self.spec_mem_wmask = Signal(4)
+        self.spec_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8))
-        self.spec_mem_wdata = Signal(32)
+        self.spec_mem_wdata = Signal(self.RISCV_FORMAL_XLEN)
+
+        # Additional wires and registers
+        self.insn_padding = Signal(self.RISCV_FORMAL_ILEN)
+        self.insn_imm = Signal(self.RISCV_FORMAL_XLEN)
+        self.insn_funct7 = Signal(7)
+        self.insn_funct6 = Signal(6)
+        self.insn_shamt = Signal(6)
+        self.insn_rs2 = Signal(5)
+        self.insn_rs1 = Signal(5)
+        self.insn_funct3 = Signal(3)
+        self.insn_rd = Signal(5)
+        self.insn_opcode = Signal(7)
+        self.misa_ok = Signal(1)
+        self.ialign16 = Signal(1)
     def ports(self):
         input_ports = [
             self.rvfi_valid,
@@ -31,6 +59,8 @@ class rvfi_insn(Elaboratable):
             self.rvfi_rs2_rdata,
             self.rvfi_mem_rdata
         ]
+        if self.RISCV_FORMAL_CSR_MISA:
+            input_ports.append(self.rvfi_csr_misa_rdata)
         output_ports = [
             self.spec_valid,
             self.spec_trap,
@@ -44,8 +74,33 @@ class rvfi_insn(Elaboratable):
             self.spec_mem_wmask,
             self.spec_mem_wdata
         ]
+        if self.RISCV_FORMAL_CSR_MISA:
+            output_ports.append(self.spec_csr_misa_rmask)
         return input_ports + output_ports
     def elaborate(self, platform):
         m = Module()
 
+        m.d.comb += self.insn_padding.eq(self.rvfi_insn >> 32)
+        m.d.comb += self.insn_funct7.eq(self.rvfi_insn[25:32])
+        m.d.comb += self.insn_funct6.eq(self.rvfi_insn[26:32])
+        m.d.comb += self.insn_shamt.eq(self.rvfi_insn[20:26])
+        m.d.comb += self.insn_rs2.eq(self.rvfi_insn[20:25])
+        m.d.comb += self.insn_rs1.eq(self.rvfi_insn[15:20])
+        m.d.comb += self.insn_funct3.eq(self.rvfi_insn[12:15])
+        m.d.comb += self.insn_rd.eq(self.rvfi_insn[7:12])
+        m.d.comb += self.insn_opcode.eq(self.rvfi_insn[:7])
+
+        # default assignments
+        m.d.comb += self.spec_valid.eq(0)
+        m.d.comb += self.spec_trap.eq(~self.misa_ok)
+        m.d.comb += self.spec_rs1_addr.eq(0)
+        m.d.comb += self.spec_rs2_addr.eq(0)
+        m.d.comb += self.spec_rd_addr.eq(0)
+        m.d.comb += self.spec_rd_wdata.eq(0)
+        m.d.comb += self.spec_pc_wdata.eq(0)
+        m.d.comb += self.spec_mem_addr.eq(0)
+        m.d.comb += self.spec_mem_rmask.eq(0)
+        m.d.comb += self.spec_mem_wmask.eq(0)
+        m.d.comb += self.spec_mem_wdata.eq(0)
+
         return m

insns/insn_I.py

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

insns/insn_I_shift.py

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

insns/insn_R.py

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

insns/insn_S.py

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

insns/insn_SB.py

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

insns/insn_U.py

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

insns/insn_UJ.py

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

insns/insn_add.py

@@ -1,21 +1,15 @@
-from insn_R import *
+from insn_rv32i_r_type import *
 
-class rvfi_insn_add(rvfi_insn_R):
+"""
-    def __init__(self):
+ADD instruction
-        super(rvfi_insn_add, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_add, self).ports()
+class InsnAdd(InsnRV32IRType):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b000, 0b0110011)
     def elaborate(self, platform):
-        m = super(rvfi_insn_add, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # ADD instruction
+        m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata + self.rvfi_rs2_rdata, 0))
-        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

insns/insn_addi.py

@@ -1,20 +1,15 @@
-from insn_I import *
+from insn_rv32i_i_type_arith import *
 
-class rvfi_insn_addi(rvfi_insn_I):
+"""
-    def __init__(self):
+ADDI instruction
-        super(rvfi_insn_addi, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_addi, self).ports()
+class InsnAddi(InsnRV32IITypeArith):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b000)
     def elaborate(self, platform):
-        m = super(rvfi_insn_addi, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # ADDI instruction
+        m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata + self.insn_imm, 0))
-        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

insns/insn_and.py

@@ -1,21 +1,15 @@
-from insn_R import *
+from insn_rv32i_r_type import *
 
-class rvfi_insn_and(rvfi_insn_R):
+"""
-    def __init__(self):
+AND instruction
-        super(rvfi_insn_and, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_and, self).ports()
+class InsnAnd(InsnRV32IRType):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b111, 0b0110011)
     def elaborate(self, platform):
-        m = super(rvfi_insn_and, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # AND instruction
+        m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata & self.rvfi_rs2_rdata, 0))
-        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

insns/insn_andi.py

@@ -1,20 +1,15 @@
-from insn_I import *
+from insn_rv32i_i_type_arith import *
 
-class rvfi_insn_andi(rvfi_insn_I):
+"""
-    def __init__(self):
+ANDI instruction
-        super(rvfi_insn_andi, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_andi, self).ports()
+class InsnAndi(InsnRV32IITypeArith):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b111)
     def elaborate(self, platform):
-        m = super(rvfi_insn_andi, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # ANDI instruction
+        m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata & self.insn_imm, 0))
-        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

insns/insn_auipc.py

@@ -1,17 +1,15 @@
-from insn_U import *
+from insn_rv32i_u_type import *
 
-class rvfi_insn_auipc(rvfi_insn_U):
+"""
-    def __init__(self):
+AUIPC instruction
-        super(rvfi_insn_auipc, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_auipc, self).ports()
+class InsnAuipc(InsnRV32IUType):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0010111)
     def elaborate(self, platform):
-        m = super(rvfi_insn_auipc, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # AUIPC instruction
-        m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_opcode == 0b0010111))
-        m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
         m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_pc_rdata + self.insn_imm, 0))
-        m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
 
         return m

insns/insn_beq.py

@@ -1,21 +1,17 @@
-from insn_SB import *
+from insn_rv32i_sb_type import *
 
-class rvfi_insn_beq(rvfi_insn_SB):
+"""
-    def __init__(self):
+BEQ instruction
-        super(rvfi_insn_beq, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_beq, self).ports()
+class InsnBeq(InsnRV32ISBType):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b000)
     def elaborate(self, platform):
-        m = super(rvfi_insn_beq, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # BEQ instruction
+        next_pc = Signal(self.RISCV_FORMAL_XLEN)
-        cond = Signal(1)
+        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 += 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)
 

insns/insn_bge.py

@@ -1,21 +1,17 @@
-from insn_SB import *
+from insn_rv32i_sb_type import *
 
-class rvfi_insn_bge(rvfi_insn_SB):
+"""
-    def __init__(self):
+BGE instruction
-        super(rvfi_insn_bge, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_bge, self).ports()
+class InsnBge(InsnRV32ISBType):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b101)
     def elaborate(self, platform):
-        m = super(rvfi_insn_bge, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # BGE instruction
+        next_pc = Signal(self.RISCV_FORMAL_XLEN)
-        cond = Signal(1)
+        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 += 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)
 

insns/insn_bgeu.py

@@ -1,21 +1,17 @@
-from insn_SB import *
+from insn_rv32i_sb_type import *
 
-class rvfi_insn_bgeu(rvfi_insn_SB):
+"""
-    def __init__(self):
+BGEU instruction
-        super(rvfi_insn_bgeu, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_bgeu, self).ports()
+class InsnBgeu(InsnRV32ISBType):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b111)
     def elaborate(self, platform):
-        m = super(rvfi_insn_bgeu, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # BGEU instruction
+        next_pc = Signal(self.RISCV_FORMAL_XLEN)
-        cond = Signal(1)
+        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 += 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)
 

insns/insn_blt.py

@@ -1,21 +1,17 @@
-from insn_SB import *
+from insn_rv32i_sb_type import *
 
-class rvfi_insn_blt(rvfi_insn_SB):
+"""
-    def __init__(self):
+BLT instruction
-        super(rvfi_insn_blt, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_blt, self).ports()
+class InsnBlt(InsnRV32ISBType):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b100)
     def elaborate(self, platform):
-        m = super(rvfi_insn_blt, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # BLT instruction
+        next_pc = Signal(self.RISCV_FORMAL_XLEN)
-        cond = Signal(1)
+        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 += 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)
 

insns/insn_bltu.py

@@ -1,21 +1,17 @@
-from insn_SB import *
+from insn_rv32i_sb_type import *
 
-class rvfi_insn_bltu(rvfi_insn_SB):
+"""
-    def __init__(self):
+BLTU instruction
-        super(rvfi_insn_bltu, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_bltu, self).ports()
+class InsnBltu(InsnRV32ISBType):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b110)
     def elaborate(self, platform):
-        m = super(rvfi_insn_bltu, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # BLTU instruction
+        next_pc = Signal(self.RISCV_FORMAL_XLEN)
-        cond = Signal(1)
+        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 += 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)
 

insns/insn_bne.py

@@ -1,21 +1,17 @@
-from insn_SB import *
+from insn_rv32i_sb_type import *
 
-class rvfi_insn_bne(rvfi_insn_SB):
+"""
-    def __init__(self):
+BNE instruction
-        super(rvfi_insn_bne, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_bne, self).ports()
+class InsnBne(InsnRV32ISBType):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, 0b001)
     def elaborate(self, platform):
-        m = super(rvfi_insn_bne, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # BNE instruction
+        next_pc = Signal(self.RISCV_FORMAL_XLEN)
-        cond = Signal(1)
+        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 += 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)
 

insns/insn_div.py

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

insns/insn_divu.py

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

insns/insn_jal.py

@@ -1,16 +1,31 @@
-from insn_UJ import *
+from insn import *
 
-class rvfi_insn_jal(rvfi_insn_UJ):
+"""
-    def __init__(self):
+JAL instruction
-        super(rvfi_insn_jal, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_jal, self).ports()
+class InsnJal(Insn):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
+        self.RISCV_FORMAL_COMPRESSED = RISCV_FORMAL_COMPRESSED
     def elaborate(self, platform):
-        m = super(rvfi_insn_jal, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # JAL instruction
+        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))
-        next_pc = Signal(32)
+
-        m.d.comb += next_pc.eq(self.rvfi_pc_rdata + self.insn_imm)
+        if self.RISCV_FORMAL_CSR_MISA:
+            m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
+            m.d.comb += self.spec_csr_misa_rmask.eq(4)
+            m.d.comb += self.ialign16.eq((self.rvfi_csr_misa_rdata & 4) != 0)
+        else:
+            m.d.comb += self.misa_ok.eq(1)
+            if self.RISCV_FORMAL_COMPRESSED:
+                m.d.comb += self.ialign16.eq(1)
+            else:
+                m.d.comb += self.ialign16.eq(0)
+
+        next_pc = Signal(self.RISCV_FORMAL_XLEN)
+        m.d.comb += next_pc.eq(self.rvfi_rs1_rdata + self.insn_imm)
         m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_opcode == 0b1101111))
         m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
         m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_pc_rdata + 4, 0))

insns/insn_jalr.py

@@ -1,15 +1,28 @@
-from insn_I import *
+from insn_rv32i_i_type import *
 
-class rvfi_insn_jalr(rvfi_insn_I):
+"""
-    def __init__(self):
+JALR instruction
-        super(rvfi_insn_jalr, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_jalr, self).ports()
+class InsnJalr(InsnRV32IIType):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
+        self.RISCV_FORMAL_COMPRESSED = RISCV_FORMAL_COMPRESSED
     def elaborate(self, platform):
-        m = super(rvfi_insn_jalr, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # JALR instruction
+        if self.RISCV_FORMAL_CSR_MISA:
-        next_pc = Signal(32)
+            m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
+            m.d.comb += self.spec_csr_misa_rmask.eq(4)
+            m.d.comb += self.ialign16.eq((self.rvfi_csr_misa_rdata & 4) != 0)
+        else:
+            m.d.comb += self.misa_ok.eq(1)
+            if self.RISCV_FORMAL_COMPRESSED:
+                m.d.comb += self.ialign16.eq(1)
+            else:
+                m.d.comb += self.ialign16.eq(0)
+
+        next_pc = Signal(self.RISCV_FORMAL_XLEN)
         m.d.comb += next_pc.eq((self.rvfi_rs1_rdata + self.insn_imm) & ~1)
         m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == 0b000) & (self.insn_opcode == 0b1100111))
         m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)

insns/insn_lb.py

@@ -1,25 +1,9 @@
-from insn_I import *
+from insn_rv32i_i_type_load import *
 
-class rvfi_insn_lb(rvfi_insn_I):
+"""
-    def __init__(self):
+LB instruction
-        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
+class InsnLb(InsnRV32IITypeLoad):
-        addr = Signal(32)
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
-        m.d.comb += addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b000, 1, True)
-        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

insns/insn_lbu.py

@@ -1,25 +1,9 @@
-from insn_I import *
+from insn_rv32i_i_type_load import *
 
-class rvfi_insn_lbu(rvfi_insn_I):
+"""
-    def __init__(self):
+LBU instruction
-        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
+class InsnLbu(InsnRV32IITypeLoad):
-        addr = Signal(32)
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
-        m.d.comb += addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b100, 1, False)
-        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

insns/insn_lh.py

@@ -1,25 +1,9 @@
-from insn_I import *
+from insn_rv32i_i_type_load import *
 
-class rvfi_insn_lh(rvfi_insn_I):
+"""
-    def __init__(self):
+LH instruction
-        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
+class InsnLh(InsnRV32IITypeLoad):
-        addr = Signal(32)
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
-        m.d.comb += addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b001, 2, True)
-        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

insns/insn_lhu.py

@@ -1,25 +1,9 @@
-from insn_I import *
+from insn_rv32i_i_type_load import *
 
-class rvfi_insn_lhu(rvfi_insn_I):
+"""
-    def __init__(self):
+LHU instruction
-        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
+class InsnLhu(InsnRV32IITypeLoad):
-        addr = Signal(32)
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
-        m.d.comb += addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b101, 2, False)
-        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

insns/insn_lui.py

@@ -1,17 +1,15 @@
-from insn_U import *
+from insn_rv32i_u_type import *
 
-class rvfi_insn_lui(rvfi_insn_U):
+"""
-    def __init__(self):
+LUI instruction
-        super(rvfi_insn_lui, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_lui, self).ports()
+class InsnLui(InsnRV32IUType):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0110111)
     def elaborate(self, platform):
-        m = super(rvfi_insn_lui, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # LUI instruction
-        m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_opcode == 0b0110111))
-        m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
         m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.insn_imm, 0))
-        m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
 
         return m

insns/insn_lw.py

@@ -1,25 +1,9 @@
-from insn_I import *
+from insn_rv32i_i_type_load import *
 
-class rvfi_insn_lw(rvfi_insn_I):
+"""
-    def __init__(self):
+LW instruction
-        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
+class InsnLw(InsnRV32IITypeLoad):
-        addr = Signal(32)
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
-        m.d.comb += addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b010, 4, True)
-        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

insns/insn_mul.py

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

insns/insn_mulh.py

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

insns/insn_mulhsu.py

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

insns/insn_mulhu.py

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

insns/insn_or.py

@@ -1,21 +1,15 @@
-from insn_R import *
+from insn_rv32i_r_type import *
 
-class rvfi_insn_or(rvfi_insn_R):
+"""
-    def __init__(self):
+OR instruction
-        super(rvfi_insn_or, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_or, self).ports()
+class InsnOr(InsnRV32IRType):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b110, 0b0110011)
     def elaborate(self, platform):
-        m = super(rvfi_insn_or, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # OR instruction
+        m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata | self.rvfi_rs2_rdata, 0))
-        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

insns/insn_ori.py

@@ -1,20 +1,15 @@
-from insn_I import *
+from insn_rv32i_i_type_arith import *
 
-class rvfi_insn_ori(rvfi_insn_I):
+"""
-    def __init__(self):
+ORI instruction
-        super(rvfi_insn_ori, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_ori, self).ports()
+class InsnOri(InsnRV32IITypeArith):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b110)
     def elaborate(self, platform):
-        m = super(rvfi_insn_ori, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # ORI instruction
+        m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata | self.insn_imm, 0))
-        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

insns/insn_rem.py

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

insns/insn_remu.py

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

insns/insn_rv32i_i_type.py

@@ -0,0 +1,13 @@
+from insn import *
+
+"""
+RV32I I-Type Instruction
+"""
+
+class InsnRV32IIType(Insn):
+    def elaborate(self, platform):
+        m = super().elaborate(platform)
+
+        m.d.comb += self.insn_imm.eq(Value.as_signed(self.rvfi_insn[20:32]))
+
+        return m

insns/insn_rv32i_i_type_arith.py

@@ -0,0 +1,25 @@
+from insn_rv32i_i_type import *
+
+"""
+RV32I I-Type Instruction (Arithmetic Variation)
+"""
+
+class InsnRV32IITypeArith(InsnRV32IIType):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, funct3):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
+        self.funct3 = funct3
+    def elaborate(self, platform):
+        m = super().elaborate(platform)
+
+        if self.RISCV_FORMAL_CSR_MISA:
+            m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
+            m.d.comb += self.spec_csr_misa_rmask.eq(0)
+        else:
+            m.d.comb += self.misa_ok.eq(1)
+
+        m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == self.funct3) & (self.insn_opcode == 0b0010011))
+        m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
+        m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
+        m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
+
+        return m

insns/insn_rv32i_i_type_load.py

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

insns/insn_rv32i_i_type_shift.py

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

insns/insn_rv32i_r_type.py

@@ -0,0 +1,28 @@
+from insn import *
+
+"""
+RV32I R-Type Instruction
+"""
+
+class InsnRV32IRType(Insn):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, funct7, funct3, opcode):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
+        self.funct7 = funct7
+        self.funct3 = funct3
+        self.opcode = opcode
+    def elaborate(self, platform):
+        m = super().elaborate(platform)
+
+        if self.RISCV_FORMAL_CSR_MISA:
+            m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
+            m.d.comb += self.spec_csr_misa_rmask.eq(0)
+        else:
+            m.d.comb += self.misa_ok.eq(1)
+
+        m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct7 == self.funct7) & (self.insn_funct3 == self.funct3) & (self.insn_opcode == self.opcode))
+        m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
+        m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
+        m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
+        m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
+
+        return m

insns/insn_rv32i_s_type.py

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

insns/insn_rv32i_sb_type.py

@@ -0,0 +1,32 @@
+from insn import *
+
+"""
+RV32I SB-Type Instruction
+"""
+
+class InsnRV32ISBType(Insn):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_COMPRESSED, funct3):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
+        self.RISCV_FORMAL_COMPRESSED = RISCV_FORMAL_COMPRESSED
+        self.funct3 = funct3
+    def elaborate(self, platform):
+        m = super().elaborate(platform)
+
+        m.d.comb += self.insn_imm.eq(Value.as_signed(Cat(self.rvfi_insn[8:12], self.rvfi_insn[25:31], self.rvfi_insn[7], self.rvfi_insn[31]) << 1))
+
+        if self.RISCV_FORMAL_CSR_MISA:
+            m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
+            m.d.comb += self.spec_csr_misa_rmask.eq(4)
+            m.d.comb += self.ialign16.eq((self.rvfi_csr_misa_rdata & 4) != 0)
+        else:
+            m.d.comb += self.misa_ok.eq(1)
+            if self.RISCV_FORMAL_COMPRESSED:
+                m.d.comb += self.ialign16.eq(1)
+            else:
+                m.d.comb += self.ialign16.eq(0)
+
+        m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_funct3 == self.funct3) & (self.insn_opcode == 0b1100011))
+        m.d.comb += self.spec_rs1_addr.eq(self.insn_rs1)
+        m.d.comb += self.spec_rs2_addr.eq(self.insn_rs2)
+
+        return m

insns/insn_rv32i_u_type.py

@@ -0,0 +1,26 @@
+from insn import *
+
+"""
+RV32I U-Type Instruction
+"""
+
+class InsnRV32IUType(Insn):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, opcode):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA)
+        self.opcode = opcode
+    def elaborate(self, platform):
+        m = super().elaborate(platform)
+
+        m.d.comb += self.insn_imm.eq(Value.as_signed(self.rvfi_insn[12:32] << 12))
+
+        if self.RISCV_FORMAL_CSR_MISA:
+            m.d.comb += self.misa_ok.eq((self.rvfi_csr_misa_rdata & 0) == 0)
+            m.d.comb += self.spec_csr_misa_rmask.eq(0)
+        else:
+            m.d.comb += self.misa_ok.eq(1)
+
+        m.d.comb += self.spec_valid.eq(self.rvfi_valid & (~self.insn_padding) & (self.insn_opcode == self.opcode))
+        m.d.comb += self.spec_rd_addr.eq(self.insn_rd)
+        m.d.comb += self.spec_pc_wdata.eq(self.rvfi_pc_rdata + 4)
+
+        return m

insns/insn_sb.py

@@ -1,23 +1,9 @@
-from insn_S import *
+from insn_rv32i_s_type import *
 
-class rvfi_insn_sb(rvfi_insn_S):
+"""
-    def __init__(self):
+SB instruction
-        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
+class InsnSb(InsnRV32ISType):
-        addr = Signal(32)
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
-        m.d.comb += addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b000, 1)
-        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

insns/insn_sh.py

@@ -1,23 +1,9 @@
-from insn_S import *
+from insn_rv32i_s_type import *
 
-class rvfi_insn_sh(rvfi_insn_S):
+"""
-    def __init__(self):
+SH instruction
-        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
+class InsnSh(InsnRV32ISType):
-        addr = Signal(32)
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
-        m.d.comb += addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b001, 2)
-        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

insns/insn_sll.py

@@ -1,23 +1,15 @@
-from insn_R import *
+from insn_rv32i_r_type import *
 
-class rvfi_insn_sll(rvfi_insn_R):
+"""
-    def __init__(self):
+SLL instruction
-        super(rvfi_insn_sll, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_sll, self).ports()
+class InsnSll(InsnRV32IRType):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b001, 0b0110011)
     def elaborate(self, platform):
-        m = super(rvfi_insn_sll, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # SLL instruction
+        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))
-        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

insns/insn_slli.py

@@ -1,20 +1,15 @@
-from insn_I_shift import *
+from insn_rv32i_i_type_shift import *
 
-class rvfi_insn_slli(rvfi_insn_I_shift):
+"""
-    def __init__(self):
+SLLI instruction
-        super(rvfi_insn_slli, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_slli, self).ports()
+class InsnSlli(InsnRV32IITypeShift):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b000000, 0b001)
     def elaborate(self, platform):
-        m = super(rvfi_insn_slli, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # SLLI instruction
+        m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata << self.insn_shamt, 0))
-        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

insns/insn_slt.py

@@ -1,21 +1,15 @@
-from insn_R import *
+from insn_rv32i_r_type import *
 
-class rvfi_insn_slt(rvfi_insn_R):
+"""
-    def __init__(self):
+SLT instruction
-        super(rvfi_insn_slt, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_slt, self).ports()
+class InsnSlt(InsnRV32IRType):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b010, 0b0110011)
     def elaborate(self, platform):
-        m = super(rvfi_insn_slt, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # SLT instruction
+        m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, Value.as_signed(self.rvfi_rs1_rdata) < Value.as_signed(self.rvfi_rs2_rdata), 0))
-        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

insns/insn_slti.py

@@ -1,20 +1,15 @@
-from insn_I import *
+from insn_rv32i_i_type_arith import *
 
-class rvfi_insn_slti(rvfi_insn_I):
+"""
-    def __init__(self):
+SLTI instruction
-        super(rvfi_insn_slti, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_slti, self).ports()
+class InsnSlti(InsnRV32IITypeArith):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b010)
     def elaborate(self, platform):
-        m = super(rvfi_insn_slti, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # SLTI instruction
+        m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, Value.as_signed(self.rvfi_rs1_rdata) < Value.as_signed(self.insn_imm), 0))
-        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

insns/insn_sltiu.py

@@ -1,20 +1,15 @@
-from insn_I import *
+from insn_rv32i_i_type_arith import *
 
-class rvfi_insn_sltiu(rvfi_insn_I):
+"""
-    def __init__(self):
+SLTIU instruction
-        super(rvfi_insn_sltiu, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_sltiu, self).ports()
+class InsnSltiu(InsnRV32IITypeArith):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b011)
     def elaborate(self, platform):
-        m = super(rvfi_insn_sltiu, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # SLTIU instruction
+        m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata < self.insn_imm, 0))
-        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

insns/insn_sltu.py

@@ -1,21 +1,15 @@
-from insn_R import *
+from insn_rv32i_r_type import *
 
-class rvfi_insn_sltu(rvfi_insn_R):
+"""
-    def __init__(self):
+SLTU instruction
-        super(rvfi_insn_sltu, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_sltu, self).ports()
+class InsnSltu(InsnRV32IRType):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b011, 0b0110011)
     def elaborate(self, platform):
-        m = super(rvfi_insn_sltu, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # SLTU instruction
+        m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata < self.rvfi_rs2_rdata, 0))
-        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

insns/insn_sra.py

@@ -1,23 +1,15 @@
-from insn_R import *
+from insn_rv32i_r_type import *
 
-class rvfi_insn_sra(rvfi_insn_R):
+"""
-    def __init__(self):
+SRA instruction
-        super(rvfi_insn_sra, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_sra, self).ports()
+class InsnSra(InsnRV32IRType):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0100000, 0b101, 0b0110011)
     def elaborate(self, platform):
-        m = super(rvfi_insn_sra, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # SRA instruction
+        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
-        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

insns/insn_srai.py

@@ -1,20 +1,15 @@
-from insn_I_shift import *
+from insn_rv32i_i_type_shift import *
 
-class rvfi_insn_srai(rvfi_insn_I_shift):
+"""
-    def __init__(self):
+SRAI instruction
-        super(rvfi_insn_srai, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_srai, self).ports()
+class InsnSrai(InsnRV32IITypeShift):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b010000, 0b101)
     def elaborate(self, platform):
-        m = super(rvfi_insn_srai, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # SRAI instruction
+        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))
-        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

insns/insn_srl.py

@@ -1,23 +1,15 @@
-from insn_R import *
+from insn_rv32i_r_type import *
 
-class rvfi_insn_srl(rvfi_insn_R):
+"""
-    def __init__(self):
+SRL instruction
-        super(rvfi_insn_srl, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_srl, self).ports()
+class InsnSrl(InsnRV32IRType):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b100, 0b0110011)
     def elaborate(self, platform):
-        m = super(rvfi_insn_srl, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # SRL instruction
+        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))
-        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

insns/insn_srli.py

@@ -1,20 +1,15 @@
-from insn_I_shift import *
+from insn_rv32i_i_type_shift import *
 
-class rvfi_insn_srli(rvfi_insn_I_shift):
+"""
-    def __init__(self):
+SRLI instruction
-        super(rvfi_insn_srli, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_srli, self).ports()
+class InsnSrli(InsnRV32IITypeShift):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b000000, 0b101)
     def elaborate(self, platform):
-        m = super(rvfi_insn_srli, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # SRLI instruction
+        m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata >> self.insn_shamt, 0))
-        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

insns/insn_sub.py

@@ -1,21 +1,15 @@
-from insn_R import *
+from insn_rv32i_r_type import *
 
-class rvfi_insn_sub(rvfi_insn_R):
+"""
-    def __init__(self):
+SUB instruction
-        super(rvfi_insn_sub, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_sub, self).ports()
+class InsnSub(InsnRV32IRType):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0100000, 0b000, 0b0110011)
     def elaborate(self, platform):
-        m = super(rvfi_insn_sub, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # SUB instruction
+        m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata - self.rvfi_rs2_rdata, 0))
-        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

insns/insn_sw.py

@@ -1,23 +1,9 @@
-from insn_S import *
+from insn_rv32i_s_type import *
 
-class rvfi_insn_sw(rvfi_insn_S):
+"""
-    def __init__(self):
+SW instruction
-        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
+class InsnSw(InsnRV32ISType):
-        addr = Signal(32)
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM):
-        m.d.comb += addr.eq(self.rvfi_rs1_rdata + self.insn_imm)
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, RISCV_FORMAL_ALIGNED_MEM, 0b010, 4)
-        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

insns/insn_types.md

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

insns/insn_xor.py

@@ -1,21 +1,15 @@
-from insn_R import *
+from insn_rv32i_r_type import *
 
-class rvfi_insn_xor(rvfi_insn_R):
+"""
-    def __init__(self):
+XOR instruction
-        super(rvfi_insn_xor, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_xor, self).ports()
+class InsnXor(InsnRV32IRType):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b0000000, 0b100, 0b0110011)
     def elaborate(self, platform):
-        m = super(rvfi_insn_xor, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # XOR instruction
+        m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata ^ self.rvfi_rs2_rdata, 0))
-        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

insns/insn_xori.py

@@ -1,20 +1,15 @@
-from insn_I import *
+from insn_rv32i_i_type_arith import *
 
-class rvfi_insn_xori(rvfi_insn_I):
+"""
-    def __init__(self):
+XORI instruction
-        super(rvfi_insn_xori, self).__init__()
+"""
-    def ports(self):
+
-        return super(rvfi_insn_xori, self).ports()
+class InsnXori(InsnRV32IITypeArith):
+    def __init__(self, RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA):
+        super().__init__(RISCV_FORMAL_ILEN, RISCV_FORMAL_XLEN, RISCV_FORMAL_CSR_MISA, 0b100)
     def elaborate(self, platform):
-        m = super(rvfi_insn_xori, self).elaborate(platform)
+        m = super().elaborate(platform)
 
-        # XORI instruction
+        m.d.comb += self.spec_rd_wdata.eq(Mux(self.spec_rd_addr, self.rvfi_rs1_rdata ^ self.insn_imm, 0))
-        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

insns/isa_rv32i.txt

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

insns/isa_rv32i_gen.py

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

insns/isa_rv32im.txt

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

insns/isa_rv32im_gen.py

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