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 soc.decoder.power_enums import InternalOp
  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)
  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         comb += dut.i.ctx.op.eq(rec)
  63
  64         # Assert that op gets copied from the input to output
  65         for rec_sig in rec.ports():
  66             name = rec_sig.name
  67             dut_sig = getattr(dut.o.ctx.op, name)
  68             comb += Assert(dut_sig == rec_sig)
  69
  70         # signed and signed/32 versions of input a
  71         a_signed = Signal(signed(64))
  72         a_signed_32 = Signal(signed(32))
  73         comb += a_signed.eq(a)
  74         comb += a_signed_32.eq(a[0:32])
  75
  76         # do not check MSBs of a/b in 32-bit mode
  77         with m.If(rec.is_32bit):
  78             comb += Assume(a[32:64] == 0)
  79             comb += Assume(b[32:64] == 0)
  80
  81         # Data.ok checking.  these only to be valid when there is a change
  82         # in the output that needs to go into a regfile
  83         o_ok = Signal()
  84         cr0_ok = Signal()
  85         ov_ok = Signal()
  86         ca_ok = Signal()
  87         comb += cr0_ok.eq(0)
  88         comb += ov_ok.eq(0)
  89         comb += ca_ok.eq(0)
  90
  91         # main assertion of arithmetic operations
  92         with m.Switch(rec.insn_type):
  93             with m.Case(InternalOp.OP_ADD):
  94
  95                 # check result of 65-bit add-with-carry
  96                 comb += Assert(Cat(o, ca_o) == (a + b + ca_in))
  97
  98                 # CA32 - XXX note this fails! replace with ca_in and it works
  99                 comb += Assert((a[0:32] + b[0:32] + ca_in)[32] == ca32_o)
 100
 101                 # From microwatt execute1.vhdl line 130, calc_ov() function
 102                 comb += Assert(ov_o == ((ca_o ^ o[-1]) & ~(a[-1] ^ b[-1])))
 103                 comb += Assert(ov32_o == ((ca32_o ^ o[31]) & ~(a[31] ^ b[31])))
 104                 comb += ov_ok.eq(1)
 105                 comb += ca_ok.eq(1)
 106                 comb += o_ok.eq(1)
 107
 108             with m.Case(InternalOp.OP_EXTS):
 109                 for i in [1, 2, 4]:
 110                     with m.If(rec.data_len == i):
 111                         # main part, then sign-bit replicated up
 112                         comb += Assert(o[0:i*8] == a[0:i*8])
 113                         comb += Assert(o[i*8:64] == Repl(a[i*8-1], 64-(i*8)))
 114                 comb += o_ok.eq(1)
 115
 116             with m.Case(InternalOp.OP_CMP):
 117                 # CMP is defined as not taking in carry
 118                 comb += Assume(ca_in == 0)
 119                 comb += Assert(o == (a+b)[0:64])
 120
 121             with m.Case(InternalOp.OP_CMPEQB):
 122                 src1 = a[0:8]
 123                 eqs = Signal(8)
 124                 for i in range(8):
 125                     comb += eqs[i].eq(src1 == b[i*8:(i+1)*8])
 126                 comb += Assert(dut.o.cr0.data[2] == eqs.any())
 127                 comb += cr0_ok.eq(1)
 128
 129         # check that data ok was only enabled when op actioned
 130         comb += Assert(dut.o.o.ok == o_ok)
 131         comb += Assert(dut.o.cr0.ok == cr0_ok)
 132         comb += Assert(dut.o.xer_ov.ok == ov_ok)
 133         comb += Assert(dut.o.xer_ca.ok == ca_ok)
 134
 135         return m
 136
 137
 138 class ALUTestCase(FHDLTestCase):
 139     def test_formal(self):
 140         module = Driver()
 141         self.assertFormal(module, mode="bmc", depth=2)
 142         self.assertFormal(module, mode="cover", depth=2)
 143     def test_ilang(self):
 144         dut = Driver()
 145         vl = rtlil.convert(dut, ports=[])
 146         with open("alu_main_stage.il", "w") as f:
 147             f.write(vl)
 148
 149
 150 if __name__ == '__main__':
 151     unittest.main()