Verification baseline

riscvmodel/golden.py

@@ -0,0 +1,96 @@
+from abc import ABCMeta, abstractmethod
+from collections import deque
+
+from .variant import Variant
+from .model import Model, Memory
+from .isa import InstructionNOP
+from .program import Program
+from .types import RVFISignals, TraceIntegerRegister, Register
+from .code import decode
+
+
+class GoldenException(Exception):
+    pass
+
+
+class GoldenProgramEndException(Exception):
+    pass
+
+
+class Golden(metaclass=ABCMeta):
+    def __init__(self, variant: Variant):
+        self.model = Model(variant)
+        self.memory = Memory()
+        self.program = None
+
+    @abstractmethod
+    def fetch(self, pc):
+        pass
+
+
+class GoldenUnbuffered(Golden):
+    def __init__(self, variant: Variant, *, pc: int = 0):
+        super().__init__(variant)
+        self.reset(pc=pc)
+
+    def fetch(self, pc):
+        if self.pc != pc:
+            raise GoldenException("Unexpected fetch PC: {}, expected {}".format(pc, self.pc))
+        try:
+            insn = self.program[pc >> 2]
+        except IndexError:
+            raise GoldenProgramEndException()
+        self.issued.append(insn)
+        self.pc += 4
+        return insn
+
+    def commit(self, trace, *, insn = None):
+        if not isinstance(trace, list):
+            trace = [trace]
+
+        # Test if any other exceptions are issued and get in order
+        try:
+            exp = self.issued.popleft()
+        except IndexError:
+            # If not we may be able to verify this is a NOP, then its okay. If no NOP, its probably okay too..
+            if insn is not None:
+                if insn != InstructionNOP():
+                    raise GoldenProgramEndException()
+            raise GoldenProgramEndException()
+
+        # If we got an instruction check if it matches
+        if insn is not None:
+            if exp != insn:
+                raise GoldenException("Expected instruction: {}, expected {}".format(insn, exp))
+
+        # Execute the expected instruction and verify the state is the same
+        exp_trace = self.model.issue(exp)
+        if not self.model.check(trace):
+            print(exp_trace)
+            raise GoldenException("Unexpected state change: {}, expected: {}".format(",".join([str(t) for t in trace]),
+                                                                                     ",".join([str(t) for t in exp_trace])))
+
+
+    def reset(self, *, pc: int = 0):
+        self.model.reset(pc=pc)
+        self.pc = pc
+        self.issued = deque()
+
+    def load_program(self, pgm: Program):
+        self.program = pgm.insns
+
+
+def traces_from_rvfi(rvfi: RVFISignals) -> list:
+    insn = decode(rvfi.insn)
+    if rvfi.valid != 1:
+        return []
+    t = []
+    if rvfi.rd_addr == 0 and rvfi.rd_wdata != 0:
+        raise ValueError("rd[0] cannot be written by core")
+    if rvfi.rd_addr != 0:
+        if "rd" in insn.__dict__:
+            reg = Register(32)
+            reg.set(rvfi.rd_wdata)
+            t.append(TraceIntegerRegister(rvfi.rd_addr, reg))
+
+    return t

riscvmodel/insn.py

@@ -66,6 +66,8 @@ def __setattr__(self, key, value):
             raise AttributeError("Instruction does not allow to overwrite immediates, use set() on them")
         super().__setattr__(key, value)
 
+    def __eq__(self, other):
+        return self._opcode == other._opcode and self._funct3 == other._funct3 and self._funct7 == other._funct7
 
 class InstructionRType(Instruction):
     """
@@ -102,6 +104,10 @@ def encode(self) -> int:
     def __str__(self):
         return "{} x{}, x{}, x{}".format(self._mnemonic, self.rd, self.rs1, self.rs2)
 
+    def __eq__(self, other):
+        if not super().__eq__(other):
+            return False
+        return self.rs1 == other.rs1 and self.rs2 == other.rs2 and self.rd == other.rd
 
 class InstructionIType(Instruction):
     """
@@ -144,6 +150,10 @@ def encode(self) -> int:
     def __str__(self):
         return "{} x{}, x{}, {}".format(self._mnemonic, self.rd, self.rs1, self.imm)
 
+    def __eq__(self, other):
+        if not super().__eq__(other):
+            return False
+        return self.rd == other.rd and self.rs1 == other.rs1 and self.imm == other.imm
 
 class InstructionILType(InstructionIType):
     """
@@ -194,6 +204,11 @@ def randomize(self, variant: Variant):
     def __str__(self):
         return "{} x{}, x{}, 0x{:02x}".format(self._mnemonic, self.rd, self.rs1, self.shamt)
 
+    def __eq__(self, other):
+        if not super().__eq__(other):
+            return False
+        return self.rd == other.rd and self.rs2 == other.rs2 and self.shamt == other.shamt
+
 
 class InstructionSType(Instruction):
     """
@@ -236,6 +251,11 @@ def encode(self) -> int:
     def __str__(self):
         return "{} x{}, {}(x{})".format(self._mnemonic, self.rs2, self.imm, self.rs1)
 
+    def __eq__(self, other):
+        if not super().__eq__(other):
+            return False
+        return self.rs1 == other.rs1 and self.rs2 == other.rs2 and self.imm == other.imm
+
 
 class InstructionBType(Instruction):
     """
@@ -283,6 +303,11 @@ def encode(self) -> int:
     def __str__(self):
         return "{} x{}, x{}, .{:+}".format(self._mnemonic, self.rs1, self.rs2, self.imm)
 
+    def __eq__(self, other):
+        if not super().__eq__(other):
+            return False
+        return self.rs1 == other.rs1 and self.rs2 == other.rs2 and self.imm == other.imm
+
 
 class InstructionUType(Instruction):
     """
@@ -314,6 +339,11 @@ def encode(self):
     def __str__(self):
         return "{} x{}, {}".format(self._mnemonic, self.rd, self.imm)
 
+    def __eq__(self, other):
+        if not super().__eq__(other):
+            return False
+        return self.rd == other.rd and self.imm == other.imm
+
 
 class InstructionJType(Instruction):
     """
@@ -355,6 +385,10 @@ def encode(self):
     def __str__(self):
         return "{} x{}, .{:+}".format(self._mnemonic, self.rd, self.imm)
 
+    def __eq__(self, other):
+        if not super().__eq__(other):
+            return False
+        return self.rd == other.rd and self.imm == other.imm
 
 def isa(mnemonic: str, opcode: int, funct3: int=None, funct7: int=None):
     """
@@ -394,6 +428,18 @@ def _match(machinecode: int):
     return wrapper
 
 
