This "minimal" example is kind of long, but you said you[Whitequark] think you know what buy we're hitting. I'll keep this example as is for now and try to trim it later.

"""Simple example of a FSM-based ALU

This demonstrates a design that follows the valid/ready protocol of the
ALU, but with a FSM implementation, instead of a pipeline.  It is also
intended to comply with both the CompALU API and the nmutil Pipeline API
(Liskov Substitution Principle)

The basic rules are:

1) p.ready_o is asserted on the initial ("Idle") state, otherwise it keeps low.
2) n.valid_o is asserted on the final ("Done") state, otherwise it keeps low.
3) The FSM stays in the Idle state while p.valid_i is low, otherwise
   it accepts the input data and moves on.
4) The FSM stays in the Done state while n.ready_i is low, otherwise
   it releases the output data and goes back to the Idle state.

"""

from nmigen import Elaboratable, Signal, Module, Cat
cxxsim = True
if cxxsim:
    from nmigen.sim.cxxsim import Simulator, Settle
else:
    from nmigen.back.pysim import Simulator, Settle
from nmigen.cli import rtlil
from math import log2


class Dummy:
    pass


class Shifter(Elaboratable):
    """Simple sequential shifter

    Prev port data:
    * p.data_i.data:  value to be shifted
    * p.data_i.shift: shift amount
    *                 When zero, no shift occurs.
    *                 On POWER, range is 0 to 63 for 32-bit,
    *                 and 0 to 127 for 64-bit.
    *                 Other values wrap around.

    Next port data:
    * n.data_o.data: shifted value
    """
    class PrevData:
        def __init__(self, width):
            self.data = Signal(width, name="p_data_i")
            self.shift = Signal(width, name="p_shift_i")

        def _get_data(self):
            return [self.data, self.shift]

    class NextData:
        def __init__(self, width):
            self.data = Signal(width, name="n_data_o")

        def _get_data(self):
            return [self.data]

    def __init__(self, width):
        self.width = width
        self.p = Dummy()
        self.n = Dummy()
        self.p.valid_i = Signal(name="p_valid_i")
        self.p.ready_o = Signal(name="p_ready_o")
        self.n.ready_i = Signal(name="n_ready_i")
        self.n.valid_o = Signal(name="n_valid_o")

        self.p.data_i = Shifter.PrevData(width)
        self.n.data_o = Shifter.NextData(width)

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

        # Note:
        # It is good practice to design a sequential circuit as
        # a data path and a control path.

        # Data path
        # ---------
        # The idea is to have a register that can be
        # loaded or shifted (left and right).

        # the control signals
        load = Signal()
        shift = Signal()
        # the data flow
        shift_in = Signal(self.width)
        shift_left_by_1 = Signal(self.width)
        next_shift = Signal(self.width)
        # the register
        shift_reg = Signal(self.width, reset_less=True)
        # build the data flow
        m.d.comb += [
            # connect input and output
            shift_in.eq(self.p.data_i.data),
            self.n.data_o.data.eq(shift_reg),
            # generate shifted views of the register
            shift_left_by_1.eq(Cat(0, shift_reg[:-1])),
        ]
        # choose the next value of the register according to the
        # control signals
        # default is no change
        m.d.comb += next_shift.eq(shift_reg)
        with m.If(load):
            m.d.comb += next_shift.eq(shift_in)
        with m.Elif(shift):
            m.d.comb += next_shift.eq(shift_left_by_1)

        # register the next value
        m.d.sync += shift_reg.eq(next_shift)

        # Control path
        # ------------
        # The idea is to have a SHIFT state where the shift register
        # is shifted every cycle, while a counter decrements.
        # This counter is loaded with shift amount in the initial state.
        # The SHIFT state is left when the counter goes to zero.

        # Shift counter
        shift_width = int(log2(self.width)) + 1
        next_count = Signal(shift_width)
        count = Signal(shift_width, reset_less=True)
        m.d.sync += count.eq(next_count)

        #m.d.comb += self.p.ready_o.eq(1)

        with m.FSM():
            with m.State("IDLE"):
                m.d.comb += [
                    # keep p.ready_o active on IDLE
                    self.p.ready_o.eq(1),
                    # keep loading the shift register and shift count
                    load.eq(1),
                    next_count.eq(self.p.data_i.shift),
                ]
                with m.If(self.p.valid_i):
                    # Leave IDLE when data arrives
                    with m.If(next_count == 0):
                        # short-circuit for zero shift
                        m.next = "DONE"
                    with m.Else():
                        m.next = "SHIFT"
            with m.State("SHIFT"):
                m.d.comb += [
                    # keep shifting, while counter is not zero
                    shift.eq(1),
                    # decrement the shift counter
                    next_count.eq(count - 1),
                ]
                with m.If(next_count == 0):
                    # exit when shift counter goes to zero
                    m.next = "DONE"
            with m.State("DONE"):
                # keep n.valid_o active while the data is not accepted
                m.d.comb += self.n.valid_o.eq(1)
                with m.If(self.n.ready_i):
                    # go back to IDLE when the data is accepted
                    m.next = "IDLE"

        return m

    def __iter__(self):
        yield self.p.data_i.data
        yield self.p.data_i.shift
        yield self.p.valid_i
        yield self.p.ready_o
        yield self.n.ready_i
        yield self.n.valid_o
        yield self.n.data_o.data

    def ports(self):
        return list(self)


