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 import unittest
  20 from nmutil.extend import exts
  21
  22
  23 # This defines a module to drive the device under test and assert
  24 # properties about its outputs
  25 class Driver(Elaboratable):
  26     def __init__(self):
  27         # inputs and outputs
  28         pass
  29
  30     def elaborate(self, platform):
  31         m = Module()
  32         comb = m.d.comb
  33
  34         rec = CompSROpSubset()
  35         # Setup random inputs for dut.op
  36         for p in rec.ports():
  37             comb += p.eq(AnyConst(p.width))
  38
  39         pspec = ShiftRotPipeSpec(id_wid=2)
  40         m.submodules.dut = dut = ShiftRotMainStage(pspec)
  41
  42         # convenience variables
  43         a = dut.i.rs
  44         b = dut.i.rb
  45         ra = dut.i.a
  46         carry_in = dut.i.xer_ca[0]
  47         carry_in32 = dut.i.xer_ca[1]
  48         carry_out = dut.o.xer_ca
  49         o = dut.o.o.data
  50         print ("fields", rec.fields)
  51         itype = rec.insn_type
  52
  53         # instruction fields
  54         m_fields = dut.fields.FormM
  55         md_fields = dut.fields.FormMD
  56
  57         # setup random inputs
  58         comb += a.eq(AnyConst(64))
  59         comb += b.eq(AnyConst(64))
  60         comb += carry_in.eq(AnyConst(1))
  61         comb += carry_in32.eq(AnyConst(1))
  62
  63         # copy operation
  64         comb += dut.i.ctx.op.eq(rec)
  65
  66         # check that the operation (op) is passed through (and muxid)
  67         comb += Assert(dut.o.ctx.op == dut.i.ctx.op)
  68         comb += Assert(dut.o.ctx.muxid == dut.i.ctx.muxid)
  69
  70         # signed and signed/32 versions of input a
  71         a_signed = Signal(signed(64))
  72         a_signed_32 = Signal(signed(32))
  73         comb += a_signed.eq(a)
  74         comb += a_signed_32.eq(a[0:32])
  75
  76         # masks: start-left
  77         mb = Signal(7, reset_less=True)
  78         ml = Signal(64, reset_less=True)
  79
  80         # clear left?
  81         with m.If((itype == MicrOp.OP_RLC) | (itype == MicrOp.OP_RLCL)):
  82             with m.If(rec.is_32bit):
  83                 comb += mb.eq(m_fields.MB[0:-1])
  84             with m.Else():
  85                 comb += mb.eq(md_fields.mb[0:-1])
  86         with m.Else():
  87             with m.If(rec.is_32bit):
  88                 comb += mb.eq(b[0:6])
  89             with m.Else():
  90                 comb += mb.eq(b+32)
  91         comb += ml.eq(left_mask(m, mb))
  92
  93         # masks: end-right
  94         me = Signal(7, reset_less=True)
  95         mr = Signal(64, reset_less=True)
  96
  97         # clear right?
  98         with m.If((itype == MicrOp.OP_RLC) | (itype == MicrOp.OP_RLCR)):
  99             with m.If(rec.is_32bit):
 100                 comb += me.eq(m_fields.ME[0:-1])
 101             with m.Else():
 102                 comb += me.eq(md_fields.me[0:-1])
 103         with m.Else():
 104             with m.If(rec.is_32bit):
 105                 comb += me.eq(b[0:6])
 106             with m.Else():
 107                 comb += me.eq(63-b)
 108         comb += mr.eq(right_mask(m, me))
 109
 110         # must check Data.ok
 111         o_ok = Signal()
 112         comb += o_ok.eq(1)
 113
 114         # main assertion of arithmetic operations
 115         with m.Switch(itype):
 116
 117             # left-shift: 64/32-bit
 118             with m.Case(MicrOp.OP_SHL):
 119                 comb += Assume(ra == 0)
 120                 with m.If(rec.is_32bit):
 121                     comb += Assert(o[0:32] == ((a << b[0:6]) & 0xffffffff))
 122                     comb += Assert(o[32:64] == 0)
 123                 with m.Else():
 124                     comb += Assert(o == ((a << b[0:7]) & ((1 << 64)-1)))
 125
 126             # right-shift: 64/32-bit / signed
 127             with m.Case(MicrOp.OP_SHR):
 128                 comb += Assume(ra == 0)
 129                 with m.If(~rec.is_signed):
 130                     with m.If(rec.is_32bit):
 131                         comb += Assert(o[0:32] == (a[0:32] >> b[0:6]))
 132                         comb += Assert(o[32:64] == 0)
 133                     with m.Else():
 134                         comb += Assert(o == (a >> b[0:7]))
 135                 with m.Else():
 136                     with m.If(rec.is_32bit):
 137                         comb += Assert(o[0:32] == (a_signed_32 >> b[0:6]))
 138                         comb += Assert(o[32:64] == Repl(a[31], 32))
 139                     with m.Else():
 140                         comb += Assert(o == (a_signed >> b[0:7]))
 141
 142             # extswsli: 32/64-bit moded
 143             with m.Case(MicrOp.OP_EXTSWSLI):
 144                 comb += Assume(ra == 0)
 145                 with m.If(rec.is_32bit):
 146                     comb += Assert(o[0:32] == ((a << b[0:6]) & 0xffffffff))
 147                     comb += Assert(o[32:64] == 0)
 148                 with m.Else():
 149                     # sign-extend to 64 bit
 150                     a_s = Signal(64, reset_less=True)
 151                     comb += a_s.eq(exts(a, 32, 64))
 152                     comb += Assert(o == ((a_s << b[0:7]) & ((1 << 64)-1)))
 153
 154             #TODO
 155             with m.Case(MicrOp.OP_RLC):
 156                 pass
 157             with m.Case(MicrOp.OP_RLCR):
 158                 pass
 159             with m.Case(MicrOp.OP_RLCL):
 160                 pass
 161             with m.Default():
 162                 comb += o_ok.eq(0)
 163
 164         # check that data ok was only enabled when op actioned
 165         comb += Assert(dut.o.o.ok == o_ok)
 166
 167         return m
 168
 169
 170 class ALUTestCase(FHDLTestCase):
 171     def test_formal(self):
 172         module = Driver()
 173         self.assertFormal(module, mode="bmc", depth=2)
 174         self.assertFormal(module, mode="cover", depth=2)
 175     def test_ilang(self):
 176         dut = Driver()
 177         vl = rtlil.convert(dut, ports=[])
 178         with open("main_stage.il", "w") as f:
 179             f.write(vl)
 180
 181
 182 if __name__ == '__main__':
 183     unittest.main()