src/soc/fu/alu/formal/proof_main_stage.py

   1 # Proof of correctness for ALU pipeline, main stage
   2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
   3 """
   4 Links:
   5 * https://bugs.libre-soc.org/show_bug.cgi?id=306
   6 * https://bugs.libre-soc.org/show_bug.cgi?id=305
   7 * https://bugs.libre-soc.org/show_bug.cgi?id=343
   8 """
   9
  10 from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
  11                     signed)
  12 from nmigen.asserts import Assert, AnyConst, Assume, Cover
  13 from nmutil.formaltest import FHDLTestCase
  14 from nmigen.cli import rtlil
  15
  16 from soc.fu.alu.main_stage import ALUMainStage
  17 from soc.fu.alu.pipe_data import ALUPipeSpec
  18 from soc.fu.alu.alu_input_record import CompALUOpSubset
  19 from openpower.decoder.power_enums import MicrOp
  20 import unittest
  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             width = p.width
  38             comb += p.eq(AnyConst(width))
  39
  40         pspec = ALUPipeSpec(id_wid=2, parent_pspec=None)
  41         m.submodules.dut = dut = ALUMainStage(pspec)
  42
  43         # convenience variables
  44         a = dut.i.a
  45         b = dut.i.b
  46         ca_in = dut.i.xer_ca[0]   # CA carry in
  47         ca32_in = dut.i.xer_ca[1]  # CA32 carry in 32
  48         so_in = dut.i.xer_so      # SO sticky overflow
  49
  50         ca_o = dut.o.xer_ca.data[0]   # CA carry out
  51         ca32_o = dut.o.xer_ca.data[1]  # CA32 carry out32
  52         ov_o = dut.o.xer_ov.data[0]   # OV overflow
  53         ov32_o = dut.o.xer_ov.data[1]  # OV32 overflow32
  54         o = dut.o.o.data
  55
  56         # setup random inputs
  57         comb += [a.eq(AnyConst(64)),
  58                  b.eq(AnyConst(64)),
  59                  ca_in.eq(AnyConst(0b11)),
  60                  so_in.eq(AnyConst(1))]
  61
  62         # and for the context muxid
  63         width = dut.i.ctx.muxid.width
  64         comb += dut.i.ctx.muxid.eq(AnyConst(width))
  65
  66         # assign the PowerDecode2 operation subset
  67         comb += dut.i.ctx.op.eq(rec)
  68
  69         # check that the operation (op) is passed through (and muxid)
  70         comb += Assert(dut.o.ctx.op == dut.i.ctx.op)
  71         comb += Assert(dut.o.ctx.muxid == dut.i.ctx.muxid)
  72
  73         # signed and signed/32 versions of input a
  74         a_signed = Signal(signed(64))
  75         a_signed_32 = Signal(signed(32))
  76         comb += a_signed.eq(a)
  77         comb += a_signed_32.eq(a[0:32])
  78
  79         # do not check MSBs of a/b in 32-bit mode
  80         with m.If(rec.is_32bit):
  81             comb += Assume(a[32:64] == 0)
  82             comb += Assume(b[32:64] == 0)
  83
  84         # Data.ok checking.  these only to be valid when there is a change
  85         # in the output that needs to go into a regfile
  86         o_ok = Signal()
  87         cr0_ok = Signal()
  88         ov_ok = Signal()
  89         ca_ok = Signal()
  90         comb += cr0_ok.eq(0)
  91         comb += ov_ok.eq(0)
  92         comb += ca_ok.eq(0)
  93
  94         # main assertion of arithmetic operations
  95         with m.Switch(rec.insn_type):
  96             with m.Case(MicrOp.OP_ADD):
  97
  98                 # check result of 65-bit add-with-carry
  99                 comb += Assert(Cat(o, ca_o) == (a + b + ca_in))
 100
 101                 # CA32 - XXX note this fails! replace with ca_in and it works
 102                 comb += Assert((a[0:32] + b[0:32] + ca_in)[32] == ca32_o)
 103
 104                 # From microwatt execute1.vhdl line 130, calc_ov() function
 105                 comb += Assert(ov_o == ((ca_o ^ o[-1]) & ~(a[-1] ^ b[-1])))
 106                 comb += Assert(ov32_o == ((ca32_o ^ o[31]) & ~(a[31] ^ b[31])))
 107                 comb += ov_ok.eq(1)
 108                 comb += ca_ok.eq(1)
 109                 comb += o_ok.eq(1)
 110
 111             with m.Case(MicrOp.OP_EXTS):
 112                 for i in [1, 2, 4]:
 113                     with m.If(rec.data_len == i):
 114                         # main part, then sign-bit replicated up
 115                         comb += Assert(o[0:i*8] == a[0:i*8])
 116                         comb += Assert(o[i*8:64] == Repl(a[i*8-1], 64-(i*8)))
 117                 comb += o_ok.eq(1)
 118
 119             with m.Case(MicrOp.OP_CMP):
 120                 # CMP is defined as not taking in carry
 121                 comb += Assume(ca_in == 0)
 122                 comb += Assert(o == (a+b)[0:64])
 123
 124             with m.Case(MicrOp.OP_CMPEQB):
 125                 src1 = a[0:8]
 126                 eqs = Signal(8)
 127                 for i in range(8):
 128                     comb += eqs[i].eq(src1 == b[i*8:(i+1)*8])
 129                 comb += Assert(dut.o.cr0.data[2] == eqs.any())
 130                 comb += cr0_ok.eq(1)
 131
 132         # check that data ok was only enabled when op actioned
 133         comb += Assert(dut.o.o.ok == o_ok)
 134         comb += Assert(dut.o.cr0.ok == cr0_ok)
 135         comb += Assert(dut.o.xer_ov.ok == ov_ok)
 136         comb += Assert(dut.o.xer_ca.ok == ca_ok)
 137
 138         return m
 139
 140
 141 class ALUTestCase(FHDLTestCase):
 142     def test_formal(self):
 143         module = Driver()
 144         self.assertFormal(module, mode="bmc", depth=2)
 145         self.assertFormal(module, mode="cover", depth=2)
 146
 147     def test_ilang(self):
 148         dut = Driver()
 149         vl = rtlil.convert(dut, ports=[])
 150         with open("alu_main_stage.il", "w") as f:
 151             f.write(vl)
 152
 153
 154 if __name__ == '__main__':
 155     unittest.main()