Sequential Equivalency Checks in HLS

Higher level synthesis (HLS) of an IP block involves taking its high-level design specification –usually captured in SystemC or C++, synthesizes and generates its RTL equivalent. HLS provides a faster convergence path to design code stability, promotes design reuse and lowers front-end design inception cost.

HLS and Mentor Catapult Platform
The current rise in the HLS adoption has been partly attributed to the availability of verification solutions, which facilitate the validation of the generated RTL codes against the high-level reference design. Both design abstractions can be validated through either simulation based verification (such as coverage metric and assertion driven), or formal verification method to check for their equivalencies.

Mentor’s Catapult® HLS Platform provides a complete C++/SystemC verification solution that interfaces with Questa® (or third party simulators) for RTL verification as shown in figure 1. The platform consists of a design checker (Catapult DesignChecks or CDesign Checker), a coverage tool (Catapult Code Coverage or CCOV), a high-level synthesis (Catapult HLS) and a formal tool SLEC HLS (Sequential Logic Equivalence Check).

Logic and Sequential Transformations
During RTL-GDS2 design implementation, timing optimization frequently necessitates logic restructuring and transformation to meet PPA (Power Performance Area) tradeoffs. While critical timing paths can be resolved through the manipulation of logic cone topology –such as buffering, drive strength adjustments, better resource sharing, and an interconnect layer promotion, sequential related design manipulation can provide opportunities for solving critical timing paths that otherwise impossible to tackle. Such design transformation is hardly available in the later stage of gate level timing optimization as it may introduce state changes and complicates the verification tasks.

Several timing driven sequential modifications include pipelining (managing number of stages along data or control paths to meet throughput target); register retiming (shifting register to balance logic cone latency); state recoding in FSM block (such as from binary-encoded to one-hot implementation); and resource scheduling (what-if scenarios to meet optimal area and performance targets).

Furthermore, a number of design refinements might also introduce changes in sequential element count such as a block interface conversion from abstract data types to bit-accurate busses and augmenting test mode operation involving scan path logic insertion.

Designer also run Catapult HLS to generate power optimized verification ready RTL, which involves sequential transformations due to enable manipulation technique (enable extraction or strengthening) –yielding further clock gating that reduces switching activities. Figure 2 shows the additional clock gatings due to sequential analysis.

All of the previously described design changes alter the maps between registers of the two design abstractions, and render traditional combinational equivalence checkers ineffective. Instead, designers could run SLEC HLS to validate between C++/System C to RTL as well as RTL versus RTL (before and after an incremental power optimization).

The Mechanics of SLEC HLS
Unlike the traditional equivalence checker for combinational logic, proving equivalency across two design abstraction such as C++ versus RTL requires a different approach such as identifying the sequential differences. SLEC HLS has advanced analysis that allows designers to explore what-if refinements that normally might trigger traditional equivalence checkers to generate a false positive. It employs a fine-grain partitioning of design sections in order to provide scalability in handling large design codes.

As illustrated in figure 3, fracturing a function to its associated basic blocks, SLEC HLS analyzes and map them to its corresponding control FSM to schedule the dataflow analysis. Comparison is then performed at the interface of these “state-like” basic blocks along the time axis using micro transactions. HLS synthesis provides both basic block boundaries and information about the micro transactions.

Running and Analyzing SLEC HLS Results
SLEC HLS run setup is quite straight-forward and is achieved by black-boxing non-synthesizable design parts including large memory blocks, and specifying the same reset states and sequences usually captured for synthesis. Other design setting such as state correspondence, which reduces verification complexity as well as clocking and port mapping are automatically derived from the high-level reference codes. To improve run time and quality of results, the tool uses function-based partitioned blocks in the form called CCOREs (Catapult C Optimized Reusable Entities) –which are called for multiple times in the design, to perform a hierarchical verification.

At SLEC HLS run completion, there are 3 possible outcomes: a full proof of equivalency, a mismatch, or a partial proof –which indicates that some remaining points in logic being compared needed further analysis. A neat feature of SLEC HLS is when a mismatch occurs. In this instance, it will generate counter example testbenches containing stimulus sequences that designers use to trace design differences. These testbenches include flip-flop initialization values and all primary input stimuli intended to demonstrate the difference –which are simulation ready, and can be used for further analysis with functional verification tool. Subsequent fixes to mismatches may involve source code or I/O cycle/sampling adjustments, constraint changes and a rerun.

In the case of a partial proof, SLEC HLS will generate a formal coverage report that quantifies the exploration of all possible inputs and states, which is helpful to root-cause issues such as dead-code situation. Such information can also be used to identify incorrect assumptions or constraints that were provided to SLEC HLS such as conflicting dual assignments to an input. Hence, adding a formal verification in the flow reduces the need to do full-blown RTL simulation and cutting the overall verification time.

As part of the Catapult HLS Platform integrated verification solution, SLEC HLS provides designers with formal validation of designs across different abstractions (C++, SystemC, RTL) or refinement stages (pre- vs post-power optimization). Such vectorless validation can be used to complement simulations to deliver a more comprehensive verification and reducing the overall efforts and cost.

Check HERE for HLS and HERE for SLEC HLS.