src/aig/kit/kitFactor.c File Reference

#include "kit.h"
Include dependency graph for kitFactor.c:

Go to the source code of this file.

Defines

#define KIT_FACTOR_MEM_LIMIT   (1<<16)

Functions

static Kit_Edge_t Kit_SopFactor_rec (Kit_Graph_t *pFForm, Kit_Sop_t *cSop, int nLits, Vec_Int_t *vMemory)
static Kit_Edge_t Kit_SopFactorLF_rec (Kit_Graph_t *pFForm, Kit_Sop_t *cSop, Kit_Sop_t *cSimple, int nLits, Vec_Int_t *vMemory)
static Kit_Edge_t Kit_SopFactorTrivial (Kit_Graph_t *pFForm, Kit_Sop_t *cSop, int nLits)
static Kit_Edge_t Kit_SopFactorTrivialCube (Kit_Graph_t *pFForm, unsigned uCube, int nLits)
int Kit_SopFactorVerify (Vec_Int_t *cSop, Kit_Graph_t *pFForm, int nVars)
Kit_Graph_t * Kit_SopFactor (Vec_Int_t *vCover, int fCompl, int nVars, Vec_Int_t *vMemory)
Kit_Edge_t Kit_SopFactorTrivialCube_rec (Kit_Graph_t *pFForm, unsigned uCube, int nStart, int nFinish)
Kit_Edge_t Kit_SopFactorTrivial_rec (Kit_Graph_t *pFForm, unsigned *pCubes, int nCubes, int nLits)
void Kit_FactorTest (unsigned *pTruth, int nVars)

Define Documentation

#define KIT_FACTOR_MEM_LIMIT   (1<<16)

CFile****************************************************************

FileName [kitFactor.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

Synopsis [Algebraic factoring.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Dec 6, 2006.]

Revision [

Id
kitFactor.c,v 1.00 2006/12/06 00:00:00 alanmi Exp

] DECLARATIONS ///

Definition at line 28 of file kitFactor.c.

Function Documentation

void Kit_FactorTest ( unsigned *  pTruth,
int  nVars 
)

Function*************************************************************

Synopsis [Testing procedure for the factoring code.]

Description []

SideEffects []

SeeAlso []

Definition at line 305 of file kitFactor.c.

00306 {
00307     Vec_Int_t * vCover, * vMemory;
00308     Kit_Graph_t * pGraph;
00309 //    unsigned uTruthRes;
00310     int RetValue;
00311 
00312     // derive SOP
00313     vCover = Vec_IntAlloc( 0 );
00314     RetValue = Kit_TruthIsop( pTruth, nVars, vCover, 0 );
00315     assert( RetValue == 0 );
00316 
00317     // derive factored form
00318     vMemory = Vec_IntAlloc( 0 );
00319     pGraph = Kit_SopFactor( vCover, 0, nVars, vMemory );
00320 /*
00321     // derive truth table
00322     assert( nVars <= 5 );
00323     uTruthRes = Kit_GraphToTruth( pGraph );
00324     if ( uTruthRes != pTruth[0] )
00325         printf( "Verification failed!" );
00326 */
00327     printf( "Vars = %2d. Cubes = %3d. FFNodes = %3d. FF_memory = %3d.\n",
00328         nVars, Vec_IntSize(vCover), Kit_GraphNodeNum(pGraph), Vec_IntSize(vMemory) );
00329 
00330     Vec_IntFree( vMemory );
00331     Vec_IntFree( vCover );
00332     Kit_GraphFree( pGraph );
00333 }

Kit_Graph_t* Kit_SopFactor ( Vec_Int_t *  vCover,
int  fCompl,
int  nVars,
Vec_Int_t *  vMemory 
)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Factors the cover.]

Description []

SideEffects []

SeeAlso []

Definition at line 52 of file kitFactor.c.

