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.alu.pipe_data import ALUPipeSpec
  16 from soc.fu.alu.alu_input_record import CompALUOpSubset
  17 from soc.decoder.power_enums import MicrOp
  18 import unittest
  19 from nmutil.extend import exts
  20
  21
  22 # This defines a module to drive the device under test and assert
  23 # properties about its outputs
  24 class Driver(Elaboratable):
  25     def __init__(self):
  26         # inputs and outputs
  27         pass
  28
  29     def elaborate(self, platform):
  30         m = Module()
  31         comb = m.d.comb
  32
  33         rec = CompALUOpSubset()
  34         # Setup random inputs for dut.op
  35         for p in rec.ports():
  36             comb += p.eq(AnyConst(p.width))
  37
  38         pspec = ALUPipeSpec(id_wid=2)
  39         m.submodules.dut = dut = ShiftRotMainStage(pspec)
  40
  41         # convenience variables
  42         a = dut.i.rs
  43         b = dut.i.rb
  44         ra = dut.i.a
  45         carry_in = dut.i.xer_ca[0]
  46         carry_in32 = dut.i.xer_ca[1]
  47         carry_out = dut.o.xer_ca
  48         o = dut.o.o.data
  49
  50         # setup random inputs
  51         comb += a.eq(AnyConst(64))
  52         comb += b.eq(AnyConst(64))
  53         comb += carry_in.eq(AnyConst(1))
  54         comb += carry_in32.eq(AnyConst(1))
  55
  56         # copy operation
  57         comb += dut.i.ctx.op.eq(rec)
  58
  59         # Assert that op gets copied from the input to output
  60         for rec_sig in rec.ports():
  61             name = rec_sig.name
  62             dut_sig = getattr(dut.o.ctx.op, name)
  63             comb += Assert(dut_sig == rec_sig)
  64
  65         # signed and signed/32 versions of input a
  66         a_signed = Signal(signed(64))
  67         a_signed_32 = Signal(signed(32))
  68         comb += a_signed.eq(a)
  69         comb += a_signed_32.eq(a[0:32])
  70
  71         # must check Data.ok
  72         o_ok = Signal()
  73         comb += o_ok.eq(1)
  74
  75         # main assertion of arithmetic operations
  76         with m.Switch(rec.insn_type):
  77
  78             # left-shift: 64/32-bit
  79             with m.Case(MicrOp.OP_SHL):
  80                 comb += Assume(ra == 0)
  81                 with m.If(rec.is_32bit):
  82                     comb += Assert(o[0:32] == ((a << b[0:6]) & 0xffffffff))
  83                     comb += Assert(o[32:64] == 0)
  84                 with m.Else():
  85                     comb += Assert(o == ((a << b[0:7]) & ((1 << 64)-1)))
  86
  87             # right-shift: 64/32-bit / signed
  88             with m.Case(MicrOp.OP_SHR):
  89                 comb += Assume(ra == 0)
  90                 with m.If(~rec.is_signed):
  91                     with m.If(rec.is_32bit):
  92                         comb += Assert(o[0:32] == (a[0:32] >> b[0:6]))
  93                         comb += Assert(o[32:64] == 0)
  94                     with m.Else():
  95                         comb += Assert(o == (a >> b[0:7]))
  96                 with m.Else():
  97                     with m.If(rec.is_32bit):
  98                         comb += Assert(o[0:32] == (a_signed_32 >> b[0:6]))
  99                         comb += Assert(o[32:64] == Repl(a[31], 32))
 100                     with m.Else():
 101                         comb += Assert(o == (a_signed >> b[0:7]))
 102
 103             # extswsli: 32/64-bit moded
 104             with m.Case(MicrOp.OP_EXTSWSLI):
 105                 comb += Assume(ra == 0)
 106                 with m.If(rec.is_32bit):
 107                     comb += Assert(o[0:32] == ((a << b[0:6]) & 0xffffffff))
 108                     comb += Assert(o[32:64] == 0)
 109                 with m.Else():
 110                     # sign-extend to 64 bit
 111                     a_s = Signal(64, reset_less=True)
 112                     comb += a_s.eq(exts(a, 32, 64))
 113                     comb += Assert(o == ((a_s << b[0:7]) & ((1 << 64)-1)))
 114
 115             #TODO
 116             with m.Case(MicrOp.OP_RLC):
 117                 pass
 118             with m.Case(MicrOp.OP_RLCR):
 119                 pass
 120             with m.Case(MicrOp.OP_RLCL):
 121                 pass
 122             with m.Default():
 123                 comb += o_ok.eq(0)
 124
 125         # check that data ok was only enabled when op actioned
 126         comb += Assert(dut.o.o.ok == o_ok)
 127
 128         return m
 129
 130
 131 class ALUTestCase(FHDLTestCase):
 132     def test_formal(self):
 133         module = Driver()
 134         self.assertFormal(module, mode="bmc", depth=2)
 135         self.assertFormal(module, mode="cover", depth=2)
 136     def test_ilang(self):
 137         dut = Driver()
 138         vl = rtlil.convert(dut, ports=[])
 139         with open("main_stage.il", "w") as f:
 140             f.write(vl)
 141
 142
 143 if __name__ == '__main__':
 144     unittest.main()