diff options
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | abc.dsp | 12 | ||||
| -rw-r--r-- | src/aig/aig-alan.tar.gz | bin | 27265 -> 0 bytes | |||
| -rw-r--r-- | src/aig/ivy/ivyFactor.c | 833 | ||||
| -rw-r--r-- | src/aig/rwt/module.make | 6 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 30 | ||||
| -rw-r--r-- | src/base/abci/abcIf.c | 7 | ||||
| -rw-r--r-- | src/base/abci/abcPrint.c | 9 | ||||
| -rw-r--r-- | src/map/fpga/fpga.c | 4 | ||||
| -rw-r--r-- | src/map/if/if.h | 44 | ||||
| -rw-r--r-- | src/map/if/ifCore.c | 41 | ||||
| -rw-r--r-- | src/map/if/ifMan.c | 9 | ||||
| -rw-r--r-- | src/map/if/ifMap.c | 223 | ||||
| -rw-r--r-- | src/map/if/ifReduce.c | 576 | ||||
| -rw-r--r-- | src/map/if/ifSelect.c | 175 | ||||
| -rw-r--r-- | src/map/if/ifSeq.c | 170 | ||||
| -rw-r--r-- | src/map/if/module.make | 4 | ||||
| -rw-r--r-- | src/sat/fraig/fraigMan.c | 3 |
18 files changed, 2060 insertions, 90 deletions
@@ -7,9 +7,9 @@ CP := cp PROG := abc MODULES := src/base/abc src/base/abci src/base/cmd src/base/io src/base/main src/base/ver \ - src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco src/mem/deco src/aig/ec \ + src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco src/aig/mem src/aig/ec \ src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr src/bdd/parse src/bdd/reo \ - src/map/fpga src/map/pga src/map/mapper src/map/mio src/map/super src/map/if \ + src/map/fpga src/map/mapper src/map/mio src/map/super src/map/if \ src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/espresso src/misc/nm src/misc/vec src/misc/hash \ src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/sim src/opt/ret \ src/sat/asat src/sat/bsat src/sat/csat src/sat/msat src/sat/fraig @@ -1826,6 +1826,18 @@ SOURCE=.\src\map\if\ifMap.c # End Source File # Begin Source File +SOURCE=.\src\map\if\ifReduce.c +# End Source File +# Begin Source File + +SOURCE=.\src\map\if\ifSelect.c +# End Source File +# Begin Source File + +SOURCE=.\src\map\if\ifSeq.c +# End Source File +# Begin Source File + SOURCE=.\src\map\if\ifUtil.c # End Source File # End Group diff --git a/src/aig/aig-alan.tar.gz b/src/aig/aig-alan.tar.gz Binary files differdeleted file mode 100644 index b61827ad..00000000 --- a/src/aig/aig-alan.tar.gz +++ /dev/null diff --git a/src/aig/ivy/ivyFactor.c b/src/aig/ivy/ivyFactor.c new file mode 100644 index 00000000..d8323931 --- /dev/null +++ b/src/aig/ivy/ivyFactor.c @@ -0,0 +1,833 @@ +/**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 /// +//////////////////////////////////////////////////////////////////////// + +extern Dec_Edge_t Dec_Factor32_rec( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars ); +extern Dec_Edge_t Dec_Factor32LF_rec( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars, Vec_Int_t * vSimple ); +extern Dec_Edge_t Dec_Factor32Trivial( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars ); +extern Dec_Edge_t Dec_Factor32TrivialCube( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars, Mvc_Cube_t * pCube, Vec_Int_t * vEdgeLits ); +extern Dec_Edge_t Dec_Factor32TrivialTree_rec( Dec_Graph_t * pFForm, Dec_Edge_t * peNodes, int nNodes, int fNodeOr ); +extern Vec_Int_t * Dec_Factor32Divisor( Vec_Int_t * vCover, int nVars ); +extern void Dec_Factor32DivisorZeroKernel( Vec_Int_t * vCover, int nVars ); +extern int Dec_Factor32WorstLiteral( Vec_Int_t * vCover, int nVars ); + +extern Vec_Int_t * Mvc_CoverCommonCubeCover( Vec_Int_t * vCover ); + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Factors the cover.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Dec_Factor32( Vec_Int_t * vCover, int nVars ) +{ + Dec_Graph_t * pFForm; + Dec_Edge_t eRoot; + + // check for trivial functions + if ( Vec_IntSize(vCover) == 0 ) + return Dec_GraphCreateConst0(); + if ( Vec_IntSize(vCover) == 1 && /* tautology */ ) + return Dec_GraphCreateConst1(); + + // perform CST + Mvc_CoverInverse( vCover ); // CST + // start the factored form + pFForm = Dec_GraphCreate( Abc_SopGetVarNum(pSop) ); + // factor the cover + eRoot = Dec_Factor32_rec( pFForm, vCover, nVars ); + // finalize the factored form + Dec_GraphSetRoot( pFForm, eRoot ); + // verify the factored form +// if ( !Dec_Factor32Verify( pSop, pFForm ) ) +// printf( "Verification has failed.\n" ); +// Mvc_CoverInverse( vCover ); // undo CST + return pFForm; +} + +/**Function************************************************************* + + Synopsis [Internal recursive factoring procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Edge_t Dec_Factor32_rec( Dec_Graph_t * pFForm, Vec_Int_t * vCover, int nVars ) +{ + Vec_Int_t * vDiv, * vQuo, * vRem, * vCom; + Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem; + Dec_Edge_t eNodeAnd, eNode; + + // make sure the cover contains some cubes + assert( Vec_IntSize(vCover) ); + + // get the divisor + vDiv = Dec_Factor32Divisor( vCover, nVars ); + if ( vDiv == NULL ) + return Dec_Factor32Trivial( pFForm, vCover, nVars ); + + // divide the cover by the divisor + Mvc_CoverDivideInternal( vCover, nVars, vDiv, &vQuo, &vRem ); + assert( Vec_IntSize(vQuo) ); + + Vec_IntFree( vDiv ); + Vec_IntFree( vRem ); + + // check the trivial case + if ( Vec_IntSize(vQuo) == 1 ) + { + eNode = Dec_Factor32LF_rec( pFForm, vCover, nVars, vQuo ); + Vec_IntFree( vQuo ); + return eNode; + } + + // make the quotient cube free + Mvc_CoverMakeCubeFree( vQuo ); + + // divide the cover by the quotient + Mvc_CoverDivideInternal( vCover, nVars, vQuo, &vDiv, &vRem ); + + // check the trivial case + if ( Mvc_CoverIsCubeFree( vDiv ) ) + { + eNodeDiv = Dec_Factor32_rec( pFForm, vDiv ); + eNodeQuo = Dec_Factor32_rec( pFForm, vQuo ); + Vec_IntFree( vDiv ); + 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 = Mvc_CoverCommonCubeCover( vDiv ); + Vec_IntFree( vDiv ); + Vec_IntFree( vQuo ); + Vec_IntFree( vRem ); + + // solve the simple problem + eNode = Dec_Factor32LF_rec( pFForm, vCover, nVars, 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 * vCover, int nVars, Vec_Int_t * vSimple ) +{ + Dec_Man_t * pManDec = Abc_FrameReadManDec(); + Vec_Int_t * vEdgeLits = pManDec->vLits; + Vec_Int_t * vDiv, * vQuo, * vRem; + Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem; + Dec_Edge_t eNodeAnd; + + // get the most often occurring literal + vDiv = Mvc_CoverBestLiteralCover( vCover, nVars, vSimple ); + // divide the cover by the literal + Mvc_CoverDivideByLiteral( vCover, nVars, vDiv, &vQuo, &vRem ); + // get the node pointer for the literal + eNodeDiv = Dec_Factor32TrivialCube( pFForm, vDiv, Mvc_CoverReadCubeHead(vDiv), vEdgeLits ); + Vec_IntFree( vDiv ); + // 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 * vCover, int nVars ) +{ + 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; + Mvc_Cube_t * pCube; + int i; + // create the factored form for each cube + Vec_IntClear( vEdgeCubes ); + Mvc_CoverForEachCube( vCover, pCube ) + { + eNode = Dec_Factor32TrivialCube( pFForm, vCover, nVars, pCube, 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 * vCover, Mvc_Cube_t * pCube, int nVars, Vec_Int_t * vEdgeLits ) +{ + Dec_Edge_t eNode; + int iBit, Value; + // create the factored form for each literal + Vec_IntClear( vEdgeLits ); + Mvc_CubeForEachBit( vCover, pCube, 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 ); +} + +/**Function************************************************************* + + Synopsis [Returns the quick divisor of the cover.] + + Description [Returns NULL, if there is not divisor other than + trivial.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Dec_Factor32Divisor( Vec_Int_t * vCover, int nVars ) +{ + Vec_Int_t * pKernel; + if ( Vec_IntSize(vCover) <= 1 ) + return NULL; + // allocate the literal array and count literals + if ( Mvc_CoverAnyLiteral( vCover, NULL ) == -1 ) + return NULL; + // duplicate the cover + pKernel = Mvc_CoverDup(vCover); + // perform the kerneling + Dec_Factor32DivisorZeroKernel( pKernel ); + assert( Vec_IntSize(pKernel) ); + return pKernel; +} + +/**Function************************************************************* + + Synopsis [Computes a level-zero kernel.] + + Description [Modifies the cover to contain one level-zero kernel.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dec_Factor32DivisorZeroKernel( Vec_Int_t * vCover, int nVars ) +{ + int iLit; + // find any literal that occurs at least two times +// iLit = Mvc_CoverAnyLiteral( vCover, NULL ); + iLit = Dec_Factor32WorstLiteral( vCover, NULL ); +// iLit = Mvc_CoverBestLiteral( vCover, NULL ); + if ( iLit == -1 ) + return; + // derive the cube-free quotient + Mvc_CoverDivideByLiteralQuo( vCover, iLit ); // the same cover + Mvc_CoverMakeCubeFree( vCover ); // the same cover + // call recursively + Dec_Factor32DivisorZeroKernel( vCover ); // the same cover +} + +/**Function************************************************************* + + Synopsis [Find the most often occurring literal.] + + Description [Find the most often occurring literal among those + that occur more than once.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dec_Factor32WorstLiteral( Vec_Int_t * vCover, int nVars ) +{ + Mvc_Cube_t * pCube; + int nWord, nBit; + int i, iMin, nLitsMin, nLitsCur; + int fUseFirst = 1; + + // go through each literal + iMin = -1; + nLitsMin = 1000000; + for ( i = 0; i < vCover->nBits; i++ ) + { + // get the word and bit of this literal + nWord = Mvc_CubeWhichWord(i); + nBit = Mvc_CubeWhichBit(i); + // go through all the cubes + nLitsCur = 0; + Mvc_CoverForEachCube( vCover, pCube ) + if ( pCube->pData[nWord] & (1<<nBit) ) + 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 [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Mvc_CoverCommonCubeCover( Vec_Int_t * vCover ) +{ + Vec_Int_t * vRes; + unsigned uTemp, uCube; + int i; + uCube = ~(unsigned)0; + Vec_IntForEachEntry( vCover, uTemp, i ) + uCube &= uTemp; + vRes = Vec_IntAlloc( 1 ); + Vec_IntPush( vRes, uCube ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the support of cover2 is contained in the support of cover1.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mvc_CoverCheckSuppContainment( Vec_Int_t * vCover1, Vec_Int_t * vCover2 ) +{ + unsigned uTemp, uSupp1, uSupp2; + int i; + // set the supports + uSupp1 = 0; + Vec_IntForEachEntry( vCover1, uTemp, i ) + uSupp1 |= uTemp; + uSupp2 = 0; + Vec_IntForEachEntry( vCover2, uTemp, i ) + uSupp2 |= uTemp; + // return containment + return uSupp1 & !uSupp2; +// Mvc_CubeBitNotImpl( Result, vCover2->pMask, vCover1->pMask ); +// return !Result; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mvc_CoverDivide( Vec_Int_t * vCover, Vec_Int_t * vDiv, Vec_Int_t ** pvQuo, Vec_Int_t ** pvRem ) +{ + // check the number of cubes + if ( Vec_IntSize( vCover ) < Vec_IntSize( vDiv ) ) + { + *pvQuo = NULL; + *pvRem = NULL; + return; + } + + // make sure that support of vCover contains that of vDiv + if ( !Mvc_CoverCheckSuppContainment( vCover, vDiv ) ) + { + *pvQuo = NULL; + *pvRem = NULL; + return; + } + + // perform the general division + Mvc_CoverDivideInternal( vCover, vDiv, pvQuo, pvRem ); +} + + +/**Function************************************************************* + + Synopsis [Merge the cubes inside the groups.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mvc_CoverDivideInternal( Vec_Int_t * vCover, Vec_Int_t * vDiv, Vec_Int_t ** pvQuo, Vec_Int_t ** pvRem ) +{ + Vec_Int_t * vQuo, * vRem; + Mvc_Cube_t * pCubeC, * pCubeD, * pCubeCopy; + Mvc_Cube_t * pCube1, * pCube2; + int * pGroups, nGroups; // the cube groups + int nCubesC, nCubesD, nMerges, iCubeC, iCubeD, iMerge; + int fSkipG, GroupSize, g, c, RetValue; + int nCubes; + + // get cover sizes + nCubesD = Vec_IntSize( vDiv ); + nCubesC = Vec_IntSize( vCover ); + + // check trivial cases + if ( nCubesD == 1 ) + { + if ( Mvc_CoverIsOneLiteral( vDiv ) ) + Mvc_CoverDivideByLiteral( vCover, vDiv, pvQuo, pvRem ); + else + Mvc_CoverDivideByCube( vCover, vDiv, pvQuo, pvRem ); + return; + } + + // create the divisor and the remainder + vQuo = Mvc_CoverAlloc( vCover->pMem, vCover->nBits ); + vRem = Mvc_CoverAlloc( vCover->pMem, vCover->nBits ); + + // get the support of the divisor + Mvc_CoverAllocateMask( vDiv ); + Mvc_CoverSupport( vDiv, vDiv->pMask ); + + // sort the cubes of the divisor + Mvc_CoverSort( vDiv, NULL, Mvc_CubeCompareInt ); + // sort the cubes of the cover + Mvc_CoverSort( vCover, vDiv->pMask, Mvc_CubeCompareIntOutsideAndUnderMask ); + + // allocate storage for cube groups + pGroups = MEM_ALLOC( vCover->pMem, int, nCubesC + 1 ); + + // mask contains variables in the support of Div + // split the cubes into groups using the mask + Mvc_CoverList2Array( vCover ); + Mvc_CoverList2Array( vDiv ); + pGroups[0] = 0; + nGroups = 1; + for ( c = 1; c < nCubesC; c++ ) + { + // get the cubes + pCube1 = vCover->pCubes[c-1]; + pCube2 = vCover->pCubes[c ]; + // compare the cubes + Mvc_CubeBitEqualOutsideMask( RetValue, pCube1, pCube2, vDiv->pMask ); + if ( !RetValue ) + pGroups[nGroups++] = c; + } + // finish off the last group + pGroups[nGroups] = nCubesC; + + // consider each group separately and decide + // whether it can produce a quotient cube + nCubes = 0; + for ( g = 0; g < nGroups; g++ ) + { + // if the group has less than nCubesD cubes, + // there is no way it can produce the quotient cube + // copy the cubes to the remainder + GroupSize = pGroups[g+1] - pGroups[g]; + if ( GroupSize < nCubesD ) + { + for ( c = pGroups[g]; c < pGroups[g+1]; c++ ) + { + pCubeCopy = Mvc_CubeDup( vRem, vCover->pCubes[c] ); + Mvc_CoverAddCubeTail( vRem, pCubeCopy ); + nCubes++; + } + continue; + } + + // mark the cubes as those that should be added to the remainder + for ( c = pGroups[g]; c < pGroups[g+1]; c++ ) + Mvc_CubeSetSize( vCover->pCubes[c], 1 ); + + // go through the cubes in the group and at the same time + // go through the cubes in the divisor + iCubeD = 0; + iCubeC = 0; + pCubeD = vDiv->pCubes[iCubeD++]; + pCubeC = vCover->pCubes[pGroups[g]+iCubeC++]; + fSkipG = 0; + nMerges = 0; + + while ( 1 ) + { + // compare the topmost cubes in F and in D + RetValue = Mvc_CubeCompareIntUnderMask( pCubeC, pCubeD, vDiv->pMask ); + // cube are ordered in increasing order of their int value + if ( RetValue == -1 ) // pCubeC is above pCubeD + { // cube in C should be added to the remainder + // check that there is enough cubes in the group + if ( GroupSize - iCubeC < nCubesD - nMerges ) + { + fSkipG = 1; + break; + } + // get the next cube in the cover + pCubeC = vCover->pCubes[pGroups[g]+iCubeC++]; + continue; + } + if ( RetValue == 1 ) // pCubeD is above pCubeC + { // given cube in D does not have a corresponding cube in the cover + fSkipG = 1; + break; + } + // mark the cube as the one that should NOT be added to the remainder + Mvc_CubeSetSize( pCubeC, 0 ); + // remember this merged cube + iMerge = iCubeC-1; + nMerges++; + + // stop if we considered the last cube of the group + if ( iCubeD == nCubesD ) + break; + + // advance the cube of the divisor + assert( iCubeD < nCubesD ); + pCubeD = vDiv->pCubes[iCubeD++]; + + // advance the cube of the group + assert( pGroups[g]+iCubeC < nCubesC ); + pCubeC = vCover->pCubes[pGroups[g]+iCubeC++]; + } + + if ( fSkipG ) + { + // the group has failed, add all the cubes to the remainder + for ( c = pGroups[g]; c < pGroups[g+1]; c++ ) + { + pCubeCopy = Mvc_CubeDup( vRem, vCover->pCubes[c] ); + Mvc_CoverAddCubeTail( vRem, pCubeCopy ); + nCubes++; + } + continue; + } + + // the group has worked, add left-over cubes to the remainder + for ( c = pGroups[g]; c < pGroups[g+1]; c++ ) + { + pCubeC = vCover->pCubes[c]; + if ( Mvc_CubeReadSize(pCubeC) ) + { + pCubeCopy = Mvc_CubeDup( vRem, pCubeC ); + Mvc_CoverAddCubeTail( vRem, pCubeCopy ); + nCubes++; + } + } + + // create the quotient cube + pCube1 = Mvc_CubeAlloc( vQuo ); + Mvc_CubeBitSharp( pCube1, vCover->pCubes[pGroups[g]+iMerge], vDiv->pMask ); + // add the cube to the quotient + Mvc_CoverAddCubeTail( vQuo, pCube1 ); + nCubes += nCubesD; + } + assert( nCubes == nCubesC ); + + // deallocate the memory + MEM_FREE( vCover->pMem, int, nCubesC + 1, pGroups ); + + // return the results + *pvRem = vRem; + *pvQuo = vQuo; +// Mvc_CoverVerifyDivision( vCover, vDiv, vQuo, vRem ); +} + + +/**Function************************************************************* + + Synopsis [Divides the cover by a cube.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mvc_CoverDivideByCube( Vec_Int_t * vCover, Vec_Int_t * vDiv, Vec_Int_t ** pvQuo, Vec_Int_t ** pvRem ) +{ + Vec_Int_t * vQuo, * vRem; + Mvc_Cube_t * pCubeC, * pCubeD, * pCubeCopy; + int ComvResult; + + // get the only cube of D + assert( Vec_IntSize(vDiv) == 1 ); + + // start the quotient and the remainder + vQuo = Mvc_CoverAlloc( vCover->pMem, vCover->nBits ); + vRem = Mvc_CoverAlloc( vCover->pMem, vCover->nBits ); + + // get the first and only cube of the divisor + pCubeD = Mvc_CoverReadCubeHead( vDiv ); + + // iterate through the cubes in the cover + Mvc_CoverForEachCube( vCover, pCubeC ) + { + // check the containment of literals from pCubeD in pCube + Mvc_Cube2BitNotImpl( ComvResult, pCubeD, pCubeC ); + if ( !ComvResult ) + { // this cube belongs to the quotient + // alloc the cube + pCubeCopy = Mvc_CubeAlloc( vQuo ); + // clean the support of D + Mvc_CubeBitSharp( pCubeCopy, pCubeC, pCubeD ); + // add the cube to the quotient + Mvc_CoverAddCubeTail( vQuo, pCubeCopy ); + } + else + { + // copy the cube + pCubeCopy = Mvc_CubeDup( vRem, pCubeC ); + // add the cube to the remainder + Mvc_CoverAddCubeTail( vRem, pCubeCopy ); + } + } + // return the results + *pvRem = vRem; + *pvQuo = vQuo; +} + +/**Function************************************************************* + + Synopsis [Divides the cover by a literal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mvc_CoverDivideByLiteral( Vec_Int_t * vCover, Vec_Int_t * vDiv, Vec_Int_t ** pvQuo, Vec_Int_t ** pvRem ) +{ + Vec_Int_t * vQuo, * vRem; + Mvc_Cube_t * pCubeC, * pCubeCopy; + int iLit; + + // get the only cube of D + assert( Vec_IntSize(vDiv) == 1 ); + + // start the quotient and the remainder + vQuo = Mvc_CoverAlloc( vCover->pMem, vCover->nBits ); + vRem = Mvc_CoverAlloc( vCover->pMem, vCover->nBits ); + + // get the first and only literal in the divisor cube + iLit = Mvc_CoverFirstCubeFirstLit( vDiv ); + + // iterate through the cubes in the cover + Mvc_CoverForEachCube( vCover, pCubeC ) + { + // copy the cube + pCubeCopy = Mvc_CubeDup( vCover, pCubeC ); + // add the cube to the quotient or to the remainder depending on the literal + if ( Mvc_CubeBitValue( pCubeCopy, iLit ) ) + { // remove the literal + Mvc_CubeBitRemove( pCubeCopy, iLit ); + // add the cube ot the quotient + Mvc_CoverAddCubeTail( vQuo, pCubeCopy ); + } + else + { // add the cube ot the remainder + Mvc_CoverAddCubeTail( vRem, pCubeCopy ); + } + } + // return the results + *pvRem = vRem; + *pvQuo = vQuo; +} + + +/**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 Mvc_CoverDivideByLiteralQuo( Vec_Int_t * vCover, int iLit ) +{ + Mvc_Cube_t * pCube, * pCube2, * pPrev; + // delete those cubes that do not have this literal + // remove this literal from other cubes + pPrev = NULL; + Mvc_CoverForEachCubeSafe( vCover, pCube, pCube2 ) + { + if ( Mvc_CubeBitValue( pCube, iLit ) == 0 ) + { // delete the cube from the cover + Mvc_CoverDeleteCube( vCover, pPrev, pCube ); + Mvc_CubeFree( vCover, pCube ); + // don't update the previous cube + } + else + { // delete this literal from the cube + Mvc_CubeBitRemove( pCube, iLit ); + // update the previous cube + pPrev = pCube; + } + } +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/rwt/module.make b/src/aig/rwt/module.make index 2852f2ba..439d576f 100644 --- a/src/aig/rwt/module.make +++ b/src/aig/rwt/module.make @@ -1,3 +1,3 @@ -SRC += src/hop/rwt/rwtDec.c \ - src/hop/rwt/rwtMan.c \ - src/hop/rwt/rwtUtil.c +SRC += src/aig/rwt/rwtDec.c \ + src/aig/rwt/rwtMan.c \ + src/aig/rwt/rwtUtil.c diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 4164f67a..dbbe9d7e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7090,7 +7090,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) fRecovery = 1; fSwitching = 0; fLatchPaths = 0; - fVerbose = 1; + fVerbose = 0; DelayTarget =-1; nLutSize =-1; Extra_UtilGetoptReset(); @@ -7392,18 +7392,20 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults memset( pPars, 0, sizeof(If_Par_t) ); pPars->Mode = 0; - pPars->nLutSize = 5; + pPars->nLutSize = 4; // pPars->pLutLib = Abc_FrameReadLibLut(); - pPars->nCutsMax = 10; + pPars->nCutsMax = 20; + pPars->fPreprocess = 1; pPars->fArea = 0; pPars->fFancy = 0; pPars->fLatchPaths = 0; + pPars->fExpRed = 1; pPars->fSeq = 0; pPars->nLatches = 0; pPars->DelayTarget = -1; - pPars->fVerbose = 1; + pPars->fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "MKCDaflsvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "MKCDpaflrsvh" ) ) != EOF ) { switch ( c ) { @@ -7451,6 +7453,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->DelayTarget <= 0.0 ) goto usage; break; + case 'p': + pPars->fPreprocess ^= 1; + break; case 'a': pPars->fArea ^= 1; break; @@ -7460,6 +7465,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'l': pPars->fLatchPaths ^= 1; break; + case 'r': + pPars->fExpRed ^= 1; + break; case 's': pPars->fSeq ^= 1; break; @@ -7478,6 +7486,12 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } + if ( pPars->fSeq ) + { + fprintf( pErr, "Sequential mapping is currently being implemented.\n" ); + goto usage; + } + if ( pPars->Mode < 0 || pPars->Mode > 4 ) { fprintf( pErr, "Incorrect mapping mode.\n" ); @@ -7547,7 +7561,7 @@ usage: sprintf( LutSize, "library" ); else sprintf( LutSize, "%d", pPars->nLutSize ); - fprintf( pErr, "usage: if [-M num] [-K num] [-C num] [-D float] [-aflsvh]\n" ); + fprintf( pErr, "usage: if [-M num] [-K num] [-C num] [-D float] [-pafrsvh]\n" ); fprintf( pErr, "\t performs FPGA mapping of the network as follows:\n" ); fprintf( pErr, "\t 1 - delay only\n" ); fprintf( pErr, "\t 2 - area only\n" ); @@ -7557,9 +7571,11 @@ usage: fprintf( pErr, "\t-K num : the number of LUT inputs (2 < num < 32) [default = %s]\n", LutSize ); fprintf( pErr, "\t-C num : the max number of cuts to use (1 < num < 2^12) [default = %d]\n", pPars->nCutsMax ); fprintf( pErr, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer ); + fprintf( pErr, "\t-p : toggles preprocessing using several starting points [default = %s]\n", pPars->fPreprocess? "yes": "no" ); fprintf( pErr, "\t-a : toggles area-oriented mapping [default = %s]\n", pPars->fArea? "yes": "no" ); fprintf( pErr, "\t-f : toggles one fancy feature [default = %s]\n", pPars->fFancy? "yes": "no" ); - fprintf( pErr, "\t-l : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" ); +// fprintf( pErr, "\t-l : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" ); + fprintf( pErr, "\t-r : enables expansion/reduction of the best cuts [default = %s]\n", pPars->fExpRed? "yes": "no" ); fprintf( pErr, "\t-s : toggles sequential mapping [default = %s]\n", pPars->fSeq? "yes": "no" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : prints the command usage\n"); diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c index 70971952..704c8ebb 100644 --- a/src/base/abci/abcIf.c +++ b/src/base/abci/abcIf.c @@ -55,7 +55,11 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars ) // print a warning about choice nodes if ( Abc_NtkGetChoiceNum( pNtk ) ) - printf( "Performing FPGA mapping with choices.\n" ); + { +// printf( "Performing FPGA mapping with choices.\n" ); + printf( "Currently mapping with choices is not enabled.\n" ); + return NULL; + } // get timing information pPars->pTimesArr = Abc_NtkGetCiArrivalFloats(pNtk); @@ -223,7 +227,6 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t return pNodeNew; } - /**Function************************************************************* Synopsis [Recursively derives the truth table for the cut.] diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index 40bf30a6..002a885c 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -148,18 +148,18 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) // print the statistic into a file { FILE * pTable; - pTable = fopen( "fpga/fpga_stats.txt", "a+" ); + pTable = fopen( "a/fpga_stats.txt", "a+" ); fprintf( pTable, "%s ", pNtk->pName ); fprintf( pTable, "%d ", Abc_NtkLevel(pNtk) ); fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) ); - fprintf( pTable, "%.2f ", (float)(s_MappingMem)/(float)(1<<20) ); - fprintf( pTable, "%.2f", (float)(s_MappingTime)/(float)(CLOCKS_PER_SEC) ); +// fprintf( pTable, "%.2f ", (float)(s_MappingMem)/(float)(1<<20) ); +// fprintf( pTable, "%.2f", (float)(s_MappingTime)/(float)(CLOCKS_PER_SEC) ); fprintf( pTable, "\n" ); fclose( pTable ); } */ - +/* // print the statistic into a file { static int Counter = 0; @@ -176,6 +176,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) fprintf( pTable, "\n" ); fclose( pTable ); } +*/ /* // print the statistic into a file diff --git a/src/map/fpga/fpga.c b/src/map/fpga/fpga.c index d7a128b0..d04c9910 100644 --- a/src/map/fpga/fpga.c +++ b/src/map/fpga/fpga.c @@ -57,8 +57,8 @@ void Fpga_Init( Abc_Frame_t * pAbc ) { // set the default library //Fpga_LutLib_t s_LutLib = { "lutlib", 6, {0,1,2,4,8,16,32}, {0,1,2,3,4,5,6} }; - Fpga_LutLib_t s_LutLib = { "lutlib", 5, {0,1,1,1,1,1}, {0,1,1,1,1,1} }; -// Fpga_LutLib_t s_LutLib = { "lutlib", 4, {0,1,1,1,1}, {0,1,1,1,1} }; +// Fpga_LutLib_t s_LutLib = { "lutlib", 5, {0,1,1,1,1,1}, {0,1,1,1,1,1} }; + Fpga_LutLib_t s_LutLib = { "lutlib", 4, {0,1,1,1,1}, {0,1,1,1,1} }; //Fpga_LutLib_t s_LutLib = { "lutlib", 3, {0,1,1,1}, {0,1,1,1} }; Abc_FrameSetLibLut( Fpga_LutLibDup(&s_LutLib) ); diff --git a/src/map/if/if.h b/src/map/if/if.h index a1d2d41b..31c07528 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -55,7 +55,7 @@ typedef enum { IF_BO, // 6: box output IF_BOX, // 7: box IF_VOID // 8: unused object -} Hop_Type_t; +} If_Type_t; //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// @@ -75,8 +75,10 @@ struct If_Par_t_ If_Lib_t * pLutLib; // the LUT library int nCutsMax; // the max number of cuts int fVerbose; // the verbosity flag + int fPreprocess; // preprossing int fArea; // area-oriented mapping int fFancy; // a fancy feature + int fExpRed; // expand/reduce of the best cuts int fLatchPaths; // reset timing on latch paths int fSeq; // sequential mapping int nLatches; // the number of latches @@ -115,6 +117,7 @@ struct If_Man_t_ int nCutsUsed; // the number of cuts currently used int nCutsMerged; // the total number of cuts merged int nCutsMax; // the maximum number of cuts at a node + float Fi; // the current value of the clock period (for seq mapping) // memory management Mem_Fixed_t * pMem; // memory manager int nEntrySize; // the size of the entry @@ -127,15 +130,16 @@ struct If_Man_t_ // priority cut struct If_Cut_t_ { - float Delay; // the delay of the cut - float Area; // the area of the cut - If_Cut_t * pOne; // the parent cut - If_Cut_t * pTwo; // the parent cut - char fCompl0; // the complemented attribute - char fCompl1; // the complemented attribute - char Phase; // the complemented attribute - char nLeaves; // the number of leaves - int * pLeaves; // the array of fanins + float Delay; // delay of the cut + float Area; // area (or area-flow) of the cut + If_Cut_t * pOne; // parent cut + If_Cut_t * pTwo; // parent cut + unsigned uSign; // cut signature + char fCompl0; // complemented attribute + char fCompl1; // complemented attribute + char Phase; // complemented attribute + char nLeaves; // number of leaves + int * pLeaves; // array of fanins }; // node extension @@ -149,8 +153,7 @@ struct If_Obj_t_ unsigned Level : 24; // logic level of the node int Id; // integer ID int nRefs; // the number of references - short nCuts; // the number of cuts - short iCut; // the number of the best cut + int nCuts; // the number of cuts If_Obj_t * pFanin0; // the first fanin If_Obj_t * pFanin1; // the second fanin If_Obj_t * pEquiv; // the choice node @@ -188,7 +191,8 @@ static inline void If_ObjSetChoice( If_Obj_t * pObj, If_Obj_t * pEqu ) { p static inline If_Cut_t * If_ObjCut( If_Obj_t * pObj, int iCut ) { return pObj->Cuts + iCut; } static inline If_Cut_t * If_ObjCutTriv( If_Obj_t * pObj ) { return pObj->Cuts; } -static inline If_Cut_t * If_ObjCutBest( If_Obj_t * pObj ) { return pObj->Cuts + pObj->iCut; } +static inline If_Cut_t * If_ObjCutBest( If_Obj_t * pObj ) { return pObj->Cuts + 1; } +static inline unsigned If_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId % 31)); } static inline void * If_CutData( If_Cut_t * pCut ) { return *(void **)pCut; } static inline void If_CutSetData( If_Cut_t * pCut, void * pData ) { *(void **)pCut = pData; } @@ -239,6 +243,7 @@ static inline float If_CutLutArea( If_Man_t * p, If_Cut_t * pCut ) { r /*=== ifCore.c ==========================================================*/ extern int If_ManPerformMapping( If_Man_t * p ); +extern int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fRequired ); /*=== ifMan.c ==========================================================*/ extern If_Man_t * If_ManStart( If_Par_t * pPars ); extern void If_ManStop( If_Man_t * p ); @@ -247,6 +252,19 @@ extern If_Obj_t * If_ManCreatePo( If_Man_t * p, If_Obj_t * pDriver, int fCo extern If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_t * pFan1, int fCompl1 ); /*=== ifMap.c ==========================================================*/ extern void If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode ); +extern float If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut, int nLevels ); +extern float If_CutAreaRefed( If_Man_t * p, If_Cut_t * pCut, int nLevels ); +extern float If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels ); +extern float If_CutRef( If_Man_t * p, If_Cut_t * pCut, int nLevels ); +extern void If_CutPrint( If_Man_t * p, If_Cut_t * pCut ); +extern float If_CutDelay( If_Man_t * p, If_Cut_t * pCut ); +extern float If_CutFlow( If_Man_t * p, If_Cut_t * pCut ); +extern int If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut, int nLimit ); +extern void If_CutCopy( If_Cut_t * pCutDest, If_Cut_t * pCutSrc ); +/*=== ifReduce.c ==========================================================*/ +extern void If_ManImproveMapping( If_Man_t * p ); +/*=== ifSelect.c ==========================================================*/ +extern void If_ManPerformMappingPreprocess( If_Man_t * p ); /*=== ifUtil.c ==========================================================*/ extern float If_ManDelayMax( If_Man_t * p ); extern void If_ManCleanNodeCopy( If_Man_t * p ); diff --git a/src/map/if/ifCore.c b/src/map/if/ifCore.c index 37a22d8b..e139e14b 100644 --- a/src/map/if/ifCore.c +++ b/src/map/if/ifCore.c @@ -24,8 +24,6 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -44,7 +42,7 @@ static int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode ); int If_ManPerformMapping( If_Man_t * p ) { If_Obj_t * pObj; - int nItersFlow = 2; + int nItersFlow = 1; int nItersArea = 1; int clkTotal = clock(); int i; @@ -56,13 +54,27 @@ int If_ManPerformMapping( If_Man_t * p ) If_ManForEachPi( p, pObj, i ) pObj->EstRefs = (float)1.0; // delay oriented mapping - If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0 ); + if ( p->pPars->fPreprocess && !p->pPars->fArea && p->pPars->nCutsMax >= 4 ) + If_ManPerformMappingPreprocess( p ); + else + If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 1 ); + // try to improve area by expanding and reducing the cuts + if ( p->pPars->fExpRed ) + If_ManImproveMapping( p ); // area flow oriented mapping for ( i = 0; i < nItersFlow; i++ ) - If_ManPerformMappingRound( p, p->pPars->nCutsMax, 1 ); + { + If_ManPerformMappingRound( p, p->pPars->nCutsMax, 1, 1 ); + if ( p->pPars->fExpRed ) + If_ManImproveMapping( p ); + } // area oriented mapping for ( i = 0; i < nItersArea; i++ ) - If_ManPerformMappingRound( p, p->pPars->nCutsMax, 2 ); + { + If_ManPerformMappingRound( p, p->pPars->nCutsMax, 2, 1 ); + if ( p->pPars->fExpRed ) + If_ManImproveMapping( p ); + } if ( p->pPars->fVerbose ) { PRT( "Total time", clock() - clkTotal ); @@ -81,7 +93,7 @@ int If_ManPerformMapping( If_Man_t * p ) SeeAlso [] ***********************************************************************/ -int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode ) +int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fRequired ) { If_Obj_t * pObj; int i, clk = clock(); @@ -94,15 +106,18 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode ) If_ManForEachNode( p, pObj, i ) If_ObjPerformMapping( p, pObj, Mode ); // compute required times and stats - If_ManComputeRequired( p, Mode==0 ); - if ( p->pPars->fVerbose ) + if ( fRequired ) { - char Symb = (Mode == 0)? 'D' : ((Mode == 1)? 'F' : 'A'); - printf( "%c: Del = %6.2f. Area = %8.2f. Cuts = %6d. Lim = %2d. Ave = %5.2f. ", - Symb, p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) ); - PRT( "T", clock() - clk ); + If_ManComputeRequired( p, Mode==0 ); + if ( p->pPars->fVerbose ) + { + char Symb = (Mode == 0)? 'D' : ((Mode == 1)? 'F' : 'A'); + printf( "%c: Del = %6.2f. Area = %8.2f. Cuts = %6d. Lim = %2d. Ave = %5.2f. ", + Symb, p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) ); + PRT( "T", clock() - clk ); // printf( "Max number of cuts = %d. Average number of cuts = %5.2f.\n", // p->nCutsMax, 1.0 * p->nCutsMerged / If_ManAndNum(p) ); + } } return 1; } diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c index bc13c6f0..b0c12fea 100644 --- a/src/map/if/ifMan.c +++ b/src/map/if/ifMan.c @@ -191,6 +191,7 @@ If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_ ***********************************************************************/ If_Obj_t * If_ManSetupObj( If_Man_t * p ) { + If_Cut_t * pCut; If_Obj_t * pObj; int i, * pArrays; // get memory for the object @@ -204,10 +205,12 @@ If_Obj_t * If_ManSetupObj( If_Man_t * p ) pObj->Id = Vec_PtrSize(p->vObjs); Vec_PtrPush( p->vObjs, pObj ); // assign elementary cut + pCut = pObj->Cuts; + pCut->nLeaves = 1; + pCut->pLeaves[0] = p->pPars->fSeq? (pObj->Id << 8) : pObj->Id; + pCut->uSign = If_ObjCutSign( pCut->pLeaves[0] ); + // set the number of cuts pObj->nCuts = 1; - pObj->Cuts[0].nLeaves = 1; - pObj->Cuts[0].pLeaves[0] = pObj->Id; - pObj->iCut = 0; // set the required times pObj->Required = IF_FLOAT_LARGE; return pObj; diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index 0b505062..9134dc9a 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -39,6 +39,26 @@ /**Function************************************************************* + Synopsis [Counts the number of 1s in the signature.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int If_WordCountOnes( unsigned uWord ) +{ + uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555); + uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333); + uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F); + uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF); + return (uWord & 0x0000FFFF) + (uWord>>16); +} + +/**Function************************************************************* + Synopsis [Returns 1 if pDom is contained in pCut.] Description [] @@ -95,7 +115,7 @@ static inline int If_CutCheckEquality( If_Cut_t * pDom, If_Cut_t * pCut ) SeeAlso [] ***********************************************************************/ -int If_CutFilter( If_Man_t * p, If_Cut_t * pCut ) +int If_CutFilter( If_Man_t * p, If_Cut_t * pCut, int Mode ) { If_Cut_t * pTemp; int i; @@ -103,21 +123,37 @@ int If_CutFilter( If_Man_t * p, If_Cut_t * pCut ) { pTemp = p->ppCuts[i]; if ( pTemp->nLeaves > pCut->nLeaves ) - continue; - // skip the non-contained cuts -// if ( (pTemp->uSign & pCut->uSign) != pTemp->uSign ) + { // continue; - // check containment seriously - if ( If_CutCheckDominance( pTemp, pCut ) ) -// if ( If_CutCheckEquality( pTemp, pCut ) ) - return 1; + // skip the non-contained cuts + if ( (pTemp->uSign & pCut->uSign) != pCut->uSign ) + continue; + // check containment seriously + if ( If_CutCheckDominance( pCut, pTemp ) ) + { + // removed contained cut + p->ppCuts[i] = p->ppCuts[p->nCuts-1]; + p->ppCuts[p->nCuts-1] = pTemp; + p->nCuts--; + i--; + } + } + else + { + // skip the non-contained cuts + if ( (pTemp->uSign & pCut->uSign) != pTemp->uSign ) + continue; + // check containment seriously + if ( If_CutCheckDominance( pTemp, pCut ) ) + return 1; + } } return 0; } /**Function************************************************************* - Synopsis [Prepares the object for FPGA mapping.] + Synopsis [Merges two cuts.] Description [] @@ -126,7 +162,7 @@ int If_CutFilter( If_Man_t * p, If_Cut_t * pCut ) SeeAlso [] ***********************************************************************/ -int If_CutMergeOrdered( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC, int nLimit ) +static inline int If_CutMergeOrdered( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC, int nLimit ) { int i, k, c; assert( pC0->nLeaves >= pC1->nLeaves ); @@ -203,6 +239,58 @@ int If_CutMergeOrdered( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC, int nLimi /**Function************************************************************* + Synopsis [Merges two cuts.] + + Description [Special case when the cut is known to exist.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int If_CutMergeOrdered2( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC, int nLimit ) +{ + int i, k, c; + assert( pC0->nLeaves >= pC1->nLeaves ); + // copy the first cut + for ( i = 0; i < pC0->nLeaves; i++ ) + pC->pLeaves[i] = pC0->pLeaves[i]; + pC->nLeaves = pC0->nLeaves; + // the case when one of the cuts is the largest + if ( pC0->nLeaves == nLimit ) + return 1; + // add nodes of the second cut + k = 0; + for ( i = 0; i < pC1->nLeaves; i++ ) + { + // find k-th node before which i-th node should be added + for ( ; k < pC->nLeaves; k++ ) + if ( pC->pLeaves[k] >= pC1->pLeaves[i] ) + break; + // check the case when this should be the last node + if ( k == pC->nLeaves ) + { + pC->pLeaves[k++] = pC1->pLeaves[i]; + pC->nLeaves++; + continue; + } + // check the case when equal node is found + if ( pC1->pLeaves[i] == pC->pLeaves[k] ) + continue; + // add the node + for ( c = pC->nLeaves; c > k; c-- ) + pC->pLeaves[c] = pC->pLeaves[c-1]; + pC->pLeaves[k++] = pC1->pLeaves[i]; + pC->nLeaves++; + } + assert( pC->nLeaves <= nLimit ); + for ( i = 1; i < pC->nLeaves; i++ ) + assert( pC->pLeaves[i-1] < pC->pLeaves[i] ); + return 1; +} + +/**Function************************************************************* + Synopsis [Prepares the object for FPGA mapping.] Description [] @@ -212,7 +300,7 @@ int If_CutMergeOrdered( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC, int nLimi SeeAlso [] ***********************************************************************/ -static inline int If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut, int nLimit ) +int If_CutMerge( If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pCut, int nLimit ) { // merge the nodes if ( pCut0->nLeaves < pCut1->nLeaves ) @@ -243,17 +331,17 @@ int If_CutCompareDelay( If_Cut_t ** ppC0, If_Cut_t ** ppC1 ) { If_Cut_t * pC0 = *ppC0; If_Cut_t * pC1 = *ppC1; - if ( pC0->Delay < pC1->Delay ) + if ( pC0->Delay < pC1->Delay - 0.0001 ) return -1; - if ( pC0->Delay > pC1->Delay ) + if ( pC0->Delay > pC1->Delay + 0.0001 ) return 1; if ( pC0->nLeaves < pC1->nLeaves ) return -1; if ( pC0->nLeaves > pC1->nLeaves ) return 1; - if ( pC0->Area < pC1->Area ) + if ( pC0->Area < pC1->Area - 0.0001 ) return -1; - if ( pC0->Area > pC1->Area ) + if ( pC0->Area > pC1->Area + 0.0001 ) return 1; return 0; } @@ -273,13 +361,13 @@ int If_CutCompareDelayOld( If_Cut_t ** ppC0, If_Cut_t ** ppC1 ) { If_Cut_t * pC0 = *ppC0; If_Cut_t * pC1 = *ppC1; - if ( pC0->Delay < pC1->Delay ) + if ( pC0->Delay < pC1->Delay - 0.0001 ) return -1; - if ( pC0->Delay > pC1->Delay ) + if ( pC0->Delay > pC1->Delay + 0.0001 ) return 1; - if ( pC0->Area < pC1->Area ) + if ( pC0->Area < pC1->Area - 0.0001 ) return -1; - if ( pC0->Area > pC1->Area ) + if ( pC0->Area > pC1->Area + 0.0001 ) return 1; if ( pC0->nLeaves < pC1->nLeaves ) return -1; @@ -303,17 +391,17 @@ int If_CutCompareArea( If_Cut_t ** ppC0, If_Cut_t ** ppC1 ) { If_Cut_t * pC0 = *ppC0; If_Cut_t * pC1 = *ppC1; - if ( pC0->Area < pC1->Area ) + if ( pC0->Area < pC1->Area - 0.0001 ) return -1; - if ( pC0->Area > pC1->Area ) + if ( pC0->Area > pC1->Area + 0.0001 ) return 1; if ( pC0->nLeaves < pC1->nLeaves ) return -1; if ( pC0->nLeaves > pC1->nLeaves ) return 1; - if ( pC0->Delay < pC1->Delay ) + if ( pC0->Delay < pC1->Delay - 0.0001 ) return -1; - if ( pC0->Delay > pC1->Delay ) + if ( pC0->Delay > pC1->Delay + 0.0001 ) return 1; return 0; } @@ -405,7 +493,7 @@ float If_CutFlow( If_Man_t * p, If_Cut_t * pCut ) SeeAlso [] ***********************************************************************/ -float If_CutRef( If_Man_t * p, If_Cut_t * pCut, int nLevels ) +float If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels ) { If_Obj_t * pLeaf; float Area; @@ -413,10 +501,10 @@ float If_CutRef( If_Man_t * p, If_Cut_t * pCut, int nLevels ) Area = If_CutLutArea(p, pCut); If_CutForEachLeaf( p, pCut, pLeaf, i ) { - assert( pLeaf->nRefs >= 0 ); - if ( pLeaf->nRefs++ > 0 || !If_ObjIsAnd(pLeaf) || nLevels == 1 ) + assert( pLeaf->nRefs > 0 ); + if ( --pLeaf->nRefs > 0 || !If_ObjIsAnd(pLeaf) || nLevels == 1 ) continue; - Area += If_CutRef( p, If_ObjCutBest(pLeaf), nLevels - 1 ); + Area += If_CutDeref( p, If_ObjCutBest(pLeaf), nLevels - 1 ); } return Area; } @@ -432,7 +520,7 @@ float If_CutRef( If_Man_t * p, If_Cut_t * pCut, int nLevels ) SeeAlso [] ***********************************************************************/ -float If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels ) +float If_CutRef( If_Man_t * p, If_Cut_t * pCut, int nLevels ) { If_Obj_t * pLeaf; float Area; @@ -440,16 +528,36 @@ float If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels ) Area = If_CutLutArea(p, pCut); If_CutForEachLeaf( p, pCut, pLeaf, i ) { - assert( pLeaf->nRefs > 0 ); - if ( --pLeaf->nRefs > 0 || !If_ObjIsAnd(pLeaf) || nLevels == 1 ) + assert( pLeaf->nRefs >= 0 ); + if ( pLeaf->nRefs++ > 0 || !If_ObjIsAnd(pLeaf) || nLevels == 1 ) continue; - Area += If_CutDeref( p, If_ObjCutBest(pLeaf), nLevels - 1 ); + Area += If_CutRef( p, If_ObjCutBest(pLeaf), nLevels - 1 ); } return Area; } /**Function************************************************************* + Synopsis [Prints one cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_CutPrint( If_Man_t * p, If_Cut_t * pCut ) +{ + int i; + printf( "{" ); + for ( i = 0; i < pCut->nLeaves; i++ ) + printf( " %d", pCut->pLeaves[i] ); + printf( " }\n" ); +} + +/**Function************************************************************* + Synopsis [Computes area of the first level.] Description [The cut need to be derefed.] @@ -459,7 +567,7 @@ float If_CutDeref( If_Man_t * p, If_Cut_t * pCut, int nLevels ) SeeAlso [] ***********************************************************************/ -float If_CutArea( If_Man_t * p, If_Cut_t * pCut, int nLevels ) +float If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut, int nLevels ) { float aResult, aResult2; assert( pCut->nLeaves > 1 ); @@ -480,6 +588,27 @@ float If_CutArea( If_Man_t * p, If_Cut_t * pCut, int nLevels ) SeeAlso [] ***********************************************************************/ +float If_CutAreaRefed( If_Man_t * p, If_Cut_t * pCut, int nLevels ) +{ + float aResult, aResult2; + assert( pCut->nLeaves > 1 ); + aResult2 = If_CutDeref( p, pCut, nLevels ); + aResult = If_CutRef( p, pCut, nLevels ); + assert( aResult == aResult2 ); + return aResult; +} + +/**Function************************************************************* + + Synopsis [Computes area of the first level.] + + Description [The cut need to be derefed.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void If_CutCopy( If_Cut_t * pCutDest, If_Cut_t * pCutSrc ) { int * pArray; @@ -503,7 +632,7 @@ void If_CutCopy( If_Cut_t * pCutDest, If_Cut_t * pCutSrc ) void If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode ) { If_Cut_t * pCut0, * pCut1, * pCut; - int i, k; + int i, k, iCut; // prepare if ( Mode == 0 ) @@ -521,17 +650,22 @@ void If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode ) pCut = If_ObjCutBest(pObj); pCut->Delay = If_CutDelay( p, pCut ); assert( pCut->Delay <= pObj->Required + p->fEpsilon ); - pCut->Area = (Mode == 2)? If_CutArea( p, pCut, 100 ) : If_CutFlow( p, pCut ); + pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut ); // save the best cut from the previous iteration If_CutCopy( p->ppCuts[p->nCuts++], pCut ); p->nCutsMerged++; } + // prepare room for the next cut + iCut = p->nCuts; + pCut = p->ppCuts[iCut]; // generate cuts - pCut = p->ppCuts[p->nCuts]; If_ObjForEachCut( pObj->pFanin0, pCut0, i ) If_ObjForEachCut( pObj->pFanin1, pCut1, k ) { + // make sure K-feasible cut exists + if ( If_WordCountOnes(pCut0->uSign | pCut1->uSign) > p->pPars->nLutSize ) + continue; // prefilter using arrival times if ( Mode && (pCut0->Delay > pObj->Required + p->fEpsilon || pCut1->Delay > pObj->Required + p->fEpsilon) ) continue; @@ -539,7 +673,8 @@ void If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode ) if ( !If_CutMerge( pCut0, pCut1, pCut, p->pPars->nLutSize ) ) continue; // check if this cut is contained in any of the available cuts - if ( If_CutFilter( p, pCut ) ) + pCut->uSign = pCut0->uSign | pCut1->uSign; + if ( If_CutFilter( p, pCut, Mode ) ) continue; // check if the cut satisfies the required times pCut->Delay = If_CutDelay( p, pCut ); @@ -549,18 +684,26 @@ void If_ObjPerformMapping( If_Man_t * p, If_Obj_t * pObj, int Mode ) pCut->pOne = pCut0; pCut->fCompl0 = pObj->fCompl0; pCut->pTwo = pCut1; pCut->fCompl1 = pObj->fCompl1; // pCut->Phase = ... - pCut->Area = (Mode == 2)? If_CutArea( p, pCut, 100 ) : If_CutFlow( p, pCut ); +// pCut->Phase = (char)(int)If_CutAreaDerefed( p, pCut, 1 ); + pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut ); p->nCutsMerged++; + // make sure the cut is the last one (after filtering it may not be so) + assert( pCut == p->ppCuts[iCut] ); + p->ppCuts[iCut] = p->ppCuts[p->nCuts]; + p->ppCuts[p->nCuts] = pCut; // prepare room for the next cut - pCut = p->ppCuts[++p->nCuts]; + iCut = ++p->nCuts; + pCut = p->ppCuts[iCut]; } +//printf( "%d ", p->nCuts ); assert( p->nCuts > 0 ); + // sort if we have more cuts If_ManSortCuts( p, Mode ); - // take the first + // decide how many cuts to use pObj->nCuts = IF_MIN( p->nCuts + 1, p->nCutsUsed ); + // take the first If_ObjForEachCutStart( pObj, pCut, i, 1 ) If_CutCopy( pCut, p->ppCuts[i-1] ); - pObj->iCut = 1; assert( If_ObjCutBest(pObj)->nLeaves > 1 ); // assign delay of the trivial cut If_ObjCutTriv(pObj)->Delay = If_ObjCutBest(pObj)->Delay; diff --git a/src/map/if/ifReduce.c b/src/map/if/ifReduce.c new file mode 100644 index 00000000..5c8da0d0 --- /dev/null +++ b/src/map/if/ifReduce.c @@ -0,0 +1,576 @@ +/**CFile**************************************************************** + + FileName [ifExpand.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [FPGA mapping based on priority cuts.] + + Synopsis [Incremental improvement of current mapping.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - November 21, 2006.] + + Revision [$Id: ifExpand.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "if.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void If_ManImproveReduce( If_Man_t * p, int nLimit ); +static void If_ManImproveExpand( If_Man_t * p, int nLimit ); +static void If_ManImproveNodeExpand( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vFrontOld, Vec_Ptr_t * vVisited ); +static void If_ManImproveNodePrepare( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vFrontOld, Vec_Ptr_t * vVisited ); +static void If_ManImproveNodeUpdate( If_Man_t * p, If_Obj_t * pObj, Vec_Ptr_t * vFront ); +static void If_ManImproveNodeFaninCompact( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Improves current mapping using expand/Expand of one cut.] + + Description [Assumes current mapping assigned and required times computed.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_ManImproveMapping( If_Man_t * p ) +{ + int clk; + + clk = clock(); + If_ManImproveExpand( p, p->pPars->nLutSize ); + If_ManComputeRequired( p, 0 ); + if ( p->pPars->fVerbose ) + { + printf( "E: Del = %6.2f. Area = %8.2f. Cuts = %6d. Lim = %2d. Ave = %5.2f. ", + p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) ); + PRT( "T", clock() - clk ); + } +/* + clk = clock(); + If_ManImproveReduce( p, p->pPars->nLutSize ); + If_ManComputeRequired( p, 0 ); + if ( p->pPars->fVerbose ) + { + printf( "R: Del = %6.2f. Area = %8.2f. Cuts = %6d. Lim = %2d. Ave = %5.2f. ", + p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) ); + PRT( "T", clock() - clk ); + } + + clk = clock(); + If_ManImproveExpand( p, p->pPars->nLutSize ); + If_ManComputeRequired( p, 0 ); + if ( p->pPars->fVerbose ) + { + printf( "E: Del = %6.2f. Area = %8.2f. Cuts = %6d. Lim = %2d. Ave = %5.2f. ", + p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) ); + PRT( "T", clock() - clk ); + } +*/ +} + +/**Function************************************************************* + + Synopsis [Performs area recovery for each node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_ManImproveExpand( If_Man_t * p, int nLimit ) +{ + Vec_Ptr_t * vFront, * vFrontOld, * vVisited; + If_Obj_t * pObj; + int i; + vFront = Vec_PtrAlloc( nLimit ); + vFrontOld = Vec_PtrAlloc( nLimit ); + vVisited = Vec_PtrAlloc( 100 ); + // iterate through all nodes in the topological order + If_ManForEachNode( p, pObj, i ) + If_ManImproveNodeExpand( p, pObj, nLimit, vFront, vFrontOld, vVisited ); + Vec_PtrFree( vFront ); + Vec_PtrFree( vFrontOld ); + Vec_PtrFree( vVisited ); +} + +/**Function************************************************************* + + Synopsis [Counts the number of nodes with no external fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_ManImproveCutCost( If_Man_t * p, Vec_Ptr_t * vFront ) +{ + If_Obj_t * pFanin; + int i, Counter = 0; + Vec_PtrForEachEntry( vFront, pFanin, i ) + if ( pFanin->nRefs == 0 ) + Counter++; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Performs area recovery for each node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_ManImproveNodeExpand( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vFrontOld, Vec_Ptr_t * vVisited ) +{ + If_Obj_t * pFanin; + If_Cut_t * pCut; + int CostBef, CostAft, i; + float DelayOld, AreaBef, AreaAft; + pCut = If_ObjCutBest(pObj); + assert( pCut->Delay <= pObj->Required + p->fEpsilon ); + if ( pObj->nRefs == 0 ) + return; + // get the delay + DelayOld = pCut->Delay; + // get the area + AreaBef = If_CutAreaRefed( p, pCut, 100000 ); +// if ( AreaBef == 1 ) +// return; + // the cut is non-trivial + If_ManImproveNodePrepare( p, pObj, nLimit, vFront, vFrontOld, vVisited ); + // iteratively modify the cut + If_CutDeref( p, pCut, 100000 ); + CostBef = If_ManImproveCutCost( p, vFront ); + If_ManImproveNodeFaninCompact( p, pObj, nLimit, vFront, vVisited ); + CostAft = If_ManImproveCutCost( p, vFront ); + If_CutRef( p, pCut, 100000 ); + assert( CostBef >= CostAft ); + // clean up + Vec_PtrForEachEntry( vVisited, pFanin, i ) + pFanin->fMark = 0; + // update the node + If_ManImproveNodeUpdate( p, pObj, vFront ); + pCut->Delay = If_CutDelay( p, pCut ); + // get the new area + AreaAft = If_CutAreaRefed( p, pCut, 100000 ); + if ( AreaAft > AreaBef || pCut->Delay > pObj->Required + p->fEpsilon ) + { + If_ManImproveNodeUpdate( p, pObj, vFrontOld ); + AreaAft = If_CutAreaRefed( p, pCut, 100000 ); + assert( AreaAft == AreaBef ); + pCut->Delay = DelayOld; + } +} + +/**Function************************************************************* + + Synopsis [Performs area recovery for each node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_ManImproveMark_rec( If_Man_t * p, If_Obj_t * pObj, Vec_Ptr_t * vVisited ) +{ + if ( pObj->fMark ) + return; + assert( If_ObjIsAnd(pObj) ); + If_ManImproveMark_rec( p, If_ObjFanin0(pObj), vVisited ); + If_ManImproveMark_rec( p, If_ObjFanin1(pObj), vVisited ); + Vec_PtrPush( vVisited, pObj ); + pObj->fMark = 1; +} + +/**Function************************************************************* + + Synopsis [Prepares node mapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_ManImproveNodePrepare( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vFrontOld, Vec_Ptr_t * vVisited ) +{ + If_Cut_t * pCut; + If_Obj_t * pLeaf; + int i; + Vec_PtrClear( vFront ); + Vec_PtrClear( vFrontOld ); + Vec_PtrClear( vVisited ); + // expand the cut downwards from the given place + pCut = If_ObjCutBest(pObj); + If_CutForEachLeaf( p, pCut, pLeaf, i ) + { + Vec_PtrPush( vFront, pLeaf ); + Vec_PtrPush( vFrontOld, pLeaf ); + Vec_PtrPush( vVisited, pLeaf ); + pLeaf->fMark = 1; + } + // mark the nodes in the cone + If_ManImproveMark_rec( p, pObj, vVisited ); +} + +/**Function************************************************************* + + Synopsis [Updates the frontier.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_ManImproveNodeUpdate( If_Man_t * p, If_Obj_t * pObj, Vec_Ptr_t * vFront ) +{ + If_Cut_t * pCut; + If_Obj_t * pFanin; + int i; + pCut = If_ObjCutBest(pObj); + // deref node's cut + If_CutDeref( p, pCut, 10000 ); + // update the node's cut + pCut->nLeaves = Vec_PtrSize(vFront); + Vec_PtrForEachEntry( vFront, pFanin, i ) + pCut->pLeaves[i] = pFanin->Id; + // ref the new cut + If_CutRef( p, pCut, 10000 ); +} + + +/**Function************************************************************* + + Synopsis [Returns 1 if the number of fanins will grow.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_ManImproveNodeWillGrow( If_Man_t * p, If_Obj_t * pObj ) +{ + If_Obj_t * pFanin0, * pFanin1; + assert( If_ObjIsAnd(pObj) ); + pFanin0 = If_ObjFanin0(pObj); + pFanin1 = If_ObjFanin1(pObj); + return !pFanin0->fMark && !pFanin1->fMark; +} + +/**Function************************************************************* + + Synopsis [Returns the increase in the number of fanins with no external refs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_ManImproveNodeFaninCost( If_Man_t * p, If_Obj_t * pObj ) +{ + int Counter = 0; + assert( If_ObjIsAnd(pObj) ); + // check if the node has external refs + if ( pObj->nRefs == 0 ) + Counter--; + // increment the number of fanins without external refs + if ( !If_ObjFanin0(pObj)->fMark && If_ObjFanin0(pObj)->nRefs == 0 ) + Counter++; + // increment the number of fanins without external refs + if ( !If_ObjFanin1(pObj)->fMark && If_ObjFanin1(pObj)->nRefs == 0 ) + Counter++; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Updates the frontier.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_ManImproveNodeFaninUpdate( If_Man_t * p, If_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited ) +{ + If_Obj_t * pFanin; + assert( If_ObjIsAnd(pObj) ); + Vec_PtrRemove( vFront, pObj ); + pFanin = If_ObjFanin0(pObj); + if ( !pFanin->fMark ) + { + Vec_PtrPush( vFront, pFanin ); + Vec_PtrPush( vVisited, pFanin ); + pFanin->fMark = 1; + } + pFanin = If_ObjFanin1(pObj); + if ( !pFanin->fMark ) + { + Vec_PtrPush( vFront, pFanin ); + Vec_PtrPush( vVisited, pFanin ); + pFanin->fMark = 1; + } +} + +/**Function************************************************************* + + Synopsis [Compacts the number of external refs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_ManImproveNodeFaninCompact0( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited ) +{ + If_Obj_t * pFanin; + int i; + Vec_PtrForEachEntry( vFront, pFanin, i ) + { + if ( If_ObjIsPi(pFanin) ) + continue; + if ( If_ManImproveNodeWillGrow(p, pFanin) ) + continue; + if ( If_ManImproveNodeFaninCost(p, pFanin) <= 0 ) + { + If_ManImproveNodeFaninUpdate( p, pFanin, vFront, vVisited ); + return 1; + } + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Compacts the number of external refs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_ManImproveNodeFaninCompact1( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited ) +{ + If_Obj_t * pFanin; + int i; + Vec_PtrForEachEntry( vFront, pFanin, i ) + { + if ( If_ObjIsPi(pFanin) ) + continue; + if ( If_ManImproveNodeFaninCost(p, pFanin) < 0 ) + { + If_ManImproveNodeFaninUpdate( p, pFanin, vFront, vVisited ); + return 1; + } + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Compacts the number of external refs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_ManImproveNodeFaninCompact2( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited ) +{ + If_Obj_t * pFanin; + int i; + Vec_PtrForEachEntry( vFront, pFanin, i ) + { + if ( If_ObjIsPi(pFanin) ) + continue; + if ( If_ManImproveNodeFaninCost(p, pFanin) <= 0 ) + { + If_ManImproveNodeFaninUpdate( p, pFanin, vFront, vVisited ); + return 1; + } + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Compacts the number of external refs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_ManImproveNodeFaninCompact_int( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited ) +{ + if ( If_ManImproveNodeFaninCompact0(p, pObj, nLimit, vFront, vVisited) ) + return 1; + if ( Vec_PtrSize(vFront) < nLimit && If_ManImproveNodeFaninCompact1(p, pObj, nLimit, vFront, vVisited) ) + return 1; + if ( Vec_PtrSize(vFront) < nLimit && If_ManImproveNodeFaninCompact2(p, pObj, nLimit, vFront, vVisited) ) + return 1; + assert( Vec_PtrSize(vFront) <= nLimit ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Compacts the number of external refs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_ManImproveNodeFaninCompact( If_Man_t * p, If_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited ) +{ + while ( If_ManImproveNodeFaninCompact_int( p, pObj, nLimit, vFront, vVisited ) ); +} + + + + + +/**Function************************************************************* + + Synopsis [Performs fast mapping for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_ManImproveNodeReduce( If_Man_t * p, If_Obj_t * pObj, int nLimit ) +{ + If_Cut_t * pCut, * pCut0, * pCut1, * pCutR; + If_Obj_t * pFanin0, * pFanin1; + float AreaBef, AreaAft; + int RetValue; + + assert( nLimit <= 32 ); + assert( If_ObjIsAnd(pObj) ); + // get the fanins + pFanin0 = If_ObjFanin0(pObj); + pFanin1 = If_ObjFanin1(pObj); + // get the cuts + pCut = If_ObjCutBest(pObj); + pCut0 = If_ObjIsPi(pFanin0) ? If_ObjCutTriv(pFanin0) : If_ObjCutBest(pFanin0); + pCut1 = If_ObjIsPi(pFanin1) ? If_ObjCutTriv(pFanin1) : If_ObjCutBest(pFanin1); + assert( pCut->Delay <= pObj->Required + p->fEpsilon ); + + // deref the cut if the node is refed + if ( pObj->nRefs > 0 ) + If_CutDeref( p, pCut, 100000 ); + // get the area + AreaBef = If_CutAreaDerefed( p, pCut, 100000 ); + // get the fanin support + if ( pFanin0->nRefs > 2 && pCut0->Delay < pObj->Required + p->fEpsilon ) +// if ( pSupp0->nRefs > 0 && pSupp0->Delay < pSupp->DelayR ) // this leads to 2% worse results + { + pCut0 = If_ObjCutTriv(pFanin0); + } + // get the fanin support + if ( pFanin1->nRefs > 2 && pCut1->Delay < pObj->Required + p->fEpsilon ) +// if ( pSupp1->nRefs > 0 && pSupp1->Delay < pSupp->DelayR ) + { + pCut1 = If_ObjCutTriv(pFanin1); + } + + // merge the cuts + pCutR = p->ppCuts[0]; + RetValue = If_CutMerge( pCut0, pCut1, pCutR, nLimit ); + // try very simple cut + if ( !RetValue ) + { + RetValue = If_CutMerge( If_ObjCutTriv(pFanin0), If_ObjCutTriv(pFanin1), pCutR, nLimit ); + assert( RetValue == 1 ); + } + if ( RetValue ) + { + pCutR->Delay = If_CutDelay( p, pCutR ); + AreaAft = If_CutAreaDerefed( p, pCutR, 100000 ); + // update the best cut + if ( AreaAft < AreaBef - p->fEpsilon && pCutR->Delay < pObj->Required + p->fEpsilon ) + If_CutCopy( pCut, pCutR ); + } + // recompute the delay of the best cut + pCut->Delay = If_CutDelay( p, pCut ); + // ref the cut if the node is refed + if ( pObj->nRefs > 0 ) + If_CutRef( p, pCut, 100000 ); +} + +/**Function************************************************************* + + Synopsis [Performs area recovery for each node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_ManImproveReduce( If_Man_t * p, int nLimit ) +{ + If_Obj_t * pObj; + int i; + If_ManForEachNode( p, pObj, i ) + { + if ( 278 == i ) + { + int s = 0; + } + If_ManImproveNodeReduce( p, pObj, nLimit ); + } +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/map/if/ifSelect.c b/src/map/if/ifSelect.c new file mode 100644 index 00000000..d54abb29 --- /dev/null +++ b/src/map/if/ifSelect.c @@ -0,0 +1,175 @@ +/**CFile**************************************************************** + + FileName [ifSelect.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [FPGA mapping based on priority cuts.] + + Synopsis [Selects what mapping to use.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - November 21, 2006.] + + Revision [$Id: ifSelect.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "if.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void If_ManPerformMappingMoveBestCut( If_Man_t * p, int iPosNew, int iPosOld ); +static void If_ManPerformMappingAdjust( If_Man_t * p, int nCuts ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Merges the results of delay, relaxed delay and area-based mapping.] + + Description [Delay target may be different from minimum delay!!!] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_ManPerformMappingPreprocess( If_Man_t * p ) +{ + float delayArea, delayDelay, delayPure; + int clk = clock(); + assert( p->pPars->nCutsMax >= 4 ); + + // perform min-area mapping and move the cut to the end + p->pPars->fArea = 1; + If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 0 ); + p->pPars->fArea = 0; + delayArea = If_ManDelayMax( p ); + if ( p->pPars->DelayTarget != -1 && delayArea < p->pPars->DelayTarget - p->fEpsilon ) + delayArea = p->pPars->DelayTarget; + If_ManPerformMappingMoveBestCut( p, p->pPars->nCutsMax - 1, 1 ); + + // perfrom min-delay mapping and move the cut to the end + p->pPars->fFancy = 1; + If_ManPerformMappingRound( p, p->pPars->nCutsMax - 1, 0, 0 ); + p->pPars->fFancy = 0; + delayDelay = If_ManDelayMax( p ); + if ( p->pPars->DelayTarget != -1 && delayDelay < p->pPars->DelayTarget - p->fEpsilon ) + delayDelay = p->pPars->DelayTarget; + If_ManPerformMappingMoveBestCut( p, p->pPars->nCutsMax - 2, 1 ); + + // perform min-area mapping + If_ManPerformMappingRound( p, p->pPars->nCutsMax - 2, 0, 0 ); + delayPure = If_ManDelayMax( p ); + if ( p->pPars->DelayTarget != -1 && delayPure < p->pPars->DelayTarget - p->fEpsilon ) + delayPure = p->pPars->DelayTarget; + + // decide what to do + if ( delayPure < delayDelay - p->fEpsilon && delayPure < delayArea - p->fEpsilon ) + { + // copy the remaining two cuts + if ( p->pPars->nCutsMax > 4 ) + { + If_ManPerformMappingMoveBestCut( p, 2, p->pPars->nCutsMax - 2 ); + If_ManPerformMappingMoveBestCut( p, 3, p->pPars->nCutsMax - 1 ); + } + If_ManComputeRequired( p, 1 ); + If_ManPerformMappingAdjust( p, 4 ); + } + else if ( delayDelay < delayArea - p->fEpsilon ) + { + If_ManPerformMappingMoveBestCut( p, 1, p->pPars->nCutsMax - 2 ); + If_ManPerformMappingMoveBestCut( p, 2, p->pPars->nCutsMax - 1 ); + If_ManComputeRequired( p, 1 ); + If_ManPerformMappingAdjust( p, 3 ); + } + else + { + If_ManPerformMappingMoveBestCut( p, 1, p->pPars->nCutsMax - 1 ); + If_ManComputeRequired( p, 1 ); + If_ManPerformMappingAdjust( p, 2 ); + } + If_ManComputeRequired( p, 1 ); + if ( p->pPars->fVerbose ) + { + printf( "S: Del = %6.2f. Area = %8.2f. Cuts = %6d. Lim = %2d. Ave = %5.2f. ", + p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) ); + PRT( "T", clock() - clk ); + } +} + +/**Function************************************************************* + + Synopsis [Moves the best cut to the given position.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_ManPerformMappingMoveBestCut( If_Man_t * p, int iPosNew, int iPosOld ) +{ + If_Obj_t * pObj; + int i; + assert( iPosOld != iPosNew ); + assert( iPosOld > 0 && iPosOld < p->pPars->nCutsMax ); + assert( iPosNew > 0 && iPosNew < p->pPars->nCutsMax ); + If_ManForEachNode( p, pObj, i ) + If_CutCopy( pObj->Cuts + iPosNew, pObj->Cuts + iPosOld ); +} + +/**Function************************************************************* + + Synopsis [Adjusts mapping for the given cuts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_ManPerformMappingAdjust( If_Man_t * p, int nCuts ) +{ + If_Cut_t * pCut, * pCutBest; + If_Obj_t * pObj; + int i, c; + assert( nCuts >= 2 && nCuts <= 4 ); + If_ManForEachNode( p, pObj, i ) + { + pCutBest = NULL; + for ( c = 1; c < nCuts; c++ ) + { + pCut = pObj->Cuts + c; + pCut->Delay = If_CutDelay( p, pCut ); + pCut->Area = If_CutFlow( p, pCut ); + assert( pCutBest || pCut->Delay < pObj->Required + p->fEpsilon ); + if ( pCutBest == NULL || + (pCut->Delay < pObj->Required + p->fEpsilon && + pCut->Area < pCutBest->Area - p->fEpsilon) ) + pCutBest = pCut; + } + assert( pCutBest != NULL ); + // check if we need to move + if ( pCutBest != pObj->Cuts + 1 ) + If_CutCopy( pObj->Cuts + 1, pCutBest ); + // set the number of cuts + pObj->nCuts = 2; + } +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/map/if/ifSeq.c b/src/map/if/ifSeq.c new file mode 100644 index 00000000..ce353f49 --- /dev/null +++ b/src/map/if/ifSeq.c @@ -0,0 +1,170 @@ +/**CFile**************************************************************** + + FileName [ifSeq.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [FPGA mapping based on priority cuts.] + + Synopsis [Sequential mapping.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - November 21, 2006.] + + Revision [$Id: ifSeq.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "if.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void If_ObjPerformMappingLI( If_Man_t * p, If_Obj_t * pLatch ); +static void If_ObjPerformMappingLO( If_Man_t * p, If_Obj_t * pLatch, If_Obj_t * pObj ); +static int If_ManMappingSeqConverged( If_Man_t * p ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs sequential mapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_ManPerformMappingSeq( If_Man_t * p ) +{ + If_Obj_t * pObj, * pLatch; + int i, clkTotal = clock(); + // set the number of cuts used + p->nCutsUsed = p->pPars->nCutsMax; + // set arrival times and trivial cuts at const 1 and PIs + If_ManConst1(p)->Cuts[0].Delay = 0.0; + If_ManForEachPi( p, pObj, i ) + pObj->Cuts[0].Delay = p->pPars->pTimesArr[i]; + // set the fanout estimates of the PIs + If_ManForEachPi( p, pObj, i ) + pObj->EstRefs = (float)1.0; + // delay oriented mapping + p->pPars->fFancy = 1; + If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 0 ); + p->pPars->fFancy = 0; + + // perform iterations over the circuit + while ( !If_ManMappingSeqConverged( p ) ) + { + // assign cuts to latches + If_ManForEachLatch( p, pLatch, i ) + If_ObjPerformMappingLI( p, pLatch ); + // assign cuts to primary inputs + If_ManForEachLatch( p, pLatch, i ) + If_ObjPerformMappingLO( p, pLatch, If_ManPi(p, If_ManPiNum(p) - If_ManPoNum(p) + i) ); + // map the nodes + If_ManForEachNode( p, pObj, i ) + If_ObjPerformMapping( p, pObj, 0 ); + } + + if ( p->pPars->fVerbose ) + { + PRT( "Total time", clock() - clkTotal ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Performs sequential mapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_CutLift( If_Cut_t * pCut ) +{ + int i; + for ( i = 0; i < pCut->nLeaves; i++ ) + pCut->pLeaves[i] = ((pCut->pLeaves[i] >> 8) << 8) | ((pCut->pLeaves[i] & 255) + 1); +} + +/**Function************************************************************* + + Synopsis [Performs sequential mapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_ObjPerformMappingLI( If_Man_t * p, If_Obj_t * pLatch ) +{ + If_Obj_t * pFanin; + int c; + assert( If_ObjIsPo(pLatch) ); + pFanin = If_ObjFanin0(pLatch); + for ( c = 0; c < pFanin->nCuts; c++ ) + If_CutCopy( pLatch->Cuts + c, pFanin->Cuts + c ); +} + +/**Function************************************************************* + + Synopsis [Performs sequential mapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_ObjPerformMappingLO( If_Man_t * p, If_Obj_t * pLatch, If_Obj_t * pObj ) +{ + If_Cut_t * pCut; + int c, Limit = IF_MIN( p->nCuts + 1, p->nCutsUsed ); + assert( If_ObjIsPo(pLatch) ); + for ( c = 1; c < Limit; c++ ) + { + pCut = pObj->Cuts + c; + If_CutCopy( pCut, pLatch->Cuts + c - 1 ); + If_CutLift( pCut ); + pCut->Delay -= p->Fi; + } +} + +/**Function************************************************************* + + Synopsis [Performs sequential mapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_ManMappingSeqConverged( If_Man_t * p ) +{ + return 0; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/map/if/module.make b/src/map/if/module.make index be044da2..362318da 100644 --- a/src/map/if/module.make +++ b/src/map/if/module.make @@ -1,4 +1,8 @@ SRC += src/map/if/ifCore.c \ + src/map/if/ifCut.c \ src/map/if/ifMan.c \ src/map/if/ifMap.c \ + src/map/if/ifReduce.c \ + src/map/if/ifSelect.c \ + src/map/if/ifSeq.c \ src/map/if/ifUtil.c diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c index 4e188cf0..4e12dfe4 100644 --- a/src/sat/fraig/fraigMan.c +++ b/src/sat/fraig/fraigMan.c @@ -64,7 +64,8 @@ void Prove_ParamsSetDefault( Prove_Params_t * pParams ) pParams->nBddSizeLimit = 1000000; // the number of BDD nodes when construction is aborted pParams->fBddReorder = 1; // enables dynamic BDD variable reordering // last-gasp mitering - pParams->nMiteringLimitLast = 1000000; // final mitering limit +// pParams->nMiteringLimitLast = 1000000; // final mitering limit + pParams->nMiteringLimitLast = 0; // final mitering limit // global SAT solver limits pParams->nTotalBacktrackLimit = 0; // global limit on the number of backtracks pParams->nTotalInspectLimit = 0; // global limit on the number of clause inspects |