From ccd1b57264d3bf1514410747cdcf6e4731ac7f2a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 10 Apr 2009 08:01:00 -0700 Subject: Version abc90410 --- src/base/abc/abc.h | 2 +- src/base/abc/abcNtk.c | 2 +- src/base/abc/abcRefs.c | 20 ++++++------- src/base/abci/abc.c | 75 ++++++++++++++++++++++++++++++++++------------ src/base/abci/abcCut.c | 4 +-- src/base/abci/abcDar.c | 10 ++++++- src/base/abci/abcPrint.c | 4 +-- src/base/abci/abcResub.c | 4 +-- src/base/io/ioWriteAiger.c | 2 +- 9 files changed, 84 insertions(+), 39 deletions(-) (limited to 'src/base') diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 2869352c..73a487e9 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -779,7 +779,7 @@ extern ABC_DLL int Abc_NodeMffcSizeSupp( Abc_Obj_t * pNode ); extern ABC_DLL int Abc_NodeMffcSizeStop( Abc_Obj_t * pNode ); extern ABC_DLL int Abc_NodeMffcLabelAig( Abc_Obj_t * pNode ); extern ABC_DLL int Abc_NodeMffcLabel( Abc_Obj_t * pNode ); -extern ABC_DLL void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp ); +extern ABC_DLL void Abc_NodeMffcConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp ); extern ABC_DLL int Abc_NodeDeref_rec( Abc_Obj_t * pNode ); extern ABC_DLL int Abc_NodeRef_rec( Abc_Obj_t * pNode ); /*=== abcRefactor.c ==========================================================*/ diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index d6ab7ea1..3e233d90 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -741,7 +741,7 @@ Abc_Ntk_t * Abc_NtkCreateMffc( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNode vCone = Vec_PtrAlloc( 100 ); vSupp = Vec_PtrAlloc( 100 ); Abc_NodeDeref_rec( pNode ); - Abc_NodeMffsConeSupp( pNode, vCone, vSupp ); + Abc_NodeMffcConeSupp( pNode, vCone, vSupp ); Abc_NodeRef_rec( pNode ); // create the PIs Vec_PtrForEachEntry( vSupp, pObj, i ) diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c index fadb492a..ec89eaed 100644 --- a/src/base/abc/abcRefs.c +++ b/src/base/abc/abcRefs.c @@ -260,7 +260,7 @@ int Abc_NodeRef_rec( Abc_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -void Abc_NodeMffsConeSupp_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp, int fTopmost ) +void Abc_NodeMffcConeSupp_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp, int fTopmost ) { Abc_Obj_t * pFanin; int i; @@ -276,7 +276,7 @@ void Abc_NodeMffsConeSupp_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * } // recur on the children Abc_ObjForEachFanin( pNode, pFanin, i ) - Abc_NodeMffsConeSupp_rec( pFanin, vCone, vSupp, 0 ); + Abc_NodeMffcConeSupp_rec( pFanin, vCone, vSupp, 0 ); // collect the internal node if ( vCone ) Vec_PtrPush( vCone, pNode ); // printf( "%d ", pNode->Id ); @@ -293,14 +293,14 @@ void Abc_NodeMffsConeSupp_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * SeeAlso [] ***********************************************************************/ -void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp ) +void Abc_NodeMffcConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp ) { assert( Abc_ObjIsNode(pNode) ); assert( !Abc_ObjIsComplement(pNode) ); if ( vCone ) Vec_PtrClear( vCone ); if ( vSupp ) Vec_PtrClear( vSupp ); Abc_NtkIncrementTravId( pNode->pNtk ); - Abc_NodeMffsConeSupp_rec( pNode, vCone, vSupp, 1 ); + Abc_NodeMffcConeSupp_rec( pNode, vCone, vSupp, 1 ); // printf( "\n" ); } @@ -315,7 +315,7 @@ void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSu SeeAlso [] ***********************************************************************/ -void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode ) +void Abc_NodeMffcConeSuppPrint( Abc_Obj_t * pNode ) { Vec_Ptr_t * vCone, * vSupp; Abc_Obj_t * pObj; @@ -323,7 +323,7 @@ void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode ) vCone = Vec_PtrAlloc( 100 ); vSupp = Vec_PtrAlloc( 100 ); Abc_NodeDeref_rec( pNode ); - Abc_NodeMffsConeSupp( pNode, vCone, vSupp ); + Abc_NodeMffcConeSupp( pNode, vCone, vSupp ); Abc_NodeRef_rec( pNode ); printf( "Node = %6s : Supp = %3d Cone = %3d (", Abc_ObjName(pNode), Vec_PtrSize(vSupp), Vec_PtrSize(vCone) ); @@ -345,7 +345,7 @@ void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -int Abc_NodeMffsInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vInside ) +int Abc_NodeMffcInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vInside ) { Abc_Obj_t * pObj; int i, Count1, Count2; @@ -355,7 +355,7 @@ int Abc_NodeMffsInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vIns // dereference the node Count1 = Abc_NodeDeref_rec( pNode ); // collect the nodes inside the MFFC - Abc_NodeMffsConeSupp( pNode, vInside, NULL ); + Abc_NodeMffcConeSupp( pNode, vInside, NULL ); // reference it back Count2 = Abc_NodeRef_rec( pNode ); assert( Count1 == Count2 ); @@ -376,7 +376,7 @@ int Abc_NodeMffsInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vIns SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Abc_NodeMffsInsideCollect( Abc_Obj_t * pNode ) +Vec_Ptr_t * Abc_NodeMffcInsideCollect( Abc_Obj_t * pNode ) { Vec_Ptr_t * vInside; int Count1, Count2; @@ -384,7 +384,7 @@ Vec_Ptr_t * Abc_NodeMffsInsideCollect( Abc_Obj_t * pNode ) Count1 = Abc_NodeDeref_rec( pNode ); // collect the nodes inside the MFFC vInside = Vec_PtrAlloc( 10 ); - Abc_NodeMffsConeSupp( pNode, vInside, NULL ); + Abc_NodeMffcConeSupp( pNode, vInside, NULL ); // reference it back Count2 = Abc_NodeRef_rec( pNode ); assert( Count1 == Count2 ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c48b7e95..8ac8b241 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -9515,7 +9515,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Dch_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptgcvh" ) ) != EOF ) { switch ( c ) { @@ -9561,6 +9561,12 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv ) case 't': pPars->fSimulateTfo ^= 1; break; + case 'g': + pPars->fUseGia ^= 1; + break; + case 'c': + pPars->fUseCSat ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -9591,7 +9597,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: dch [-WCS num] [-sptvh]\n" ); + fprintf( pErr, "usage: dch [-WCS num] [-sptgcvh]\n" ); fprintf( pErr, "\t computes structural choices using a new approach\n" ); fprintf( pErr, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords ); fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); @@ -9599,6 +9605,8 @@ usage: fprintf( pErr, "\t-s : toggle synthesizing three snapshots [default = %s]\n", pPars->fSynthesis? "yes": "no" ); fprintf( pErr, "\t-p : toggle power-aware rewriting [default = %s]\n", pPars->fPower? "yes": "no" ); fprintf( pErr, "\t-t : toggle simulation of the TFO classes [default = %s]\n", pPars->fSimulateTfo? "yes": "no" ); + fprintf( pErr, "\t-g : toggle using GIA to prove equivalences [default = %s]\n", pPars->fUseGia? "yes": "no" ); + fprintf( pErr, "\t-c : toggle using circuit-based SAT vs. MiniSat [default = %s]\n", pPars->fUseCSat? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -21820,6 +21828,7 @@ usage: int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); + extern Aig_Man_t * Abc_NtkToDarChoices( Abc_Ntk_t * pNtk ); Gia_Man_t * pAig; Aig_Man_t * pMan; int c, fVerbose = 0; @@ -21845,12 +21854,15 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv ) printf( "The current network should be strashed.\n" ); return 1; } +// if ( Abc_NtkGetChoiceNum(pAbc->pNtkCur) ) +// { +// printf( "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pAbc->pNtkCur) ); +// Abc_AigCleanup(pAbc->pNtkCur->pManFunc); +// } if ( Abc_NtkGetChoiceNum(pAbc->pNtkCur) ) - { - printf( "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pAbc->pNtkCur) ); - Abc_AigCleanup(pAbc->pNtkCur->pManFunc); - } - pMan = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 ); + pMan = Abc_NtkToDarChoices( pAbc->pNtkCur ); + else + pMan = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 ); pAig = Gia_ManFromAig( pMan ); Aig_ManStop( pMan ); if ( pAig == NULL ) @@ -21886,6 +21898,7 @@ usage: int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ); + extern Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ); Aig_Man_t * pMan; FILE * pOut, * pErr; Abc_Ntk_t * pNtk; @@ -21917,9 +21930,27 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } - pMan = Gia_ManToAig( pAbc->pAig ); - pNtk = Abc_NtkFromAigPhase( pMan ); - Aig_ManStop( pMan ); + if ( Gia_ManHasDandling(pAbc->pAig) == 0 ) + { + pMan = Gia_ManToAig( pAbc->pAig, 0 ); + pNtk = Abc_NtkFromAigPhase( pMan ); + Aig_ManStop( pMan ); + } + else + { + Abc_Ntk_t * pNtkNoCh; +// printf( "Transforming AIG with %d choice nodes.\n", Gia_ManEquivCountClasses(pAbc->pAig) ); + // create network without choices + pMan = Gia_ManToAig( pAbc->pAig, 0 ); + pNtkNoCh = Abc_NtkFromAigPhase( pMan ); + pNtkNoCh->pName = Extra_UtilStrsav(pMan->pName); + Aig_ManStop( pMan ); + // derive network with choices + pMan = Gia_ManToAig( pAbc->pAig, 1 ); + pNtk = Abc_NtkFromDarChoices( pNtkNoCh, pMan ); + Abc_NtkDelete( pNtkNoCh ); + Aig_ManStop( pMan ); + } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtk ); return 0; @@ -22204,7 +22235,7 @@ int Abc_CommandAbc9Show( Abc_Frame_t * pAbc, int argc, char ** argv ) printf( "Abc_CommandAbc9Show(): There is no AIG.\n" ); return 1; } - pMan = Gia_ManToAig( pAbc->pAig ); + pMan = Gia_ManToAig( pAbc->pAig, 0 ); Aig_ManShow( pMan, 0, NULL ); Aig_ManStop( pMan ); return 0; @@ -23400,7 +23431,7 @@ usage: fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames ); fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" ); - fprintf( stdout, "\t-r : toggle using implication rings for equivalence classes [default = %s]\n", pPars->fUseRings? "yes": "no" ); + fprintf( stdout, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" ); fprintf( stdout, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" ); fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); @@ -23425,7 +23456,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Cec_ManCorSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FCfrcvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FCfrecvh" ) ) != EOF ) { switch ( c ) { @@ -23457,6 +23488,9 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'r': pPars->fUseRings ^= 1; break; + case 'e': + pPars->fMakeChoices ^= 1; + break; case 'c': pPars->fUseCSat ^= 1; break; @@ -23483,12 +23517,13 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( stdout, "usage: &scorr [-FC num] [-frcvh]\n" ); + fprintf( stdout, "usage: &scorr [-FC num] [-frecvh]\n" ); fprintf( stdout, "\t performs signal correpondence computation\n" ); fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames ); fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" ); - fprintf( stdout, "\t-r : toggle using implication rings for equivalence classes [default = %s]\n", pPars->fUseRings? "yes": "no" ); + fprintf( stdout, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" ); + fprintf( stdout, "\t-e : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" ); fprintf( stdout, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" ); fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); @@ -23513,7 +23548,7 @@ int Abc_CommandAbc9Choice( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Cec_ManChcSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Cvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Ccvh" ) ) != EOF ) { switch ( c ) { @@ -23528,6 +23563,9 @@ int Abc_CommandAbc9Choice( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nBTLimit < 0 ) goto usage; break; + case 'c': + pPars->fUseCSat ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -23540,8 +23578,6 @@ int Abc_CommandAbc9Choice( Abc_Frame_t * pAbc, int argc, char ** argv ) printf( "Abc_CommandAbc9Choice(): There is no AIG.\n" ); return 1; } - printf("The command is not yet ready.\n" ); - return 0; pAbc->pAig = Cec_ManChoiceComputation( pTemp = pAbc->pAig, pPars ); if ( pAbc->pAig == NULL ) { @@ -23553,9 +23589,10 @@ int Abc_CommandAbc9Choice( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( stdout, "usage: &choice [-C num] [-vh]\n" ); + fprintf( stdout, "usage: &choice [-C num] [-cvh]\n" ); fprintf( stdout, "\t performs computation of structural choices\n" ); fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); + fprintf( stdout, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" ); fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c index 48c2f8e0..cc97796f 100644 --- a/src/base/abci/abcCut.c +++ b/src/base/abci/abcCut.c @@ -586,7 +586,7 @@ Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk ) Abc_Obj_t * pObj;//, * pTemp; int i;//, k; int nNodesTotal = 0, nMffcsTotal = 0; - extern Vec_Ptr_t * Abc_NodeMffsInsideCollect( Abc_Obj_t * pNode ); + extern Vec_Ptr_t * Abc_NodeMffcInsideCollect( Abc_Obj_t * pNode ); vAttrs = Vec_IntStart( Abc_NtkObjNumMax(pNtk) + 1 ); // Abc_NtkForEachCi( pNtk, pObj, i ) @@ -615,7 +615,7 @@ Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk ) { if ( Vec_IntEntry( vAttrs, pObj->Id ) ) { - vNodes = Abc_NodeMffsInsideCollect( pObj ); + vNodes = Abc_NodeMffcInsideCollect( pObj ); Vec_PtrForEachEntry( vNodes, pTemp, k ) if ( pTemp != pObj ) Vec_IntWriteEntry( vAttrs, pTemp->Id, 0 ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 840068d6..a5973153 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -896,6 +896,7 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars ) { extern Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose ); + extern Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ); Vec_Ptr_t * vAigs; Aig_Man_t * pMan, * pTemp; @@ -911,6 +912,10 @@ clk = clock(); // vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fVerbose ); vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fPower, 0 ); Aig_ManStop( pMan ); + // swap around the first and the last + pTemp = Vec_PtrPop( vAigs ); + Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) ); + Vec_PtrWriteEntry( vAigs, 0, pTemp ); } else { @@ -918,7 +923,10 @@ clk = clock(); Vec_PtrPush( vAigs, pMan ); } pPars->timeSynth = clock() - clk; - pMan = Dch_ComputeChoices( vAigs, pPars ); + if ( pPars->fUseGia ) + pMan = Cec_ComputeChoices( vAigs, pPars ); + else + pMan = Dch_ComputeChoices( vAigs, pPars ); pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan ); // pNtkAig = Abc_NtkFromDar( pNtk, pMan ); Aig_ManStop( pMan ); diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index d47dfe1f..10e3ba2d 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -704,9 +704,9 @@ void Abc_NtkPrintMffc( FILE * pFile, Abc_Ntk_t * pNtk ) { Abc_Obj_t * pNode; int i; - extern void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode ); + extern void Abc_NodeMffcConeSuppPrint( Abc_Obj_t * pNode ); Abc_NtkForEachNode( pNtk, pNode, i ) - Abc_NodeMffsConeSuppPrint( pNode ); + Abc_NodeMffcConeSuppPrint( pNode ); } /**Function************************************************************* diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c index 861a5e66..655f158e 100644 --- a/src/base/abci/abcResub.c +++ b/src/base/abci/abcResub.c @@ -1624,7 +1624,7 @@ void Abc_ManResubCleanup( Abc_ManRes_t * p ) ***********************************************************************/ Dec_Graph_t * Abc_ManResubEval( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int nSteps, bool fUpdateLevel, bool fVerbose ) { - extern int Abc_NodeMffsInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vInside ); + extern int Abc_NodeMffcInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vInside ); Dec_Graph_t * pGraph; int Required; int clk; @@ -1639,7 +1639,7 @@ Dec_Graph_t * Abc_ManResubEval( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * // collect the MFFC clk = clock(); - p->nMffc = Abc_NodeMffsInside( pRoot, vLeaves, p->vTemp ); + p->nMffc = Abc_NodeMffcInside( pRoot, vLeaves, p->vTemp ); p->timeMffc += clock() - clk; assert( p->nMffc > 0 ); diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c index 8957743c..54db0641 100644 --- a/src/base/io/ioWriteAiger.c +++ b/src/base/io/ioWriteAiger.c @@ -728,7 +728,7 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f // write the comment fprintfBz2Aig( &b, "c" ); if ( pNtk->pName && strlen(pNtk->pName) > 0 ) - fprintfBz2Aig( &b, "n%s%c", pNtk->pName, '\0' ); + fprintfBz2Aig( &b, "\n%s%c", pNtk->pName, '\0' ); fprintfBz2Aig( &b, "\nThis file was written by ABC on %s\n", Extra_TimeStamp() ); fprintfBz2Aig( &b, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" ); -- cgit v1.2.3