src/soc/fu/trap/formal/proof_main_stage.py

   1 # Proof of correctness for trap pipeline, main stage
   2
   3
   4 """
   5 Links:
   6 * https://bugs.libre-soc.org/show_bug.cgi?id=421
   7 """
   8
   9
  10 import unittest
  11
  12 from nmigen import Cat, Const, Elaboratable, Module, Signal
  13 from nmigen.asserts import Assert, AnyConst
  14 from nmigen.cli import rtlil
  15
  16 from nmutil.formaltest import FHDLTestCase
  17
  18 from soc.consts import MSR
  19
  20 from soc.decoder.power_enums import MicrOp
  21
  22 from soc.fu.trap.main_stage import TrapMainStage
  23 from soc.fu.trap.pipe_data import TrapPipeSpec
  24 from soc.fu.trap.trap_input_record import CompTrapOpSubset
  25
  26
  27 def is_ok(sig, value):
  28     """
  29     Answers with a list of assertions that checks for valid data on
  30     a pipeline stage output.  sig.data must have the anticipated value,
  31     and sig.ok must be asserted.  The `value` is constrained to the width
  32     of the sig.data field it's verified against, so it's safe to add, etc.
  33     offsets to Nmigen signals without having to worry about inequalities from
  34     differing signal widths.
  35     """
  36     return [
  37         Assert(sig.data == value[0:len(sig.data)]),
  38         Assert(sig.ok),
  39     ]
  40
  41
  42 def full_function_bits(msr):
  43     """
  44     Answers with a numeric constant signal with all "full functional"
  45     bits filled in, but all partial functional bits zeroed out.
  46
  47     See src/soc/fu/trap/main_stage.py:msr_copy commentary for details.
  48     """
  49     zeros16_21 = Const(0, (22 - 16))
  50     zeros27_30 = Const(0, (31 - 27))
  51     return Cat(msr[0:16], zeros16_21, msr[22:27], zeros27_30, msr[31:64])
  52
  53
  54 class Driver(Elaboratable):
  55     """
  56     """
  57
  58     def elaborate(self, platform):
  59         m = Module()
  60         comb = m.d.comb
  61
  62         rec = CompTrapOpSubset()
  63         pspec = TrapPipeSpec(id_wid=2)
  64
  65         m.submodules.dut = dut = TrapMainStage(pspec)
  66
  67         # frequently used aliases
  68         op = dut.i.ctx.op
  69
  70         comb += op.eq(rec)
  71
  72         # start of properties
  73         with m.Switch(op.insn_type):
  74             with m.Case(MicrOp.OP_SC):
  75                 comb += [
  76                     is_ok(dut.o.nia, Const(0xC00)),
  77                     is_ok(dut.o.srr0, dut.i.cia + 4),
  78                     is_ok(dut.o.srr1, full_function_bits(dut.i.msr)),
  79                 ]
  80             with m.Case(MicrOp.OP_RFID):
  81                 desired_msr = Signal(len(dut.o.msr.data))
  82                 msr_i = dut.i.msr
  83                 srr1_i = dut.i.srr1
  84
  85                 # I don't understand why assertion ABACAB, below, fails.
  86                 # This code is just short of a raw cut-and-paste of the
  87                 # production code.  This should be bit-for-bit identical.
  88                 # GTKWave waveforms do not appear to be helpful.
  89                 comb += [
  90                     desired_msr[0:16].eq(srr1_i[0:16]),
  91                     desired_msr[22:27].eq(srr1_i[22:27]),
  92                     desired_msr[31:64].eq(srr1_i[31:64]),
  93                 ]
  94
  95                 with m.If(msr_i[MSR.PR]):
  96                     comb += [
  97                         desired_msr[MSR.EE].eq(1),
  98                         desired_msr[MSR.IR].eq(1),
  99                         desired_msr[MSR.DR].eq(1),
 100                     ]
 101
 102                 with m.If((msr_i[63-31:63-29] != Const(0b010, 3)) |
 103                           (srr1_i[63-31:63-29] != Const(0b000, 3))):
 104                     comb += desired_msr[63-31:63-29].eq(srr1_i[63-31:63-29])
 105                 with m.Else():
 106                     comb += desired_msr[63-31:63-29].eq(msr_i[63-31:63-29])
 107
 108                 comb += [
 109                     is_ok(dut.o.nia, Cat(Const(0, 2), dut.i.srr0[2:])),
 110                     Assert(dut.o.msr.data[0:16] == desired_msr[0:16]),  # ABACAB #
 111                     Assert(dut.o.msr.ok),
 112                 ]
 113
 114         comb += dut.i.ctx.matches(dut.o.ctx)
 115
 116         return m
 117
 118
 119 class TrapMainStageTestCase(FHDLTestCase):
 120     def test_formal(self):
 121         self.assertFormal(Driver(), mode="bmc", depth=10)
 122         self.assertFormal(Driver(), mode="cover", depth=10)
 123
 124     def test_ilang(self):
 125         vl = rtlil.convert(Driver(), ports=[])
 126         with open("trap_main_stage.il", "w") as f:
 127             f.write(vl)
 128
 129
 130 if __name__ == '__main__':
 131     unittest.main()
 132