Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: m-labs/nmigen
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: e3122ed86790^
Choose a base ref
...
head repository: m-labs/nmigen
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: da61076b57ad
Choose a head ref
  • 2 commits
  • 3 files changed
  • 1 contributor

Commits on Sep 12, 2019

  1. lib.fifo: adjust properties to have consistent naming.

    whitequark committed Sep 12, 2019
    Copy the full SHA
    e3122ed View commit details
  2. lib.fifo: adjust for new CDC primitive conventions.

    Refs #97.
    whitequark committed Sep 12, 2019
    Copy the full SHA
    da61076 View commit details
Showing with 229 additions and 169 deletions.
  1. +160 −101 nmigen/lib/fifo.py
  2. +2 −1 nmigen/test/compat/support.py
  3. +67 −67 nmigen/test/test_lib_fifo.py
261 changes: 160 additions & 101 deletions nmigen/lib/fifo.py
Original file line number Diff line number Diff line change
@@ -2,7 +2,7 @@

from .. import *
from ..asserts import *
from ..tools import log2_int
from ..tools import log2_int, deprecated
from .coding import GrayEncoder
from .cdc import MultiReg

@@ -25,35 +25,37 @@ class FIFOInterface:
Attributes
----------
{attributes}
din : in, width
w_data : in, width
Input data.
writable : out
Asserted if there is space in the queue, i.e. ``we`` can be asserted to write a new entry.
we : in
Write strobe. Latches ``din`` into the queue. Does nothing if ``writable`` is not asserted.
w_rdy : out
Asserted if there is space in the queue, i.e. ``w_en`` can be asserted to write
a new entry.
w_en : in
Write strobe. Latches ``w_data`` into the queue. Does nothing if ``w_rdy`` is not asserted.
{w_attributes}
dout : out, width
Output data. {dout_valid}
readable : out
Asserted if there is an entry in the queue, i.e. ``re`` can be asserted to read this entry.
re : in
Read strobe. Makes the next entry (if any) available on ``dout`` at the next cycle.
Does nothing if ``readable`` is not asserted.
r_data : out, width
Output data. {r_data_valid}
r_rdy : out
Asserted if there is an entry in the queue, i.e. ``r_en`` can be asserted to read
an existing entry.
r_en : in
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}
"""

__doc__ = _doc_template.format(description="""
Data written to the input interface (``din``, ``we``, ``writable``) is buffered and can be
read at the output interface (``dout``, ``re``, ``readable`). The data entry written first
Data written to the input interface (``w_data``, ``w_rdy``, ``w_en``) is buffered and can be
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.
""",
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="""
fwft : bool
First-word fallthrough. If set, when ``readable`` rises, the first entry is already
available, i.e. ``dout`` is valid. Otherwise, after ``readable`` rises, it is necessary
to strobe ``re`` for ``dout`` to become valid.
First-word fallthrough. If set, when ``r_rdy`` rises, the first entry is already
available, i.e. ``r_data`` is valid. Otherwise, after ``r_rdy`` rises, it is necessary
to strobe ``r_en`` for ``r_data`` to become valid.
""".strip(),
w_attributes="",
r_attributes="")
@@ -63,30 +65,66 @@ def __init__(self, width, depth, *, fwft):
self.depth = depth
self.fwft = fwft

self.din = Signal(width, reset_less=True)
self.writable = Signal() # not full
self.we = Signal()
self.w_data = Signal(width, reset_less=True)
self.w_rdy = Signal() # not full
self.w_en = Signal()

self.dout = Signal(width, reset_less=True)
self.readable = Signal() # not empty
self.re = Signal()
self.r_data = Signal(width, reset_less=True)
self.r_rdy = Signal() # not empty
self.r_en = Signal()

def read(self):
"""Read method for simulation."""
assert (yield self.readable)
yield self.re.eq(1)
assert (yield self.r_rdy)
yield self.r_en.eq(1)
yield
value = (yield self.dout)
yield self.re.eq(0)
value = (yield self.r_data)
yield self.r_en.eq(0)
return value

def write(self, data):
"""Write method for simulation."""
assert (yield self.writable)
yield self.din.eq(data)
yield self.we.eq(1)
assert (yield self.w_rdy)
yield self.w_data.eq(data)
yield self.w_en.eq(1)
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):
@@ -108,11 +146,11 @@ class SyncFIFO(Elaboratable, FIFOInterface):
fwft : bool
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
necessary to assert ``re`` for ``dout`` to become valid.
necessary to assert ``r_en`` for ``r_data`` to become valid.
""".strip(),
dout_valid="""
For FWFT queues, valid if ``readable`` is asserted. For non-FWFT queues, valid on the next
cycle after ``readable`` and ``re`` have been asserted.
r_data_valid="""
For FWFT queues, valid if ``r_rdy`` is asserted. For non-FWFT queues, valid on the next
cycle after ``r_rdy`` and ``r_en`` have been asserted.
""".strip(),
attributes="",
r_attributes="""
@@ -129,34 +167,34 @@ def __init__(self, width, depth, *, fwft=True):
def elaborate(self, platform):
m = Module()
m.d.comb += [
self.writable.eq(self.level != self.depth),
self.readable.eq(self.level != 0)
self.w_rdy.eq(self.level != self.depth),
self.r_rdy.eq(self.level != 0)
]

do_read = self.readable & self.re
do_write = self.writable & self.we
do_read = self.r_rdy & self.r_en
do_write = self.w_rdy & self.w_en

storage = Memory(self.width, self.depth)
wrport = m.submodules.wrport = storage.write_port()
rdport = m.submodules.rdport = storage.read_port(
w_port = m.submodules.w_port = storage.write_port()
r_port = m.submodules.r_port = storage.read_port(
domain="comb" if self.fwft else "sync", transparent=self.fwft)
produce = Signal.range(self.depth)
consume = Signal.range(self.depth)

m.d.comb += [
wrport.addr.eq(produce),
wrport.data.eq(self.din),
wrport.en.eq(self.we & self.writable)
w_port.addr.eq(produce),
w_port.data.eq(self.w_data),
w_port.en.eq(self.w_en & self.w_rdy)
]
with m.If(do_write):
m.d.sync += produce.eq(_incr(produce, self.depth))

m.d.comb += [
rdport.addr.eq(consume),
self.dout.eq(rdport.data),
r_port.addr.eq(consume),
self.r_data.eq(r_port.data),
]
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):
m.d.sync += consume.eq(_incr(consume, self.depth))

@@ -201,15 +239,15 @@ class SyncFIFOBuffered(Elaboratable, FIFOInterface):
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.
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.
""".strip(),
parameters="""
fwft : bool
Always set.
""".strip(),
attributes="",
dout_valid="Valid if ``readable`` is asserted.",
r_data_valid="Valid if ``r_rdy`` is asserted.",
r_attributes="""
level : out
Number of unread entries.
@@ -229,21 +267,21 @@ def elaborate(self, platform):
m.submodules.unbuffered = fifo = SyncFIFO(self.width, self.depth - 1, fwft=False)

m.d.comb += [
fifo.din.eq(self.din),
fifo.we.eq(self.we),
self.writable.eq(fifo.writable),
fifo.w_data.eq(self.w_data),
fifo.w_en.eq(self.w_en),
self.w_rdy.eq(fifo.w_rdy),
]

m.d.comb += [
self.dout.eq(fifo.dout),
fifo.re.eq(fifo.readable & (~self.readable | self.re)),
self.r_data.eq(fifo.r_data),
fifo.r_en.eq(fifo.r_rdy & (~self.r_rdy | self.r_en)),
]
with m.If(fifo.re):
m.d.sync += self.readable.eq(1)
with m.Elif(self.re):
m.d.sync += self.readable.eq(0)
with m.If(fifo.r_en):
m.d.sync += self.r_rdy.eq(1)
with m.Elif(self.r_en):
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

@@ -253,21 +291,29 @@ class AsyncFIFO(Elaboratable, FIFOInterface):
description="""
Asynchronous first in, first out queue.
Read and write interfaces are accessed from different clock domains, called ``read``
and ``write``; use :class:`DomainRenamer` to rename them as appropriate for the design.
Read and write interfaces are accessed from different clock domains, which can be set when
constructing the FIFO.
""".strip(),
parameters="""
r_domain : str
Read clock domain.
w_domain : str
Write clock domain.
""".strip(),
attributes="""
fwft : bool
Always set.
""".strip(),
attributes="",
dout_valid="Valid if ``readable`` is asserted.",
r_data_valid="Valid if ``r_rdy`` is asserted.",
r_attributes="",
w_attributes="")

def __init__(self, width, depth):
def __init__(self, width, depth, *, r_domain="read", w_domain="write"):
super().__init__(width, depth, fwft=True)

self._r_domain = r_domain
self._w_domain = w_domain

try:
self._ctr_bits = log2_int(depth, need_pow2=True) + 1
except ValueError as e:
@@ -280,57 +326,57 @@ def elaborate(self, platform):

m = Module()

do_write = self.writable & self.we
do_read = self.readable & self.re
do_write = self.w_rdy & self.w_en
do_read = self.r_rdy & self.r_en

# TODO: extract this pattern into lib.cdc.GrayCounter
produce_w_bin = Signal(self._ctr_bits)
produce_w_nxt = Signal(self._ctr_bits)
m.d.comb += produce_w_nxt.eq(produce_w_bin + do_write)
m.d.write += produce_w_bin.eq(produce_w_nxt)
m.d.comb += produce_w_nxt.eq(produce_w_bin + do_write)
m.d[self._w_domain] += produce_w_bin.eq(produce_w_nxt)

consume_r_bin = Signal(self._ctr_bits)
consume_r_nxt = Signal(self._ctr_bits)
m.d.comb += consume_r_nxt.eq(consume_r_bin + do_read)
m.d.read += consume_r_bin.eq(consume_r_nxt)
m.d.comb += consume_r_nxt.eq(consume_r_bin + do_read)
m.d[self._r_domain] += consume_r_bin.eq(consume_r_nxt)

produce_w_gry = Signal(self._ctr_bits)
produce_r_gry = Signal(self._ctr_bits)
produce_enc = m.submodules.produce_enc = \
GrayEncoder(self._ctr_bits)
produce_cdc = m.submodules.produce_cdc = \
MultiReg(produce_w_gry, produce_r_gry, o_domain="read")
m.d.comb += produce_enc.i.eq(produce_w_nxt),
m.d.write += produce_w_gry.eq(produce_enc.o)
MultiReg(produce_w_gry, produce_r_gry, o_domain=self._r_domain)
m.d.comb += produce_enc.i.eq(produce_w_nxt),
m.d[self._w_domain] += produce_w_gry.eq(produce_enc.o)

consume_r_gry = Signal(self._ctr_bits)
consume_w_gry = Signal(self._ctr_bits)
consume_enc = m.submodules.consume_enc = \
GrayEncoder(self._ctr_bits)
consume_cdc = m.submodules.consume_cdc = \
MultiReg(consume_r_gry, consume_w_gry, o_domain="write")
m.d.comb += consume_enc.i.eq(consume_r_nxt)
m.d.read += consume_r_gry.eq(consume_enc.o)
MultiReg(consume_r_gry, consume_w_gry, o_domain=self._w_domain)
m.d.comb += consume_enc.i.eq(consume_r_nxt)
m.d[self._r_domain] += consume_r_gry.eq(consume_enc.o)

m.d.comb += [
self.writable.eq(
self.w_rdy.eq(
(produce_w_gry[-1] == consume_w_gry[-1]) |
(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)
wrport = m.submodules.wrport = storage.write_port(domain="write")
rdport = m.submodules.rdport = storage.read_port (domain="read")
w_port = m.submodules.w_port = storage.write_port(domain=self._w_domain)
r_port = m.submodules.r_port = storage.read_port (domain=self._r_domain)
m.d.comb += [
wrport.addr.eq(produce_w_bin[:-1]),
wrport.data.eq(self.din),
wrport.en.eq(do_write)
w_port.addr.eq(produce_w_bin[:-1]),
w_port.data.eq(self.w_data),
w_port.en.eq(do_write)
]
m.d.comb += [
rdport.addr.eq((consume_r_bin + do_read)[:-1]),
self.dout.eq(rdport.data),
r_port.addr.eq((consume_r_bin + do_read)[:-1]),
self.r_data.eq(r_port.data),
]

if platform == "formal":
@@ -346,40 +392,53 @@ class AsyncFIFOBuffered(Elaboratable, FIFOInterface):
description="""
Buffered asynchronous first in, first out queue.
Read and write interfaces are accessed from different clock domains, which can be set when
constructing the FIFO.
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.
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.
""".strip(),
parameters="""
r_domain : str
Read clock domain.
w_domain : str
Write clock domain.
""".strip(),
attributes="""
fwft : bool
Always set.
""".strip(),
attributes="",
dout_valid="Valid if ``readable`` is asserted.",
r_data_valid="Valid if ``r_rdy`` is asserted.",
r_attributes="",
w_attributes="")

def __init__(self, width, depth):
def __init__(self, width, depth, *, r_domain="read", w_domain="write"):
super().__init__(width, depth, fwft=True)

self._r_domain = r_domain
self._w_domain = w_domain

def elaborate(self, platform):
m = Module()
m.submodules.unbuffered = fifo = AsyncFIFO(self.width, self.depth - 1)
m.submodules.unbuffered = fifo = AsyncFIFO(self.width, self.depth - 1,
r_domain=self._r_domain, w_domain=self._w_domain)

m.d.comb += [
fifo.din.eq(self.din),
self.writable.eq(fifo.writable),
fifo.we.eq(self.we),
fifo.w_data.eq(self.w_data),
self.w_rdy.eq(fifo.w_rdy),
fifo.w_en.eq(self.w_en),
]

with m.If(self.re | ~self.readable):
m.d.read += [
self.dout.eq(fifo.dout),
self.readable.eq(fifo.readable)
with m.If(self.r_en | ~self.r_rdy):
m.d[self._r_domain] += [
self.r_data.eq(fifo.r_data),
self.r_rdy.eq(fifo.r_rdy),
]
m.d.comb += [
fifo.r_en.eq(1)
]
m.d.comb += \
fifo.re.eq(1)

return m
3 changes: 2 additions & 1 deletion nmigen/test/compat/support.py
Original file line number Diff line number Diff line change
@@ -12,4 +12,5 @@ def test_to_verilog(self):
verilog.convert(self.tb)

def run_with(self, generator):
run_simulation(self.tb, generator)
with _ignore_deprecated():
run_simulation(self.tb, generator)
134 changes: 67 additions & 67 deletions nmigen/test/test_lib_fifo.py
Original file line number Diff line number Diff line change
@@ -12,10 +12,10 @@ def assertSyncFIFOWorks(self, fifo, xfrm=lambda x: x):
def process():
yield from fifo.write(1)
yield from fifo.write(2)
while not (yield fifo.readable):
while not (yield fifo.r_rdy):
yield
if not fifo.fwft:
yield fifo.re.eq(1)
yield fifo.r_en.eq(1)
yield
self.assertEqual((yield from fifo.read()), 1)
self.assertEqual((yield from fifo.read()), 2)
@@ -45,48 +45,48 @@ class FIFOModel(Elaboratable, FIFOInterface):
"""
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)

self.rdomain = rdomain
self.wdomain = wdomain
self.r_domain = r_domain
self.w_domain = w_domain

self.level = Signal.range(self.depth + 1)

def elaborate(self, platform):
m = Module()

storage = Memory(self.width, self.depth)
wrport = m.submodules.wrport = storage.write_port(domain=self.wdomain)
rdport = m.submodules.rdport = storage.read_port (domain="comb")
w_port = m.submodules.w_port = storage.write_port(domain=self.w_domain)
r_port = m.submodules.r_port = storage.read_port (domain="comb")

produce = Signal.range(self.depth)
consume = Signal.range(self.depth)

m.d.comb += self.readable.eq(self.level > 0)
m.d.comb += rdport.addr.eq((consume + 1) % self.depth)
m.d.comb += self.r_rdy.eq(self.level > 0)
m.d.comb += r_port.addr.eq((consume + 1) % self.depth)
if self.fwft:
m.d.comb += self.dout.eq(rdport.data)
with m.If(self.re & self.readable):
m.d.comb += self.r_data.eq(r_port.data)
with m.If(self.r_en & self.r_rdy):
if not self.fwft:
m.d[self.rdomain] += self.dout.eq(rdport.data)
m.d[self.rdomain] += consume.eq(rdport.addr)
m.d[self.r_domain] += self.r_data.eq(r_port.data)
m.d[self.r_domain] += consume.eq(r_port.addr)

m.d.comb += self.writable.eq(self.level < self.depth)
m.d.comb += wrport.data.eq(self.din)
with m.If(self.we & self.writable):
m.d.comb += wrport.addr.eq((produce + 1) % self.depth)
m.d.comb += wrport.en.eq(1)
m.d[self.wdomain] += produce.eq(wrport.addr)
m.d.comb += self.w_rdy.eq(self.level < self.depth)
m.d.comb += w_port.data.eq(self.w_data)
with m.If(self.w_en & self.w_rdy):
m.d.comb += w_port.addr.eq((produce + 1) % self.depth)
m.d.comb += w_port.en.eq(1)
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)
with m.Else():
m.d.sync += self.level.eq(self.level
+ (self.writable & self.we)
- (self.readable & self.re))
+ (self.w_rdy & self.w_en)
- (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

@@ -97,36 +97,36 @@ class FIFOModelEquivalenceSpec(Elaboratable):
signals, the behavior of the implementation under test exactly matches the ideal 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.rdomain = rdomain
self.wdomain = wdomain
self.r_domain = r_domain
self.w_domain = w_domain

def elaborate(self, platform):
m = Module()
m.submodules.dut = dut = self.fifo
m.submodules.gold = gold = FIFOModel(dut.width, dut.depth, dut.fwft,
self.rdomain, self.wdomain)
m.submodules.gold = gold = FIFOModel(dut.width, dut.depth, fwft=dut.fwft,
r_domain=self.r_domain, w_domain=self.w_domain)

m.d.comb += [
gold.re.eq(dut.readable & dut.re),
gold.we.eq(dut.we),
gold.din.eq(dut.din),
gold.r_en.eq(dut.r_rdy & dut.r_en),
gold.w_en.eq(dut.w_en),
gold.w_data.eq(dut.w_data),
]

m.d.comb += Assert(dut.readable.implies(gold.readable))
m.d.comb += Assert(dut.writable.implies(gold.writable))
m.d.comb += Assert(dut.r_rdy.implies(gold.r_rdy))
m.d.comb += Assert(dut.w_rdy.implies(gold.w_rdy))
if hasattr(dut, "level"):
m.d.comb += Assert(dut.level == gold.level)

if dut.fwft:
m.d.comb += Assert(dut.readable
.implies(dut.dout == gold.dout))
m.d.comb += Assert(dut.r_rdy
.implies(dut.r_data == gold.r_data))
else:
m.d.comb += Assert((Past(dut.readable, domain=self.rdomain) &
Past(dut.re, domain=self.rdomain))
.implies(dut.dout == gold.dout))
m.d.comb += Assert((Past(dut.r_rdy, domain=self.r_domain) &
Past(dut.r_en, domain=self.r_domain))
.implies(dut.r_data == gold.r_data))

return m

@@ -137,10 +137,10 @@ class FIFOContractSpec(Elaboratable):
consecutively, they must be read out consecutively at some later point, no matter all other
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.rdomain = rdomain
self.wdomain = wdomain
self.r_domain = r_domain
self.w_domain = w_domain
self.bound = bound

def elaborate(self, platform):
@@ -149,45 +149,45 @@ def elaborate(self, platform):

m.domains += ClockDomain("sync")
m.d.comb += ResetSignal().eq(0)
if self.wdomain != "sync":
m.domains += ClockDomain(self.wdomain)
m.d.comb += ResetSignal(self.wdomain).eq(0)
if self.rdomain != "sync":
m.domains += ClockDomain(self.rdomain)
m.d.comb += ResetSignal(self.rdomain).eq(0)
if self.w_domain != "sync":
m.domains += ClockDomain(self.w_domain)
m.d.comb += ResetSignal(self.w_domain).eq(0)
if self.r_domain != "sync":
m.domains += ClockDomain(self.r_domain)
m.d.comb += ResetSignal(self.r_domain).eq(0)

entry_1 = 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.If(fifo.writable):
with m.If(fifo.w_rdy):
m.d.comb += [
fifo.din.eq(entry_1),
fifo.we.eq(1)
fifo.w_data.eq(entry_1),
fifo.w_en.eq(1)
]
m.next = "WRITE-2"
with m.State("WRITE-2"):
with m.If(fifo.writable):
with m.If(fifo.w_rdy):
m.d.comb += [
fifo.din.eq(entry_2),
fifo.we.eq(1)
fifo.w_data.eq(entry_2),
fifo.w_en.eq(1)
]
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_2 = Signal(fifo.width)
with m.State("READ"):
m.d.comb += fifo.re.eq(1)
m.d.comb += fifo.r_en.eq(1)
if fifo.fwft:
readable = fifo.readable
r_rdy = fifo.r_rdy
else:
readable = Past(fifo.readable, domain=self.rdomain)
with m.If(readable):
r_rdy = Past(fifo.r_rdy, domain=self.r_domain)
with m.If(r_rdy):
m.d.sync += [
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)):
m.next = "DONE"
@@ -198,18 +198,18 @@ def elaborate(self, platform):
with m.If(Past(Initial(), self.bound - 1)):
m.d.comb += Assert(read_fsm.ongoing("DONE"))

if self.wdomain != "sync" or self.rdomain != "sync":
m.d.comb += Assume(Rose(ClockSignal(self.wdomain)) |
Rose(ClockSignal(self.rdomain)))
if self.w_domain != "sync" or self.r_domain != "sync":
m.d.comb += Assume(Rose(ClockSignal(self.w_domain)) |
Rose(ClockSignal(self.r_domain)))

return m


class FIFOFormalCase(FHDLTestCase):
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)
self.assertFormal(FIFOContractSpec(fifo, rdomain="sync", wdomain="sync",
self.assertFormal(FIFOContractSpec(fifo, r_domain="sync", w_domain="sync",
bound=fifo.depth * 2 + 1),
mode="hybrid", depth=fifo.depth * 2 + 1)

@@ -237,9 +237,9 @@ def test_sync_buffered_potm1(self):
def check_async_fifo(self, fifo):
# TODO: properly doing model equivalence checking on this likely requires multiclock,
# 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)
self.assertFormal(FIFOContractSpec(fifo, rdomain="read", wdomain="write",
self.assertFormal(FIFOContractSpec(fifo, r_domain="read", w_domain="write",
bound=fifo.depth * 4 + 1),
mode="hybrid", depth=fifo.depth * 4 + 1)