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

   1 # Proof of correctness for Condition Register pipeline
   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 nmutil.formaltest 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         cr_a_in = Signal(4)
  45
  46         cr_o = Signal(32)
  47
  48         a = dut.i.a
  49         b = dut.i.b
  50         cr = full_cr_in
  51         full_cr_out = dut.o.full_cr.data
  52         o = dut.o.o.data
  53
  54         # setup random inputs
  55         comb += [a.eq(AnyConst(64)),
  56                  b.eq(AnyConst(64)),
  57                  cr_a_in.eq(AnyConst(4)),
  58                  full_cr_in.eq(AnyConst(32))]
  59
  60         a_fields = dut.fields.FormA
  61         xl_fields = dut.fields.FormXL
  62         xfx_fields = dut.fields.FormXFX
  63
  64         # I'd like to be able to prove this module using the proof
  65         # written before I made the change to use 4 bit cr inputs for
  66         # OP_MCRF and OP_CROP. So I'm going to set up the machinery to
  67         # let me do that here
  68
  69         cr_input_arr = Array([full_cr_in[(7-i)*4:(7-i)*4+4] for i in range(8)])
  70         cr_output_arr = Array([cr_o[(7-i)*4:(7-i)*4+4] for i in range(8)])
  71
  72         bf = Signal(xl_fields.BF[0:-1].shape())
  73         bfa = Signal(xl_fields.BFA[0:-1].shape())
  74         comb += bf.eq(xl_fields.BF[0:-1])
  75         comb += bfa.eq(xl_fields.BFA[0:-1])
  76
  77         with m.Switch(rec.insn_type):
  78             # CR_ISEL takes cr_a
  79             with m.Case(InternalOp.OP_ISEL):
  80                 # grab the MSBs of the cr bit selector
  81                 bc = Signal(3, reset_less=True)
  82                 comb += bc.eq(a_fields.BC[2:5])
  83
  84                 # Use the MSBs to select which CR register to feed
  85                 # into cr_a
  86                 comb += dut.i.cr_a.eq(cr_input_arr[bc])
  87
  88
  89             # For OP_CROP, we need to input the corresponding CR
  90             # registers for BA, BB, and BT
  91             with m.Case(InternalOp.OP_CROP):
  92                 # grab the MSBs of the 3 bit selectors
  93                 bt = Signal(3, reset_less=True)
  94                 ba = Signal(3, reset_less=True)
  95                 bb = Signal(3, reset_less=True)
  96                 comb += bt.eq(xl_fields.BT[2:5])
  97                 comb += ba.eq(xl_fields.BA[2:5])
  98                 comb += bb.eq(xl_fields.BB[2:5])
  99
 100                 # Grab the cr register containing the bit from BA, BB,
 101                 # and BT, and feed it to the cr inputs
 102                 comb += dut.i.cr_a.eq(cr_input_arr[ba])
 103                 comb += dut.i.cr_b.eq(cr_input_arr[bb])
 104                 comb += dut.i.cr_c.eq(cr_input_arr[bt])
 105
 106                 # Insert the output into the output CR register so the
 107                 # proof below can use it
 108                 for i in range(8):
 109                     with m.If(i != bt):
 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.data)
 113
 114             with m.Case(InternalOp.OP_MCRF):
 115                 # This does a similar thing to OP_CROP above, with
 116                 # less inputs. The CR selection fields are already 3
 117                 # bits so there's no need to grab only the MSBs
 118
 119                 # set cr_a to the CR selected by BFA
 120                 comb += dut.i.cr_a.eq(cr_input_arr[bfa])
 121                 for i in range(8):
 122                     # Similar to above, insert the result cr back into
 123                     # the full cr register so the proof below can use
 124                     # it
 125                     with m.If(i != bf):
 126                         comb += cr_output_arr[i].eq(cr_input_arr[i])
 127                     with m.Else():
 128                         comb += cr_output_arr[i].eq(dut.o.cr.data)
 129
 130             # Set the input similar to OP_MCRF
 131             with m.Case(InternalOp.OP_SETB):
 132                 comb += dut.i.cr_a.eq(cr_input_arr[bfa])
 133
 134             # For the other two, they take the full CR as input, and
 135             # output a full CR. This handles that
 136             with m.Default():
 137                 comb += dut.i.full_cr.eq(full_cr_in)
 138                 comb += cr_o.eq(full_cr_out)
 139
 140         comb += dut.i.ctx.op.eq(rec)
 141
 142         # test signals for output conditions.  these must only be enabled for
 143         # specific instructions, indicating that they generated the output.
 144         # this is critically important because the "ok" signals are used by
 145         # MultiCompUnit to request a write to the regfile.
 146         o_ok = Signal()
 147         cr_o_ok = Signal()
 148         full_cr_o_ok = Signal()
 149
 150         # Assert that op gets copied from the input to output
 151         for rec_sig in rec.ports():
 152             name = rec_sig.name
 153             dut_sig = getattr(dut.o.ctx.op, name)
 154             comb += Assert(dut_sig == rec_sig)
 155
 156         # big endian indexing. *sigh*
 157         cr_arr = Array([cr[31-i] for i in range(32)])
 158         cr_o_arr = Array([cr_o[31-i] for i in range(32)])
 159
 160         FXM = xfx_fields.FXM[0:-1]
 161         with m.Switch(rec.insn_type):
 162             with m.Case(InternalOp.OP_MTCRF):
 163                 for i in range(8):
 164                     with m.If(FXM[i]):
 165                         comb += Assert(cr_o[4*i:4*i+4] == a[4*i:4*i+4])
 166                 comb += full_cr_o_ok.eq(1)
 167
 168             with m.Case(InternalOp.OP_MFCR):
 169                 with m.If(rec.insn[20]):  # mfocrf
 170                     for i in range(8):
 171                         with m.If(FXM[i]):
 172                             comb += Assert(o[4*i:4*i+4] == cr[4*i:4*i+4])
 173                         with m.Else():
 174                             comb += Assert(o[4*i:4*i+4] == 0)
 175                 with m.Else(): # mfcrf
 176                     comb += Assert(o == cr)
 177                 comb += o_ok.eq(1)
 178
 179             with m.Case(InternalOp.OP_MCRF):
 180                 BF = xl_fields.BF[0:-1]
 181                 BFA = xl_fields.BFA[0:-1]
 182                 for i in range(4):
 183                     comb += Assert(cr_o_arr[BF*4+i] == cr_arr[BFA*4+i])
 184                 for i in range(8):
 185                     with m.If(BF != 7-i):
 186                         comb += Assert(cr_o[i*4:i*4+4] == cr[i*4:i*4+4])
 187                 comb += cr_o_ok.eq(1)
 188
 189             with m.Case(InternalOp.OP_CROP):
 190                 bt = Signal(xl_fields.BT[0:-1].shape(), reset_less=True)
 191                 ba = Signal(xl_fields.BA[0:-1].shape(), reset_less=True)
 192                 bb = Signal(xl_fields.BB[0:-1].shape(), reset_less=True)
 193                 comb += bt.eq(xl_fields.BT[0:-1])
 194                 comb += ba.eq(xl_fields.BA[0:-1])
 195                 comb += bb.eq(xl_fields.BB[0:-1])
 196
 197                 bit_a = Signal()
 198                 bit_b = Signal()
 199                 bit_o = Signal()
 200                 comb += bit_a.eq(cr_arr[ba])
 201                 comb += bit_b.eq(cr_arr[bb])
 202                 comb += bit_o.eq(cr_o_arr[bt])
 203
 204                 lut = Signal(4)
 205                 comb += lut.eq(rec.insn[6:10])
 206                 with m.If(lut == 0b1000):
 207                     comb += Assert(bit_o == bit_a & bit_b)
 208                 with m.If(lut == 0b0100):
 209                     comb += Assert(bit_o == bit_a & ~bit_b)
 210                 with m.If(lut == 0b1001):
 211                     comb += Assert(bit_o == ~(bit_a ^ bit_b))
 212                 with m.If(lut == 0b0111):
 213                     comb += Assert(bit_o == ~(bit_a & bit_b))
 214                 with m.If(lut == 0b0001):
 215                     comb += Assert(bit_o == ~(bit_a | bit_b))
 216                 with m.If(lut == 0b1110):
 217                     comb += Assert(bit_o == bit_a | bit_b)
 218                 with m.If(lut == 0b1101):
 219                     comb += Assert(bit_o == bit_a | ~bit_b)
 220                 with m.If(lut == 0b0110):
 221                     comb += Assert(bit_o == bit_a ^ bit_b)
 222
 223                 comb += cr_o_ok.eq(1)
 224
 225             with m.Case(InternalOp.OP_ISEL):
 226                 # Extract the bit selector of the CR
 227                 bc = Signal(a_fields.BC[0:-1].shape(), reset_less=True)
 228                 comb += bc.eq(a_fields.BC[0:-1])
 229
 230                 # Extract the bit from CR
 231                 cr_bit = Signal(reset_less=True)
 232                 comb += cr_bit.eq(cr_arr[bc])
 233
 234                 # select a or b as output
 235                 comb += Assert(o == Mux(cr_bit, a, b))
 236                 comb += o_ok.eq(1)
 237
 238             with m.Case(InternalOp.OP_SETB):
 239                 with m.If(cr_arr[4*bfa]):
 240                     comb += Assert(o == ((1<<64)-1))
 241                 with m.Elif(cr_arr[4*bfa+1]):
 242                     comb += Assert(o == 1)
 243                 with m.Else():
 244                     comb += Assert(o == 0)
 245                 comb += o_ok.eq(1)
 246
 247         # check that data ok was only enabled when op actioned
 248         comb += Assert(dut.o.o.ok == o_ok)
 249         comb += Assert(dut.o.cr.ok == cr_o_ok)
 250         comb += Assert(dut.o.full_cr.ok == full_cr_o_ok)
 251
 252         return m
 253
 254
 255 class CRTestCase(FHDLTestCase):
 256     def test_formal(self):
 257         module = Driver()
 258         self.assertFormal(module, mode="bmc", depth=2)
 259     def test_ilang(self):
 260         dut = Driver()
 261         vl = rtlil.convert(dut, ports=[])
 262         with open("cr_main_stage.il", "w") as f:
 263             f.write(vl)
 264
 265
 266 if __name__ == '__main__':
 267     unittest.main()