kitFactor.c File Reference

#include "kit.h"

Go to the source code of this file.

Macros
#define	KIT_FACTOR_MEM_LIMIT   (1<<20)
	DECLARATIONS ///. More...

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)
	FUNCTION DEFINITIONS ///. More...
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)

Macro Definition Documentation

#define KIT_FACTOR_MEM_LIMIT   (1<<20)

DECLARATIONS ///.

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

]

Definition at line 31 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 308 of file kitFactor.c.

{
    Vec_Int_t * vCover, * vMemory;
    Kit_Graph_t * pGraph;
//    unsigned uTruthRes;
    int RetValue;

    // derive SOP
    vCover = Vec_IntAlloc( 0 );
    RetValue = Kit_TruthIsop( pTruth, nVars, vCover, 0 );
    assert( RetValue == 0 );

    // derive factored form
    vMemory = Vec_IntAlloc( 0 );
    pGraph = Kit_SopFactor( vCover, 0, nVars, vMemory );
/*
    // derive truth table
    assert( nVars <= 5 );
    uTruthRes = Kit_GraphToTruth( pGraph );
    if ( uTruthRes != pTruth[0] )
        printf( "Verification failed!" );
*/
    printf( "Vars = %2d. Cubes = %3d. FFNodes = %3d. FF_memory = %3d.\n",
        nVars, Vec_IntSize(vCover), Kit_GraphNodeNum(pGraph), Vec_IntSize(vMemory) );

    Vec_IntFree( vMemory );
    Vec_IntFree( vCover );
    Kit_GraphFree( pGraph );
}

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 55 of file kitFactor.c.

{
    Kit_Sop_t Sop, * cSop = &Sop;
    Kit_Graph_t * pFForm;
    Kit_Edge_t eRoot;
//    int nCubes;

    // works for up to 15 variables because division procedure
    // used the last bit for marking the cubes going to the remainder
    assert( nVars < 16 );

    // check for trivial functions
    if ( Vec_IntSize(vCover) == 0 )
        return Kit_GraphCreateConst0();
    if ( Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0 )
        return Kit_GraphCreateConst1();

    // prepare memory manager
//    Vec_IntClear( vMemory );
    Vec_IntGrow( vMemory, KIT_FACTOR_MEM_LIMIT );

    // perform CST
    Kit_SopCreateInverse( cSop, vCover, 2 * nVars, vMemory ); // CST

    // start the factored form
    pFForm = Kit_GraphCreate( nVars );
    // factor the cover
    eRoot = Kit_SopFactor_rec( pFForm, cSop, 2 * nVars, vMemory );
    // finalize the factored form
    Kit_GraphSetRoot( pFForm, eRoot );
    if ( fCompl )
        Kit_GraphComplement( pFForm );

    // verify the factored form
//    nCubes = Vec_IntSize(vCover);
//    Vec_IntShrink( vCover, nCubes );
//    if ( !Kit_SopFactorVerify( vCover, pFForm, nVars ) )
//        printf( "Verification has failed.\n" );
    return pFForm;
}

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 108 of file kitFactor.c.

{
    Kit_Sop_t Div, Quo, Rem, Com;
    Kit_Sop_t * cDiv = &Div, * cQuo = &Quo, * cRem = &Rem, * cCom = &Com;
    Kit_Edge_t eNodeDiv, eNodeQuo, eNodeRem, eNodeAnd;

    // make sure the cover contains some cubes
    assert( Kit_SopCubeNum(cSop) > 0 );

    // get the divisor
    if ( !Kit_SopDivisor(cDiv, cSop, nLits, vMemory) )
        return Kit_SopFactorTrivial( pFForm, cSop, nLits );

    // divide the cover by the divisor
    Kit_SopDivideInternal( cSop, cDiv, cQuo, cRem, vMemory );

    // check the trivial case
    assert( Kit_SopCubeNum(cQuo) > 0 );
    if ( Kit_SopCubeNum(cQuo) == 1 )
        return Kit_SopFactorLF_rec( pFForm, cSop, cQuo, nLits, vMemory );

    // make the quotient cube ABC_FREE
    Kit_SopMakeCubeFree( cQuo );

    // divide the cover by the quotient
    Kit_SopDivideInternal( cSop, cQuo, cDiv, cRem, vMemory );

    // check the trivial case
    if ( Kit_SopIsCubeFree( cDiv ) )
    {
        eNodeDiv = Kit_SopFactor_rec( pFForm, cDiv, nLits, vMemory );
        eNodeQuo = Kit_SopFactor_rec( pFForm, cQuo, nLits, vMemory );
        eNodeAnd = Kit_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
        if ( Kit_SopCubeNum(cRem) == 0 )
            return eNodeAnd;
        eNodeRem = Kit_SopFactor_rec( pFForm, cRem, nLits, vMemory );
        return Kit_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
    }

    // get the common cube
    Kit_SopCommonCubeCover( cCom, cDiv, vMemory );

    // solve the simple problem
    return Kit_SopFactorLF_rec( pFForm, cSop, cCom, nLits, vMemory );
}

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 166 of file kitFactor.c.

