The AbcIntf Object: ABC/Verific Interface



The Logic Tools Package.

June 4th 2009

Andy Fox, andy@

Tel 831 621 0999

Important Note

The utilities outlined in this document are intended for use with the Verific language processing product [2] (see ) and operate on the Verific data structures. To use these utilities you must first obtain a Verific license (Verific provide a binary evaluation) -- no Verific source or header file are included in the logic tools package. To obtain the package, e-mail andy@.

Revision History

|Version |Description |

|0.0 |AF : Initial |

|0.1 |AF: details logictools.exe binary |

1.0 Summary

Logic Tools is a package of small programs for synthesis, optimization and formal logic verification using Verific net-list data structures and for converting to/from the abc [1] package.

The intent of this package is to provide utilities which most integrators of the Verific language processing programs need in various synthesis and optimization flows.

Test programs showing how to access each utility are provided.

The package comprises:

|ABC interface |

|A Verific ABC interface. This allows the powerful abc package from UC Berkeley to be directly accessed from the Verific |

|package. This includes a full data structure level integration both Verific to abc and abc to Verific. |

|Formal verification and SAT-Simulation |

|A formal verification utility which runs natively on the Verific netlist data structures is provided. This uses the well known |

|SAT-Simulation approach. Because SAT-Simulation is a useful utility in its own right (for example for network sweeping, clock gate |

|extraction) an API is provided to the SAT-Simulation algorithms. |

|Network Utilities |

|network utilities which run on the Verific data structures which save a developer of Verific applications programming time. For |

|example a functor for a generic Dfs is provided along with utilities for traversing, trimming (removing unreachable elements), |

|finding strongly connected (loop) elements, and debugging Verific net lists (eg topologically sorted levelized printing). |

|Cut Utilities |

|Cuts are collections of nodes in a network which provide a useful subset for optimization. The cut utility package includes methods|

|for generating and manipulating cuts. |

|Synchronous Micro-pipeline generation |

|A synchronous micro-pipeline is a special form of synchronous logic network in which each gate is latched. The synchronous |

|micro-pipeline package provides a means for generating and analyzing such networks. |

|Clock Gate Extraction for Power Reduction |

|The clock gate extraction algorithm generates clock gates for the state elements in the design by detecting (using SAT-sim) when |

|the d/q values for the next cycle are identical. This uses the algorithm outlined in [5]. |

|Test implementations |

|A test command line driven application which allows each package to be demonstrated and exercised is provided in source form. The |

|resulting binary, logictools.exe, provides clock gating, formal verification, and abc command execution on the verific netlists. |

2.0 Modules In Source Distribution

|Directory/File |Description |

|abcintf/ |Abc interface (Interface to the powerful UC Berkeley logic synthesis engine). |

|abcintf/abcintf.h |Interface class (allows all abc commands to be executed) |

|abcintf/abcintf.cpp |Conversion routines (Verific -> ABC, ABC -> Verific) |

|abcintf/preprocess.cpp |Preprocessing for verific netlist |

|abcintf/readblif.cpp |Read blif using abc blif reader. |

|formalverify/ |Formal verification for Verific netlists. (formally compares two Verific netlists) |

|formalverify.cpp |Formal verification (cec) |

|formalverify.h | |

|dfscutclausegen.cpp |Cut clause generation for formal verification |

|dfscutclausegen.h | |

|satsim.cpp |Sat-simulation utilities |

|nwsim.cpp |Network simulation. |

| | |

|nwk/ |Network Utilities |

|nwkutil.h |Network utilities for verific netlists header file (Includes a generic dfs). |

|nwkutil.cpp | |

|dfsprint.cpp |Pretty print for debugging |

|dfstrim.h |Trim out unreachable logic. |

|scc.h |Strongly-connected components (for quickly finding elements in loops) |

|dfslevel.h |Functor for accumulating portref levels in netlist. |

|dfslevel.cpp | |

| | |

|util/ |Utilities |

|util/utilexception.h |Exception handler |

|util/verificutil.h |utility methods. For verific netlists. |

|util/errrep.h |Error reporting |

|util/util.h |Package wide defines |

|util/linescanner.h |Line scanner base class (lexical analysis, token extraction) |

|util/blifscanner.cpp |Native blif reader – generates Verific data structures directly from blif. (Blif is |

|util/blifscanner.h |a useful format for representing logic networks favored by academic tools). |

