kitFactor.c File Reference

#include "kit.h"

Include dependency graph for kitFactor.c:

Go to the source code of this file.

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

Functions
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 ///.
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

KIT_FACTOR_MEM_LIMIT

#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

Kit_FactorTest()

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 );
}

Here is the call graph for this function:

Kit_SopFactor()

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_SopFactorTrivial_rec()

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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_SopFactorTrivialCube_rec()

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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Kit_SopFactorVerify()

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

extern