{
    Kit_Sop_t Div, Quo, Rem;
    Kit_Sop_t * cDiv = &Div, * cQuo = &Quo, * cRem = &Rem;
    Kit_Edge_t eNodeDiv, eNodeQuo, eNodeRem, eNodeAnd;
    assert( Kit_SopCubeNum(cSimple) == 1 );
    // get the most often occurring literal
    Kit_SopBestLiteralCover( cDiv, cSop, Kit_SopCube(cSimple, 0), nLits, vMemory );
    // divide the cover by the literal
    Kit_SopDivideByCube( cSop, cDiv, cQuo, cRem, vMemory );
    // get the node pointer for the literal
    eNodeDiv = Kit_SopFactorTrivialCube( pFForm, Kit_SopCube(cDiv, 0), nLits );
    // factor the quotient and remainder
    eNodeQuo = Kit_SopFactor_rec( pFForm, cQuo, nLits, vMemory );
    eNodeAnd = Kit_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
    if ( Kit_SopCubeNum(cRem) == 0 )
        return eNodeAnd;
    eNodeRem = Kit_SopFactor_rec( pFForm, cRem, nLits, vMemory );
    return Kit_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
}

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 291 of file kitFactor.c.

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

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 263 of file kitFactor.c.

{
    Kit_Edge_t eNode1, eNode2;
    int nCubes1, nCubes2;
    if ( nCubes == 1 )
        return Kit_SopFactorTrivialCube_rec( pFForm, pCubes[0], 0, nLits );
    // split the cubes into two parts
    nCubes1 = nCubes/2;
    nCubes2 = nCubes - nCubes1;
//    nCubes2 = nCubes/2;
//    nCubes1 = nCubes - nCubes2;
    // recursively construct the tree for the parts
    eNode1 = Kit_SopFactorTrivial_rec( pFForm, pCubes,           nCubes1, nLits );
    eNode2 = Kit_SopFactorTrivial_rec( pFForm, pCubes + nCubes1, nCubes2, nLits );
    return Kit_GraphAddNodeOr( pFForm, eNode1, eNode2 );
}

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

static

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

Synopsis [Factoring cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 247 of file kitFactor.c.

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

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 199 of file kitFactor.c.

{
    Kit_Edge_t eNode1, eNode2;
    int i, iLit = -1, nLits, nLits1, nLits2;
    assert( uCube );
    // count the number of literals in this interval
    nLits = 0;
    for ( i = nStart; i < nFinish; i++ )
        if ( Kit_CubeHasLit(uCube, i) )
        {
            iLit = i;
            nLits++;
        }
    assert( iLit != -1 );
    // quit if there is only one literal        
    if ( nLits == 1 )
        return Kit_EdgeCreate( iLit/2, iLit%2 ); // CST
    // split the literals into two parts
    nLits1 = nLits/2;
    nLits2 = nLits - nLits1;
//    nLits2 = nLits/2;
//    nLits1 = nLits - nLits2;
    // find the splitting point
    nLits = 0;
    for ( i = nStart; i < nFinish; i++ )
        if ( Kit_CubeHasLit(uCube, i) )
        {
            if ( nLits == nLits1 )
                break;
            nLits++;
        }
    // recursively construct the tree for the parts
    eNode1 = Kit_SopFactorTrivialCube_rec( pFForm, uCube, nStart, i  );
    eNode2 = Kit_SopFactorTrivialCube_rec( pFForm, uCube, i, nFinish );
    return Kit_GraphAddNodeAnd( pFForm, eNode1, eNode2 );
}

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 198 of file kitBdd.c.

{
    static DdManager * dd = NULL;
    Kit_Sop_t Sop, * cSop = &Sop;
    DdNode * bFunc1, * bFunc2;
    Vec_Int_t * vMemory;
    int RetValue;
    // get the manager
    if ( dd == NULL )
        dd = Cudd_Init( 16, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
    // derive SOP
    vMemory = Vec_IntAlloc( Vec_IntSize(vCover) );
    Kit_SopCreate( cSop, vCover, nVars, vMemory );
    // get the functions
    bFunc1 = Kit_SopToBdd( dd, cSop, nVars );      Cudd_Ref( bFunc1 );
    bFunc2 = Kit_GraphToBdd( dd, pFForm );         Cudd_Ref( bFunc2 );
//Extra_bddPrint( dd, bFunc1 ); printf("\n");
//Extra_bddPrint( dd, bFunc2 ); printf("\n");
    RetValue = (bFunc1 == bFunc2);
    if ( bFunc1 != bFunc2 )
    {
        int s;
        Extra_bddPrint( dd, bFunc1 ); printf("\n");
        Extra_bddPrint( dd, bFunc2 ); printf("\n");
        s  = 0;
    }
    Cudd_RecursiveDeref( dd, bFunc1 );
    Cudd_RecursiveDeref( dd, bFunc2 );
    Vec_IntFree( vMemory );
    return RetValue;
}