src/soc/experiment/formal/proof_alu_fsm.py

   1 import unittest
   2 import os
   3
   4 from nmigen import Elaboratable, Signal, Module
   5 from nmigen.asserts import Assert, Assume, Cover, Past, Stable
   6 from nmigen.cli import rtlil
   7
   8 from nmutil.formaltest import FHDLTestCase
   9 from nmutil.gtkw import write_gtkw
  10
  11 from soc.experiment.alu_fsm import Shifter
  12
  13
  14 # This defines a module to drive the device under test and assert
  15 # properties about its outputs
  16 class Driver(Elaboratable):
  17     def __init__(self):
  18         # inputs and outputs
  19         pass
  20
  21     @staticmethod
  22     def elaborate(_):
  23         m = Module()
  24         comb = m.d.comb
  25         sync = m.d.sync
  26
  27         m.submodules.dut = dut = Shifter(8)
  28         # Coverage condition (one bit for each coverage case)
  29         cov = Signal(8)
  30         # input data to the shifter
  31         data_i = Signal(8)
  32         shift_i = Signal(8)
  33         op_sdir = Signal()
  34         # expected result
  35         expected = Signal(8)
  36         # transaction count for each port
  37         write_cnt = Signal(4)
  38         read_cnt = Signal(4)
  39         # keep data and valid stable, until accepted
  40         with m.If(Past(dut.p.valid_i) & ~Past(dut.p.ready_o)):
  41             comb += [
  42                 Assume(Stable(dut.op.sdir)),
  43                 Assume(Stable(dut.p.data_i.data)),
  44                 Assume(Stable(dut.p.data_i.shift)),
  45                 Assume(Stable(dut.p.valid_i)),
  46             ]
  47         # force reading the output in a reasonable time,
  48         # necessary to pass induction
  49         with m.If(Past(dut.n.valid_o) & ~Past(dut.n.ready_i)):
  50             comb += Assume(dut.n.ready_i)
  51         # capture transferred input data
  52         with m.If(dut.p.ready_o & dut.p.valid_i):
  53             sync += [
  54                 data_i.eq(dut.p.data_i.data),
  55                 shift_i.eq(dut.p.data_i.shift),
  56                 op_sdir.eq(dut.op.sdir),
  57                 # increment write counter
  58                 write_cnt.eq(write_cnt + 1),
  59             ]
  60             # calculate the expected result
  61             dut_data_i = dut.p.data_i.data
  62             dut_shift_i = dut.p.data_i.shift[:4]
  63             dut_sdir = dut.op.sdir
  64             with m.If(dut_sdir):
  65                 sync += expected.eq(dut_data_i >> dut_shift_i)
  66             with m.Else():
  67                 sync += expected.eq(dut_data_i << dut_shift_i)
  68         # check coverage as output data is accepted
  69         with m.If(dut.n.ready_i & dut.n.valid_o):
  70             # increment read counter
  71             sync += read_cnt.eq(read_cnt + 1)
  72             # check result
  73             comb += Assert(dut.n.data_o.data == expected)
  74             # cover zero data, with zero and non-zero shift
  75             # (any direction)
  76             with m.If(data_i == 0):
  77                 with m.If(shift_i == 0):
  78                     sync += cov[0].eq(1)
  79                 with m.If(shift_i[:3].any() & ~shift_i[3]):
  80                     sync += cov[1].eq(1)
  81             # cover non-zero data, with zero and non-zero shift
  82             # (both directions)
  83             with m.If(data_i != 0):
  84                 with m.If(shift_i == 0):
  85                     sync += cov[2].eq(1)
  86                 with m.If(shift_i[:3].any() & ~shift_i[3]):
  87                     with m.If(op_sdir):
  88                         sync += cov[3].eq(1)
  89                     with m.Else():
  90                         sync += cov[4].eq(1)
  91                 # cover big shift
  92                 with m.If(shift_i[3] != 0):
  93                     sync += cov[5].eq(1)
  94             # cover non-zero shift giving non-zero result
  95             with m.If(data_i.any() & shift_i.any() & dut.n.data_o.data.any()):
  96                 sync += cov[6].eq(1)
  97             # dummy condition, to avoid optimizing-out the counters
  98             with m.If((write_cnt != 0) | (read_cnt != 0)):
  99                 sync += cov[7].eq(1)
 100         # check that each condition above occurred at least once
 101         comb += Cover(cov.all())
 102         return m
 103
 104
 105 class ALUFSMTestCase(FHDLTestCase):
 106     def test_formal(self):
 107         traces = [
 108             'clk',
 109             'p_data_i[7:0]', 'p_shift_i[7:0]', 'op__sdir',
 110             'p_valid_i', 'p_ready_o',
 111             'n_data_o[7:0]',
 112             'n_valid_o', 'n_ready_i',
 113             ('formal', {'module': 'top'}, [
 114                 'write_cnt[3:0]', 'read_cnt[3:0]', 'cov[7:0]'
 115             ])
 116         ]
 117         write_gtkw(
 118             'test_formal_cover_alu_fsm.gtkw',
 119             os.path.dirname(__file__) +
 120             '/proof_alu_fsm_formal/engine_0/trace0.vcd',
 121             traces,
 122             module='top.dut',
 123             zoom=-6.3
 124         )
 125         write_gtkw(
 126             'test_formal_bmc_alu_fsm.gtkw',
 127             os.path.dirname(__file__) +
 128             '/proof_alu_fsm_formal/engine_0/trace.vcd',
 129             traces,
 130             module='top.dut',
 131             zoom=-6.3
 132         )
 133         write_gtkw(
 134             'test_formal_induct_alu_fsm.gtkw',
 135             os.path.dirname(__file__) +
 136             '/proof_alu_fsm_formal/engine_0/trace_induct.vcd',
 137             traces,
 138             module='top.dut',
 139             zoom=-6.3
 140         )
 141         module = Driver()
 142         self.assertFormal(module, mode="prove", depth=18)
 143         self.assertFormal(module, mode="cover", depth=32)
 144
 145     @staticmethod
 146     def test_rtlil():
 147         dut = Driver()
 148         vl = rtlil.convert(dut, ports=[])
 149         with open("alu_fsm.il", "w") as f:
 150             f.write(vl)
 151
 152
 153 if __name__ == '__main__':
 154     unittest.main()