src/soc/experiment/formal/proof_icache.py

   1 from nmigen import (Cat, Const, Elaboratable, Module, Signal, signed)
   2 from nmigen.asserts import (Assert, AnyConst, AnySeq, Assume)
   3 from nmutil.formaltest import FHDLTestCase
   4 from nmutil.stageapi import StageChain
   5 from nmigen.cli import rtlil
   6
   7 import unittest
   8
   9 from soc.experiment.icache import ICache
  10
  11 from nmigen_soc.wishbone.sram import SRAM
  12 from nmigen import Memory
  13
  14 class Driver(Elaboratable):
  15     def elaborate(self, platform):
  16         m     = Module()
  17         comb  = m.d.comb
  18         sync  = m.d.sync
  19
  20         mem_init = [(i*2) | ((i*2+1) << 32) for i in range(512)]
  21         memory   = Memory(width=64, depth=512, init=mem_init)
  22         sram     = SRAM(memory=memory, granularity=8)
  23
  24         m.submodules.dut  = dut = ICache()
  25         m.submodules.sram = sram
  26
  27         m.d.comb += sram.bus.cyc.eq(dut.wb_out.cyc)
  28         m.d.comb += sram.bus.stb.eq(dut.wb_out.stb)
  29         m.d.comb += sram.bus.we.eq(dut.wb_out.we)
  30         m.d.comb += sram.bus.sel.eq(dut.wb_out.sel)
  31         m.d.comb += sram.bus.adr.eq(dut.wb_out.adr)
  32         m.d.comb += sram.bus.dat_w.eq(dut.wb_out.dat)
  33
  34         m.d.comb += dut.wb_in.ack.eq(sram.bus.ack)
  35         m.d.comb += dut.wb_in.dat.eq(sram.bus.dat_r)
  36
  37         i_out     = dut.i_in
  38         i_in      = dut.i_out
  39         m_out     = dut.m_in
  40         stall_in  = dut.stall_in
  41         stall_out = dut.stall_out
  42         flush_in  = dut.flush_in
  43         inval_in  = dut.inval_in
  44         wb_in     = dut.wb_in
  45         wb_out    = dut.wb_out
  46         log_out   = dut.log_out
  47
  48
  49 class ICacheTestCase(FHDLTestCase):
  50     def test_formal(self):
  51         self.assertFormal(Driver(), mode="bmc", depth=10)
  52         self.assertFormal(Driver(), mode="cover", depth=10)
  53
  54     def test_ilang(self):
  55         vl = rtlil.convert(Driver(), ports=[])
  56         with open("icache_formal.il", "w") as f:
  57             f.write(vl)
  58
  59
  60 if __name__ == '__main__':
  61     unittest.main()