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 = dut.i.full_cr
  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         comb += Assume(rec.insn_type == InternalOp.OP_CROP)
  68         with m.Switch(rec.insn_type):
  69             with m.Case(InternalOp.OP_CROP):
  70                 comb += Assume(full_cr_in != 0)
  71                 bt = Signal(3, reset_less=True)
  72                 ba = Signal(3, reset_less=True)
  73                 bb = Signal(3, reset_less=True)
  74                 comb += bt.eq(xl_fields.BT[2:5])
  75                 comb += ba.eq(xl_fields.BA[2:5])
  76                 comb += bb.eq(xl_fields.BB[2:5])
  77
  78                 comb += dut.i.cr_a.eq(cr_input_arr[ba])
  79                 comb += dut.i.cr_b.eq(cr_input_arr[bb])
  80                 comb += dut.i.cr_c.eq(cr_input_arr[bt])
  81
  82
  83                 for i in range(8):
  84                     with m.If(i != bt):
  85                         comb += cr_output_arr[i].eq(cr_input_arr[i])
  86                     with m.Else():
  87                         comb += cr_output_arr[i].eq(dut.o.cr_o)
  88
  89
  90             with m.Case(InternalOp.OP_MCRF):
  91                 pass
  92             with m.Default():
  93                 comb += cr.eq(full_cr_in)
  94                 comb += cr_o.eq(dut.o.full_cr)
  95
  96
  97
  98
  99
 100
 101
 102
 103
 104         comb += dut.i.ctx.op.eq(rec)
 105
 106         # Assert that op gets copied from the input to output
 107         for rec_sig in rec.ports():
 108             name = rec_sig.name
 109             dut_sig = getattr(dut.o.ctx.op, name)
 110             comb += Assert(dut_sig == rec_sig)
 111
 112         # big endian indexing. *sigh*
 113         cr_arr = Array([cr[31-i] for i in range(32)])
 114         cr_o_arr = Array([cr_o[31-i] for i in range(32)])
 115
 116         FXM = xfx_fields.FXM[0:-1]
 117         with m.Switch(rec.insn_type):
 118             with m.Case(InternalOp.OP_MTCRF):
 119                 for i in range(8):
 120                     with m.If(FXM[i]):
 121                         comb += Assert(cr_o[4*i:4*i+4] == a[4*i:4*i+4])
 122             with m.Case(InternalOp.OP_MFCR):
 123                 with m.If(rec.insn[20]):  # mfocrf
 124                     for i in range(8):
 125                         with m.If(FXM[i]):
 126                             comb += Assert(o[4*i:4*i+4] == cr[4*i:4*i+4])
 127                         with m.Else():
 128                             comb += Assert(o[4*i:4*i+4] == 0)
 129                 with m.Else(): # mfcrf
 130                     comb += Assert(o == cr)
 131             with m.Case(InternalOp.OP_MCRF):
 132                 BF = xl_fields.BF[0:-1]
 133                 BFA = xl_fields.BFA[0:-1]
 134                 for i in range(4):
 135                     comb += Assert(cr_o_arr[BF*4+i] == cr_arr[BFA*4+i])
 136                 for i in range(8):
 137                     with m.If(BF != 7-i):
 138                         comb += Assert(cr_o[i*4:i*4+4] == cr[i*4:i*4+4])
 139
 140             with m.Case(InternalOp.OP_CROP):
 141                 bt = Signal(xl_fields.BT[0:-1].shape(), reset_less=True)
 142                 ba = Signal(xl_fields.BA[0:-1].shape(), reset_less=True)
 143                 bb = Signal(xl_fields.BB[0:-1].shape(), reset_less=True)
 144                 comb += bt.eq(xl_fields.BT[0:-1])
 145                 comb += ba.eq(xl_fields.BA[0:-1])
 146                 comb += bb.eq(xl_fields.BB[0:-1])
 147
 148                 bit_a = Signal()
 149                 bit_b = Signal()
 150                 bit_o = Signal()
 151                 comb += bit_a.eq(cr_arr[ba])
 152                 comb += bit_b.eq(cr_arr[bb])
 153                 comb += bit_o.eq(cr_o_arr[bt])
 154
 155                 lut = Signal(4)
 156                 comb += lut.eq(rec.insn[6:10])
 157                 with m.If(lut == 0b1000):
 158                     comb += Assert(bit_o == bit_a & bit_b)
 159                 with m.If(lut == 0b0100):
 160                     comb += Assert(bit_o == bit_a & ~bit_b)
 161                 with m.If(lut == 0b1001):
 162                     comb += Assert(bit_o == ~(bit_a ^ bit_b))
 163                 with m.If(lut == 0b0111):
 164                     comb += Assert(bit_o == ~(bit_a & bit_b))
 165                 with m.If(lut == 0b0001):
 166                     comb += Assert(bit_o == ~(bit_a | bit_b))
 167                 with m.If(lut == 0b1110):
 168                     comb += Assert(bit_o == bit_a | bit_b)
 169                 with m.If(lut == 0b1101):
 170                     comb += Assert(bit_o == bit_a | ~bit_b)
 171                 with m.If(lut == 0b0110):
 172                     comb += Assert(bit_o == bit_a ^ bit_b)
 173
 174         return m
 175
 176
 177 class CRTestCase(FHDLTestCase):
 178     def test_formal(self):
 179         module = Driver()
 180         self.assertFormal(module, mode="bmc", depth=2)
 181     def test_ilang(self):
 182         dut = Driver()
 183         vl = rtlil.convert(dut, ports=[])
 184         with open("cr_main_stage.il", "w") as f:
 185             f.write(vl)
 186
 187
 188 if __name__ == '__main__':
 189     unittest.main()