00053 {
00054     Kit_Sop_t Sop, * cSop = &Sop;
00055     Kit_Graph_t * pFForm;
00056     Kit_Edge_t eRoot;
00057 //    int nCubes;
00058 
00059     // works for up to 15 variables because divisin procedure
00060     // used the last bit for marking the cubes going to the remainder
00061     assert( nVars < 16 );
00062 
00063     // check for trivial functions
00064     if ( Vec_IntSize(vCover) == 0 )
00065         return Kit_GraphCreateConst0();
00066     if ( Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0 )
00067         return Kit_GraphCreateConst1();
00068 
00069     // prepare memory manager
00070 //    Vec_IntClear( vMemory );
00071     Vec_IntGrow( vMemory, KIT_FACTOR_MEM_LIMIT );
00072 
00073     // perform CST
00074     Kit_SopCreateInverse( cSop, vCover, 2 * nVars, vMemory ); // CST
00075 
00076     // start the factored form
00077     pFForm = Kit_GraphCreate( nVars );
00078     // factor the cover
00079     eRoot = Kit_SopFactor_rec( pFForm, cSop, 2 * nVars, vMemory );
00080     // finalize the factored form
00081     Kit_GraphSetRoot( pFForm, eRoot );
00082     if ( fCompl )
00083         Kit_GraphComplement( pFForm );
00084 
00085     // verify the factored form
00086 //    nCubes = Vec_IntSize(vCover);
00087 //    Vec_IntShrink( vCover, nCubes );
00088 //    if ( !Kit_SopFactorVerify( vCover, pFForm, nVars ) )
00089 //        printf( "Verification has failed.\n" );
00090     return pFForm;
00091 }

Kit_Edge_t Kit_SopFactor_rec ( Kit_Graph_t *  pFForm,
Kit_Sop_t *  cSop,
int  nLits,
Vec_Int_t *  vMemory 
) [static]

Function*************************************************************

Synopsis [Recursive factoring procedure.]

Description [For the pseudo-code, see Hachtel/Somenzi, Logic synthesis and verification algorithms, Kluwer, 1996, p. 432.]

SideEffects []

SeeAlso []

Definition at line 105 of file kitFactor.c.

00106 {
00107     Kit_Sop_t Div, Quo, Rem, Com;
00108     Kit_Sop_t * cDiv = &Div, * cQuo = &Quo, * cRem = &Rem, * cCom = &Com;
00109     Kit_Edge_t eNodeDiv, eNodeQuo, eNodeRem, eNodeAnd;
00110 
00111     // make sure the cover contains some cubes
00112     assert( Kit_SopCubeNum(cSop) > 0 );
00113 
00114     // get the divisor
00115     if ( !Kit_SopDivisor(cDiv, cSop, nLits, vMemory) )
00116         return Kit_SopFactorTrivial( pFForm, cSop, nLits );
00117 
00118     // divide the cover by the divisor
00119     Kit_SopDivideInternal( cSop, cDiv, cQuo, cRem, vMemory );
00120 
00121     // check the trivial case
00122     assert( Kit_SopCubeNum(cQuo) > 0 );
00123     if ( Kit_SopCubeNum(cQuo) == 1 )
00124         return Kit_SopFactorLF_rec( pFForm, cSop, cQuo, nLits, vMemory );
00125 
00126     // make the quotient cube free
00127     Kit_SopMakeCubeFree( cQuo );
00128 
00129     // divide the cover by the quotient
00130     Kit_SopDivideInternal( cSop, cQuo, cDiv, cRem, vMemory );
00131 
00132     // check the trivial case
00133     if ( Kit_SopIsCubeFree( cDiv ) )
00134     {
00135         eNodeDiv = Kit_SopFactor_rec( pFForm, cDiv, nLits, vMemory );
00136         eNodeQuo = Kit_SopFactor_rec( pFForm, cQuo, nLits, vMemory );
00137         eNodeAnd = Kit_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
00138         if ( Kit_SopCubeNum(cRem) == 0 )
00139             return eNodeAnd;
00140         eNodeRem = Kit_SopFactor_rec( pFForm, cRem, nLits, vMemory );
00141         return Kit_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
00142     }
00143 
00144     // get the common cube
00145     Kit_SopCommonCubeCover( cCom, cDiv, vMemory );
00146 
00147     // solve the simple problem
00148     return Kit_SopFactorLF_rec( pFForm, cSop, cCom, nLits, vMemory );
00149 }

