src/soc/experiment/formal/proof_datamerger.py

   1 # Proof of correctness for DataMerger
   2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
   3 # Copyright (C) 2020 Tobias Platen <tplaten@posteo.de>
   4
   5 from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
   6                     signed)
   7 from nmigen.asserts import Assert, AnyConst, AnySeq, Assume, Cover
   8 from nmutil.formaltest import FHDLTestCase
   9 from nmigen.cli import rtlil
  10
  11 from soc.experiment.l0_cache import DataMerger
  12
  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         array_size = 8
  28         m.submodules.dut = dut = DataMerger(array_size)
  29
  30         # assign anyseq to inputs
  31         for j in range(dut.array_size):
  32             comb += dut.addr_array_i[j].eq(AnyConst(dut.array_size))
  33             comb += dut.data_i[j].eq(AnyConst(16+128))
  34
  35         allzero = 1
  36         for j in range(dut.array_size):
  37             allzero = (dut.addr_array_i[j] == 0) & allzero
  38
  39         with m.If(allzero):
  40             # assert that the output is zero when the datamerger is idle
  41             comb += Assert(dut.data_o == 0)
  42         with m.Else():
  43             comb += Assume(dut.data_o != 0) # at least one output bit is set
  44             for j in range(dut.array_size):
  45                 for b in range(8):
  46                     with m.If(dut.data_o.en[b]):
  47                         comb += Assume(dut.data_i[j].en[b])
  48                 for b in range(128):
  49                     with m.If(dut.data_o.data[b]):
  50                         comb += Assume(dut.data_i[j].data[b])
  51
  52         return m
  53
  54
  55 class DataMergerTestCase(FHDLTestCase):
  56     def test_formal(self):
  57         module = Driver()
  58         # bounded model check first
  59         self.assertFormal(module, mode="bmc", depth=2)
  60         # self.assertFormal(module, mode="cover", depth=2)     # case can happen
  61         # XXX self.assertFormal(module, mode="prove")          # uses induction
  62
  63     def test_ilang(self):
  64         dut = Driver()
  65         vl = rtlil.convert(dut, ports=[])
  66         with open("main_stage.il", "w") as f:
  67             f.write(vl)
  68
  69
  70 if __name__ == '__main__':
  71     unittest.main()