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

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