lib.fifo: adjust properties to have consistent naming.

This commit is contained in:
whitequark 2019-09-12 19:51:01 +00:00
parent 9ea3ff7ae2
commit da4b810fe1
3 changed files with 189 additions and 150 deletions

View file

@ -2,7 +2,7 @@
from .. import * from .. import *
from ..asserts import * from ..asserts import *
from ..tools import log2_int from ..tools import log2_int, deprecated
from .coding import GrayEncoder from .coding import GrayEncoder
from .cdc import MultiReg from .cdc import MultiReg
@ -25,35 +25,37 @@ class FIFOInterface:
Attributes Attributes
---------- ----------
{attributes} {attributes}
din : in, width w_data : in, width
Input data. Input data.
writable : out w_rdy : out
Asserted if there is space in the queue, i.e. ``we`` can be asserted to write a new entry. Asserted if there is space in the queue, i.e. ``w_en`` can be asserted to write
we : in a new entry.
Write strobe. Latches ``din`` into the queue. Does nothing if ``writable`` is not asserted. w_en : in
Write strobe. Latches ``w_data`` into the queue. Does nothing if ``w_rdy`` is not asserted.
{w_attributes} {w_attributes}
dout : out, width r_data : out, width
Output data. {dout_valid} Output data. {r_data_valid}
readable : out r_rdy : out
Asserted if there is an entry in the queue, i.e. ``re`` can be asserted to read this entry. Asserted if there is an entry in the queue, i.e. ``r_en`` can be asserted to read
re : in an existing entry.
Read strobe. Makes the next entry (if any) available on ``dout`` at the next cycle. r_en : in
Does nothing if ``readable`` is not asserted. Read strobe. Makes the next entry (if any) available on ``r_data`` at the next cycle.
Does nothing if ``r_rdy`` is not asserted.
{r_attributes} {r_attributes}
""" """
__doc__ = _doc_template.format(description=""" __doc__ = _doc_template.format(description="""
Data written to the input interface (``din``, ``we``, ``writable``) is buffered and can be Data written to the input interface (``w_data``, ``w_rdy``, ``w_en``) is buffered and can be
read at the output interface (``dout``, ``re``, ``readable`). The data entry written first read at the output interface (``r_data``, ``r_rdy``, ``r_en`). The data entry written first
to the input also appears first on the output. to the input also appears first on the output.
""", """,
parameters="", parameters="",
dout_valid="The conditions in which ``dout`` is valid depends on the type of the queue.", r_data_valid="The conditions in which ``r_data`` is valid depends on the type of the queue.",
attributes=""" attributes="""
fwft : bool fwft : bool
First-word fallthrough. If set, when ``readable`` rises, the first entry is already First-word fallthrough. If set, when ``r_rdy`` rises, the first entry is already
available, i.e. ``dout`` is valid. Otherwise, after ``readable`` rises, it is necessary available, i.e. ``r_data`` is valid. Otherwise, after ``r_rdy`` rises, it is necessary
to strobe ``re`` for ``dout`` to become valid. to strobe ``r_en`` for ``r_data`` to become valid.
""".strip(), """.strip(),
w_attributes="", w_attributes="",
r_attributes="") r_attributes="")
@ -63,30 +65,66 @@ class FIFOInterface:
self.depth = depth self.depth = depth
self.fwft = fwft self.fwft = fwft
self.din = Signal(width, reset_less=True) self.w_data = Signal(width, reset_less=True)
self.writable = Signal() # not full self.w_rdy = Signal() # not full
self.we = Signal() self.w_en = Signal()
self.dout = Signal(width, reset_less=True) self.r_data = Signal(width, reset_less=True)
self.readable = Signal() # not empty self.r_rdy = Signal() # not empty
self.re = Signal() self.r_en = Signal()
def read(self): def read(self):
"""Read method for simulation.""" """Read method for simulation."""
assert (yield self.readable) assert (yield self.r_rdy)
yield self.re.eq(1) yield self.r_en.eq(1)
yield yield
value = (yield self.dout) value = (yield self.r_data)
yield self.re.eq(0) yield self.r_en.eq(0)
return value return value
def write(self, data): def write(self, data):
"""Write method for simulation.""" """Write method for simulation."""
assert (yield self.writable) assert (yield self.w_rdy)
yield self.din.eq(data) yield self.w_data.eq(data)
yield self.we.eq(1) yield self.w_en.eq(1)
yield yield
yield self.we.eq(0) yield self.w_en.eq(0)
# TODO(nmigen-0.2): move this to nmigen.compat and make it a deprecated extension
@property
@deprecated("instead of `fifo.din`, use `fifo.w_data`")
def din(self):
return self.w_data
# TODO(nmigen-0.2): move this to nmigen.compat and make it a deprecated extension
@property
@deprecated("instead of `fifo.writable`, use `fifo.w_rdy`")
def writable(self):
return self.w_rdy
# TODO(nmigen-0.2): move this to nmigen.compat and make it a deprecated extension
@property
@deprecated("instead of `fifo.we`, use `fifo.w_en`")
def we(self):
return self.w_en
# TODO(nmigen-0.2): move this to nmigen.compat and make it a deprecated extension
@property
@deprecated("instead of `fifo.dout`, use `fifo.r_data`")
def dout(self):
return self.r_data
# TODO(nmigen-0.2): move this to nmigen.compat and make it a deprecated extension
@property
@deprecated("instead of `fifo.readable`, use `fifo.r_rdy`")
def readable(self):
return self.r_rdy
# TODO(nmigen-0.2): move this to nmigen.compat and make it a deprecated extension
@property
@deprecated("instead of `fifo.re`, use `fifo.r_en`")
def re(self):
return self.r_en
def _incr(signal, modulo): def _incr(signal, modulo):
@ -108,11 +146,11 @@ class SyncFIFO(Elaboratable, FIFOInterface):
fwft : bool fwft : bool
First-word fallthrough. If set, when the queue is empty and an entry is written into it, First-word fallthrough. If set, when the queue is empty and an entry is written into it,
that entry becomes available on the output on the same clock cycle. Otherwise, it is that entry becomes available on the output on the same clock cycle. Otherwise, it is
necessary to assert ``re`` for ``dout`` to become valid. necessary to assert ``r_en`` for ``r_data`` to become valid.
""".strip(), """.strip(),
dout_valid=""" r_data_valid="""
For FWFT queues, valid if ``readable`` is asserted. For non-FWFT queues, valid on the next For FWFT queues, valid if ``r_rdy`` is asserted. For non-FWFT queues, valid on the next
cycle after ``readable`` and ``re`` have been asserted. cycle after ``r_rdy`` and ``r_en`` have been asserted.
""".strip(), """.strip(),
attributes="", attributes="",
r_attributes=""" r_attributes="""
@ -129,34 +167,34 @@ class SyncFIFO(Elaboratable, FIFOInterface):
def elaborate(self, platform): def elaborate(self, platform):
m = Module() m = Module()
m.d.comb += [ m.d.comb += [
self.writable.eq(self.level != self.depth), self.w_rdy.eq(self.level != self.depth),
self.readable.eq(self.level != 0) self.r_rdy.eq(self.level != 0)
] ]
do_read = self.readable & self.re do_read = self.r_rdy & self.r_en
do_write = self.writable & self.we do_write = self.w_rdy & self.w_en
storage = Memory(self.width, self.depth) storage = Memory(self.width, self.depth)
wrport = m.submodules.wrport = storage.write_port() w_port = m.submodules.w_port = storage.write_port()
rdport = m.submodules.rdport = storage.read_port( r_port = m.submodules.r_port = storage.read_port(
domain="comb" if self.fwft else "sync", transparent=self.fwft) domain="comb" if self.fwft else "sync", transparent=self.fwft)
produce = Signal.range(self.depth) produce = Signal.range(self.depth)
consume = Signal.range(self.depth) consume = Signal.range(self.depth)
m.d.comb += [ m.d.comb += [
wrport.addr.eq(produce), w_port.addr.eq(produce),
wrport.data.eq(self.din), w_port.data.eq(self.w_data),
wrport.en.eq(self.we & self.writable) w_port.en.eq(self.w_en & self.w_rdy)
] ]
with m.If(do_write): with m.If(do_write):
m.d.sync += produce.eq(_incr(produce, self.depth)) m.d.sync += produce.eq(_incr(produce, self.depth))
m.d.comb += [ m.d.comb += [
rdport.addr.eq(consume), r_port.addr.eq(consume),
self.dout.eq(rdport.data), self.r_data.eq(r_port.data),
] ]
if not self.fwft: if not self.fwft:
m.d.comb += rdport.en.eq(self.re) m.d.comb += r_port.en.eq(self.r_en)
with m.If(do_read): with m.If(do_read):
m.d.sync += consume.eq(_incr(consume, self.depth)) m.d.sync += consume.eq(_incr(consume, self.depth))
@ -201,7 +239,7 @@ class SyncFIFOBuffered(Elaboratable, FIFOInterface):
This queue's interface is identical to :class:`SyncFIFO` configured as ``fwft=True``, but it This queue's interface is identical to :class:`SyncFIFO` configured as ``fwft=True``, but it
does not use asynchronous memory reads, which are incompatible with FPGA block RAMs. does not use asynchronous memory reads, which are incompatible with FPGA block RAMs.
In exchange, the latency between an entry being written to an empty queue and that entry In exchange, the latency betw_enen an entry being written to an empty queue and that entry
becoming available on the output is increased to one cycle. becoming available on the output is increased to one cycle.
""".strip(), """.strip(),
parameters=""" parameters="""
@ -209,7 +247,7 @@ class SyncFIFOBuffered(Elaboratable, FIFOInterface):
Always set. Always set.
""".strip(), """.strip(),
attributes="", attributes="",
dout_valid="Valid if ``readable`` is asserted.", r_data_valid="Valid if ``r_rdy`` is asserted.",
r_attributes=""" r_attributes="""
level : out level : out
Number of unread entries. Number of unread entries.
@ -229,21 +267,21 @@ class SyncFIFOBuffered(Elaboratable, FIFOInterface):
m.submodules.unbuffered = fifo = SyncFIFO(self.width, self.depth - 1, fwft=False) m.submodules.unbuffered = fifo = SyncFIFO(self.width, self.depth - 1, fwft=False)
m.d.comb += [ m.d.comb += [
fifo.din.eq(self.din), fifo.w_data.eq(self.w_data),
fifo.we.eq(self.we), fifo.w_en.eq(self.w_en),
self.writable.eq(fifo.writable), self.w_rdy.eq(fifo.w_rdy),
] ]
m.d.comb += [ m.d.comb += [
self.dout.eq(fifo.dout), self.r_data.eq(fifo.r_data),
fifo.re.eq(fifo.readable & (~self.readable | self.re)), fifo.r_en.eq(fifo.r_rdy & (~self.r_rdy | self.r_en)),
] ]
with m.If(fifo.re): with m.If(fifo.r_en):
m.d.sync += self.readable.eq(1) m.d.sync += self.r_rdy.eq(1)
with m.Elif(self.re): with m.Elif(self.r_en):
m.d.sync += self.readable.eq(0) m.d.sync += self.r_rdy.eq(0)
m.d.comb += self.level.eq(fifo.level + self.readable) m.d.comb += self.level.eq(fifo.level + self.r_rdy)
return m return m
@ -261,7 +299,7 @@ class AsyncFIFO(Elaboratable, FIFOInterface):
Always set. Always set.
""".strip(), """.strip(),
attributes="", attributes="",
dout_valid="Valid if ``readable`` is asserted.", r_data_valid="Valid if ``r_rdy`` is asserted.",
r_attributes="", r_attributes="",
w_attributes="") w_attributes="")
@ -280,8 +318,8 @@ class AsyncFIFO(Elaboratable, FIFOInterface):
m = Module() m = Module()
do_write = self.writable & self.we do_write = self.w_rdy & self.w_en
do_read = self.readable & self.re do_read = self.r_rdy & self.r_en
# TODO: extract this pattern into lib.cdc.GrayCounter # TODO: extract this pattern into lib.cdc.GrayCounter
produce_w_bin = Signal(self._ctr_bits) produce_w_bin = Signal(self._ctr_bits)
@ -313,24 +351,24 @@ class AsyncFIFO(Elaboratable, FIFOInterface):
m.d.read += consume_r_gry.eq(consume_enc.o) m.d.read += consume_r_gry.eq(consume_enc.o)
m.d.comb += [ m.d.comb += [
self.writable.eq( self.w_rdy.eq(
(produce_w_gry[-1] == consume_w_gry[-1]) | (produce_w_gry[-1] == consume_w_gry[-1]) |
(produce_w_gry[-2] == consume_w_gry[-2]) | (produce_w_gry[-2] == consume_w_gry[-2]) |
(produce_w_gry[:-2] != consume_w_gry[:-2])), (produce_w_gry[:-2] != consume_w_gry[:-2])),
self.readable.eq(consume_r_gry != produce_r_gry) self.r_rdy.eq(consume_r_gry != produce_r_gry)
] ]
storage = Memory(self.width, self.depth) storage = Memory(self.width, self.depth)
wrport = m.submodules.wrport = storage.write_port(domain="write") w_port = m.submodules.w_port = storage.write_port(domain="write")
rdport = m.submodules.rdport = storage.read_port (domain="read") r_port = m.submodules.r_port = storage.read_port (domain="read")
m.d.comb += [ m.d.comb += [
wrport.addr.eq(produce_w_bin[:-1]), w_port.addr.eq(produce_w_bin[:-1]),
wrport.data.eq(self.din), w_port.data.eq(self.w_data),
wrport.en.eq(do_write) w_port.en.eq(do_write)
] ]
m.d.comb += [ m.d.comb += [
rdport.addr.eq((consume_r_bin + do_read)[:-1]), r_port.addr.eq((consume_r_bin + do_read)[:-1]),
self.dout.eq(rdport.data), self.r_data.eq(r_port.data),
] ]
if platform == "formal": if platform == "formal":
@ -349,7 +387,7 @@ class AsyncFIFOBuffered(Elaboratable, FIFOInterface):
This queue's interface is identical to :class:`AsyncFIFO`, but it has an additional register This queue's interface is identical to :class:`AsyncFIFO`, but it has an additional register
on the output, improving timing in case of block RAM that has large clock-to-output delay. on the output, improving timing in case of block RAM that has large clock-to-output delay.
In exchange, the latency between an entry being written to an empty queue and that entry In exchange, the latency betw_enen an entry being written to an empty queue and that entry
becoming available on the output is increased to one cycle. becoming available on the output is increased to one cycle.
""".strip(), """.strip(),
parameters=""" parameters="""
@ -357,7 +395,7 @@ class AsyncFIFOBuffered(Elaboratable, FIFOInterface):
Always set. Always set.
""".strip(), """.strip(),
attributes="", attributes="",
dout_valid="Valid if ``readable`` is asserted.", r_data_valid="Valid if ``r_rdy`` is asserted.",
r_attributes="", r_attributes="",
w_attributes="") w_attributes="")
@ -369,17 +407,17 @@ class AsyncFIFOBuffered(Elaboratable, FIFOInterface):
m.submodules.unbuffered = fifo = AsyncFIFO(self.width, self.depth - 1) m.submodules.unbuffered = fifo = AsyncFIFO(self.width, self.depth - 1)
m.d.comb += [ m.d.comb += [
fifo.din.eq(self.din), fifo.w_data.eq(self.w_data),
self.writable.eq(fifo.writable), self.w_rdy.eq(fifo.w_rdy),
fifo.we.eq(self.we), fifo.w_en.eq(self.w_en),
] ]
with m.If(self.re | ~self.readable): with m.If(self.r_en | ~self.r_rdy):
m.d.read += [ m.d.read += [
self.dout.eq(fifo.dout), self.r_data.eq(fifo.r_data),
self.readable.eq(fifo.readable) self.r_rdy.eq(fifo.r_rdy)
] ]
m.d.comb += \ m.d.comb += \
fifo.re.eq(1) fifo.r_en.eq(1)
return m return m

