From 67357cda2f389f39ed45e81e7579d549b7280174 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 19 May 2013 10:58:36 -0700 Subject: Added new switched to command &frames. --- src/aig/gia/gia.h | 14 ++++++++++++++ src/aig/gia/giaFrames.c | 37 +++++++++++++++++++++++++++++++------ src/base/abci/abc.c | 22 +++++++++++++++------- 3 files changed, 60 insertions(+), 13 deletions(-) diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index c184950e..12d255a4 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -205,6 +205,8 @@ struct Gia_ParFra_t_ int nFrames; // the number of frames to unroll int fInit; // initialize the timeframes int fSaveLastLit; // adds POs for outputs of each frame + int fDisableSt; // disables strashing + int fOrPos; // ORs respective POs in each timeframe int fVerbose; // enables verbose output }; @@ -513,6 +515,18 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 ) } return Gia_ObjId( p, pObj ) << 1; } +static inline int Gia_ManAppendAnd2( Gia_Man_t * p, int iLit0, int iLit1 ) +{ + if ( iLit0 < 2 ) + return iLit0 ? iLit1 : 0; + if ( iLit1 < 2 ) + return iLit1 ? iLit0 : 0; + if ( iLit0 == iLit1 ) + return iLit1; + if ( iLit0 == Abc_LitNot(iLit1) ) + return 0; + return Gia_ManAppendAnd( p, iLit0, iLit1 ); +} static inline int Gia_ManAppendXorReal( Gia_Man_t * p, int iLit0, int iLit1 ) { Gia_Obj_t * pObj = Gia_ManAppendObj( p ); diff --git a/src/aig/gia/giaFrames.c b/src/aig/gia/giaFrames.c index a62d17ca..b19e223b 100644 --- a/src/aig/gia/giaFrames.c +++ b/src/aig/gia/giaFrames.c @@ -864,15 +864,19 @@ Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars ) { Gia_Man_t * pFrames, * pTemp; Gia_Obj_t * pObj; + Vec_Int_t * vPoLits = NULL; int i, f; assert( Gia_ManRegNum(pAig) > 0 ); assert( pPars->nFrames > 0 ); if ( pPars->fInit ) return Gia_ManFramesInit( pAig, pPars ); + if ( pPars->fOrPos ) + vPoLits = Vec_IntStart( Gia_ManPoNum(pAig) ); pFrames = Gia_ManStart( pPars->nFrames * Gia_ManObjNum(pAig) ); pFrames->pName = Abc_UtilStrsav( pAig->pName ); pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec ); - Gia_ManHashAlloc( pFrames ); + if ( !pPars->fDisableSt ) + Gia_ManHashAlloc( pFrames ); Gia_ManConst0(pAig)->Value = 0; for ( f = 0; f < pPars->nFrames; f++ ) { @@ -888,12 +892,31 @@ Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars ) } Gia_ManForEachPi( pAig, pObj, i ) pObj->Value = Gia_ManAppendCi( pFrames ); - Gia_ManForEachAnd( pAig, pObj, i ) - pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Gia_ManForEachPo( pAig, pObj, i ) - pObj->Value = Gia_ManAppendCo( pFrames, Gia_ObjFanin0Copy(pObj) ); + if ( !pPars->fDisableSt ) + Gia_ManForEachAnd( pAig, pObj, i ) + pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else + Gia_ManForEachAnd( pAig, pObj, i ) + pObj->Value = Gia_ManAppendAnd2( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( vPoLits ) + { + if ( !pPars->fDisableSt ) + Gia_ManForEachPo( pAig, pObj, i ) + Vec_IntWriteEntry( vPoLits, i, Gia_ManHashOr(pFrames, Vec_IntEntry(vPoLits, i), Gia_ObjFanin0Copy(pObj)) ); + else + Gia_ManForEachPo( pAig, pObj, i ) + Vec_IntWriteEntry( vPoLits, i, Abc_LitNot(Gia_ManAppendAnd2(pFrames, Abc_LitNot(Vec_IntEntry(vPoLits, i)), Abc_LitNot(Gia_ObjFanin0Copy(pObj)))) ); + } + else + { + Gia_ManForEachPo( pAig, pObj, i ) + pObj->Value = Gia_ManAppendCo( pFrames, Gia_ObjFanin0Copy(pObj) ); + } if ( f == pPars->nFrames - 1 ) { + if ( vPoLits ) + Gia_ManForEachPo( pAig, pObj, i ) + pObj->Value = Gia_ManAppendCo( pFrames, Vec_IntEntry(vPoLits, i) ); Gia_ManForEachRi( pAig, pObj, i ) pObj->Value = Gia_ManAppendCo( pFrames, Gia_ObjFanin0Copy(pObj) ); } @@ -903,7 +926,9 @@ Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars ) pObj->Value = Gia_ObjFanin0Copy(pObj); } } - Gia_ManHashStop( pFrames ); + Vec_IntFreeP( &vPoLits ); + if ( !pPars->fDisableSt ) + Gia_ManHashStop( pFrames ); Gia_ManFraTransformCis( pAig, pFrames->vCis ); Gia_ManSetRegNum( pFrames, Gia_ManRegNum(pAig) ); if ( Gia_ManCombMarkUsed(pFrames) < Gia_ManAndNum(pFrames) ) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b93dd29b..5c8b4a7f 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -26219,11 +26219,11 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_ParFra_t Pars, * pPars = &Pars; int c; int nCofFanLit = 0; - int fNewAlgo = 1; + int fNewAlgo = 0; int fInitSpecial = 0; Gia_ManFraSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FLiasvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FLsoibavh" ) ) != EOF ) { switch ( c ) { @@ -26249,15 +26249,21 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nCofFanLit < 0 ) goto usage; break; + case 's': + pPars->fDisableSt ^= 1; + break; + case 'o': + pPars->fOrPos ^= 1; + break; case 'i': pPars->fInit ^= 1; break; + case 'b': + fInitSpecial ^= 1; + break; case 'a': fNewAlgo ^= 1; break; - case 's': - fInitSpecial ^= 1; - break; case 'v': pPars->fVerbose ^= 1; break; @@ -26289,13 +26295,15 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &frames [-FL ] [-iasvh]\n" ); + Abc_Print( -2, "usage: &frames [-FL ] [-soibavh]\n" ); Abc_Print( -2, "\t unrolls the design for several timeframes\n" ); Abc_Print( -2, "\t-F num : the number of frames to unroll [default = %d]\n", pPars->nFrames ); Abc_Print( -2, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit ); + Abc_Print( -2, "\t-s : toggle disabling structural hashing [default = %s]\n", pPars->fDisableSt? "yes": "no" ); + Abc_Print( -2, "\t-o : toggle ORing corresponding POs [default = %s]\n", pPars->fOrPos? "yes": "no" ); Abc_Print( -2, "\t-i : toggle initializing registers [default = %s]\n", pPars->fInit? "yes": "no" ); + Abc_Print( -2, "\t-b : toggle computing special AIG for BMC [default = %s]\n", fInitSpecial? "yes": "no" ); Abc_Print( -2, "\t-a : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes": "no" ); - Abc_Print( -2, "\t-s : toggle computing special AIG for BMC [default = %s]\n", fInitSpecial? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; -- cgit v1.2.3