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)
  41         m.submodules.dut = dut = CRMainStage(pspec)
  42
  43         full_cr_in = Signal(32)
  44
  45         cr_o = Signal(32)
  46
  47         a = dut.i.a
  48         cr = full_cr_in
  49         full_cr_out = dut.o.full_cr
  50         o = dut.o.o
  51
  52         # setup random inputs
  53         comb += [a.eq(AnyConst(64)),
  54                  full_cr_in.eq(AnyConst(32))]
  55
  56         xl_fields = dut.fields.FormXL
  57         xfx_fields = dut.fields.FormXFX
  58
  59         # I'd like to be able to prove this module using the proof
  60         # written before I made the change to use 4 bit cr inputs for
  61         # OP_MCRF and OP_CROP. So I'm going to set up the machinery to
  62         # let me do that here
  63
  64         cr_input_arr = Array([full_cr_in[(7-i)*4:(7-i)*4+4] for i in range(8)])
  65         cr_output_arr = Array([cr_o[(7-i)*4:(7-i)*4+4] for i in range(8)])
  66
  67         with m.Switch(rec.insn_type):
  68             # For OP_CROP, we need to input the corresponding CR
  69             # registers for BA, BB, and BT
  70             with m.Case(InternalOp.OP_CROP):
  71                 # grab the MSBs of the 3 bit selectors
  72                 bt = Signal(3, reset_less=True)
  73                 ba = Signal(3, reset_less=True)
  74                 bb = Signal(3, reset_less=True)
  75                 comb += bt.eq(xl_fields.BT[2:5])
  76                 comb += ba.eq(xl_fields.BA[2:5])
  77                 comb += bb.eq(xl_fields.BB[2:5])
  78
  79                 # Grab the cr register containing the bit from BA, BB,
  80                 # and BT, and feed it to the cr inputs
  81                 comb += dut.i.cr_a.eq(cr_input_arr[ba])
  82                 comb += dut.i.cr_b.eq(cr_input_arr[bb])
  83                 comb += dut.i.cr_c.eq(cr_input_arr[bt])
  84
  85                 # Insert the output into the output CR register so the
  86                 # proof below can use it
  87                 for i in range(8):
  88                     with m.If(i != bt):
  89                         comb += cr_output_arr[i].eq(cr_input_arr[i])
  90                     with m.Else():
  91                         comb += cr_output_arr[i].eq(dut.o.cr_o)
  92
  93
  94             with m.Case(InternalOp.OP_MCRF):
  95                 # This does a similar thing to OP_CROP above, with
  96                 # less inputs. The CR selection fields are already 3
  97                 # bits so there's no need to grab only the MSBs
  98                 bf = Signal(xl_fields.BF[0:-1].shape())
  99                 bfa = Signal(xl_fields.BFA[0:-1].shape())
 100                 comb += bf.eq(xl_fields.BF[0:-1])
 101                 comb += bfa.eq(xl_fields.BFA[0:-1])
 102
 103                 # set cr_a to the CR selected by BFA
 104                 comb += dut.i.cr_a.eq(cr_input_arr[bfa])
 105                 for i in range(8):
 106                     # Similar to above, insert the result cr back into
 107                     # the full cr register so the proof below can use
 108                     # it
 109                     with m.If(i != bf):
 110                         comb += cr_output_arr[i].eq(cr_input_arr[i])
 111                     with m.Else():
 112                         comb += cr_output_arr[i].eq(dut.o.cr_o)
 113             # For the other two, they take the full CR as input, and
 114             # output a full CR. This handles that
 115             with m.Default():
 116                 comb += dut.i.full_cr.eq(full_cr_in)
 117                 comb += cr_o.eq(dut.o.full_cr)
 118
 119
 120
 121
 122
 123
 124
 125
 126
 127         comb += dut.i.ctx.op.eq(rec)
 128
 129         # Assert that op gets copied from the input to output
 130         for rec_sig in rec.ports():
 131             name = rec_sig.name
 132             dut_sig = getattr(dut.o.ctx.op, name)
 133             comb += Assert(dut_sig == rec_sig)
 134
 135         # big endian indexing. *sigh*
 136         cr_arr = Array([cr[31-i] for i in range(32)])
 137         cr_o_arr = Array([cr_o[31-i] for i in range(32)])
 138
 139         FXM = xfx_fields.FXM[0:-1]
 140         with m.Switch(rec.insn_type):
 141             with m.Case(InternalOp.OP_MTCRF):
 142                 for i in range(8):
 143                     with m.If(FXM[i]):
 144                         comb += Assert(cr_o[4*i:4*i+4] == a[4*i:4*i+4])
 145             with m.Case(InternalOp.OP_MFCR):
 146                 with m.If(rec.insn[20]):  # mfocrf
 147                     for i in range(8):
 148                         with m.If(FXM[i]):
 149                             comb += Assert(o[4*i:4*i+4] == cr[4*i:4*i+4])
 150                         with m.Else():
 151                             comb += Assert(o[4*i:4*i+4] == 0)
 152                 with m.Else(): # mfcrf
 153                     comb += Assert(o == cr)
 154             with m.Case(InternalOp.OP_MCRF):
 155                 BF = xl_fields.BF[0:-1]
 156                 BFA = xl_fields.BFA[0:-1]
 157                 for i in range(4):
 158                     comb += Assert(cr_o_arr[BF*4+i] == cr_arr[BFA*4+i])
 159                 for i in range(8):
 160                     with m.If(BF != 7-i):
 161                         comb += Assert(cr_o[i*4:i*4+4] == cr[i*4:i*4+4])
 162
 163             with m.Case(InternalOp.OP_CROP):
 164                 bt = Signal(xl_fields.BT[0:-1].shape(), reset_less=True)
 165                 ba = Signal(xl_fields.BA[0:-1].shape(), reset_less=True)
 166                 bb = Signal(xl_fields.BB[0:-1].shape(), reset_less=True)
 167                 comb += bt.eq(xl_fields.BT[0:-1])
 168                 comb += ba.eq(xl_fields.BA[0:-1])
 169                 comb += bb.eq(xl_fields.BB[0:-1])
 170
 171                 bit_a = Signal()
 172                 bit_b = Signal()
 173                 bit_o = Signal()
 174                 comb += bit_a.eq(cr_arr[ba])
 175                 comb += bit_b.eq(cr_arr[bb])
 176                 comb += bit_o.eq(cr_o_arr[bt])
 177
 178                 lut = Signal(4)
 179                 comb += lut.eq(rec.insn[6:10])
 180                 with m.If(lut == 0b1000):
 181                     comb += Assert(bit_o == bit_a & bit_b)
 182                 with m.If(lut == 0b0100):
 183                     comb += Assert(bit_o == bit_a & ~bit_b)
 184                 with m.If(lut == 0b1001):
 185                     comb += Assert(bit_o == ~(bit_a ^ bit_b))
 186                 with m.If(lut == 0b0111):
 187                     comb += Assert(bit_o == ~(bit_a & bit_b))
 188                 with m.If(lut == 0b0001):
 189                     comb += Assert(bit_o == ~(bit_a | bit_b))
 190                 with m.If(lut == 0b1110):
 191                     comb += Assert(bit_o == bit_a | bit_b)
 192                 with m.If(lut == 0b1101):
 193                     comb += Assert(bit_o == bit_a | ~bit_b)
 194                 with m.If(lut == 0b0110):
 195                     comb += Assert(bit_o == bit_a ^ bit_b)
 196
 197         return m
 198
 199
 200 class CRTestCase(FHDLTestCase):
 201     def test_formal(self):
 202         module = Driver()
 203         self.assertFormal(module, mode="bmc", depth=2)
 204     def test_ilang(self):
 205         dut = Driver()
 206         vl = rtlil.convert(dut, ports=[])
 207         with open("cr_main_stage.il", "w") as f:
 208             f.write(vl)
 209
 210
 211 if __name__ == '__main__':
 212     unittest.main()