#!/usr/bin/env python3
"""Structural CDC / RDC / interface-path check on a Yosys JSON gate netlist.

usage: netlist_check.py MAPPED_JSON LIBERTY TOP OUT_JSON OUT_MD [--per-flop] [--owner-only]
                        [--top-file RTL_PATH] [--clock aclk] [--reset aresetn]
  --per-flop    list every flop (register name, cell type, clock root, reset root)
  --owner-only  group flops by source file only (no register names)

Checks (purely structural, on the flattened standard-cell netlist):
  * every sequential cell (from the liberty ff/latch groups) and the root of its
    clock pin, traced back through buffers/inverters to a top-level port;
    more than one clock root, or a clock pin driven by other logic, is a FAIL;
  * latches (any latch is reported; FAIL for this IP);
  * asynchronous clear/preset pins and their roots (must be the reset port,
    through buffers/inverters only; reset generated by other logic is a FAIL);
  * reset-domain crossings: flops without an asynchronous reset whose data cone
    contains an asynchronously reset flop (reported, integrator note);
  * the reset port used as data (combinational cone of a data pin);
  * combinational input-port -> output-port paths.
Exit status is 0 on PASS and 1 on FAIL.
"""
import hashlib
import json
import re
import sys
from collections import Counter, defaultdict

sys.setrecursionlimit(1_000_000)


def parse_liberty(path):
    """Return {cell: {'kind': 'ff'|'latch', 'clock': pin, 'clear': pin|None, 'preset': pin|None,
    'data': [pins]}} and {cell: {pin: direction}}."""
    text = open(path, encoding="utf-8", errors="replace").read()
    seq, dirs = {}, {}
    for m in re.finditer(r"\bcell\s*\(\s*\"?([A-Za-z0-9_]+)\"?\s*\)\s*\{", text):
        name, start = m.group(1), m.end()
        depth, i = 1, start
        while depth and i < len(text):
            if text[i] == "{":
                depth += 1
            elif text[i] == "}":
                depth -= 1
            i += 1
        body = text[start:i]
        pins = {}
        for pm in re.finditer(r"\bpin\s*\(\s*\"?([A-Za-z0-9_]+)\"?\s*\)\s*\{([^{}]*(?:\{[^{}]*\}[^{}]*)*)\}", body):
            dm = re.search(r"direction\s*:\s*\"?(\w+)\"?", pm.group(2))
            if dm:
                pins[pm.group(1)] = dm.group(1)
        dirs[name] = pins
        g = re.search(r"\b(ff|latch)\s*\([^)]*\)\s*\{([^}]*)\}", body)
        if g:
            attrs = dict(re.findall(r"(\w+)\s*:\s*\"([^\"]*)\"", g.group(2)))
            pin_of = lambda expr: re.sub(r"[!() ]", "", expr) if expr else None
            clk = attrs.get("clocked_on") or attrs.get("enable")
            seq[name] = {"kind": g.group(1), "clock": pin_of(clk),
                         "clear": pin_of(attrs.get("clear")), "preset": pin_of(attrs.get("preset"))}
    return seq, dirs


