"""IceBreaker (iCE40 UP5K) vendor-backed async FIFO example.

This module uses Amaranth's `Memory` with separate write/read ports in different
clock domains. With the icestorm toolchain the memory typically maps to
`SB_RAM40_4K` block RAMs. The control (full/empty) is implemented with
gray-pointer logic and two-stage synchronization of opposing pointers.

Notes:
- This prefers block RAM for storage (small LUT usage, lower power).
- The write/read ports are in independent domains; backend maps ports to
  dual-port RAM primitives when available.
"""

from amaranth import *


class Ice40AsyncFIFO(Elaboratable):
    def __init__(self, depth=256, wdomain="src", rdomain="dst"):
        assert depth & (depth - 1) == 0, "depth must be power of two"
        self.depth = depth
        self.aw = (depth - 1).bit_length()
        self.wdomain = wdomain
        self.rdomain = rdomain

        # serial (1-bit) interface
        self.wdata = Signal()
        self.w_en = Signal()
        self.w_full = Signal()

        self.rdata = Signal()
        self.r_en = Signal()
        self.r_valid = Signal()
        self.r_empty = Signal()

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

        # single-bit-wide memory mapped to vendor BRAMs by the backend
        mem = Memory(width=1, depth=self.depth)
        wp = mem.write_port(domain=self.wdomain)
        rp = mem.read_port(domain=self.rdomain, transparent=False)
        m.submodules += wp, rp

        # pointers (aw+1 bits to include wrap bit)
        wbin = Signal(self.aw + 1)
        wgray = Signal(self.aw + 1)
        rbin = Signal(self.aw + 1)
        rgray = Signal(self.aw + 1)

        # sync registers for opposing pointers (two-stage)
        rgray_sync0 = Signal(self.aw + 1)
        rgray_sync1 = Signal(self.aw + 1)
        wgray_sync0 = Signal(self.aw + 1)
        wgray_sync1 = Signal(self.aw + 1)

        # write-side
        with m.Domain(self.wdomain):
            next_wbin = Signal(self.aw + 1)
            next_wgray = Signal(self.aw + 1)
            m.d.comb += next_wbin.eq(wbin + self.w_en)
            m.d.comb += next_wgray.eq(next_wbin ^ (next_wbin >> 1))

            # sync read pointer into write domain
            for i in range(self.aw + 1):
                m.d[self.wdomain] += rgray_sync0[i].eq(rgray[i])
                m.d[self.wdomain] += rgray_sync1[i].eq(rgray_sync0[i])

            # full detection (standard gray-pointer trick)
            top = self.aw
            low_eq = Signal()
            msb_cmp = Signal()
            m.d.comb += low_eq.eq(next_wgray[top - 1:0] == rgray_sync1[top - 1:0])
            m.d.comb += msb_cmp.eq((next_wgray[top] != rgray_sync1[top]) & (next_wgray[top - 1] != rgray_sync1[top - 1]))
            m.d.comb += self.w_full.eq(low_eq & msb_cmp)

            # perform write
            with m.If(self.w_en & ~self.w_full):
                m.d[self.wdomain] += wp.addr.eq(wbin[self.aw - 1:0])
                m.d[self.wdomain] += wp.data.eq(self.wdata)
                m.d[self.wdomain] += wp.en.eq(1)
                m.d[self.wdomain] += wbin.eq(next_wbin)
                m.d[self.wdomain] += wgray.eq(next_wgray)
            with m.Else():
                m.d[self.wdomain] += wp.en.eq(0)

        # read-side
        with m.Domain(self.rdomain):
            next_rbin = Signal(self.aw + 1)
            next_rgray = Signal(self.aw + 1)
            m.d.comb += next_rbin.eq(rbin + self.r_en)
            m.d.comb += next_rgray.eq(next_rbin ^ (next_rbin >> 1))

            # sync write pointer into read domain
            for i in range(self.aw + 1):
                m.d[self.rdomain] += wgray_sync0[i].eq(wgray[i])
                m.d[self.rdomain] += wgray_sync1[i].eq(wgray_sync0[i])

            m.d.comb += self.r_empty.eq(rgray == wgray_sync1)

            with m.If(self.r_en & ~self.r_empty):
                m.d[self.rdomain] += rp.addr.eq(rbin[self.aw - 1:0])
                m.d[self.rdomain] += rp.en.eq(1)
                m.d[self.rdomain] += rbin.eq(next_rbin)
                m.d[self.rdomain] += rgray.eq(next_rgray)
                m.d[self.rdomain] += self.r_valid.eq(1)
                m.d[self.rdomain] += self.rdata.eq(rp.data)
            with m.Else():
                m.d[self.rdomain] += rp.en.eq(0)
                m.d[self.rdomain] += self.r_valid.eq(0)

        return m


if __name__ == "__main__":
    # Quick smoke-check: instantiate and print fragment
    from amaranth.back import verilog

    fifo = Ice40AsyncFIFO(depth=256)
    print(verilog.convert(fifo, ports=[fifo.wdata, fifo.w_en, fifo.w_full, fifo.rdata, fifo.r_en, fifo.r_valid, fifo.r_empty]))