| /**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 |
| |
