Function is fixed at handoff: the netlist must stay equivalent to the RTL it proved against. Equivalence is re-proven after every later patch.
Constraint intent is fixed too. Physical design may meet it differently, but it may not redefine what correct means.
Placement and routing replace estimates with reality, then reshape the netlist to fit it. Each change below is normal, and each must keep equivalence.
Change | Why it happens | What to watch |
|---|---|---|
Buffering and sizing | Real route lengths differ from estimates | Area and power drift from the synthesis reports |
Local restructuring | Congested spots need friendlier logic | Correlation gap on touched paths |
Clock tree build | Synthesis saw an ideal clock, not a tree | Skew appears where none was modelled |
Threshold swaps | Leakage and speed traded per path | Library views must cover every swap |
Synthesis timing and routed timing disagree by construction. Estimates, ideal clocks, and missing parasitics separate them.
The gap is tracked, not wished away. A path with 0.05 slack in synthesis and 0.4 extra route delay was never really closed.
The program below checks three handoff rules on an inline netlist: unique instance names, no unconnected pins, and no behavioural assign statements. It must clear the clean netlist and flag exactly three faults in the broken one.
import sys
GOOD = """
module top(input a, input b, input c, output y);
wire n1;
NAND2 g1 (.A(a), .B(b), .Y(n1));
NOR2 g2 (.A(n1), .B(c), .Y(y));
endmodule
"""
BAD = """
module top(input a, input b, input c, output y);
wire n1;
NAND2 g1 (.A(a), .B(b), .Y(n1));
NOR2 g1 (.A(n1), .B(), .Y(y));
assign y = n1;
endmodule
"""
def check_netlist(src):
issues = []
names = {}
for lineno, raw in enumerate(src.splitlines(), start=1):
line = raw.strip()
if not line:
continue
if line.startswith("module") or line.startswith("endmodule"):
continue
if line.startswith("input") or line.startswith("output") or line.startswith("wire"):
continue
if line.startswith("assign"):
issues.append("assign statement at line " + str(lineno))
continue
if "(" in line and line.endswith(";"):
head = line.split("(")[0].strip().split()
if len(head) >= 2:
inst = head[-1]
if inst in names:
issues.append("duplicate instance " + inst + " at line " + str(lineno))
else:
names[inst] = lineno
nospace = line.replace(" ", "")
if "()" in nospace:
issues.append("unconnected pin at line " + str(lineno))
return issues
good_issues = check_netlist(GOOD)
if len(good_issues) != 0:
print("FAIL: clean netlist raised " + str(len(good_issues)) + " issues")
sys.exit(1)
bad_issues = check_netlist(BAD)
if len(bad_issues) != 3:
print("FAIL: broken netlist raised " + str(len(bad_issues)) + " issues, want 3")
sys.exit(1)
joined = " ".join(bad_issues)
for kind in ["duplicate", "unconnected", "assign"]:
if kind not in joined:
print("FAIL: broken netlist missing a " + kind + " fault")
sys.exit(1)
print("PASS: checker clears the clean netlist and flags 3 faults")Yes: an equivalence re-proof. Any netlist edit, however helpful, needs the miter to agree again.
One duplicate instance name, one empty pin connection, and one assign statement. Each rule fires once.