src/soc/fu/shift_rot/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=340
   6 """
   7
   8 from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
   9                     signed)
  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.shift_rot.main_stage import ShiftRotMainStage
  15 from soc.fu.shift_rot.rotator import right_mask, left_mask
  16 from soc.fu.shift_rot.pipe_data import ShiftRotPipeSpec
  17 from soc.fu.shift_rot.sr_input_record import CompSROpSubset
  18 from soc.decoder.power_enums import MicrOp
  19 from soc.consts import field
  20
  21 import unittest
  22 from nmutil.extend import exts
  23
  24
  25 # This defines a module to drive the device under test and assert
  26 # properties about its outputs
  27 class Driver(Elaboratable):
  28     def __init__(self):
  29         # inputs and outputs
  30         pass
  31
  32     def elaborate(self, platform):
  33         m = Module()
  34         comb = m.d.comb
  35
  36         rec = CompSROpSubset()
  37         # Setup random inputs for dut.op
  38         for p in rec.ports():
  39             comb += p.eq(AnyConst(p.width))
  40
  41         pspec = ShiftRotPipeSpec(id_wid=2)
  42         m.submodules.dut = dut = ShiftRotMainStage(pspec)
  43
  44         # convenience variables
  45         a = dut.i.rs
  46         b = dut.i.rb
  47         ra = dut.i.a
  48         carry_in = dut.i.xer_ca[0]
  49         carry_in32 = dut.i.xer_ca[1]
  50         carry_out = dut.o.xer_ca
  51         o = dut.o.o.data
  52         print ("fields", rec.fields)
  53         itype = rec.insn_type
  54
  55         # instruction fields
  56         m_fields = dut.fields.FormM
  57         md_fields = dut.fields.FormMD
  58
  59         # setup random inputs
  60         comb += a.eq(AnyConst(64))
  61         comb += b.eq(AnyConst(64))
  62         comb += carry_in.eq(AnyConst(1))
  63         comb += carry_in32.eq(AnyConst(1))
  64
  65         # copy operation
  66         comb += dut.i.ctx.op.eq(rec)
  67
  68         # check that the operation (op) is passed through (and muxid)
  69         comb += Assert(dut.o.ctx.op == dut.i.ctx.op)
  70         comb += Assert(dut.o.ctx.muxid == dut.i.ctx.muxid)
  71
  72         # signed and signed/32 versions of input a
  73         a_signed = Signal(signed(64))
  74         a_signed_32 = Signal(signed(32))
  75         comb += a_signed.eq(a)
  76         comb += a_signed_32.eq(a[0:32])
  77
  78         # masks: start-left
  79         mb = Signal(7, reset_less=True)
  80         ml = Signal(64, reset_less=True)
  81
  82         # clear left?
  83         with m.If((itype == MicrOp.OP_RLC) | (itype == MicrOp.OP_RLCL)):
  84             with m.If(rec.is_32bit):
  85                 comb += mb.eq(m_fields.MB[0:-1])
  86             with m.Else():
  87                 comb += mb.eq(md_fields.mb[0:-1])
  88         with m.Else():
  89             with m.If(rec.is_32bit):
  90                 comb += mb.eq(b[0:6])
  91             with m.Else():
  92                 comb += mb.eq(b+32)
  93         comb += ml.eq(left_mask(m, mb))
  94
  95         # masks: end-right
  96         me = Signal(7, reset_less=True)
  97         mr = Signal(64, reset_less=True)
  98
  99         # clear right?
 100         with m.If((itype == MicrOp.OP_RLC) | (itype == MicrOp.OP_RLCR)):
 101             with m.If(rec.is_32bit):
 102                 comb += me.eq(m_fields.ME[0:-1])
 103             with m.Else():
 104                 comb += me.eq(md_fields.me[0:-1])
 105         with m.Else():
 106             with m.If(rec.is_32bit):
 107                 comb += me.eq(b[0:6])
 108             with m.Else():
 109                 comb += me.eq(63-b)
 110         comb += mr.eq(right_mask(m, me))
 111
 112         # must check Data.ok
 113         o_ok = Signal()
 114         comb += o_ok.eq(1)
 115
 116         # main assertion of arithmetic operations
 117         with m.Switch(itype):
 118
 119             # left-shift: 64/32-bit
 120             with m.Case(MicrOp.OP_SHL):
 121                 comb += Assume(ra == 0)
 122                 with m.If(rec.is_32bit):
 123                     comb += Assert(o[0:32] == ((a << b[0:6]) & 0xffffffff))
 124                     comb += Assert(o[32:64] == 0)
 125                 with m.Else():
 126                     comb += Assert(o == ((a << b[0:7]) & ((1 << 64)-1)))
 127
 128             # right-shift: 64/32-bit / signed
 129             with m.Case(MicrOp.OP_SHR):
 130                 comb += Assume(ra == 0)
 131                 with m.If(~rec.is_signed):
 132                     with m.If(rec.is_32bit):
 133                         comb += Assert(o[0:32] == (a[0:32] >> b[0:6]))
 134                         comb += Assert(o[32:64] == 0)
 135                     with m.Else():
 136                         comb += Assert(o == (a >> b[0:7]))
 137                 with m.Else():
 138                     with m.If(rec.is_32bit):
 139                         comb += Assert(o[0:32] == (a_signed_32 >> b[0:6]))
 140                         comb += Assert(o[32:64] == Repl(a[31], 32))
 141                     with m.Else():
 142                         comb += Assert(o == (a_signed >> b[0:7]))
 143
 144             # extswsli: 32/64-bit moded
 145             with m.Case(MicrOp.OP_EXTSWSLI):
 146                 comb += Assume(ra == 0)
 147                 with m.If(rec.is_32bit):
 148                     comb += Assert(o[0:32] == ((a << b[0:6]) & 0xffffffff))
 149                     comb += Assert(o[32:64] == 0)
 150                 with m.Else():
 151                     # sign-extend to 64 bit
 152                     a_s = Signal(64, reset_less=True)
 153                     comb += a_s.eq(exts(a, 32, 64))
 154                     comb += Assert(o == ((a_s << b[0:7]) & ((1 << 64)-1)))
 155
 156             # rlwinm, rlwnm, rlwimi
 157             # *CAN* these even be 64-bit capable?  I don't think they are.
 158             with m.Case(MicrOp.OP_RLC):
 159                 comb += Assume(ra == 0)
 160
 161                 # Duplicate some signals so that they're much easier to find in gtkwave.
 162                 # Pro-tip: when debugging, factor out expressions into explicitly named
 163                 # signals, and search using a unique grep-tag (RLC in my case).  After
 164                 # debugging, resubstitute values to comply with surrounding code norms.
 165
 166                 mrl = Signal(64, reset_less=True, name='MASK_FOR_RLC')
 167                 comb += mrl.eq(ml | mr)
 168
 169                 ainp = Signal(64, reset_less=True, name='A_INP_FOR_RLC')
 170                 comb += ainp.eq(field(a, 32, 63))
 171
 172                 sh = Signal(6, reset_less=True, name='SH_FOR_RLC')
 173                 comb += sh.eq(b[0:6])
 174
 175                 exp_shl = Signal(64, reset_less=True, name='A_SHIFTED_LEFT_BY_SH_FOR_RLC')
 176                 comb += exp_shl.eq((ainp << sh) & 0xFFFFFFFF)
 177
 178                 exp_shr = Signal(64, reset_less=True, name='A_SHIFTED_RIGHT_FOR_RLC')
 179                 comb += exp_shr.eq((ainp >> (32 - sh)) & 0xFFFFFFFF)
 180
 181                 exp_rot = Signal(64, reset_less=True, name='A_ROTATED_LEFT_FOR_RLC')
 182                 comb += exp_rot.eq(exp_shl | exp_shr)
 183
 184                 exp_ol = Signal(32, reset_less=True, name='EXPECTED_OL_FOR_RLC')
 185                 comb += exp_ol.eq(field((exp_rot & mrl) | (ainp & ~mrl), 32, 63))
 186
 187                 act_ol = Signal(32, reset_less=True, name='ACTUAL_OL_FOR_RLC')
 188                 comb += act_ol.eq(field(o, 32, 63))
 189
 190                 # If I uncomment the following lines, I can confirm that all
 191                 # 32-bit rotations work.  If I uncomment only one of the
 192                 # following lines, I can confirm that all 32-bit rotations
 193                 # work.  When I remove/recomment BOTH lines, however, the
 194                 # assertion fails.  Why??
 195
 196 #               comb += Assume(mr == 0xFFFFFFFF)
 197 #               comb += Assume(ml == 0xFFFFFFFF)
 198                 with m.If(rec.is_32bit):
 199                     comb += Assert(act_ol == exp_ol)
 200                     comb += Assert(field(o, 0, 31) == 0)
 201
 202             #TODO
 203             with m.Case(MicrOp.OP_RLCR):
 204                 pass
 205             with m.Case(MicrOp.OP_RLCL):
 206                 pass
 207             with m.Default():
 208                 comb += o_ok.eq(0)
 209
 210         # check that data ok was only enabled when op actioned
 211         comb += Assert(dut.o.o.ok == o_ok)
 212
 213         return m
 214
 215
 216 class ALUTestCase(FHDLTestCase):
 217     def test_formal(self):
 218         module = Driver()
 219         self.assertFormal(module, mode="bmc", depth=2)
 220         self.assertFormal(module, mode="cover", depth=2)
 221     def test_ilang(self):
 222         dut = Driver()
 223         vl = rtlil.convert(dut, ports=[])
 224         with open("main_stage.il", "w") as f:
 225             f.write(vl)
 226
 227
 228 if __name__ == '__main__':
 229     unittest.main()