lib.fifo: adjust properties to have consistent naming.
This commit is contained in:
parent
9ea3ff7ae2
commit
da4b810fe1
|
@ -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
|
||||||
|
|
|
@ -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)
|
||||||
|
|
|
@ -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)
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue