SYNTHESIS

Turn RTL Intent into a Checkable Netlist

Build one traceable contract from RTL through SDC, synthesis, and equivalence. Open-source results teach the loop; a production release still needs the project’s qualified libraries, modes, corners, and approved formal setup.

Inputs

Elaborated RTL, top module, and reset/clock intent
Liberty timing/power views and technology mapping rules
Versioned SDC plus mode/corner assumptions

Method

Lint and elaborate the exact release RTL; record parameters, black boxes, and generated clocks before optimization.
Author SDC from interface intent: clocks, generated clocks, I/O delays, uncertainty, and only reviewed timing exceptions.
Run synthesis and inspect area, unmapped logic, inferred latches, and unconstrained paths; fix causes in RTL or constraints rather than masking reports.
Compare RTL and mapped netlist with reset/X and black-box assumptions explicitly matched; classify every unproven point.
Freeze named input versions and publish a constraint-coverage review with waiver owners and expiry dates.

Deliverables

Mapped netlist and synthesis QoR report
Reviewed SDC and constraint-coverage report
LEC result, assumptions, and bounded waiver log

Pitfalls

A clean timing report can omit unconstrained paths; inspect them explicitly.
An open-source formal pass is not a substitute for the qualified library and formal signoff methodology required by a foundry/customer flow.

Sources

Debugging timing ↗
OpenSTA · Constrained and unconstrained timing reports

equiv_make — prepare a circuit for equivalence checking ↗
YosysHQ · Equivalence-check construction

OpenLane Architecture ↗
OpenLane · Open-source RTL-to-GDS stages and checks