def test_shifter():
    m = Module()
    m.submodules.shf = dut = Shifter(8)
    print("Shifter port names:")
    for port in dut:
        print("-", port.name)
    # generate RTLIL
    # try "proc; show" in yosys to check the data path
    il = rtlil.convert(dut, ports=dut.ports())
    with open("test_shifter.il", "w") as f:
        f.write(il)
    sim = Simulator(m)
    sim.add_clock(1e-6)

    def send(data, shift):
        yield
        yield
        yield
        yield
        yield
        yield
        yield
        # present input data and assert valid_i
        yield dut.p.data_i.data.eq(data)
        yield dut.p.data_i.shift.eq(shift)
        yield dut.p.valid_i.eq(1)
        yield
        print ("set up signals")
        # wait for p.ready_o to be asserted
        ready_o = yield dut.p.ready_o
        print ("ready_o", ready_o)
        while not (yield dut.p.ready_o):
            ready_o = yield dut.p.ready_o
            print ("ready_o", ready_o)
            yield
        print ("done ready check")
        # clear input data and negate p.valid_i
        yield dut.p.valid_i.eq(0)
        yield dut.p.data_i.data.eq(0)
        yield dut.p.data_i.shift.eq(0)
        print ("done send")

    def receive(expected):
        yield
        # signal readiness to receive data
        yield dut.n.ready_i.eq(1)
        yield
        # wait for n.valid_o to be asserted
        valid_o = yield dut.n.valid_o
        print ("        valid_o", valid_o)
        while not (yield dut.n.valid_o):
            valid_o = yield dut.n.valid_o
            print ("        valid_o", valid_o)
            yield

        # read result
        result = yield dut.n.data_o.data

        # "FIX" the problem with this line:
        #yield    # <---- remove this - pysim "works" but cxxsim does not

        # negate n.ready_i
        yield dut.n.ready_i.eq(0)
        # check result
        assert result == expected
        print ("        done receive")

    def producer():
        print ("start of producer")
        yield from send(3, 4)
        print ("end of producer")

    def consumer():
        yield
        # the consumer is not in step with the producer, but the
        # order of the results are preserved
        # 3 << 4 = 48
        print ("        start of receiver")
        yield from receive(48)
        print ("        end of receiver")

    sim.add_sync_process(producer)
    sim.add_sync_process(consumer)
    sim_writer = sim.write_vcd(
        "test_shifter.vcd",
    )
    with sim_writer:
        sim.run()


if __name__ == "__main__":
    test_shifter()

Issue by dlharmon Sunday Sep 22, 2019 at 20:56 GMT Originally opened as https://github.com/m-labs/nmigen/pull/227

Related: #212

This tags the first register in each MultiReg or ResetSynchronizer with the attribute nmigen_async_ff and then applies a false path and max delay constraint to all registers tagged with that attribute in the .xdc file.

The max delay defaults to 5 ns and has an override, max_delay where it can be changed for the > whole project. It's possible to make this an argument to MultiReg instead, but is more complex. > git commit -m "add clock domain crossing constraints on Vivado This tags the first register in each MultiReg or ResetSynchronizer with the attribute nmigen_async_ff and then applies a false path and max delay constraint to all registers tagged with that attribute in the .xdc file.

The max delay defaults to 5 ns and has an override, max_delay where it can be changed for the whole project. It's possible to make this an optional argument to MultiReg instead, but is more complex. It would probably work to set nmigen_async_ff to the desired delay rather than just TRUE. I'm not sure how hard it would be to extract that in the TCL or if it would be easier to keep a dict of all used delay values and put a line for each into the .xdc file.

dlharmon included the following code: https://github.com/m-labs/nmigen/pull/227/commits

Issue by ZirconiumX Saturday Sep 21, 2019 at 16:24 GMT Originally opened as https://github.com/m-labs/nmigen/pull/221

This adds SDR support for Altera chips, or at least enough flops and buffers for it.

ZirconiumX included the following code: https://github.com/m-labs/nmigen/pull/221/commits

Issue by jfng Tuesday Mar 19, 2019 at 19:14 GMT Originally opened as https://github.com/m-labs/nmigen/pull/46

• Tests are missing.
• This PR depends on https://github.com/m-labs/nmigen/pull/45

This is a proof-of-concept for a nMigen equivalent of Migen's build system.

The main difference lies in the use of Edalize to invoke vendor tools instead of doing so ourselves.

However, as far as I understand, constraint file (XDC, PCF, etc.) formatting must still be done on our side, which prevents nMigen from being completely vendor agnostic.

jfng included the following code: https://github.com/m-labs/nmigen/pull/46/commits

Issue by RobertBaruch Monday Oct 14, 2019 at 14:23 GMT Originally opened as https://github.com/m-labs/nmigen/issues/254

When dumping the result of covers and counterexamples, Symbiyosys writes .vcd files. However, any signals that were enums or FSM states are no longer strings, but just plain old binary.

In gtkwave, it's possible to select a signal and then Edit > Data Format > Translate Filter File. You can then select a filter file, which is just a map of original value to string value:

00 ZERO
01 FIRST
02 TOOOO

The configuration can also be saved in a .gtkw file. However, this only affects displayed signals. If you delete the signal and display it again, it is not translated. This is horrible.

Proposal:

Better might be to just go into the vcd file and edit the values. Although it would require an extra step, I wouldn't object to something like this:

python3 <toplevel.py> stringify <input_vcd> -o <output_vcd>

This would parse the input vcd file, replace numeric values with string values for enum and fsm states, and output the result.

Issue by whitequark Monday Dec 17, 2018 at 20:57 GMT Originally opened as https://github.com/m-labs/nmigen/issues/9

I know @jordens expressed in the past a desire to simplify the boilerplate around .get_fragment. Also, there is currently both Module.lower and Module.get_fragment (aliased to one another), which is confusing and unnecessary. Also#2, Migen has a Module.get_fragment() and combining Migen modules with nMigen modules gets even more confusing with that.

The design I see for the function currently named .get_fragment() is as follows:

• There are 2 kinds of synthesizable entities in nMigen: fragments (which are directly synthesizable) and anything that has .get_fragment(platform) (which is iterated to a fixed point, i.e. a fragment, when a fragment is required).
• Instances, memory ports, etc, are synthesizable. Which class they actually are is an implementation detail that is subject to change. (Instances are currently just fragments, memory ports are significantly more complex due to some mismatch between Yosys and Migen representation of ports, etc).
• There is a Fragment.get(obj, platform) function that iterates an object to a fixed point with .get_fragment(platform) or fails in a nice way.

Modules are in a somewhat weird space here. Modules should be synthesizable so that you can replace:

sm = Module()
# ... operate on sm
m = Module()
m.submodules += sm

with:

class SubCircuit:
    def get_fragment(self, platform):
        m = Module()
        return m.lower(platform)
sm = SubCircuit()
m = Module()
m.submodules += sm

that is without having to do downstream changes after replacing a Module with a user class. This means that in principle you can directly return a module, like return m.

But this means two things:

