src/soc/fu/alu/formal/proof_output_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, signed
   5 from nmigen.asserts import Assert, AnyConst, Assume, Cover
   6 from nmigen.test.utils import FHDLTestCase
   7 from nmigen.cli import rtlil
   8
   9 from soc.fu.alu.output_stage import ALUOutputStage
  10 from soc.fu.alu.pipe_data import ALUPipeSpec
  11 from soc.fu.alu.alu_input_record import CompALUOpSubset
  12 from soc.decoder.power_enums import InternalOp
  13 import unittest
  14
  15
  16 # This defines a module to drive the device under test and assert
  17 # properties about its outputs
  18 class Driver(Elaboratable):
  19     def __init__(self):
  20         # inputs and outputs
  21         pass
  22
  23     def elaborate(self, platform):
  24         m = Module()
  25         comb = m.d.comb
  26
  27         rec = CompALUOpSubset()
  28         recwidth = 0
  29         # Setup random inputs for dut.op
  30         for p in rec.ports():
  31             width = p.width
  32             recwidth += width
  33             comb += p.eq(AnyConst(width))
  34
  35         pspec = ALUPipeSpec(id_wid=2, op_wid=recwidth)
  36         m.submodules.dut = dut = ALUOutputStage(pspec)
  37
  38         o = Signal(64)
  39         carry_out = Signal()
  40         carry_out32 = Signal()
  41         ov = Signal()
  42         ov32 = Signal()
  43         cr0 = Signal(4)
  44         so = Signal()
  45         comb += [dut.i.o.eq(o),
  46                  dut.i.carry_out.eq(carry_out),
  47                  dut.i.so.eq(so),
  48                  dut.i.carry_out32.eq(carry_out32),
  49                  dut.i.cr0.eq(cr0),
  50                  dut.i.ov.eq(ov),
  51                  dut.i.ov32.eq(ov32),
  52                  o.eq(AnyConst(64)),
  53                  carry_out.eq(AnyConst(1)),
  54                  carry_out32.eq(AnyConst(1)),
  55                  ov.eq(AnyConst(1)),
  56                  ov32.eq(AnyConst(1)),
  57                  cr0.eq(AnyConst(4)),
  58                  so.eq(AnyConst(1))]
  59
  60         comb += dut.i.ctx.op.eq(rec)
  61
  62         with m.If(dut.i.ctx.op.invert_out):
  63             comb += Assert(dut.o.o == ~o)
  64         with m.Else():
  65             comb += Assert(dut.o.o == o)
  66
  67         cr_out = Signal.like(cr0)
  68         comb += cr_out.eq(dut.o.cr0)
  69
  70         o_signed = Signal(signed(64))
  71         comb += o_signed.eq(dut.o.o)
  72         # Assert only one of the comparison bits is set
  73         comb += Assert(cr_out[3] + cr_out[2] + cr_out[1] == 1)
  74         with m.If(o_signed == 0):
  75             comb += Assert(cr_out[1] == 1)
  76         with m.Elif(o_signed > 0):
  77             # sigh.  see https://bugs.libre-soc.org/show_bug.cgi?id=305#c61
  78             # for OP_CMP we do b-a rather than a-b (just like ADD) and
  79             # then invert the *test condition*.
  80             with m.If(rec.insn_type == InternalOp.OP_CMP):
  81                 comb += Assert(cr_out[3] == 1)
  82             with m.Else():
  83                 comb += Assert(cr_out[2] == 1)
  84         with m.Elif(o_signed < 0):
  85             # ditto as above
  86             with m.If(rec.insn_type == InternalOp.OP_CMP):
  87                 comb += Assert(cr_out[2] == 1)
  88             with m.Else():
  89                 comb += Assert(cr_out[3] == 1)
  90
  91
  92         # Assert that op gets copied from the input to output
  93         for p in rec.ports():
  94             name = p.name
  95             rec_sig = p
  96             dut_sig = getattr(dut.o.ctx.op, name)
  97             comb += Assert(dut_sig == rec_sig)
  98
  99
 100         return m
 101
 102 class GTCombinerTestCase(FHDLTestCase):
 103     def test_formal(self):
 104         module = Driver()
 105         self.assertFormal(module, mode="bmc", depth=4)
 106         self.assertFormal(module, mode="cover", depth=4)
 107     def test_ilang(self):
 108         dut = Driver()
 109         vl = rtlil.convert(dut, ports=[])
 110         with open("output_stage.il", "w") as f:
 111             f.write(vl)
 112
 113
 114 if __name__ == '__main__':
 115     unittest.main()