diff options
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 88 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 72 | ||||
-rw-r--r-- | src/base/abci/abcGen.c | 60 | ||||
-rw-r--r-- | src/base/abci/abcMiter.c | 18 | ||||
-rw-r--r-- | src/base/abci/abcPrint.c | 112 | ||||
-rw-r--r-- | src/base/abci/abcQuant.c | 2 | ||||
-rw-r--r-- | src/base/abci/abcRr.c | 2 | ||||
-rw-r--r-- | src/base/abci/abcStrash.c | 4 | ||||
-rw-r--r-- | src/base/abci/abcVerify.c | 12 |
9 files changed, 320 insertions, 50 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 99da9201..11ef85f9 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -685,7 +685,7 @@ int Abc_CommandPrintLatch( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - fPrintSccs = 1; + fPrintSccs = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF ) { @@ -736,17 +736,22 @@ int Abc_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk; int c; + int fVerbose; pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults + fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) { switch ( c ) { + case 'v': + fVerbose ^= 1; + break; case 'h': goto usage; default: @@ -761,12 +766,16 @@ int Abc_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv ) } // print the nodes - Abc_NtkPrintFanio( pOut, pNtk ); + if ( fVerbose ) + Abc_NtkPrintFanio( pOut, pNtk ); + else + Abc_NtkPrintFanioNew( pOut, pNtk ); return 0; usage: - fprintf( pErr, "usage: print_fanio [-h]\n" ); + fprintf( pErr, "usage: print_fanio [-vh]\n" ); fprintf( pErr, "\t prints the statistics about fanins/fanouts of all nodes\n" ); + fprintf( pErr, "\t-v : toggles verbose way of printing the stats [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -2066,10 +2075,12 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; + Abc_Obj_t * pObj; int c; int fAllNodes; int fRecord; int fCleanup; + int fComplOuts; pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -2079,8 +2090,9 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv ) fAllNodes = 0; fCleanup = 1; fRecord = 0; + fComplOuts= 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "acrh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "acrih" ) ) != EOF ) { switch ( c ) { @@ -2093,6 +2105,9 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'r': fRecord ^= 1; break; + case 'i': + fComplOuts ^= 1; + break; case 'h': goto usage; default: @@ -2113,16 +2128,20 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Strashing has failed.\n" ); return 1; } + if ( fComplOuts ) + Abc_NtkForEachCo( pNtkRes, pObj, c ) + Abc_ObjXorFaninC( pObj, 0 ); // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; usage: - fprintf( pErr, "usage: strash [-acrh]\n" ); + fprintf( pErr, "usage: strash [-acrih]\n" ); fprintf( pErr, "\t transforms combinational logic into an AIG\n" ); fprintf( pErr, "\t-a : toggles between using all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "DFS" ); fprintf( pErr, "\t-c : toggles cleanup to remove the dagling AIG nodes [default = %s]\n", fCleanup? "all": "DFS" ); - fprintf( pErr, "\t-r : enables using the record of AIG subgraphs [default = %s]\n", fRecord? "yes": "no" ); + fprintf( pErr, "\t-r : toggles using the record of AIG subgraphs [default = %s]\n", fRecord? "yes": "no" ); + fprintf( pErr, "\t-i : toggles complementing the COs of the AIG [default = %s]\n", fComplOuts? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -3281,20 +3300,21 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - pPars->nWinTfoLevs = 2; - pPars->nFanoutsMax = 10; - pPars->nDepthMax = 20; - pPars->nDivMax = 250; - pPars->nWinSizeMax = 300; - pPars->nGrowthLevel = 0; - pPars->fResub = 1; - pPars->fArea = 0; - pPars->fMoreEffort = 0; - pPars->fSwapEdge = 0; - pPars->fVerbose = 0; - pPars->fVeryVerbose = 0; + pPars->nWinTfoLevs = 2; + pPars->nFanoutsMax = 10; + pPars->nDepthMax = 20; + pPars->nDivMax = 250; + pPars->nWinSizeMax = 300; + pPars->nGrowthLevel = 0; + pPars->nBTLimit =10000; + pPars->fResub = 1; + pPars->fArea = 0; + pPars->fMoreEffort = 0; + pPars->fSwapEdge = 0; + pPars->fVerbose = 0; + pPars->fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLraesvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCraesvwh" ) ) != EOF ) { switch ( c ) { @@ -3353,6 +3373,17 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY ) goto usage; break; + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBTLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBTLimit < 0 ) + goto usage; + break; case 'r': pPars->fResub ^= 1; break; @@ -3398,13 +3429,14 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: mfs [-WFDML <num>] [-raesvh]\n" ); + fprintf( pErr, "usage: mfs [-WFDMLC <num>] [-raesvh]\n" ); fprintf( pErr, "\t performs don't-care-based optimization of logic networks\n" ); fprintf( pErr, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs ); fprintf( pErr, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax ); fprintf( pErr, "\t-D <num> : the max depth nodes to try (0 = no limit) [default = %d]\n", pPars->nDepthMax ); fprintf( pErr, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax ); fprintf( pErr, "\t-L <num> : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); + fprintf( pErr, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit ); fprintf( pErr, "\t-r : toggle resubstitution and dc-minimization [default = %s]\n", pPars->fResub? "resub": "dc-min" ); fprintf( pErr, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" ); fprintf( pErr, "\t-e : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" ); @@ -4423,6 +4455,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; int fCheck; int fComb; + int fImplic; int nPartSize; pNtk = Abc_FrameReadNtk(pAbc); @@ -4432,9 +4465,10 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fComb = 1; fCheck = 1; + fImplic = 0; nPartSize = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Pch" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Pcih" ) ) != EOF ) { switch ( c ) { @@ -4452,6 +4486,9 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'c': fComb ^= 1; break; + case 'i': + fImplic ^= 1; + break; default: goto usage; } @@ -4463,7 +4500,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; // compute the miter - pNtkRes = Abc_NtkMiter( pNtk1, pNtk2, fComb, nPartSize ); + pNtkRes = Abc_NtkMiter( pNtk1, pNtk2, fComb, nPartSize, fImplic ); if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); @@ -4482,10 +4519,11 @@ usage: strcpy( Buffer, "unused" ); else sprintf( Buffer, "%d", nPartSize ); - fprintf( pErr, "usage: miter [-P num] [-ch] <file1> <file2>\n" ); + fprintf( pErr, "usage: miter [-P num] [-cih] <file1> <file2>\n" ); fprintf( pErr, "\t computes the miter of the two circuits\n" ); fprintf( pErr, "\t-P num : output partition size [default = %s]\n", Buffer ); - fprintf( pErr, "\t-c : computes combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" ); + fprintf( pErr, "\t-c : toggles deriving combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" ); + fprintf( pErr, "\t-i : toggles deriving implication miter (file1 => file2) [default = %s]\n", fImplic? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\tfile1 : (optional) the file with the first network\n"); fprintf( pErr, "\tfile2 : (optional) the file with the second network\n"); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 6f5138c8..d69a7097 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -85,7 +85,7 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters ) printf( "Warning: %d registers in this network have don't-care init values.\n", nDontCares ); printf( "The don't-care are assumed to be 0. The result may not verify.\n" ); printf( "Use command \"print_latch\" to see the init values of registers.\n" ); - printf( "Use command \"init\" to change the values.\n" ); + printf( "Use command \"zero\" to convert or \"init\" to change the values.\n" ); } } // create the manager @@ -97,6 +97,9 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters ) pMan->nRegs = Abc_NtkLatchNum(pNtk); pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs ); // pMan->vFlopNums = NULL; +// pMan->vOnehots = Abc_NtkConverLatchNamesIntoNumbers( pNtk ); + if ( pNtk->vOnehots ) + pMan->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots ); } // transfer the pointers to the basic nodes Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan); @@ -974,7 +977,7 @@ int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVe if ( pNtk2 != NULL ) { // get the miter of the two networks - pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 ); + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0 ); if ( pMiter == NULL ) { printf( "Miter computation has failed.\n" ); @@ -1224,7 +1227,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetim int RetValue; // get the miter of the two networks - pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 ); + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0 ); if ( pMiter == NULL ) { printf( "Miter computation has failed.\n" ); @@ -1525,7 +1528,7 @@ Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose ) +Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose ) { extern Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose ); Abc_Ntk_t * pNtkAig; @@ -1573,6 +1576,67 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose SeeAlso [] ***********************************************************************/ +Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose ) +{ + Abc_Ntk_t * pNtkOn1, * pNtkOff1, * pNtkInter1, * pNtkInter; + Abc_Obj_t * pObj; + int i; + if ( Abc_NtkCoNum(pNtkOn) != Abc_NtkCoNum(pNtkOff) ) + { + printf( "Currently works only for networks with equal number of POs.\n" ); + return NULL; + } + if ( Abc_NtkCoNum(pNtkOn) == 1 ) + return Abc_NtkInterOne( pNtkOn, pNtkOff, fVerbose ); + // start the new newtork + pNtkInter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); + pNtkInter->pName = Extra_UtilStrsav(pNtkOn->pName); + Abc_NtkForEachPi( pNtkOn, pObj, i ) + Abc_NtkDupObj( pNtkInter, pObj, 1 ); + // process each POs separately + Abc_NtkForEachCo( pNtkOn, pObj, i ) + { + pNtkOn1 = Abc_NtkCreateCone( pNtkOn, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 1 ); + if ( Abc_ObjFaninC0(pObj) ) + Abc_ObjXorFaninC( Abc_NtkPo(pNtkOn1, 0), 0 ); + + pObj = Abc_NtkCo(pNtkOff, i); + pNtkOff1 = Abc_NtkCreateCone( pNtkOff, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 1 ); + if ( Abc_ObjFaninC0(pObj) ) + Abc_ObjXorFaninC( Abc_NtkPo(pNtkOff1, 0), 0 ); + + if ( Abc_NtkNodeNum(pNtkOn1) == 0 ) + pNtkInter1 = Abc_NtkDup( pNtkOn1 ); + else if ( Abc_NtkNodeNum(pNtkOff1) == 0 ) + { + pNtkInter1 = Abc_NtkDup( pNtkOff1 ); + Abc_ObjXorFaninC( Abc_NtkPo(pNtkInter1, 0), 0 ); + } + else + pNtkInter1 = Abc_NtkInterOne( pNtkOn1, pNtkOff1, fVerbose ); + Abc_NtkAppend( pNtkInter, pNtkInter1, 1 ); + + Abc_NtkDelete( pNtkOn1 ); + Abc_NtkDelete( pNtkOff1 ); + Abc_NtkDelete( pNtkInter1 ); + } + // return the network + if ( !Abc_NtkCheck( pNtkInter ) ) + fprintf( stdout, "Abc_NtkAttachBottom(): Network check has failed.\n" ); + return pNtkInter; +} + +/**Function************************************************************* + + Synopsis [Interplates two networks.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose ) { // extern Vec_Ptr_t * Aig_ManRegPartitionLinear( Aig_Man_t * pAig, int nPartSize ); diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c index 0b66c476..7c18ca2c 100644 --- a/src/base/abci/abcGen.c +++ b/src/base/abci/abcGen.c @@ -1,12 +1,12 @@ /**CFile**************************************************************** - FileName [abc_.c] + FileName [abcGen.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Network and node package.] - Synopsis [] + Synopsis [Procedures to generate various type of circuits.] Author [Alan Mishchenko] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: abcGen.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ @@ -545,6 +545,60 @@ void Abc_GenOneHot( char * pFileName, int nVars ) fclose( pFile ); } +/**Function************************************************************* + + Synopsis [Generates structure of L K-LUTs implementing an N-var function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_GenOneHotIntervals( char * pFileName, int nPis, int nRegs, Vec_Ptr_t * vOnehots ) +{ + Vec_Int_t * vLine; + FILE * pFile; + int i, j, k, iReg1, iReg2, Counter, Counter2, nDigitsIn, nDigitsOut; + pFile = fopen( pFileName, "w" ); + fprintf( pFile, "# One-hotness with %d vars and %d regs generated by ABC on %s\n", nPis, nRegs, Extra_TimeStamp() ); + fprintf( pFile, "# Used %d intervals of 1-hot registers: { ", Vec_PtrSize(vOnehots) ); + Counter = 0; + Vec_PtrForEachEntry( vOnehots, vLine, k ) + { + fprintf( pFile, "%d ", Vec_IntSize(vLine) ); + Counter += Vec_IntSize(vLine) * (Vec_IntSize(vLine) - 1) / 2; + } + fprintf( pFile, "}\n" ); + fprintf( pFile, ".model 1hot_%dvars_%dregs\n", nPis, nRegs ); + fprintf( pFile, ".inputs" ); + nDigitsIn = Extra_Base10Log( nPis+nRegs ); + for ( i = 0; i < nPis+nRegs; i++ ) + fprintf( pFile, " i%0*d", nDigitsIn, i ); + fprintf( pFile, "\n" ); + fprintf( pFile, ".outputs" ); + nDigitsOut = Extra_Base10Log( Counter ); + for ( i = 0; i < Counter; i++ ) + fprintf( pFile, " o%0*d", nDigitsOut, i ); + fprintf( pFile, "\n" ); + Counter2 = 0; + Vec_PtrForEachEntry( vOnehots, vLine, k ) + { + Vec_IntForEachEntry( vLine, iReg1, i ) + Vec_IntForEachEntryStart( vLine, iReg2, j, i+1 ) + { + fprintf( pFile, ".names i%0*d i%0*d o%0*d\n", nDigitsIn, nPis+iReg1, nDigitsIn, nPis+iReg2, nDigitsOut, Counter2 ); + fprintf( pFile, "11 0\n" ); + Counter2++; + } + } + assert( Counter == Counter2 ); + fprintf( pFile, ".end\n" ); + fprintf( pFile, "\n" ); + fclose( pFile ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index a054a474..3e3c9580 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -24,10 +24,10 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize ); +static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize, int fImplic ); static void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize ); static void Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter ); -static void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize ); +static void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize, int fImplic ); static void Abc_NtkAddFrame( Abc_Ntk_t * pNetNew, Abc_Ntk_t * pNet, int iFrame ); // to be exported @@ -50,7 +50,7 @@ static void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, i SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize ) +Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize, int fImplic ) { Abc_Ntk_t * pTemp = NULL; int fRemove1, fRemove2; @@ -63,7 +63,7 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int n fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0, 0)); fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0, 0)); if ( pNtk1 && pNtk2 ) - pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb, nPartSize ); + pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb, nPartSize, fImplic ); if ( fRemove1 ) Abc_NtkDelete( pNtk1 ); if ( fRemove2 ) Abc_NtkDelete( pNtk2 ); return pTemp; @@ -80,7 +80,7 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int n SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize ) +Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize, int fImplic ) { char Buffer[1000]; Abc_Ntk_t * pNtkMiter; @@ -97,7 +97,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, in Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize ); Abc_NtkMiterAddOne( pNtk1, pNtkMiter ); Abc_NtkMiterAddOne( pNtk2, pNtkMiter ); - Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize ); + Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize, fImplic ); Abc_AigCleanup(pNtkMiter->pManFunc); // make sure that everything is okay @@ -250,7 +250,7 @@ void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * p SeeAlso [] ***********************************************************************/ -void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize ) +void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize, int fImplic ) { Vec_Ptr_t * vPairs; Abc_Obj_t * pMiter, * pNode; @@ -285,7 +285,7 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt // add the miter if ( nPartSize <= 0 ) { - pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairs ); + pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairs, fImplic ); Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter ); Vec_PtrFree( vPairs ); } @@ -309,7 +309,7 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt Vec_PtrPush( vPairsPart, Vec_PtrEntry(vPairs, 2*iCur ) ); Vec_PtrPush( vPairsPart, Vec_PtrEntry(vPairs, 2*iCur+1) ); } - pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairsPart ); + pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairsPart, fImplic ); pNode = Abc_NtkCreatePo( pNtkMiter ); Abc_ObjAddFanin( pNode, pMiter ); // assign the name to the node diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index 239b155c..e5f028fe 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -468,6 +468,118 @@ void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk ) Vec_IntFree( vFanins ); Vec_IntFree( vFanouts ); } +/**Function************************************************************* + + Synopsis [Prints the distribution of fanins/fanouts in the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t * pNtk ) +{ + char Buffer[100]; + Abc_Obj_t * pNode; + Vec_Int_t * vFanins, * vFanouts; + int nFanins, nFanouts, nFaninsMax, nFanoutsMax, nFaninsAll, nFanoutsAll; + int i, k, nSizeMax; + + // determine the largest fanin and fanout + nFaninsMax = nFanoutsMax = 0; + nFaninsAll = nFanoutsAll = 0; + Abc_NtkForEachNode( pNtk, pNode, i ) + { + nFanins = Abc_ObjFaninNum(pNode); + if ( Abc_NtkIsNetlist(pNtk) ) + nFanouts = Abc_ObjFanoutNum( Abc_ObjFanout0(pNode) ); + else + nFanouts = Abc_ObjFanoutNum(pNode); + nFaninsAll += nFanins; + nFanoutsAll += nFanouts; + nFaninsMax = ABC_MAX( nFaninsMax, nFanins ); + nFanoutsMax = ABC_MAX( nFanoutsMax, nFanouts ); + } + + // allocate storage for fanin/fanout numbers + nSizeMax = ABC_MAX( 10 * (Extra_Base10Log(nFaninsMax) + 1), 10 * (Extra_Base10Log(nFanoutsMax) + 1) ); + vFanins = Vec_IntStart( nSizeMax ); + vFanouts = Vec_IntStart( nSizeMax ); + + // count the number of fanins and fanouts + Abc_NtkForEachNode( pNtk, pNode, i ) + { + nFanins = Abc_ObjFaninNum(pNode); + if ( Abc_NtkIsNetlist(pNtk) ) + nFanouts = Abc_ObjFanoutNum( Abc_ObjFanout0(pNode) ); + else + nFanouts = Abc_ObjFanoutNum(pNode); +// nFanouts = Abc_NodeMffcSize(pNode); + + if ( nFanins < 10 ) + Vec_IntAddToEntry( vFanins, nFanins, 1 ); + else if ( nFanins < 100 ) + Vec_IntAddToEntry( vFanins, 10 + nFanins/10, 1 ); + else if ( nFanins < 1000 ) + Vec_IntAddToEntry( vFanins, 20 + nFanins/100, 1 ); + else if ( nFanins < 10000 ) + Vec_IntAddToEntry( vFanins, 30 + nFanins/1000, 1 ); + else if ( nFanins < 100000 ) + Vec_IntAddToEntry( vFanins, 40 + nFanins/10000, 1 ); + else if ( nFanins < 1000000 ) + Vec_IntAddToEntry( vFanins, 50 + nFanins/100000, 1 ); + else if ( nFanins < 10000000 ) + Vec_IntAddToEntry( vFanins, 60 + nFanins/1000000, 1 ); + + if ( nFanouts < 10 ) + Vec_IntAddToEntry( vFanouts, nFanouts, 1 ); + else if ( nFanouts < 100 ) + Vec_IntAddToEntry( vFanouts, 10 + nFanouts/10, 1 ); + else if ( nFanouts < 1000 ) + Vec_IntAddToEntry( vFanouts, 20 + nFanouts/100, 1 ); + else if ( nFanouts < 10000 ) + Vec_IntAddToEntry( vFanouts, 30 + nFanouts/1000, 1 ); + else if ( nFanouts < 100000 ) + Vec_IntAddToEntry( vFanouts, 40 + nFanouts/10000, 1 ); + else if ( nFanouts < 1000000 ) + Vec_IntAddToEntry( vFanouts, 50 + nFanouts/100000, 1 ); + else if ( nFanouts < 10000000 ) + Vec_IntAddToEntry( vFanouts, 60 + nFanouts/1000000, 1 ); + } + + fprintf( pFile, "The distribution of fanins and fanouts in the network:\n" ); + fprintf( pFile, " Number Nodes with fanin Nodes with fanout\n" ); + for ( k = 0; k < nSizeMax; k++ ) + { + if ( vFanins->pArray[k] == 0 && vFanouts->pArray[k] == 0 ) + continue; + if ( k < 10 ) + fprintf( pFile, "%15d : ", k ); + else + { + sprintf( Buffer, "%d - %d", (int)pow(10, k/10) * (k%10), (int)pow(10, k/10) * (k%10+1) - 1 ); + fprintf( pFile, "%15s : ", Buffer ); + } + if ( vFanins->pArray[k] == 0 ) + fprintf( pFile, " " ); + else + fprintf( pFile, "%12d ", vFanins->pArray[k] ); + fprintf( pFile, " " ); + if ( vFanouts->pArray[k] == 0 ) + fprintf( pFile, " " ); + else + fprintf( pFile, "%12d ", vFanouts->pArray[k] ); + fprintf( pFile, "\n" ); + } + Vec_IntFree( vFanins ); + Vec_IntFree( vFanouts ); + + fprintf( pFile, "Fanins: Max = %d. Ave = %.2f. Fanouts: Max = %d. Ave = %.2f.\n", + nFaninsMax, 1.0*nFaninsAll/Abc_NtkNodeNum(pNtk), + nFanoutsMax, 1.0*nFanoutsAll/Abc_NtkNodeNum(pNtk) ); +} /**Function************************************************************* diff --git a/src/base/abci/abcQuant.c b/src/base/abci/abcQuant.c index 0f2bd72f..24981d1c 100644 --- a/src/base/abci/abcQuant.c +++ b/src/base/abci/abcQuant.c @@ -187,7 +187,7 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose ) Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pObj) ); Vec_PtrPush( vPairs, Abc_NtkPi(pNtkNew, i+nLatches) ); } - pMiter = Abc_AigMiter( pNtkNew->pManFunc, vPairs ); + pMiter = Abc_AigMiter( pNtkNew->pManFunc, vPairs, 0 ); Vec_PtrFree( vPairs ); // add the primary output Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), Abc_ObjNot(pMiter) ); diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c index 92adc718..80d234f1 100644 --- a/src/base/abci/abcRr.c +++ b/src/base/abci/abcRr.c @@ -354,7 +354,7 @@ int Abc_NtkRRProve( Abc_RRMan_t * p ) Abc_NtkRRUpdate( pWndCopy, p->pNode->pCopy->pCopy, p->pFanin->pCopy->pCopy, p->pFanout? p->pFanout->pCopy->pCopy : NULL ); if ( !Abc_NtkIsDfsOrdered(pWndCopy) ) Abc_NtkReassignIds(pWndCopy); - p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1, 0 ); + p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1, 0, 0 ); Abc_NtkDelete( pWndCopy ); clk = clock(); RetValue = Abc_NtkMiterProve( &p->pMiter, p->pParams ); diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index c77f8dea..744d9c95 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -260,7 +260,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos ) { Abc_NtkDupObj( pNtk1, pObj, 0 ); Abc_ObjAddFanin( pObj->pCopy, Abc_ObjChild0Copy(pObj) ); - Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj->pCopy), NULL ); + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL ); } } else @@ -271,6 +271,8 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos ) Abc_NtkForEachCo( pNtk2, pObj, i ) { iNodeId = Nm_ManFindIdByNameTwoTypes( pNtk1->pManName, Abc_ObjName(pObj), ABC_OBJ_PO, ABC_OBJ_BI ); +// if ( iNodeId < 0 ) +// continue; assert( iNodeId >= 0 ); pObjOld = Abc_NtkObj( pNtk1, iNodeId ); // derive the new driver diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 9c9bbcfd..1d72a767 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -52,7 +52,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI int RetValue; // get the miter of the two networks - pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0 ); + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0, 0 ); if ( pMiter == NULL ) { printf( "Miter computation has failed.\n" ); @@ -120,7 +120,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV int RetValue; // get the miter of the two networks - pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0 ); + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0, 0 ); if ( pMiter == NULL ) { printf( "Miter computation has failed.\n" ); @@ -225,7 +225,7 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in assert( nPartSize > 0 ); // get the miter of the two networks - pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, nPartSize ); + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, nPartSize, 0 ); if ( pMiter == NULL ) { printf( "Miter computation has failed.\n" ); @@ -342,7 +342,7 @@ void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds // pParams->fVerbose = 1; // get the miter of the two networks - pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 1 ); + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 1, 0 ); if ( pMiter == NULL ) { printf( "Miter computation has failed.\n" ); @@ -456,7 +456,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI int RetValue; // get the miter of the two networks - pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 ); + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0 ); if ( pMiter == NULL ) { printf( "Miter computation has failed.\n" ); @@ -538,7 +538,7 @@ int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFr int RetValue; // get the miter of the two networks - pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 ); + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0 ); if ( pMiter == NULL ) { printf( "Miter computation has failed.\n" ); |