Skip to main content

Formal methods for EDA

Formal Technologies and Solutions

Overview

We apply formal methods in two different EDA domains: Power consumption and synthesis. We do this in two projects:

  • GateAlert
  • SatSyn

GateAlert
Power consumption has become a major factor in modern chip design. An efficient and widely used technique for reducing power consumption is clock gating, which is aimed at reducing dynamic power by eliminating unnecessary latch-clocking events. GateAlert is a power reduction tool that harnesses the strength of formal methods to automatically extract clock gating conditions. The tool consists of a set of clock gating analysis algorithms that can find clock gating opportunities given a gate-level representation of a design. Since GateAlert performs a formal analysis of the logic, it is able to extract clock gating conditions regardless of the language or coding style being used.

GateAlert can read RTL specifications, enabling analysis at an early design stage and eliminating the need to go through the entire synthesis process. GateAlert provides the means for controlling the logic depth of the circuitry required for implementing the clock gating functions and constraining the LCB-to-latch ratio. These come in the form of algorithms for clustering and approximating clock gating functions.

When run as a stand-alone tool, GateAlert outputs a human-readable advice file containing suggestions for clock gating. In addition, it provides partial support for generating modified VIM if run as part of the synthesis environment.

We are also exploring new related directions, such as data gating. Data gating is a low-power technique used for reducing switching activity of combinational logic or sequential elements. The basic idea is to prevent unnecessary signal propagation in parts of the design when they are not being used. Currently, due to its pervasive and behavior-dependent nature, data gating is hardly applied by designers.

SatSyn
Logic optimization is a fundamental step in the logic synthesis process. As synthesis tools are facing increasingly large design blocks, it has become evident that robust logic optimization techniques, which can unlock the full reduction potential of such blocks, need to be developed. The goal of the SatSyn project is to increase the size of designs that can be processed efficiently in logic synthesis tools by employing Sat solving technology in the optimization phase.

SAT solvers are usually superior to other symbolic methods (e.g., BDDs) in terms of handling large Boolean expressions. As many of the logic optimization techniques, for example redundant logic elimination, can be formulated as satisfiability problems, SAT solvers are a natural choice for enabling logic optimization in large designs. SatSyn incorporates logic optimization techniques based on the Mage SAT solver, a robust SAT solver originally developed by the Haifa team for the RuleBase PE formal verification platform.

SatSyn is being developed in collaboration with the Logic and Physical Synthesis group in the IBM Watson Research Center, who are responsible for the PDS synthesis tool.