1. The actual get_fragment call for that module is delayed. The conversion of a module to a fragment is mostly (but not entirely) error-free, so delaying this call means some errors lose context. I think it might be more useful to make Module.get_fragment actually never fail, and permit return m.
2. If a parent module directly calls get_fragment on a submodule, it gets a Module object with the DSL enabled, as opposed to a Fragment object. So it can potentially abuse the DSL that way. This isn't very likely so maybe we should just ignore it.

And finally, there is an important question of what to rename .get_fragment too. I don't want something like .build because it is ambiguous and prone to collisions. What about .synthesize?

Issue by RobertBaruch Monday Sep 02, 2019 at 21:09 GMT Originally opened as https://github.com/m-labs/nmigen/issues/193

assert_fail.py is nMigen source, and assert_pass.sv should be the equivalent SV code. However, the Assert in assert_fail.py passes when it should not.

failme.sby runs Symbiyosys against assert_fail.py and erroneously passes.

passme.sby runs Symbiyosys against assert_pass.sv and correctly fails.

assert_fail.zip

Issue by emilazy Saturday Sep 14, 2019 at 21:28 GMT Originally opened as https://github.com/m-labs/nmigen/issues/207

#206:

we don't currently have anything like first-class enumerated signals

In response to #292 we've added operators that reinterpret a value of any signedness as a signed or unsigned value of the same width. It would be nice to have an operator that changes the width of a value, too.

Current workaround: for truncation, use v[:new_width]; for extension, use a no-op bitwise operation, like v | C(0, new_width).

• Downside: this code is confusing when it is encountered among a bunch of arithmetic operations.
• Downside: this code is fragile because neither of these operations is guaranteed to return a value with width new_width.

The workaround seems unacceptable to me.

Proposal 1: add two new operators, v.trunc(new_width) for truncation and v.extend(new_width) for zero/sign extension depending on the signedness of v. The new operators would make it an error to truncate to a larger width, or extend to a smaller width than the width of v.

• Upside: the new operators reliably return a value with requested width.
• Upside: the new operators eliminate bugs caused by extension being used instead of truncation or vice versa
• Downside: the new operators accept a width, not a shape, so there is no way to extend a value until it matches the width inferred for range or an enum.
• Downside: two new operators with quite limited use

Proposal 2: like Proposal 1, but the operators accept a new_shape rather than new_width, enforcing the same preconditions. The signedness of the result matches the signedness of the shape.

• Upside: the new operators reliably return a value with requested width.
• Upside: the new operators eliminate bugs caused by extension being used instead of truncation or vice versa
• Upside: the new operators are quite expressive, and as_unsigned/as_signed can be implemented in terms of either.
• Downside: two new flexible operators but "either extend or truncate"--chiefly what happens in x.eq(y)--still isn't expressible and requires an intermediate wire

Proposal 3: add one new operator, v.as(new_shape) for truncation, zero/sign extension, and type conversion. The new operator would extend v if new_shape.width > len(v), truncate v if new_shape.width < len(v), and return a value with shape new_shape.

• Upside: the new operator reliably returns a value with requested width.
• Upside: one operator that can express every implicit shape conversion done by nMigen, including as_unsigned/as_signed.
• Downside: the new operator can hide bugs caused by extension being used instead of truncation or vice versa

Proposal 4: Proposals 2 and 3 at the same time

Thoughts?

Issue by emilazy Monday Sep 30, 2019 at 00:22 GMT Originally opened as https://github.com/m-labs/nmigen/issues/242

It's currently broken in PyPy and I feel like I've managed to poke it into memory unsafe behaviour from the CPython REPL before. Only pysim uses it so I imagine it could pretty easily be replaced with a combination of Python's bigints and lists.

The following code seems to cause a YoSys parser error when it is built:

from nmigen import *
from nmigen_boards.icestick import *

class Parsicide( Elaboratable ):
  def __init__( self ):
    self.a = Signal( 32, reset = 0 )
    self.b = Signal( 32, reset = 0 )
    self.y = Signal( 32, reset = 0 )
  def elaborate( self, platform ):
    m = Module()
    m.d.comb += self.y.eq( self.a << self.b )
    return m

if __name__ == "__main__":
  ICEStickPlatform().build( Parsicide(), do_program = False )

This is the error I get:

