diff options
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 400 | ||||
-rw-r--r-- | src/base/abci/abcAuto.c | 2 | ||||
-rw-r--r-- | src/base/abci/abcCas.c | 111 | ||||
-rw-r--r-- | src/base/abci/abcClpBdd.c | 2 | ||||
-rw-r--r-- | src/base/abci/abcDsd.c | 2 | ||||
-rw-r--r-- | src/base/abci/abcMiter.c | 14 | ||||
-rw-r--r-- | src/base/abci/abcPlace.c | 38 | ||||
-rw-r--r-- | src/base/abci/abcQuant.c | 389 | ||||
-rw-r--r-- | src/base/abci/abcRewrite.c | 8 | ||||
-rw-r--r-- | src/base/abci/abcStrash.c | 2 | ||||
-rw-r--r-- | src/base/abci/abcUnate.c | 2 | ||||
-rw-r--r-- | src/base/abci/abcUnreach.c | 10 | ||||
-rw-r--r-- | src/base/abci/module.make | 2 |
13 files changed, 945 insertions, 37 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index e7f8c8ea..ae00ce5c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -67,6 +67,7 @@ static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandRestructure ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandResubstitute ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRr ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCascade ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandComb ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -96,6 +97,10 @@ static int Abc_CommandGen ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandDouble ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandQuaVar ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandQuaRel ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandQuaReach ( Abc_Frame_t * pAbc, int argc, char ** argv ); + static int Abc_CommandIStrash ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandICut ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -203,6 +208,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) // Cmd_CommandAdd( pAbc, "Synthesis", "restructure", Abc_CommandRestructure, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "resub", Abc_CommandResubstitute, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "rr", Abc_CommandRr, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "cascade", Abc_CommandCascade, 1 ); Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 ); Cmd_CommandAdd( pAbc, "Various", "comb", Abc_CommandComb, 1 ); @@ -232,6 +238,10 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "double", Abc_CommandDouble, 1 ); Cmd_CommandAdd( pAbc, "Various", "test", Abc_CommandTest, 0 ); + Cmd_CommandAdd( pAbc, "Various", "qvar", Abc_CommandQuaVar, 1 ); + Cmd_CommandAdd( pAbc, "Various", "qrel", Abc_CommandQuaRel, 1 ); + Cmd_CommandAdd( pAbc, "Various", "qreach", Abc_CommandQuaReach, 1 ); + Cmd_CommandAdd( pAbc, "New AIG", "istrash", Abc_CommandIStrash, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "icut", Abc_CommandICut, 0 ); Cmd_CommandAdd( pAbc, "New AIG", "irw", Abc_CommandIRewrite, 1 ); @@ -3234,6 +3244,109 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandCascade( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c, nLutSize; + int fCheck; + int fVerbose; + extern Abc_Ntk_t * Abc_NtkCascade( Abc_Ntk_t * pNtk, int nLutSize, int fCheck, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nLutSize = 12; + fCheck = 0; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Kcvh" ) ) != EOF ) + { + switch ( c ) + { + case 'K': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" ); + goto usage; + } + nLutSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLutSize < 0 ) + goto usage; + break; + case 'c': + fCheck ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "Can only collapse a logic network or an AIG.\n" ); + return 1; + } + + // get the new network + if ( Abc_NtkIsStrash(pNtk) ) + pNtkRes = Abc_NtkCascade( pNtk, nLutSize, fCheck, fVerbose ); + else + { + pNtk = Abc_NtkStrash( pNtk, 0, 0 ); + pNtkRes = Abc_NtkCascade( pNtk, nLutSize, fCheck, fVerbose ); + Abc_NtkDelete( pNtk ); + } + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Cascade synthesis has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: cascade [-K <num>] [-cvh]\n" ); + fprintf( pErr, "\t performs LUT cascade synthesis for the current network\n" ); + fprintf( pErr, "\t-K num : the number of LUT inputs [default = %d]\n", nLutSize ); + fprintf( pErr, "\t-c : check equivalence after synthesis [default = %s]\n", fCheck? "yes": "no" ); + fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "\t \n"); + fprintf( pErr, " A lookup-table cascade is a programmable architecture developed by\n"); + fprintf( pErr, " Professor Tsutomu Sasao (sasao@cse.kyutech.ac.jp) at Kyushu Institute\n"); + fprintf( pErr, " of Technology. This work received Takeda Techno-Entrepreneurship Award:\n"); + fprintf( pErr, " http://www.lsi-cad.com/sasao/photo/takeda.html\n"); + fprintf( pErr, "\t \n"); + return 1; +} + /**Function************************************************************* @@ -5536,6 +5649,293 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandQuaVar( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c, iVar, fVerbose, RetValue; + extern int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int iVar, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + iVar = 0; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF ) + { + switch ( c ) + { + case 'I': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + iVar = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( iVar < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( Abc_NtkGetChoiceNum( pNtk ) ) + { + fprintf( pErr, "This command cannot be applied to an AIG with choice nodes.\n" ); + return 1; + } + + // get the strashed network + pNtkRes = Abc_NtkStrash( pNtk, 0, 1 ); + RetValue = Abc_NtkQuantify( pNtkRes, iVar, fVerbose ); + // clean temporary storage for the cofactors + Abc_NtkCleanData( pNtkRes ); + Abc_AigCleanup( pNtkRes->pManFunc ); + // check the result + if ( !RetValue ) + { + fprintf( pErr, "Command has failed.\n" ); + return 0; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: qvar [-I num] [-vh]\n" ); + fprintf( pErr, "\t quantifies one variable using the AIG\n" ); + fprintf( pErr, "\t-I num : the zero-based index of a variable to quantify [default = %d]\n", iVar ); + fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandQuaRel( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c, iVar, fInputs, fVerbose; + extern Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + iVar = 0; + fInputs = 1; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Iqvh" ) ) != EOF ) + { + switch ( c ) + { + case 'I': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + iVar = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( iVar < 0 ) + goto usage; + break; + case 'q': + fInputs ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( Abc_NtkGetChoiceNum( pNtk ) ) + { + fprintf( pErr, "This command cannot be applied to an AIG with choice nodes.\n" ); + return 1; + } + if ( Abc_NtkIsComb(pNtk) ) + { + fprintf( pErr, "This command works only for sequential circuits.\n" ); + return 1; + } + + // get the strashed network + if ( !Abc_NtkIsStrash(pNtk) ) + { + pNtk = Abc_NtkStrash( pNtk, 0, 1 ); + pNtkRes = Abc_NtkTransRel( pNtk, fInputs, fVerbose ); + Abc_NtkDelete( pNtk ); + } + else + pNtkRes = Abc_NtkTransRel( pNtk, fInputs, fVerbose ); + // check if the result is available + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Command has failed.\n" ); + return 0; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: qrel [-qvh]\n" ); + fprintf( pErr, "\t computes transition relation of the sequential network\n" ); +// fprintf( pErr, "\t-I num : the zero-based index of a variable to quantify [default = %d]\n", iVar ); + fprintf( pErr, "\t-q : perform quantification of inputs [default = %s]\n", fInputs? "yes": "no" ); + fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandQuaReach( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c, nIters, fVerbose; + extern Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtk, int nIters, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nIters = 256; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF ) + { + switch ( c ) + { + case 'I': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nIters = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nIters < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( Abc_NtkGetChoiceNum( pNtk ) ) + { + fprintf( pErr, "This command cannot be applied to an AIG with choice nodes.\n" ); + return 1; + } + if ( !Abc_NtkIsComb(pNtk) ) + { + fprintf( pErr, "This command works only for combinational transition relations.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } + if ( Abc_NtkPoNum(pNtk) > 1 ) + { + fprintf( pErr, "The transition relation should have one output.\n" ); + return 1; + } + if ( Abc_NtkPiNum(pNtk) % 2 != 0 ) + { + fprintf( pErr, "The transition relation should have an even number of inputs.\n" ); + return 1; + } + + pNtkRes = Abc_NtkReachability( pNtk, nIters, fVerbose ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Command has failed.\n" ); + return 0; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: qreach [-I num] [-vh]\n" ); + fprintf( pErr, "\t computes unreachable states using AIG-based quantification\n" ); + fprintf( pErr, "\t assumes that the current network is a transition relation\n" ); + fprintf( pErr, "\t assumes that the initial state is composed of all zeros\n" ); + fprintf( pErr, "\t-I num : the number of image computations to perform [default = %d]\n", nIters ); + fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* diff --git a/src/base/abci/abcAuto.c b/src/base/abci/abcAuto.c index 3b307ac2..40212c17 100644 --- a/src/base/abci/abcAuto.c +++ b/src/base/abci/abcAuto.c @@ -74,7 +74,7 @@ void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose ) // print the size of the BDDs if ( fVerbose ) - printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); // allocate additional variables for ( i = 0; i < nInputs; i++ ) diff --git a/src/base/abci/abcCas.c b/src/base/abci/abcCas.c new file mode 100644 index 00000000..4ed7a774 --- /dev/null +++ b/src/base/abci/abcCas.c @@ -0,0 +1,111 @@ +/**CFile**************************************************************** + + FileName [abcCas.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Decomposition of shared BDDs into LUT cascade.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcCas.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +/* + This LUT cascade synthesis algorithm is described in the paper: + A. Mishchenko and T. Sasao, "Encoding of Boolean functions and its + application to LUT cascade synthesis", Proc. IWLS '02, pp. 115-120. + http://www.eecs.berkeley.edu/~alanmi/publications/2002/iwls02_enc.pdf +*/ + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern int Abc_CascadeExperiment( char * pFileGeneric, DdManager * dd, DdNode ** pOutputs, int nInputs, int nOutputs, int nLutSize, int fCheck, int fVerbose ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkCascade( Abc_Ntk_t * pNtk, int nLutSize, int fCheck, int fVerbose ) +{ + DdManager * dd; + DdNode ** ppOutputs; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pNode; + char * pFileGeneric; + int fBddSizeMax = 500000; + int fReorder = 1; + int i, clk = clock(); + + assert( Abc_NtkIsStrash(pNtk) ); + // compute the global BDDs + if ( Abc_NtkBuildGlobalBdds(pNtk, fBddSizeMax, 1, fReorder, fVerbose) == NULL ) + return NULL; + + if ( fVerbose ) + { + DdManager * dd = Abc_NtkGlobalBddMan( pNtk ); + printf( "Shared BDD size = %6d nodes. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + PRT( "BDD construction time", clock() - clk ); + } + + // collect global BDDs + dd = Abc_NtkGlobalBddMan( pNtk ); + ppOutputs = ALLOC( DdNode *, Abc_NtkCoNum(pNtk) ); + Abc_NtkForEachCo( pNtk, pNode, i ) + ppOutputs[i] = Abc_ObjGlobalBdd(pNode); + + // call the decomposition + pFileGeneric = Extra_FileNameGeneric( pNtk->pSpec ); + if ( !Abc_CascadeExperiment( pFileGeneric, dd, ppOutputs, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), nLutSize, fCheck, fVerbose ) ) + { + // the LUT size is too small + } + + // for now, duplicate the network + pNtkNew = Abc_NtkDup( pNtk ); + + // cleanup + Abc_NtkFreeGlobalBdds( pNtk, 1 ); + free( ppOutputs ); + free( pFileGeneric ); + +// if ( pNtk->pExdc ) +// pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); + // make sure that everything is okay + if ( !Abc_NtkCheck( pNtkNew ) ) + { + printf( "Abc_NtkCollapse: The network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcClpBdd.c b/src/base/abci/abcClpBdd.c index ce67aff7..341ff5b0 100644 --- a/src/base/abci/abcClpBdd.c +++ b/src/base/abci/abcClpBdd.c @@ -54,7 +54,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i if ( fVerbose ) { DdManager * dd = Abc_NtkGlobalBddMan( pNtk ); - printf( "The shared BDD size is %d nodes. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + printf( "Shared BDD size = %6d nodes. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); PRT( "BDD construction time", clock() - clk ); } diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c index 200f4eec..235c3672 100644 --- a/src/base/abci/abcDsd.c +++ b/src/base/abci/abcDsd.c @@ -62,7 +62,7 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool if ( dd == NULL ) return NULL; if ( fVerbose ) - printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); // transform the result of mapping into a BDD network pNtkNew = Abc_NtkDsdInternal( pNtk, fVerbose, fPrint, fShort ); Extra_StopManager( dd ); diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index 15a81723..cbd330da 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -294,7 +294,7 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) +Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOr, int fCompl2 ) { char Buffer[1000]; Abc_Ntk_t * pNtkMiter; @@ -313,7 +313,8 @@ Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) // start the new network pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); - sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName ); +// sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName ); + sprintf( Buffer, "product" ); pNtkMiter->pName = Extra_UtilStrsav(Buffer); // perform strashing @@ -324,10 +325,13 @@ Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) pRoot1 = Abc_NtkPo(pNtk1,0); pRoot2 = Abc_NtkPo(pNtk2,0); pOutput1 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot1)->pCopy, Abc_ObjFaninC0(pRoot1) ); - pOutput2 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot2)->pCopy, Abc_ObjFaninC0(pRoot2) ); - + pOutput2 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot2)->pCopy, Abc_ObjFaninC0(pRoot2) ^ fCompl2 ); + // create the miter of the two outputs - pMiter = Abc_AigAnd( pNtkMiter->pManFunc, pOutput1, pOutput2 ); + if ( fOr ) + pMiter = Abc_AigOr( pNtkMiter->pManFunc, pOutput1, pOutput2 ); + else + pMiter = Abc_AigAnd( pNtkMiter->pManFunc, pOutput1, pOutput2 ); Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter ); // make sure that everything is okay diff --git a/src/base/abci/abcPlace.c b/src/base/abci/abcPlace.c index 5ceffd6f..87c99e99 100644 --- a/src/base/abci/abcPlace.c +++ b/src/base/abci/abcPlace.c @@ -120,7 +120,7 @@ float Abc_PlaceEvaluateCut( Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins ) SeeAlso [] ***********************************************************************/ -void Abc_PlaceUpdate( Vec_Ptr_t * vUpdates, int nNodesOld ) +void Abc_PlaceUpdate( Vec_Ptr_t * vAddedCells, Vec_Ptr_t * vUpdatedNets ) { Abc_Obj_t * pObj, * pFanin; int i, k; @@ -130,24 +130,26 @@ void Abc_PlaceUpdate( Vec_Ptr_t * vUpdates, int nNodesOld ) vCells = Vec_PtrAlloc( 16 ); vNets = Vec_PtrAlloc( 32 ); - // go through the modified nodes - Vec_PtrForEachEntry( vUpdates, pObj, i ) + // go through the new nodes + Vec_PtrForEachEntry( vAddedCells, pObj, i ) { - if ( pObj->Id > nNodesOld ) // pObj is a new node - { - Abc_PlaceCreateCell( pObj, 1 ); - Abc_PlaceUpdateNet( pObj ); - - // add the new cell and its fanin nets to temporary storage - Vec_PtrPush( vCells, &(cells[pObj->Id]) ); - Abc_ObjForEachFanin( pObj, pFanin, k ) - Vec_PtrPushUnique( vNets, &(nets[pFanin->Id]) ); - } - else // pObj is an old node - { - Abc_PlaceUpdateNet( Abc_ObjFanin0(pObj) ); - Abc_PlaceUpdateNet( Abc_ObjFanin1(pObj) ); - } + assert( !Abc_ObjIsComplement(pObj) ); + Abc_PlaceCreateCell( pObj, 1 ); + Abc_PlaceUpdateNet( pObj ); + + // add the new cell and its fanin nets to temporary storage + Vec_PtrPush( vCells, &(cells[pObj->Id]) ); + Abc_ObjForEachFanin( pObj, pFanin, k ) + Vec_PtrPushUnique( vNets, &(nets[pFanin->Id]) ); + } + + // go through the modified nets + Vec_PtrForEachEntry( vUpdatedNets, pObj, i ) + { + assert( !Abc_ObjIsComplement(pObj) ); + if ( Abc_ObjType(pObj) == ABC_OBJ_NONE ) // dead node + continue; + Abc_PlaceUpdateNet( pObj ); } // update the placement diff --git a/src/base/abci/abcQuant.c b/src/base/abci/abcQuant.c new file mode 100644 index 00000000..77d640c2 --- /dev/null +++ b/src/base/abci/abcQuant.c @@ -0,0 +1,389 @@ +/**CFile**************************************************************** + + FileName [abcQuant.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [AIG-based variable quantification.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcQuant.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Existentially quantifies one variable.] + + Description [] + + SideEffects [This procedure creates dangling nodes in the AIG.] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int iVar, int fVerbose ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pObj, * pNext, * pFanin; + int i; + assert( Abc_NtkIsStrash(pNtk) ); + assert( iVar < Abc_NtkCiNum(pNtk) ); + + // collect the internal nodes + pObj = Abc_NtkCi( pNtk, iVar ); + vNodes = Abc_NtkDfsReverseNodes( pNtk, &pObj, 1 ); + + // assign the cofactors of the CI node to be constants + pObj->pCopy = Abc_ObjNot( Abc_AigConst1(pNtk) ); + pObj->pData = Abc_AigConst1(pNtk); + + // quantify the nodes + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + for ( pNext = pObj? pObj->pCopy : pObj; pObj; pObj = pNext, pNext = pObj? pObj->pCopy : pObj ) + { + pFanin = Abc_ObjFanin0(pObj); + if ( !Abc_NodeIsTravIdCurrent(pFanin) ) + pFanin->pCopy = pFanin->pData = pFanin; + pFanin = Abc_ObjFanin1(pObj); + if ( !Abc_NodeIsTravIdCurrent(pFanin) ) + pFanin->pCopy = pFanin->pData = pFanin; + pObj->pCopy = Abc_AigAnd( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); + pObj->pData = Abc_AigAnd( pNtk->pManFunc, Abc_ObjChild0Data(pObj), Abc_ObjChild1Data(pObj) ); + } + } + Vec_PtrFree( vNodes ); + + // update the affected COs + Abc_NtkForEachCo( pNtk, pObj, i ) + { + if ( !Abc_NodeIsTravIdCurrent(pObj) ) + continue; + pFanin = Abc_ObjFanin0(pObj); + // get the result of quantification + pNext = Abc_AigOr( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) ); + pNext = Abc_ObjNotCond( pNext, Abc_ObjFaninC0(pObj) ); + if ( Abc_ObjRegular(pNext) == pFanin ) + continue; + // update the fanins of the CO + Abc_ObjPatchFanin( pObj, pFanin, pNext ); +// if ( Abc_ObjFanoutNum(pFanin) == 0 ) +// Abc_AigDeleteNode( pNtk->pManFunc, pFanin ); + } + + // make sure the node has no fanouts +// pObj = Abc_NtkCi( pNtk, iVar ); +// assert( Abc_ObjFanoutNum(pObj) == 0 ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Constructs the transition relation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose ) +{ + char Buffer[1000]; + Vec_Ptr_t * vPairs; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj, * pMiter; + int i, nLatches; + + assert( Abc_NtkIsStrash(pNtk) ); + assert( Abc_NtkLatchNum(pNtk) ); + nLatches = Abc_NtkLatchNum(pNtk); + // start the network + pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); + // duplicate the name and the spec + sprintf( Buffer, "%s_TR", pNtk->pName ); + pNtkNew->pName = Extra_UtilStrsav(pNtk->pName); +// pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec); + Abc_NtkCleanCopy( pNtk ); + // create current state variables + Abc_NtkForEachLatchOutput( pNtk, pObj, i ) + { + pObj->pCopy = Abc_NtkCreatePi(pNtkNew); + Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL ); + } + // create next state variables + Abc_NtkForEachLatchInput( pNtk, pObj, i ) + Abc_ObjAssignName( Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj), NULL ); + // create PI variables + Abc_NtkForEachPi( pNtk, pObj, i ) + Abc_NtkDupObj( pNtkNew, pObj, 1 ); + // restrash the nodes (assuming a topological order of the old network) + Abc_NtkForEachNode( pNtk, pObj, i ) + pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); + // create the function of the primary output + assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) ); + vPairs = Vec_PtrAlloc( 2*nLatches ); + Abc_NtkForEachLatchInput( pNtk, pObj, i ) + { + Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pObj) ); + Vec_PtrPush( vPairs, Abc_NtkPi(pNtkNew, i+nLatches) ); + } + pMiter = Abc_AigMiter( pNtkNew->pManFunc, vPairs ); + Vec_PtrFree( vPairs ); + // add the primary output + Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), Abc_ObjNot(pMiter) ); + Abc_ObjAssignName( Abc_NtkPo(pNtkNew,0), "rel", NULL ); + + // quantify inputs + if ( fInputs ) + { + assert( Abc_NtkPiNum(pNtkNew) == Abc_NtkPiNum(pNtk) + 2*nLatches ); + for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- ) + Abc_NtkQuantify( pNtkNew, i, fVerbose ); + Abc_NtkCleanData( pNtkNew ); + Abc_AigCleanup( pNtkNew->pManFunc ); + for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- ) + { + pObj = Abc_NtkPi( pNtkNew, i ); + assert( Abc_ObjFanoutNum(pObj) == 0 ); + Abc_NtkDeleteObj( pObj ); + } + } + + // make sure that everything is okay + if ( !Abc_NtkCheck( pNtkNew ) ) + { + printf( "Abc_NtkTransRel: The network check has failed.\n" ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + return pNtkNew; +} + + +/**Function************************************************************* + + Synopsis [Performs one image computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkInitialState( Abc_Ntk_t * pNtk ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pMiter; + int i, nVars = Abc_NtkPiNum(pNtk)/2; + assert( Abc_NtkIsStrash(pNtk) ); + // start the new network + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); + // compute the all-zero state in terms of the CS variables + pMiter = Abc_AigConst1(pNtkNew); + for ( i = 0; i < nVars; i++ ) + pMiter = Abc_AigAnd( pNtkNew->pManFunc, pMiter, Abc_ObjNot( Abc_NtkPi(pNtkNew, i) ) ); + // add the PO + Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), pMiter ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Swaps current state and next state variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkSwapVariables( Abc_Ntk_t * pNtk ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pMiter, * pObj, * pObj0, * pObj1; + int i, nVars = Abc_NtkPiNum(pNtk)/2; + assert( Abc_NtkIsStrash(pNtk) ); + // start the new network + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); + // update the PIs + for ( i = 0; i < nVars; i++ ) + { + pObj0 = Abc_NtkPi( pNtk, i ); + pObj1 = Abc_NtkPi( pNtk, i+nVars ); + pMiter = pObj0->pCopy; + pObj0->pCopy = pObj1->pCopy; + pObj1->pCopy = pMiter; + } + // restrash + Abc_NtkForEachNode( pNtk, pObj, i ) + pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); + // add the PO + pMiter = Abc_ObjChild0Copy( Abc_NtkPo(pNtk,0) ); + Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), pMiter ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Performs reachability analisys.] + + Description [Assumes that the input is the transition relation.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose ) +{ + Abc_Obj_t * pObj; + Abc_Ntk_t * pNtkFront, * pNtkReached, * pNtkNext, * pNtkTemp; + int clk, i, v, nVars, nNodesOld, nNodesNew, nNodesPrev; + int fFixedPoint = 0; + int fSynthesis = 1; + + assert( Abc_NtkIsStrash(pNtkRel) ); + assert( Abc_NtkLatchNum(pNtkRel) == 0 ); + assert( Abc_NtkPiNum(pNtkRel) % 2 == 0 ); + + // compute the network composed of the initial states + pNtkFront = Abc_NtkInitialState( pNtkRel ); + pNtkReached = Abc_NtkDup( pNtkFront ); +//Abc_NtkShow( pNtkReached, 0, 0, 0 ); + + if ( fVerbose ) + printf( "Transition relation = %6d.\n", Abc_NtkNodeNum(pNtkRel) ); + + // perform iterations of reachability analysis + nNodesPrev = Abc_NtkNodeNum(pNtkFront); + nVars = Abc_NtkPiNum(pNtkRel)/2; + for ( i = 0; i < nIters; i++ ) + { + clk = clock(); + // get the set of next states + pNtkNext = Abc_NtkMiterAnd( pNtkRel, pNtkFront, 0, 0 ); + Abc_NtkDelete( pNtkFront ); + // quantify the current state variables + for ( v = 0; v < nVars; v++ ) + { + Abc_NtkQuantify( pNtkNext, v, fVerbose ); + if ( fSynthesis && (v % 3 == 2) ) + { + Abc_NtkCleanData( pNtkNext ); + Abc_AigCleanup( pNtkNext->pManFunc ); + + Abc_NtkRewrite( pNtkNext, 0, 0, 0, 0, 0 ); + pNtkNext = Abc_NtkBalance( pNtkTemp = pNtkNext, 0, 0, 0 ); + Abc_NtkDelete( pNtkTemp ); + } + } + Abc_NtkCleanData( pNtkNext ); + Abc_AigCleanup( pNtkNext->pManFunc ); + if ( fSynthesis ) + { + Abc_NtkRewrite( pNtkNext, 0, 0, 0, 0, 0 ); + pNtkNext = Abc_NtkBalance( pNtkTemp = pNtkNext, 0, 0, 0 ); + Abc_NtkDelete( pNtkTemp ); + + Abc_NtkRewrite( pNtkNext, 0, 0, 0, 0, 0 ); + Abc_NtkRefactor( pNtkReached, 10, 16, 0, 0, 0, 0 ); + pNtkNext = Abc_NtkBalance( pNtkTemp = pNtkNext, 0, 0, 0 ); + Abc_NtkDelete( pNtkTemp ); + } + // map the next states into the current states + pNtkNext = Abc_NtkSwapVariables( pNtkTemp = pNtkNext ); + Abc_NtkDelete( pNtkTemp ); + // check the termination condition + if ( Abc_ObjFanin0(Abc_NtkPo(pNtkNext,0)) == Abc_AigConst1(pNtkNext) ) + { + fFixedPoint = 1; + printf( "Fixed point is reached!\n" ); + Abc_NtkDelete( pNtkNext ); + break; + } + // compute new front + pNtkFront = Abc_NtkMiterAnd( pNtkNext, pNtkReached, 0, 1 ); + Abc_NtkDelete( pNtkNext ); + // add the reached states + pNtkReached = Abc_NtkMiterAnd( pNtkTemp = pNtkReached, pNtkFront, 1, 0 ); + Abc_NtkDelete( pNtkTemp ); + // compress the size of Front + nNodesOld = Abc_NtkNodeNum(pNtkFront); + if ( fSynthesis ) + { + Abc_NtkRewrite( pNtkFront, 0, 0, 0, 0, 0 ); + pNtkFront = Abc_NtkBalance( pNtkTemp = pNtkFront, 0, 0, 0 ); + Abc_NtkDelete( pNtkTemp ); + + Abc_NtkRewrite( pNtkReached, 0, 0, 0, 0, 0 ); + pNtkReached = Abc_NtkBalance( pNtkTemp = pNtkReached, 0, 0, 0 ); + Abc_NtkDelete( pNtkTemp ); + } + nNodesNew = Abc_NtkNodeNum(pNtkFront); + // print statistics + if ( fVerbose ) + { + printf( "I = %3d : Reached = %6d Front = %6d FrontM = %6d %6.2f %% ", + i + 1, Abc_NtkNodeNum(pNtkReached), nNodesOld, nNodesNew, 100.0*(nNodesNew-nNodesPrev)/nNodesNew ); + PRT( "T", clock() - clk ); + } + nNodesPrev = Abc_NtkNodeNum(pNtkFront); + } + if ( !fFixedPoint ) + fprintf( stdout, "Reachability analysis stopped after %d iterations.\n", nIters ); + + // report the stats + if ( fVerbose ) + { +// nMints = 1; +// fprintf( stdout, "The estimated number of minterms in the reachable state set = %d. (%6.2f %%)\n", nMints, 100.0*nMints/(1<<Abc_NtkLatchNum(pNtk)) ); + } + + // complement the output to represent the set of unreachable states + Abc_ObjXorFaninC( Abc_NtkPo(pNtkReached,0), 0 ); + + // remove next state variables + for ( i = 2*nVars - 1; i >= nVars; i-- ) + { + pObj = Abc_NtkPi( pNtkReached, i ); + assert( Abc_ObjFanoutNum(pObj) == 0 ); + Abc_NtkDeleteObj( pObj ); + } + + // make sure that everything is okay + if ( !Abc_NtkCheck( pNtkReached ) ) + { + printf( "Abc_NtkReachability: The network check has failed.\n" ); + Abc_NtkDelete( pNtkReached ); + return NULL; + } + return pNtkReached; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c index a3209275..3d06dddf 100644 --- a/src/base/abci/abcRewrite.c +++ b/src/base/abci/abcRewrite.c @@ -38,7 +38,7 @@ static void Abc_ManShowCutCone( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves ); extern void Abc_PlaceBegin( Abc_Ntk_t * pNtk ); extern void Abc_PlaceEnd( Abc_Ntk_t * pNtk ); -extern void Abc_PlaceUpdate( Vec_Ptr_t * vUpdates, int nNodesOld ); +extern void Abc_PlaceUpdate( Vec_Ptr_t * vAddedCells, Vec_Ptr_t * vUpdatedNets ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -61,7 +61,7 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerb Cut_Man_t * pManCut; Rwr_Man_t * pManRwr; Abc_Obj_t * pNode; - Vec_Ptr_t * vUpdates = NULL; + Vec_Ptr_t * vAddedCells = NULL, * vUpdatedNets = NULL; Dec_Graph_t * pGraph; int i, nNodes, nGain, fCompl; int clk, clkStart = clock(); @@ -74,7 +74,7 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerb if ( fPlaceEnable ) { Abc_PlaceBegin( pNtk ); - vUpdates = Abc_AigUpdateStart( pNtk->pManFunc ); + vAddedCells = Abc_AigUpdateStart( pNtk->pManFunc, &vUpdatedNets ); } // start the rewriting manager @@ -132,7 +132,7 @@ Rwr_ManAddTimeUpdate( pManRwr, clock() - clk ); // use the array of changed nodes to update placement if ( fPlaceEnable ) - Abc_PlaceUpdate( vUpdates, nNodes ); + Abc_PlaceUpdate( vAddedCells, vUpdatedNets ); } Extra_ProgressBarStop( pProgress ); Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart ); diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index 2ce80a8f..88ef009b 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -55,7 +55,7 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup ) // print warning about choice nodes if ( Abc_NtkGetChoiceNum( pNtk ) ) printf( "Warning: The choice nodes in the original AIG are removed by strashing.\n" ); - // start the new network (constants and CIs are already mappined after this step + // start the new network (constants and CIs of the old network will point to the their counterparts in the new network) pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); // restrash the nodes (assuming a topological order of the old network) Abc_NtkForEachNode( pNtk, pObj, i ) diff --git a/src/base/abci/abcUnate.c b/src/base/abci/abcUnate.c index 8fd2a12f..20804d19 100644 --- a/src/base/abci/abcUnate.c +++ b/src/base/abci/abcUnate.c @@ -84,7 +84,7 @@ clkBdd = clock() - clk; // pbGlobal = (DdNode **)Vec_PtrArray( pNtk->vFuncsGlob ); // print the size of the BDDs - printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); // perform naive BDD-based computation if ( fUseNaive ) diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c index 7697fde1..ea0a4cd2 100644 --- a/src/base/abci/abcUnreach.c +++ b/src/base/abci/abcUnreach.c @@ -62,7 +62,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose ) if ( dd == NULL ) return 0; if ( fVerbose ) - printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + printf( "Shared BDD size = %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); // create the transition relation (dereferenced global BDDs) bRelation = Abc_NtkTransitionRelation( dd, pNtk, fVerbose ); Cudd_Ref( bRelation ); @@ -221,7 +221,7 @@ DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * b { DdNode * bRelation, * bReached, * bCubeCs; DdNode * bCurrent, * bNext, * bTemp; - int nIters; + int nIters, nMints; // perform reachability analisys bCurrent = bInitial; Cudd_Ref( bCurrent ); @@ -258,9 +258,9 @@ DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * b // report the stats if ( fVerbose ) { - fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters ); - fprintf( stdout, "The number of minterms in the reachable state set = %d.\n", - (int)Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) ) ); + nMints = (int)Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) ); + fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters ); + fprintf( stdout, "The number of minterms in the reachable state set = %d. (%6.2f %%)\n", nMints, 100.0*nMints/(1<<Abc_NtkLatchNum(pNtk)) ); } //PRB( dd, bReached ); Cudd_Deref( bReached ); diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 4aa05d07..016ada60 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -3,6 +3,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcAuto.c \ src/base/abci/abcBalance.c \ src/base/abci/abcBmc.c \ + src/base/abci/abcCas.c \ src/base/abci/abcClpBdd.c \ src/base/abci/abcClpSop.c \ src/base/abci/abcCut.c \ @@ -29,6 +30,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcPlace.c \ src/base/abci/abcPrint.c \ src/base/abci/abcProve.c \ + src/base/abci/abcQuant.c \ src/base/abci/abcReconv.c \ src/base/abci/abcRefactor.c \ src/base/abci/abcRenode.c \ |