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

   1 # Proof of correctness for partitioned equal signal combiner
   2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
   3
   4 from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
   5                     signed, Array)
   6 from nmigen.asserts import Assert, AnyConst, Assume, Cover
   7 from nmigen.test.utils import FHDLTestCase
   8 from nmigen.cli import rtlil
   9
  10 from soc.fu.cr.main_stage import CRMainStage
  11 from soc.fu.alu.pipe_data import ALUPipeSpec
  12 from soc.fu.alu.alu_input_record import CompALUOpSubset
  13 from soc.decoder.power_enums import InternalOp
  14 import unittest
  15
  16
  17 # This defines a module to drive the device under test and assert
  18 # properties about its outputs
  19 class Driver(Elaboratable):
  20     def __init__(self):
  21         # inputs and outputs
  22         pass
  23
  24     def elaborate(self, platform):
  25         m = Module()
  26         comb = m.d.comb
  27
  28         rec = CompALUOpSubset()
  29         recwidth = 0
  30         # Setup random inputs for dut.op
  31         for p in rec.ports():
  32             width = p.width
  33             recwidth += width
  34             comb += p.eq(AnyConst(width))
  35
  36         pspec = ALUPipeSpec(id_wid=2, op_wid=recwidth)
  37         m.submodules.dut = dut = CRMainStage(pspec)
  38
  39         a = dut.i.a
  40         cr = dut.i.cr
  41         cr_o = dut.o.cr
  42
  43         # setup random inputs
  44         comb += [a.eq(AnyConst(64)),
  45                  cr.eq(AnyConst(64))]
  46
  47         comb += dut.i.ctx.op.eq(rec)
  48
  49         # Assert that op gets copied from the input to output
  50         for rec_sig in rec.ports():
  51             name = rec_sig.name
  52             dut_sig = getattr(dut.o.ctx.op, name)
  53             comb += Assert(dut_sig == rec_sig)
  54
  55         # big endian indexing. *sigh*
  56         cr_arr = Array([cr[31-i] for i in range(32)])
  57         cr_o_arr = Array([cr_o[31-i] for i in range(32)])
  58
  59         xl_fields = dut.fields.FormXL
  60         xfx_fields = dut.fields.FormXFX
  61         with m.Switch(rec.insn_type):
  62             with m.Case(InternalOp.OP_MTCRF):
  63                 FXM = xfx_fields.FXM[0:-1]
  64                 for i in range(8):
  65                     with m.If(FXM[i]):
  66                         comb += Assert(cr_o[4*i:4*i+4] == a[4*i:4*i+4])
  67             with m.Case(InternalOp.OP_CROP):
  68                 bt = Signal(xl_fields.BT[0:-1].shape(), reset_less=True)
  69                 ba = Signal(xl_fields.BA[0:-1].shape(), reset_less=True)
  70                 bb = Signal(xl_fields.BB[0:-1].shape(), reset_less=True)
  71                 comb += bt.eq(xl_fields.BT[0:-1])
  72                 comb += ba.eq(xl_fields.BA[0:-1])
  73                 comb += bb.eq(xl_fields.BB[0:-1])
  74
  75                 bit_a = Signal()
  76                 bit_b = Signal()
  77                 bit_o = Signal()
  78                 comb += bit_a.eq(cr_arr[ba])
  79                 comb += bit_b.eq(cr_arr[bb])
  80                 comb += bit_o.eq(cr_o_arr[bt])
  81
  82                 lut = Signal(4)
  83                 comb += lut.eq(rec.insn[6:10])
  84                 with m.If(lut == 0b1000):
  85                     comb += Assert(bit_o == bit_a & bit_b)
  86                 with m.If(lut == 0b0100):
  87                     comb += Assert(bit_o == bit_a & ~bit_b)
  88                 with m.If(lut == 0b1001):
  89                     comb += Assert(bit_o == ~(bit_a ^ bit_b))
  90                 with m.If(lut == 0b0111):
  91                     comb += Assert(bit_o == ~(bit_a & bit_b))
  92                 with m.If(lut == 0b0001):
  93                     comb += Assert(bit_o == ~(bit_a | bit_b))
  94                 with m.If(lut == 0b1110):
  95                     comb += Assert(bit_o == bit_a | bit_b)
  96                 with m.If(lut == 0b1101):
  97                     comb += Assert(bit_o == bit_a | ~bit_b)
  98                 with m.If(lut == 0b0110):
  99                     comb += Assert(bit_o == bit_a ^ bit_b)
 100
 101         return m
 102
 103
 104 class CRTestCase(FHDLTestCase):
 105     def test_formal(self):
 106         module = Driver()
 107         self.assertFormal(module, mode="bmc", depth=2)
 108     def test_ilang(self):
 109         dut = Driver()
 110         vl = rtlil.convert(dut, ports=[])
 111         with open("cr_main_stage.il", "w") as f:
 112             f.write(vl)
 113
 114
 115 if __name__ == '__main__':
 116     unittest.main()