|cut/ |Cut representation and generation |

|cut.h |Cut representation |

|cut.cpp | |

|boundarycutgen.h |Generate boundary cuts (a special form of cut that extends between nominated |

|boundarycutgen.cpp |invariant points eg flops/pads/non-combinational elements). |

|cutsim.cpp |Cut simulation (used in sat simulation). |

| | |

|Cgate |clock gate extraction utilities |

|cgate.h |Generate clock gate extraction |

|cgate.cpp | |

|Supipe |Synchronous Micro-pipeline generation |

|supipe.cpp | |

|supipe.h | |

|supipelib.cpp | |

|examples/ |Examples |

|test_main.cpp |Test program for exercising all aspects of system |

|test_abcintf.cpp |Test the abc interface. |

|test_verify.cpp |Test the formal verifier. |

|test_satsim.cpp |Test the sat simulation interface. |

|test_cgate.cpp |Test the clock gating algorithms. |

|test_map.cpp |Test the mapper |

|doc/ |Documentation |

|doc/logictools.doc |Package documentation (this file) |

| | |

|Minisat |Public domain minisat package |

|Boost |Public domain boost package |

|Abc |Public domain abc package |

2.0 Formal Verification & SAT-Simulation

The formal verification system allows two Verific net lists to be formally compared for combinational equivalence. It works using a combination of SAT and simulation which are run on the native Verific net-list. References outlining the algorithms used are [3, 4, 5]. A general purpose SAT/simulation interface is provided.

2.1 Formal Verification Object and Usage

The API is through the FormalVerify Object which provides the facility for registering two netlists to be compared: the “specification” and the “implementation”, and a “Verify” method which performs the equivalency check. For example, the specification may be the net list prior to some optimization (such as logic remapping or rewriting or clock gating) and the implementation the resultant of the optimization. An example of invoking the verifier is:

Netlist* _nl; //a flattened verific netlist

FormalVerify fv; //formal verification object

//register the specification

fv.RegisterSpecification(_nl);

//

//do something to netlist _nl: eg mapping

//

MyTransform(_nl);

//register the implementation

fv.RegisterImplementation(_nl);

//formally verify, report the number of discrepancies to nominated

//stream

if (fv.Verify(std::cout)==0)

printf("Successfully verified design\n");

else

printf("Cannot verify design");

2.2 Formal Verification API

FormalVerify()

Create the formal verification object.

void RegisterSpecification(Netlist* nw1)

Register the specification netlist.

void RegisterImplementation(Netlist* nw1)

Register the implementation netlist.

int Verify(std::ostream& op_log);

Formally verify the equivalence of the specification and implementation. Return the number of discrepancies (which are reported to stream op_log).

2.3 SAT-Simulation API and Usage

The formal verifier works using a method called SAT-simulation. This involves simulating a Verific net-list and finding candidate equivalent points which are then proven (or otherwise) as being equivalent using SAT. Because SAT-simulation is a useful technique for various applications (eg clock gate extraction [5] and net list sweeping [6]) an interface to the sat simulation engine is provided. A key point to note is that the SAT-simulation is performed on the native Verific netlist, allowing the logical structure of the netlist (which comprises gates, possibly post placement and routing in some systems) to be preserved for analysis as opposed to using a technology independent view (eg AIG, BDD).

Equivalent pins are stored in a dictionary: EquivalentPinsDictionary which offers the following api:

2.3.1 EquivalentPinsObject api:

bool GetEquivalentPins(PortRef& p1, std::vector& equiv_pins);

Return vector of equivalent pins for p1. This set will include p1 itself and to be non-trivial must be of length > 1.

void Print();

Print out the equivalent pins.

The most useful sat-sim api methods are accessible from a formalverify object:

2.3.2 bool Verify(PortRef& p1, PortRef& p2)

Test if two points in logic netlist have same logic function. Invokes SAT-Simulation.

2.3.3 void MiterNetlists(Netlist& nw1,

Netlist& nw2,

Netlist& nw3,

std::set &miter_ops,

bool miter_op_only=false

)

Form the “miter” of two verific netlists. The outputs of the miters are stored in the miter_ops set. If miter_op_only is true, only insert miters at primary outputs, else insert miters on all invariant points (eg non-combinational elements, flops, memories etc).

2.3.4 void SimEquivCandidates(Netlist& nw, std::vector > &candidates);

