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.
main
Jean-François Nguyen 2 years ago
parent cee4f7e569
commit 331e4b76ba

@ -50,8 +50,11 @@ class InsnTestbench(Elaboratable):
m.submodules.spec = spec = self.check.spec m.submodules.spec = spec = self.check.spec


m.d.comb += [ m.d.comb += [
spec.pfv.insn .eq(AnyConst(spec.pfv.insn.shape())),
spec.pfv.order.eq(dut.pfv.order), spec.pfv.order.eq(dut.pfv.order),
spec.pfv.cia .eq(dut.pfv.cia), spec.pfv.cia .eq(dut.pfv.cia),

Assume(spec.pfv.stb),
] ]


with m.If(t_post.zero): with m.If(t_post.zero):

@ -1,8 +1,6 @@
from operator import attrgetter from operator import attrgetter


from amaranth import * from amaranth import *
from amaranth.asserts import AnyConst
from amaranth.hdl.ast import ValueCastable, Value




__all__ = ["InsnField", "WordInsn"] __all__ = ["InsnField", "WordInsn"]
@ -35,38 +33,34 @@ class InsnField:
.format(value)) .format(value))
self._value = 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(Record):
class WordInsn(ValueCastable):
SIZE = 32 SIZE = 32


def __init__(self): def __init__(self, name=None, src_loc_at=0):
value_map = {}
field_map = {}
curr_offset = 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): if not isinstance(field, InsnField):
raise TypeError("Field must be an instance of InsnField, not {!r}" raise TypeError("Field must be an instance of InsnField, not {!r}"
.format(field)) .format(field))
if field.name in field_map:
raise ValueError("Duplicate field name '{}'".format(field.name))
if curr_offset > field.offset: if curr_offset > field.offset:
raise ValueError("Field '{}' at offset {} overlaps with its predecessor" raise ValueError("Field '{}' at offset {} overlaps with its predecessor"
.format(field.name, field.offset)) .format(field.name, field.offset))


# Add undefined bits located between this field and its predecessor. # Add undefined bits located between this field and its predecessor.
if curr_offset < field.offset: if curr_offset < field.offset:
undef_bits = AnyConst(unsigned(field.offset - curr_offset)) undef_bits = field.offset - curr_offset
value_map[curr_offset] = undef_bits layout.append((f"_{curr_offset}", unsigned(undef_bits)))
pattern += "-" * undef_bits


value_map[field.offset] = field.as_const() layout.append((field.name, field.shape))
field_map[field.name ] = field 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 curr_offset = field.offset + field.shape.width


@ -75,37 +69,16 @@ class WordInsn(ValueCastable):


# Add undefined bits located after the last field. # Add undefined bits located after the last field.
if curr_offset < self.SIZE: if curr_offset < self.SIZE:
undef_bits = AnyConst(unsigned(self.SIZE - curr_offset)) undef_bits = self.SIZE - curr_offset
value_map[curr_offset] = undef_bits layout.append((f"_{curr_offset}", unsigned(undef_bits)))
pattern += "-" * undef_bits


self.field_map = field_map self._pattern = pattern
self.value_map = value_map super().__init__(reversed(layout), name=name, src_loc_at=1 + src_loc_at)


@property @property
def fields(self): def pattern(self):
return self._fields return self._pattern


def __getattr__(self, name): def is_valid(self):
return self[name] return self.as_value().matches(self.pattern)

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

@ -15,8 +15,8 @@ class AddSubSpec(InsnSpec, Elaboratable):
m = Module() m = Module()


m.d.comb += [ m.d.comb += [
self.pfv.stb .eq(1), self.insn .eq(self.pfv.insn[32:]),
self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()),
self.pfv.intr.eq(0), self.pfv.intr.eq(0),
self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)),
self.pfv.msr.r_mask.sf.eq(1), self.pfv.msr.r_mask.sf.eq(1),

@ -15,8 +15,8 @@ class BCDAssistSpec(InsnSpec, Elaboratable):
m = Module() m = Module()


m.d.comb += [ m.d.comb += [
self.pfv.stb .eq(1), self.insn .eq(self.pfv.insn[32:]),
self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()),
self.pfv.intr.eq(0), self.pfv.intr.eq(0),
self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)),
self.pfv.msr.r_mask.sf.eq(1), self.pfv.msr.r_mask.sf.eq(1),

@ -16,8 +16,8 @@ class BranchSpec(InsnSpec, Elaboratable):
m = Module() m = Module()


m.d.comb += [ m.d.comb += [
self.pfv.stb .eq(1), self.insn .eq(self.pfv.insn[32:]),
self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), 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.sf.eq(1),
] ]



@ -15,8 +15,8 @@ class ByteReverseSpec(InsnSpec, Elaboratable):
m = Module() m = Module()


m.d.comb += [ m.d.comb += [
self.pfv.stb .eq(1), self.insn .eq(self.pfv.insn[32:]),
self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()),
self.pfv.intr.eq(0), self.pfv.intr.eq(0),
self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)),
self.pfv.msr.r_mask.sf.eq(1), self.pfv.msr.r_mask.sf.eq(1),

@ -15,8 +15,8 @@ class CompareSpec(InsnSpec, Elaboratable):
m = Module() m = Module()