Traceback (most recent call last):
  File "yosys_err.py", line 15, in <module>
    ICEStickPlatform().build( Parsicide(), do_program = False )
  File "[...]/nmigen/build/plat.py", line 78, in build
    plan = self.prepare(elaboratable, name, **kwargs)
  File "[...]/nmigen/build/plat.py", line 151, in prepare
    return self.toolchain_prepare(fragment, name, **kwargs)
  File "[...]/nmigen/build/plat.py", line 398, in toolchain_prepare
    render(content_tpl, origin=content_tpl))
  File "[...]/nmigen/build/plat.py", line 392, in render
    "autogenerated": autogenerated,
  File "[...]/jinja2/environment.py", line 1090, in render
    self.environment.handle_exception()
  File "[...]/jinja2/environment.py", line 832, in handle_exception
    reraise(*rewrite_traceback_stack(source=source))
  File "[...]/jinja2/_compat.py", line 28, in reraise
    raise value.with_traceback(tb)
  File "<template>", line 2, in top-level template code
  File "[...]/nmigen/build/plat.py", line 294, in emit_debug_verilog
    strip_internal_attrs=False, write_verilog_opts=opts)
  File "[...]/nmigen/back/verilog.py", line 67, in _convert_rtlil_text
    raise YosysError(error.strip())
nmigen.back.verilog.YosysError: ERROR: Parser error in line 29: invalid slice

Replacing the left shift with a right shift results in the module building without problems (besides the 'no clocks' warnings). I think I'm using a pretty recent version of YoSys: 0.9+1706 (git sha1 ed4fa19b)

Repro:

import enum
from amaranth import *
from amaranth.lib import data


class B(enum.Enum):
    FOO = 0b00
    BAR = 0b01


class A(data.Struct):
    b: B
    c: unsigned(1)


a = A()
print(len(a.b)) # 1

The width of an enum Field is currently inferred from Shape.cast(), as the smallest width required to represent all of its members.

In the above example, a user may actually want the A.b field to have a width of 2 bits. Currently, the enum would need a third member with a value of 0b10 or 0b11.

In the 0.3 release, overrides such as nextpnr_opts can be specified as a list of strings, which are joined together by the options filter in the jinja2 templates. However, #694 adds type checking to get_override() that defaults to requiring a string, so a list is rejected before it's passed to options.

This ends up being a breaking change from 0.3, but I don't know what behaviour you'd rather have. It seems convenient to keep allowing lists and using the options filter, but then get_override should probably accept both strings and lists-of-strings by default. Another option is to always require strings and remove the options filter altogether.

What are your thoughts about adding PEP 484 / PEP 526 type hints to the amaranth.* code? I know that many functions are documented in docstrings, but this lets static analyzers have a go at validating user-written code. If you're game, I'd like to try.

I am attempting to use a ResetSynchronizer with Vivado, and I am finding that the timing analysis for the implementation is not being done properly (and arguably the implementation schematic is also wrong).

My minimal example to show this is:

#!/usr/bin/env python3

from amaranth import *
import amaranth.cli
from amaranth.lib.cdc import ResetSynchronizer
from amaranth.vendor.xilinx import XilinxPlatform


class Test(Elaboratable):
    def __init__(self):
        self.rst_in = Signal()
        self.toggle = Signal()
        self.rstdomain = ClockDomain()

    def elaborate(self, platform):
        m = Module()
        m.domains += self.rstdomain
        rst_in_q = Signal(reset=1)
        m.submodules.sync_rst = ResetSynchronizer(rst_in_q)
        m.d.rstdomain += rst_in_q.eq(self.rst_in)
        m.d.sync += self.toggle.eq(~self.toggle)
        return m


class MyPlatform(XilinxPlatform):
    device = "xc7z010"
    package = "clg400"
    speed = "1"
    resources = []
    connectors = []


if __name__ == '__main__':
    top = Test()
    platform = MyPlatform()
    amaranth.cli.main(
        top, platform=platform,
        ports=[top.rst_in, top.toggle,
               top.rstdomain.clk, top.rstdomain.rst])

This has a rstdomain clock domain for an external reset input rst_in, which is registered by the flip-flop rst_in_q. Then a ResetSynchronizer is used to generate the reset of the sync domain, in which we find a flip-flop that keeps toggling.

The generated Verilog code is:

/* Generated by Yosys 0.21+18 (git sha1 0ab726e20, clang 10.0.0-4ubuntu1 -fPIC -Os) */

