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 openpower.decoder.power_enums import MicrOp
  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, parent_pspec=None)
  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(MicrOp.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             # For OP_CROP, we need to input the corresponding CR
  89             # registers for BA, BB, and BT
  90             with m.Case(MicrOp.OP_CROP):
  91                 # grab the MSBs of the 3 bit selectors
  92                 bt = Signal(3, reset_less=True)
  93                 ba = Signal(3, reset_less=True)
  94                 bb = Signal(3, reset_less=True)
  95                 comb += bt.eq(xl_fields.BT[2:5])
  96                 comb += ba.eq(xl_fields.BA[2:5])
  97                 comb += bb.eq(xl_fields.BB[2:5])
  98
  99                 # Grab the cr register containing the bit from BA, BB,
 100                 # and BT, and feed it to the cr inputs
 101                 comb += dut.i.cr_a.eq(cr_input_arr[ba])
 102                 comb += dut.i.cr_b.eq(cr_input_arr[bb])
 103                 comb += dut.i.cr_c.eq(cr_input_arr[bt])
 104
 105                 # Insert the output into the output CR register so the
 106                 # proof below can use it
 107                 for i in range(8):
 108                     with m.If(i != bt):
 109                         comb += cr_output_arr[i].eq(cr_input_arr[i])
 110                     with m.Else():
 111                         comb += cr_output_arr[i].eq(dut.o.cr.data)
 112
 113             with m.Case(MicrOp.OP_MCRF):
 114                 # This does a similar thing to OP_CROP above, with
 115                 # less inputs. The CR selection fields are already 3
 116                 # bits so there's no need to grab only the MSBs
 117
 118                 # set cr_a to the CR selected by BFA
 119                 comb += dut.i.cr_a.eq(cr_input_arr[bfa])
 120                 for i in range(8):
 121                     # Similar to above, insert the result cr back into
 122                     # the full cr register so the proof below can use
 123                     # it
 124                     with m.If(i != bf):
 125                         comb += cr_output_arr[i].eq(cr_input_arr[i])
 126                     with m.Else():
 127                         comb += cr_output_arr[i].eq(dut.o.cr.data)
 128
 129             # Set the input similar to OP_MCRF
 130             with m.Case(MicrOp.OP_SETB):
 131                 comb += dut.i.cr_a.eq(cr_input_arr[bfa])
 132
 133             # For the other two, they take the full CR as input, and
 134             # output a full CR. This handles that
 135             with m.Default():
 136                 comb += dut.i.full_cr.eq(full_cr_in)
 137                 comb += cr_o.eq(full_cr_out)
 138
 139         comb += dut.i.ctx.op.eq(rec)
 140
 141         # test signals for output conditions.  these must only be enabled for
 142         # specific instructions, indicating that they generated the output.
 143         # this is critically important because the "ok" signals are used by
 144         # MultiCompUnit to request a write to the regfile.
 145         o_ok = Signal()
 146         cr_o_ok = Signal()
 147         full_cr_o_ok = Signal()
 148
 149         # Assert that op gets copied from the input to output
 150         for rec_sig in rec.ports():
 151             name = rec_sig.name
 152             dut_sig = getattr(dut.o.ctx.op, name)
 153             comb += Assert(dut_sig == rec_sig)
 154
 155         # big endian indexing. *sigh*
 156         cr_arr = Array([cr[31-i] for i in range(32)])
 157         cr_o_arr = Array([cr_o[31-i] for i in range(32)])
 158
 159         FXM = xfx_fields.FXM[0:-1]
 160         with m.Switch(rec.insn_type):
 161             with m.Case(MicrOp.OP_MTCRF):
 162                 for i in range(8):
 163                     with m.If(FXM[i]):
 164                         comb += Assert(cr_o[4*i:4*i+4] == a[4*i:4*i+4])
 165                 comb += full_cr_o_ok.eq(1)
 166
 167             with m.Case(MicrOp.OP_MFCR):
 168                 with m.If(rec.insn[20]):  # mfocrf
 169                     for i in range(8):
 170                         with m.If(FXM[i]):
 171                             comb += Assert(o[4*i:4*i+4] == cr[4*i:4*i+4])
 172                         with m.Else():
 173                             comb += Assert(o[4*i:4*i+4] == 0)
 174                 with m.Else():  # mfcrf
 175                     comb += Assert(o == cr)
 176                 comb += o_ok.eq(1)
 177
 178             with m.Case(MicrOp.OP_MCRF):
 179                 BF = xl_fields.BF[0:-1]
 180                 BFA = xl_fields.BFA[0:-1]
 181                 for i in range(4):
 182                     comb += Assert(cr_o_arr[BF*4+i] == cr_arr[BFA*4+i])
 183                 for i in range(8):
 184                     with m.If(BF != 7-i):
 185                         comb += Assert(cr_o[i*4:i*4+4] == cr[i*4:i*4+4])
 186                 comb += cr_o_ok.eq(1)
 187
 188             with m.Case(MicrOp.OP_CROP):
 189                 bt = Signal(xl_fields.BT[0:-1].shape(), reset_less=True)
 190                 ba = Signal(xl_fields.BA[0:-1].shape(), reset_less=True)
 191                 bb = Signal(xl_fields.BB[0:-1].shape(), reset_less=True)
 192                 comb += bt.eq(xl_fields.BT[0:-1])
 193                 comb += ba.eq(xl_fields.BA[0:-1])
 194                 comb += bb.eq(xl_fields.BB[0:-1])
 195
 196                 bit_a = Signal()
 197                 bit_b = Signal()
 198                 bit_o = Signal()
 199                 comb += bit_a.eq(cr_arr[ba])
 200                 comb += bit_b.eq(cr_arr[bb])
 201                 comb += bit_o.eq(cr_o_arr[bt])
 202
 203                 lut = Signal(4)
 204                 comb += lut.eq(rec.insn[6:10])
 205                 with m.If(lut == 0b1000):
 206                     comb += Assert(bit_o == bit_a & bit_b)
 207                 with m.If(lut == 0b0100):
 208                     comb += Assert(bit_o == bit_a & ~bit_b)
 209                 with m.If(lut == 0b1001):
 210                     comb += Assert(bit_o == ~(bit_a ^ bit_b))
 211                 with m.If(lut == 0b0111):
 212                     comb += Assert(bit_o == ~(bit_a & bit_b))
 213                 with m.If(lut == 0b0001):
 214                     comb += Assert(bit_o == ~(bit_a | bit_b))
 215                 with m.If(lut == 0b1110):
 216                     comb += Assert(bit_o == bit_a | bit_b)
 217                 with m.If(lut == 0b1101):
 218                     comb += Assert(bit_o == bit_a | ~bit_b)
 219                 with m.If(lut == 0b0110):
 220                     comb += Assert(bit_o == bit_a ^ bit_b)
 221
 222                 comb += cr_o_ok.eq(1)
 223
 224             with m.Case(MicrOp.OP_ISEL):
 225                 # Extract the bit selector of the CR
 226                 bc = Signal(a_fields.BC[0:-1].shape(), reset_less=True)
 227                 comb += bc.eq(a_fields.BC[0:-1])
 228
 229                 # Extract the bit from CR
 230                 cr_bit = Signal(reset_less=True)
 231                 comb += cr_bit.eq(cr_arr[bc])
 232
 233                 # select a or b as output
 234                 comb += Assert(o == Mux(cr_bit, a, b))
 235                 comb += o_ok.eq(1)
 236
 237             with m.Case(MicrOp.OP_SETB):
 238                 with m.If(cr_arr[4*bfa]):
 239                     comb += Assert(o == ((1 << 64)-1))
 240                 with m.Elif(cr_arr[4*bfa+1]):
 241                     comb += Assert(o == 1)
 242                 with m.Else():
 243                     comb += Assert(o == 0)
 244                 comb += o_ok.eq(1)
 245
 246         # check that data ok was only enabled when op actioned
 247         comb += Assert(dut.o.o.ok == o_ok)
 248         comb += Assert(dut.o.cr.ok == cr_o_ok)
 249         comb += Assert(dut.o.full_cr.ok == full_cr_o_ok)
 250
 251         return m
 252
 253
 254 class CRTestCase(FHDLTestCase):
 255     def test_formal(self):
 256         module = Driver()
 257         self.assertFormal(module, mode="bmc", depth=2)
 258
 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()