Completeness check

Refactor `InstructionChecker` to subclass `InstructionCheckerBase`.
Add `CompleteIsaChecker` which also subclasses the same, with adjustments to perform ISA completeness checking.
`CompleteIsaChecker` takes two lists, one for valid opcodes (compared against `rvfi.insn[6:0]`), and one for arbitrary (combinatorial) validity checks (tested NERV under `base_isa` with a skip for `if key == "lb"`, included commented out here so I don't forget how I did it).
Refactor submodule `__init__.py` files to import instead of assign (which works better with VSCode for code following).
Move base rvfi observers into `base_observers` function in `rvfi` submodule.
Also split `defined_checks` into a method call.

Author: KrystalDelusion

src/checks/__init__.py

@@ -1,3 +1,6 @@
-from . import generic_checker
+from .generic_checker import GenericChecker
 
-GenericChecker = generic_checker.GenericChecker
+from .instruction_checker import (
+    InstructionChecker,
+    CompleteISAChecker,
+)

src/checks/base_isa.py

@@ -4,48 +4,15 @@
 
 import click
 
-from .instruction_checker import InstructionChecker
+from . import InstructionChecker, CompleteISAChecker
 from ..insns import Instruction, builtins
 from ..rvfi import (
-    Observer,
-    SpeculativeObserver,
-    ZeroedObserver,
+    base_observers,
     SpeculativeEvaluation,
 )
 
-def dump_isa(
-    name: str,
-    insns: dict[str, Instruction],
-    xlen: int,
-    format: str,
-    channel: Optional[int] = None,
-    channelized: bool = True,
-) -> str:
-    rvfi: dict[str, Observer] = {o.name: o for o in [
-        SpeculativeObserver("valid", "1"),
-                   Observer("order", "64"),
-                   Observer("insn", "`RISCV_FORMAL_ILEN"),
-        SpeculativeObserver("trap", "1"),
-                   Observer("halt", "1"),
-                   Observer("intr", "1"),
-                   Observer("mode", "2"),
-                   Observer("ixl", "2"),
-        SpeculativeObserver("rs1_addr", "5", "rvfi.rs1_addr"),
-        SpeculativeObserver("rs2_addr", "5", "rvfi.rs2_addr"),
-             ZeroedObserver("rs1_rdata", "`RISCV_FORMAL_XLEN", "spec_rs1_addr == 0"),
-             ZeroedObserver("rs2_rdata", "`RISCV_FORMAL_XLEN", "spec_rs2_addr == 0"),
-        SpeculativeObserver("rd_addr", "5"),
-        SpeculativeObserver("rd_wdata", "`RISCV_FORMAL_XLEN"),
-                   Observer("pc_rdata", "`RISCV_FORMAL_XLEN"),
-        SpeculativeObserver("pc_wdata", "`RISCV_FORMAL_XLEN", "rvfi.pc_rdata + 4"),
-        SpeculativeObserver("mem_addr", "`RISCV_FORMAL_XLEN"),
-        SpeculativeObserver("mem_rmask", "`RISCV_FORMAL_XLEN/8"),
-        SpeculativeObserver("mem_wmask", "`RISCV_FORMAL_XLEN/8"),
-                   Observer("mem_rdata", "`RISCV_FORMAL_XLEN"),
-        SpeculativeObserver("mem_wdata", "`RISCV_FORMAL_XLEN"),
-    ]}
-
-    defined_checks: list[SpeculativeEvaluation] = [
+def base_checks() -> list[SpeculativeEvaluation]:
+    return [
         SpeculativeEvaluation(
             "if (rvfi.rs1_addr == 0) assert(rvfi.rs1_rdata == 0);",
             ignore_trap = True,
@@ -81,13 +48,39 @@ def dump_isa(
         ),
     ]
 
+def dump_isa(
+    name: str,
+    insns: dict[str, Instruction],
+    xlen: int,
+    format: str,
+    channel: Optional[int] = None,
+    channelized: bool = True,
+) -> str:
+    rvfi = base_observers()
+    defined_checks = base_checks()
+
+    # checks base_isa with a missing lb insn check
+    # isa_checker = CompleteISAChecker(
+    #     name = name,
+    #     instructions = insns,
+    #     observers = rvfi,
+    #     channel = channel,
+    #     channelized = channelized if channelized is not None else channel is not None,
+    #     valid_opcodes = [
+    #         "1110011", # SYSTEM
+    #     ], 
+    #     extra_valid_checks = [
+    #         "rvfi.insn[14:12] == 3'b 000 && rvfi.insn[6:0] == 7'b 0000011", # lb
+    #     ]
+    # )
+
     isa_checker = InstructionChecker(
         name = name,
         instructions = insns,
         observers = rvfi,
         defined_checks = defined_checks,
         channel = channel,
-        channelized = channelized if channelized is not None else channel is not None
+        channelized = channelized if channelized is not None else channel is not None,
     )
 
     isa_checker.configure_io()

src/checks/instruction_checker.py

@@ -11,42 +11,26 @@
     SpeculativeEvaluation,
 )
 
+
 @dataclass(kw_only=True)
-class InstructionChecker(GenericChecker):
+class InstructionCheckerBase(GenericChecker):
     instructions: dict[str, Instruction] = field(default_factory=dict)
     observers: dict[str, Observer] = field(default_factory=dict)
 
-    defined_checks: list[SpeculativeEvaluation] = field(default_factory=list)
-
-    registered_checks: ClassVar[list[SpeculativeEvaluation]] = []
-    registered_verilog: ClassVar[list[str]] = []
     registered_speculators: ClassVar[dict[str, tuple[SpeculativeObserver, Callable[[Instruction], Optional[str]]]]] = {}
-    registered_hw_traps: ClassVar[dict[str, Callable[[dict[str, Observer]], str]]] = {}
 
     def configure_io(self):
         for insn in self.instructions.values():
             insn.select_inputs(self.observers.values())
             insn.select_outputs([o for o in self.observers.values() if isinstance(o, SpeculativeObserver)])
 
-    @classmethod
-    def register_check(cls, check: SpeculativeEvaluation):
-        cls.registered_checks.append(check)
-
-    @classmethod
-    def register_verilog(cls, verilog: str):
-        cls.registered_verilog.append(verilog)
-
     @classmethod
     def register_speculator(cls,
         spec_obs: SpeculativeObserver,
         speculator: Callable[[Instruction], Optional[str]],
     ):
         cls.registered_speculators[spec_obs.name] = (spec_obs, speculator)
 
-    @classmethod
-    def register_hw_trap(cls, condition: str, handler: Callable[[dict[str, Observer]], str]):
-        cls.registered_hw_traps[condition] = handler
-
     def _v_io(self) -> str:
         # macro defined RVFI inputs
         return dedent("""\
@@ -124,6 +108,47 @@ def _v_instantiation(self) -> str:
             v_str += "    end"
         v_str += "\nend\n"
 
+        return v_str
+
+    def _v_spec_check(self) -> str:
+        raise NotImplementedError()
+
+    def _v_body(self) -> str:
+        v_str = self._v_format_block(self._v_rvfi_channel())
+        v_str += self._v_format_block(self._v_instantiation())
+        v_str += self._v_format_block(self._v_spec_check())
+        return v_str
+
+    def to_verilog(self, xlen: int):
+        v_str = ""
+        for insn in self.instructions.values():
+            v_str += insn.to_verilog(xlen) + '\n\n'
+        return v_str + super().to_verilog()
+
+
+@dataclass(kw_only=True)
+class InstructionChecker(InstructionCheckerBase):
+    defined_checks: list[SpeculativeEvaluation] = field(default_factory=list)
+
+    registered_checks: ClassVar[list[SpeculativeEvaluation]] = []
+    registered_verilog: ClassVar[list[str]] = []
+    registered_hw_traps: ClassVar[dict[str, Callable[[dict[str, Observer]], str]]] = {}
+
+    @classmethod
+    def register_check(cls, check: SpeculativeEvaluation):
+        cls.registered_checks.append(check)
+
+    @classmethod
+    def register_verilog(cls, verilog: str):
+        cls.registered_verilog.append(verilog)
+
+    @classmethod
+    def register_hw_trap(cls, condition: str, handler: Callable[[dict[str, Observer]], str]):
+        cls.registered_hw_traps[condition] = handler
+
+    def _v_instantiation(self) -> str:
+        v_str = super()._v_instantiation()
+
         if self.registered_verilog:
             v_str += "\n"
             v_str += "\n\n".join(self.registered_verilog)
@@ -180,14 +205,42 @@ def _v_spec_check(self) -> str:
         )
         return v_str
 
-    def _v_body(self) -> str:
-        v_str = self._v_format_block(self._v_rvfi_channel())
-        v_str += self._v_format_block(self._v_instantiation())
-        v_str += self._v_format_block(self._v_spec_check())
-        return v_str
 
-    def to_verilog(self, xlen: int):
+@dataclass(kw_only=True)
+class CompleteISAChecker(InstructionCheckerBase):
+    valid_opcodes: list[str] = field(default_factory=list)
+    extra_valid_checks: list[str] = field(default_factory=list)
+
+    def _v_spec_check(self) -> str:
         v_str = ""
-        for insn in self.instructions.values():
-            v_str += insn.to_verilog(xlen) + '\n\n'
-        return v_str + super().to_verilog()
+
+        v_str += "wire opcode_valid = "
+        if self.valid_opcodes:
+            op_checks: list[str] = []
+            for op in self.valid_opcodes:
+                if len(op) == 7:
+                    try:
+                        int(op, 2)
+                    except ValueError:
+                        # not valid binary
+                        pass
+                    else:
+                        op = f"7'b {op}"
+                op_checks.append(f"(rvfi.insn[6:0] == {op})")
+            v_str += "\n    || ".join(op_checks)
+        else:
+            v_str += "0"
+        v_str += ";\n\n"
+
+        v_str += "wire extra_valid = "
+        v_str += "\n    || ".join(f"({check})" for check in self.extra_valid_checks) or "0"
+        v_str += ";\n\n"
+
+        v_str +=dedent("""\
+            always @* begin
+                if (!reset && rvfi.valid && !rvfi.trap && !opcode_valid && !extra_valid) begin
+                    assert(spec_valid && !spec_trap);
+                end
+            end""")
+
+        return v_str

src/insns/__init__.py

@@ -1,7 +1,9 @@
-from . import model, wrapped_model, builtins
+from .model import (
+    Instruction,
+    MemoryInstruction,
+    AltopsInstruction,
+)
 
-Instruction = model.Instruction
-MemoryInstruction = model.MemoryInstruction
-AltopsInstruction = model.AltopsInstruction
-WrappedInstruction = wrapped_model.WrappedInstruction
-builtins = builtins.builtins
+from .wrapped_model import WrappedInstruction
+
+from .builtins import builtins

src/rvfi/__init__.py

@@ -1,7 +1,9 @@
-from . import observer, speculative_evaluation
+from .observer import (    
+    Observer, 
+    SpeculativeObserver, 
+    ZeroedObserver, 
+)
 
-Observer = observer.Observer
-SpeculativeObserver = observer.SpeculativeObserver
-ZeroedObserver = observer.ZeroedObserver
+from .speculative_evaluation import SpeculativeEvaluation
 
-SpeculativeEvaluation = speculative_evaluation.SpeculativeEvaluation
+from .base import base_observers

src/rvfi/base.py

@@ -0,0 +1,26 @@
+from .observer import Observer, SpeculativeObserver, ZeroedObserver
+
+def base_observers() -> dict[str, Observer]:
+    return {o.name: o for o in [
+        SpeculativeObserver("valid", "1"),
+                   Observer("order", "64"),
+                   Observer("insn", "`RISCV_FORMAL_ILEN"),
+        SpeculativeObserver("trap", "1"),
+                   Observer("halt", "1"),
+                   Observer("intr", "1"),
+                   Observer("mode", "2"),
+                   Observer("ixl", "2"),
+        SpeculativeObserver("rs1_addr", "5", "rvfi.rs1_addr"),
+        SpeculativeObserver("rs2_addr", "5", "rvfi.rs2_addr"),
+             ZeroedObserver("rs1_rdata", "`RISCV_FORMAL_XLEN", "spec_rs1_addr == 0"),
+             ZeroedObserver("rs2_rdata", "`RISCV_FORMAL_XLEN", "spec_rs2_addr == 0"),
+        SpeculativeObserver("rd_addr", "5"),
+        SpeculativeObserver("rd_wdata", "`RISCV_FORMAL_XLEN"),
+                   Observer("pc_rdata", "`RISCV_FORMAL_XLEN"),
+        SpeculativeObserver("pc_wdata", "`RISCV_FORMAL_XLEN", "rvfi.pc_rdata + 4"),
+        SpeculativeObserver("mem_addr", "`RISCV_FORMAL_XLEN"),
+        SpeculativeObserver("mem_rmask", "`RISCV_FORMAL_XLEN/8"),
+        SpeculativeObserver("mem_wmask", "`RISCV_FORMAL_XLEN/8"),
+                   Observer("mem_rdata", "`RISCV_FORMAL_XLEN"),
+        SpeculativeObserver("mem_wdata", "`RISCV_FORMAL_XLEN"),
+    ]}

src/rvfi/mem_fault.py

@@ -1,6 +1,6 @@
 from textwrap import dedent
 
-from ..checks.instruction_checker import InstructionChecker
+from ..checks import InstructionChecker
 from .observer import Observer
 
 def mem_fault_handler(observers: dict[str, Observer]) -> str:

src/rvfi/misa_fault.py

@@ -1,10 +1,13 @@
 from textwrap import dedent
 from typing import Optional
 
-from ..checks.instruction_checker import InstructionChecker
+from ..checks import InstructionChecker
 from ..insns import Instruction
-from .observer import Observer, SpeculativeObserver
-from . import SpeculativeEvaluation
+from . import (
+    Observer,
+    SpeculativeObserver,
+    SpeculativeEvaluation,
+)
 
 MISA_MAP = {
     "A": 1 <<  0, # Atomic