Synopsys Presents SAT-Sweeping Enhancements for Logic Synthesis

There was a “research reviewed” panel on Thursday at DAC entitled Shortening the Wires Between High-Level Synthesis and Logic Synthesis. Chaired by Alric Althoff of Tortuga Logic, the panel explored methods to deal with wire delays in high-level synthesis and logic synthesis. The four speakers and their focus were:

• Licheng Guo, PhD student at UCLA: synthesized circuits with HLS lead to frequency degradation due to long signal broadcasts – a set of easy to implement approaches to address this is discussed
• Po-Chun Chien, Research Assistant at National Taiwan University: a method to multiplex pins in FPGAs through structural and functional circuit folding
• Luca Amaru, Senior R&D Manage at Synopsys: a SAT-sweeper method for simplifying logic networks
• He-Teng Zhang, Researcher at National Taiwan University: a scalable approach to fanout-bounded logic synthesis

Luca Amaru, a senior R&D manager at Synopsys presented a very interesting approach to logic synthesis optimization that I’d like to cover in this post. Before getting that, there was a poll question for this event – Does your organization use high level synthesis (HLS) today? Below are the results of the poll. It appears HLS is catching on.

Luca began by explaining that the work he was presenting is a collaboration between Synopsys, EPFL in Lausanne, Switzerland and UC Berkeley. First, a bit of background on the core concept of the presentation – SAT, or Boolean Satisfiability. This technique has application in formal verification and logic synthesis. The task at hand is to prove that two gates in a circuit are functionally equivalent. This means that there is no input pattern such that the two assume different values. The results of proofs like this can drive optimization approaches.

As proving functional equivalence is very complex, run times can explode in an exponential manner. Methods to manage this problem and why equivalence is important for logic synthesis were the focus of Luca’s presentation. The options available to solve a problem like this were enumerated by Luca as follows:

• Exhaustive simulation
• Partial simulation with binary decision diagram (BDD) construction
• Structural hashing of and-inverter graphs (AIG)
• Partial simulation with SAT solving, or SAT sweeping

Luca explained that the first three methods have limitations, either because of extreme run times, lack of scalability or inability to look at all aspects of the problem. The last approach, called SAT sweeping was chosen because of its scalability and completeness. It turns out that using this technique for logic synthesis has some additional benefits. These circuits are not as deep as those seen in general formal applications and there aren’t as many equivalencies to prove, allowing for optimization of run times.

Luca then got into some details of the “sweeping” aspect of the approach. An initial random simulation can be run to disprove the “easy” candidates. This still leaves you with a lot of gate pairs. Calling a SAT solver for each will still result in very long run times. Further optimization can be done by grouping gates in equivalence classes that have the same simulation pattern. The next decision is how to process the network, top-down or bottom-up. It turns out the top-down approach works better for logic synthesis. Prior simulation patterns and heuristics can be added to optimize the process even further. All of this leads to the idea of a SAT preprocessing engine.  Characteristics of this approach were summarized in the list, below.

Luca concluded with benchmark results on 11 varying size design examples. A speed-up of 1.5X and even an order of magnitude is possible with this approach. This allows for much better synthesis results post P&R thanks to more effective use of the run-time budget.

The information reviewed by all presenters in this session is relevant and useful. If you have a DAC pass, I recommend you check out this session. I believe the DAC sessions will be available for an extended period of time. You can find this session on Shortening the Wires Between High-Level Synthesis and Logic Synthesis here.

Also Read:

DAC Panel – Artificial Intelligence Comes to CAD: Where’s the Data?

Hierarchical CDC analysis is possible, with the right tools

What’s New in Verdi? Faster Debug