The Logic Tools Package.
June 4th 2009
Andy Fox,
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 .
Revision History
Version / Description0.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 verificationusing 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 interfaceA 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 / Descriptionabcintf/ / 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
formalverify.h / Formal verification (cec)
dfscutclausegen.cpp
dfscutclausegen.h / Cut clause generation for formal verification
satsim.cpp / Sat-simulation utilities
nwsim.cpp / Network simulation.
nwk/ / Network Utilities
nwkutil.h
nwkutil.cpp / Network utilities for verific netlists header file (Includes a generic dfs).
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
dfslevel.cpp / Functor for accumulating portref levels in netlist.
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
util/blifscanner.h / Native blif reader – generates Verific data structures directly from blif.(Blif is a useful format for representing logic networks favored by academic tools).
cut/ / Cut representation and generation
cut.h
cut.cpp / Cut representation
boundarycutgen.h
boundarycutgen.cpp / Generate boundary cuts (a special form of cut that extends between nominated invariant points eg flops/pads/non-combinational elements).
cutsim.cpp / Cut simulation (used in sat simulation).
Cgate / clock gate extraction utilities
cgate.h
cgate.cpp / Generate clock gate extraction
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 netlists 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 netlist 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 netlist 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<PortRef*& 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.2bool Verify(PortRef& p1, PortRef& p2)
Test if two points in logic netlist have same logic function. Invokes SAT-Simulation.
2.3.3void MiterNetlists(Netlist& nw1,
Netlist& nw2,
Netlist& nw3,
std::set<PortRef*> &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.4void SimEquivCandidates(Netlist& nw, std::vector<std::pair< int, std::vector<PortRef*> > > &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.5int FormalVerify::ProveCandidates(Netlist& nw_in,
std::vector<std::pair<int,std::vector<PortRef*> > > &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 < "Success : verified the mapping" < std::endl;
else
std::cout < "Failure cannot compare 2 netlists" < std::endl;
}
catch (utilException except){
except.Print(std::cout);
}
The ABC package provides many exciting and interesting commands – such as retiming, logic rewriting (a form of technology independent optimization) as well as extensive support for formal verification (eg sequential bounded model checking and combinational logic equivalence checking). These commands are available through the ExecuteAbcCommand interface.
4.0 Synchronous Micro-pipeline Generation (SALT network generation)
A synchronous micro-pipeline is a circuit in which every gate output is latched. This class of circuit has some useful properties (for example, it maps directly to certain full custom dynamic layout design styles --such as precharge/evaluation logic methodology SALT -- and can be mapped directly to lut cascades for execution on specialized lut machines).
Consider the following circuit:
The synchronous micro-pipeline version is:
The original circuit had a maximum of 3 levels of logic between any input pad and flop. This means that the upper bound on the clock frequence is 1/((3*gate delay)+setup + hold time). The synchronous micropipelined circuit can be clocked much more quickly (1/(gate delay + setup + hold time) by a microcycle clock (uclock) and the output is made available every 3 uclock cycles. Autonomous counters are automatically inserted at the outputs to strobe the updated output.
4.1 API Usage
The interface to the synchronous micropipeline generator is object SuPipe.
Netlist* _nl; //a flattened verific netlist
SuPipe su_pipe(_nl); //initialize the synchronous
//micropipeline generator
Netlist* upipe_nl = su_pipe.CreateUSynchronizationNetlist();
The interface includes various useful methods for analyzing synchronous micro-pipelines.
4.2 API Calls
Netlist* CreateUSynchronizationNetlist();
Create a micro-pipeline for the netlist.
int getUcycleCount()
Get the maximum micro-cycle count – this is the number of micro-cycles clocks corresponding to the user clock tick.
void setUcycleCount(int val)
Set the maximum microcycle clock count.
void UPipeline();
Pipeline the logic to satisfy the required micro-cycle clock count (cannot be less than the maximum number of micro-cycles per user clock).
5.0 Clock Gating
Clock gating is performed using the algorithms outlined in [5]. This involves finding logic expressions for which (a) The state elements do not change value on the next cycle. (b) The output of state elements is not observed on the next cycle. In each case the value of the state elements can be preserved without corrupting the design.
6.0 How To Build
The system has been tested and developed using MS Visual Studio (v 6.0 or later). The approach used was to link in the abc static library (abc.lib) boost and verific libraries. An abc library is included with the code. The verific library and header files must be obtained from Verific.
Test programs showing the invocation of the various apis are included in the “examples” directory. The test program test_main.cpp shows the invocation of the main routines.
For example to build the test main program the following command can be used:
g++ test_main.cpp –o logictools.exe –I../include liblogictools.a libverific.a libabc.a boost.a
In Visual Studio the library logictools.lib must be included in the project along with links to the verify, abc and boost libraries.
7.0 The logictools.exe demonstration binary.
7.1 Introduction
To demonstrate the various algorithms and packages a binary “logictools.exe” is available, this requires a Verific license and can be built from the sources using the file test_main.cpp. This binary takes the following arguments:
./logictools.exe [--help] --[mode] --[mode arguments] --I [verilog search directory] --v [verilog files] --r [root_object] [--vin verilog_file_name] [--vout verilog_file_name]
The vin and vout arguments force the binary to write the design to the nominated verilog files before and after running the various packages.
The following arguments show the use of the binary:
7.2 Using Binary To Execute abc on Verilog and write out Verilog result.
./logictools.exe --package abc --v counter1.v --v2k true --root counter --abcscript cmd.txt --vout vout.v
Read in the verilog file counter1.v build the abc data structures, invoke the abc commands in cnd.txt, convert the result back to verific data structures and write the result out to file vout.v
The code to implement this flow is shown in file test_abcintf.cpp
An example abc script is:
strash
if -K 4
write_blif c:/temp/test2.blif
7.3 Formal synchronous verification using abc dsec command.
./logictools.exe --package abcdsec --v1 counter.v --v2 counter1.v --v2k true --root counter
Read in the verilog files counter.v, counter1.v and compare them using the abc dsec algorithm. This performs a full synchronous comparison by converting the designs to a form abc can understand and then using the abc dsec command to perform a synchronous compare.
The code to implement this flow is shown in file test_verifyabc.cpp.
7.4 Generating clock gates
./logictools.exe --package cgate --v cgate1.v --v2k true --root cgate1 --cg_ip true
Read in the verilog file cgate1.v extract and report the enable conditions for which d==q for each state element on the next cycle.