def main():
    args = [a for a in sys.argv[1:] if not a.startswith("--")]
    opts = sys.argv[1:]
    mapped, liberty, top, out_json, out_md = args[:5]
    clock_port = opts[opts.index("--clock") + 1] if "--clock" in opts else "aclk"
    reset_port = opts[opts.index("--reset") + 1] if "--reset" in opts else "aresetn"
    per_flop = "--per-flop" in opts
    owner_only = "--owner-only" in opts
    top_file = opts[opts.index("--top-file") + 1] if "--top-file" in opts else ""
    seq, libdirs = parse_liberty(liberty)
    raw = open(mapped, "rb").read()
    mod = json.loads(raw)["modules"][top]

    port_of_bit, out_bits = {}, []
    for pname, p in mod["ports"].items():
        for i, b in enumerate(p["bits"]):
            if p["direction"] == "input":
                port_of_bit[b] = pname
            else:
                out_bits.append((pname, i, b))
    names_of_bit = defaultdict(list)
    for nname, n in mod["netnames"].items():
        if n.get("hide_name", 0):
            continue
        for i, b in enumerate(n["bits"]):
            if isinstance(b, int):
                names_of_bit[b].append(nname.lstrip("\\") if len(n["bits"]) == 1 else f"{nname.lstrip(chr(92))}[{i}]")
    name_of_bit = {b: max(v, key=lambda x: (x.count("."), -len(x))) for b, v in names_of_bit.items()}

    def flop_name(q_bits, owner_is_top):
        """Top-level flops: their top-level net name; submodule flops: deepest hierarchical name."""
        for b in q_bits:
            cand = names_of_bit.get(b)
            if cand:
                if owner_is_top:
                    flat = [x for x in cand if "." not in x]
                    if flat:
                        return min(flat, key=len)
                return max(cand, key=lambda x: (x.count("."), -len(x)))
        return ""

    driver = {}
    cells = mod["cells"]
    for cname, c in cells.items():
        pdirs = c.get("port_directions") or libdirs.get(c["type"], {})
        for pin, bits in c["connections"].items():
            if pdirs.get(pin) == "output":
                for b in bits:
                    if isinstance(b, int):
                        driver[b] = (cname, pin)

    def cell_inputs(cname):
        c = cells[cname]
        pdirs = c.get("port_directions") or libdirs.get(c["type"], {})
        return [b for pin, bits in c["connections"].items() if pdirs.get(pin) == "input" for b in bits]

    def is_buf_inv(cname):
        t = cells[cname]["type"]
        return t.startswith("BUF_") or t.startswith("INV_") or t.startswith("CLKBUF_")

    def trace_root(bit):
        """Follow a net through buffers/inverters to a port, constant, or other logic."""
        hops = []
        while True:
            if not isinstance(bit, int):
                return ("const", str(bit)), hops
            if bit in port_of_bit:
                return ("port", port_of_bit[bit]), hops
            d = driver.get(bit)
            if d is None:
                return ("undriven", name_of_bit.get(bit, str(bit))), hops
            cname, _ = d
            if cells[cname]["type"] in seq:
                return ("flop", cname), hops
            if is_buf_inv(cname):
                hops.append(cells[cname]["type"])
                bit = cell_inputs(cname)[0]
                continue
            return ("logic", cells[cname]["type"] + ":" + cname), hops

    memo = {}

    def cone(bit):
        """Combinational fan-in of a net: (input ports, has async-reset flop source)."""
        if not isinstance(bit, int):
            return (frozenset(), False)
        if bit in memo:
            return memo[bit]
        memo[bit] = (frozenset(), False)        # cycle guard
        if bit in port_of_bit:
            res = (frozenset([port_of_bit[bit]]), False)
        else:
            d = driver.get(bit)
            if d is None:
                res = (frozenset(), False)
            elif cells[d[0]]["type"] in seq:
                res = (frozenset(), d[0] in async_reset_flops)
            else:
                ports, rs = set(), False
                for ib in cell_inputs(d[0]):
                    p, r = cone(ib)
                    ports |= p
                    rs = rs or r
                res = (frozenset(ports), rs)
        memo[bit] = res
        return res

    flops, async_reset_flops = [], set()
    for cname, c in cells.items():
        info = seq.get(c["type"])
        if not info:
            continue
        conn = c["connections"]
        clk_root, clk_hops = trace_root(conn[info["clock"]][0])
        rst = []
        for role in ("clear", "preset"):
            pin = info[role]
            if pin and pin in conn:
                root, hops = trace_root(conn[pin][0])
                if root[0] != "const":
                    rst.append((role, pin, root, hops))
        if rst:
            async_reset_flops.add(cname)
        q_bits = [b for pin, bits in conn.items()
                  if (c.get("port_directions") or libdirs.get(c["type"], {})).get(pin) == "output" for b in bits]
        src = c.get("attributes", {}).get("src", "")
        owner = src.split(":")[0] if src else ""
        qname = flop_name(q_bits, owner == top_file)
        if not owner:
            owner = "(no source attribute: memory-mapped flops)"
        pdirs = c.get("port_directions") or libdirs.get(c["type"], {})
        ctrl_pins = {info["clock"], info["clear"], info["preset"]}
        data_bits = [b for p, bits in conn.items()
                     if pdirs.get(p) == "input" and p not in ctrl_pins for b in bits]
        flops.append({"cell": cname, "type": c["type"], "kind": info["kind"],
                      "clock_root": clk_root, "clock_hops": clk_hops, "resets": rst,
                      "data_bits": data_bits, "q": qname, "owner": owner})

    checks, fail = [], False
    clock_roots = Counter(f"{r[0]}:{r[1]}" for r in (f["clock_root"] for f in flops))
    latches = [f for f in flops if f["kind"] == "latch"]
    derived = [f for f in flops if f["clock_root"][0] != "port"]
    ok_clock = (len(clock_roots) == 1 and f"port:{clock_port}" in clock_roots and not derived)
    checks.append({"check": "single clock domain", "pass": ok_clock,
                   "detail": dict(clock_roots)})
    clock_hops = Counter(tuple(f["clock_hops"]) for f in flops)
    checks.append({"check": "clock pins driven by the clock port directly or through buffers only",
                   "pass": not derived, "detail": {" -> ".join(k) or "direct": v for k, v in clock_hops.items()}})
    checks.append({"check": "no latches", "pass": not latches, "detail": len(latches)})
    reset_roots = Counter()
    bad_reset = []
    for f in flops:
        for role, pin, root, hops in f["resets"]:
            reset_roots[f"{role}:{root[0]}:{root[1]}"] += 1
            if root != ("port", reset_port):
                bad_reset.append(f["cell"])
    checks.append({"check": f"asynchronous clear/preset only from port {reset_port} (buffers/inverters only)",
                   "pass": not bad_reset, "detail": dict(reset_roots)})
    fail = not all(c["pass"] for c in checks)

    nonreset = [f for f in flops if not f["resets"]]
    rdc = []
    reset_as_data = []
    for f in flops:
        ports, rsrc = set(), False
        for b in f["data_bits"]:
            p, r = cone(b)
            ports |= p
            rsrc = rsrc or r
        if reset_port in ports:
            reset_as_data.append(f)
        if not f["resets"] and rsrc:
            rdc.append(f)

    comb = {}
    for pname, i, b in out_bits:
        p, _ = cone(b)
        if p:
            comb.setdefault(pname, set()).update(p)
    comb = {k: sorted(v) for k, v in sorted(comb.items())}

    def group(f):
        if owner_only:
            return f["owner"]
        return f"{f['owner']} :: {re.split(r'[\[]', f['q'])[0] or '(unnamed)'}"

    hier = defaultdict(lambda: {"flops": 0, "async_reset": 0, "no_reset": 0})
    by_owner = defaultdict(lambda: {"flops": 0, "async_reset": 0, "no_reset": 0})
    for f in flops:
        for g in (hier[group(f)], by_owner[f["owner"]]):
            g["flops"] += 1
            g["async_reset" if f["resets"] else "no_reset"] += 1

    report = {
        "design": top,
        "netlist_json_sha256": hashlib.sha256(raw).hexdigest(),
        "scope": "Structural check of the flattened pre-layout standard-cell netlist (Yosys JSON). "
                 "Not a formal CDC/RDC sign-off and not a timing analysis.",
        "result": "FAIL" if fail else "PASS",
        "sequential_cells": len(flops),
        "sequential_cell_types": dict(Counter(f["type"] for f in flops)),
        "latches": len(latches),
        "clock_roots": dict(clock_roots),
        "clock_domains": len(clock_roots),
        "flops_with_async_reset": len(async_reset_flops),
        "flops_without_reset": len(nonreset),
        "async_reset_roots": dict(reset_roots),
        "rdc_nonreset_flops_with_async_reset_flop_in_data_cone": len(rdc),
        "reset_port_in_data_cone_of_flops": len(reset_as_data),
        "combinational_input_to_output_paths": comb,
        "flops_by_source_file": dict(sorted(by_owner.items())),
        "flops_by_group": dict(sorted(hier.items())),
        "checks": checks,
        "integrator_requirements": [
            f"Drive every flop from the single clock {clock_port}; no internal clock generation or gating exists.",
            f"{reset_port} is asserted asynchronously and must be released synchronously to {clock_port} "
            "(two-flop reset synchronizer or equivalent in the integrating design).",
        ],
    }
    if rdc:
        report["integrator_requirements"].append(
            f"{len(rdc)} flops without reset (storage) are fed by asynchronously reset logic: contents written "
            "around reset assertion are not guaranteed; reload them after reset (consistent with the IP specification).")
    if reset_as_data:
        report["integrator_requirements"].append(
            f"{reset_port} also reaches the data input cone of {len(reset_as_data)} flops (reset used as a "
            "synchronous qualifier inside the IP); its release must therefore meet setup/hold like a data input.")
    if per_flop:
        report["flops"] = [{"q": f["q"], "source": f["owner"], "type": f["type"],
                            "clock": f["clock_root"][1],
                            "async_reset": ",".join(f"{r[0]}<-{r[2][1]}" for r in f["resets"]) or "none"}
                           for f in sorted(flops, key=lambda x: x["q"])]
    json.dump(report, open(out_json, "w"), indent=1)

    md = [f"# Structural CDC / RDC report: `{top}`", "",
          f"Result: **{report['result']}**. " + report["scope"], "",
          f"- Netlist JSON sha256: `{report['netlist_json_sha256']}`",
          f"- Sequential cells: {len(flops)} ({', '.join(f'{k} {v}' for k, v in report['sequential_cell_types'].items())}); latches: {len(latches)}",
          f"- Clock roots: {', '.join(f'{k} ({v} flops)' for k, v in clock_roots.items())} -> {len(clock_roots)} clock domain(s)",
          f"- Flops with asynchronous reset: {len(async_reset_flops)}; without reset: {len(nonreset)}",
          f"- Asynchronous reset roots: {', '.join(f'{k} ({v})' for k, v in reset_roots.items()) or 'none'}",
          f"- Flops without reset whose data cone contains an asynchronously reset flop: {len(rdc)}",
          f"- Flops whose data cone contains `{reset_port}`: {len(reset_as_data)}",
          "", "| Check | Result | Detail |", "|---|---|---|"]
    for c in checks:
        md.append(f"| {c['check']} | {'PASS' if c['pass'] else 'FAIL'} | `{json.dumps(c['detail'])}` |")
    md += ["", "## Combinational input-to-output paths", ""]
    if comb:
        md += ["| Output | Inputs in its combinational fan-in |", "|---|---|"]
        md += [f"| `{k}` | {', '.join(f'`{x}`' for x in v)} |" for k, v in comb.items()]
    else:
        md.append("None: every output is driven from flip-flops only.")
    md += ["", "## Flops by source file", "", "| Source file | Flops | Async reset | No reset |", "|---|---|---|---|"]
    md += [f"| `{k}` | {v['flops']} | {v['async_reset']} | {v['no_reset']} |" for k, v in report["flops_by_source_file"].items()]
    if owner_only:
        del report["flops_by_group"]
        json.dump(report, open(out_json, "w"), indent=1)
    md += ["", "## Flops by register", "", "| Source file :: register | Flops | Async reset | No reset |", "|---|---|---|---|"] if not owner_only else []
    if not owner_only:
        md += [f"| `{k}` | {v['flops']} | {v['async_reset']} | {v['no_reset']} |" for k, v in report["flops_by_group"].items()]
    md += ["", "## Integrator requirements", ""] + [f"- {r}" for r in report["integrator_requirements"]]
    open(out_md, "w").write("\n".join(md) + "\n")
    print(f"{top}: {report['result']} flops={len(flops)} clock_domains={len(clock_roots)} "
          f"async_reset={len(async_reset_flops)} no_reset={len(nonreset)} rdc={len(rdc)} "
          f"reset_as_data={len(reset_as_data)} comb_paths={sum(len(v) for v in comb.values())}")
    sys.exit(1 if fail else 0)


if __name__ == "__main__":
    main()