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