m.d.comb += [ m.d.comb += [
self.pfv.stb .eq(1), self.insn .eq(self.pfv.insn[32:]),
self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()),
self.pfv.intr.eq(0), self.pfv.intr.eq(0),
self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)),
self.pfv.msr.r_mask.sf.eq(1), self.pfv.msr.r_mask.sf.eq(1),

@ -18,8 +18,8 @@ class CRLogicalSpec(InsnSpec, Elaboratable):
m = Module() m = Module()


m.d.comb += [ m.d.comb += [
self.pfv.stb .eq(1), self.insn .eq(self.pfv.insn[32:]),
self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()),
self.pfv.intr.eq(0), self.pfv.intr.eq(0),
self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)),
self.pfv.msr.r_mask.sf.eq(1), self.pfv.msr.r_mask.sf.eq(1),
@ -70,16 +70,12 @@ class CRLogicalSpec(InsnSpec, Elaboratable):




class CRMoveSpec(InsnSpec, Elaboratable): class CRMoveSpec(InsnSpec, Elaboratable):
def __init__(self, insn):
self.pfv = pfv.Interface()
self.insn = insn

def elaborate(self, platform): def elaborate(self, platform):
m = Module() m = Module()


m.d.comb += [ m.d.comb += [
self.pfv.stb .eq(1), self.insn .eq(self.pfv.insn[32:]),
self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()),
self.pfv.intr.eq(0), self.pfv.intr.eq(0),
self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)),
self.pfv.msr.r_mask.sf.eq(1), self.pfv.msr.r_mask.sf.eq(1),

@ -17,8 +17,8 @@ class LoadStoreSpec(InsnSpec, Elaboratable):
m = Module() m = Module()


m.d.comb += [ m.d.comb += [
self.pfv.stb .eq(1), self.insn .eq(self.pfv.insn[32:]),
self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), 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.sf.eq(1),
] ]



@ -32,8 +32,8 @@ class LogicalSpec(InsnSpec, Elaboratable):
m = Module() m = Module()


m.d.comb += [ m.d.comb += [
self.pfv.stb .eq(1), self.insn .eq(self.pfv.insn[32:]),
self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()),
self.pfv.intr.eq(0), self.pfv.intr.eq(0),
self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)),
self.pfv.msr.r_mask.sf.eq(1), self.pfv.msr.r_mask.sf.eq(1),

@ -17,8 +17,8 @@ class MSRMoveSpec(InsnSpec, Elaboratable):
m = Module() m = Module()


m.d.comb += [ m.d.comb += [
self.pfv.stb .eq(1), self.insn .eq(self.pfv.insn[32:]),
self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), 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.sf.eq(1),
self.pfv.msr.r_mask.pr.eq(1) self.pfv.msr.r_mask.pr.eq(1)
] ]

@ -16,8 +16,8 @@ class MultiplySpec(InsnSpec, Elaboratable):
m = Module() m = Module()


m.d.comb += [ m.d.comb += [
self.pfv.stb .eq(1), self.insn .eq(self.pfv.insn[32:]),
self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()),
self.pfv.intr.eq(0), self.pfv.intr.eq(0),
self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)),
self.pfv.msr.r_mask.sf.eq(1), self.pfv.msr.r_mask.sf.eq(1),
@ -150,8 +150,8 @@ class DivideSpec(InsnSpec, Elaboratable):
m = Module() m = Module()


m.d.comb += [ m.d.comb += [
self.pfv.stb .eq(1), self.insn .eq(self.pfv.insn[32:]),
self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), self.pfv.stb .eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()),
self.pfv.intr.eq(0), self.pfv.intr.eq(0),
self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)), self.pfv.nia .eq(iea(self.pfv.cia + 4, self.pfv.msr.r_data.sf)),
self.pfv.msr.r_mask.sf.eq(1), self.pfv.msr.r_mask.sf.eq(1),

@ -16,8 +16,8 @@ class RotateShiftSpec(InsnSpec, Elaboratable):
m = Module() m = Module()


m.d.comb += [ m.d.comb += [
self.pfv.stb .eq(1), self.insn .eq(self.pfv.insn[32:]),
self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), 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.sf.eq(1),
] ]



@ -17,8 +17,8 @@ class SPRMoveSpec(InsnSpec, Elaboratable):
m = Module() m = Module()


m.d.comb += [ m.d.comb += [
self.pfv.stb .eq(1), self.insn .eq(self.pfv.insn[32:]),
self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), 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.sf.eq(1),
self.pfv.msr.r_mask.pr.eq(1), self.pfv.msr.r_mask.pr.eq(1),
] ]

@ -16,8 +16,8 @@ class SystemCallSpec(InsnSpec, Elaboratable):
m = Module() m = Module()


m.d.comb += [ m.d.comb += [
self.pfv.stb .eq(1), self.insn .eq(self.pfv.insn[32:]),
self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), self.pfv.stb.eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()),
] ]


if isinstance(self.insn, SC): if isinstance(self.insn, SC):

@ -16,8 +16,8 @@ class TrapSpec(InsnSpec, Elaboratable):
m = Module() m = Module()


m.d.comb += [ m.d.comb += [
self.pfv.stb .eq(1), self.insn .eq(self.pfv.insn[32:]),
self.pfv.insn.eq(Cat(Const(0, 32), self.insn.as_value())), self.pfv.stb.eq(self.insn.is_valid() & ~self.pfv.insn[:32].any()),
] ]


src_a = Signal(signed(64)) src_a = Signal(signed(64))

Loading…
Cancel
Save