From 331e4b76bae002b90b6abfe42b2691422b767b46 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jean-Fran=C3=A7ois=20Nguyen?= Date: Wed, 24 Aug 2022 11:04:10 +0200 Subject: [PATCH] insn: use records to define instruction encodings. Before this commit, instructions were defined by a sequence of Const for fixed fields (e.g. PO/XO) and AnyConst for others (e.g. operands). This approach restricted their use to BMC use-cases, and prevented them from appearing in VCD traces. After this commit, an instruction encoding is defined by a Record. As fields can now be set to arbitrary values, the corresponding InsnSpec will only assert `pfv.stb` if `pfv.insn` matches a valid encoding (i.e. fixed fields have correct values). On the other side, BMC testbenches will drive `pfv.insn` with an AnyConst, and assume `pfv.stb` is high. --- power_fv/check/insn/__init__.py | 3 ++ power_fv/insn/__init__.py | 73 +++++++++++---------------------- power_fv/insn/spec/addsub.py | 4 +- power_fv/insn/spec/bcd.py | 4 +- power_fv/insn/spec/branch.py | 4 +- power_fv/insn/spec/byterev.py | 4 +- power_fv/insn/spec/compare.py | 4 +- power_fv/insn/spec/cr.py | 12 ++---- power_fv/insn/spec/loadstore.py | 4 +- power_fv/insn/spec/logical.py | 4 +- power_fv/insn/spec/msr.py | 4 +- power_fv/insn/spec/muldiv.py | 8 ++-- power_fv/insn/spec/rotate.py | 4 +- power_fv/insn/spec/spr.py | 4 +- power_fv/insn/spec/syscall.py | 4 +- power_fv/insn/spec/trap.py | 4 +- 16 files changed, 58 insertions(+), 86 deletions(-) diff --git a/power_fv/check/insn/__init__.py b/power_fv/check/insn/__init__.py index 09203f8..138e0d0 100644 --- a/power_fv/check/insn/__init__.py +++ b/power_fv/check/insn/__init__.py @@ -50,8 +50,11 @@ class InsnTestbench(Elaboratable): m.submodules.spec = spec = self.check.spec m.d.comb += [ + spec.pfv.insn .eq(AnyConst(spec.pfv.insn.shape())), spec.pfv.order.eq(dut.pfv.order), spec.pfv.cia .eq(dut.pfv.cia), + + Assume(spec.pfv.stb), ] with m.If(t_post.zero): diff --git a/power_fv/insn/__init__.py b/power_fv/insn/__init__.py index 31a4cf9..29c754e 100644 --- a/power_fv/insn/__init__.py +++ b/power_fv/insn/__init__.py @@ -1,8 +1,6 @@ from operator import attrgetter from amaranth import * -from amaranth.asserts import AnyConst -from amaranth.hdl.ast import ValueCastable, Value __all__ = ["InsnField", "WordInsn"] @@ -35,38 +33,34 @@ class InsnField: .format(value)) self._value = value - def as_const(self): - if self.value is not None: - return Const(self.value, self.shape) - else: - return AnyConst(self.shape) - -class WordInsn(ValueCastable): +class WordInsn(Record): SIZE = 32 - def __init__(self): - value_map = {} - field_map = {} + def __init__(self, name=None, src_loc_at=0): curr_offset = 0 + layout = [] + pattern = "" - for field in sorted(self.fields, key=attrgetter('offset')): + for field in sorted(self._fields, key=attrgetter("offset")): if not isinstance(field, InsnField): raise TypeError("Field must be an instance of InsnField, not {!r}" .format(field)) - if field.name in field_map: - raise ValueError("Duplicate field name '{}'".format(field.name)) if curr_offset > field.offset: raise ValueError("Field '{}' at offset {} overlaps with its predecessor" .format(field.name, field.offset)) # Add undefined bits located between this field and its predecessor. if curr_offset < field.offset: - undef_bits = AnyConst(unsigned(field.offset - curr_offset)) - value_map[curr_offset] = undef_bits + undef_bits = field.offset - curr_offset + layout.append((f"_{curr_offset}", unsigned(undef_bits))) + pattern += "-" * undef_bits - value_map[field.offset] = field.as_const() - field_map[field.name ] = field + layout.append((field.name, field.shape)) + if field.value is not None: + pattern += "{:0{}b}".format(field.value, field.shape.width) + else: + pattern += "-" * field.shape.width curr_offset = field.offset + field.shape.width @@ -75,37 +69,16 @@ class WordInsn(ValueCastable): # Add undefined bits located after the last field. if curr_offset < self.SIZE: - undef_bits = AnyConst(unsigned(self.SIZE - curr_offset)) - value_map[curr_offset] = undef_bits + undef_bits = self.SIZE - curr_offset + layout.append((f"_{curr_offset}", unsigned(undef_bits))) + pattern += "-" * undef_bits - self.field_map = field_map - self.value_map = value_map + self._pattern = pattern + super().__init__(reversed(layout), name=name, src_loc_at=1 + src_loc_at) @property - def fields(self): - return self._fields - - def __getattr__(self, name): - return self[name] - - def __getitem__(self, item): - if isinstance(item, str): - try: - field = self.field_map[item] - except KeyError: - raise AttributeError("WordInsn {!r} does not have a field '{}'" - .format(self, item)) - value = self.value_map[field.offset] - return value - else: - try: - return Value.__getitem__(self, item) - except KeyError: - raise AttributeError("WordInsn {!r} does not have a field '{}'" - .format(self, item)) - - @ValueCastable.lowermethod - def as_value(self): - value = Cat(v for o, v in sorted(self.value_map.items(), reverse=True)) - assert len(value) == self.SIZE - return value + def pattern(self): + return self._pattern + + def is_valid(self): + return self.as_value().matches(self.pattern) diff --git a/power_fv/insn/spec/addsub.py b/power_fv/insn/spec/addsub.py index 4b0a675..1dfc0d2 100644 --- a/power_fv/insn/spec/addsub.py +++ b/power_fv/insn/spec/addsub.py @@ -15,8 +15,8 @@ class AddSubSpec(InsnSpec, Elaboratable): m = Module() m.d.comb += [ - self.pfv.stb .eq(1), - self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), + self.insn .eq(self.pfv.insn[32:]), + self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()), self.pfv.intr.eq(0), self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), self.pfv.msr.r_mask.sf.eq(1), diff --git a/power_fv/insn/spec/bcd.py b/power_fv/insn/spec/bcd.py index 88b1b61..a473cd2 100644 --- a/power_fv/insn/spec/bcd.py +++ b/power_fv/insn/spec/bcd.py @@ -15,8 +15,8 @@ class BCDAssistSpec(InsnSpec, Elaboratable): m = Module() m.d.comb += [ - self.pfv.stb .eq(1), - self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), + self.insn .eq(self.pfv.insn[32:]), + self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()), self.pfv.intr.eq(0), self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), self.pfv.msr.r_mask.sf.eq(1), diff --git a/power_fv/insn/spec/branch.py b/power_fv/insn/spec/branch.py index e54427c..55d171d 100644 --- a/power_fv/insn/spec/branch.py +++ b/power_fv/insn/spec/branch.py @@ -16,8 +16,8 @@ class BranchSpec(InsnSpec, Elaboratable): m = Module() m.d.comb += [ - self.pfv.stb .eq(1), - self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), + self.insn .eq(self.pfv.insn[32:]), + self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()), self.pfv.msr.r_mask.sf.eq(1), ] diff --git a/power_fv/insn/spec/byterev.py b/power_fv/insn/spec/byterev.py index a084660..18fd638 100644 --- a/power_fv/insn/spec/byterev.py +++ b/power_fv/insn/spec/byterev.py @@ -15,8 +15,8 @@ class ByteReverseSpec(InsnSpec, Elaboratable): m = Module() m.d.comb += [ - self.pfv.stb .eq(1), - self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), + self.insn .eq(self.pfv.insn[32:]), + self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()), self.pfv.intr.eq(0), self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), self.pfv.msr.r_mask.sf.eq(1), diff --git a/power_fv/insn/spec/compare.py b/power_fv/insn/spec/compare.py index f9caaf2..286370a 100644 --- a/power_fv/insn/spec/compare.py +++ b/power_fv/insn/spec/compare.py @@ -15,8 +15,8 @@ class CompareSpec(InsnSpec, Elaboratable): m = Module() m.d.comb += [ - self.pfv.stb .eq(1), - self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), + self.insn .eq(self.pfv.insn[32:]), + self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()), self.pfv.intr.eq(0), self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), self.pfv.msr.r_mask.sf.eq(1), diff --git a/power_fv/insn/spec/cr.py b/power_fv/insn/spec/cr.py index ff14ddb..1b17209 100644 --- a/power_fv/insn/spec/cr.py +++ b/power_fv/insn/spec/cr.py @@ -18,8 +18,8 @@ class CRLogicalSpec(InsnSpec, Elaboratable): m = Module() m.d.comb += [ - self.pfv.stb .eq(1), - self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), + self.insn .eq(self.pfv.insn[32:]), + self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()), self.pfv.intr.eq(0), self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), self.pfv.msr.r_mask.sf.eq(1), @@ -70,16 +70,12 @@ class CRLogicalSpec(InsnSpec, Elaboratable): class CRMoveSpec(InsnSpec, Elaboratable): - def __init__(self, insn): - self.pfv = pfv.Interface() - self.insn = insn - def elaborate(self, platform): m = Module() m.d.comb += [ - self.pfv.stb .eq(1), - self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), + self.insn .eq(self.pfv.insn[32:]), + self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()), self.pfv.intr.eq(0), self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), self.pfv.msr.r_mask.sf.eq(1), diff --git a/power_fv/insn/spec/loadstore.py b/power_fv/insn/spec/loadstore.py index e1109c1..f2acf7d 100644 --- a/power_fv/insn/spec/loadstore.py +++ b/power_fv/insn/spec/loadstore.py @@ -17,8 +17,8 @@ class LoadStoreSpec(InsnSpec, Elaboratable): m = Module() m.d.comb += [ - self.pfv.stb .eq(1), - self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), + self.insn .eq(self.pfv.insn[32:]), + self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()), self.pfv.msr.r_mask.sf.eq(1), ] diff --git a/power_fv/insn/spec/logical.py b/power_fv/insn/spec/logical.py index 4dc4d21..a3f0f1c 100644 --- a/power_fv/insn/spec/logical.py +++ b/power_fv/insn/spec/logical.py @@ -32,8 +32,8 @@ class LogicalSpec(InsnSpec, Elaboratable): m = Module() m.d.comb += [ - self.pfv.stb .eq(1), - self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), + self.insn .eq(self.pfv.insn[32:]), + self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()), self.pfv.intr.eq(0), self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), self.pfv.msr.r_mask.sf.eq(1), diff --git a/power_fv/insn/spec/msr.py b/power_fv/insn/spec/msr.py index c0d0e98..4a9daf1 100644 --- a/power_fv/insn/spec/msr.py +++ b/power_fv/insn/spec/msr.py @@ -17,8 +17,8 @@ class MSRMoveSpec(InsnSpec, Elaboratable): m = Module() m.d.comb += [ - self.pfv.stb .eq(1), - self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), + self.insn .eq(self.pfv.insn[32:]), + self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()), self.pfv.msr.r_mask.sf.eq(1), self.pfv.msr.r_mask.pr.eq(1) ] diff --git a/power_fv/insn/spec/muldiv.py b/power_fv/insn/spec/muldiv.py index 42d03f9..a9833ff 100644 --- a/power_fv/insn/spec/muldiv.py +++ b/power_fv/insn/spec/muldiv.py @@ -16,8 +16,8 @@ class MultiplySpec(InsnSpec, Elaboratable): m = Module() m.d.comb += [ - self.pfv.stb .eq(1), - self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), + self.insn .eq(self.pfv.insn[32:]), + self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()), self.pfv.intr.eq(0), self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), self.pfv.msr.r_mask.sf.eq(1), @@ -150,8 +150,8 @@ class DivideSpec(InsnSpec, Elaboratable): m = Module() m.d.comb += [ - self.pfv.stb .eq(1), - self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), + self.insn .eq(self.pfv.insn[32:]), + self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()), self.pfv.intr.eq(0), self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), self.pfv.msr.r_mask.sf.eq(1), diff --git a/power_fv/insn/spec/rotate.py b/power_fv/insn/spec/rotate.py index e62ada6..231336b 100644 --- a/power_fv/insn/spec/rotate.py +++ b/power_fv/insn/spec/rotate.py @@ -16,8 +16,8 @@ class RotateShiftSpec(InsnSpec, Elaboratable): m = Module() m.d.comb += [ - self.pfv.stb .eq(1), - self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), + self.insn .eq(self.pfv.insn[32:]), + self.pfv.stb.eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()), self.pfv.msr.r_mask.sf.eq(1), ] diff --git a/power_fv/insn/spec/spr.py b/power_fv/insn/spec/spr.py index 7780bee..f3ccc89 100644 --- a/power_fv/insn/spec/spr.py +++ b/power_fv/insn/spec/spr.py @@ -17,8 +17,8 @@ class SPRMoveSpec(InsnSpec, Elaboratable): m = Module() m.d.comb += [ - self.pfv.stb .eq(1), - self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), + self.insn .eq(self.pfv.insn[32:]), + self.pfv.stb.eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()), self.pfv.msr.r_mask.sf.eq(1), self.pfv.msr.r_mask.pr.eq(1), ] diff --git a/power_fv/insn/spec/syscall.py b/power_fv/insn/spec/syscall.py index 254d1a3..5ca25a3 100644 --- a/power_fv/insn/spec/syscall.py +++ b/power_fv/insn/spec/syscall.py @@ -16,8 +16,8 @@ class SystemCallSpec(InsnSpec, Elaboratable): m = Module() m.d.comb += [ - self.pfv.stb .eq(1), - self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), + self.insn .eq(self.pfv.insn[32:]), + self.pfv.stb.eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()), ] if isinstance(self.insn, SC): diff --git a/power_fv/insn/spec/trap.py b/power_fv/insn/spec/trap.py index 8a536c9..a4e159c 100644 --- a/power_fv/insn/spec/trap.py +++ b/power_fv/insn/spec/trap.py @@ -16,8 +16,8 @@ class TrapSpec(InsnSpec, Elaboratable): m = Module() m.d.comb += [ - self.pfv.stb .eq(1), - self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), + self.insn .eq(self.pfv.insn[32:]), + self.pfv.stb.eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()), ] src_a = Signal(signed(64))