diff options
Diffstat (limited to 'src/base/abci')
31 files changed, 830 insertions, 1573 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c1327f43..8cf0e0af 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -45,6 +45,7 @@ static int Abc_CommandPrintAuto ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandPrintKMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintGates ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintSharing ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintSkews ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandShowBdd ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandShowCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -73,6 +74,7 @@ static int Abc_CommandOrPos ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandFrames ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSop ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBdd ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandReorder ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandOrder ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMuxes ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -95,6 +97,7 @@ static int Abc_CommandIRewrite ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandIRewriteSeq ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIResyn ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandHaig ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandMini ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFraigTrust ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -131,6 +134,9 @@ static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandTraceStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandHoward ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSkewForward ( Abc_Frame_t * pAbc, int argc, char ** argv ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -164,6 +170,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Printing", "print_kmap", Abc_CommandPrintKMap, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_gates", Abc_CommandPrintGates, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_sharing", Abc_CommandPrintSharing, 0 ); + Cmd_CommandAdd( pAbc, "Printing", "print_skews", Abc_CommandPrintSkews, 0 ); Cmd_CommandAdd( pAbc, "Printing", "show_bdd", Abc_CommandShowBdd, 0 ); Cmd_CommandAdd( pAbc, "Printing", "show_cut", Abc_CommandShowCut, 0 ); @@ -192,6 +199,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "frames", Abc_CommandFrames, 1 ); Cmd_CommandAdd( pAbc, "Various", "sop", Abc_CommandSop, 0 ); Cmd_CommandAdd( pAbc, "Various", "bdd", Abc_CommandBdd, 0 ); + Cmd_CommandAdd( pAbc, "Various", "aig", Abc_CommandAig, 0 ); Cmd_CommandAdd( pAbc, "Various", "reorder", Abc_CommandReorder, 0 ); Cmd_CommandAdd( pAbc, "Various", "order", Abc_CommandOrder, 0 ); Cmd_CommandAdd( pAbc, "Various", "muxes", Abc_CommandMuxes, 1 ); @@ -214,6 +222,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "New AIG", "irws", Abc_CommandIRewriteSeq, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "iresyn", Abc_CommandIResyn, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "haig", Abc_CommandHaig, 1 ); + Cmd_CommandAdd( pAbc, "New AIG", "mini", Abc_CommandMini, 1 ); Cmd_CommandAdd( pAbc, "Fraiging", "fraig", Abc_CommandFraig, 1 ); Cmd_CommandAdd( pAbc, "Fraiging", "fraig_trust", Abc_CommandFraigTrust, 1 ); @@ -247,8 +256,11 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "sat", Abc_CommandSat, 0 ); Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 ); - Cmd_CommandAdd( pAbc, "Verification", "trace_start", Abc_CommandTraceStart, 0 ); - Cmd_CommandAdd( pAbc, "Verification", "trace_check", Abc_CommandTraceCheck, 0 ); +// Cmd_CommandAdd( pAbc, "Verification", "trace_start", Abc_CommandTraceStart, 0 ); +// Cmd_CommandAdd( pAbc, "Verification", "trace_check", Abc_CommandTraceCheck, 0 ); + + Cmd_CommandAdd( pAbc, "Sequential", "howard", Abc_CommandHoward, 0 ); + Cmd_CommandAdd( pAbc, "Sequential", "skew_fwd", Abc_CommandSkewForward, 0 ); // Rwt_Man4ExploreStart(); // Map_Var3Print(); @@ -1297,6 +1309,74 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandPrintSkews( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int fPrintAll; + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fPrintAll = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF ) + { + switch ( c ) + { + case 'a': + fPrintAll = 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( !Abc_NtkIsSeq(pNtk) && Abc_NtkLatchNum(pNtk) == 0 ) + { + fprintf( pErr, "The network has no latches.\n" ); + return 0; + } + + if ( pNtk->vSkews == NULL || pNtk->vSkews->nSize == 0 ) + { + fprintf( pErr, "The network has no clock skew schedule.\n" ); + return 0; + } + + Abc_NtkPrintSkews( pOut, pNtk, fPrintAll ); + return 0; + +usage: + fprintf( pErr, "usage: print_skews [-h] [-a]\n" ); + fprintf( pErr, "\t prints information about a clock skew schedule\n" ); + fprintf( pErr, "\t-a : dumps the skew of every latch [default = no]\n"); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; @@ -3309,29 +3389,26 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } - if ( pNtk == NULL ) { fprintf( pErr, "Empty network.\n" ); return 1; } - - // get the new network - if ( !Abc_NtkIsBddLogic(pNtk) ) + if ( !Abc_NtkIsLogic(pNtk) ) { - fprintf( pErr, "Converting to SOP is possible when node functions are BDDs.\n" ); + fprintf( pErr, "Converting to SOP is possible only for logic networks.\n" ); return 1; } - if ( !Abc_NtkBddToSop( pNtk, fDirect ) ) + if ( !Abc_NtkLogicToSop(pNtk, fDirect) ) { - fprintf( pErr, "Converting to SOP has failed.\n" ); + fprintf( pErr, "Converting to BDD has failed.\n" ); return 1; } return 0; usage: fprintf( pErr, "usage: sop [-dh]\n" ); - fprintf( pErr, "\t converts node functions from BDD to SOP\n" ); + fprintf( pErr, "\t converts node functions to SOP\n" ); fprintf( pErr, "\t-d : toggles using both phases or only positive [default = %s]\n", fDirect? "direct": "both" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -3370,19 +3447,22 @@ int Abc_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } - if ( pNtk == NULL ) { fprintf( pErr, "Empty network.\n" ); return 1; } - - if ( !Abc_NtkIsSopLogic(pNtk) ) + if ( !Abc_NtkIsLogic(pNtk) ) { - fprintf( pErr, "Converting to BDD is possible when node functions are SOPs.\n" ); + fprintf( pErr, "Converting to BDD is possible only for logic networks.\n" ); return 1; } - if ( !Abc_NtkSopToBdd( pNtk ) ) + if ( Abc_NtkIsBddLogic(pNtk) ) + { + fprintf( pOut, "The logic network is already in the BDD form.\n" ); + return 0; + } + if ( !Abc_NtkLogicToBdd(pNtk) ) { fprintf( pErr, "Converting to BDD has failed.\n" ); return 1; @@ -3391,7 +3471,69 @@ int Abc_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( pErr, "usage: bdd [-h]\n" ); - fprintf( pErr, "\t converts node functions from SOP to BDD\n" ); + fprintf( pErr, "\t converts node functions to BDD\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAig( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsLogic(pNtk) ) + { + fprintf( pErr, "Converting to AIG is possible only for logic networks.\n" ); + return 1; + } + if ( Abc_NtkIsAigLogic(pNtk) ) + { + fprintf( pOut, "The logic network is already in the AIG form.\n" ); + return 0; + } + if ( !Abc_NtkLogicToAig(pNtk) ) + { + fprintf( pErr, "Converting to AIG has failed.\n" ); + return 1; + } + return 0; + +usage: + fprintf( pErr, "usage: aig [-h]\n" ); + fprintf( pErr, "\t converts node functions to AIG\n" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -3759,7 +3901,7 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( argc == globalUtilOptind + 1 ) { - pNodeCo = Abc_NtkFindCo( pNtk, argv[globalUtilOptind] ); + pNodeCo = Abc_NtkFindTerm( pNtk, argv[globalUtilOptind] ); pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] ); if ( pNode == NULL ) { @@ -5271,6 +5413,73 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandMini( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c; + extern Abc_Ntk_t * Abc_NtkMiniBalance( Abc_Ntk_t * pNtk ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( Abc_NtkIsSeq(pNtk) ) + { + fprintf( pErr, "Only works for non-sequential networks.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "Only works for combinatinally strashed AIG networks.\n" ); + return 1; + } + + pNtkRes = Abc_NtkMiniBalance( pNtk ); + 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: mini [-h]\n" ); + fprintf( pErr, "\t perform balancing using new package\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* @@ -5913,7 +6122,6 @@ int Abc_CommandUnmap( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk; int c; - extern int Abc_NtkUnmap( Abc_Ntk_t * pNtk ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -5944,7 +6152,7 @@ int Abc_CommandUnmap( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - if ( !Abc_NtkUnmap( pNtk ) ) + if ( !Abc_NtkMapToSop( pNtk ) ) { fprintf( pErr, "Unmapping has failed.\n" ); return 1; @@ -5974,7 +6182,6 @@ int Abc_CommandAttach( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk; int c; - extern int Abc_NtkUnmap( Abc_Ntk_t * pNtk ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -7982,13 +8189,14 @@ int Abc_CommandTraceStart( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "This command is applicable to AIGs.\n" ); return 1; } - +/* Abc_HManStart(); if ( !Abc_HManPopulate( pNtk ) ) { fprintf( pErr, "Failed to start the tracing database.\n" ); return 1; } +*/ return 0; usage: @@ -8042,7 +8250,7 @@ int Abc_CommandTraceCheck( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "This command is applicable to AIGs.\n" ); return 1; } - +/* if ( !Abc_HManIsRunning(pNtk) ) { fprintf( pErr, "The tracing database is not available.\n" ); @@ -8052,6 +8260,7 @@ int Abc_CommandTraceCheck( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( !Abc_HManVerify( 1, pNtk->Id ) ) fprintf( pErr, "Verification failed.\n" ); Abc_HManStop(); +*/ return 0; usage: @@ -8060,6 +8269,168 @@ usage: fprintf( pErr, "\t-h : print the command usage\n"); return 1; } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandHoward( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int fVerbose; + double result; + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( !Abc_NtkIsSeq(pNtk) && Abc_NtkLatchNum(pNtk) == 0 ) + { + fprintf( pErr, "The network has no latches. Analysis is not performed.\n" ); + return 0; + } + + if ( Abc_NtkHasAig(pNtk) ) + { + // quit if there are choice nodes + if ( Abc_NtkGetChoiceNum(pNtk) ) + { + fprintf( pErr, "Currently cannot analyze networks with choice nodes.\n" ); + return 0; + } + + /* + if ( Abc_NtkIsStrash(pNtk) ) + pNtkRes = Abc_NtkAigToSeq(pNtk); + else + pNtkRes = Abc_NtkDup(pNtk); + + */ + + fprintf( pErr, "Currently cannot analyze unmapped networks.\n" ); + return 0; + } + + result = Seq_NtkHoward( pNtk, fVerbose ); + + if (result < 0) { + fprintf( pErr, "Analysis failed.\n" ); + return 0; + } + + printf("Maximum mean cycle time = %.2f\n", result); + + return 1; + +usage: + fprintf( pErr, "usage: howard [-h]\n" ); + fprintf( pErr, "\t computes the maximum mean cycle time using Howard's algorithm\n" ); + fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandSkewForward( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int fMinimize; + float target; + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + target = pNtk->maxMeanCycle; + fMinimize = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "mh" ) ) != EOF ) + { + switch ( c ) + { + case 'm': + fMinimize ^= 1; + break; + default: + goto usage; + } + } + + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( !Abc_NtkIsSeq(pNtk) && Abc_NtkLatchNum(pNtk) == 0 ) + { + fprintf( pErr, "The network has no latches.\n" ); + return 0; + } + + if ( pNtk->vSkews == NULL || pNtk->vSkews->nSize == 0 ) + { + fprintf( pErr, "The network has no clock skew schedule.\n" ); + return 0; + } + + Seq_NtkSkewForward( pNtk, target, fMinimize ); + + return 1; + +usage: + fprintf( pErr, "usage: skew_fwd [-h] [-m] [-t float]\n" ); + fprintf( pErr, "\t converts a skew schedule into a set of forward skews 0<skew<T\n" ); + fprintf( pErr, "\t-m : minimizes sum of skews [default = %s]\n", fMinimize? "yes": "no" ); + fprintf( pErr, "\t-t : clock period, T [default = maxMeanCycle] (unimplemented)\n"); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c index 389a7977..819974bf 100644 --- a/src/base/abci/abcBalance.c +++ b/src/base/abci/abcBalance.c @@ -233,7 +233,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_ vSuper = Abc_NodeBalanceCone( pNodeOld, vStorage, Level, fDuplicate, fSelective ); if ( vSuper->nSize == 0 ) { // it means that the supergate contains two nodes in the opposite polarity - pNodeOld->pCopy = Abc_ObjNot(Abc_NtkConst1(pNtkNew)); + pNodeOld->pCopy = Abc_ObjNot(Abc_AigConst1(pNtkNew)); return pNodeOld->pCopy; } // for each old node, derive the new well-balanced node @@ -263,9 +263,8 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_ assert( pNodeOld->pCopy == NULL ); // mark the old node with the new node pNodeOld->pCopy = vSuper->pArray[0]; - Abc_HManAddProto( pNodeOld->pCopy, pNodeOld ); vSuper->nSize = 0; -// if ( Abc_ObjRegular(pNodeOld->pCopy) == Abc_NtkConst1(pNtkNew) ) +// if ( Abc_ObjRegular(pNodeOld->pCopy) == Abc_AigConst1(pNtkNew) ) // printf( "Constant node\n" ); // assert( pNodeOld->Level >= Abc_ObjRegular(pNodeOld->pCopy)->Level ); return pNodeOld->pCopy; diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c index c7c164b9..7024a970 100644 --- a/src/base/abci/abcCut.c +++ b/src/base/abci/abcCut.c @@ -95,8 +95,8 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) continue; } // skip constant node, it has no cuts - if ( Abc_NodeIsConst(pObj) ) - continue; +// if ( Abc_NodeIsConst(pObj) ) +// continue; Extra_ProgressBarUpdate( pProgress, i, NULL ); // compute the cuts to the internal node Abc_NodeGetCuts( p, pObj, pParams->fDag, pParams->fTree ); @@ -107,7 +107,7 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) Cut_NodeTryDroppingCuts( p, Abc_ObjFaninId1(pObj) ); } // add cuts due to choices - if ( Abc_NodeIsAigChoice(pObj) ) + if ( Abc_AigNodeIsChoice(pObj) ) { Vec_IntClear( vChoices ); for ( pNode = pObj; pNode; pNode = pNode->pData ) @@ -171,8 +171,8 @@ void Abc_NtkCutsOracle( Abc_Ntk_t * pNtk, Cut_Oracle_t * p ) continue; } // skip constant node, it has no cuts - if ( Abc_NodeIsConst(pObj) ) - continue; +// if ( Abc_NodeIsConst(pObj) ) +// continue; // compute the cuts to the internal node Cut_OracleComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj), Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); @@ -218,7 +218,7 @@ Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) p = Cut_ManStart( pParams ); // set cuts for the constant node and the PIs - pObj = Abc_NtkConst1(pNtk); + pObj = Abc_AigConst1(pNtk); if ( Abc_ObjFanoutNum(pObj) > 0 ) Cut_NodeSetTriv( p, pObj->Id ); Abc_NtkForEachPi( pNtk, pObj, i ) @@ -247,7 +247,7 @@ Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) { Abc_NodeGetCutsSeq( p, pObj, nIters==0 ); // add cuts due to choices - if ( Abc_NodeIsAigChoice(pObj) ) + if ( Abc_AigNodeIsChoice(pObj) ) { Vec_IntClear( vChoices ); for ( pNode = pObj; pNode; pNode = pNode->pData ) diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c index 79d2b729..cd8f9047 100644 --- a/src/base/abci/abcDsd.c +++ b/src/base/abci/abcDsd.c @@ -172,7 +172,7 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * int i, nNodesDsd; // save the CI nodes in the DSD nodes - Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_NtkConst1(pNtk)->pCopy ); + Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_AigConst1(pNtkNew) ); Abc_NtkForEachCi( pNtk, pNode, i ) { pNodeDsd = Dsd_ManagerReadInput( pManDsd, i ); @@ -191,7 +191,7 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * pDriver = Abc_ObjFanin0( pNode ); if ( !Abc_ObjIsNode(pDriver) ) continue; - if ( !Abc_NodeIsAigAnd(pDriver) ) + if ( !Abc_AigNodeIsAnd(pDriver) ) continue; pNodeDsd = Dsd_ManagerReadRoot( pManDsd, i ); pNodeNew = (Abc_Obj_t *)Dsd_NodeReadMark( Dsd_Regular(pNodeDsd) ); @@ -419,14 +419,14 @@ void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager pNodeC = Abc_ObjFanin( pNode, iVar ); // get the negative cofactor - pNode1 = Abc_NodeClone( pNode ); + pNode1 = Abc_NtkCloneObj( pNode ); pNode1->pData = Cudd_Cofactor( dd, pNode->pData, Cudd_Not(dd->vars[iVar]) ); Cudd_Ref( pNode1->pData ); Abc_NodeMinimumBase( pNode1 ); if ( Abc_NodeIsForDsd(pNode1) ) Vec_PtrPush( vNodes, pNode1 ); // get the positive cofactor - pNode2 = Abc_NodeClone( pNode ); + pNode2 = Abc_NtkCloneObj( pNode ); pNode2->pData = Cudd_Cofactor( dd, pNode->pData, dd->vars[iVar] ); Cudd_Ref( pNode2->pData ); Abc_NodeMinimumBase( pNode2 ); if ( Abc_NodeIsForDsd(pNode2) ) diff --git a/src/base/abci/abcEspresso.c b/src/base/abci/abcEspresso.c index ad43534d..8f9c7277 100644 --- a/src/base/abci/abcEspresso.c +++ b/src/base/abci/abcEspresso.c @@ -52,12 +52,12 @@ void Abc_NtkEspresso( Abc_Ntk_t * pNtk, int fVerbose ) assert( Abc_NtkIsLogic(pNtk) ); // convert the network to have SOPs if ( Abc_NtkHasMapping(pNtk) ) - Abc_NtkUnmap(pNtk); + Abc_NtkMapToSop(pNtk); else if ( Abc_NtkHasBdd(pNtk) ) { if ( !Abc_NtkBddToSop(pNtk, 0) ) { - printf( "Converting to SOPs has failed.\n" ); + printf( "Abc_NtkEspresso(): Converting to SOPs has failed.\n" ); return; } } diff --git a/src/base/abci/abcFpga.c b/src/base/abci/abcFpga.c index a59ef2af..e5286487 100644 --- a/src/base/abci/abcFpga.c +++ b/src/base/abci/abcFpga.c @@ -143,6 +143,7 @@ Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, float * pSwitching, // create PIs and remember them in the old nodes Abc_NtkCleanCopy( pNtk ); + Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Fpga_ManReadConst1(pMan); Abc_NtkForEachCi( pNtk, pNode, i ) { pNodeFpga = Fpga_ManReadInputs(pMan)[i]; @@ -157,12 +158,6 @@ Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, float * pSwitching, Vec_PtrForEachEntry( vNodes, pNode, i ) { Extra_ProgressBarUpdate( pProgress, i, NULL ); - // consider the case of a constant - if ( Abc_NodeIsConst(pNode) ) - { - Abc_NtkConst1(pNtk)->pCopy = (Abc_Obj_t *)Fpga_ManReadConst1(pMan); - continue; - } // add the node to the mapper pNodeFpga = Fpga_NodeAnd( pMan, Fpga_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ), @@ -173,7 +168,7 @@ Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, float * pSwitching, if ( pSwitching ) Fpga_NodeSetSwitching( pNodeFpga, pSwitching[pNode->Id] ); // set up the choice node - if ( Abc_NodeIsAigChoice( pNode ) ) + if ( Abc_AigNodeIsChoice( pNode ) ) for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData ) { Fpga_NodeSetNextE( (Fpga_Node_t *)pPrev->pCopy, (Fpga_Node_t *)pFanin->pCopy ); @@ -214,7 +209,7 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk ) Abc_NtkForEachCi( pNtk, pNode, i ) Fpga_NodeSetData0( Fpga_ManReadInputs(pMan)[i], (char *)pNode->pCopy ); // set the constant node - Fpga_NodeSetData0( Fpga_ManReadConst1(pMan), (char *)Abc_NtkConst1(pNtkNew) ); + Fpga_NodeSetData0( Fpga_ManReadConst1(pMan), (char *)Abc_NodeCreateConst1(pNtkNew) ); // process the nodes in topological order pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); Abc_NtkForEachCo( pNtk, pNode, i ) diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c index 46f2cdf0..778c8284 100644 --- a/src/base/abci/abcFraig.c +++ b/src/base/abci/abcFraig.c @@ -113,7 +113,7 @@ void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExd // map the constant node Abc_NtkCleanCopy( pNtk ); - Abc_NtkConst1(pNtk)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan); + Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan); // create PIs and remember them in the old nodes Abc_NtkForEachCi( pNtk, pNode, i ) pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i); @@ -168,7 +168,7 @@ Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtkMain, Abc // strash the EXDC network pNtkStrash = Abc_NtkStrash( pNtkExdc, 0, 0 ); Abc_NtkCleanCopy( pNtkStrash ); - Abc_NtkConst1(pNtkStrash)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan); + Abc_AigConst1(pNtkStrash)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan); // set the mapping of the PI nodes ppNames = Abc_NtkCollectCioNames( pNtkMain, 0 ); Abc_NtkForEachCi( pNtkStrash, pObj, i ) @@ -285,7 +285,7 @@ Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ) Abc_NtkForEachCi( pNtk, pNode, i ) Fraig_NodeSetData1( Fraig_ManReadIthVar(pMan, i), (Fraig_Node_t *)pNode->pCopy ); // set the constant node - Fraig_NodeSetData1( Fraig_ManReadConst1(pMan), (Fraig_Node_t *)Abc_NtkConst1(pNtkNew) ); + Fraig_NodeSetData1( Fraig_ManReadConst1(pMan), (Fraig_Node_t *)Abc_AigConst1(pNtkNew) ); // process the nodes in topological order pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); Abc_NtkForEachCo( pNtk, pNode, i ) @@ -384,7 +384,7 @@ Abc_Ntk_t * Abc_NtkFromFraig2( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ) // map the nodes into their lowest level representives tTable = stmm_init_table(stmm_ptrcmp,stmm_ptrhash); - pNode = Abc_NtkConst1(pNtk); + pNode = Abc_AigConst1(pNtk); if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) ) *ppSlot = pNode; Abc_NtkForEachCi( pNtk, pNode, i ) @@ -607,7 +607,7 @@ Abc_Obj_t * Abc_NodeFraigTrust( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode ) assert( nFanins == Abc_SopGetVarNum(pNode->pData) ); // check if it is a constant if ( nFanins == 0 ) - return Abc_ObjNotCond( Abc_NtkConst1(pNtkNew), Abc_SopIsConst0(pNode->pData) ); + return Abc_ObjNotCond( Abc_AigConst1(pNtkNew), Abc_SopIsConst0(pNode->pData) ); if ( nFanins == 1 ) return Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_SopIsInv(pNode->pData) ); if ( nFanins == 2 && Abc_SopIsAndType(pNode->pData) ) diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c index a8e656ce..b6d57a5c 100644 --- a/src/base/abci/abcFxu.c +++ b/src/base/abci/abcFxu.c @@ -53,22 +53,19 @@ static void Abc_NtkFxuReconstruct( Abc_Ntk_t * pNtk, Fxu_Data_t * p ); bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p ) { assert( Abc_NtkIsLogic(pNtk) ); - // convert nodes to SOPs - if ( Abc_NtkIsMappedLogic(pNtk) ) - Abc_NtkUnmap(pNtk); - else if ( Abc_NtkIsBddLogic(pNtk) ) - { - if ( !Abc_NtkBddToSop(pNtk, 0) ) - { - printf( "Converting to SOPs has failed.\n" ); - return 0; - } - } - else + // if the network is already in the SOP form, it may come from BLIF file + // and it may not be SCC-free, in which case FXU will not work correctly + if ( Abc_NtkIsSopLogic(pNtk) ) { // to make sure the SOPs are SCC-free // Abc_NtkSopToBdd(pNtk); // Abc_NtkBddToSop(pNtk); } + // get the network in the SOP form + if ( !Abc_NtkLogicToSop(pNtk, 0) ) + { + printf( "Abc_NtkFastExtract(): Converting to SOPs has failed.\n" ); + return 0; + } // check if the network meets the requirements if ( !Abc_NtkFxuCheck(pNtk) ) { diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c index 42d5173a..6538b360 100644 --- a/src/base/abci/abcIvy.c +++ b/src/base/abci/abcIvy.c @@ -77,7 +77,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc ) { if ( !Abc_NtkBddToSop(pNtk, 0) ) { - printf( "Converting to SOPs has failed.\n" ); + printf( "Abc_NtkIvyBefore(): Converting to SOPs has failed.\n" ); return NULL; } } @@ -329,7 +329,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk ) if ( !Abc_NtkBddToSop(pNtk, 0) ) { FREE( pInit ); - printf( "Converting to SOPs has failed.\n" ); + printf( "Abc_NtkIvy(): Converting to SOPs has failed.\n" ); return NULL; } } @@ -437,7 +437,7 @@ Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan ) // perform strashing pNtk = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); // transfer the pointers to the basic nodes - Ivy_ManConst1(pMan)->TravId = Abc_EdgeFromNode( Abc_NtkConst1(pNtk) ); + Ivy_ManConst1(pMan)->TravId = Abc_EdgeFromNode( Abc_AigConst1(pNtk) ); Abc_NtkForEachCi( pNtkOld, pObj, i ) Ivy_ManPi(pMan, i)->TravId = Abc_EdgeFromNode( pObj->pCopy ); // rebuild the AIG @@ -494,7 +494,7 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig // perform strashing pNtk = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); // transfer the pointers to the basic nodes - Ivy_ManConst1(pMan)->TravId = Abc_EdgeFromNode( Abc_NtkConst1(pNtk) ); + Ivy_ManConst1(pMan)->TravId = Abc_EdgeFromNode( Abc_AigConst1(pNtk) ); Abc_NtkForEachPi( pNtkOld, pObj, i ) Ivy_ManPi(pMan, i)->TravId = Abc_EdgeFromNode( pObj->pCopy ); // create latches of the new network @@ -583,10 +583,11 @@ Ivy_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld ) Ivy_Obj_t * pFanin; int i; // create the manager - assert( Abc_NtkHasSop(pNtkOld) || Abc_NtkHasAig(pNtkOld) ); + assert( Abc_NtkHasSop(pNtkOld) || Abc_NtkIsStrash(pNtkOld) ); pMan = Ivy_ManStart(); // create the PIs - Abc_NtkConst1(pNtkOld)->pCopy = (Abc_Obj_t *)Ivy_ManConst1(pMan); + if ( Abc_NtkIsStrash(pNtkOld) ) + Abc_AigConst1(pNtkOld)->pCopy = (Abc_Obj_t *)Ivy_ManConst1(pMan); Abc_NtkForEachCi( pNtkOld, pObj, i ) pObj->pCopy = (Abc_Obj_t *)Ivy_ObjCreatePi(pMan); // perform the conversion of the internal nodes @@ -646,14 +647,13 @@ Ivy_Obj_t * Abc_NodeStrashAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode ) int fUseFactor = 1; char * pSop; Ivy_Obj_t * pFanin0, * pFanin1; - extern int Abc_SopIsExorType( char * pSop ); assert( Abc_ObjIsNode(pNode) ); // consider the case when the graph is an AIG if ( Abc_NtkIsStrash(pNode->pNtk) ) { - if ( Abc_NodeIsConst(pNode) ) + if ( Abc_AigNodeIsConst(pNode) ) return Ivy_ManConst1(pMan); pFanin0 = (Ivy_Obj_t *)Abc_ObjFanin0(pNode)->pCopy; pFanin0 = Ivy_NotCond( pFanin0, Abc_ObjFaninC0(pNode) ); diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c index c579eb84..276e41d0 100644 --- a/src/base/abci/abcMap.c +++ b/src/base/abci/abcMap.c @@ -159,6 +159,7 @@ Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, f // create PIs and remember them in the old nodes Abc_NtkCleanCopy( pNtk ); + Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Map_ManReadConst1(pMan); Abc_NtkForEachCi( pNtk, pNode, i ) { pNodeMap = Map_ManReadInputs(pMan)[i]; @@ -173,12 +174,6 @@ Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, f Vec_PtrForEachEntry( vNodes, pNode, i ) { Extra_ProgressBarUpdate( pProgress, i, NULL ); - // consider the case of a constant - if ( Abc_NodeIsConst(pNode) ) - { - Abc_NtkConst1(pNtk)->pCopy = (Abc_Obj_t *)Map_ManReadConst1(pMan); - continue; - } // add the node to the mapper pNodeMap = Map_NodeAnd( pMan, Map_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ), @@ -189,7 +184,7 @@ Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, f if ( pSwitching ) Map_NodeSetSwitching( pNodeMap, pSwitching[pNode->Id] ); // set up the choice node - if ( Abc_NodeIsAigChoice( pNode ) ) + if ( Abc_AigNodeIsChoice( pNode ) ) for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData ) { Map_NodeSetNextE( (Map_Node_t *)pPrev->pCopy, (Map_Node_t *)pFanin->pCopy ); @@ -223,16 +218,12 @@ Abc_Ntk_t * Abc_NtkFromMap( Map_Man_t * pMan, Abc_Ntk_t * pNtk ) Map_Node_t * pNodeMap; Abc_Obj_t * pNode, * pNodeNew; int i, nDupGates; - // create the new network pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_MAP ); // make the mapper point to the new network Map_ManCleanData( pMan ); Abc_NtkForEachCi( pNtk, pNode, i ) Map_NodeSetData( Map_ManReadInputs(pMan)[i], 1, (char *)pNode->pCopy ); - // set the constant node - Map_NodeSetData( Map_ManReadConst1(pMan), 1, (char *)Abc_NtkConst1(pNtkNew) ); - // assign the mapping of the required phase to the POs pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); Abc_NtkForEachCo( pNtk, pNode, i ) @@ -266,6 +257,10 @@ Abc_Obj_t * Abc_NodeFromMap_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, int { Abc_Obj_t * pNodeNew, * pNodeInv; + // check the case of constant node + if ( Map_NodeIsConst(pNodeMap) ) + return fPhase? Abc_NodeCreateConst1(pNtkNew) : Abc_NodeCreateConst0(pNtkNew); + // check if the phase is already implemented pNodeNew = (Abc_Obj_t *)Map_NodeReadData( pNodeMap, fPhase ); if ( pNodeNew ) @@ -393,38 +388,6 @@ Abc_Obj_t * Abc_NodeFromMapSuper_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap } -/**Function************************************************************* - - Synopsis [Unmaps the network.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkUnmap( Abc_Ntk_t * pNtk ) -{ - Abc_Obj_t * pNode; - char * pSop; - int i; - - assert( Abc_NtkIsMappedLogic(pNtk) ); - // update the functionality manager - assert( pNtk->pManFunc == Abc_FrameReadLibGen() ); - pNtk->pManFunc = Extra_MmFlexStart(); - pNtk->ntkFunc = ABC_FUNC_SOP; - // update the nodes - Abc_NtkForEachNode( pNtk, pNode, i ) - { - pSop = Mio_GateReadSop(pNode->pData); - assert( Abc_SopGetVarNum(pSop) == Abc_ObjFaninNum(pNode) ); - pNode->pData = Abc_SopRegister( pNtk->pManFunc, pSop ); - } - return 1; -} - @@ -524,7 +487,7 @@ Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk ) pNtkNew = Abc_NtkRenode( pNtkNew2, 0, 20, 0, 0, 1, 0 ); if ( !Abc_NtkBddToSop( pNtkNew, 0 ) ) { - printf( "Converting to SOPs has failed.\n" ); + printf( "Abc_NtkFromMapSuperChoice(): Converting to SOPs has failed.\n" ); return NULL; } @@ -545,8 +508,8 @@ Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk ) } Abc_NtkForEachNode( pNtk, pNode, i ) { - if ( Abc_NodeIsConst(pNode) ) - continue; +// if ( Abc_NodeIsConst(pNode) ) +// continue; Map_NodeSetData( (Map_Node_t *)pNode->pNext, 0, (char *)Abc_NodeCreateInv(pNtkNew,pNode->pCopy) ); Map_NodeSetData( (Map_Node_t *)pNode->pNext, 1, (char *)pNode->pCopy ); } @@ -556,8 +519,8 @@ Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk ) Abc_NtkForEachNode( pNtk, pNode, i ) { Extra_ProgressBarUpdate( pProgress, i, NULL ); - if ( Abc_NodeIsConst(pNode) ) - continue; +// if ( Abc_NodeIsConst(pNode) ) +// continue; Abc_NodeSuperChoice( pNtkNew, pNode ); } Extra_ProgressBarStop( pProgress ); diff --git a/src/base/abci/abcMini.c b/src/base/abci/abcMini.c new file mode 100644 index 00000000..037f058a --- /dev/null +++ b/src/base/abci/abcMini.c @@ -0,0 +1,152 @@ +/**CFile**************************************************************** + + FileName [abcMini.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Interface to the minimalistic AIG package.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcMini.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static Aig_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtk ); +static Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkMiniBalance( Abc_Ntk_t * pNtk ) +{ + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan, * pTemp; + assert( Abc_NtkIsStrash(pNtk) ); + // convert to the AIG manager + pMan = Abc_NtkToAig( pNtk ); + if ( pMan == NULL ) + return NULL; + if ( !Aig_ManCheck( pMan ) ) + { + printf( "AIG check has failed.\n" ); + Aig_ManStop( pMan ); + return NULL; + } + // perform balance + Aig_ManPrintStats( pMan ); + pMan = Aig_ManBalance( pTemp = pMan, 1 ); + Aig_ManStop( pTemp ); + Aig_ManPrintStats( pMan ); + // convert from the AIG manager + pNtkAig = Abc_NtkFromAig( pNtk, pMan ); + if ( pNtkAig == NULL ) + return NULL; + Aig_ManStop( pMan ); + // make sure everything is okay + if ( !Abc_NtkCheck( pNtkAig ) ) + { + printf( "Abc_NtkStrash: The network check has failed.\n" ); + Abc_NtkDelete( pNtkAig ); + return NULL; + } + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Converts the network from the AIG manager into ABC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtk ) +{ + Aig_Man_t * pMan; + Abc_Obj_t * pObj; + int i; + // create the manager + pMan = Aig_ManStart(); + // transfer the pointers to the basic nodes + Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan); + Abc_NtkForEachCi( pNtk, pObj, i ) + pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreatePi(pMan); + // perform the conversion of the internal nodes (assumes DFS ordering) + Abc_NtkForEachNode( pNtk, pObj, i ) + pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) ); + // create the POs + Abc_NtkForEachCo( pNtk, pObj, i ) + Aig_ObjCreatePo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) ); + Aig_ManCleanup( pMan ); + return pMan; +} + +/**Function************************************************************* + + Synopsis [Converts the network from the AIG manager into ABC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtk, Aig_Man_t * pMan ) +{ + Vec_Ptr_t * vNodes; + Abc_Ntk_t * pNtkNew; + Aig_Obj_t * pObj; + int i; + // perform strashing + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); + // transfer the pointers to the basic nodes + Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew); + Aig_ManForEachPi( pMan, pObj, i ) + pObj->pData = Abc_NtkCi(pNtkNew, i); + // rebuild the AIG + vNodes = Aig_ManDfs( pMan ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) ); + Vec_PtrFree( vNodes ); + // connect the PO nodes + Aig_ManForEachPo( pMan, pObj, i ) + Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) ); + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkFromAig(): Network check has failed.\n" ); + return pNtkNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index ea1beb8c..dfd49f6e 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -125,8 +125,8 @@ void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtk // clean the copy field in all objects // Abc_NtkCleanCopy( pNtk1 ); // Abc_NtkCleanCopy( pNtk2 ); - Abc_NtkConst1(pNtk1)->pCopy = Abc_NtkConst1(pNtkMiter); - Abc_NtkConst1(pNtk2)->pCopy = Abc_NtkConst1(pNtkMiter); + Abc_AigConst1(pNtk1)->pCopy = Abc_AigConst1(pNtkMiter); + Abc_AigConst1(pNtk2)->pCopy = Abc_AigConst1(pNtkMiter); if ( fComb ) { @@ -216,11 +216,11 @@ void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * p Abc_Obj_t * pNode; int i; // map the constant nodes - Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkMiter); + Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkMiter); // perform strashing vNodes = Abc_NtkDfsNodes( pNtk, &pRoot, 1 ); Vec_PtrForEachEntry( vNodes, pNode, i ) - if ( Abc_NodeIsAigAnd(pNode) ) + if ( Abc_AigNodeIsAnd(pNode) ) pNode->pCopy = Abc_AigAnd( pNtkMiter->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) ); Vec_PtrFree( vNodes ); } @@ -372,12 +372,12 @@ Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues ) continue; if ( Value == 0 ) { - Abc_NtkCi(pNtk, i)->pCopy = Abc_ObjNot( Abc_NtkConst1(pNtkMiter) ); + Abc_NtkCi(pNtk, i)->pCopy = Abc_ObjNot( Abc_AigConst1(pNtkMiter) ); continue; } if ( Value == 1 ) { - Abc_NtkCi(pNtk, i)->pCopy = Abc_NtkConst1(pNtkMiter); + Abc_NtkCi(pNtk, i)->pCopy = Abc_AigConst1(pNtkMiter); continue; } assert( 0 ); @@ -433,9 +433,9 @@ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In // perform strashing Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1 ); // set the first cofactor - Abc_NtkCi(pNtk, In1)->pCopy = Abc_ObjNot( Abc_NtkConst1(pNtkMiter) ); + Abc_NtkCi(pNtk, In1)->pCopy = Abc_ObjNot( Abc_AigConst1(pNtkMiter) ); if ( In2 >= 0 ) - Abc_NtkCi(pNtk, In2)->pCopy = Abc_NtkConst1( pNtkMiter ); + Abc_NtkCi(pNtk, In2)->pCopy = Abc_AigConst1(pNtkMiter); // add the first cofactor Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot ); @@ -443,9 +443,9 @@ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In pOutput1 = Abc_ObjFanin0(pRoot)->pCopy; // set the second cofactor - Abc_NtkCi(pNtk, In1)->pCopy = Abc_NtkConst1( pNtkMiter ); + Abc_NtkCi(pNtk, In1)->pCopy = Abc_AigConst1(pNtkMiter); if ( In2 >= 0 ) - Abc_NtkCi(pNtk, In2)->pCopy = Abc_ObjNot( Abc_NtkConst1(pNtkMiter) ); + Abc_NtkCi(pNtk, In2)->pCopy = Abc_ObjNot( Abc_AigConst1(pNtkMiter) ); // add the second cofactor Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot ); @@ -497,7 +497,7 @@ Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist ) // perform strashing Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1 ); // set the first cofactor - Abc_NtkCi(pNtk, In)->pCopy = Abc_ObjNot( Abc_NtkConst1(pNtkMiter) ); + Abc_NtkCi(pNtk, In)->pCopy = Abc_ObjNot( Abc_AigConst1(pNtkMiter) ); // add the first cofactor Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot ); // save the output @@ -505,7 +505,7 @@ Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist ) pOutput1 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot)->pCopy, Abc_ObjFaninC0(pRoot) ); // set the second cofactor - Abc_NtkCi(pNtk, In)->pCopy = Abc_NtkConst1( pNtkMiter ); + Abc_NtkCi(pNtk, In)->pCopy = Abc_AigConst1(pNtkMiter); // add the second cofactor Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot ); // save the output @@ -581,9 +581,9 @@ int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter ) Abc_NtkForEachPo( pMiter, pNodePo, i ) { pChild = Abc_ObjChild0( pNodePo ); - if ( Abc_ObjIsNode(Abc_ObjRegular(pChild)) && Abc_NodeIsConst(pChild) ) + if ( Abc_ObjIsNode(Abc_ObjRegular(pChild)) && Abc_AigNodeIsConst(pChild) ) { - assert( Abc_ObjRegular(pChild) == Abc_NtkConst1(pMiter) ); + assert( Abc_ObjRegular(pChild) == Abc_AigConst1(pMiter) ); if ( !Abc_ObjIsComplement(pChild) ) { // if the miter is constant 1, return immediately @@ -617,7 +617,7 @@ void Abc_NtkMiterReport( Abc_Ntk_t * pMiter ) if ( Abc_NtkPoNum(pMiter) == 1 ) { pChild = Abc_ObjChild0( Abc_NtkPo(pMiter,0) ); - if ( Abc_ObjIsNode(Abc_ObjRegular(pChild)) && Abc_NodeIsConst(pChild) ) + if ( Abc_ObjIsNode(Abc_ObjRegular(pChild)) && Abc_AigNodeIsConst(pChild) ) { if ( Abc_ObjIsComplement(pChild) ) printf( "Unsatisfiable.\n" ); @@ -633,7 +633,7 @@ void Abc_NtkMiterReport( Abc_Ntk_t * pMiter ) { pChild = Abc_ObjChild0( Abc_NtkPo(pMiter,i) ); printf( "Output #%2d : ", i ); - if ( Abc_ObjIsNode(Abc_ObjRegular(pChild)) && Abc_NodeIsConst(pChild) ) + if ( Abc_ObjIsNode(Abc_ObjRegular(pChild)) && Abc_AigNodeIsConst(pChild) ) { if ( Abc_ObjIsComplement(pChild) ) printf( "Unsatisfiable.\n" ); @@ -690,7 +690,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial ) Counter++; } else - pLatch->pCopy = Abc_ObjNotCond( Abc_NtkConst1(pNtkFrames), Abc_LatchIsInit0(pLatch) ); + pLatch->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames), Abc_LatchIsInit0(pLatch) ); } if ( Counter ) printf( "Warning: %d uninitialized latches are replaced by free PI variables.\n", Counter ); @@ -756,7 +756,7 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame ) // create the prefix to be added to the node names sprintf( Buffer, "_%02d", iFrame ); // map the constant nodes - Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkFrames); + Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkFrames); // add the new PI nodes Abc_NtkForEachPi( pNtk, pNode, i ) Abc_NtkLogicStoreNamePlus( Abc_NtkDupObj(pNtkFrames, pNode), Abc_ObjName(pNode), Buffer ); @@ -829,7 +829,7 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram Counter++; } else { - pLatch->pCopy = Abc_ObjNotCond( Abc_NtkConst1(pNtkFrames), Abc_LatchIsInit0(pLatch) ); + pLatch->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames), Abc_LatchIsInit0(pLatch) ); } if (addFrameMapping) addFrameMapping(pLatch->pCopy, pLatch, 0, arg); @@ -899,8 +899,8 @@ void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec Abc_Obj_t * pConst1, * pConst1New; int i; // get the constant nodes - pConst1 = Abc_NtkConst1( pNtk ); - pConst1New = Abc_NtkConst1( pNtkFrames ); + pConst1 = Abc_AigConst1(pNtk); + pConst1New = Abc_AigConst1(pNtkFrames); // create the prefix to be added to the node names sprintf( Buffer, "_%02d", iFrame ); // add the new PI nodes @@ -1037,7 +1037,7 @@ int Abc_NtkOrPos( Abc_Ntk_t * pNtk ) assert( Abc_NtkIsStrash(pNtk) ); assert( Abc_NtkLatchNum(pNtk) == 0 ); // OR the POs - pMiter = Abc_ObjNot( Abc_NtkConst1(pNtk) ); + pMiter = Abc_ObjNot( Abc_AigConst1(pNtk) ); Abc_NtkForEachPo( pNtk, pNode, i ) pMiter = Abc_AigOr( pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) ); // remove the POs and their names diff --git a/src/base/abci/abcNewAig.c b/src/base/abci/abcNewAig.c deleted file mode 100644 index 62ae51ed..00000000 --- a/src/base/abci/abcNewAig.c +++ /dev/null @@ -1,391 +0,0 @@ -/**CFile**************************************************************** - - FileName [aigNewAig.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Network and node package.] - - Synopsis [Strashing of the current network.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: aigNewAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" -#include "extra.h" -#include "dec.h" -#include "aig.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ); -static Aig_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld ); - -static void Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Aig_Man_t * pMan ); -static Aig_Node_t * Abc_NodeStrashAig( Aig_Man_t * pMan, Abc_Obj_t * pNode ); -static Aig_Node_t * Abc_NodeStrashAigSopAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop ); -static Aig_Node_t * Abc_NodeStrashAigExorAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop ); -static Aig_Node_t * Abc_NodeStrashAigFactorAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop ); -extern char * Mio_GateReadSop( void * pGate ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Gives the current ABC network to AIG manager for processing.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ) -{ - Aig_Man_t * pMan; - Abc_Ntk_t * pNtkAig; -// Aig_ProofType_t RetValue; - int fCleanup = 1; - int nNodes; - extern void Aig_MffcTest( Aig_Man_t * pMan ); - - - assert( !Abc_NtkIsNetlist(pNtk) ); - assert( !Abc_NtkIsSeq(pNtk) ); - if ( Abc_NtkIsBddLogic(pNtk) ) - { - if ( !Abc_NtkBddToSop(pNtk, 0) ) - { - printf( "Converting to SOPs has failed.\n" ); - return; - } - } - // print warning about choice nodes - if ( Abc_NtkGetChoiceNum( pNtk ) ) - printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" ); - - // convert to the AIG manager - pMan = Abc_NtkToAig( pNtk ); - - Aig_MffcTest( pMan ); - -/* - // execute a command in the AIG manager - RetValue = Aig_FraigProve( pMan ); - if ( RetValue == AIG_PROOF_SAT ) - printf( "Satisfiable.\n" ); - else if ( RetValue == AIG_PROOF_UNSAT ) - printf( "Unsatisfiable.\n" ); - else if ( RetValue == AIG_PROOF_TIMEOUT ) - printf( "Undecided.\n" ); - else - assert( 0 ); -*/ - - // convert from the AIG manager - pNtkAig = Abc_NtkFromAig( pNtk, pMan ); - Aig_ManStop( pMan ); - - // report the cleanup results - if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) ) - printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes ); - // duplicate EXDC - if ( pNtk->pExdc ) - pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc ); - // make sure everything is okay - if ( !Abc_NtkCheck( pNtkAig ) ) - { - printf( "Abc_NtkStrash: The network check has failed.\n" ); - Abc_NtkDelete( pNtkAig ); - return NULL; - } - return pNtkAig; -} - -/**Function************************************************************* - - Synopsis [Converts the network from the AIG manager into ABC.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) -{ - Abc_Ntk_t * pNtk; - Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1; - Aig_Node_t * pAnd; - int i; - // perform strashing - pNtk = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); - // transfer the pointers to the basic nodes - Aig_ManConst1(pMan)->Data = Abc_NtkConst1(pNtk)->Id; - Abc_NtkForEachCi( pNtkOld, pObj, i ) - Aig_ManPi(pMan, i)->Data = pObj->pCopy->Id; - // rebuild the AIG - Aig_ManForEachAnd( pMan, pAnd, i ) - { - // add the first fanins - pFaninNew0 = Abc_NtkObj( pNtk, Aig_NodeFanin0(pAnd)->Data ); - pFaninNew0 = Abc_ObjNotCond( pFaninNew0, Aig_NodeFaninC0(pAnd) ); - // add the first second - pFaninNew1 = Abc_NtkObj( pNtk, Aig_NodeFanin1(pAnd)->Data ); - pFaninNew1 = Abc_ObjNotCond( pFaninNew1, Aig_NodeFaninC1(pAnd) ); - // create the new node - pObjNew = Abc_AigAnd( pNtk->pManFunc, pFaninNew0, pFaninNew1 ); - pAnd->Data = pObjNew->Id; - } - // connect the PO nodes - Abc_NtkForEachCo( pNtkOld, pObj, i ) - { - pAnd = Aig_ManPo( pMan, i ); - pFaninNew = Abc_NtkObj( pNtk, Aig_NodeFanin0(pAnd)->Data ); - pFaninNew = Abc_ObjNotCond( pFaninNew, Aig_NodeFaninC0(pAnd) ); - Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); - } - return pNtk; -} - -/**Function************************************************************* - - Synopsis [Converts the network from the AIG manager into ABC.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld ) -{ - Aig_Param_t Params; - Aig_Man_t * pMan; - Abc_Obj_t * pObj; - Aig_Node_t * pFanin; - int i; - // create the manager - Aig_ManSetDefaultParams( &Params ); - pMan = Aig_ManStart( &Params ); - // create the PIs - Abc_NtkConst1(pNtkOld)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan); - Abc_NtkForEachCi( pNtkOld, pObj, i ) - pObj->pCopy = (Abc_Obj_t *)Aig_NodeCreatePi(pMan); - Abc_NtkForEachCo( pNtkOld, pObj, i ) - pObj->pCopy = (Abc_Obj_t *)Aig_NodeCreatePo(pMan); - // perform the conversion of the internal nodes - Abc_NtkStrashPerformAig( pNtkOld, pMan ); - // create the POs - Abc_NtkForEachCo( pNtkOld, pObj, i ) - { - pFanin = (Aig_Node_t *)Abc_ObjFanin0(pObj)->pCopy; - pFanin = Aig_NotCond( pFanin, Abc_ObjFaninC0(pObj) ); - Aig_NodeConnectPo( pMan, (Aig_Node_t *)pObj->pCopy, pFanin ); - } - return pMan; -} - -/**Function************************************************************* - - Synopsis [Prepares the network for strashing.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Aig_Man_t * pMan ) -{ -// ProgressBar * pProgress; - Vec_Ptr_t * vNodes; - Abc_Obj_t * pNode; - int i; - vNodes = Abc_NtkDfs( pNtk, 0 ); -// pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize ); - Vec_PtrForEachEntry( vNodes, pNode, i ) - { -// Extra_ProgressBarUpdate( pProgress, i, NULL ); - pNode->pCopy = (Abc_Obj_t *)Abc_NodeStrashAig( pMan, pNode ); - } -// Extra_ProgressBarStop( pProgress ); - Vec_PtrFree( vNodes ); -} - -/**Function************************************************************* - - Synopsis [Strashes one logic node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Node_t * Abc_NodeStrashAig( Aig_Man_t * pMan, Abc_Obj_t * pNode ) -{ - int fUseFactor = 1; - char * pSop; - Aig_Node_t * pFanin0, * pFanin1; - extern int Abc_SopIsExorType( char * pSop ); - - assert( Abc_ObjIsNode(pNode) ); - - // consider the case when the graph is an AIG - if ( Abc_NtkIsStrash(pNode->pNtk) ) - { - if ( Abc_NodeIsConst(pNode) ) - return Aig_ManConst1(pMan); - pFanin0 = (Aig_Node_t *)Abc_ObjFanin0(pNode)->pCopy; - pFanin0 = Aig_NotCond( pFanin0, Abc_ObjFaninC0(pNode) ); - pFanin1 = (Aig_Node_t *)Abc_ObjFanin1(pNode)->pCopy; - pFanin1 = Aig_NotCond( pFanin1, Abc_ObjFaninC1(pNode) ); - return Aig_And( pMan, pFanin0, pFanin1 ); - } - - // get the SOP of the node - if ( Abc_NtkHasMapping(pNode->pNtk) ) - pSop = Mio_GateReadSop(pNode->pData); - else - pSop = pNode->pData; - - // consider the constant node - if ( Abc_NodeIsConst(pNode) ) - return Aig_NotCond( Aig_ManConst1(pMan), Abc_SopIsConst0(pSop) ); - - // consider the special case of EXOR function - if ( Abc_SopIsExorType(pSop) ) - return Abc_NodeStrashAigExorAig( pMan, pNode, pSop ); - - // decide when to use factoring - if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 ) - return Abc_NodeStrashAigFactorAig( pMan, pNode, pSop ); - return Abc_NodeStrashAigSopAig( pMan, pNode, pSop ); -} - -/**Function************************************************************* - - Synopsis [Strashes one logic node using its SOP.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Node_t * Abc_NodeStrashAigSopAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop ) -{ - Abc_Obj_t * pFanin; - Aig_Node_t * pAnd, * pSum; - char * pCube; - int i, nFanins; - - // get the number of node's fanins - nFanins = Abc_ObjFaninNum( pNode ); - assert( nFanins == Abc_SopGetVarNum(pSop) ); - // go through the cubes of the node's SOP - pSum = Aig_Not( Aig_ManConst1(pMan) ); - Abc_SopForEachCube( pSop, nFanins, pCube ) - { - // create the AND of literals - pAnd = Aig_ManConst1(pMan); - Abc_ObjForEachFanin( pNode, pFanin, i ) // pFanin can be a net - { - if ( pCube[i] == '1' ) - pAnd = Aig_And( pMan, pAnd, (Aig_Node_t *)pFanin->pCopy ); - else if ( pCube[i] == '0' ) - pAnd = Aig_And( pMan, pAnd, Aig_Not((Aig_Node_t *)pFanin->pCopy) ); - } - // add to the sum of cubes - pSum = Aig_Or( pMan, pSum, pAnd ); - } - // decide whether to complement the result - if ( Abc_SopIsComplement(pSop) ) - pSum = Aig_Not(pSum); - return pSum; -} - -/**Function************************************************************* - - Synopsis [Strashed n-input XOR function.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Node_t * Abc_NodeStrashAigExorAig( Aig_Man_t * pMan, Abc_Obj_t * pNode, char * pSop ) -{ - Abc_Obj_t * pFanin; - Aig_Node_t * pSum; - int i, nFanins; - // get the number of node's fanins - nFanins = Abc_ObjFaninNum( pNode ); - assert( nFanins == Abc_SopGetVarNum(pSop) ); - // go through the cubes of the node's SOP - pSum = Aig_Not( Aig_ManConst1(pMan) ); - for ( i = 0; i < nFanins; i++ ) - { - pFanin = Abc_ObjFanin( pNode, i ); - pSum = Aig_Xor( pMan, pSum, (Aig_Node_t *)pFanin->pCopy ); - } - if ( Abc_SopIsComplement(pSop) ) - pSum = Aig_Not(pSum); - return pSum; -} - -/**Function************************************************************* - - Synopsis [Strashes one logic node using its SOP.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Node_t * Abc_NodeStrashAigFactorAig( Aig_Man_t * pMan, Abc_Obj_t * pRoot, char * pSop ) -{ - Dec_Graph_t * pFForm; - Dec_Node_t * pNode; - Aig_Node_t * pAnd; - int i; - extern Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph ); - - // perform factoring - pFForm = Dec_Factor( pSop ); - // collect the fanins - Dec_GraphForEachLeaf( pFForm, pNode, i ) - pNode->pFunc = Abc_ObjFanin(pRoot,i)->pCopy; - // perform strashing - pAnd = Dec_GraphToNetworkAig( pMan, pFForm ); - Dec_GraphFree( pFForm ); - return pAnd; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c index 0976b652..99ed5636 100644 --- a/src/base/abci/abcNtbdd.c +++ b/src/base/abci/abcNtbdd.c @@ -189,7 +189,7 @@ Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew ) // create the table mapping BDD nodes into the ABC nodes tBdd2Node = st_init_table( st_ptrcmp, st_ptrhash ); // add the constant and the elementary vars - st_insert( tBdd2Node, (char *)b1, (char *)Abc_NtkConst1(pNtkNew) ); + st_insert( tBdd2Node, (char *)b1, (char *)Abc_AigConst1(pNtkNew) ); Abc_ObjForEachFanin( pNodeOld, pFaninOld, i ) st_insert( tBdd2Node, (char *)Cudd_bddIthVar(dd, i), (char *)pFaninOld->pCopy ); // create the new nodes recursively @@ -271,7 +271,7 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly Cudd_Ref( dd->vars[i] ); } // assign the constant node BDD - pNode = Abc_NtkConst1( pNtk ); + pNode = Abc_AigConst1(pNtk); if ( Abc_ObjFanoutNum(pNode) > 0 ) { pNode->pCopy = (Abc_Obj_t *)dd->one; diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index cb32def5..cb1d2a38 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -68,7 +68,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) fprintf( pFile, " net = %5d", Abc_NtkNetNum(pNtk) ); fprintf( pFile, " nd = %5d", Abc_NtkNodeNum(pNtk) ); } - else if ( Abc_NtkHasAig(pNtk) ) + else if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) ) { fprintf( pFile, " and = %5d", Abc_NtkNodeNum(pNtk) ); if ( Num = Abc_NtkGetChoiceNum(pNtk) ) @@ -83,7 +83,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) else fprintf( pFile, " nd = %5d", Abc_NtkNodeNum(pNtk) ); - if ( Abc_NtkHasSop(pNtk) ) + if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) ) + { + } + else if ( Abc_NtkHasSop(pNtk) ) { fprintf( pFile, " cube = %5d", Abc_NtkGetCubeNum(pNtk) ); @@ -91,6 +94,8 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) if ( fFactored ) fprintf( pFile, " lit(fac) = %5d", Abc_NtkGetLitFactNum(pNtk) ); } + else if ( Abc_NtkHasAig(pNtk) ) + fprintf( pFile, " aig = %5d", Abc_NtkGetAigNodeNum(pNtk) ); else if ( Abc_NtkHasBdd(pNtk) ) fprintf( pFile, " bdd = %5d", Abc_NtkGetBddNodeNum(pNtk) ); else if ( Abc_NtkHasMapping(pNtk) ) @@ -98,7 +103,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) fprintf( pFile, " area = %5.2f", Abc_NtkGetMappedArea(pNtk) ); fprintf( pFile, " delay = %5.2f", Abc_NtkDelayTrace(pNtk) ); } - else if ( !Abc_NtkHasAig(pNtk) ) + else if ( !Abc_NtkHasBlackbox(pNtk) ) { assert( 0 ); } @@ -661,12 +666,15 @@ void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary ) return; } + if ( Abc_NtkIsAigLogic(pNtk) ) + return; + // transform logic functions from BDD to SOP if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) ) { if ( !Abc_NtkBddToSop(pNtk, 0) ) { - printf( "Converting to SOPs has failed.\n" ); + printf( "Abc_NtkPrintGates(): Converting to SOPs has failed.\n" ); return; } } @@ -785,6 +793,40 @@ void Abc_NtkPrintStrSupports( Abc_Ntk_t * pNtk ) } } +/**Function************************************************************* + + Synopsis [Prints information about the clock skew schedule.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkPrintSkews( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintAll ) { + + Abc_Obj_t * pObj; + int i; + int nNonZero = 0; + float skew, sum = 0.0, avg; + + if (fPrintAll) fprintf( pFile, "Full Clock Skew Schedule:\n\tGlobal Skew = %.2f\n", pNtk->globalSkew ); + + Abc_NtkForEachLatch( pNtk, pObj, i ) { + skew = Abc_NtkGetLatSkew( pNtk, i ); + if ( skew != 0.0 ) { + nNonZero++; + sum += ABS( skew ); + } + if (fPrintAll) fprintf( pFile, "\tLatch %d (Id = %d) \t Endpoint Skew = %.2f\n", i, pObj->Id, skew); + } + + avg = sum / Abc_NtkLatchNum( pNtk ); + + fprintf( pFile, "Endpoint Skews : Total |Skew| = %.2f\t Avg |Skew| = %.2f\t Non-Zero Skews = %d\n", + sum, avg, nNonZero ); +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c index 3dd6c519..3d301cd6 100644 --- a/src/base/abci/abcRefactor.c +++ b/src/base/abci/abcRefactor.c @@ -109,8 +109,8 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool { Extra_ProgressBarUpdate( pProgress, i, NULL ); // skip the constant node - if ( Abc_NodeIsConst(pNode) ) - continue; +// if ( Abc_NodeIsConst(pNode) ) +// continue; // skip persistant nodes if ( Abc_NodeIsPersistant(pNode) ) continue; diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c index f7d351d2..2e448ce5 100644 --- a/src/base/abci/abcRenode.c +++ b/src/base/abci/abcRenode.c @@ -124,7 +124,7 @@ void Abc_NtkRenodeInt( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) int i; // set the constant node - pConst1 = Abc_NtkConst1(pNtk); + pConst1 = Abc_AigConst1(pNtk); if ( Abc_ObjFanoutNum(pConst1) > 0 ) { pNodeNew = Abc_NtkCreateNode( pNtkNew ); @@ -173,7 +173,7 @@ Abc_Obj_t * Abc_NtkRenode_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld ) if ( pNodeOld->pCopy ) return pNodeOld->pCopy; assert( Abc_ObjIsNode(pNodeOld) ); - assert( !Abc_NodeIsConst(pNodeOld) ); + assert( !Abc_AigNodeIsConst(pNodeOld) ); assert( pNodeOld->fMarkA ); //printf( "%d ", Abc_NodeMffcSizeSupp(pNodeOld) ); @@ -214,7 +214,7 @@ DdNode * Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t Abc_Obj_t * pFaninOld; DdNode * bFunc; int i; - assert( !Abc_NodeIsConst(pNodeOld) ); + assert( !Abc_AigNodeIsConst(pNodeOld) ); assert( Abc_ObjIsNode(pNodeOld) ); // set the elementary BDD variables for the input nodes for ( i = 0; i < vFaninsOld->nSize; i++ ) @@ -389,8 +389,8 @@ void Abc_NtkRenodeSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax ) Abc_NtkForEachNode( pNtk, pNode, i ) { // skip PI/PO nodes - if ( Abc_NodeIsConst(pNode) ) - continue; +// if ( Abc_NodeIsConst(pNode) ) +// continue; // mark the nodes with multiple fanouts nFanouts = Abc_ObjFanoutNum(pNode); nConeSize = Abc_NodeMffcSize(pNode); @@ -406,8 +406,8 @@ void Abc_NtkRenodeSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax ) Abc_NtkForEachNode( pNtk, pNode, i ) { // skip PI/PO nodes - if ( Abc_NodeIsConst(pNode) ) - continue; +// if ( Abc_NodeIsConst(pNode) ) +// continue; if ( pNode->fMarkA == 0 ) continue; // continue cutting branches until it meets the fanin limit @@ -420,8 +420,8 @@ void Abc_NtkRenodeSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax ) Abc_NtkForEachNode( pNtk, pNode, i ) { // skip PI/PO nodes - if ( Abc_NodeIsConst(pNode) ) - continue; +// if ( Abc_NodeIsConst(pNode) ) +// continue; if ( pNode->fMarkA == 0 ) continue; Abc_NtkRenodeCone( pNode, vCone ); @@ -455,8 +455,8 @@ void Abc_NtkRenodeSetBoundsCnf( Abc_Ntk_t * pNtk ) Abc_NtkForEachNode( pNtk, pNode, i ) { // skip PI/PO nodes - if ( Abc_NodeIsConst(pNode) ) - continue; +// if ( Abc_NodeIsConst(pNode) ) +// continue; // mark the nodes with multiple fanouts if ( Abc_ObjFanoutNum(pNode) > 1 ) pNode->fMarkA = 1; @@ -487,8 +487,8 @@ void Abc_NtkRenodeSetBoundsCnf( Abc_Ntk_t * pNtk ) Abc_NtkForEachNode( pNtk, pNode, i ) { // skip PI/PO nodes - if ( Abc_NodeIsConst(pNode) ) - continue; +// if ( Abc_NodeIsConst(pNode) ) +// continue; if ( Abc_NodeIsMuxType(pNode) && Abc_ObjFanin0(pNode)->fMarkA == 0 && Abc_ObjFanin1(pNode)->fMarkA == 0 ) @@ -521,8 +521,8 @@ void Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk, int nThresh ) Abc_NtkForEachNode( pNtk, pNode, i ) { // skip PI/PO nodes - if ( Abc_NodeIsConst(pNode) ) - continue; +// if ( Abc_NodeIsConst(pNode) ) +// continue; // mark the nodes with multiple fanouts // if ( Abc_ObjFanoutNum(pNode) > 1 ) // pNode->fMarkA = 1; diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c index d738123a..9dc84999 100644 --- a/src/base/abci/abcRestruct.c +++ b/src/base/abci/abcRestruct.c @@ -132,8 +132,8 @@ pManRst->timeCut += clock() - clk; { Extra_ProgressBarUpdate( pProgress, i, NULL ); // skip the constant node - if ( Abc_NodeIsConst(pNode) ) - continue; +// if ( Abc_NodeIsConst(pNode) ) +// continue; // skip persistant nodes if ( Abc_NodeIsPersistant(pNode) ) continue; diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c index b0061b61..9fcc6979 100644 --- a/src/base/abci/abcResub.c +++ b/src/base/abci/abcResub.c @@ -158,8 +158,8 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, bool fUpd { Extra_ProgressBarUpdate( pProgress, i, NULL ); // skip the constant node - if ( Abc_NodeIsConst(pNode) ) - continue; +// if ( Abc_NodeIsConst(pNode) ) +// continue; // skip persistant nodes if ( Abc_NodeIsPersistant(pNode) ) continue; diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c index 703f05d9..2af10271 100644 --- a/src/base/abci/abcRewrite.c +++ b/src/base/abci/abcRewrite.c @@ -86,8 +86,8 @@ Rwr_ManAddTimeCuts( pManRwr, clock() - clk ); if ( i >= nNodes ) break; // skip the constant node - if ( Abc_NodeIsConst(pNode) ) - continue; +// if ( Abc_NodeIsConst(pNode) ) +// continue; // skip persistant nodes if ( Abc_NodeIsPersistant(pNode) ) continue; diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c index b3788d31..61bc8b09 100644 --- a/src/base/abci/abcRr.c +++ b/src/base/abci/abcRr.c @@ -120,8 +120,8 @@ int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFa if ( i >= nNodes ) break; // skip the constant node - if ( Abc_NodeIsConst(pNode) ) - continue; +// if ( Abc_NodeIsConst(pNode) ) +// continue; // skip persistant nodes if ( Abc_NodeIsPersistant(pNode) ) continue; @@ -680,8 +680,7 @@ Abc_Ntk_t * Abc_NtkWindow( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vC // duplicate the name and the spec pNtkNew->pName = Extra_UtilStrsav( "temp" ); // map the constant nodes - if ( Abc_NtkConst1(pNtk) ) - Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew); + Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); // create and map the PIs Vec_PtrForEachEntry( vLeaves, pObj, i ) pObj->pCopy = Abc_NtkCreatePi(pNtkNew); @@ -728,7 +727,7 @@ void Abc_NtkRRSimulateStart( Abc_Ntk_t * pNtk ) Abc_Obj_t * pObj; unsigned uData, uData0, uData1; int i; - Abc_NtkConst1(pNtk)->pData = (void *)~((unsigned)0); + Abc_AigConst1(pNtk)->pData = (void *)~((unsigned)0); Abc_NtkForEachCi( pNtk, pObj, i ) pObj->pData = (void *)SIM_RANDOM_UNSIGNED; Abc_NtkForEachNode( pNtk, pObj, i ) @@ -801,7 +800,7 @@ Vec_Str_t * Abc_NtkRRSimulate( Abc_Ntk_t * pNtk ) } // simulate patters and store them in copy - Abc_NtkConst1(pNtk)->pCopy = (Abc_Obj_t *)~((unsigned)0); + Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)~((unsigned)0); Abc_NtkForEachCi( pNtk, pObj, i ) pObj->pCopy = (Abc_Obj_t *)SIM_RANDOM_UNSIGNED; Abc_NtkForEachNode( pNtk, pObj, i ) diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index b8491d06..86f13884 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -452,7 +452,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront ) // vCircuit = Vec_VecStart( 184 ); // add the clause for the constant node - pNode = Abc_NtkConst1(pNtk); + pNode = Abc_AigConst1(pNtk); pNode->fMarkA = 1; pNode->pCopy = (Abc_Obj_t *)vNodes->nSize; Vec_PtrPush( vNodes, pNode ); @@ -488,7 +488,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront ) Vec_PtrForEachEntry( vNodes, pNode, i ) { assert( !Abc_ObjIsComplement(pNode) ); - if ( !Abc_NodeIsAigAnd(pNode) ) + if ( !Abc_AigNodeIsAnd(pNode) ) continue; //printf( "%d ", pNode->Id ); diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index b546d8be..c69aeabf 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -26,13 +26,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -// static functions -static void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fAllNodes ); -static Abc_Obj_t * Abc_NodeStrashSop( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop ); -static Abc_Obj_t * Abc_NodeStrashExor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop ); -static Abc_Obj_t * Abc_NodeStrashFactor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop ); - -extern char * Mio_GateReadSop( void * pGate ); +static void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, bool fAllNodes ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -40,10 +34,57 @@ extern char * Mio_GateReadSop( void * pGate ); /**Function************************************************************* - Synopsis [Creates the strashed AIG network.] + Synopsis [Reapplies structural hashing to the AIG.] + + Description [Because of the structural hashing, this procedure should not + change the number of nodes. It is useful to detect the bugs in the original AIG.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup ) +{ + Abc_Ntk_t * pNtkAig; + Abc_Obj_t * pObj; + int i, nNodes; + assert( Abc_NtkIsStrash(pNtk) ); + // 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 + 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 ) + pObj->pCopy = Abc_AigAnd( pNtkAig->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); + // finalize the network + Abc_NtkFinalize( pNtk, pNtkAig ); + // print warning about self-feed latches +// if ( Abc_NtkCountSelfFeedLatches(pNtkAig) ) +// printf( "Warning: The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtkAig) ); + // perform cleanup if requested + if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) ) + printf( "Abc_NtkRestrash(): AIG cleanup removed %d nodes (this is a bug).\n", nNodes ); + // duplicate EXDC + if ( pNtk->pExdc ) + pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc ); + // make sure everything is okay + if ( !Abc_NtkCheck( pNtkAig ) ) + { + printf( "Abc_NtkStrash: The network check has failed.\n" ); + Abc_NtkDelete( pNtkAig ); + return NULL; + } + return pNtkAig; + +} + +/**Function************************************************************* + + Synopsis [Transforms logic network into structurally hashed AIG.] - Description [Converts the logic network or the AIG into a - structurally hashed AIG.] + Description [] SideEffects [] @@ -54,33 +95,28 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup ) { Abc_Ntk_t * pNtkAig; int nNodes; - - assert( !Abc_NtkIsNetlist(pNtk) ); - assert( !Abc_NtkIsSeq(pNtk) ); - if ( Abc_NtkIsBddLogic(pNtk) ) + assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) ); + // consider the special case when the network is already structurally hashed + if ( Abc_NtkIsStrash(pNtk) ) + return Abc_NtkRestrash( pNtk, fCleanup ); + // convert the node representation in the logic network to the AIG form + if ( !Abc_NtkLogicToAig(pNtk) ) { - if ( !Abc_NtkBddToSop(pNtk, 0) ) - { - printf( "Converting to SOPs has failed.\n" ); - return NULL; - } + printf( "Converting to AIGs has failed.\n" ); + return NULL; } - // print warning about choice nodes - if ( Abc_NtkGetChoiceNum( pNtk ) ) - printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" ); // perform strashing + Abc_NtkCleanCopy( pNtk ); pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); - if ( Abc_NtkConst1(pNtk) ) - Abc_NtkConst1(pNtk)->pCopy = NULL; Abc_NtkStrashPerform( pNtk, pNtkAig, fAllNodes ); Abc_NtkFinalize( pNtk, pNtkAig ); // print warning about self-feed latches // if ( Abc_NtkCountSelfFeedLatches(pNtkAig) ) // printf( "Warning: The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtkAig) ); - if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) ) - { + // perform cleanup if requested + nNodes = fCleanup? Abc_AigCleanup(pNtkAig->pManFunc) : 0; +// if ( nNodes ) // printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes ); - } // duplicate EXDC if ( pNtk->pExdc ) pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc ); @@ -115,13 +151,10 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) // the first network should be an AIG assert( Abc_NtkIsStrash(pNtk1) ); assert( Abc_NtkIsLogic(pNtk2) || Abc_NtkIsStrash(pNtk2) ); - if ( Abc_NtkIsBddLogic(pNtk2) ) + if ( Abc_NtkIsLogic(pNtk2) && !Abc_NtkLogicToAig(pNtk2) ) { - if ( !Abc_NtkBddToSop(pNtk2, 0) ) - { - printf( "Converting to SOPs has failed.\n" ); - return 0; - } + printf( "Converting to AIGs has failed.\n" ); + return 0; } // check that the networks have the same PIs // reorder PIs of pNtk2 according to pNtk1 @@ -132,7 +165,11 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) Abc_NtkForEachCi( pNtk2, pObj, i ) pObj->pCopy = Abc_NtkCi(pNtk1, i); // add pNtk2 to pNtk1 while strashing - Abc_NtkStrashPerform( pNtk2, pNtk1, 1 ); + if ( Abc_NtkIsLogic(pNtk2) ) + Abc_NtkStrashPerform( pNtk2, pNtk1, 1 ); + else + Abc_NtkForEachNode( pNtk2, pObj, i ) + pObj->pCopy = Abc_AigAnd( pNtk1->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); // make sure that everything is okay if ( !Abc_NtkCheck( pNtk1 ) ) { @@ -142,7 +179,6 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) return 1; } - /**Function************************************************************* Synopsis [Prepares the network for strashing.] @@ -154,85 +190,28 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) SeeAlso [] ***********************************************************************/ -void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, bool fAllNodes ) +void Abc_NtkStrashPerform( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew, bool fAllNodes ) { ProgressBar * pProgress; Vec_Ptr_t * vNodes; - Abc_Obj_t * pNode, * pNodeNew, * pObj; + Abc_Obj_t * pNodeOld; int i; - - // perform strashing - vNodes = Abc_NtkDfs( pNtk, fAllNodes ); + assert( Abc_NtkIsLogic(pNtkOld) ); + assert( Abc_NtkIsStrash(pNtkNew) ); + vNodes = Abc_NtkDfs( pNtkOld, fAllNodes ); pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize ); - Vec_PtrForEachEntry( vNodes, pNode, i ) + Vec_PtrForEachEntry( vNodes, pNodeOld, i ) { Extra_ProgressBarUpdate( pProgress, i, NULL ); - // get the node - assert( Abc_ObjIsNode(pNode) ); - // strash the node - pNodeNew = Abc_NodeStrash( pNtkNew, pNode ); - // get the old object - pObj = Abc_ObjFanout0Ntk( pNode ); - // make sure the node is not yet strashed - assert( pObj->pCopy == NULL ); - // mark the old object with the new AIG node - pObj->pCopy = pNodeNew; - Abc_HManAddProto( pObj->pCopy, pObj ); + pNodeOld->pCopy = Abc_NodeStrash( pNtkNew, pNodeOld ); } - Vec_PtrFree( vNodes ); Extra_ProgressBarStop( pProgress ); + Vec_PtrFree( vNodes ); } /**Function************************************************************* - Synopsis [Strashes one logic node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode ) -{ - int fUseFactor = 1; - char * pSop; - extern int Abc_SopIsExorType( char * pSop ); - - assert( Abc_ObjIsNode(pNode) ); - - // consider the case when the graph is an AIG - if ( Abc_NtkIsStrash(pNode->pNtk) ) - { - if ( Abc_NodeIsConst(pNode) ) - return Abc_NtkConst1(pNtkNew); - return Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) ); - } - - // get the SOP of the node - if ( Abc_NtkHasMapping(pNode->pNtk) ) - pSop = Mio_GateReadSop(pNode->pData); - else - pSop = pNode->pData; - - // consider the constant node - if ( Abc_NodeIsConst(pNode) ) - return Abc_ObjNotCond( Abc_NtkConst1(pNtkNew), Abc_SopIsConst0(pSop) ); - - // consider the special case of EXOR function - if ( Abc_SopIsExorType(pSop) ) - return Abc_NodeStrashExor( pNtkNew, pNode, pSop ); - - // decide when to use factoring - if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 ) - return Abc_NodeStrashFactor( pNtkNew, pNode, pSop ); - return Abc_NodeStrashSop( pNtkNew, pNode, pSop ); -} - -/**Function************************************************************* - - Synopsis [Strashes one logic node using its SOP.] + Synopsis [Transfers the AIG from one manager into another.] Description [] @@ -241,96 +220,56 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -Abc_Obj_t * Abc_NodeStrashSop( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop ) +void Abc_NodeStrash_rec( Abc_Aig_t * pMan, Aig_Obj_t * pObj ) { - Abc_Aig_t * pMan = pNtkNew->pManFunc; - Abc_Obj_t * pFanin, * pAnd, * pSum; - char * pCube; - int i, nFanins; - - // get the number of node's fanins - nFanins = Abc_ObjFaninNum( pNode ); - assert( nFanins == Abc_SopGetVarNum(pSop) ); - // go through the cubes of the node's SOP - pSum = Abc_ObjNot( Abc_NtkConst1(pNtkNew) ); - Abc_SopForEachCube( pSop, nFanins, pCube ) - { - // create the AND of literals - pAnd = Abc_NtkConst1(pNtkNew); - Abc_ObjForEachFanin( pNode, pFanin, i ) // pFanin can be a net - { - if ( pCube[i] == '1' ) - pAnd = Abc_AigAnd( pMan, pAnd, pFanin->pCopy ); - else if ( pCube[i] == '0' ) - pAnd = Abc_AigAnd( pMan, pAnd, Abc_ObjNot(pFanin->pCopy) ); - } - // add to the sum of cubes - pSum = Abc_AigOr( pMan, pSum, pAnd ); - } - // decide whether to complement the result - if ( Abc_SopIsComplement(pSop) ) - pSum = Abc_ObjNot(pSum); - return pSum; + assert( !Aig_IsComplement(pObj) ); + if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) ) + return; + Abc_NodeStrash_rec( pMan, Aig_ObjFanin0(pObj) ); + Abc_NodeStrash_rec( pMan, Aig_ObjFanin1(pObj) ); + pObj->pData = Abc_AigAnd( pMan, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) ); + assert( !Aig_ObjIsMarkA(pObj) ); // loop detection + Aig_ObjSetMarkA( pObj ); } /**Function************************************************************* - Synopsis [Strashed n-input XOR function.] + Synopsis [Strashes one logic node.] - Description [] + Description [Assume the network is in the AIG form] SideEffects [] - + SeeAlso [] ***********************************************************************/ -Abc_Obj_t * Abc_NodeStrashExor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop ) +Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld ) { - Abc_Aig_t * pMan = pNtkNew->pManFunc; - Abc_Obj_t * pFanin, * pSum; - int i, nFanins; - // get the number of node's fanins - nFanins = Abc_ObjFaninNum( pNode ); - assert( nFanins == Abc_SopGetVarNum(pSop) ); - // go through the cubes of the node's SOP - pSum = Abc_ObjNot( Abc_NtkConst1(pNtkNew) ); - for ( i = 0; i < nFanins; i++ ) - { - pFanin = Abc_ObjFanin( pNode, i ); - pSum = Abc_AigXor( pMan, pSum, pFanin->pCopy ); - } - if ( Abc_SopIsComplement(pSop) ) - pSum = Abc_ObjNot(pSum); - return pSum; + Aig_Man_t * pMan; + Aig_Obj_t * pRoot; + Abc_Obj_t * pFanin; + int i; + assert( Abc_ObjIsNode(pNodeOld) ); + assert( Abc_NtkIsAigLogic(pNodeOld->pNtk) ); + // get the local AIG manager and the local root node + pMan = pNodeOld->pNtk->pManFunc; + pRoot = pNodeOld->pData; + // check the constant case + if ( Abc_NodeIsConst(pNodeOld) ) + return Abc_ObjNotCond( Abc_AigConst1(pNtkNew), Aig_IsComplement(pRoot) ); + // set elementary variables + Abc_ObjForEachFanin( pNodeOld, pFanin, i ) + Aig_IthVar(pMan, i)->pData = pFanin->pCopy; + // strash the AIG of this node + Abc_NodeStrash_rec( pNtkNew->pManFunc, Aig_Regular(pRoot) ); + Aig_ConeUnmark_rec( Aig_Regular(pRoot) ); + // return the final node + return Abc_ObjNotCond( Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) ); } -/**Function************************************************************* - - Synopsis [Strashes one logic node using its SOP.] - Description [] - - SideEffects [] - SeeAlso [] -***********************************************************************/ -Abc_Obj_t * Abc_NodeStrashFactor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pRoot, char * pSop ) -{ - Dec_Graph_t * pFForm; - Dec_Node_t * pNode; - Abc_Obj_t * pAnd; - int i; - // perform factoring - pFForm = Dec_Factor( pSop ); - // collect the fanins - Dec_GraphForEachLeaf( pFForm, pNode, i ) - pNode->pFunc = Abc_ObjFanin(pRoot,i)->pCopy; - // perform strashing - pAnd = Dec_GraphToNetwork( pNtkNew, pFForm ); - Dec_GraphFree( pFForm ); - return pAnd; -} @@ -380,7 +319,7 @@ Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels ) // start the network pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG ); pNtkNew->pName = Extra_UtilStrsav(pNtk->pName); - Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew); + Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); // create PIs below the cut and nodes above the cut Abc_NtkCleanCopy( pNtk ); pObjNew = Abc_NtkTopmost_rec( pNtkNew, Abc_ObjFanin0(Abc_NtkPo(pNtk, 0)), LevelCut ); diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c index 3665584e..8f1ab180 100644 --- a/src/base/abci/abcSweep.c +++ b/src/base/abci/abcSweep.c @@ -448,7 +448,7 @@ int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose ) { Vec_Ptr_t * vNodes; int Counter; - assert( !Abc_NtkHasAig(pNtk) ); + assert( Abc_NtkIsLogic(pNtk) ); // mark the nodes reachable from the POs vNodes = Abc_NtkDfs( pNtk, 0 ); Counter = Abc_NtkReduceNodes( pNtk, vNodes ); @@ -473,7 +473,7 @@ int Abc_NtkReduceNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes ) { Abc_Obj_t * pNode; int i, Counter; - assert( !Abc_NtkIsStrash(pNtk) ); + assert( Abc_NtkIsLogic(pNtk) ); // mark the nodes reachable from the POs for ( i = 0; i < vNodes->nSize; i++ ) { @@ -481,9 +481,6 @@ int Abc_NtkReduceNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes ) assert( Abc_ObjIsNode(pNode) ); pNode->fMarkA = 1; } - // if it is an AIG, also mark the constant 1 node - if ( Abc_NtkConst1(pNtk) ) - Abc_NtkConst1(pNtk)->fMarkA = 1; // remove the non-marked nodes Counter = 0; Abc_NtkForEachNode( pNtk, pNode, i ) diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c index d2d731d9..5add0dda 100644 --- a/src/base/abci/abcTiming.c +++ b/src/base/abci/abcTiming.c @@ -37,9 +37,9 @@ struct Abc_ManTime_t_ // static functions static Abc_ManTime_t * Abc_ManTimeStart(); static void Abc_ManTimeExpand( Abc_ManTime_t * p, int nSize, int fProgressive ); -static void Abc_NtkTimePrepare( Abc_Ntk_t * pNtk ); +void Abc_NtkTimePrepare( Abc_Ntk_t * pNtk ); -static void Abc_NodeDelayTraceArrival( Abc_Obj_t * pNode ); +void Abc_NodeDelayTraceArrival( Abc_Obj_t * pNode ); // accessing the arrival and required times of a node static inline Abc_Time_t * Abc_NodeArrival( Abc_Obj_t * pNode ) { return pNode->pNtk->pManTime->vArrs->pArray[pNode->Id]; } @@ -595,13 +595,12 @@ void Abc_NodeDelayTraceArrival( Abc_Obj_t * pNode ) // start the arrival time of the node pTimeOut = Abc_NodeArrival(pNode); - pTimeOut->Rise = pTimeOut->Fall = 0; + pTimeOut->Rise = pTimeOut->Fall = -ABC_INFINITY; // go through the pins of the gate pPin = Mio_GateReadPins(pNode->pData); Abc_ObjForEachFanin( pNode, pFanin, i ) { pTimeIn = Abc_NodeArrival(pFanin); - assert( pTimeIn->Worst != -ABC_INFINITY ); // get the interesting parameters of this pin PinPhase = Mio_PinReadPhase(pPin); tDelayBlockRise = (float)Mio_PinReadDelayBlockRise( pPin ); @@ -647,7 +646,7 @@ void Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk ) Vec_Ptr_t * vNodes; Abc_Obj_t * pObj, * pFanout; int i, k, nLevelsCur; -// assert( Abc_NtkIsStrash(pNtk) ); + assert( Abc_NtkIsStrash(pNtk) ); // remember the maximum number of direct levels // pNtk->LevelMax = Abc_AigGetLevelNum(pNtk); pNtk->LevelMax = Abc_NtkGetLevelNum(pNtk); diff --git a/src/base/abci/abcTrace.c b/src/base/abci/abcTrace.c deleted file mode 100644 index 4abe235e..00000000 --- a/src/base/abci/abcTrace.c +++ /dev/null @@ -1,804 +0,0 @@ -/**CFile**************************************************************** - - FileName [abcHistory.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Network and node package.] - - Synopsis [] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: abcHistory.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -#define ABC_SIM_VARS 16 // the max number of variables in the cone -#define ABC_SIM_OBJS 200 // the max number of objects in the cone - -typedef struct Abc_HMan_t_ Abc_HMan_t; -typedef struct Abc_HObj_t_ Abc_HObj_t; -typedef struct Abc_HNum_t_ Abc_HNum_t; - -struct Abc_HNum_t_ -{ - unsigned fCompl : 1; // set to 1 if the node is complemented - unsigned NtkId : 6; // the network ID - unsigned ObjId : 24; // the node ID -}; - -struct Abc_HObj_t_ -{ - // object info - unsigned fProof : 1; // set to 1 if the node is proved - unsigned fPhase : 1; // set to 1 if the node's phase differs from Old - unsigned fPi : 1; // the node is a PI - unsigned fPo : 1; // the node is a PO - unsigned fConst : 1; // the node is a constant - unsigned fVisited: 1; // the flag shows if the node is visited - unsigned NtkId : 10; // the network ID - unsigned Num : 16; // a temporary number - // history record - Abc_HNum_t Fan0; // immediate fanin - Abc_HNum_t Fan1; // immediate fanin - Abc_HNum_t Proto; // old node if present -// Abc_HNum_t Equ; // equiv node if present -}; - -struct Abc_HMan_t_ -{ - // storage for history information - Vec_Vec_t * vNtks; // the history nodes belonging to each network - Vec_Int_t * vProof; // flags showing if the network is proved - // storage for simulation info - int nVarsMax; // the max number of cone leaves - int nObjsMax; // the max number of cone nodes - Vec_Ptr_t * vObjs; // the cone nodes - int nBits; // the number of simulation bits - int nWords; // the number of unsigneds for siminfo - int nWordsCur; // the current number of words - Vec_Ptr_t * vSims; // simulation info - unsigned * pInfo; // pointer to simulation info - // other info - Vec_Ptr_t * vCone0; - Vec_Ptr_t * vCone1; - // memory manager - Extra_MmFixed_t* pMmObj; // memory manager for objects -}; - -static Abc_HMan_t * s_pHMan = NULL; - -static inline int Abc_HObjProof( Abc_HObj_t * p ) { return p->fProof; } -static inline int Abc_HObjPhase( Abc_HObj_t * p ) { return p->fPhase; } -static inline int Abc_HObjPi ( Abc_HObj_t * p ) { return p->fPi; } -static inline int Abc_HObjPo ( Abc_HObj_t * p ) { return p->fPo; } -static inline int Abc_HObjConst( Abc_HObj_t * p ) { return p->fConst; } -static inline int Abc_HObjNtkId( Abc_HObj_t * p ) { return p->NtkId; } -static inline int Abc_HObjNum ( Abc_HObj_t * p ) { return p->Num; } -static inline Abc_HObj_t * Abc_HObjFanin0( Abc_HObj_t * p ) { return !p->Fan0.NtkId ? NULL : Vec_PtrEntry( Vec_VecEntry(s_pHMan->vNtks, p->Fan0.NtkId), p->Fan0.ObjId ); } -static inline Abc_HObj_t * Abc_HObjFanin1( Abc_HObj_t * p ) { return !p->Fan1.NtkId ? NULL : Vec_PtrEntry( Vec_VecEntry(s_pHMan->vNtks, p->Fan1.NtkId), p->Fan1.ObjId ); } -static inline Abc_HObj_t * Abc_HObjProto ( Abc_HObj_t * p ) { return !p->Proto.NtkId ? NULL : Vec_PtrEntry( Vec_VecEntry(s_pHMan->vNtks, p->Proto.NtkId), p->Proto.ObjId ); } -static inline int Abc_HObjFaninC0( Abc_HObj_t * p ) { return p->Fan0.fCompl; } -static inline int Abc_HObjFaninC1( Abc_HObj_t * p ) { return p->Fan1.fCompl; } - -static inline Abc_HObj_t * Abc_ObjHObj( Abc_Obj_t * p ) { return Vec_PtrEntry( Vec_VecEntry(s_pHMan->vNtks, p->pNtk->Id), p->Id ); } - -static int Abc_HManVerifyPair( int NtkIdOld, int NtkIdNew ); -static int Abc_HManVerifyNodes_rec( Abc_HObj_t * pHOld, Abc_HObj_t * pHNew ); - -static Vec_Ptr_t * Abc_HManCollectLeaves( Abc_HObj_t * pHNew ); -static Vec_Ptr_t * Abc_HManCollectCone( Abc_HObj_t * pHOld, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone ); -static int Abc_HManSimulate( Vec_Ptr_t * vCone0, Vec_Ptr_t * vCone1, int nLeaves, int * pPhase ); - - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_HManStart() -{ - Abc_HMan_t * p; - unsigned * pData; - int i, k; - assert( s_pHMan == NULL ); - assert( sizeof(unsigned) == 4 ); - // allocate manager - p = ALLOC( Abc_HMan_t, 1 ); - memset( p, 0, sizeof(Abc_HMan_t) ); - // allocate storage for all nodes - p->vNtks = Vec_VecStart( 1 ); - p->vProof = Vec_IntStart( 1 ); - // allocate temporary storage for objects - p->nVarsMax = ABC_SIM_VARS; - p->nObjsMax = ABC_SIM_OBJS; - p->vObjs = Vec_PtrAlloc( p->nObjsMax ); - // allocate simulation info - p->nBits = (1 << p->nVarsMax); - p->nWords = (p->nBits <= 32)? 1 : (p->nBits / 32); - p->pInfo = ALLOC( unsigned, p->nWords * p->nObjsMax ); - memset( p->pInfo, 0, sizeof(unsigned) * p->nWords * p->nVarsMax ); - p->vSims = Vec_PtrAlloc( p->nObjsMax ); - for ( i = 0; i < p->nObjsMax; i++ ) - Vec_PtrPush( p->vSims, p->pInfo + i * p->nWords ); - // set elementary truth tables - for ( k = 0; k < p->nVarsMax; k++ ) - { - pData = p->vSims->pArray[k]; - for ( i = 0; i < p->nBits; i++ ) - if ( i & (1 << k) ) - pData[i>>5] |= (1 << (i&31)); - } - // allocate storage for the nodes - p->pMmObj = Extra_MmFixedStart( sizeof(Abc_HObj_t) ); - p->vCone0 = Vec_PtrAlloc( p->nObjsMax ); - p->vCone1 = Vec_PtrAlloc( p->nObjsMax ); - s_pHMan = p; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_HManStop() -{ - assert( s_pHMan != NULL ); - Extra_MmFixedStop( s_pHMan->pMmObj, 0 ); - Vec_PtrFree( s_pHMan->vObjs ); - Vec_PtrFree( s_pHMan->vSims ); - Vec_VecFree( s_pHMan->vNtks ); - Vec_IntFree( s_pHMan->vProof ); - Vec_PtrFree( s_pHMan->vCone0 ); - Vec_PtrFree( s_pHMan->vCone1 ); - free( s_pHMan->pInfo ); - free( s_pHMan ); - s_pHMan = NULL; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_HManIsRunning() -{ - return s_pHMan != NULL; -} - -/**Function************************************************************* - - Synopsis [Called when a new network is created.] - - Description [Returns the new ID for the network.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_HManGetNewNtkId() -{ - if ( s_pHMan == NULL ) - return 0; - return Vec_VecSize( s_pHMan->vNtks ); // what if the new network has no nodes? -} - -/**Function************************************************************* - - Synopsis [Called when the object is created.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_HManAddObj( Abc_Obj_t * pObj ) -{ - Abc_HObj_t * pHObj; - if ( s_pHMan == NULL ) - return; - pHObj = (Abc_HObj_t *)Extra_MmFixedEntryFetch( s_pHMan->pMmObj ); - memset( pHObj, 0, sizeof(Abc_HObj_t) ); - // set the object type - pHObj->NtkId = pObj->pNtk->Id; - if ( Abc_ObjIsCi(pObj) ) - pHObj->fPi = 1; - else if ( Abc_ObjIsCo(pObj) ) - pHObj->fPo = 1; - Vec_VecPush( s_pHMan->vNtks, pObj->pNtk->Id, pHObj ); - // set the proof parameter for the network - if ( Vec_IntSize( s_pHMan->vProof ) == pObj->pNtk->Id ) - Vec_IntPush( s_pHMan->vProof, 0 ); -} - -/**Function************************************************************* - - Synopsis [Called when the fanin is added to the object.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_HManAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin ) -{ - Abc_HObj_t * pHObj; - int fCompl; - if ( s_pHMan == NULL ) - return; - // take off the complemented attribute - assert( !Abc_ObjIsComplement(pObj) ); - fCompl = Abc_ObjIsComplement(pFanin); - pFanin = Abc_ObjRegular(pFanin); - // add the fanin - assert( pObj->pNtk == pFanin->pNtk ); - pHObj = Abc_ObjHObj(pObj); - if ( pHObj->Fan0.NtkId == 0 ) - { - pHObj->Fan0.NtkId = pFanin->pNtk->Id; - pHObj->Fan0.ObjId = pFanin->Id; - pHObj->Fan0.fCompl = fCompl; - } - else if ( pHObj->Fan1.NtkId == 0 ) - { - pHObj->Fan1.NtkId = pFanin->pNtk->Id; - pHObj->Fan1.ObjId = pFanin->Id; - pHObj->Fan1.fCompl = fCompl; - } - else assert( 0 ); -} - -/**Function************************************************************* - - Synopsis [Called when the fanin's input should be complemented.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_HManXorFaninC( Abc_Obj_t * pObj, int iFanin ) -{ - Abc_HObj_t * pHObj; - if ( s_pHMan == NULL ) - return; - assert( iFanin < 2 ); - pHObj = Abc_ObjHObj(pObj); - if ( iFanin == 0 ) - pHObj->Fan0.fCompl ^= 1; - else if ( iFanin == 1 ) - pHObj->Fan1.fCompl ^= 1; -} - -/**Function************************************************************* - - Synopsis [Called when the fanin is added to the object.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_HManRemoveFanins( Abc_Obj_t * pObj ) -{ - Abc_HObj_t * pHObj; - if ( s_pHMan == NULL ) - return; - assert( !Abc_ObjIsComplement(pObj) ); - pHObj = Abc_ObjHObj(pObj); - pHObj->Fan0.NtkId = 0; - pHObj->Fan0.ObjId = 0; - pHObj->Fan0.fCompl = 0; - pHObj->Fan1.NtkId = 0; - pHObj->Fan1.ObjId = 0; - pHObj->Fan1.fCompl = 0; -} - -/**Function************************************************************* - - Synopsis [Called when a new prototype of the old object is set.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_HManAddProto( Abc_Obj_t * pObj, Abc_Obj_t * pProto ) -{ - Abc_HObj_t * pHObj; - if ( s_pHMan == NULL ) - return; - // ignore polarity for now - pObj = Abc_ObjRegular(pObj); - pProto = Abc_ObjRegular(pProto); - // set the prototype - assert( pObj->pNtk != pProto->pNtk ); - if ( pObj->pNtk->Id == 0 ) - return; - pHObj = Abc_ObjHObj(pObj); - pHObj->Proto.NtkId = pProto->pNtk->Id; - pHObj->Proto.ObjId = pProto->Id; -} - -/**Function************************************************************* - - Synopsis [Called when an equivalent node is created.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_HManMapAddEqu( Abc_Obj_t * pObj, Abc_Obj_t * pEqu ) -{ -/* - Abc_HObj_t * pHObj; - if ( s_pHMan == NULL ) - return; - // ignore polarity for now - pObj = Abc_ObjRegular(pObj); - pEqu = Abc_ObjRegular(pEqu); - // set the equivalent node - assert( pObj->pNtk == pEqu->pNtk ); - pHObj = Abc_ObjHObj(pObj); - Abc_ObjHObj(pObj)->Equ.NtkId = pEqu->pNtk->Id; - Abc_ObjHObj(pObj)->Equ.ObjId = pEqu->Id; -*/ -} - - - -/**Function************************************************************* - - Synopsis [Starts the verification procedure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_HManPopulate( Abc_Ntk_t * pNtk ) -{ - Abc_Obj_t * pObj; - int i; - if ( !Abc_NtkIsStrash(pNtk) ) - return 0; - // allocate the network ID - pNtk->Id = Abc_HManGetNewNtkId(); - assert( pNtk->Id == 1 ); - // create the objects - Abc_NtkForEachObj( pNtk, pObj, i ) - { - Abc_HManAddObj( pObj ); - if ( Abc_ObjFaninNum(pObj) > 0 ) - Abc_HManAddFanin( pObj, Abc_ObjChild0(pObj) ); - if ( Abc_ObjFaninNum(pObj) > 1 ) - Abc_HManAddFanin( pObj, Abc_ObjChild1(pObj) ); - } - return 1; -} - -/**Function************************************************************* - - Synopsis [The main verification procedure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_HManVerify( int NtkIdOld, int NtkIdNew ) -{ - int i; - // prove the equality pairwise - for ( i = NtkIdOld; i < NtkIdNew; i++ ) - { - if ( Vec_IntEntry(s_pHMan->vProof, i) ) - continue; - if ( !Abc_HManVerifyPair( i, i+1 ) ) - return 0; - Vec_IntWriteEntry( s_pHMan->vProof, i, 1 ); - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Verifies two networks.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_HManVerifyPair( int NtkIdOld, int NtkIdNew ) -{ - Vec_Ptr_t * vNtkNew, * vNtkOld, * vPosNew; - Abc_HObj_t * pHObj; - int i; - // get hold of the network nodes - vNtkNew = Vec_VecEntry( s_pHMan->vNtks, NtkIdNew ); - vNtkOld = Vec_VecEntry( s_pHMan->vNtks, NtkIdOld ); - Vec_PtrForEachEntry( vNtkNew, pHObj, i ) - pHObj->fVisited = 0; - Vec_PtrForEachEntry( vNtkOld, pHObj, i ) - pHObj->fVisited = 0; - // collect new POs - vPosNew = Vec_PtrAlloc( 100 ); - Vec_PtrForEachEntry( vNtkNew, pHObj, i ) - if ( pHObj->fPo ) - Vec_PtrPush( vPosNew, pHObj ); - // prove them recursively (assuming PO ordering is the same) - Vec_PtrForEachEntry( vPosNew, pHObj, i ) - { - if ( Abc_HObjProto(pHObj) == NULL ) - { - printf( "History: PO %d has no prototype\n", i ); - return 0; - } - if ( !Abc_HManVerifyNodes_rec( Abc_HObjProto(pHObj), pHObj ) ) - { - printf( "History: Verification failed for outputs of PO pair number %d\n", i ); - return 0; - } - } - printf( "History: Verification succeeded.\n" ); - return 1; -} - -/**Function************************************************************* - - Synopsis [Recursively verifies two nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_HManVerifyNodes_rec( Abc_HObj_t * pHOld, Abc_HObj_t * pHNew ) -{ - Vec_Ptr_t * vLeaves; - Abc_HObj_t * pHObj, * pHPro0, * pHPro1; - int i, fPhase; - - assert( Abc_HObjProto(pHNew) == pHOld ); - if ( pHNew->fProof ) - return 1; - pHNew->fProof = 1; - // consider simple cases - if ( pHNew->fPi || pHNew->fConst ) - return 1; - if ( pHNew->fPo ) - { - if ( !Abc_HManVerifyNodes_rec( Abc_HObjFanin0(pHOld), Abc_HObjFanin0(pHNew) ) ) - return 0; - if ( (Abc_HObjFaninC0(pHOld) ^ Abc_HObjFaninC0(pHNew)) != (int)pHNew->fPhase ) - { - printf( "History: Phase of PO nodes does not agree.\n" ); - return 0; - } - return 1; - } - // the elementary node - pHPro0 = Abc_HObjProto( Abc_HObjFanin0(pHNew) ); - pHPro1 = Abc_HObjProto( Abc_HObjFanin1(pHNew) ); - if ( pHPro0 && pHPro1 ) - { - if ( !Abc_HManVerifyNodes_rec( pHPro0, Abc_HObjFanin0(pHNew) ) ) - return 0; - if ( !Abc_HManVerifyNodes_rec( pHPro1, Abc_HObjFanin1(pHNew) ) ) - return 0; - if ( Abc_HObjFanin0(pHOld) != pHPro0 || Abc_HObjFanin1(pHOld) != pHPro1 ) - { - printf( "History: Internal node does not match.\n" ); - return 0; - } - if ( Abc_HObjFaninC0(pHOld) != Abc_HObjFaninC0(pHNew) || - Abc_HObjFaninC1(pHOld) != Abc_HObjFaninC1(pHNew) ) - { - printf( "History: Phase of internal node does not match.\n" ); - return 0; - } - return 1; - } - // collect the leaves - vLeaves = Abc_HManCollectLeaves( pHNew ); - if ( Vec_PtrSize(vLeaves) > 16 ) - { - printf( "History: The bound on the number of inputs is exceeded.\n" ); - return 0; - } - s_pHMan->nWordsCur = ((1 << Vec_PtrSize(vLeaves)) <= 32)? 1 : ((1 << Vec_PtrSize(vLeaves)) / 32); - // prove recursively - Vec_PtrForEachEntry( vLeaves, pHObj, i ) - if ( !Abc_HManVerifyNodes_rec( Abc_HObjProto(pHObj), pHObj ) ) - { - Vec_PtrFree( vLeaves ); - return 0; - } - // get the first node - Abc_HManCollectCone( pHNew, vLeaves, s_pHMan->vCone1 ); - if ( Vec_PtrSize(s_pHMan->vCone1) > ABC_SIM_OBJS - ABC_SIM_VARS - 1 ) - { - printf( "History: The bound on the number of cone nodes is exceeded.\n" ); - return 0; - } - // get the second cone - Vec_PtrForEachEntry( vLeaves, pHObj, i ) - Vec_PtrWriteEntry( vLeaves, i, Abc_HObjProto(pHObj) ); - Abc_HManCollectCone( pHOld, vLeaves, s_pHMan->vCone0 ); - if ( Vec_PtrSize(s_pHMan->vCone0) > ABC_SIM_OBJS - ABC_SIM_VARS - 1 ) - { - printf( "History: The bound on the number of cone nodes is exceeded.\n" ); - return 0; - } - // compare the truth tables - if ( !Abc_HManSimulate( s_pHMan->vCone0, s_pHMan->vCone1, Vec_PtrSize(vLeaves), &fPhase ) ) - { - Vec_PtrFree( vLeaves ); - printf( "History: Verification failed at an internal node.\n" ); - return 0; - } - printf( "Succeeded.\n" ); - pHNew->fPhase = fPhase; - Vec_PtrFree( vLeaves ); - return 1; -} - -/**Function************************************************************* - - Synopsis [Finds the leaves of the TFI cone.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_HManCollectLeaves_rec( Abc_HObj_t * pHNew, Vec_Ptr_t * vLeaves ) -{ - Abc_HObj_t * pHPro; - if ( pHPro = Abc_HObjProto( pHNew ) ) - { - Vec_PtrPushUnique( vLeaves, pHNew ); - return; - } - assert( !pHNew->fPi && !pHNew->fPo && !pHNew->fConst ); - Abc_HManCollectLeaves_rec( Abc_HObjFanin0(pHNew), vLeaves ); - Abc_HManCollectLeaves_rec( Abc_HObjFanin1(pHNew), vLeaves ); -} - -/**Function************************************************************* - - Synopsis [Finds the leaves of the TFI cone.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Abc_HManCollectLeaves( Abc_HObj_t * pHNew ) -{ - Vec_Ptr_t * vLeaves; - vLeaves = Vec_PtrAlloc( 100 ); - Abc_HManCollectLeaves_rec( Abc_HObjFanin0(pHNew), vLeaves ); - Abc_HManCollectLeaves_rec( Abc_HObjFanin1(pHNew), vLeaves ); - return vLeaves; -} - - -/**Function************************************************************* - - Synopsis [Collects the TFI cone.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_HManCollectCone_rec( Abc_HObj_t * pHObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone ) -{ - if ( pHObj->fVisited ) - return; - pHObj->fVisited = 1; - assert( !pHObj->fPi && !pHObj->fPo && !pHObj->fConst ); - Abc_HManCollectCone_rec( Abc_HObjFanin0(pHObj), vLeaves, vCone ); - Abc_HManCollectCone_rec( Abc_HObjFanin1(pHObj), vLeaves, vCone ); - pHObj->Num = Vec_PtrSize(vCone); - Vec_PtrPush( vCone, pHObj ); -} - -/**Function************************************************************* - - Synopsis [Collects the TFI cone.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Abc_HManCollectCone( Abc_HObj_t * pHRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone ) -{ - Abc_HObj_t * pHObj; - int i; - Vec_PtrClear( vCone ); - Vec_PtrForEachEntry( vLeaves, pHObj, i ) - { - pHObj->fVisited = 1; - pHObj->Num = Vec_PtrSize(vCone); - Vec_PtrPush( vCone, pHObj ); - } - Abc_HManCollectCone_rec( Abc_HObjFanin0(pHRoot), vLeaves, vCone ); - Abc_HManCollectCone_rec( Abc_HObjFanin1(pHRoot), vLeaves, vCone ); - return vCone; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_HManSimulateOne( Vec_Ptr_t * vCone, int nLeaves, int fUsePhase ) -{ - Abc_HObj_t * pHObj, * pHFan0, * pHFan1; - unsigned * puData0, * puData1, * puData; - int k, i, fComp0, fComp1; - // set the leaves - Vec_PtrForEachEntryStart( vCone, pHObj, i, nLeaves ) - { - pHFan0 = Abc_HObjFanin0(pHObj); - pHFan1 = Abc_HObjFanin1(pHObj); - // consider the case of interver or buffer - if ( pHFan1 == NULL ) - { - puData = Vec_PtrEntry(s_pHMan->vSims, ABC_SIM_VARS+i-nLeaves); - puData0 = ((int)pHFan0->Num < nLeaves)? Vec_PtrEntry(s_pHMan->vSims, pHFan0->Num) : - Vec_PtrEntry(s_pHMan->vSims, ABC_SIM_VARS+pHFan0->Num-nLeaves); - fComp0 = Abc_HObjFaninC0(pHObj) ^ (fUsePhase && (int)pHFan0->Num < nLeaves && pHFan0->fPhase); - if ( fComp0 ) - for ( k = 0; k < s_pHMan->nWordsCur; k++ ) - puData[k] = ~puData0[k]; - else - for ( k = 0; k < s_pHMan->nWordsCur; k++ ) - puData[k] = puData0[k]; - continue; - } - // get the pointers to simulation data - puData = Vec_PtrEntry(s_pHMan->vSims, ABC_SIM_VARS+i-nLeaves); - puData0 = ((int)pHFan0->Num < nLeaves)? Vec_PtrEntry(s_pHMan->vSims, pHFan0->Num) : - Vec_PtrEntry(s_pHMan->vSims, ABC_SIM_VARS+pHFan0->Num-nLeaves); - puData1 = ((int)pHFan1->Num < nLeaves)? Vec_PtrEntry(s_pHMan->vSims, pHFan1->Num) : - Vec_PtrEntry(s_pHMan->vSims, ABC_SIM_VARS+pHFan1->Num-nLeaves); - // here are the phases - fComp0 = Abc_HObjFaninC0(pHObj) ^ (fUsePhase && (int)pHFan0->Num < nLeaves && pHFan0->fPhase); - fComp1 = Abc_HObjFaninC1(pHObj) ^ (fUsePhase && (int)pHFan1->Num < nLeaves && pHFan1->fPhase); - // simulate - if ( fComp0 && fComp1 ) - for ( k = 0; k < s_pHMan->nWordsCur; k++ ) - puData[k] = ~puData0[k] & ~puData1[k]; - else if ( fComp0 ) - for ( k = 0; k < s_pHMan->nWordsCur; k++ ) - puData[k] = ~puData0[k] & puData1[k]; - else if ( fComp1 ) - for ( k = 0; k < s_pHMan->nWordsCur; k++ ) - puData[k] = puData0[k] & ~puData1[k]; - else - for ( k = 0; k < s_pHMan->nWordsCur; k++ ) - puData[k] = puData0[k] & puData1[k]; - } -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_HManSimulate( Vec_Ptr_t * vCone0, Vec_Ptr_t * vCone1, int nLeaves, int * pPhase ) -{ - unsigned * pDataTop, * pDataLast; - int w; - // simulate the first one - Abc_HManSimulateOne( vCone0, nLeaves, 0 ); - // save the last simulation value - pDataTop = Vec_PtrEntry( s_pHMan->vSims, ((Abc_HObj_t *)Vec_PtrEntryLast(vCone0))->Num ); - pDataLast = Vec_PtrEntry( s_pHMan->vSims, Vec_PtrSize(s_pHMan->vSims)-1 ); - for ( w = 0; w < s_pHMan->nWordsCur; w++ ) - pDataLast[w] = pDataTop[w]; - // simulate the other one - Abc_HManSimulateOne( vCone1, nLeaves, 1 ); - // complement the output if needed - pDataTop = Vec_PtrEntry( s_pHMan->vSims, ((Abc_HObj_t *)Vec_PtrEntryLast(vCone1))->Num ); - // mask unused bits - if ( nLeaves < 5 ) - { - pDataTop[0] &= ((~((unsigned)0)) >> (32-(1<<nLeaves))); - pDataLast[0] &= ((~((unsigned)0)) >> (32-(1<<nLeaves))); - } - if ( *pPhase = ((pDataTop[0] & 1) != (pDataLast[0] & 1)) ) - for ( w = 0; w < s_pHMan->nWordsCur; w++ ) - pDataTop[w] = ~pDataTop[w]; - // compare - for ( w = 0; w < s_pHMan->nWordsCur; w++ ) - if ( pDataLast[w] != pDataTop[w] ) - return 0; - return 1; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c index f1ec3847..b5306bea 100644 --- a/src/base/abci/abcUnreach.c +++ b/src/base/abci/abcUnreach.c @@ -333,7 +333,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn // transform the network to the SOP representation if ( !Abc_NtkBddToSop( pNtkNew, 0 ) ) { - printf( "Converting to SOPs has failed.\n" ); + printf( "Abc_NtkConstructExdc(): Converting to SOPs has failed.\n" ); return NULL; } return pNtkNew; diff --git a/src/base/abci/abcVanEijk.c b/src/base/abci/abcVanEijk.c index 81423c30..58d9f64e 100644 --- a/src/base/abci/abcVanEijk.c +++ b/src/base/abci/abcVanEijk.c @@ -526,7 +526,7 @@ Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nF pNtkFrames->pName = Extra_UtilStrsav(Buffer); } // map the constant nodes - Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkFrames); + Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkFrames); // create new latches and remember them in the new latches Abc_NtkForEachLatch( pNtk, pLatch, i ) Abc_NtkDupObj( pNtkFrames, pLatch ); @@ -589,7 +589,7 @@ void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFram // remember the CI mapping if ( vCorresp ) { - pNode = Abc_NtkConst1(pNtk); + pNode = Abc_AigConst1(pNtk); Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) ); Abc_NtkForEachCi( pNtk, pNode, i ) Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) ); @@ -667,7 +667,7 @@ Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ) // clean the copy fields in the old network Abc_NtkCleanCopy( pMulti ); // map the constant nodes - Abc_NtkConst1(pMulti)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan); + Abc_AigConst1(pMulti)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan); if ( fInit ) { // map the PI nodes @@ -724,14 +724,14 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ) pNtkNew->pSpec = NULL; // map the constant nodes - Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew); + Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); // for each CI, create PI Abc_NtkForEachCi( pNtk, pObj, i ) Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj) ); // cannot add latches here because pLatch->pCopy pointers are used // create the cones for each pair of nodes in an equivalence class - pTotal = Abc_ObjNot( Abc_NtkConst1(pNtkNew) ); + pTotal = Abc_ObjNot( Abc_AigConst1(pNtkNew) ); Vec_PtrForEachEntry( vClasses, pClass, i ) { assert( pClass->pNext ); @@ -783,7 +783,7 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ) Abc_NtkDeleteObj( pObjNew ); // make the old network point to the new things - Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew); + Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); Abc_NtkForEachCi( pNtk, pObj, i ) pObj->pCopy = Abc_NtkPi( pNtkNew, i ); */ diff --git a/src/base/abci/abcVanImp.c b/src/base/abci/abcVanImp.c index 77de5185..29b5d3a6 100644 --- a/src/base/abci/abcVanImp.c +++ b/src/base/abci/abcVanImp.c @@ -487,7 +487,7 @@ printf( "PO = %d\n", pNode1->Id ); // go through the pairs of signals in the frames pProgress = Extra_ProgressBarStart( stdout, p->nIdMax ); - pConst1 = Abc_NtkConst1( p->pNtkSingle ); + pConst1 = Abc_AigConst1(p->pNtkSingle); p->vImps = Vec_IntAlloc( 100 ); p->vZeros = Vec_PtrAlloc( 100 ); Abc_NtkForEachObj( p->pNtkSingle, pNode1, i ) @@ -882,14 +882,14 @@ Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_I pNtkNew->pSpec = NULL; // map the constant nodes - Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew); + Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); // for each CI, create PI Abc_NtkForEachCi( pNtk, pObj, i ) Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj) ); // cannot add latches here because pLatch->pCopy pointers are used // build logic cone for zero nodes - pTotal = Abc_ObjNot( Abc_NtkConst1(pNtkNew) ); + pTotal = Abc_ObjNot( Abc_AigConst1(pNtkNew) ); Vec_PtrForEachEntry( vZeros, pNode, i ) { // build the logic cone for the node @@ -961,7 +961,7 @@ Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_I Abc_NtkDeleteObj( pObjNew ); // make the old network point to the new things - Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew); + Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); Abc_NtkForEachCi( pNtk, pObj, i ) pObj->pCopy = Abc_NtkPi( pNtkNew, i ); */ diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index d9478b04..c6782b07 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -422,9 +422,9 @@ int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel ) vNodes = Abc_NtkDfs( pNtk, 1 ); Vec_PtrForEachEntry( vNodes, pNode, i ) { - if ( Abc_NodeIsConst(pNode) ) - pNode->pCopy = NULL; - else +// if ( Abc_NodeIsConst(pNode) ) +// pNode->pCopy = NULL; +// else { Value0 = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode); Value1 = ((int)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode); diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 2e338e48..54c6f05c 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -31,7 +31,6 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcSweep.c \ src/base/abci/abcSymm.c \ src/base/abci/abcTiming.c \ - src/base/abci/abcTrace.c \ src/base/abci/abcUnate.c \ src/base/abci/abcUnreach.c \ src/base/abci/abcVanEijk.c \ |