src/soc/minerva/test/test_cache.py

   1 from nmigen import Elaboratable, Module, Signal, Record
   2 from nmutil.formaltest import FHDLTestCase
   3 from nmigen.asserts import AnyConst, AnySeq, Assert, Assume, Past, Initial
   4
   5 from soc.minerva.cache import L1Cache
   6
   7
   8 class L1CacheSpec(Elaboratable):
   9     """
  10     A cache read at a given address must either:
  11     - miss and start a cache refill;
  12     - hit and return the last refilled value for that address.
  13     """
  14     def __init__(self, cache):
  15         self.cache = cache
  16
  17     def elaborate(self, platform):
  18         m = Module()
  19         m.submodules.dut = cache = self.cache
  20
  21         addr  = AnyConst(cache.s1_addr.shape())
  22         s1_re = AnySeq(1)
  23
  24         with m.If(~cache.s1_stall):
  25             m.d.sync += [
  26                 cache.s2_addr.eq(cache.s1_addr),
  27                 cache.s2_re.eq(s1_re),
  28                 cache.s2_valid.eq(cache.s1_valid)
  29             ]
  30
  31         m.d.comb += Assume(cache.s1_valid.implies(cache.s1_addr == addr))
  32         with m.If(cache.s2_re & cache.s2_miss & cache.s2_valid):
  33             m.d.comb += Assume(cache.s1_stall)
  34
  35         spec_s2_rdata = Signal(32)
  36         spec_bus_re   = Signal()
  37         spec_bus_addr = Record.like(cache.bus_addr)
  38         spec_bus_last = Signal()
  39         last_offset   = Signal.like(cache.s2_addr.offset)
  40
  41         with m.If(~Past(cache.s1_stall)):
  42             with m.If(cache.s2_re & cache.s2_miss & cache.s2_valid):
  43                 m.d.sync += [
  44                     spec_bus_re.eq(1),
  45                     spec_bus_addr.eq(cache.s2_addr),
  46                     last_offset.eq(cache.s2_addr.offset - 1)
  47                 ]
  48
  49         with m.If(cache.bus_re):
  50             with m.If(cache.bus_valid):
  51                 # Lines are refilled with an incremental burst that
  52                 # starts at the missed address
  53                 # and wraps around the offset bits.
  54                 m.d.sync += spec_bus_addr.offset.eq(spec_bus_addr.offset + 1)
  55                 with m.If((cache.bus_addr == cache.s2_addr) & ~cache.bus_error):
  56                     m.d.sync += spec_s2_rdata.eq(cache.bus_rdata)
  57             # A burst ends when all words in the line have
  58             # been refilled, or an error occured.
  59             m.d.comb += spec_bus_last.eq(cache.bus_addr.offset == last_offset)
  60             with m.If(cache.bus_valid & cache.bus_last | cache.bus_error):
  61                 m.d.sync += spec_bus_re.eq(0)
  62
  63         with m.If(cache.s2_re & cache.s2_valid & ~cache.s2_miss):
  64             m.d.comb += Assert(cache.s2_rdata == spec_s2_rdata)
  65
  66         m.d.comb += Assert(cache.bus_re == spec_bus_re)
  67         with m.If(cache.bus_re):
  68             m.d.comb += [
  69                 Assert(cache.bus_addr == spec_bus_addr),
  70                 Assert(cache.bus_last == spec_bus_last)
  71             ]
  72
  73         with m.If(Initial()):
  74             m.d.comb += [
  75                 Assume(cache.s1_stall),
  76                 Assume(~cache.s2_valid),
  77                 Assume(~cache.bus_re),
  78                 Assume(~spec_bus_re)
  79             ]
  80
  81         return m
  82
  83
  84 class L1CacheTestCase(FHDLTestCase):
  85     def check(self, cache):
  86         self.assertFormal(L1CacheSpec(cache), mode="bmc", depth=10)
  87
  88     def test_direct_mapped(self):
  89         self.check(L1Cache(nways=1, nlines=2, nwords=4, base=0, limit=1024))
  90
  91     def test_2_ways(self):
  92         self.check(L1Cache(nways=2, nlines=2, nwords=4, base=0, limit=1024))