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 from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
   5                     signed)
   6 from nmigen.asserts import Assert, AnyConst, Assume, Cover
   7 from nmigen.test.utils import FHDLTestCase
   8 from nmigen.cli import rtlil
   9
  10 from soc.fu.shift_rot.main_stage import ShiftRotMainStage
  11 from soc.fu.alu.pipe_data import ALUPipeSpec
  12 from soc.fu.alu.alu_input_record import CompALUOpSubset
  13 from soc.decoder.power_enums import InternalOp
  14 import unittest
  15
  16
  17 # This defines a module to drive the device under test and assert
  18 # properties about its outputs
  19 class Driver(Elaboratable):
  20     def __init__(self):
  21         # inputs and outputs
  22         pass
  23
  24     def elaborate(self, platform):
  25         m = Module()
  26         comb = m.d.comb
  27
  28         rec = CompALUOpSubset()
  29         # Setup random inputs for dut.op
  30         for p in rec.ports():
  31             comb += p.eq(AnyConst(p.width))
  32
  33         pspec = ALUPipeSpec(id_wid=2)
  34         m.submodules.dut = dut = ShiftRotMainStage(pspec)
  35
  36         # convenience variables
  37         a = dut.i.rs
  38         b = dut.i.rb
  39         ra = dut.i.a
  40         carry_in = dut.i.xer_ca[0]
  41         carry_in32 = dut.i.xer_ca[1]
  42         carry_out = dut.o.xer_ca
  43         o = dut.o.o
  44
  45         # setup random inputs
  46         comb += [a.eq(AnyConst(64)),
  47                  b.eq(AnyConst(64)),
  48                  carry_in.eq(AnyConst(1)),
  49                  carry_in32.eq(AnyConst(1)),
  50                  ]
  51
  52         comb += dut.i.ctx.op.eq(rec)
  53
  54         # Assert that op gets copied from the input to output
  55         for rec_sig in rec.ports():
  56             name = rec_sig.name
  57             dut_sig = getattr(dut.o.ctx.op, name)
  58             comb += Assert(dut_sig == rec_sig)
  59
  60         # signed and signed/32 versions of input a
  61         a_signed = Signal(signed(64))
  62         a_signed_32 = Signal(signed(32))
  63         comb += a_signed.eq(a)
  64         comb += a_signed_32.eq(a[0:32])
  65
  66         # main assertion of arithmetic operations
  67         with m.Switch(rec.insn_type):
  68             with m.Case(InternalOp.OP_SHL):
  69                 comb += Assume(ra == 0)
  70                 with m.If(rec.is_32bit):
  71                     comb += Assert(o[0:32] == ((a << b[0:6]) & 0xffffffff))
  72                     comb += Assert(o[32:64] == 0)
  73                 with m.Else():
  74                     comb += Assert(o == ((a << b[0:7]) & ((1 << 64)-1)))
  75             with m.Case(InternalOp.OP_SHR):
  76                 comb += Assume(ra == 0)
  77                 with m.If(~rec.is_signed):
  78                     with m.If(rec.is_32bit):
  79                         comb += Assert(o[0:32] == (a[0:32] >> b[0:6]))
  80                         comb += Assert(o[32:64] == 0)
  81                     with m.Else():
  82                         comb += Assert(o == (a >> b[0:7]))
  83                 with m.Else():
  84                     with m.If(rec.is_32bit):
  85                         comb += Assert(o[0:32] == (a_signed_32 >> b[0:6]))
  86                         comb += Assert(o[32:64] == Repl(a[31], 32))
  87                     with m.Else():
  88                         comb += Assert(o == (a_signed >> b[0:7]))
  89
  90         return m
  91
  92
  93 class ALUTestCase(FHDLTestCase):
  94     def test_formal(self):
  95         module = Driver()
  96         self.assertFormal(module, mode="bmc", depth=2)
  97         self.assertFormal(module, mode="cover", depth=2)
  98     def test_ilang(self):
  99         dut = Driver()
 100         vl = rtlil.convert(dut, ports=[])
 101         with open("main_stage.il", "w") as f:
 102             f.write(vl)
 103
 104
 105 if __name__ == '__main__':
 106     unittest.main()