diff options
Diffstat (limited to 'src/aig')
| -rw-r--r-- | src/aig/ivy/ivy.h | 2 | ||||
| -rw-r--r-- | src/aig/ivy/ivyFactor.c | 783 | ||||
| -rw-r--r-- | src/aig/ivy/ivyFpga.c | 378 | ||||
| -rw-r--r-- | src/aig/ivy/ivyIsop.c | 327 | ||||
| -rw-r--r-- | src/aig/ivy/module.make | 1 |
5 files changed, 0 insertions, 1491 deletions
diff --git a/src/aig/ivy/ivy.h b/src/aig/ivy/ivy.h index 91d4d767..f48466ef 100644 --- a/src/aig/ivy/ivy.h +++ b/src/aig/ivy/ivy.h @@ -466,8 +466,6 @@ extern void Ivy_ManHaigPostprocess( Ivy_Man_t * p, int fVerbose ); extern void Ivy_ManHaigCreateObj( Ivy_Man_t * p, Ivy_Obj_t * pObj ); extern void Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew ); extern void Ivy_ManHaigSimulate( Ivy_Man_t * p ); -/*=== ivyIsop.c ==========================================================*/ -extern int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth ); /*=== ivyMan.c ==========================================================*/ extern Ivy_Man_t * Ivy_ManStart(); extern Ivy_Man_t * Ivy_ManStartFrom( Ivy_Man_t * p ); diff --git a/src/aig/ivy/ivyFactor.c b/src/aig/ivy/ivyFactor.c deleted file mode 100644 index 19a40b3f..00000000 --- a/src/aig/ivy/ivyFactor.c +++ /dev/null @@ -1,783 +0,0 @@ -/**CFile**************************************************************** - - FileName [ivyFactor.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [And-Inverter Graph package.] - - Synopsis [Factoring the cover up to 16 inputs.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - May 11, 2006.] - - Revision [$Id: ivyFactor.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "ivy.h" -#include "dec.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -// ISOP computation fails if intermediate memory usage exceed this limit -#define IVY_FACTOR_MEM_LIMIT 16*4096 - -// intermediate ISOP representation -typedef struct Ivy_Sop_t_ Ivy_Sop_t; -struct Ivy_Sop_t_ -{ - unsigned * uCubes; - int nCubes; -}; - -static inline int Ivy_CubeHasLit( unsigned uCube, int i ) { return (uCube & (unsigned)(1<<i)) > 0;} -static inline unsigned Ivy_CubeSetLit( unsigned uCube, int i ) { return uCube | (unsigned)(1<<i); } -static inline unsigned Ivy_CubeXorLit( unsigned uCube, int i ) { return uCube ^ (unsigned)(1<<i); } -static inline unsigned Ivy_CubeRemLit( unsigned uCube, int i ) { return uCube & ~(unsigned)(1<<i); } - -static inline int Ivy_CubeContains( unsigned uLarge, unsigned uSmall ) { return (uLarge & uSmall) == uSmall; } -static inline unsigned Ivy_CubeSharp( unsigned uCube, unsigned uPart ) { return uCube & ~uPart; } -static inline unsigned Ivy_CubeMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); } - -static inline int Ivy_CubeIsMarked( unsigned uCube ) { return Ivy_CubeHasLit( uCube, 31 ); } -static inline void Ivy_CubeMark( unsigned uCube ) { Ivy_CubeSetLit( uCube, 31 ); } -static inline void Ivy_CubeUnmark( unsigned uCube ) { Ivy_CubeRemLit( uCube, 31 ); } - -static inline int Ivy_SopCubeNum( Ivy_Sop_t * cSop ) { return cSop->nCubes; } -static inline unsigned Ivy_SopCube( Ivy_Sop_t * cSop, int i ) { return cSop->uCubes[i]; } -static inline void Ivy_SopAddCube( Ivy_Sop_t * cSop, unsigned uCube ) { cSop->uCubes[cSop->nCubes++] = uCube; } -static inline void Ivy_SopSetCube( Ivy_Sop_t * cSop, unsigned uCube, int i ) { cSop->uCubes[i] = uCube; } -static inline void Ivy_SopShrink( Ivy_Sop_t * cSop, int nCubesNew ) { cSop->nCubes = nCubesNew; } - -// iterators -#define Ivy_SopForEachCube( cSop, uCube, i ) \ - for ( i = 0; (i < Ivy_SopCubeNum(cSop)) && ((uCube) = Ivy_SopCube(cSop, i)); i++ ) -#define Ivy_CubeForEachLiteral( uCube, Lit, nLits, i ) \ - for ( i = 0; (i < (nLits)) && ((Lit) = Ivy_CubeHasLit(uCube, i)); i++ ) - -/**Function************************************************************* - - Synopsis [Divides cover by one cube.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_SopDivideByCube( Vec_Int_t * vStore, int nVars, Ivy_Sop_t * cSop, Ivy_Sop_t * cDiv, Ivy_Sop_t * vQuo, Ivy_Sop_t * vRem ) -{ - unsigned uCube, uDiv; - int i; - // get the only cube - assert( Ivy_SopCubeNum(cDiv) == 1 ); - uDiv = Ivy_SopCube(cDiv, 0); - // allocate covers - vQuo->nCubes = 0; - vQuo->uCubes = Vec_IntFetch( vStore, Ivy_SopCubeNum(cSop) ); - vRem->nCubes = 0; - vRem->uCubes = Vec_IntFetch( vStore, Ivy_SopCubeNum(cSop) ); - // sort the cubes - Ivy_SopForEachCube( cSop, uCube, i ) - { - if ( Ivy_CubeContains( uCube, uDiv ) ) - Ivy_SopAddCube( vQuo, Ivy_CubeSharp(uCube, uDiv) ); - else - Ivy_SopAddCube( vRem, uCube ); - } -} - -/**Function************************************************************* - - Synopsis [Divides cover by one cube.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_SopDivideInternal( Vec_Int_t * vStore, int nVars, Ivy_Sop_t * cSop, Ivy_Sop_t * cDiv, Ivy_Sop_t * vQuo, Ivy_Sop_t * vRem ) -{ - unsigned uCube, uCube2, uDiv, uDiv2, uQuo; - int i, i2, k, k2; - assert( Ivy_SopCubeNum(cSop) >= Ivy_SopCubeNum(cDiv) ); - if ( Ivy_SopCubeNum(cDiv) == 1 ) - { - Ivy_SopDivideByCube( cSop, cDiv, vQuo, vRem ); - return; - } - // allocate quotient - vQuo->nCubes = 0; - vQuo->uCubes = Vec_IntFetch( vStore, Ivy_SopCubeNum(cSop) / Ivy_SopCubeNum(cDiv) ); - // for each cube of the cover - // it either belongs to the quotient or to the remainder - Ivy_SopForEachCube( cSop, uCube, i ) - { - // skip taken cubes - if ( Ivy_CubeIsMarked(uCube) ) - continue; - // mark the cube - Ivy_SopSetCube( cSop, Ivy_CubeMark(uCube), i ); - // find a matching cube in the divisor - Ivy_SopForEachCube( cDiv, uDiv, k ) - if ( Ivy_CubeContains( uCube, uDiv ) ) - break; - // the case when the cube is not found - // (later we will add marked cubes to the remainder) - if ( k == Ivy_SopCubeNum(cDiv) ) - continue; - // if the quotient cube exist, it will be - uQuo = Ivy_CubeSharp( uCube, uDiv ); - // try to find other cubes of the divisor - Ivy_SopForEachCube( cDiv, uDiv2, k2 ) - { - if ( k2 == k ) - continue; - // find a matching cube - Ivy_SopForEachCube( cSop, uCube2, i2 ) - { - // skip taken cubes - if ( Ivy_CubeIsMarked(uCube2) ) - continue; - // check if the cube can be used - if ( Ivy_CubeContains( uCube2, uDiv2 ) && uQuo == Ivy_CubeSharp( uCube2, uDiv2 ) ) - break; - } - // the case when the cube is not found - if ( i2 == Ivy_SopCubeNum(cSop) ) - break; - // the case when the cube is found - mark it and keep going - Ivy_SopSetCube( cSop, Ivy_CubeMark(uCube2), i2 ); - } - // if we did not find some cube, continue - // (later we will add marked cubes to the remainder) - if ( k2 != Ivy_SopCubeNum(cDiv) ) - continue; - // we found all cubes - add the quotient cube - Ivy_SopAddCube( vQuo, uQuo ); - } - // allocate remainder - vRem->nCubes = 0; - vRem->uCubes = Vec_IntFetch( vStore, Ivy_SopCubeNum(cSop) - Ivy_SopCubeNum(vQuo) * Ivy_SopCubeNum(cDiv) ); - // finally add the remaining cubes to the remainder - // and clean the marked cubes in the cover - Ivy_SopForEachCube( cSop, uCube, i ) - { - if ( !Ivy_CubeIsMarked(uCube) ) - continue; - Ivy_SopSetCube( cSop, Ivy_CubeUnmark(uCube), i ); - Ivy_SopAddCube( vRem, Ivy_CubeUnmark(uCube) ); - } -} - -/**Function************************************************************* - - Synopsis [Derives the quotient of division by literal.] - - Description [Reduces the cover to be the equal to the result of - division of the given cover by the literal.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_SopDivideByLiteralQuo( Ivy_Sop_t * cSop, int iLit ) -{ - unsigned uCube; - int i, k = 0; - Ivy_SopForEachCube( cSop, uCube, i ) - { - if ( Ivy_CubeHasLit(uCube, iLit) ) - Ivy_SopSetCube( cSop, Ivy_CubeRemLit(uCube, iLit), k++ ); - } - Ivy_SopShrink( cSop, k ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_SopCommonCubeCover( Ivy_Sop_t * cSop, Ivy_Sop_t * vCommon, Vec_Int_t * vStore ) -{ - unsigned uTemp, uCube; - int i; - uCube = ~(unsigned)0; - Ivy_SopForEachCube( cSop, uTemp, i ) - uCube &= uTemp; - vCommon->nCubes = 0; - vCommon->uCubes = Vec_IntFetch( vStore, 1 ); - Ivy_SopPush( vCommon, uCube ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_SopCreateInverse( Ivy_Sop_t * cSop, Vec_Int_t * vInput, int nVars, Vec_Int_t * vStore ) -{ - unsigned uCube, uMask; - int i; - // start the cover - cSop->nCubes = 0; - cSop->uCubes = Vec_IntFetch( vStore, Vec_IntSize(vInput) ); - // add the cubes - uMask = Ivy_CubeMask( nVars ); - Vec_IntForEachEntry( vInput, uCube, i ) - Vec_IntPush( cSop, Ivy_CubeSharp(uMask, uCube) ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_SopDup( Ivy_Sop_t * cSop, Ivy_Sop_t * vCopy, Vec_Int_t * vStore ) -{ - unsigned uCube; - int i; - // start the cover - vCopy->nCubes = 0; - vCopy->uCubes = Vec_IntFetch( vStore, Vec_IntSize(cSop) ); - // add the cubes - Ivy_SopForEachCube( cSop, uTemp, i ) - Ivy_SopPush( vCopy, uTemp ); -} - - -/**Function************************************************************* - - Synopsis [Find the least often occurring literal.] - - Description [Find the least often occurring literal among those - that occur more than once.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ivy_SopWorstLiteral( Ivy_Sop_t * cSop, int nLits ) -{ - unsigned uCube; - int nWord, nBit; - int i, k, iMin, nLitsMin, nLitsCur; - int fUseFirst = 1; - - // go through each literal - iMin = -1; - nLitsMin = 1000000; - for ( i = 0; i < nLits; i++ ) - { - // go through all the cubes - nLitsCur = 0; - Ivy_SopForEachCube( cSop, uCube, k ) - if ( Ivy_CubeHasLit(uCube, i) ) - nLitsCur++; - // skip the literal that does not occur or occurs once - if ( nLitsCur < 2 ) - continue; - // check if this is the best literal - if ( fUseFirst ) - { - if ( nLitsMin > nLitsCur ) - { - nLitsMin = nLitsCur; - iMin = i; - } - } - else - { - if ( nLitsMin >= nLitsCur ) - { - nLitsMin = nLitsCur; - iMin = i; - } - } - } - if ( nLitsMin < 1000000 ) - return iMin; - return -1; -} - -/**Function************************************************************* - - Synopsis [Computes a level-zero kernel.] - - Description [Modifies the cover to contain one level-zero kernel.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_SopMakeCubeFree( Ivy_Sop_t * cSop ) -{ - unsigned uMask; - int i; - assert( Ivy_SopCubeNum(cSop) > 0 ); - // find the common cube - uMask = ~(unsigned)0; - Ivy_SopForEachCube( cSop, uCube, i ) - uMask &= uCube; - if ( uMask == 0 ) - return; - // remove the common cube - Ivy_SopForEachCube( cSop, uCube, i ) - Ivy_SopSetCube( cSop, Ivy_CubeSharp(uCube, uMask), i ); -} - -/**Function************************************************************* - - Synopsis [Computes a level-zero kernel.] - - Description [Modifies the cover to contain one level-zero kernel.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_SopDivisorZeroKernel_rec( Ivy_Sop_t * cSop, int nLits ) -{ - int iLit; - // find any literal that occurs at least two times - iLit = Ivy_SopWorstLiteral( cSop, nLits ); - if ( iLit == -1 ) - return; - // derive the cube-free quotient - Ivy_SopDivideByLiteralQuo( cSop, iLit ); // the same cover - Ivy_SopMakeCubeFree( cSop ); // the same cover - // call recursively - Ivy_SopDivisorZeroKernel_rec( cSop ); // the same cover -} - -/**Function************************************************************* - - Synopsis [Returns the quick divisor of the cover.] - - Description [Returns NULL, if there is not divisor other than - trivial.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ivy_SopDivisor( Ivy_Sop_t * cSop, int nLits, Ivy_Sop_t * cDiv, Vec_Int_t * vStore ) -{ - if ( Ivy_SopCubeNum(cSop) <= 1 ) - return 0; - if ( Ivy_SopWorstLiteral( cSop, nLits ) == -1 ) - return 0; - // duplicate the cover - Ivy_SopDup( cSop, cDiv, vStore ); - // perform the kerneling - Ivy_SopDivisorZeroKernel_rec( cDiv, int nLits ); - assert( Ivy_SopCubeNum(cDiv) > 0 ); - return 1; -} - - - - - -extern Dec_Edge_t Dec_Factor32_rec( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nVars ); -extern Dec_Edge_t Dec_Factor32LF_rec( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nVars, Vec_Int_t * vSimple ); -extern Dec_Edge_t Dec_Factor32Trivial( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nVars ); -extern Dec_Edge_t Dec_Factor32TrivialCube( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nVars, unsigned uCube, Vec_Int_t * vEdgeLits ); -extern Dec_Edge_t Dec_Factor32TrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr ); -extern int Dec_Factor32Verify( Vec_Int_t * cSop, Dec_Graph_t * pFForm ) - - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Factors the cover.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Dec_Graph_t * Dec_Factor32( Vec_Int_t * cSop, int nVars, Vec_Int_t * vStore ) -{ - Ivy_Sop_t cSop, cRes; - Ivy_Sop_t * pcSop = &cSop, * pcRes = &cRes; - Dec_Graph_t * pFForm; - Dec_Edge_t eRoot; - - assert( nVars < 16 ); - - // check for trivial functions - if ( Vec_IntSize(cSop) == 0 ) - return Dec_GraphCreateConst0(); - if ( Vec_IntSize(cSop) == 1 && Vec_IntEntry(cSop, 0) == Ivy_CubeMask(nVars) ) - return Dec_GraphCreateConst1(); - - // prepare memory manager - Vec_IntClear( vStore ); - Vec_IntGrow( vStore, IVY_FACTOR_MEM_LIMIT ); - - // perform CST - Ivy_SopCreateInverse( cSop, pcSop, nVars, vStore ); // CST - - // start the factored form - pFForm = Dec_GraphCreate( nVars ); - // factor the cover - eRoot = Dec_Factor32_rec( pFForm, cSop, 2 * nVars ); - // finalize the factored form - Dec_GraphSetRoot( pFForm, eRoot ); - - // verify the factored form - if ( !Dec_Factor32Verify( pSop, pFForm, nVars ) ) - printf( "Verification has failed.\n" ); - return pFForm; -} - -/**Function************************************************************* - - Synopsis [Internal recursive factoring procedure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Dec_Edge_t Dec_Factor32_rec( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nLits ) -{ - Vec_Int_t * cDiv, * vQuo, * vRem, * vCom; - Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem; - Dec_Edge_t eNodeAnd, eNode; - - // make sure the cover contains some cubes - assert( Vec_IntSize(cSop) ); - - // get the divisor - cDiv = Ivy_SopDivisor( cSop, nLits ); - if ( cDiv == NULL ) - return Dec_Factor32Trivial( pFForm, cSop, nLits ); - - // divide the cover by the divisor - Ivy_SopDivideInternal( cSop, nLits, cDiv, &vQuo, &vRem ); - assert( Vec_IntSize(vQuo) ); - - Vec_IntFree( cDiv ); - Vec_IntFree( vRem ); - - // check the trivial case - if ( Vec_IntSize(vQuo) == 1 ) - { - eNode = Dec_Factor32LF_rec( pFForm, cSop, nLits, vQuo ); - Vec_IntFree( vQuo ); - return eNode; - } - - // make the quotient cube free - Ivy_SopMakeCubeFree( vQuo ); - - // divide the cover by the quotient - Ivy_SopDivideInternal( cSop, nLits, vQuo, &cDiv, &vRem ); - - // check the trivial case - if ( Ivy_SopIsCubeFree( cDiv ) ) - { - eNodeDiv = Dec_Factor32_rec( pFForm, cDiv ); - eNodeQuo = Dec_Factor32_rec( pFForm, vQuo ); - Vec_IntFree( cDiv ); - Vec_IntFree( vQuo ); - eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo ); - if ( Vec_IntSize(vRem) == 0 ) - { - Vec_IntFree( vRem ); - return eNodeAnd; - } - else - { - eNodeRem = Dec_Factor32_rec( pFForm, vRem ); - Vec_IntFree( vRem ); - return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem ); - } - } - - // get the common cube - vCom = Ivy_SopCommonCubeCover( cDiv ); - Vec_IntFree( cDiv ); - Vec_IntFree( vQuo ); - Vec_IntFree( vRem ); - - // solve the simple problem - eNode = Dec_Factor32LF_rec( pFForm, cSop, nLits, vCom ); - Vec_IntFree( vCom ); - return eNode; -} - - -/**Function************************************************************* - - Synopsis [Internal recursive factoring procedure for the leaf case.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Dec_Edge_t Dec_Factor32LF_rec( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nLits, Vec_Int_t * vSimple ) -{ - Dec_Man_t * pManDec = Abc_FrameReadManDec(); - Vec_Int_t * vEdgeLits = pManDec->vLits; - Vec_Int_t * cDiv, * vQuo, * vRem; - Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem; - Dec_Edge_t eNodeAnd; - - // get the most often occurring literal - cDiv = Ivy_SopBestLiteralCover( cSop, nLits, vSimple ); - // divide the cover by the literal - Ivy_SopDivideByLiteral( cSop, nLits, cDiv, &vQuo, &vRem ); - // get the node pointer for the literal - eNodeDiv = Dec_Factor32TrivialCube( pFForm, cDiv, Ivy_SopReadCubeHead(cDiv), vEdgeLits ); - Vec_IntFree( cDiv ); - // factor the quotient and remainder - eNodeQuo = Dec_Factor32_rec( pFForm, vQuo ); - Vec_IntFree( vQuo ); - eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo ); - if ( Vec_IntSize(vRem) == 0 ) - { - Vec_IntFree( vRem ); - return eNodeAnd; - } - else - { - eNodeRem = Dec_Factor32_rec( pFForm, vRem ); - Vec_IntFree( vRem ); - return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem ); - } -} - - - -/**Function************************************************************* - - Synopsis [Factoring the cover, which has no algebraic divisors.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Dec_Edge_t Dec_Factor32Trivial( Dec_Graph_t * pFForm, Vec_Int_t * cSop, int nLits ) -{ - Dec_Man_t * pManDec = Abc_FrameReadManDec(); - Vec_Int_t * vEdgeCubes = pManDec->vCubes; - Vec_Int_t * vEdgeLits = pManDec->vLits; - Mvc_Manager_t * pMem = pManDec->pMvcMem; - Dec_Edge_t eNode; - unsigned uCube; - int i; - // create the factored form for each cube - Vec_IntClear( vEdgeCubes ); - Ivy_SopForEachCube( cSop, uCube ) - { - eNode = Dec_Factor32TrivialCube( pFForm, cSop, nLits, uCube, vEdgeLits ); - Vec_IntPush( vEdgeCubes, Dec_EdgeToInt_(eNode) ); - } - // balance the factored forms - return Dec_Factor32TrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeCubes->pArray, vEdgeCubes->nSize, 1 ); -} - -/**Function************************************************************* - - Synopsis [Factoring the cube.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Dec_Edge_t Dec_Factor32TrivialCube( Dec_Graph_t * pFForm, Vec_Int_t * cSop, unsigned uCube, int nLits, Vec_Int_t * vEdgeLits ) -{ - Dec_Edge_t eNode; - int iBit, Value; - // create the factored form for each literal - Vec_IntClear( vEdgeLits ); - Mvc_CubeForEachLit( cSop, uCube, iBit, Value ) - if ( Value ) - { - eNode = Dec_EdgeCreate( iBit/2, iBit%2 ); // CST - Vec_IntPush( vEdgeLits, Dec_EdgeToInt_(eNode) ); - } - // balance the factored forms - return Dec_Factor32TrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeLits->pArray, vEdgeLits->nSize, 0 ); -} - -/**Function************************************************************* - - Synopsis [Create the well-balanced tree of nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Dec_Edge_t Dec_Factor32TrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr ) -{ - Dec_Edge_t eNode1, eNode2; - int nNodes1, nNodes2; - - if ( nNodes == 1 ) - return peNodes[0]; - - // split the nodes into two parts - nNodes1 = nNodes/2; - nNodes2 = nNodes - nNodes1; -// nNodes2 = nNodes/2; -// nNodes1 = nNodes - nNodes2; - - // recursively construct the tree for the parts - eNode1 = Dec_Factor32TrivialTree_rec( pFForm, peNodes, nNodes1, fNodeOr ); - eNode2 = Dec_Factor32TrivialTree_rec( pFForm, peNodes + nNodes1, nNodes2, fNodeOr ); - - if ( fNodeOr ) - return Dec_GraphAddNodeOr( pFForm, eNode1, eNode2 ); - else - return Dec_GraphAddNodeAnd( pFForm, eNode1, eNode2 ); -} - - - - -// verification using temporary BDD package -#include "cuddInt.h" - -/**Function************************************************************* - - Synopsis [Verifies that the factoring is correct.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -DdNode * Ivy_SopCoverToBdd( DdManager * dd, Vec_Int_t * cSop, int nVars ) -{ - DdNode * bSum, * bCube, * bTemp, * bVar; - unsigned uCube; - int Value, v; - assert( nVars < 16 ); - // start the cover - bSum = Cudd_ReadLogicZero(dd); Cudd_Ref( bSum ); - // check the logic function of the node - Vec_IntForEachEntry( cSop, uCube, i ) - { - bCube = Cudd_ReadOne(dd); Cudd_Ref( bCube ); - for ( v = 0; v < nVars; v++ ) - { - Value = ((uCube >> 2*v) & 3); - if ( Value == 1 ) - bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) ); - else if ( Value == 2 ) - bVar = Cudd_bddIthVar( dd, v ); - else - continue; - bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar ); Cudd_Ref( bCube ); - Cudd_RecursiveDeref( dd, bTemp ); - } - bSum = Cudd_bddOr( dd, bTemp = bSum, bCube ); - Cudd_Ref( bSum ); - Cudd_RecursiveDeref( dd, bTemp ); - Cudd_RecursiveDeref( dd, bCube ); - } - // complement the result if necessary - Cudd_Deref( bSum ); - return bSum; -} - -/**Function************************************************************* - - Synopsis [Verifies that the factoring is correct.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dec_Factor32Verify( Vec_Int_t * cSop, Dec_Graph_t * pFForm, int nVars ) -{ - static DdManager * dd = NULL; - DdNode * bFunc1, * bFunc2; - int RetValue; - // get the manager - if ( dd == NULL ) - dd = Cudd_Init( 16, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); - // get the functions - bFunc1 = Ivy_SopCoverToBdd( dd, cSop, nVars ); Cudd_Ref( bFunc1 ); - bFunc2 = Dec_GraphDeriveBdd( 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 ); - return RetValue; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/aig/ivy/ivyFpga.c b/src/aig/ivy/ivyFpga.c deleted file mode 100644 index 122cc0e2..00000000 --- a/src/aig/ivy/ivyFpga.c +++ /dev/null @@ -1,378 +0,0 @@ -/**CFile**************************************************************** - - FileName [ivyFpga.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [And-Inverter Graph package.] - - Synopsis [Prepares the AIG package to work as an FPGA mapper.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - May 11, 2006.] - - Revision [$Id: ivyFpga.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "ivy.h" -#include "attr.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Ivy_FpgaMan_t_ Ivy_FpgaMan_t; -typedef struct Ivy_FpgaObj_t_ Ivy_FpgaObj_t; -typedef struct Ivy_FpgaCut_t_ Ivy_FpgaCut_t; - -// manager -struct Ivy_FpgaMan_t_ -{ - Ivy_Man_t * pManIvy; // the AIG manager - Attr_Man_t * pManAttr; // the attribute manager - int nLutSize; // the LUT size - int nCutsMax; // the max number of cuts - int nEntrySize; // the size of the entry - int nEntryBase; // the size of the entry minus cut leaf arrays - int fVerbose; // the verbosity flag - // temporary cut storage - Ivy_FpgaCut_t * pCutStore; // the temporary cuts -}; - -// priority cut -struct Ivy_FpgaCut_t_ -{ - float Delay; // the delay of the cut - float AreaFlow; // the area flow of the cut - float Area; // the area of the cut - int nLeaves; // the number of leaves - int * pLeaves; // the array of fanins -}; - -// node extension -struct Ivy_FpgaObj_t_ -{ - unsigned Type : 4; // type - unsigned nCuts : 28; // the number of cuts - int Id; // integer ID - int nRefs; // the number of references - Ivy_FpgaObj_t * pFanin0; // the first fanin - Ivy_FpgaObj_t * pFanin1; // the second fanin - float Required; // required time of the onde - Ivy_FpgaCut_t * pCut; // the best cut - Ivy_FpgaCut_t Cuts[0]; // the cuts of the node -}; - - -static Ivy_FpgaMan_t * Ivy_ManFpgaPrepare( Ivy_Man_t * p, int nLutSize, int nCutsMax, int fVerbose ); -static void Ivy_ManFpgaUndo( Ivy_FpgaMan_t * pFpga ); -static void Ivy_ObjFpgaCreate( Ivy_FpgaMan_t * pFpga, int ObjId ); -static void Ivy_ManFpgaDelay( Ivy_FpgaMan_t * pFpga ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Performs FPGA mapping.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_ManFpga( Ivy_Man_t * p, int nLutSize, int nCutsMax, int fVerbose ) -{ - Ivy_FpgaMan_t * pFpga; - pFpga = Ivy_ManFpgaPrepare( p, nLutSize, nCutsMax, fVerbose ); - Ivy_ManFpgaDelay( pFpga ); - Ivy_ManFpgaUndo( pFpga ); -} - -/**Function************************************************************* - - Synopsis [Prepares manager for FPGA mapping.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ivy_FpgaMan_t * Ivy_ManFpgaPrepare( Ivy_Man_t * p, int nLutSize, int nCutsMax, int fVerbose ) -{ - Ivy_FpgaMan_t * pFpga; - Ivy_Obj_t * pObj; - int i; - pFpga = ALLOC( Ivy_FpgaMan_t, 1 ); - memset( pFpga, 0, sizeof(Ivy_FpgaMan_t) ); - // compute the size of the node - pFpga->pManIvy = p; - pFpga->nLutSize = nLutSize; - pFpga->nCutsMax = nCutsMax; - pFpga->fVerbose = fVerbose; - pFpga->nEntrySize = sizeof(Ivy_FpgaObj_t) + (nCutsMax + 1) * (sizeof(Ivy_FpgaCut_t) + sizeof(int) * nLutSize); - pFpga->nEntryBase = sizeof(Ivy_FpgaObj_t) + (nCutsMax + 1) * (sizeof(Ivy_FpgaCut_t)); - pFpga->pManAttr = Attr_ManStartPtrMem( Ivy_ManObjIdMax(p) + 1, pFpga->nEntrySize ); - if ( fVerbose ) - printf( "Entry size = %d. Total memory = %5.2f Mb.\n", pFpga->nEntrySize, - 1.0 * pFpga->nEntrySize * (Ivy_ManObjIdMax(p) + 1) / (1<<20) ); - // connect memory for cuts - Ivy_ManForEachObj( p, pObj, i ) - Ivy_ObjFpgaCreate( pFpga, pObj->Id ); - // create temporary cuts - pFpga->pCutStore = (Ivy_FpgaCut_t *)ALLOC( char, pFpga->nEntrySize * (nCutsMax + 1) * (nCutsMax + 1) ); - memset( pFpga->pCutStore, 0, pFpga->nEntrySize * (nCutsMax + 1) * (nCutsMax + 1) ); - { - int i, * pArrays; - pArrays = (int *)((char *)pFpga->pCutStore + sizeof(Ivy_FpgaCut_t) * (nCutsMax + 1) * (nCutsMax + 1)); - for ( i = 0; i < (nCutsMax + 1) * (nCutsMax + 1); i++ ) - pFpga->pCutStore[i].pLeaves = pArrays + i * pFpga->nLutSize; - } - return pFpga; -} - -/**Function************************************************************* - - Synopsis [Quits the manager for FPGA mapping.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_ManFpgaUndo( Ivy_FpgaMan_t * pFpga ) -{ - Attr_ManStop( pFpga->pManAttr ); - free( pFpga ); -} - - -/**Function************************************************************* - - Synopsis [Prepares the object for FPGA mapping.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_ObjFpgaCreate( Ivy_FpgaMan_t * pFpga, int ObjId ) -{ - Ivy_FpgaObj_t * pObjFpga; - int i, * pArrays; - pObjFpga = Attr_ManReadAttrPtr( pFpga->pManAttr, ObjId ); - pArrays = (int *)((char *)pObjFpga + pFpga->nEntryBase); - for ( i = 0; i <= pFpga->nCutsMax; i++ ) - pObjFpga->Cuts[i].pLeaves = pArrays + i * pFpga->nLutSize; -} - - -/**Function************************************************************* - - Synopsis [Prepares the object for FPGA mapping.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ivy_ObjFpgaMerge( Ivy_FpgaCut_t * pC0, Ivy_FpgaCut_t * pC1, Ivy_FpgaCut_t * pC, int nLimit ) -{ - int i, k, c; - assert( pC0->nLeaves >= pC1->nLeaves ); - // the case of the largest cut sizes - if ( pC0->nLeaves == nLimit && pC1->nLeaves == nLimit ) - { - for ( i = 0; i < pC0->nLeaves; i++ ) - if ( pC0->pLeaves[i] != pC1->pLeaves[i] ) - return 0; - for ( i = 0; i < pC0->nLeaves; i++ ) - pC->pLeaves[i] = pC0->pLeaves[i]; - pC->nLeaves = pC0->nLeaves; - pC->Delay = 1 + IVY_MAX( pC0->Delay, pC1->Delay ); - return 1; - } - // the case when one of the cuts is the largest - if ( pC0->nLeaves == nLimit ) - { - for ( i = 0; i < pC1->nLeaves; i++ ) - { - for ( k = pC0->nLeaves - 1; k >= 0; k-- ) - if ( pC0->pLeaves[k] == pC1->pLeaves[i] ) - break; - if ( k == -1 ) // did not find - return 0; - } - for ( i = 0; i < pC0->nLeaves; i++ ) - pC->pLeaves[i] = pC0->pLeaves[i]; - pC->nLeaves = pC0->nLeaves; - pC->Delay = 1 + IVY_MAX( pC0->Delay, pC1->Delay ); - return 1; - } - - // compare two cuts with different numbers - i = k = 0; - for ( c = 0; c < nLimit; c++ ) - { - if ( k == pC1->nLeaves ) - { - if ( i == pC0->nLeaves ) - { - pC->nLeaves = c; - pC->Delay = 1 + IVY_MAX( pC0->Delay, pC1->Delay ); - return 1; - } - pC->pLeaves[c] = pC0->pLeaves[i++]; - continue; - } - if ( i == pC0->nLeaves ) - { - if ( k == pC1->nLeaves ) - { - pC->nLeaves = c; - pC->Delay = 1 + IVY_MAX( pC0->Delay, pC1->Delay ); - return 1; - } - pC->pLeaves[c] = pC1->pLeaves[k++]; - continue; - } - if ( pC0->pLeaves[i] < pC1->pLeaves[k] ) - { - pC->pLeaves[c] = pC0->pLeaves[i++]; - continue; - } - if ( pC0->pLeaves[i] > pC1->pLeaves[k] ) - { - pC->pLeaves[c] = pC1->pLeaves[k++]; - continue; - } - pC->pLeaves[c] = pC0->pLeaves[i++]; - k++; - } - if ( i < pC0->nLeaves || k < pC1->nLeaves ) - return 0; - pC->nLeaves = c; - pC->Delay = 1 + IVY_MAX( pC0->Delay, pC1->Delay ); - return 1; -} - -/**Function************************************************************* - - Synopsis [Prepares the object for FPGA mapping.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ivy_FpgaCutCompare( Ivy_FpgaCut_t * pC0, Ivy_FpgaCut_t * pC1 ) -{ - if ( pC0->Delay < pC1->Delay ) - return -1; - if ( pC0->Delay > pC1->Delay ) - return 1; - if ( pC0->nLeaves < pC1->nLeaves ) - return -1; - if ( pC0->nLeaves > pC1->nLeaves ) - return 1; - return 0; -} - -/**Function************************************************************* - - Synopsis [Prepares the object for FPGA mapping.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_ObjFpgaDelay( Ivy_FpgaMan_t * pFpga, int ObjId, int Fan0Id, int Fan1Id ) -{ - Ivy_FpgaObj_t * pObjFpga, * pObjFpga0, * pObjFpga1; - int nCuts, i, k; - pObjFpga = Attr_ManReadAttrPtr( pFpga->pManAttr, ObjId ); - pObjFpga0 = Attr_ManReadAttrPtr( pFpga->pManAttr, Fan0Id ); - pObjFpga1 = Attr_ManReadAttrPtr( pFpga->pManAttr, Fan1Id ); - // create cross-product of the cuts - nCuts = 0; - for ( i = 0; pObjFpga0->Cuts[i].nLeaves > 0 && i < pFpga->nCutsMax; i++ ) - for ( k = 0; pObjFpga1->Cuts[k].nLeaves > 0 && k < pFpga->nCutsMax; k++ ) - if ( Ivy_ObjFpgaMerge( pObjFpga0->Cuts + i, pObjFpga1->Cuts + k, pFpga->pCutStore + nCuts, pFpga->nLutSize ) ) - nCuts++; - // sort the cuts - qsort( pFpga->pCutStore, nCuts, sizeof(Ivy_FpgaCut_t), (int (*)(const void *, const void *))Ivy_FpgaCutCompare ); - // take the first - pObjFpga->Cuts[0].nLeaves = 1; - pObjFpga->Cuts[0].pLeaves[0] = ObjId; - pObjFpga->Cuts[0].Delay = pFpga->pCutStore[0].Delay; - pObjFpga->Cuts[1] = pFpga->pCutStore[0]; -} - -/**Function************************************************************* - - Synopsis [Maps the nodes for delay.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ivy_ManFpgaDelay( Ivy_FpgaMan_t * pFpga ) -{ - Ivy_FpgaObj_t * pObjFpga; - Ivy_Obj_t * pObj; - int i, DelayBest; - int clk = clock(); - // set arrival times and trivial cuts at const 1 and PIs - pObjFpga = Attr_ManReadAttrPtr( pFpga->pManAttr, 0 ); - pObjFpga->Cuts[0].nLeaves = 1; - Ivy_ManForEachPi( pFpga->pManIvy, pObj, i ) - { - pObjFpga = Attr_ManReadAttrPtr( pFpga->pManAttr, pObj->Id ); - pObjFpga->Cuts[0].nLeaves = 1; - pObjFpga->Cuts[0].pLeaves[0] = pObj->Id; - } - // map the internal nodes - Ivy_ManForEachNode( pFpga->pManIvy, pObj, i ) - { - Ivy_ObjFpgaDelay( pFpga, pObj->Id, Ivy_ObjFaninId0(pObj), Ivy_ObjFaninId1(pObj) ); - } - // get the best arrival time of the POs - DelayBest = 0; - Ivy_ManForEachPo( pFpga->pManIvy, pObj, i ) - { - pObjFpga = Attr_ManReadAttrPtr( pFpga->pManAttr, Ivy_ObjFanin0(pObj)->Id ); - if ( DelayBest < (int)pObjFpga->Cuts[1].Delay ) - DelayBest = (int)pObjFpga->Cuts[1].Delay; - } - printf( "Best delay = %d. ", DelayBest ); - PRT( "Time", clock() - clk ); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/aig/ivy/ivyIsop.c b/src/aig/ivy/ivyIsop.c deleted file mode 100644 index ae48ca34..00000000 --- a/src/aig/ivy/ivyIsop.c +++ /dev/null @@ -1,327 +0,0 @@ -/**CFile**************************************************************** - - FileName [ivyIsop.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [And-Inverter Graph package.] - - Synopsis [Computing irredundant SOP using truth table.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - May 11, 2006.] - - Revision [$Id: ivyIsop.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "ivy.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -// ISOP computation fails if intermediate memory usage exceed this limit -#define IVY_ISOP_MEM_LIMIT 16*4096 - -// intermediate ISOP representation -typedef struct Ivy_Sop_t_ Ivy_Sop_t; -struct Ivy_Sop_t_ -{ - unsigned * pCubes; - int nCubes; -}; - -// static procedures to compute ISOP -static unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore ); -static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Computes ISOP from TT.] - - Description [Returns the cover in vCover. Uses the rest of array in vCover - as an intermediate memory storage. Returns the cover with -1 cubes, if the - the computation exceeded the memory limit (IVY_ISOP_MEM_LIMIT words of - intermediate data).] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth ) -{ - Ivy_Sop_t cRes, * pcRes = &cRes; - Ivy_Sop_t cRes2, * pcRes2 = &cRes2; - unsigned * pResult; - int RetValue = 0; - assert( nVars >= 0 && nVars < 16 ); - // if nVars < 5, make sure it does not depend on those vars -// for ( i = nVars; i < 5; i++ ) -// assert( !Extra_TruthVarInSupport(puTruth, 5, i) ); - // prepare memory manager - Vec_IntClear( vCover ); - Vec_IntGrow( vCover, IVY_ISOP_MEM_LIMIT ); - // compute ISOP for the direct polarity - pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes, vCover ); - if ( pcRes->nCubes == -1 ) - { - vCover->nSize = -1; - return 0; - } - assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) ); - if ( fTryBoth ) - { - // compute ISOP for the complemented polarity - Extra_TruthNot( puTruth, puTruth, nVars ); - pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes2, vCover ); - if ( pcRes2->nCubes >= 0 ) - { - assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) ); - if ( pcRes->nCubes > pcRes2->nCubes ) - { - RetValue = 1; - pcRes = pcRes2; - } - } - Extra_TruthNot( puTruth, puTruth, nVars ); - } -// printf( "%d ", vCover->nSize ); - // move the cover representation to the beginning of the memory buffer - memmove( vCover->pArray, pcRes->pCubes, pcRes->nCubes * sizeof(unsigned) ); - Vec_IntShrink( vCover, pcRes->nCubes ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Computes ISOP 6 variables or more.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore ) -{ - Ivy_Sop_t cRes0, cRes1, cRes2; - Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2; - unsigned * puRes0, * puRes1, * puRes2; - unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp, * pTemp0, * pTemp1; - int i, k, Var, nWords, nWordsAll; -// assert( Extra_TruthIsImply( puOn, puOnDc, nVars ) ); - // allocate room for the resulting truth table - nWordsAll = Extra_TruthWordNum( nVars ); - pTemp = Vec_IntFetch( vStore, nWordsAll ); - if ( pTemp == NULL ) - { - pcRes->nCubes = -1; - return NULL; - } - // check for constants - if ( Extra_TruthIsConst0( puOn, nVars ) ) - { - pcRes->nCubes = 0; - pcRes->pCubes = NULL; - Extra_TruthClear( pTemp, nVars ); - return pTemp; - } - if ( Extra_TruthIsConst1( puOnDc, nVars ) ) - { - pcRes->nCubes = 1; - pcRes->pCubes = Vec_IntFetch( vStore, 1 ); - if ( pcRes->pCubes == NULL ) - { - pcRes->nCubes = -1; - return NULL; - } - pcRes->pCubes[0] = 0; - Extra_TruthFill( pTemp, nVars ); - return pTemp; - } - assert( nVars > 0 ); - // find the topmost var - for ( Var = nVars-1; Var >= 0; Var-- ) - if ( Extra_TruthVarInSupport( puOn, nVars, Var ) || - Extra_TruthVarInSupport( puOnDc, nVars, Var ) ) - break; - assert( Var >= 0 ); - // consider a simple case when one-word computation can be used - if ( Var < 5 ) - { - unsigned uRes = Ivy_TruthIsop5_rec( puOn[0], puOnDc[0], Var+1, pcRes, vStore ); - for ( i = 0; i < nWordsAll; i++ ) - pTemp[i] = uRes; - return pTemp; - } - assert( Var >= 5 ); - nWords = Extra_TruthWordNum( Var ); - // cofactor - puOn0 = puOn; puOn1 = puOn + nWords; - puOnDc0 = puOnDc; puOnDc1 = puOnDc + nWords; - pTemp0 = pTemp; pTemp1 = pTemp + nWords; - // solve for cofactors - Extra_TruthSharp( pTemp0, puOn0, puOnDc1, Var ); - puRes0 = Ivy_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0, vStore ); - if ( pcRes0->nCubes == -1 ) - { - pcRes->nCubes = -1; - return NULL; - } - Extra_TruthSharp( pTemp1, puOn1, puOnDc0, Var ); - puRes1 = Ivy_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1, vStore ); - if ( pcRes1->nCubes == -1 ) - { - pcRes->nCubes = -1; - return NULL; - } - Extra_TruthSharp( pTemp0, puOn0, puRes0, Var ); - Extra_TruthSharp( pTemp1, puOn1, puRes1, Var ); - Extra_TruthOr( pTemp0, pTemp0, pTemp1, Var ); - Extra_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var ); - puRes2 = Ivy_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2, vStore ); - if ( pcRes2->nCubes == -1 ) - { - pcRes->nCubes = -1; - return NULL; - } - // create the resulting cover - pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes; - pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes ); - if ( pcRes->pCubes == NULL ) - { - pcRes->nCubes = -1; - return NULL; - } - k = 0; - for ( i = 0; i < pcRes0->nCubes; i++ ) - pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1)); - for ( i = 0; i < pcRes1->nCubes; i++ ) - pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+0)); - for ( i = 0; i < pcRes2->nCubes; i++ ) - pcRes->pCubes[k++] = pcRes2->pCubes[i]; - assert( k == pcRes->nCubes ); - // create the resulting truth table - Extra_TruthOr( pTemp0, puRes0, puRes2, Var ); - Extra_TruthOr( pTemp1, puRes1, puRes2, Var ); - // copy the table if needed - nWords <<= 1; - for ( i = 1; i < nWordsAll/nWords; i++ ) - for ( k = 0; k < nWords; k++ ) - pTemp[i*nWords + k] = pTemp[k]; - // verify in the end -// assert( Extra_TruthIsImply( puOn, pTemp, nVars ) ); -// assert( Extra_TruthIsImply( pTemp, puOnDc, nVars ) ); - return pTemp; -} - -/**Function************************************************************* - - Synopsis [Computes ISOP for 5 variables or less.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore ) -{ - unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; - Ivy_Sop_t cRes0, cRes1, cRes2; - Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2; - unsigned uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2; - int i, k, Var; - assert( nVars <= 5 ); - assert( (uOn & ~uOnDc) == 0 ); - if ( uOn == 0 ) - { - pcRes->nCubes = 0; - pcRes->pCubes = NULL; - return 0; - } - if ( uOnDc == 0xFFFFFFFF ) - { - pcRes->nCubes = 1; - pcRes->pCubes = Vec_IntFetch( vStore, 1 ); - if ( pcRes->pCubes == NULL ) - { - pcRes->nCubes = -1; - return 0; - } - pcRes->pCubes[0] = 0; - return 0xFFFFFFFF; - } - assert( nVars > 0 ); - // find the topmost var - for ( Var = nVars-1; Var >= 0; Var-- ) - if ( Extra_TruthVarInSupport( &uOn, 5, Var ) || - Extra_TruthVarInSupport( &uOnDc, 5, Var ) ) - break; - assert( Var >= 0 ); - // cofactor - uOn0 = uOn1 = uOn; - uOnDc0 = uOnDc1 = uOnDc; - Extra_TruthCofactor0( &uOn0, Var + 1, Var ); - Extra_TruthCofactor1( &uOn1, Var + 1, Var ); - Extra_TruthCofactor0( &uOnDc0, Var + 1, Var ); - Extra_TruthCofactor1( &uOnDc1, Var + 1, Var ); - // solve for cofactors - uRes0 = Ivy_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0, vStore ); - if ( pcRes0->nCubes == -1 ) - { - pcRes->nCubes = -1; - return 0; - } - uRes1 = Ivy_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var, pcRes1, vStore ); - if ( pcRes1->nCubes == -1 ) - { - pcRes->nCubes = -1; - return 0; - } - uRes2 = Ivy_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pcRes2, vStore ); - if ( pcRes2->nCubes == -1 ) - { - pcRes->nCubes = -1; - return 0; - } - // create the resulting cover - pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes; - pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes ); - if ( pcRes->pCubes == NULL ) - { - pcRes->nCubes = -1; - return 0; - } - k = 0; - for ( i = 0; i < pcRes0->nCubes; i++ ) - pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1)); - for ( i = 0; i < pcRes1->nCubes; i++ ) - pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+0)); - for ( i = 0; i < pcRes2->nCubes; i++ ) - pcRes->pCubes[k++] = pcRes2->pCubes[i]; - assert( k == pcRes->nCubes ); - // derive the final truth table - uRes2 |= (uRes0 & ~uMasks[Var]) | (uRes1 & uMasks[Var]); -// assert( (uOn & ~uRes2) == 0 ); -// assert( (uRes2 & ~uOnDc) == 0 ); - return uRes2; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/aig/ivy/module.make b/src/aig/ivy/module.make index c1f7d1b8..daef43df 100644 --- a/src/aig/ivy/module.make +++ b/src/aig/ivy/module.make @@ -9,7 +9,6 @@ SRC += src/aig/ivy/ivyBalance.c \ src/aig/ivy/ivyFastMap.c \ src/aig/ivy/ivyFraig.c \ src/aig/ivy/ivyHaig.c \ - src/aig/ivy/ivyIsop.c \ src/aig/ivy/ivyMan.c \ src/aig/ivy/ivyMem.c \ src/aig/ivy/ivyMulti.c \ |