src/soc/fu/alu/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.alu.main_stage import ALUMainStage
  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             width = p.width
  32             comb += p.eq(AnyConst(width))
  33
  34         pspec = ALUPipeSpec(id_wid=2)
  35         m.submodules.dut = dut = ALUMainStage(pspec)
  36
  37         # convenience variables
  38         a = dut.i.a
  39         b = dut.i.b
  40         ca_in = dut.i.xer_ca[0]   # CA carry in
  41         ca32_in = dut.i.xer_ca[1] # CA32 carry in 32
  42         so_in = dut.i.xer_so      # SO sticky overflow
  43
  44         ca_o = dut.o.xer_ca.data[0]   # CA carry out
  45         ca32_o = dut.o.xer_ca.data[1] # CA32 carry out32
  46         ov_o = dut.o.xer_ov.data[0]   # OV overflow
  47         ov32_o = dut.o.xer_ov.data[1] # OV32 overflow32
  48         o = dut.o.o.data
  49
  50         # setup random inputs
  51         comb += [a.eq(AnyConst(64)),
  52                  b.eq(AnyConst(64)),
  53                  ca_in.eq(AnyConst(0b11)),
  54                  so_in.eq(AnyConst(1))]
  55
  56         comb += dut.i.ctx.op.eq(rec)
  57
  58         # Assert that op gets copied from the input to output
  59         for rec_sig in rec.ports():
  60             name = rec_sig.name
  61             dut_sig = getattr(dut.o.ctx.op, name)
  62             comb += Assert(dut_sig == rec_sig)
  63
  64         # signed and signed/32 versions of input a
  65         a_signed = Signal(signed(64))
  66         a_signed_32 = Signal(signed(32))
  67         comb += a_signed.eq(a)
  68         comb += a_signed_32.eq(a[0:32])
  69
  70         with m.If(rec.is_32bit):
  71             comb += Assume(a[32:64] == 0)
  72             comb += Assume(b[32:64] == 0)
  73
  74         o_ok = Signal()
  75         comb += o_ok.eq(1) # will be set to zero if no op takes place
  76
  77         # main assertion of arithmetic operations
  78         with m.Switch(rec.insn_type):
  79             with m.Case(InternalOp.OP_ADD):
  80
  81                 comb += Assert(Cat(o, ca_o) == (a + b + ca_in))
  82
  83                 # CA32 - XXX note this fails! replace with ca_in and it works
  84                 comb += Assert((a[0:32] + b[0:32] + ca_in)[32] == ca32_o)
  85
  86                 # From microwatt execute1.vhdl line 130
  87                 comb += Assert(ov_o == ((ca_o ^ o[-1]) & ~(a[-1] ^ b[-1])))
  88                 comb += Assert(ov32_o == ((ca32_o ^ o[31]) & ~(a[31] ^ b[31])))
  89
  90             with m.Case(InternalOp.OP_EXTS):
  91                 for i in [1, 2, 4]:
  92                     with m.If(rec.data_len == i):
  93                         comb += Assert(o[0:i*8] == a[0:i*8])
  94                         comb += Assert(o[i*8:64] == Repl(a[i*8-1], 64-(i*8)))
  95
  96             with m.Case(InternalOp.OP_CMP):
  97                 # CMP is defined as not taking in carry
  98                 comb += Assume(ca_in == 0)
  99                 comb += Assert(o == (a+b)[0:64])
 100
 101             with m.Case(InternalOp.OP_CMPEQB):
 102                 src1 = a[0:8]
 103                 eqs = Signal(8)
 104                 for i in range(8):
 105                     comb += eqs[i].eq(src1 == b[i*8:(i+1)*8])
 106                 comb += Assert(dut.o.cr0.data[2] == eqs.any())
 107
 108             with m.Default():
 109                 comb += o_ok.eq(0)
 110
 111         # check that data ok was only enabled when op actioned
 112         comb += Assert(dut.o.o.ok == o_ok)
 113         #comb += Assert(dut.o.xer_ca.ok == o_ok)
 114
 115         return m
 116
 117
 118 class ALUTestCase(FHDLTestCase):
 119     def test_formal(self):
 120         module = Driver()
 121         self.assertFormal(module, mode="bmc", depth=2)
 122         self.assertFormal(module, mode="cover", depth=2)
 123     def test_ilang(self):
 124         dut = Driver()
 125         vl = rtlil.convert(dut, ports=[])
 126         with open("alu_main_stage.il", "w") as f:
 127             f.write(vl)
 128
 129
 130 if __name__ == '__main__':
 131     unittest.main()