+def isa_pseudo():
+    def wrapper(wrapped):
+        class WrappedClass(wrapped):
+            _pseudo = True
+
+        WrappedClass.__name__ = wrapped.__name__
+        WrappedClass.__module__ = wrapped.__module__
+        WrappedClass.__qualname__ = wrapped.__qualname__
+        return WrappedClass
+    return wrapper
+
+
 def get_insns(cls = None):
     """
     Get all Instructions. This is based on all known subclasses of `cls`. If non is given, all Instructions are returned.

riscvmodel/isa.py

@@ -247,3 +247,9 @@ def execute(self, model: State):
 class InstructionAND(InstructionRType):
     def execute(self, model: State):
         model.intreg[self.rd] = model.intreg[self.rs1] & model.intreg[self.rs2]
+
+
+@isa_pseudo()
+class InstructionNOP(InstructionADDI):
+    def __init__(self):
+        super().__init__(0, 0, 0)

riscvmodel/model.py

@@ -1,64 +1,54 @@
 from random import randrange
 
 from .variant import *
-from .types import Register, RegisterFile
+from .types import Register, RegisterFile, TracePC, TraceIntegerRegister, TraceMemory
 from .program import Program
 
-
 # todo: raise exception on memory misalignment
 class State(object):
     def __init__(self, variant: Variant):
         self.variant = variant
         self.intreg = RegisterFile(variant.intregs, 32, {0: 0x0})
         self.pc = Register(32)
         self.pc_update = Register(32)
+        self.memory = Memory()
         self.initialized = True
-        self.memory = {}
-        self.memory_update = None
 
     def randomize(self):
         self.intreg.randomize()
 
     def changes(self):
-        intregs = self.intreg.changes()
-        c = ["x{} = {}".format(r, c[1]) for r, c in intregs.items()]
+        c = self.intreg.changes()
         if self.pc_update.value != self.pc.value + 4:
-            c.append("pc = {}".format(self.pc_update))
-        if self.memory_update is not None:
-            if self.memory_update[0] == 1:
-                data = "{:02x}".format(self.memory_update[2] & 0xFF)
-            elif self.memory_update[0] == 2:
-                data = "{:04x}".format(self.memory_update[2] & 0xFFFF)
-            else:
-                data = "{:08x}".format(self.memory_update[2])
-            c.append("mem[{}] = {}".format(self.memory_update[1], data))
-        if len(c) == 0:
-            return "no change"
-        else:
-            return ", ".join(c)
+            c.append(TracePC(self.pc_update.value))
+        c += self.memory.changes()
+        return c
 
     def commit(self):
         self.intreg.commit()
         self.pc.set(self.pc_update.value)
-        if self.memory_update is not None:
-            address = self.memory_update[1]
-            base = address >> 2
-            offset = address & 0x3
-            if base not in self.memory:
-                self.memory[base] = randrange(0, 1 << 32)
-            data = self.memory_update[2]
-            if self.memory_update[0] == 1:
-                mask = ~(0xFF << (offset*8)) & 0xFFFFFFFF
-                data = (self.memory[base] & mask) | (data << (offset*8))
-            elif self.memory_update[0] == 2:
-                mask = ~(0xFF << (offset*8)) & 0xFFFFFFFF
-                data = (self.memory[base] & mask) | (data << (offset*8))
-            self.memory[base] = data
-            self.memory_update = None
+        self.memory.commit()
 
     def reset(self, pc = 0):
         self.pc.set(pc)
 
+    def __setattr__(self, key, value):
+        if key is "pc" and "pc_update" in self.__dict__:
+            self.pc_update.set(value)
+        else:
+            super().__setattr__(key, value)
+
+    def __str__(self):
+        return "{}".format(self.intreg)
+
+
+class Memory(object):
+    def __init__(self, *, base: int = 0, size: int = 2^32):
+        self.base = base
+        self.size = size
+        self.memory = {}
+        self.memory_updates = []
+
     def lb(self, address):
         word = address >> 2
         offset = address % 4
@@ -80,36 +70,50 @@ def lw(self, address):
         return self.memory[word]
 
     def sb(self, address, data):
-        self.memory_update = (1, address, int(data) & 0xFF)
+        self.memory_updates.append(TraceMemory(TraceMemory.GRANULARITY.BYTE, address, int(data) & 0xFF))
 
     def sh(self, address, data):
-        self.memory_update = (2, address, int(data) & 0xFFFF)
+        self.memory_updates.append(TraceMemory(TraceMemory.GRANULARITY.HALFWORD, address, int(data) & 0xFFFF))
 
     def sw(self, address, data):
-        self.memory_update = (4, address, int(data) & 0xFFFFFFFF)
+        self.memory_updates.append(TraceMemory(TraceMemory.GRANULARITY.WORD, address, int(data) & 0xFFFFFFFF))
 
-    def __setattr__(self, key, value):
-        if key is "pc" and "pc_update" in self.__dict__:
-            self.pc_update.set(value)
-        else:
-            super().__setattr__(key, value)
+    def changes(self):
+        return self.memory_updates
 
-    def __str__(self):
-        return "{}".format(self.intreg)
+    def commit(self):
+        for update in self.memory_updates:
+            address = update[1]
+            base = address >> 2
+            offset = address & 0x3
+            if base not in self.memory:
+                self.memory[base] = randrange(0, 1 << 32)
+            data = update[2]
+            if update[0] == 1:
+                mask = ~(0xFF << (offset*8)) & 0xFFFFFFFF
+                data = (self.memory[base] & mask) | (data << (offset*8))
+            elif update[0] == 2:
+                mask = ~(0xFF << (offset*8)) & 0xFFFFFFFF
+                data = (self.memory[base] & mask) | (data << (offset*8))
+            self.memory[base] = data
+
+        self.memory_updates = []
 
 
 class Model(object):
-    def __init__(self, variant: Variant, *, golden = False, verbose = False):
+    def __init__(self, variant: Variant, *, verbose = False):
         self.state = State(variant)
-        self.golden = golden
         self.verbose = verbose
 
     def issue(self, insn):
         self.state.pc += 4
+        expected_pc = self.state.pc
         insn.execute(self.state)
+        trace = self.state.changes()
         if self.verbose:
-            print("{:20} | {}".format(str(insn), self.state.changes()))
+            print("{:20} | {}".format(str(insn), trace))
         self.state.commit()
+        return trace
 
     def execute(self, insn):
         if isinstance(insn, Program):
@@ -123,6 +127,12 @@ def execute(self, insn):
     def randomize(self):
         self.state.randomize()
 
-    def reset(self, pc: int = 0):
+    def reset(self, *, pc: int = 0):
         self.state.reset(pc)
 
+    def check(self, traces):
+        for t in traces:
+            if isinstance(t, TraceIntegerRegister):
+                if int(self.state.intreg[t.id]) != int(t.value):
+                    return False
+        return True