Extract equivalent “candidate” logic points (from random simulation) in a logic netlist. These are ordered in topological order: the set of equivalent points at the lowest level in the netlist come first.

2.3.5 int FormalVerify::ProveCandidates(Netlist& nw_in,

std::vector &candidates,

EquivalentPinsDictionary& equiv_pins)

Test candidate equivalent logic points using SAT and accumulate proven equivalent points. Accumulate the equivalent pins in the dictionary “EquivPinsDictionary”. This is passed in as a parameter and is used to take advantage of pre-proven pin equivalencies which massively reduces the search complexity when proving pins equal.

3.0 ABC Interface

The abc interface is through object abcintf. This provides:

a) Data structure level integration between the ABC logic synthesis system [1] and the Verific HDL processing system [2] allowing the conversion of netlists from verific to abc.

b) An interface for safely applying the abc api commands and then converting the optimized netlist back to Verific.

3.1 Example of API Usage

The following example shows the basic facility.

#include “Database.h” /* Include the verific data base */

#include “abcintf.h” /* Include the abc interface header */

using namespace Verific;

using namespace Rushc;

Netlist* top; //Verific netlist (fully elaborated)

//assume top now populated by verific and “flattened”.

Netlist* new_top;

try {

//Constructs interface object and builds abc netlist

AbcIntf abc_interface1(*top);

//Execute an abc command (lut mapping)

if ((abc_interface1.ExecuteAbcCommand("if -K 4") == 0){

printf(“Successfully executed abc command\n”);

}

//back to Verific

new_top = abc_interface1.Abc2Verific();

}

catch (utilException except){

except.Print(std::cout);

}

It is possible to control the conversion by:

(a) Restricting the elements of the netlist which are translated by providing a “conversion set”. For example, you may only wish to apply abc to a subset of your design (eg critical logic cones etc).

(b) Controlling the conversion of state elements and full adders: (i) abc supports single clock basic DFF master/slave flops – the interface provides support for translating flip flops and for conditionally disabling their translation. (ii) Often it is desirable not to restructure full adder chains – the interface provides for conditionally disabling their translation.

3.2 API

3.2.1 Constructor: AbcIntf(const Netlist& verific_netlist_in,

bool dont_translate_flops_in=true,

bool dont_translate_fadd_in = true)

Construct the abc network from verific_netlist_in. Defaults to preserving flip flops and primitive adders. By assigning dont_translate_flops_in to false or don’t_translate_fadd_in to false, flip flops and primitive adders will be passed into abc.

Invoking the constructor generates the abc netlist. An ABC AIG is generated.

3.2.2 int ExecuteAbcCommand(char* cmd);

Invokes the abc command and return the status (0 for success).

3.2.3 Netlist* Abc2Verific();

Converts abc netlist back to Verific netlist.

3.2.4 Abc_Ntk* getAbcNetlist()

Get the abc netlist.

3.2.5 Netlist* getVerificNetlist()

Get the Verific netlist.

3.2.6 RegisterInstanceToConvert(Instance&)

Register an instance for conversion. If no instances are registered for conversion all primitive instances are converted to abc for subsequent optimization. (see prior comments about controlling flops and primitive adders). The application may restrict the logic for translation to abc by registering the instances for conversion – the intent is to provide a safe way for an application to restrict the region of the design for optimization.

3.3 Sample Application: Mapping and Verifying Using ABC

The following example shows the processing of a Verific netlist using the AbcIntf object using the abc lut mapper (if) and the abc verifier (cec).

//Use the flattened Verific netlist.

Netlist *top = Netlist::PresentDesign() ;

top -> Flatten();

try {

//construct the abc netlist from the Verific netlist.

AbcIntf abc_interface1(*top);

//write out the specification

abc_interface1.ExecuteAbcCommand("write_bench test1.bench");

//map the design

abc_interface1.ExecuteAbcCommand("if -K 4");

//convert it back to Verific

Netlist* mapped_netlist = abc_interface1.getVerificNetlist();

//Pass the mapped netlist into abc and verify it

//against the original.

AbcIntf abc_interface2(*mapped_netlist);

abc_interface2.ExecuteAbcCommand("write_bench test2.bench");

//Verify the mapped netlist

if (abc_interface2.ExecuteAbcCommand("cec test1.bench test2.bench")==0)

std::cout ................
................

In order to avoid copyright disputes, this page is only a partial summary.

Google Online Preview   Download