View file

@ -12,4 +12,5 @@ class SimCase:
verilog.convert(self.tb) verilog.convert(self.tb)
def run_with(self, generator): def run_with(self, generator):
run_simulation(self.tb, generator) with _ignore_deprecated():
run_simulation(self.tb, generator)

View file

@ -12,10 +12,10 @@ class FIFOSmokeTestCase(FHDLTestCase):
def process(): def process():
yield from fifo.write(1) yield from fifo.write(1)
yield from fifo.write(2) yield from fifo.write(2)
while not (yield fifo.readable): while not (yield fifo.r_rdy):
yield yield
if not fifo.fwft: if not fifo.fwft:
yield fifo.re.eq(1) yield fifo.r_en.eq(1)
yield yield
self.assertEqual((yield from fifo.read()), 1) self.assertEqual((yield from fifo.read()), 1)
self.assertEqual((yield from fifo.read()), 2) self.assertEqual((yield from fifo.read()), 2)
@ -45,11 +45,11 @@ class FIFOModel(Elaboratable, FIFOInterface):
""" """
Non-synthesizable first-in first-out queue, implemented naively as a chain of registers. Non-synthesizable first-in first-out queue, implemented naively as a chain of registers.
""" """
def __init__(self, width, depth, fwft, rdomain, wdomain): def __init__(self, width, depth, *, fwft, r_domain, w_domain):
super().__init__(width, depth, fwft=fwft) super().__init__(width, depth, fwft=fwft)
self.rdomain = rdomain self.r_domain = r_domain
self.wdomain = wdomain self.w_domain = w_domain
self.level = Signal.range(self.depth + 1) self.level = Signal.range(self.depth + 1)
@ -57,36 +57,36 @@ class FIFOModel(Elaboratable, FIFOInterface):
m = Module() m = Module()
storage = Memory(self.width, self.depth) storage = Memory(self.width, self.depth)
wrport = m.submodules.wrport = storage.write_port(domain=self.wdomain) w_port = m.submodules.w_port = storage.write_port(domain=self.w_domain)
rdport = m.submodules.rdport = storage.read_port (domain="comb") r_port = m.submodules.r_port = storage.read_port (domain="comb")
produce = Signal.range(self.depth) produce = Signal.range(self.depth)
consume = Signal.range(self.depth) consume = Signal.range(self.depth)
m.d.comb += self.readable.eq(self.level > 0) m.d.comb += self.r_rdy.eq(self.level > 0)
m.d.comb += rdport.addr.eq((consume + 1) % self.depth) m.d.comb += r_port.addr.eq((consume + 1) % self.depth)
if self.fwft: if self.fwft:
m.d.comb += self.dout.eq(rdport.data) m.d.comb += self.r_data.eq(r_port.data)
with m.If(self.re & self.readable): with m.If(self.r_en & self.r_rdy):
if not self.fwft: if not self.fwft:
m.d[self.rdomain] += self.dout.eq(rdport.data) m.d[self.r_domain] += self.r_data.eq(r_port.data)
m.d[self.rdomain] += consume.eq(rdport.addr) m.d[self.r_domain] += consume.eq(r_port.addr)
m.d.comb += self.writable.eq(self.level < self.depth) m.d.comb += self.w_rdy.eq(self.level < self.depth)
m.d.comb += wrport.data.eq(self.din) m.d.comb += w_port.data.eq(self.w_data)
with m.If(self.we & self.writable): with m.If(self.w_en & self.w_rdy):
m.d.comb += wrport.addr.eq((produce + 1) % self.depth) m.d.comb += w_port.addr.eq((produce + 1) % self.depth)
m.d.comb += wrport.en.eq(1) m.d.comb += w_port.en.eq(1)
m.d[self.wdomain] += produce.eq(wrport.addr) m.d[self.w_domain] += produce.eq(w_port.addr)
with m.If(ResetSignal(self.rdomain) | ResetSignal(self.wdomain)): with m.If(ResetSignal(self.r_domain) | ResetSignal(self.w_domain)):
m.d.sync += self.level.eq(0) m.d.sync += self.level.eq(0)
with m.Else(): with m.Else():
m.d.sync += self.level.eq(self.level m.d.sync += self.level.eq(self.level
+ (self.writable & self.we) + (self.w_rdy & self.w_en)
- (self.readable & self.re)) - (self.r_rdy & self.r_en))
m.d.comb += Assert(ResetSignal(self.rdomain) == ResetSignal(self.wdomain)) m.d.comb += Assert(ResetSignal(self.r_domain) == ResetSignal(self.w_domain))
return m return m
@ -97,36 +97,36 @@ class FIFOModelEquivalenceSpec(Elaboratable):
signals, the behavior of the implementation under test exactly matches the ideal model, signals, the behavior of the implementation under test exactly matches the ideal model,
except for behavior not defined by the model. except for behavior not defined by the model.
""" """
def __init__(self, fifo, rdomain, wdomain): def __init__(self, fifo, r_domain, w_domain):
self.fifo = fifo self.fifo = fifo
self.rdomain = rdomain self.r_domain = r_domain
self.wdomain = wdomain self.w_domain = w_domain
def elaborate(self, platform): def elaborate(self, platform):
m = Module() m = Module()
m.submodules.dut = dut = self.fifo m.submodules.dut = dut = self.fifo
m.submodules.gold = gold = FIFOModel(dut.width, dut.depth, dut.fwft, m.submodules.gold = gold = FIFOModel(dut.width, dut.depth, fwft=dut.fwft,
self.rdomain, self.wdomain) r_domain=self.r_domain, w_domain=self.w_domain)
m.d.comb += [ m.d.comb += [
gold.re.eq(dut.readable & dut.re), gold.r_en.eq(dut.r_rdy & dut.r_en),
gold.we.eq(dut.we), gold.w_en.eq(dut.w_en),
gold.din.eq(dut.din), gold.w_data.eq(dut.w_data),
] ]
m.d.comb += Assert(dut.readable.implies(gold.readable)) m.d.comb += Assert(dut.r_rdy.implies(gold.r_rdy))
m.d.comb += Assert(dut.writable.implies(gold.writable)) m.d.comb += Assert(dut.w_rdy.implies(gold.w_rdy))
if hasattr(dut, "level"): if hasattr(dut, "level"):
m.d.comb += Assert(dut.level == gold.level) m.d.comb += Assert(dut.level == gold.level)
if dut.fwft: if dut.fwft:
m.d.comb += Assert(dut.readable m.d.comb += Assert(dut.r_rdy
.implies(dut.dout == gold.dout)) .implies(dut.r_data == gold.r_data))
else: else:
m.d.comb += Assert((Past(dut.readable, domain=self.rdomain) & m.d.comb += Assert((Past(dut.r_rdy, domain=self.r_domain) &
Past(dut.re, domain=self.rdomain)) Past(dut.r_en, domain=self.r_domain))
.implies(dut.dout == gold.dout)) .implies(dut.r_data == gold.r_data))
return m return m
@ -137,10 +137,10 @@ class FIFOContractSpec(Elaboratable):
consecutively, they must be read out consecutively at some later point, no matter all other consecutively, they must be read out consecutively at some later point, no matter all other
circumstances, with the exception of reset. circumstances, with the exception of reset.
""" """
def __init__(self, fifo, rdomain, wdomain, bound): def __init__(self, fifo, r_domain, w_domain, bound):
self.fifo = fifo self.fifo = fifo
self.rdomain = rdomain self.r_domain = r_domain
self.wdomain = wdomain self.w_domain = w_domain
self.bound = bound self.bound = bound
def elaborate(self, platform): def elaborate(self, platform):
@ -149,45 +149,45 @@ class FIFOContractSpec(Elaboratable):
m.domains += ClockDomain("sync") m.domains += ClockDomain("sync")
m.d.comb += ResetSignal().eq(0) m.d.comb += ResetSignal().eq(0)
if self.wdomain != "sync": if self.w_domain != "sync":
m.domains += ClockDomain(self.wdomain) m.domains += ClockDomain(self.w_domain)
m.d.comb += ResetSignal(self.wdomain).eq(0) m.d.comb += ResetSignal(self.w_domain).eq(0)
if self.rdomain != "sync": if self.r_domain != "sync":
m.domains += ClockDomain(self.rdomain) m.domains += ClockDomain(self.r_domain)
m.d.comb += ResetSignal(self.rdomain).eq(0) m.d.comb += ResetSignal(self.r_domain).eq(0)
entry_1 = AnyConst(fifo.width) entry_1 = AnyConst(fifo.width)
entry_2 = AnyConst(fifo.width) entry_2 = AnyConst(fifo.width)
with m.FSM(domain=self.wdomain) as write_fsm: with m.FSM(domain=self.w_domain) as write_fsm:
with m.State("WRITE-1"): with m.State("WRITE-1"):
with m.If(fifo.writable): with m.If(fifo.w_rdy):
m.d.comb += [ m.d.comb += [
fifo.din.eq(entry_1), fifo.w_data.eq(entry_1),
fifo.we.eq(1) fifo.w_en.eq(1)
] ]
m.next = "WRITE-2" m.next = "WRITE-2"
with m.State("WRITE-2"): with m.State("WRITE-2"):
with m.If(fifo.writable): with m.If(fifo.w_rdy):
m.d.comb += [ m.d.comb += [
fifo.din.eq(entry_2), fifo.w_data.eq(entry_2),
fifo.we.eq(1) fifo.w_en.eq(1)
] ]
m.next = "DONE" m.next = "DONE"
with m.FSM(domain=self.rdomain) as read_fsm: with m.FSM(domain=self.r_domain) as read_fsm:
read_1 = Signal(fifo.width) read_1 = Signal(fifo.width)
read_2 = Signal(fifo.width) read_2 = Signal(fifo.width)
with m.State("READ"): with m.State("READ"):
m.d.comb += fifo.re.eq(1) m.d.comb += fifo.r_en.eq(1)
if fifo.fwft: if fifo.fwft:
readable = fifo.readable r_rdy = fifo.r_rdy
else: else:
readable = Past(fifo.readable, domain=self.rdomain) r_rdy = Past(fifo.r_rdy, domain=self.r_domain)
with m.If(readable): with m.If(r_rdy):
m.d.sync += [ m.d.sync += [
read_1.eq(read_2), read_1.eq(read_2),
read_2.eq(fifo.dout), read_2.eq(fifo.r_data),
] ]
with m.If((read_1 == entry_1) & (read_2 == entry_2)): with m.If((read_1 == entry_1) & (read_2 == entry_2)):
m.next = "DONE" m.next = "DONE"
@ -198,18 +198,18 @@ class FIFOContractSpec(Elaboratable):
with m.If(Past(Initial(), self.bound - 1)): with m.If(Past(Initial(), self.bound - 1)):
m.d.comb += Assert(read_fsm.ongoing("DONE")) m.d.comb += Assert(read_fsm.ongoing("DONE"))
if self.wdomain != "sync" or self.rdomain != "sync": if self.w_domain != "sync" or self.r_domain != "sync":
m.d.comb += Assume(Rose(ClockSignal(self.wdomain)) | m.d.comb += Assume(Rose(ClockSignal(self.w_domain)) |
Rose(ClockSignal(self.rdomain))) Rose(ClockSignal(self.r_domain)))
return m return m
class FIFOFormalCase(FHDLTestCase): class FIFOFormalCase(FHDLTestCase):
def check_sync_fifo(self, fifo): def check_sync_fifo(self, fifo):
self.assertFormal(FIFOModelEquivalenceSpec(fifo, rdomain="sync", wdomain="sync"), self.assertFormal(FIFOModelEquivalenceSpec(fifo, r_domain="sync", w_domain="sync"),
mode="bmc", depth=fifo.depth + 1) mode="bmc", depth=fifo.depth + 1)
self.assertFormal(FIFOContractSpec(fifo, rdomain="sync", wdomain="sync", self.assertFormal(FIFOContractSpec(fifo, r_domain="sync", w_domain="sync",
bound=fifo.depth * 2 + 1), bound=fifo.depth * 2 + 1),
mode="hybrid", depth=fifo.depth * 2 + 1) mode="hybrid", depth=fifo.depth * 2 + 1)
@ -237,9 +237,9 @@ class FIFOFormalCase(FHDLTestCase):
def check_async_fifo(self, fifo): def check_async_fifo(self, fifo):
# TODO: properly doing model equivalence checking on this likely requires multiclock, # TODO: properly doing model equivalence checking on this likely requires multiclock,
# which is not really documented nor is it clear how to use it. # which is not really documented nor is it clear how to use it.
# self.assertFormal(FIFOModelEquivalenceSpec(fifo, rdomain="read", wdomain="write"), # self.assertFormal(FIFOModelEquivalenceSpec(fifo, r_domain="read", w_domain="write"),
# mode="bmc", depth=fifo.depth * 3 + 1) # mode="bmc", depth=fifo.depth * 3 + 1)
self.assertFormal(FIFOContractSpec(fifo, rdomain="read", wdomain="write", self.assertFormal(FIFOContractSpec(fifo, r_domain="read", w_domain="write",
bound=fifo.depth * 4 + 1), bound=fifo.depth * 4 + 1),
mode="hybrid", depth=fifo.depth * 4 + 1) mode="hybrid", depth=fifo.depth * 4 + 1)