Kit_Edge_t Kit_SopFactorLF_rec ( Kit_Graph_t *  pFForm,
Kit_Sop_t *  cSop,
Kit_Sop_t *  cSimple,
int  nLits,
Vec_Int_t *  vMemory 
) [static]

Function*************************************************************

Synopsis [Internal recursive factoring procedure for the leaf case.]

Description []

SideEffects []

SeeAlso []

Definition at line 163 of file kitFactor.c.

00164 {
00165     Kit_Sop_t Div, Quo, Rem;
00166     Kit_Sop_t * cDiv = &Div, * cQuo = &Quo, * cRem = &Rem;
00167     Kit_Edge_t eNodeDiv, eNodeQuo, eNodeRem, eNodeAnd;
00168     assert( Kit_SopCubeNum(cSimple) == 1 );
00169     // get the most often occurring literal
00170     Kit_SopBestLiteralCover( cDiv, cSop, Kit_SopCube(cSimple, 0), nLits, vMemory );
00171     // divide the cover by the literal
00172     Kit_SopDivideByCube( cSop, cDiv, cQuo, cRem, vMemory );
00173     // get the node pointer for the literal
00174     eNodeDiv = Kit_SopFactorTrivialCube( pFForm, Kit_SopCube(cDiv, 0), nLits );
00175     // factor the quotient and remainder
00176     eNodeQuo = Kit_SopFactor_rec( pFForm, cQuo, nLits, vMemory );
00177     eNodeAnd = Kit_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
00178     if ( Kit_SopCubeNum(cRem) == 0 )
00179         return eNodeAnd;
00180     eNodeRem = Kit_SopFactor_rec( pFForm, cRem, nLits, vMemory );
00181     return Kit_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
00182 }

Kit_Edge_t Kit_SopFactorTrivial ( Kit_Graph_t *  pFForm,
Kit_Sop_t *  cSop,
int  nLits 
) [static]

Function*************************************************************

Synopsis [Factoring the cover, which has no algebraic divisors.]

Description []

SideEffects []

SeeAlso []

Definition at line 288 of file kitFactor.c.

00289 {
00290     return Kit_SopFactorTrivial_rec( pFForm, cSop->pCubes, cSop->nCubes, nLits );
00291 }

Kit_Edge_t Kit_SopFactorTrivial_rec ( Kit_Graph_t *  pFForm,
unsigned *  pCubes,
int  nCubes,
int  nLits 
)

Function*************************************************************

