diff options
| -rw-r--r-- | src/aig/gia/gia.h | 1 | ||||
| -rw-r--r-- | src/aig/gia/giaDup.c | 25 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 34 |
3 files changed, 50 insertions, 10 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 0ac1c740..1dda7dc0 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1099,6 +1099,7 @@ extern Gia_Man_t * Gia_ManDupAndOr( Gia_Man_t * p, int nOuts, int fUseOr extern Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fVerbose ); extern Gia_Man_t * Gia_ManMiter2( Gia_Man_t * p, char * pInit, int fVerbose ); extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p ); +extern Gia_Man_t * Gia_ManTransformToDual( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias ); extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes ); extern Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 37deb7fd..acd75e26 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -2311,6 +2311,31 @@ Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p ) Gia_ManStop( pTemp ); return pNew; } +Gia_Man_t * Gia_ManTransformToDual( Gia_Man_t * p ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManHashAlloc( pNew ); + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachPo( p, pObj, i ) + { + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManAppendCo( pNew, 0 ); + } + Gia_ManForEachRi( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} /**Function************************************************************* diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b6f8c5e4..eb19028e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -30220,11 +30220,10 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_Man_t * pSecond, * pMiter; char * FileName, * pTemp; char ** pArgvNew; - int c, nArgcNew, fMiter = 0; - int fDumpMiter = 0; + int c, nArgcNew, fMiter = 0, fDualOutput = 0, fDumpMiter = 0; Cec_ManCecSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CTmdvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CTmdavh" ) ) != EOF ) { switch ( c ) { @@ -30254,6 +30253,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) fMiter ^= 1; break; case 'd': + fDualOutput ^= 1; + break; + case 'a': fDumpMiter ^= 1; break; case 'v': @@ -30267,13 +30269,24 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( fMiter ) { - if ( Gia_ManPoNum(pAbc->pGia) & 1 ) + if ( fDualOutput ) { - Abc_Print( -1, "The dual-output miter should have an even number of outputs.\n" ); - return 1; + if ( Gia_ManPoNum(pAbc->pGia) & 1 ) + { + Abc_Print( -1, "The dual-output miter should have an even number of outputs.\n" ); + return 1; + } + Abc_Print( 1, "Assuming the current network is a double-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit ); + pAbc->Status = Cec_ManVerify( pAbc->pGia, pPars ); } - Abc_Print( 1, "Assuming the current network is a double-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit ); - pAbc->Status = Cec_ManVerify( pAbc->pGia, pPars ); + else + { + Gia_Man_t * pTemp; + Abc_Print( 1, "Assuming the current network is a single-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit ); + pTemp = Gia_ManTransformToDual( pAbc->pGia ); + pAbc->Status = Cec_ManVerify( pTemp, pPars ); + Gia_ManStop( pTemp ); + } Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb ); return 0; } @@ -30327,12 +30340,13 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &cec [-CT num] [-mdvh]\n" ); + Abc_Print( -2, "usage: &cec [-CT num] [-mdavh]\n" ); Abc_Print( -2, "\t new combinational equivalence checker\n" ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit ); Abc_Print( -2, "\t-m : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits"); - Abc_Print( -2, "\t-d : toggle dumping dual-output miter [default = %s]\n", fDumpMiter? "yes":"no"); + Abc_Print( -2, "\t-d : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no"); + Abc_Print( -2, "\t-a : toggle writing dual-output miter [default = %s]\n", fDumpMiter? "yes":"no"); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no"); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; |