(* \amaranth.hierarchy  = "top.sync_rst" *)
(* generator = "Amaranth" *)
module sync_rst(rst, clk, rst_in_q);
  reg \$auto$verilog_backend.cc:2083:dump_module$1  = 0;
  (* src = "/usr/local/lib/python3.10/dist-packages/amaranth/vendor/xilinx.py:1034" *)
  wire async_ff_clk;
  (* src = "/usr/local/lib/python3.10/dist-packages/amaranth/vendor/xilinx.py:1034" *)
  wire async_ff_rst;
  (* src = "/usr/local/lib/python3.10/dist-packages/amaranth/hdl/ir.py:527" *)
  input clk;
  wire clk;
  (* src = "/usr/local/lib/python3.10/dist-packages/amaranth/hdl/ir.py:527" *)
  output rst;
  wire rst;
  (* src = "/hdl/test_resetsynchronizer.py:18" *)
  input rst_in_q;
  wire rst_in_q;
  (* ASYNC_REG = "TRUE" *)
  (* \amaranth.vivado.false_path  = "TRUE" *)
  (* src = "/usr/local/lib/python3.10/dist-packages/amaranth/vendor/xilinx.py:1035" *)
  reg stage0 = 1'h1;
  (* src = "/usr/local/lib/python3.10/dist-packages/amaranth/vendor/xilinx.py:1035" *)
  reg \stage0$next ;
  (* ASYNC_REG = "TRUE" *)
  (* src = "/usr/local/lib/python3.10/dist-packages/amaranth/vendor/xilinx.py:1035" *)
  reg stage1 = 1'h1;
  (* src = "/usr/local/lib/python3.10/dist-packages/amaranth/vendor/xilinx.py:1035" *)
  reg \stage1$next ;
  always @(posedge async_ff_clk, posedge async_ff_rst)
    if (async_ff_rst) stage0 <= 1'h1;
    else stage0 <= \stage0$next ;
  always @(posedge async_ff_clk, posedge async_ff_rst)
    if (async_ff_rst) stage1 <= 1'h1;
    else stage1 <= \stage1$next ;
  always @* begin
    if (\$auto$verilog_backend.cc:2083:dump_module$1 ) begin end
    \stage0$next  = 1'h0;
    (* src = "/usr/local/lib/python3.10/dist-packages/amaranth/hdl/xfrm.py:519" *)
    casez (async_ff_rst)
      1'h1:
          \stage0$next  = 1'h1;
    endcase
  end
  always @* begin
    if (\$auto$verilog_backend.cc:2083:dump_module$1 ) begin end
    \stage1$next  = stage0;
    (* src = "/usr/local/lib/python3.10/dist-packages/amaranth/hdl/xfrm.py:519" *)
    casez (async_ff_rst)
      1'h1:
          \stage1$next  = 1'h1;
    endcase
  end
  assign rst = stage1;
  assign async_ff_clk = clk;
  assign async_ff_rst = rst_in_q;
endmodule

