One of the most challenging stages in an SoC design is achieving timing closure. Actually design closure is perhaps a better term since everything needs to come together such as clock tree, power nets, power budget and so on. Changes made to the design are known as ECOs (which stands for engineering change orders, a term that comes from the days when circuit boards would have colored wires added to address problems, try that on a 20nm chip). Some ECOs are minor timing changes but some are more significant and require RTL changes. This stage of the design cycle can take weeks, with multiple ECO cycles each of which requires many engineers for a few week.
The challenge with ECOs is two fold. First is to avoid the whack-a-mole problem whereby each change fixes one problem and creates two new ones in areas that were previously clean. This problem means that ECOs have to be handled incrementally and intelligently. The second problem is keeping all the views of the design in synchrony.
Keeping the views in synchrony is more difficult than it seems since the RTL may need to be altered to reflect the change. This is called a functional ECO, perhaps coming about due to a spec change or perhaps due to a late discovered issue in verification. But the entire design cannot be re-synthesized, re-placed and re-routed or the timing will never close. But ensuring that just those nets that need to be reworked are the ones that do get reworked is a challenge. Guaranteeing that this is done correctly requires the changes to be verified formally, but to completely re-verify a large design takes a lot of time and compute power.
Today Synopsys announced Formality Ultra which is aimed at precisely this problem and reduces the time taken to handle functional ECOs by a factor of two. It uses formal techniques to analyze mismatches between the (new) RTL and the (old) netlist of the design and so allows the designer to zoom into which changes are needed to implement the ECO. In addition, a new multi-point verification technology quickly checks multiple changes made to the design and so lets designers verify the correctness of their ECOs in a matter of minutes even on multi-million instance designs.
By working incrementally, the whole process is much faster than doing a full verification of the whole design from scratch. Then, to actually make the changes, Formality Ultra generates scripts for IC Compiler to use the incremental P&R capabilities there.
Synopsys have made two videos on Formality Ultra: