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