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