/**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 $] ***********************************************************************/ #include "kit.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// // factoring fails if intermediate memory usage exceed this limit #define KIT_FACTOR_MEM_LIMIT (1<<20) 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 ); extern int Kit_SopFactorVerify( Vec_Int_t * cSop, Kit_Graph_t * pFForm, int nVars ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Factors the cover.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Kit_Graph_t * Kit_SopFactor( Vec_Int_t * vCover, int fCompl, int nVars, Vec_Int_t * vMemory ) { 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; } /**Function************************************************************* Synopsis [Recursive factoring procedure.] Description [For the pseudo-code, see Hachtel/Somenzi, Logic synthesis and verification algorithms, Kluwer, 1996, p. 432.] SideEffects [] SeeAlso [] ***********************************************************************/ Kit_Edge_t Kit_SopFactor_rec( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, int nLits, Vec_Int_t * vMemory ) { 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 ); } /**Function************************************************************* Synopsis [Internal recursive factoring procedure for the leaf case.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Kit_Edge_t Kit_SopFactorLF_rec( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, Kit_Sop_t * cSimple, int nLits, Vec_Int_t * vMemory ) { 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 ); } /**Function************************************************************* Synopsis [Factoring cube.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Kit_Edge_t Kit_SopFactorTrivialCube_rec( Kit_Graph_t * pFForm, unsigned uCube, int nStart, int nFinish ) { 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 ); } /**Function************************************************************* Synopsis [Factoring cube.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Kit_Edge_t Kit_SopFactorTrivialCube( Kit_Graph_t * pFForm, unsigned uCube, int nLits ) { return Kit_SopFactorTrivialCube_rec( pFForm, uCube, 0, nLits ); } /**Function************************************************************* Synopsis [Factoring SOP.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Kit_Edge_t Kit_SopFactorTrivial_rec( Kit_Graph_t * pFForm, unsigned * pCubes, int nCubes, int nLits ) { 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 ); } /**Function************************************************************* Synopsis [Factoring the cover, which has no algebraic divisors.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Kit_Edge_t Kit_SopFactorTrivial( Kit_Graph_t * pFForm, Kit_Sop_t * cSop, int nLits ) { return Kit_SopFactorTrivial_rec( pFForm, cSop->pCubes, cSop->nCubes, nLits ); } /**Function************************************************************* Synopsis [Testing procedure for the factoring code.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Kit_FactorTest( unsigned * pTruth, int nVars ) { 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 ); } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END