Synopsis [Factoring SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 260 of file kitFactor.c.

00261 {
00262     Kit_Edge_t eNode1, eNode2;
00263     int nCubes1, nCubes2;
00264     if ( nCubes == 1 )
00265         return Kit_SopFactorTrivialCube_rec( pFForm, pCubes[0], 0, nLits );
00266     // split the cubes into two parts
00267     nCubes1 = nCubes/2;
00268     nCubes2 = nCubes - nCubes1;
00269 //    nCubes2 = nCubes/2;
00270 //    nCubes1 = nCubes - nCubes2;
00271     // recursively construct the tree for the parts
00272     eNode1 = Kit_SopFactorTrivial_rec( pFForm, pCubes,           nCubes1, nLits );
00273     eNode2 = Kit_SopFactorTrivial_rec( pFForm, pCubes + nCubes1, nCubes2, nLits );
00274     return Kit_GraphAddNodeOr( pFForm, eNode1, eNode2 );
00275 }

Kit_Edge_t Kit_SopFactorTrivialCube ( Kit_Graph_t *  pFForm,
unsigned  uCube,
int  nLits 
) [static]

Function*************************************************************

Synopsis [Factoring cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 244 of file kitFactor.c.

00245 {
00246     return Kit_SopFactorTrivialCube_rec( pFForm, uCube, 0, nLits );
00247 }

Kit_Edge_t Kit_SopFactorTrivialCube_rec ( Kit_Graph_t *  pFForm,
unsigned  uCube,
int  nStart,
int  nFinish 
)

Function*************************************************************

Synopsis [Factoring cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 196 of file kitFactor.c.

00197 {
00198     Kit_Edge_t eNode1, eNode2;
00199     int i, iLit = -1, nLits, nLits1, nLits2;
00200     assert( uCube );
00201     // count the number of literals in this interval
00202     nLits = 0;
00203     for ( i = nStart; i < nFinish; i++ )
00204         if ( Kit_CubeHasLit(uCube, i) )
00205         {
00206             iLit = i;
00207             nLits++;
00208         }
00209     assert( iLit != -1 );
00210     // quit if there is only one literal        
00211     if ( nLits == 1 )
00212         return Kit_EdgeCreate( iLit/2, iLit%2 ); // CST
00213     // split the literals into two parts
00214     nLits1 = nLits/2;
00215     nLits2 = nLits - nLits1;
00216 //    nLits2 = nLits/2;
00217 //    nLits1 = nLits - nLits2;
00218     // find the splitting point
00219     nLits = 0;
00220     for ( i = nStart; i < nFinish; i++ )
00221         if ( Kit_CubeHasLit(uCube, i) )
00222         {
00223             if ( nLits == nLits1 )
00224                 break;
00225             nLits++;
00226         }
00227     // recursively construct the tree for the parts
00228     eNode1 = Kit_SopFactorTrivialCube_rec( pFForm, uCube, nStart, i  );
00229     eNode2 = Kit_SopFactorTrivialCube_rec( pFForm, uCube, i, nFinish );
00230     return Kit_GraphAddNodeAnd( pFForm, eNode1, eNode2 );
00231 }

int Kit_SopFactorVerify ( Vec_Int_t *  vCover,
Kit_Graph_t *  pFForm,
int  nVars 
)

Function*************************************************************

Synopsis [Verifies that the factoring is correct.]

Description []

SideEffects []

SeeAlso []

Definition at line 195 of file kitBdd.c.

00196 {
00197     static DdManager * dd = NULL;
00198     Kit_Sop_t Sop, * cSop = &Sop;
00199     DdNode * bFunc1, * bFunc2;
00200     Vec_Int_t * vMemory;
00201     int RetValue;
00202     // get the manager
00203     if ( dd == NULL )
00204         dd = Cudd_Init( 16, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
00205     // derive SOP
00206     vMemory = Vec_IntAlloc( Vec_IntSize(vCover) );
00207     Kit_SopCreate( cSop, vCover, nVars, vMemory );
00208     // get the functions
00209     bFunc1 = Kit_SopToBdd( dd, cSop, nVars );      Cudd_Ref( bFunc1 );
00210     bFunc2 = Kit_GraphToBdd( dd, pFForm );         Cudd_Ref( bFunc2 );
00211 //Extra_bddPrint( dd, bFunc1 ); printf("\n");
00212 //Extra_bddPrint( dd, bFunc2 ); printf("\n");
00213     RetValue = (bFunc1 == bFunc2);
00214     if ( bFunc1 != bFunc2 )
00215     {
00216         int s;
00217         Extra_bddPrint( dd, bFunc1 ); printf("\n");
00218         Extra_bddPrint( dd, bFunc2 ); printf("\n");
00219         s  = 0;
00220     }
00221     Cudd_RecursiveDeref( dd, bFunc1 );
00222     Cudd_RecursiveDeref( dd, bFunc2 );
00223     Vec_IntFree( vMemory );
00224     return RetValue;
00225 }

Generated on Tue Jan 5 12:18:27 2010 for abc70930 by  doxygen 1.6.1