diff options
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 75 | ||||
-rw-r--r-- | src/base/abci/abcCut.c | 4 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 10 | ||||
-rw-r--r-- | src/base/abci/abcPrint.c | 4 | ||||
-rw-r--r-- | src/base/abci/abcResub.c | 4 |
5 files changed, 71 insertions, 26 deletions
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 ); |