(* \amaranth.hierarchy  = "top" *)
(* top =  1  *)
(* generator = "Amaranth" *)
module top(toggle, rstdomain_clk, rstdomain_rst, clk, rst, rst_in);
  reg \$auto$verilog_backend.cc:2083:dump_module$2  = 0;
  (* src = "/hdl/test_resetsynchronizer.py:21" *)
  wire \$1 ;
  (* src = "/usr/local/lib/python3.10/dist-packages/amaranth/hdl/ir.py:527" *)
  input clk;
  wire clk;
  (* src = "/usr/local/lib/python3.10/dist-packages/amaranth/hdl/ir.py:527" *)
  output rst;
  wire rst;
  (* src = "/hdl/test_resetsynchronizer.py:11" *)
  input rst_in;
  wire rst_in;
  (* src = "/hdl/test_resetsynchronizer.py:13" *)
  input rstdomain_clk;
  wire rstdomain_clk;
  (* src = "/hdl/test_resetsynchronizer.py:13" *)
  input rstdomain_rst;
  wire rstdomain_rst;
  (* src = "/hdl/test_resetsynchronizer.py:18" *)
  reg sync_rst_rst_in_q = 1'h1;
  (* src = "/hdl/test_resetsynchronizer.py:18" *)
  reg \sync_rst_rst_in_q$next ;
  (* src = "/hdl/test_resetsynchronizer.py:12" *)
  output toggle;
  reg toggle = 1'h0;
  (* src = "/hdl/test_resetsynchronizer.py:12" *)
  reg \toggle$next ;
  assign \$1  = ~ (* src = "/hdl/test_resetsynchronizer.py:21" *) toggle;
  always @(posedge rstdomain_clk)
    sync_rst_rst_in_q <= \sync_rst_rst_in_q$next ;
  always @(posedge clk)
    toggle <= \toggle$next ;
  sync_rst sync_rst (
    .clk(clk),
    .rst(rst),
    .rst_in_q(sync_rst_rst_in_q)
  );
  always @* begin
    if (\$auto$verilog_backend.cc:2083:dump_module$2 ) begin end
    \sync_rst_rst_in_q$next  = rst_in;
    (* src = "/usr/local/lib/python3.10/dist-packages/amaranth/hdl/xfrm.py:519" *)
    casez (rstdomain_rst)
      1'h1:
          \sync_rst_rst_in_q$next  = 1'h1;
    endcase
  end
  always @* begin
    if (\$auto$verilog_backend.cc:2083:dump_module$2 ) begin end
    \toggle$next  = \$1 ;
    (* src = "/usr/local/lib/python3.10/dist-packages/amaranth/hdl/xfrm.py:519" *)
    casez (rst)
      1'h1:
          \toggle$next  = 1'h0;
    endcase
  end
endmodule

I'm using the following XDC to perform out-of-context implementation of this Verilog in Vivado:

create_clock -period 5 -name clk [get_ports clk]
create_clock -period 5.01 -name rstdomain_clk [get_ports rstdomain_clk]
set_false_path -to [get_cells -hier -filter {amaranth.vivado.false_path == "TRUE"}]

Here is the schematic of the Vivado implementation:

Vivado is doing timing analysis of the path from sync_rst_rst_in_q_reg/C to syn_rst/stage1_reg/D, which is an inter-clock path from rstdomain_clk to clk, and thus failing timing, because I've purposely set the clock periods of clk and rstdomain_clk so that their greatest common divisor is very small.

I think that Vivado should not analyze any inter-clock paths for this example (that's the whole point of the synchronizer). It seems that the problem is that the schamatic is not really what we intended. Rather than directly connecting stage0_reg/Q to stage1_reg/D, we are getting a LUT stage1_i_1 in the middle which has sync_rst_rst_in_q. This is what causes Vivado to analyze this inter-clock path (flop stage0_reg has a false-path constraint, but stage1_reg doesn't have a false-path constraint).

I think that we wouldn't like the LUT stage1_i_1 to be there. The schematic would work well with sync_rst_rst_in_q only going to the PRE inputs of stage0_reg and stage1_reg.

It seems that Vivado is getting confused by this part of the Verilog:

  always @* begin
    if (\$auto$verilog_backend.cc:2083:dump_module$1 ) begin end
    \stage1$next  = stage0;
    (* src = "/usr/local/lib/python3.10/dist-packages/amaranth/hdl/xfrm.py:519" *)
    casez (async_ff_rst)
      1'h1:
          \stage1$next  = 1'h1;
    endcase
  end

Having \stage1$next depend on async_ff_rst is somewhat redundant, because we already model the asynchronous reset in this other block:

always @(posedge async_ff_clk, posedge async_ff_rst)
    if (async_ff_rst) stage1 <= 1'h1;
    else stage1 <= \stage1$next ;

In fact, if I replace the always @* block by only

 always @* begin
    if (\$auto$verilog_backend.cc:2083:dump_module$1 ) begin end
    \stage1$next  = stage0;
  end

I get the following schematic, which looks more sensible: However, this still gives timing failures, because Vivado is analyzing the path from sync_rst_rst_in_q_reg/C to sync_rst/stage1_reg/PRE. In this analysis, it is considering the Recov_fdpe_C_PRE for stage1_reg. I'm not sure if it is necessary to consider this recovery time for PRE, or if we can ignore it completely, so that stage1_reg/PRE should also have a false-path constraint to avoid analyzing this path.