diff options
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | abclib.dsp | 168 | ||||
| -rw-r--r-- | src/aig/gia/gia.h | 61 | ||||
| -rw-r--r-- | src/aig/gia/giaAbs.c | 746 | ||||
| -rw-r--r-- | src/aig/gia/giaAbs.h | 89 | ||||
| -rw-r--r-- | src/aig/gia/giaDup.c | 257 | ||||
| -rw-r--r-- | src/aig/gia/giaMan.c | 150 | ||||
| -rw-r--r-- | src/aig/gia/module.make | 9 | ||||
| -rw-r--r-- | src/aig/saig/module.make | 13 | ||||
| -rw-r--r-- | src/aig/saig/saig.h | 26 | ||||
| -rw-r--r-- | src/aig/saig/saigAbs.c | 133 | ||||
| -rw-r--r-- | src/aig/saig/saigAbsPba.c | 374 | ||||
| -rw-r--r-- | src/aig/saig/saigAbsVfa.c | 329 | ||||
| -rw-r--r-- | src/aig/saig/saigSimExt.c | 556 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 482 | ||||
| -rw-r--r-- | src/base/io/io.c | 1 | ||||
| -rw-r--r-- | src/opt/nwk/nwkAig.c | 2 | ||||
| -rw-r--r-- | src/proof/abs/abs.c | 52 | ||||
| -rw-r--r-- | src/proof/abs/abs.h | 131 | ||||
| -rw-r--r-- | src/proof/abs/absDup.c | 445 | ||||
| -rw-r--r-- | src/proof/abs/absGla.c (renamed from src/aig/gia/giaAbsGla2.c) | 22 | ||||
| -rw-r--r-- | src/proof/abs/absGlaOld.c (renamed from src/aig/gia/giaAbsGla.c) | 25 | ||||
| -rw-r--r-- | src/proof/abs/absIter.c (renamed from src/aig/gia/giaAbsIter.c) | 12 | ||||
| -rw-r--r-- | src/proof/abs/absOldCex.c (renamed from src/aig/saig/saigAbsCba.c) | 6 | ||||
| -rw-r--r-- | src/proof/abs/absOldRef.c (renamed from src/aig/saig/saigAbsStart.c) | 167 | ||||
| -rw-r--r-- | src/proof/abs/absOldSat.c | 986 | ||||
| -rw-r--r-- | src/proof/abs/absOldSim.c (renamed from src/aig/saig/saigSimExt2.c) | 224 | ||||
| -rw-r--r-- | src/proof/abs/absOut.c (renamed from src/aig/gia/giaAbsOut.c) | 17 | ||||
| -rw-r--r-- | src/proof/abs/absPth.c (renamed from src/aig/gia/giaAbsPth.c) | 6 | ||||
| -rw-r--r-- | src/proof/abs/absRef.c (renamed from src/aig/gia/giaAbsRef.c) | 10 | ||||
| -rw-r--r-- | src/proof/abs/absRef.h (renamed from src/aig/gia/giaAbsRef.h) | 10 | ||||
| -rw-r--r-- | src/proof/abs/absRef2.c (renamed from src/aig/gia/giaAbsRef2.c) | 10 | ||||
| -rw-r--r-- | src/proof/abs/absRef2.h (renamed from src/aig/gia/giaAbsRef2.h) | 10 | ||||
| -rw-r--r-- | src/proof/abs/absUtil.c | 257 | ||||
| -rw-r--r-- | src/proof/abs/absVta.c (renamed from src/aig/gia/giaAbsVta.c) | 50 | ||||
| -rw-r--r-- | src/proof/abs/module.make | 15 |
36 files changed, 2270 insertions, 3582 deletions
@@ -23,6 +23,7 @@ MODULES := \ src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \ src/proof/pdr src/proof/int src/proof/bbr src/proof/llb src/proof/live \ src/proof/cec src/proof/dch src/proof/fraig src/proof/fra src/proof/ssw \ + src/proof/abs \ src/aig/aig src/aig/saig src/aig/gia src/aig/ioa src/aig/ivy src/aig/hop \ src/python @@ -3223,26 +3223,6 @@ SOURCE=.\src\aig\saig\saig.h # End Source File # Begin Source File -SOURCE=.\src\aig\saig\saigAbs.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\saig\saigAbsCba.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\saig\saigAbsPba.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\saig\saigAbsStart.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\saig\saigAbsVfa.c -# End Source File -# Begin Source File - SOURCE=.\src\aig\saig\saigBmc.c # End Source File # Begin Source File @@ -3279,18 +3259,6 @@ SOURCE=.\src\aig\saig\saigDup.c # End Source File # Begin Source File -SOURCE=.\src\aig\saig\saigGlaCba.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\saig\saigGlaPba.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\saig\saigGlaPba2.c -# End Source File -# Begin Source File - SOURCE=.\src\aig\saig\saigHaig.c # End Source File # Begin Source File @@ -3327,10 +3295,6 @@ SOURCE=.\src\aig\saig\saigPhase.c # End Source File # Begin Source File -SOURCE=.\src\aig\saig\saigRefSat.c -# End Source File -# Begin Source File - SOURCE=.\src\aig\saig\saigRetFwd.c # End Source File # Begin Source File @@ -3347,14 +3311,6 @@ SOURCE=.\src\aig\saig\saigScl.c # End Source File # Begin Source File -SOURCE=.\src\aig\saig\saigSimExt.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\saig\saigSimExt2.c -# End Source File -# Begin Source File - SOURCE=.\src\aig\saig\saigSimFast.c # End Source File # Begin Source File @@ -3403,54 +3359,6 @@ SOURCE=.\src\aig\gia\gia.h # End Source File # Begin Source File -SOURCE=.\src\aig\gia\giaAbs.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\gia\giaAbs.h -# End Source File -# Begin Source File - -SOURCE=.\src\aig\gia\giaAbsGla.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\gia\giaAbsGla2.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\gia\giaAbsIter.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\gia\giaAbsOut.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\gia\giaAbsPth.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\gia\giaAbsRef.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\gia\giaAbsRef.h -# End Source File -# Begin Source File - -SOURCE=.\src\aig\gia\giaAbsRef2.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\gia\giaAbsRef2.h -# End Source File -# Begin Source File - -SOURCE=.\src\aig\gia\giaAbsVta.c -# End Source File -# Begin Source File - SOURCE=.\src\aig\gia\giaAig.c # End Source File # Begin Source File @@ -4398,6 +4306,82 @@ SOURCE=.\src\proof\ssw\sswSweep.c SOURCE=.\src\proof\ssw\sswUnique.c # End Source File # End Group +# Begin Group "abs" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\proof\abs\abs.c +# End Source File +# Begin Source File + +SOURCE=.\src\proof\abs\abs.h +# End Source File +# Begin Source File + +SOURCE=.\src\proof\abs\absDup.c +# End Source File +# Begin Source File + +SOURCE=.\src\proof\abs\absGla.c +# End Source File +# Begin Source File + +SOURCE=.\src\proof\abs\absGlaOld.c +# End Source File +# Begin Source File + +SOURCE=.\src\proof\abs\absIter.c +# End Source File +# Begin Source File + +SOURCE=.\src\proof\abs\absOldCex.c +# End Source File +# Begin Source File + +SOURCE=.\src\proof\abs\absOldRef.c +# End Source File +# Begin Source File + +SOURCE=.\src\proof\abs\absOldSat.c +# End Source File +# Begin Source File + +SOURCE=.\src\proof\abs\absOldSim.c +# End Source File +# Begin Source File + +SOURCE=.\src\proof\abs\absOut.c +# End Source File +# Begin Source File + +SOURCE=.\src\proof\abs\absPth.c +# End Source File +# Begin Source File + +SOURCE=.\src\proof\abs\absRef.c +# End Source File +# Begin Source File + +SOURCE=.\src\proof\abs\absRef.h +# End Source File +# Begin Source File + +SOURCE=.\src\proof\abs\absRef2.c +# End Source File +# Begin Source File + +SOURCE=.\src\proof\abs\absRef2.h +# End Source File +# Begin Source File + +SOURCE=.\src\proof\abs\absUtil.c +# End Source File +# Begin Source File + +SOURCE=.\src\proof\abs\absVta.c +# End Source File +# End Group # End Group # End Group # Begin Group "Header Files" diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index a00b7111..7670445a 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -33,17 +33,14 @@ #include "misc/vec/vec.h" #include "misc/util/utilCex.h" -#include "giaAbs.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// - ABC_NAMESPACE_HEADER_START - #define GIA_NONE 0x1FFFFFFF #define GIA_VOID 0x0FFFFFFF @@ -208,41 +205,6 @@ struct Gia_ParSim_t_ int iOutFail; // index of the failed output }; -// abstraction parameters -typedef struct Gia_ParVta_t_ Gia_ParVta_t; -struct Gia_ParVta_t_ -{ - int nFramesMax; // maximum frames - int nFramesStart; // starting frame - int nFramesPast; // overlap frames - int nConfLimit; // conflict limit - int nLearnedMax; // max number of learned clauses - int nLearnedStart; // max number of learned clauses - int nLearnedDelta; // delta increase of learned clauses - int nLearnedPerce; // percentage of clauses to leave - int nTimeOut; // timeout in seconds - int nRatioMin; // stop when less than this % of object is abstracted - int nRatioMax; // restart when the number of abstracted object is more than this - int fUseTermVars; // use terminal variables - int fUseRollback; // use rollback to the starting number of frames - int fPropFanout; // propagate fanout implications - int fAddLayer; // refinement strategy by adding layers - int fUseSkip; // skip proving intermediate timeframes - int fUseSimple; // use simple CNF construction - int fSkipHash; // skip hashing CNF while unrolling - int fUseFullProof; // use full proof for UNSAT cores - int fDumpVabs; // dumps the abstracted model - int fDumpMabs; // dumps the original AIG with abstraction map - int fCallProver; // calls the prover - char * pFileVabs; // dumps the abstracted model into this file - int fVerbose; // verbose flag - int fVeryVerbose; // print additional information - int iFrame; // the number of frames covered - int iFrameProved; // the number of frames proved - int nFramesNoChange; // the number of last frames without changes - int nFramesNoChangeLim; // the number of last frames without changes to dump abstraction -}; - static inline unsigned Gia_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); } static inline int Gia_WordHasOneBit( unsigned uWord ) { return (uWord & (uWord-1)) == 0; } static inline int Gia_WordHasOnePair( unsigned uWord ) { return Gia_WordHasOneBit(uWord & (uWord>>1) & 0x55555555); } @@ -717,26 +679,6 @@ static inline int Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i ) { re /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -/*=== giaAbs.c ===========================================================*/ -extern void Gia_ManCexAbstractionStart( Gia_Man_t * p, Gia_ParAbs_t * pPars ); -Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia ); -int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose ); -extern int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame ); -extern int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars ); -extern int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf ); -extern int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver ); -extern Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta ); -extern Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames ); -extern Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla ); -extern Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla ); -extern int Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla ); -extern int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla ); -/*=== giaAbsGla.c ===========================================================*/ -extern int Gia_GlaPerform( Gia_Man_t * p, Gia_ParVta_t * pPars, int fStartVta ); -extern int Ga2_ManPerform( Gia_Man_t * p, Gia_ParVta_t * pPars ); -/*=== giaAbsVta.c ===========================================================*/ -extern void Gia_VtaSetDefaultParams( Gia_ParVta_t * p ); -extern int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ); /*=== giaAiger.c ===========================================================*/ extern int Gia_FileSize( char * pFileName ); extern Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fSkipStrash, int fCheck ); @@ -800,9 +742,6 @@ extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, i extern Gia_Man_t * Gia_ManTransformMiter( 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_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses ); -extern Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses ); -extern void Gia_ManGlaCollect( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis, Vec_Int_t ** pvFlops, Vec_Int_t ** pvNodes ); extern Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis ); /*=== giaEnable.c ==========================================================*/ extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose ); diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c deleted file mode 100644 index c5acfa2a..00000000 --- a/src/aig/gia/giaAbs.c +++ /dev/null @@ -1,746 +0,0 @@ -/**CFile**************************************************************** - - FileName [giaAbs.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Scalable AIG package.] - - Synopsis [Counter-example-guided abstraction refinement.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: giaAbs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "gia.h" -#include "giaAig.h" -#include "aig/saig/saig.h" - -ABC_NAMESPACE_IMPL_START - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [This procedure sets default parameters.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManAbsSetDefaultParams( Gia_ParAbs_t * p ) -{ - memset( p, 0, sizeof(Gia_ParAbs_t) ); - p->Algo = 0; // algorithm: CBA - p->nFramesMax = 10; // timeframes for PBA - p->nConfMax = 10000; // conflicts for PBA - p->fDynamic = 1; // dynamic unfolding for PBA - p->fConstr = 0; // use constraints - p->nFramesBmc = 250; // timeframes for BMC - p->nConfMaxBmc = 5000; // conflicts for BMC - p->nStableMax = 1000000; // the number of stable frames to quit - p->nRatio = 10; // ratio of flops to quit - p->nBobPar = 1000000; // the number of frames before trying to quit - p->fUseBdds = 0; // use BDDs to refine abstraction - p->fUseDprove = 0; // use 'dprove' to refine abstraction - p->fUseStart = 1; // use starting frame - p->fVerbose = 0; // verbose output - p->fVeryVerbose= 0; // printing additional information - p->Status = -1; // the problem status - p->nFramesDone = -1; // the number of rames covered -} - -/**Function************************************************************* - - Synopsis [Transform flop list into flop map.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_ManFlops2Classes( Gia_Man_t * pGia, Vec_Int_t * vFlops ) -{ - Vec_Int_t * vFlopClasses; - int i, Entry; - vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) ); - Vec_IntForEachEntry( vFlops, Entry, i ) - Vec_IntWriteEntry( vFlopClasses, Entry, 1 ); - return vFlopClasses; -} - -/**Function************************************************************* - - Synopsis [Transform flop map into flop list.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_ManClasses2Flops( Vec_Int_t * vFlopClasses ) -{ - Vec_Int_t * vFlops; - int i, Entry; - vFlops = Vec_IntAlloc( 100 ); - Vec_IntForEachEntry( vFlopClasses, Entry, i ) - if ( Entry ) - Vec_IntPush( vFlops, i ); - return vFlops; -} - - -/**Function************************************************************* - - Synopsis [Starts abstraction by computing latch map.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManCexAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars ) -{ - Vec_Int_t * vFlops; - Aig_Man_t * pNew; - if ( pGia->vFlopClasses != NULL ) - { - printf( "Gia_ManCexAbstractionStart(): Abstraction latch map is present but will be rederived.\n" ); - Vec_IntFreeP( &pGia->vFlopClasses ); - } - pNew = Gia_ManToAig( pGia, 0 ); - vFlops = Saig_ManCexAbstractionFlops( pNew, pPars ); - pGia->pCexSeq = pNew->pSeqModel; pNew->pSeqModel = NULL; - Aig_ManStop( pNew ); - if ( vFlops ) - { - pGia->vFlopClasses = Gia_ManFlops2Classes( pGia, vFlops ); - Vec_IntFree( vFlops ); - } -} - -/**Function************************************************************* - - Synopsis [Refines abstraction using the latch map.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose ) -{ - Aig_Man_t * pNew; - Vec_Int_t * vFlops; - if ( pGia->vFlopClasses == NULL ) - { - printf( "Gia_ManCexAbstractionRefine(): Abstraction latch map is missing.\n" ); - return -1; - } - pNew = Gia_ManToAig( pGia, 0 ); - vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses ); - if ( !Saig_ManCexRefineStep( pNew, vFlops, pGia->vFlopClasses, pCex, nFfToAddMax, fTryFour, fSensePath, fVerbose ) ) - { - pGia->pCexSeq = pNew->pSeqModel; pNew->pSeqModel = NULL; - Vec_IntFree( vFlops ); - Aig_ManStop( pNew ); - return 0; - } - Vec_IntFree( pGia->vFlopClasses ); - pGia->vFlopClasses = Gia_ManFlops2Classes( pGia, vFlops ); - Vec_IntFree( vFlops ); - Aig_ManStop( pNew ); - return -1; -} - - - -/**Function************************************************************* - - Synopsis [Transform flop list into flop map.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_ManFlopsSelect( Vec_Int_t * vFlops, Vec_Int_t * vFlopsNew ) -{ - Vec_Int_t * vSelected; - int i, Entry; - vSelected = Vec_IntAlloc( Vec_IntSize(vFlopsNew) ); - Vec_IntForEachEntry( vFlopsNew, Entry, i ) - Vec_IntPush( vSelected, Vec_IntEntry(vFlops, Entry) ); - return vSelected; -} - -/**Function************************************************************* - - Synopsis [Adds flops that should be present in the abstraction.] - - Description [The second argument (vAbsFfsToAdd) is the array of numbers - of previously abstrated flops (flops replaced by PIs in the abstracted model) - that should be present in the abstraction as real flops.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManFlopsAddToClasses( Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd ) -{ - Vec_Int_t * vMapEntries; - int i, Entry, iFlopNum; - // map previously abstracted flops into their original numbers - vMapEntries = Vec_IntAlloc( Vec_IntSize(vFlopClasses) ); - Vec_IntForEachEntry( vFlopClasses, Entry, i ) - if ( Entry == 0 ) - Vec_IntPush( vMapEntries, i ); - // add these flops as real flops - Vec_IntForEachEntry( vAbsFfsToAdd, Entry, i ) - { - iFlopNum = Vec_IntEntry( vMapEntries, Entry ); - assert( Vec_IntEntry( vFlopClasses, iFlopNum ) == 0 ); - Vec_IntWriteEntry( vFlopClasses, iFlopNum, 1 ); - } - Vec_IntFree( vMapEntries ); -} - -/**Function************************************************************* - - Synopsis [Derive unrolled timeframes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars ) -{ - Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars; - Gia_Man_t * pAbs; - Aig_Man_t * pAig, * pOrig; - Vec_Int_t * vAbsFfsToAdd, * vAbsFfsToAddBest; - // check if flop classes are given - if ( pGia->vFlopClasses == NULL ) - { - Abc_Print( 0, "Initial flop map is not given. Trivial abstraction is assumed.\n" ); - pGia->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) ); - } - // derive abstraction - pAbs = Gia_ManDupAbsFlops( pGia, pGia->vFlopClasses ); - pAig = Gia_ManToAigSimple( pAbs ); - Gia_ManStop( pAbs ); - // refine abstraction using CBA - vAbsFfsToAdd = Saig_ManCbaPerform( pAig, Gia_ManPiNum(pGia), p ); - if ( vAbsFfsToAdd == NULL ) // found true CEX - { - assert( pAig->pSeqModel != NULL ); - printf( "Refinement did not happen. Discovered a true counter-example.\n" ); - printf( "Remapping counter-example from %d to %d primary inputs.\n", Aig_ManCiNum(pAig), Gia_ManPiNum(pGia) ); - // derive new counter-example - pOrig = Gia_ManToAigSimple( pGia ); - pGia->pCexSeq = Saig_ManCexRemap( pOrig, pAig, pAig->pSeqModel ); - Aig_ManStop( pOrig ); - Aig_ManStop( pAig ); - return 0; - } - // select the most useful flops among those to be added - if ( p->nFfToAddMax > 0 && Vec_IntSize(vAbsFfsToAdd) > p->nFfToAddMax ) - { - // compute new flops - Aig_Man_t * pAigBig = Gia_ManToAigSimple( pGia ); - vAbsFfsToAddBest = Saig_ManCbaFilterFlops( pAigBig, pAig->pSeqModel, pGia->vFlopClasses, vAbsFfsToAdd, p->nFfToAddMax ); - Aig_ManStop( pAigBig ); - assert( Vec_IntSize(vAbsFfsToAddBest) == p->nFfToAddMax ); - if ( p->fVerbose ) - printf( "Filtering flops based on cost (%d -> %d).\n", Vec_IntSize(vAbsFfsToAdd), Vec_IntSize(vAbsFfsToAddBest) ); - // update - Vec_IntFree( vAbsFfsToAdd ); - vAbsFfsToAdd = vAbsFfsToAddBest; - - } - Aig_ManStop( pAig ); - // update flop classes - Gia_ManFlopsAddToClasses( pGia->vFlopClasses, vAbsFfsToAdd ); - Vec_IntFree( vAbsFfsToAdd ); - if ( p->fVerbose ) - Gia_ManPrintStats( pGia, 0, 0 ); - return -1; -} - -/**Function************************************************************* - - Synopsis [Derive unrolled timeframes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame ) -{ - Gia_Man_t * pAbs; - Aig_Man_t * pAig, * pOrig; - Vec_Int_t * vFlops, * vFlopsNew, * vSelected; - int RetValue; - if ( pGia->vFlopClasses == NULL ) - { - printf( "Gia_ManPbaPerform(): Abstraction flop map is missing.\n" ); - return 0; - } - // derive abstraction - pAbs = Gia_ManDupAbsFlops( pGia, pGia->vFlopClasses ); - // refine abstraction using PBA - pAig = Gia_ManToAigSimple( pAbs ); - Gia_ManStop( pAbs ); - vFlopsNew = Saig_ManPbaDerive( pAig, Gia_ManPiNum(pGia), nStart, nFrames, nConfLimit, nTimeLimit, fVerbose, piFrame ); - // derive new classes - if ( pAig->pSeqModel == NULL ) - { - // check if there is no timeout - if ( vFlopsNew != NULL ) - { - // the problem is UNSAT - vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses ); - vSelected = Gia_ManFlopsSelect( vFlops, vFlopsNew ); - Vec_IntFree( pGia->vFlopClasses ); - pGia->vFlopClasses = Saig_ManFlops2Classes( Gia_ManRegNum(pGia), vSelected ); - Vec_IntFree( vSelected ); - - Vec_IntFree( vFlopsNew ); - Vec_IntFree( vFlops ); - } - RetValue = -1; - } - else if ( vFlopsNew == NULL ) - { - // found real counter-example - assert( pAig->pSeqModel != NULL ); - printf( "Refinement did not happen. Discovered a true counter-example.\n" ); - printf( "Remapping counter-example from %d to %d primary inputs.\n", Aig_ManCiNum(pAig), Gia_ManPiNum(pGia) ); - // derive new counter-example - pOrig = Gia_ManToAigSimple( pGia ); - pGia->pCexSeq = Saig_ManCexRemap( pOrig, pAig, pAig->pSeqModel ); - Aig_ManStop( pOrig ); - RetValue = 0; - } - else - { - // found counter-eample for the abstracted model - // update flop classes - Vec_Int_t * vAbsFfsToAdd = vFlopsNew; - Gia_ManFlopsAddToClasses( pGia->vFlopClasses, vAbsFfsToAdd ); - Vec_IntFree( vAbsFfsToAdd ); - RetValue = -1; - } - Aig_ManStop( pAig ); - if ( fVerbose ) - Gia_ManPrintStats( pGia, 0, 0 ); - return RetValue; -} - - -/**Function************************************************************* - - Synopsis [Derive unrolled timeframes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf ) -{ - extern Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose, int * piFrame ); - Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars; - Vec_Int_t * vGateClasses, * vGateClassesOld = NULL; - Aig_Man_t * pAig; - - // check if flop classes are given - if ( pGia->vGateClasses == NULL ) - Abc_Print( 0, "Initial gate map is not given. Abstraction begins from scratch.\n" ); - else - { - Abc_Print( 0, "Initial gate map is given. Abstraction refines this map.\n" ); - vGateClassesOld = pGia->vGateClasses; pGia->vGateClasses = NULL; - fNaiveCnf = 1; - } - - // perform abstraction - p->iFrame = -1; - pAig = Gia_ManToAigSimple( pGia ); - assert( vGateClassesOld == NULL || Vec_IntSize(vGateClassesOld) == Aig_ManObjNumMax(pAig) ); - vGateClasses = Aig_Gla1ManPerform( pAig, vGateClassesOld, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose, &p->iFrame ); - Aig_ManStop( pAig ); - - // update the map - Vec_IntFreeP( &vGateClassesOld ); - pGia->vGateClasses = vGateClasses; - if ( p->fVerbose ) - Gia_ManPrintStats( pGia, 0, 0 ); - return 1; -} - -/**Function************************************************************* - - Synopsis [Derive unrolled timeframes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver ) -{ - extern Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose ); - extern Vec_Int_t * Aig_Gla3ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose ); - Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars; - Vec_Int_t * vGateClasses; - Gia_Man_t * pGiaAbs; - Aig_Man_t * pAig; - - // check if flop classes are given - if ( pGia->vGateClasses == NULL ) - { - Abc_Print( 0, "Initial gate map is not given. Abstraction begins from scratch.\n" ); - pAig = Gia_ManToAigSimple( pGia ); - } - else - { - Abc_Print( 0, "Initial gate map is given. Abstraction refines this map.\n" ); - pGiaAbs = Gia_ManDupAbsGates( pGia, pGia->vGateClasses ); - pAig = Gia_ManToAigSimple( pGiaAbs ); - Gia_ManStop( pGiaAbs ); - } - - // perform abstraction - if ( fNewSolver ) - vGateClasses = Aig_Gla3ManPerform( pAig, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fSkipRand, p->fVerbose ); - else - vGateClasses = Aig_Gla2ManPerform( pAig, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fSkipRand, p->fVerbose ); - Aig_ManStop( pAig ); - - // update the BMC depth - if ( vGateClasses ) - p->iFrame = p->nFramesMax; - - // update the abstraction map (hint: AIG and GIA have one-to-one obj ID match) - if ( pGia->vGateClasses && vGateClasses ) - { - Gia_Obj_t * pObj; - int i, Counter = 0; - Gia_ManForEachObj1( pGia, pObj, i ) - { - if ( !~pObj->Value ) - continue; - if ( !Vec_IntEntry(pGia->vGateClasses, i) ) - continue; - // this obj was abstracted before - assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(pGia, pObj) ); - // if corresponding AIG object is not abstracted, remove abstraction - if ( !Vec_IntEntry(vGateClasses, Abc_Lit2Var(pObj->Value)) ) - { - Vec_IntWriteEntry( pGia->vGateClasses, i, 0 ); - Counter++; - } - } - Vec_IntFree( vGateClasses ); - if ( p->fVerbose ) - Abc_Print( 1, "Repetition of abstraction removed %d entries from the old abstraction map.\n", Counter ); - } - else - { - Vec_IntFreeP( &pGia->vGateClasses ); - pGia->vGateClasses = vGateClasses; - } - // clean up the abstraction map - if ( pGia->vGateClasses ) - { - pGiaAbs = Gia_ManDupAbsGates( pGia, pGia->vGateClasses ); - Gia_ManStop( pGiaAbs ); - } - if ( p->fVerbose ) - Gia_ManPrintStats( pGia, 0, 0 ); - return 1; -} - - - -/**Function************************************************************* - - Synopsis [Converting VTA vector to GLA vector.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta ) -{ - Gia_Obj_t * pObj; - Vec_Int_t * vGla; - int nObjMask, nObjs = Gia_ManObjNum(p); - int i, Entry, nFrames = Vec_IntEntry( vVta, 0 ); - assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) ); - // get the bitmask - nObjMask = (1 << Abc_Base2Log(nObjs)) - 1; - assert( nObjs <= nObjMask ); - // go through objects - vGla = Vec_IntStart( nObjs ); - Vec_IntForEachEntryStart( vVta, Entry, i, nFrames+2 ) - { - pObj = Gia_ManObj( p, (Entry & nObjMask) ); - assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsConst0(pObj) ); - Vec_IntAddToEntry( vGla, (Entry & nObjMask), 1 ); - } - Vec_IntWriteEntry( vGla, 0, nFrames ); - return vGla; -} - -/**Function************************************************************* - - Synopsis [Converting GLA vector to VTA vector.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames ) -{ - Vec_Int_t * vVta; - int nObjBits, nObjMask, nObjs = Gia_ManObjNum(p); - int i, k, j, Entry, Counter, nGlaSize; - //. get the GLA size - nGlaSize = Vec_IntSum(vGla); - // get the bitmask - nObjBits = Abc_Base2Log(nObjs); - nObjMask = (1 << Abc_Base2Log(nObjs)) - 1; - assert( nObjs <= nObjMask ); - // go through objects - vVta = Vec_IntAlloc( 1000 ); - Vec_IntPush( vVta, nFrames ); - Counter = nFrames + 2; - for ( i = 0; i <= nFrames; i++, Counter += i * nGlaSize ) - Vec_IntPush( vVta, Counter ); - for ( i = 0; i < nFrames; i++ ) - for ( k = 0; k <= i; k++ ) - Vec_IntForEachEntry( vGla, Entry, j ) - if ( Entry ) - Vec_IntPush( vVta, (k << nObjBits) | j ); - Counter = Vec_IntEntry(vVta, nFrames+1); - assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) ); - return vVta; -} - -/**Function************************************************************* - - Synopsis [Converting GLA vector to FLA vector.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_FlaConvertToGla_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vGla ) -{ - if ( Gia_ObjIsTravIdCurrent(p, pObj) ) - return; - Gia_ObjSetTravIdCurrent(p, pObj); - Vec_IntWriteEntry( vGla, Gia_ObjId(p, pObj), 1 ); - if ( Gia_ObjIsRo(p, pObj) ) - return; - assert( Gia_ObjIsAnd(pObj) ); - Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla ); - Gia_FlaConvertToGla_rec( p, Gia_ObjFanin1(pObj), vGla ); -} - -/**Function************************************************************* - - Synopsis [Converting FLA vector to GLA vector.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla ) -{ - Vec_Int_t * vGla; - Gia_Obj_t * pObj; - int i; - // mark const0 and relevant CI objects - Gia_ManIncrementTravId( p ); - Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p)); - Gia_ManForEachPi( p, pObj, i ) - Gia_ObjSetTravIdCurrent(p, pObj); - Gia_ManForEachRo( p, pObj, i ) - if ( !Vec_IntEntry(vFla, i) ) - Gia_ObjSetTravIdCurrent(p, pObj); - // label all objects reachable from the PO and selected flops - vGla = Vec_IntStart( Gia_ManObjNum(p) ); - Vec_IntWriteEntry( vGla, 0, 1 ); - Gia_ManForEachPo( p, pObj, i ) - Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla ); - Gia_ManForEachRi( p, pObj, i ) - if ( Vec_IntEntry(vFla, i) ) - Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla ); - return vGla; -} - -/**Function************************************************************* - - Synopsis [Converting GLA vector to FLA vector.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla ) -{ - Vec_Int_t * vFla; - Gia_Obj_t * pObj; - int i; - vFla = Vec_IntStart( Gia_ManRegNum(p) ); - Gia_ManForEachRo( p, pObj, i ) - if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) ) - Vec_IntWriteEntry( vFla, i, 1 ); - return vFla; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManGlaPurify( Gia_Man_t * p, int nPurifyRatio, int fVerbose ) -{ - int i, Entry, CountUpTo, CountAll, CountRem, * pCounts; - int nFrames = Vec_IntEntry( p->vGateClasses, 0 ); - if ( nFrames < 2 ) - { - printf( "Gate-level abstraction is missing object count information.\n" ); - return; - } - // collect info - CountAll = 0; - pCounts = ABC_CALLOC( int, nFrames + 1 ); - assert( Vec_IntSize(p->vGateClasses) == Gia_ManObjNum(p) ); - for ( i = 0; i < Gia_ManObjNum(p); i++ ) - { - Entry = Vec_IntEntry( p->vGateClasses, i ); - assert( Entry >= 0 && Entry <= nFrames ); - if ( Entry == 0 ) - continue; - CountAll++; - pCounts[Entry]++; - } - // print entries - CountUpTo = 0; - for ( i = 0; i <= nFrames; i++ ) - printf( "%d=%d(%d) ", i, pCounts[i], CountUpTo += pCounts[i] ); - printf( "\n" ); - // removing entries appearing only ones - CountRem = 0; - for ( i = 0; i < Gia_ManObjNum(p); i++ ) - { - if ( Vec_IntEntry( p->vGateClasses, i ) == 0 ) - continue; - if ( Vec_IntEntry( p->vGateClasses, i ) <= nPurifyRatio ) - { - CountRem++; - Vec_IntWriteEntry( p->vGateClasses, i, 0 ); - } - } - printf( "Removed %d entries appearing less or equal than %d times (out of %d).\n", CountRem, nPurifyRatio, CountAll ); - ABC_FREE( pCounts ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla ) -{ - Gia_Obj_t * pObj; - int i, Count = 0; - Gia_ManForEachRo( p, pObj, i ) - if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) ) - Count++; - return Count; -} -int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla ) -{ - Gia_Obj_t * pObj; - int i, Count = 0; - Gia_ManForEachAnd( p, pObj, i ) - if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) ) - Count++; - return Count; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/aig/gia/giaAbs.h b/src/aig/gia/giaAbs.h deleted file mode 100644 index 366a4d8a..00000000 --- a/src/aig/gia/giaAbs.h +++ /dev/null @@ -1,89 +0,0 @@ -/**CFile**************************************************************** - - FileName [giaAbs.h] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Scalable AIG package.] - - Synopsis [External declarations.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: giaAbs.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef ABC__aig__gia__giaAbs_h -#define ABC__aig__gia__giaAbs_h - - -//////////////////////////////////////////////////////////////////////// -/// INCLUDES /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// PARAMETERS /// -//////////////////////////////////////////////////////////////////////// - - - -ABC_NAMESPACE_HEADER_START - - -//////////////////////////////////////////////////////////////////////// -/// BASIC TYPES /// -//////////////////////////////////////////////////////////////////////// - -// abstraction parameters -typedef struct Gia_ParAbs_t_ Gia_ParAbs_t; -struct Gia_ParAbs_t_ -{ - int Algo; // the algorithm to be used - int nFramesMax; // timeframes for PBA - int nConfMax; // conflicts for PBA - int fDynamic; // dynamic unfolding for PBA - int fConstr; // use constraints - int nFramesBmc; // timeframes for BMC - int nConfMaxBmc; // conflicts for BMC - int nStableMax; // the number of stable frames to quit - int nRatio; // ratio of flops to quit - int TimeOut; // approximate timeout in seconds - int TimeOutVT; // approximate timeout in seconds - int nBobPar; // Bob's parameter - int fUseBdds; // use BDDs to refine abstraction - int fUseDprove; // use 'dprove' to refine abstraction - int fUseStart; // use starting frame - int fVerbose; // verbose output - int fVeryVerbose; // printing additional information - int Status; // the problem status - int nFramesDone; // the number of frames covered -}; - -extern void Gia_ManAbsSetDefaultParams( Gia_ParAbs_t * p ); - -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - - - - -ABC_NAMESPACE_HEADER_END - - - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 9a8c1baa..b0bf9c1e 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1665,263 +1665,6 @@ Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes ) /**Function************************************************************* - Synopsis [Duplicates the AIG manager recursively.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManDupAbsFlops_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj ) -{ - if ( ~pObj->Value ) - return; - assert( Gia_ObjIsAnd(pObj) ); - Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) ); - Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin1(pObj) ); - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); -} - -/**Function************************************************************* - - Synopsis [Performs abstraction of the AIG to preserve the included flops.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses ) -{ - Gia_Man_t * pNew, * pTemp; - Gia_Obj_t * pObj; - int i, nFlops = 0; - Gia_ManFillValue( p ); - // start the new manager - pNew = Gia_ManStart( 5000 ); - pNew->pName = Abc_UtilStrsav( p->pName ); - pNew->pSpec = Abc_UtilStrsav( p->pSpec ); - // create PIs - Gia_ManConst0(p)->Value = 0; - Gia_ManForEachPi( p, pObj, i ) - pObj->Value = Gia_ManAppendCi(pNew); - // create additional PIs - Gia_ManForEachRo( p, pObj, i ) - if ( !Vec_IntEntry(vFlopClasses, i) ) - pObj->Value = Gia_ManAppendCi(pNew); - // create ROs - Gia_ManForEachRo( p, pObj, i ) - if ( Vec_IntEntry(vFlopClasses, i) ) - pObj->Value = Gia_ManAppendCi(pNew); - // create POs - Gia_ManHashAlloc( pNew ); - Gia_ManForEachPo( p, pObj, i ) - { - Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) ); - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - } - // create RIs - Gia_ManForEachRi( p, pObj, i ) - if ( Vec_IntEntry(vFlopClasses, i) ) - { - Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) ); - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - nFlops++; - } - Gia_ManHashStop( pNew ); - Gia_ManSetRegNum( pNew, nFlops ); - // clean up - pNew = Gia_ManSeqCleanup( pTemp = pNew ); - Gia_ManStop( pTemp ); - return pNew; -} - -/**Function************************************************************* - - Synopsis [Returns the array of neighbors.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses ) -{ - Vec_Int_t * vAssigned; - Gia_Obj_t * pObj; - int i, Entry; - vAssigned = Vec_IntAlloc( 1000 ); - Vec_IntForEachEntry( vGateClasses, Entry, i ) - { - if ( Entry == 0 ) - continue; - assert( Entry > 0 ); - pObj = Gia_ManObj( p, i ); - Vec_IntPush( vAssigned, Gia_ObjId(p, pObj) ); - if ( Gia_ObjIsAnd(pObj) ) - { - Vec_IntPush( vAssigned, Gia_ObjFaninId0p(p, pObj) ); - Vec_IntPush( vAssigned, Gia_ObjFaninId1p(p, pObj) ); - } - else if ( Gia_ObjIsRo(p, pObj) ) - Vec_IntPush( vAssigned, Gia_ObjFaninId0p(p, Gia_ObjRoToRi(p, pObj)) ); - else assert( Gia_ObjIsConst0(pObj) ); - } - Vec_IntUniqify( vAssigned ); - return vAssigned; -} - -/**Function************************************************************* - - Synopsis [Collects PIs and PPIs of the abstraction.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManGlaCollect( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis, Vec_Int_t ** pvFlops, Vec_Int_t ** pvNodes ) -{ - Vec_Int_t * vAssigned; - Gia_Obj_t * pObj; - int i; - assert( Gia_ManPoNum(p) == 1 ); - assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) ); - // create included objects and their fanins - vAssigned = Gia_GlaCollectAssigned( p, vGateClasses ); - // create additional arrays - if ( pvPis ) *pvPis = Vec_IntAlloc( 100 ); - if ( pvPPis ) *pvPPis = Vec_IntAlloc( 100 ); - if ( pvFlops ) *pvFlops = Vec_IntAlloc( 100 ); - if ( pvNodes ) *pvNodes = Vec_IntAlloc( 1000 ); - Gia_ManForEachObjVec( vAssigned, p, pObj, i ) - { - if ( Gia_ObjIsPi(p, pObj) ) - { if ( pvPis ) Vec_IntPush( *pvPis, Gia_ObjId(p,pObj) ); } - else if ( !Vec_IntEntry(vGateClasses, Gia_ObjId(p,pObj)) ) - { if ( pvPPis ) Vec_IntPush( *pvPPis, Gia_ObjId(p,pObj) ); } - else if ( Gia_ObjIsRo(p, pObj) ) - { if ( pvFlops ) Vec_IntPush( *pvFlops, Gia_ObjId(p,pObj) ); } - else if ( Gia_ObjIsAnd(pObj) ) - { if ( pvNodes ) Vec_IntPush( *pvNodes, Gia_ObjId(p,pObj) ); } - else assert( Gia_ObjIsConst0(pObj) ); - } - Vec_IntFree( vAssigned ); -} - -/**Function************************************************************* - - Synopsis [Duplicates the AIG manager recursively.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManDupAbsGates_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj ) -{ - if ( ~pObj->Value ) - return; - assert( Gia_ObjIsAnd(pObj) ); - Gia_ManDupAbsGates_rec( pNew, Gia_ObjFanin0(pObj) ); - Gia_ManDupAbsGates_rec( pNew, Gia_ObjFanin1(pObj) ); - pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); -} - -/**Function************************************************************* - - Synopsis [Performs abstraction of the AIG to preserve the included gates.] - - Description [The array contains 1 for those objects (const, RO, AND) - that are included in the abstraction; 0, otherwise.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses ) -{ - Vec_Int_t * vPis, * vPPis, * vFlops, * vNodes; - Gia_Man_t * pNew, * pTemp; - Gia_Obj_t * pObj, * pCopy; - int i;//, nFlops = 0; - assert( Gia_ManPoNum(p) == 1 ); - assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) ); - - // create additional arrays - Gia_ManGlaCollect( p, vGateClasses, &vPis, &vPPis, &vFlops, &vNodes ); - - // start the new manager - pNew = Gia_ManStart( 5000 ); - pNew->pName = Abc_UtilStrsav( p->pName ); - pNew->pSpec = Abc_UtilStrsav( p->pSpec ); - // create constant - Gia_ManFillValue( p ); - Gia_ManConst0(p)->Value = 0; - // create PIs - Gia_ManForEachObjVec( vPis, p, pObj, i ) - pObj->Value = Gia_ManAppendCi(pNew); - // create additional PIs - Gia_ManForEachObjVec( vPPis, p, pObj, i ) - pObj->Value = Gia_ManAppendCi(pNew); - // create ROs - Gia_ManForEachObjVec( vFlops, p, pObj, i ) - pObj->Value = Gia_ManAppendCi(pNew); - // create internal nodes - Gia_ManForEachObjVec( vNodes, p, pObj, i ) - pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); -// Gia_ManDupAbsGates_rec( pNew, pObj ); - // create PO - Gia_ManForEachPo( p, pObj, i ) - pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - // create RIs - Gia_ManForEachObjVec( vFlops, p, pObj, i ) - Gia_ObjRoToRi(p, pObj)->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ObjRoToRi(p, pObj)) ); - Gia_ManSetRegNum( pNew, Vec_IntSize(vFlops) ); - // clean up - pNew = Gia_ManSeqCleanup( pTemp = pNew ); - // transfer copy values: (p -> pTemp -> pNew) => (p -> pNew) - if ( Gia_ManObjNum(pTemp) != Gia_ManObjNum(pNew) ) - { -// printf( "Gia_ManDupAbsGates() Internal error: object mismatch.\n" ); - Gia_ManForEachObj( p, pObj, i ) - { - if ( !~pObj->Value ) - continue; - assert( !Abc_LitIsCompl(pObj->Value) ); - pCopy = Gia_ObjCopy( pTemp, pObj ); - if ( !~pCopy->Value ) - { - Vec_IntWriteEntry( vGateClasses, i, 0 ); - pObj->Value = ~0; - continue; - } - assert( !Abc_LitIsCompl(pCopy->Value) ); - pObj->Value = pCopy->Value; - } - } - Gia_ManStop( pTemp ); - - Vec_IntFree( vPis ); - Vec_IntFree( vPPis ); - Vec_IntFree( vFlops ); - Vec_IntFree( vNodes ); - return pNew; -} - -/**Function************************************************************* - Synopsis [Copy an AIG structure related to the selected POs.] Description [] diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 2b16f326..6b57e292 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -20,6 +20,7 @@ #include "gia.h" #include "misc/tim/tim.h" +#include "proof/abs/abs.h" ABC_NAMESPACE_IMPL_START @@ -176,155 +177,6 @@ void Gia_ManPrintClasses_old( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Gia_ManPrintFlopClasses( Gia_Man_t * p ) -{ - int Counter0, Counter1; - if ( p->vFlopClasses == NULL ) - return; - if ( Vec_IntSize(p->vFlopClasses) != Gia_ManRegNum(p) ) - { - printf( "Gia_ManPrintFlopClasses(): The number of flop map entries differs from the number of flops.\n" ); - return; - } - Counter0 = Vec_IntCountEntry( p->vFlopClasses, 0 ); - Counter1 = Vec_IntCountEntry( p->vFlopClasses, 1 ); - printf( "Flop-level abstraction: Excluded FFs = %d Included FFs = %d (%.2f %%) ", - Counter0, Counter1, 100.0*Counter1/(Counter0 + Counter1 + 1) ); - if ( Counter0 + Counter1 < Gia_ManRegNum(p) ) - printf( "and there are other FF classes..." ); - printf( "\n" ); -} - -/**Function************************************************************* - - Synopsis [Prints stats for the AIG.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManPrintGateClasses( Gia_Man_t * p ) -{ - Vec_Int_t * vPis, * vPPis, * vFlops, * vNodes; - int nTotal; - if ( p->vGateClasses == NULL ) - return; - if ( Vec_IntSize(p->vGateClasses) != Gia_ManObjNum(p) ) - { - printf( "Gia_ManPrintGateClasses(): The number of flop map entries differs from the number of flops.\n" ); - return; - } - // create additional arrays - Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, &vFlops, &vNodes ); - nTotal = 1 + Vec_IntSize(vFlops) + Vec_IntSize(vNodes); - printf( "Gate-level abstraction: PI = %d PPI = %d FF = %d (%.2f %%) AND = %d (%.2f %%) Obj = %d (%.2f %%)\n", - Vec_IntSize(vPis), Vec_IntSize(vPPis), - Vec_IntSize(vFlops), 100.0*Vec_IntSize(vFlops)/(Gia_ManRegNum(p)+1), - Vec_IntSize(vNodes), 100.0*Vec_IntSize(vNodes)/(Gia_ManAndNum(p)+1), - nTotal, 100.0*nTotal /(Gia_ManRegNum(p)+Gia_ManAndNum(p)+1) ); - Vec_IntFree( vPis ); - Vec_IntFree( vPPis ); - Vec_IntFree( vFlops ); - Vec_IntFree( vNodes ); -} - -/**Function************************************************************* - - Synopsis [Prints stats for the AIG.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManPrintObjClasses( Gia_Man_t * p ) -{ - Vec_Int_t * vSeens; // objects seen so far - Vec_Int_t * vAbs = p->vObjClasses; - int i, k, Entry, iStart, iStop = -1, nFrames; - int nObjBits, nObjMask, iObj, iFrame, nWords; - unsigned * pInfo; - int * pCountAll, * pCountUni; - if ( vAbs == NULL ) - return; - nFrames = Vec_IntEntry( vAbs, 0 ); - assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) ); - pCountAll = ABC_ALLOC( int, nFrames + 1 ); - pCountUni = ABC_ALLOC( int, nFrames + 1 ); - // start storage for seen objects - nWords = Abc_BitWordNum( nFrames ); - vSeens = Vec_IntStart( Gia_ManObjNum(p) * nWords ); - // get the bitmasks - nObjBits = Abc_Base2Log( Gia_ManObjNum(p) ); - nObjMask = (1 << nObjBits) - 1; - assert( Gia_ManObjNum(p) <= nObjMask ); - // print info about frames - printf( "Frame Core F0 F1 F2 F3 ...\n" ); - for ( i = 0; i < nFrames; i++ ) - { - iStart = Vec_IntEntry( vAbs, i+1 ); - iStop = Vec_IntEntry( vAbs, i+2 ); - memset( pCountAll, 0, sizeof(int) * (nFrames + 1) ); - memset( pCountUni, 0, sizeof(int) * (nFrames + 1) ); - Vec_IntForEachEntryStartStop( vAbs, Entry, k, iStart, iStop ) - { - iObj = (Entry & nObjMask); - iFrame = (Entry >> nObjBits); - pInfo = (unsigned *)Vec_IntEntryP( vSeens, nWords * iObj ); - if ( Abc_InfoHasBit(pInfo, iFrame) == 0 ) - { - Abc_InfoSetBit( pInfo, iFrame ); - pCountUni[iFrame+1]++; - pCountUni[0]++; - } - pCountAll[iFrame+1]++; - pCountAll[0]++; - } - assert( pCountAll[0] == (iStop - iStart) ); -// printf( "%5d%5d ", pCountAll[0], pCountUni[0] ); - printf( "%3d :", i ); - printf( "%7d", pCountAll[0] ); - if ( i >= 10 ) - { - for ( k = 0; k < 4; k++ ) - printf( "%5d", pCountAll[k+1] ); - printf( " ..." ); - for ( k = i-4; k <= i; k++ ) - printf( "%5d", pCountAll[k+1] ); - } - else - { - for ( k = 0; k <= i; k++ ) - if ( k <= i ) - printf( "%5d", pCountAll[k+1] ); - } -// for ( k = 0; k < nFrames; k++ ) -// if ( k <= i ) -// printf( "%5d", pCountAll[k+1] ); - printf( "\n" ); - } - assert( iStop == Vec_IntSize(vAbs) ); - Vec_IntFree( vSeens ); - ABC_FREE( pCountAll ); - ABC_FREE( pCountUni ); -} - -/**Function************************************************************* - - Synopsis [Prints stats for the AIG.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ void Gia_ManPrintPlacement( Gia_Man_t * p ) { int i, nFixed = 0, nUndef = 0; diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index ea3ca24d..89af261a 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -1,13 +1,4 @@ SRC += src/aig/gia/gia.c \ - src/aig/gia/giaAbs.c \ - src/aig/gia/giaAbsGla.c \ - src/aig/gia/giaAbsGla2.c \ - src/aig/gia/giaAbsIter.c \ - src/aig/gia/giaAbsOut.c \ - src/aig/gia/giaAbsPth.c \ - src/aig/gia/giaAbsRef.c \ - src/aig/gia/giaAbsRef2.c \ - src/aig/gia/giaAbsVta.c \ src/aig/gia/giaAig.c \ src/aig/gia/giaAiger.c \ src/aig/gia/giaBidec.c \ diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index 42e3c090..edf5798e 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -1,9 +1,4 @@ -SRC += src/aig/saig/saigAbs.c \ - src/aig/saig/saigAbsCba.c \ - src/aig/saig/saigAbsPba.c \ - src/aig/saig/saigAbsStart.c \ - src/aig/saig/saigAbsVfa.c \ - src/aig/saig/saigBmc.c \ +SRC += src/aig/saig/saigBmc.c \ src/aig/saig/saigBmc2.c \ src/aig/saig/saigBmc3.c \ src/aig/saig/saigCexMin.c \ @@ -12,9 +7,6 @@ SRC += src/aig/saig/saigAbs.c \ src/aig/saig/saigConstr2.c \ src/aig/saig/saigDual.c \ src/aig/saig/saigDup.c \ - src/aig/saig/saigGlaCba.c \ - src/aig/saig/saigGlaPba.c \ - src/aig/saig/saigGlaPba2.c \ src/aig/saig/saigHaig.c \ src/aig/saig/saigInd.c \ src/aig/saig/saigIoa.c \ @@ -24,13 +16,10 @@ SRC += src/aig/saig/saigAbs.c \ src/aig/saig/saigMiter.c \ src/aig/saig/saigOutDec.c \ src/aig/saig/saigPhase.c \ - src/aig/saig/saigRefSat.c \ src/aig/saig/saigRetFwd.c \ src/aig/saig/saigRetMin.c \ src/aig/saig/saigRetStep.c \ src/aig/saig/saigScl.c \ - src/aig/saig/saigSimExt.c \ - src/aig/saig/saigSimExt2.c \ src/aig/saig/saigSimFast.c \ src/aig/saig/saigSimMv.c \ src/aig/saig/saigSimSeq.c \ diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index e7cdea90..8823dcac 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -27,7 +27,6 @@ //////////////////////////////////////////////////////////////////////// #include "aig/aig/aig.h" -#include "aig/gia/giaAbs.h" ABC_NAMESPACE_HEADER_START @@ -35,10 +34,6 @@ ABC_NAMESPACE_HEADER_START /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// -#define SAIG_ZER 1 -#define SAIG_ONE 2 -#define SAIG_UND 3 - //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// @@ -131,20 +126,6 @@ static inline int Saig_ObjRegId( Aig_Man_t * p, Aig_Obj_t * pObj ) { /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -/*=== sswAbs.c ==========================================================*/ -extern Vec_Int_t * Saig_ManClasses2Flops( Vec_Int_t * vFlopClasses ); -extern Vec_Int_t * Saig_ManFlops2Classes( int nRegs, Vec_Int_t * vFlops ); -extern Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexAbs ); -/*=== sswAbsCba.c ==========================================================*/ -extern Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect ); -extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose ); -extern Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose ); -extern Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAig, int nInputs, Saig_ParBmc_t * pPars ); -/*=== sswAbsPba.c ==========================================================*/ -extern Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame ); -/*=== sswAbsStart.c ==========================================================*/ -extern int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vFlopClasses, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose ); -extern Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ); /*=== saigBmc.c ==========================================================*/ extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit ); extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent ); @@ -203,8 +184,6 @@ extern int Saig_ManDemiterNew( Aig_Man_t * pMan ); extern Aig_Man_t * Saig_ManDecPropertyOutput( Aig_Man_t * pAig, int nLits, int fVerbose ); /*=== saigPhase.c ==========================================================*/ extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose ); -/*=== saigRefSat.c ==========================================================*/ -extern Vec_Int_t * Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose ); /*=== saigRetFwd.c ==========================================================*/ extern void Saig_ManMarkAutonomous( Aig_Man_t * p ); extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose ); @@ -215,11 +194,6 @@ extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, in extern int Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward, int fAddBugs ); /*=== saigScl.c ==========================================================*/ extern void Saig_ManReportUselessRegisters( Aig_Man_t * pAig ); -/*=== saigSimExt.c ==========================================================*/ -extern Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ); -extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fTryFour, int fVerbose ); -/*=== saigSimExt.c ==========================================================*/ -extern Vec_Int_t * Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fVerbose ); /*=== saigSimMv.c ==========================================================*/ extern Vec_Ptr_t * Saig_MvManSimulate( Aig_Man_t * pAig, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose ); /*=== saigStrSim.c ==========================================================*/ diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c deleted file mode 100644 index f30963a8..00000000 --- a/src/aig/saig/saigAbs.c +++ /dev/null @@ -1,133 +0,0 @@ -/**CFile**************************************************************** - - FileName [saigAbs.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Sequential AIG package.] - - Synopsis [Intergrated abstraction procedure.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: saigAbs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "saig.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Transform flop map into flop list.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_ManClasses2Flops( Vec_Int_t * vFlopClasses ) -{ - Vec_Int_t * vFlops; - int i, Entry; - vFlops = Vec_IntAlloc( 100 ); - Vec_IntForEachEntry( vFlopClasses, Entry, i ) - if ( Entry ) - Vec_IntPush( vFlops, i ); - return vFlops; -} - -/**Function************************************************************* - - Synopsis [Transform flop list into flop map.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_ManFlops2Classes( int nRegs, Vec_Int_t * vFlops ) -{ - Vec_Int_t * vFlopClasses; - int i, Entry; - vFlopClasses = Vec_IntStart( nRegs ); - Vec_IntForEachEntry( vFlops, Entry, i ) - Vec_IntWriteEntry( vFlopClasses, Entry, 1 ); - return vFlopClasses; -} - -/**Function************************************************************* - - Synopsis [Derive a new counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexAbs ) -{ - Abc_Cex_t * pCex; - Aig_Obj_t * pObj; - int i, f; - if ( !Saig_ManVerifyCex( pAbs, pCexAbs ) ) - printf( "Saig_ManCexRemap(): The initial counter-example is invalid.\n" ); -// else -// printf( "Saig_ManCexRemap(): The initial counter-example is correct.\n" ); - // start the counter-example - pCex = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 ); - pCex->iFrame = pCexAbs->iFrame; - pCex->iPo = pCexAbs->iPo; - // copy the bit data - for ( f = 0; f <= pCexAbs->iFrame; f++ ) - { - Saig_ManForEachPi( pAbs, pObj, i ) - { - if ( i == Saig_ManPiNum(p) ) - break; - if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) ) - Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + i ); - } - } - // verify the counter example - if ( !Saig_ManVerifyCex( p, pCex ) ) - { - printf( "Saig_ManCexRemap(): Counter-example is invalid.\n" ); - Abc_CexFree( pCex ); - pCex = NULL; - } - else - { - Abc_Print( 1, "Counter-example verification is successful.\n" ); - Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. \n", pCex->iPo, p->pName, pCex->iFrame ); - } - return pCex; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c deleted file mode 100644 index 34e1decf..00000000 --- a/src/aig/saig/saigAbsPba.c +++ /dev/null @@ -1,374 +0,0 @@ -/**CFile**************************************************************** - - FileName [saigAbsPba.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Sequential AIG package.] - - Synopsis [Proof-based abstraction.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: saigAbsPba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "saig.h" -#include "sat/cnf/cnf.h" -#include "sat/bsat/satSolver.h" -#include "aig/gia/giaAig.h" - -ABC_NAMESPACE_IMPL_START - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Collect nodes in the unrolled timeframes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Saig_ManUnrollForPba_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vObjs, Vec_Int_t * vRoots ) -{ - if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) - return; - Aig_ObjSetTravIdCurrent(pAig, pObj); - if ( Aig_ObjIsCo(pObj) ) - Saig_ManUnrollForPba_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots ); - else if ( Aig_ObjIsNode(pObj) ) - { - Saig_ManUnrollForPba_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots ); - Saig_ManUnrollForPba_rec( pAig, Aig_ObjFanin1(pObj), vObjs, vRoots ); - } - if ( vRoots && Saig_ObjIsLo( pAig, pObj ) ) - Vec_IntPush( vRoots, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) ); - Vec_IntPush( vObjs, Aig_ObjId(pObj) ); -} - -/**Function************************************************************* - - Synopsis [Derives unrolled timeframes for PBA.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nStart, int nFrames, Vec_Int_t ** pvPiVarMap ) -{ - Aig_Man_t * pFrames; // unrolled timeframes - Vec_Vec_t * vFrameCos; // the list of COs per frame - Vec_Vec_t * vFrameObjs; // the list of objects per frame - Vec_Int_t * vRoots, * vObjs; - Aig_Obj_t * pObj, * pObjNew; - int i, f; - assert( nStart <= nFrames ); - // collect COs and Objs visited in each frame - vFrameCos = Vec_VecStart( nFrames ); - vFrameObjs = Vec_VecStart( nFrames ); - for ( f = nFrames-1; f >= 0; f-- ) - { - // add POs of this frame - vRoots = Vec_VecEntryInt( vFrameCos, f ); - Saig_ManForEachPo( pAig, pObj, i ) - Vec_IntPush( vRoots, Aig_ObjId(pObj) ); - // collect nodes starting from the roots - Aig_ManIncrementTravId( pAig ); - Aig_ManForEachObjVec( vRoots, pAig, pObj, i ) - Saig_ManUnrollForPba_rec( pAig, pObj, - Vec_VecEntryInt( vFrameObjs, f ), - (Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) ); - } - // derive unrolled timeframes - pFrames = Aig_ManStart( 10000 ); - pFrames->pName = Abc_UtilStrsav( pAig->pName ); - pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec ); - // create activation variables - Saig_ManForEachLo( pAig, pObj, i ) - Aig_ObjCreateCi( pFrames ); - // initialize the flops - Saig_ManForEachLo( pAig, pObj, i ) - pObj->pData = Aig_Mux( pFrames, Aig_ManCi(pFrames,i), Aig_ObjCreateCi(pFrames), Aig_ManConst0(pFrames) ); - // iterate through the frames - *pvPiVarMap = Vec_IntStartFull( nFrames * Saig_ManPiNum(pAig) ); - pObjNew = Aig_ManConst0(pFrames); - for ( f = 0; f < nFrames; f++ ) - { - // construct - vObjs = Vec_VecEntryInt( vFrameObjs, f ); - Aig_ManForEachObjVec( vObjs, pAig, pObj, i ) - { - if ( Aig_ObjIsNode(pObj) ) - pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - else if ( Aig_ObjIsCo(pObj) ) - pObj->pData = Aig_ObjChild0Copy(pObj); - else if ( Saig_ObjIsPi(pAig, pObj) ) - { - Vec_IntWriteEntry( *pvPiVarMap, f * Saig_ManPiNum(pAig) + Aig_ObjCioId(pObj), Aig_ManCiNum(pFrames) ); - pObj->pData = Aig_ObjCreateCi( pFrames ); - } - else if ( Aig_ObjIsConst1(pObj) ) - pObj->pData = Aig_ManConst1(pFrames); - else if ( !Saig_ObjIsLo(pAig, pObj) ) - assert( 0 ); - } - // create output - if ( f >= nStart ) - { - Saig_ManForEachPo( pAig, pObj, i ) - pObjNew = Aig_Or( pFrames, pObjNew, (Aig_Obj_t *)pObj->pData ); - } - // transfer - if ( f == nFrames - 1 ) - break; - vRoots = Vec_VecEntryInt( vFrameCos, f ); - Aig_ManForEachObjVec( vRoots, pAig, pObj, i ) - { - if ( Saig_ObjIsLi(pAig, pObj) ) - { - int iFlopNum = Aig_ObjCioId(pObj) - Saig_ManPoNum(pAig); - assert( iFlopNum >= 0 && iFlopNum < Aig_ManRegNum(pAig) ); - Saig_ObjLiToLo(pAig, pObj)->pData = Aig_Mux( pFrames, Aig_ManCi(pFrames,iFlopNum), Aig_ObjCreateCi(pFrames), (Aig_Obj_t *)pObj->pData ); - } - } - } - // cleanup - Vec_VecFree( vFrameCos ); - Vec_VecFree( vFrameObjs ); - // create output - Aig_ObjCreateCo( pFrames, pObjNew ); - Aig_ManSetRegNum( pFrames, 0 ); - // finallize - Aig_ManCleanup( pFrames ); - return pFrames; -} - -/**Function************************************************************* - - Synopsis [Derives the counter-example from the SAT solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Saig_ManPbaDeriveCex( Aig_Man_t * pAig, sat_solver * pSat, Cnf_Dat_t * pCnf, int nFrames, Vec_Int_t * vPiVarMap ) -{ - Abc_Cex_t * pCex; - Aig_Obj_t * pObj, * pObjRi, * pObjRo; - int i, f, Entry, iBit = 0; - pCex = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames ); - pCex->iPo = -1; - pCex->iFrame = -1; - Vec_IntForEachEntry( vPiVarMap, Entry, i ) - { - if ( Entry >= 0 ) - { - int iSatVar = pCnf->pVarNums[ Aig_ObjId(Aig_ManCi(pCnf->pMan, Entry)) ]; - if ( sat_solver_var_value( pSat, iSatVar ) ) - Abc_InfoSetBit( pCex->pData, Aig_ManRegNum(pAig) + i ); - } - } - // check what frame has failed - Aig_ManCleanMarkB(pAig); - Aig_ManConst1(pAig)->fMarkB = 1; - Saig_ManForEachLo( pAig, pObj, i ) - pObj->fMarkB = Abc_InfoHasBit(pCex->pData, iBit++); - for ( f = 0; f < nFrames; f++ ) - { - // compute new state - Saig_ManForEachPi( pAig, pObj, i ) - pObj->fMarkB = Abc_InfoHasBit(pCex->pData, iBit++); - Aig_ManForEachNode( pAig, pObj, i ) - pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & - (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj)); - Aig_ManForEachCo( pAig, pObj, i ) - pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj); - Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, i ) - pObjRo->fMarkB = pObjRi->fMarkB; - // check the outputs - Saig_ManForEachPo( pAig, pObj, i ) - { - if ( pObj->fMarkB ) - { - pCex->iPo = i; - pCex->iFrame = f; - pCex->nBits = pCex->nRegs + pCex->nPis * (f+1); - break; - } - } - if ( i < Saig_ManPoNum(pAig) ) - break; - } - Aig_ManCleanMarkB(pAig); - if ( f == nFrames ) - { - Abc_Print( -1, "Saig_ManPbaDeriveCex(): Internal error! Cannot find a failed primary outputs.\n" ); - Abc_CexFree( pCex ); - pCex = NULL; - } - if ( !Saig_ManVerifyCex( pAig, pCex ) ) - { - Abc_Print( -1, "Saig_ManPbaDeriveCex(): Internal error! Counter-example is invalid.\n" ); - Abc_CexFree( pCex ); - pCex = NULL; - } - return pCex; -} - -/**Function************************************************************* - - Synopsis [Derive unrolled timeframes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nFrames, int nConfLimit, int TimeLimit, int fVerbose, int * piFrame ) -{ - Vec_Int_t * vFlops = NULL, * vMapVar2FF, * vAssumps, * vPiVarMap; - Aig_Man_t * pFrames; - sat_solver * pSat; - Cnf_Dat_t * pCnf; - Aig_Obj_t * pObj; - int nCoreLits, * pCoreLits; - int i, iVar, RetValue; - clock_t clk; -if ( fVerbose ) -{ -if ( TimeLimit ) - printf( "Abstracting from frame %d to frame %d with timeout %d sec.\n", nStart, nFrames, TimeLimit ); -else - printf( "Abstracting from frame %d to frame %d with no timeout.\n", nStart, nFrames ); -} - // create SAT solver -clk = clock(); - pFrames = Saig_ManUnrollForPba( pAig, nStart, nFrames, &vPiVarMap ); -if ( fVerbose ) -Aig_ManPrintStats( pFrames ); -// pCnf = Cnf_DeriveSimple( pFrames, 0 ); -// pCnf = Cnf_Derive( pFrames, 0 ); - pCnf = Cnf_DeriveFast( pFrames, 0 ); - pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); - if ( pSat == NULL ) - { - Aig_ManStop( pFrames ); - Cnf_DataFree( pCnf ); - return NULL; - } -if ( fVerbose ) -Abc_PrintTime( 1, "Preparing", clock() - clk ); - - // map activation variables into flop numbers - vAssumps = Vec_IntAlloc( Aig_ManRegNum(pAig) ); - vMapVar2FF = Vec_IntStartFull( pCnf->nVars ); - Aig_ManForEachCi( pFrames, pObj, i ) - { - if ( i >= Aig_ManRegNum(pAig) ) - break; - iVar = pCnf->pVarNums[Aig_ObjId(pObj)]; - Vec_IntPush( vAssumps, toLitCond(iVar, 1) ); - Vec_IntWriteEntry( vMapVar2FF, iVar, i ); - } - - // set runtime limit - if ( TimeLimit ) - sat_solver_set_runtime_limit( pSat, TimeLimit ? TimeLimit * CLOCKS_PER_SEC + clock(): 0 ); - - // run SAT solver -clk = clock(); - RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), - (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); -if ( fVerbose ) -Abc_PrintTime( 1, "Solving", clock() - clk ); - if ( RetValue != l_False ) - { - if ( RetValue == l_True ) - { - Vec_Int_t * vAbsFfsToAdd; - ABC_FREE( pAig->pSeqModel ); - pAig->pSeqModel = Saig_ManPbaDeriveCex( pAig, pSat, pCnf, nFrames, vPiVarMap ); - printf( "The problem is SAT in frame %d. Performing CEX-based refinement.\n", pAig->pSeqModel->iFrame ); - *piFrame = pAig->pSeqModel->iFrame; - // CEX is detected - refine the flops - vAbsFfsToAdd = Saig_ManCbaFilterInputs( pAig, nInputs, pAig->pSeqModel, fVerbose ); - if ( Vec_IntSize(vAbsFfsToAdd) == 0 ) - { - Vec_IntFree( vAbsFfsToAdd ); - goto finish; - } - if ( fVerbose ) - { - printf( "Adding %d registers to the abstraction (total = %d). ", Vec_IntSize(vAbsFfsToAdd), Aig_ManRegNum(pAig)+Vec_IntSize(vAbsFfsToAdd) ); - Abc_PrintTime( 1, "Time", clock() - clk ); - } - vFlops = vAbsFfsToAdd; - } - else - { - printf( "Saig_ManPerformPba(): SAT solver timed out. Current abstraction is not changed.\n" ); - } - goto finish; - } - assert( RetValue == l_False ); // UNSAT - *piFrame = nFrames; - - // get relevant SAT literals - nCoreLits = sat_solver_final( pSat, &pCoreLits ); - assert( nCoreLits > 0 ); - if ( fVerbose ) - printf( "AnalizeFinal after %d frames selected %d assumptions (out of %d). Conflicts = %d.\n", - nFrames, nCoreLits, Vec_IntSize(vAssumps), (int)pSat->stats.conflicts ); - - // collect flops - vFlops = Vec_IntAlloc( nCoreLits ); - for ( i = 0; i < nCoreLits; i++ ) - { - iVar = Vec_IntEntry( vMapVar2FF, lit_var(pCoreLits[i]) ); - assert( iVar >= 0 && iVar < Aig_ManRegNum(pAig) ); - Vec_IntPush( vFlops, iVar ); - } - Vec_IntSort( vFlops, 0 ); - - // cleanup -finish: - Vec_IntFree( vPiVarMap ); - Vec_IntFree( vAssumps ); - Vec_IntFree( vMapVar2FF ); - sat_solver_delete( pSat ); - Cnf_DataFree( pCnf ); - Aig_ManStop( pFrames ); - return vFlops; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/aig/saig/saigAbsVfa.c b/src/aig/saig/saigAbsVfa.c deleted file mode 100644 index 2c3ebbff..00000000 --- a/src/aig/saig/saigAbsVfa.c +++ /dev/null @@ -1,329 +0,0 @@ -/**CFile**************************************************************** - - FileName [saigAbsVfa.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Sequential AIG package.] - - Synopsis [Intergrated abstraction procedure.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: saigAbsVfa.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "saig.h" -#include "sat/cnf/cnf.h" -#include "sat/bsat/satSolver.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Abs_VfaMan_t_ Abs_VfaMan_t; -struct Abs_VfaMan_t_ -{ - Aig_Man_t * pAig; - int nConfLimit; - int fVerbose; - // unrolling info - int iFrame; - int nFrames; - Vec_Int_t * vObj2Vec; // maps obj ID into its vec ID - Vec_Int_t * vVec2Var; // maps vec ID into its sat Var (nFrames per vec ID) - Vec_Int_t * vVar2Inf; // maps sat Var into its frame and obj ID - Vec_Int_t * vFra2Var; // maps frame number into the first variable - // SAT solver - sat_solver * pSat; - Cnf_Dat_t * pCnf; - Vec_Int_t * vAssumps; - Vec_Int_t * vCore; -}; - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Adds CNF clauses for the MUX.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abs_VfaManSatMux( sat_solver * pSat, int VarF, int VarI, int VarT, int VarE ) -{ - int RetValue, pLits[3]; - - // f = ITE(i, t, e) - - // i' + t' + f - // i' + t + f' - // i + e' + f - // i + e + f' - - // create four clauses - pLits[0] = toLitCond(VarI, 1); - pLits[1] = toLitCond(VarT, 1); - pLits[2] = toLitCond(VarF, 0); - RetValue = sat_solver_addclause( pSat, pLits, pLits + 3 ); - assert( RetValue ); - - pLits[0] = toLitCond(VarI, 1); - pLits[1] = toLitCond(VarT, 0); - pLits[2] = toLitCond(VarF, 1); - RetValue = sat_solver_addclause( pSat, pLits, pLits + 3 ); - assert( RetValue ); - - pLits[0] = toLitCond(VarI, 0); - pLits[1] = toLitCond(VarE, 1); - pLits[2] = toLitCond(VarF, 0); - RetValue = sat_solver_addclause( pSat, pLits, pLits + 3 ); - assert( RetValue ); - - pLits[0] = toLitCond(VarI, 0); - pLits[1] = toLitCond(VarE, 0); - pLits[2] = toLitCond(VarF, 1); - RetValue = sat_solver_addclause( pSat, pLits, pLits + 3 ); - assert( RetValue ); - - // two additional clauses - // t' & e' -> f' - // t & e -> f - - // t + e + f' - // t' + e' + f - assert( VarT != VarE ); - - pLits[0] = toLitCond(VarT, 0); - pLits[1] = toLitCond(VarE, 0); - pLits[2] = toLitCond(VarF, 1); - RetValue = sat_solver_addclause( pSat, pLits, pLits + 3 ); - assert( RetValue ); - - pLits[0] = toLitCond(VarT, 1); - pLits[1] = toLitCond(VarE, 1); - pLits[2] = toLitCond(VarF, 0); - RetValue = sat_solver_addclause( pSat, pLits, pLits + 3 ); - assert( RetValue ); -} - - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abs_VfaManAddVar( Abs_VfaMan_t * p, Aig_Obj_t * pObj, int f, int * pfNew ) -{ - int i, SatId, VecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) ); - *pfNew = 0; - if ( VecId == -1 ) - return -1; - if ( VecId == 0 ) - { - VecId = Vec_IntSize( p->vVec2Var ) / p->nFrames; - for ( i = 0; i < p->nFrames; i++ ) - Vec_IntPush( p->vVec2Var, 0 ); - Vec_IntWriteEntry( p->vObj2Vec, Aig_ObjId(pObj), VecId ); - } - SatId = Vec_IntEntry( p->vVec2Var, p->nFrames * VecId + f ); - if ( SatId ) - return SatId; - SatId = Vec_IntSize( p->vVar2Inf ) / 2; - // save SatId - Vec_IntWriteEntry( p->vVec2Var, p->nFrames * VecId + f, SatId ); - Vec_IntPush( p->vVar2Inf, Aig_ObjId(pObj) ); - Vec_IntPush( p->vVar2Inf, f ); - if ( Saig_ObjIsLo( p->pAig, pObj ) ) // reserve IDs for aux vars - { - Vec_IntPush( p->vVar2Inf, -1 ); - Vec_IntPush( p->vVar2Inf, f ); - Vec_IntPush( p->vVar2Inf, -2 ); - Vec_IntPush( p->vVar2Inf, f ); - } - *pfNew = 1; - return SatId; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abs_VfaManCreateFrame_rec( Abs_VfaMan_t * p, Aig_Obj_t * pObj, int f ) -{ - int SatVar, fNew; - if ( Aig_ObjIsConst1(pObj) ) - return -1; - SatVar = Abs_VfaManAddVar( p, pObj, f, &fNew ); - if ( (SatVar > 0 && !fNew) || Saig_ObjIsPi(p->pAig, pObj) || (Aig_ObjIsCi(pObj) && f==0) ) - return SatVar; - if ( Aig_ObjIsCo(pObj) ) - return Abs_VfaManCreateFrame_rec( p, Aig_ObjFanin0(pObj), f ); - if ( Aig_ObjIsCi(pObj) ) - return Abs_VfaManCreateFrame_rec( p, Saig_ObjLoToLi(p->pAig, pObj), f-1 ); - assert( Aig_ObjIsAnd(pObj) ); - Abs_VfaManCreateFrame_rec( p, Aig_ObjFanin0(pObj), f ); - Abs_VfaManCreateFrame_rec( p, Aig_ObjFanin1(pObj), f ); - return SatVar; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abs_VfaManCreateFrame( Abs_VfaMan_t * p, int f ) -{ - Aig_Obj_t * pObj; - int i; - clock_t clk = clock(); - - Saig_ManForEachPo( p->pAig, pObj, i ) - Abs_VfaManCreateFrame_rec( p, pObj, f ); - - Vec_IntPush( p->vFra2Var, Vec_IntSize( p->vVar2Inf ) / 2 ); - - printf( "Frame = %3d : ", f ); - printf( "Vecs = %8d ", Vec_IntSize( p->vVec2Var ) / p->nFrames ); - printf( "Vars = %8d ", Vec_IntSize( p->vVar2Inf ) / 2 ); - Abc_PrintTime( 1, "Time", clock() - clk ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abs_VfaMan_t * Abs_VfaManStart( Aig_Man_t * pAig ) -{ - Abs_VfaMan_t * p; - int i; - - p = ABC_CALLOC( Abs_VfaMan_t, 1 ); - p->pAig = pAig; - p->vObj2Vec = Vec_IntStart( Aig_ManObjNumMax(pAig) ); - p->vVec2Var = Vec_IntAlloc( 1 << 20 ); - p->vVar2Inf = Vec_IntAlloc( 1 << 20 ); - p->vFra2Var = Vec_IntStart( 1 ); - - // skip the first variable - Vec_IntPush( p->vVar2Inf, -3 ); - Vec_IntPush( p->vVar2Inf, -3 ); - for ( i = 0; i < p->nFrames; i++ ) - Vec_IntPush( p->vVec2Var, -1 ); - - // transfer values from CNF - p->pCnf = Cnf_DeriveOther( pAig, 0 ); - for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ ) - if ( p->pCnf->pObj2Clause[i] == -1 ) - Vec_IntWriteEntry( p->vObj2Vec, i, -1 ); - - p->vAssumps = Vec_IntAlloc( 100 ); - p->vCore = Vec_IntAlloc( 100 ); - return p; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abs_VfaManStop( Abs_VfaMan_t * p ) -{ - Vec_IntFreeP( &p->vObj2Vec ); - Vec_IntFreeP( &p->vVec2Var ); - Vec_IntFreeP( &p->vVar2Inf ); - Vec_IntFreeP( &p->vFra2Var ); - Vec_IntFreeP( &p->vAssumps ); - Vec_IntFreeP( &p->vCore ); - if ( p->pCnf ) - Cnf_DataFree( p->pCnf ); - if ( p->pSat ) - sat_solver_delete( p->pSat ); - ABC_FREE( p ); -} - -/**Function************************************************************* - - Synopsis [Perform variable frame abstraction.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abs_VfaManTest( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fVerbose ) -{ - Abs_VfaMan_t * p; - int i; - - p = Abs_VfaManStart( pAig ); - p->nFrames = nFrames; - p->nConfLimit = nConfLimit; - p->fVerbose = fVerbose; - - - // create unrolling for the given number of frames - for ( i = 0; i < p->nFrames; i++ ) - Abs_VfaManCreateFrame( p, i ); - - - Abs_VfaManStop( p ); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/aig/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c deleted file mode 100644 index 1a5ec7e5..00000000 --- a/src/aig/saig/saigSimExt.c +++ /dev/null @@ -1,556 +0,0 @@ -/**CFile**************************************************************** - - FileName [saigSimExt.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Sequential AIG package.] - - Synopsis [Extending simulation trace to contain ternary values.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: saigSimExt.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "saig.h" -#include "proof/ssw/ssw.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static inline int Saig_ManSimInfoNot( int Value ) -{ - if ( Value == SAIG_ZER ) - return SAIG_ONE; - if ( Value == SAIG_ONE ) - return SAIG_ZER; - return SAIG_UND; -} - -static inline int Saig_ManSimInfoAnd( int Value0, int Value1 ) -{ - if ( Value0 == SAIG_ZER || Value1 == SAIG_ZER ) - return SAIG_ZER; - if ( Value0 == SAIG_ONE && Value1 == SAIG_ONE ) - return SAIG_ONE; - return SAIG_UND; -} - -static inline int Saig_ManSimInfoGet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame ) -{ - unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) ); - return 3 & (pInfo[iFrame >> 4] >> ((iFrame & 15) << 1)); -} - -static inline void Saig_ManSimInfoSet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame, int Value ) -{ - unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) ); - assert( Value >= SAIG_ZER && Value <= SAIG_UND ); - Value ^= Saig_ManSimInfoGet( vSimInfo, pObj, iFrame ); - pInfo[iFrame >> 4] ^= (Value << ((iFrame & 15) << 1)); -} - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Performs ternary simulation for one node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Saig_ManExtendOneEval( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame ) -{ - int Value0, Value1, Value; - Value0 = Saig_ManSimInfoGet( vSimInfo, Aig_ObjFanin0(pObj), iFrame ); - if ( Aig_ObjFaninC0(pObj) ) - Value0 = Saig_ManSimInfoNot( Value0 ); - if ( Aig_ObjIsCo(pObj) ) - { - Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value0 ); - return Value0; - } - assert( Aig_ObjIsNode(pObj) ); - Value1 = Saig_ManSimInfoGet( vSimInfo, Aig_ObjFanin1(pObj), iFrame ); - if ( Aig_ObjFaninC1(pObj) ) - Value1 = Saig_ManSimInfoNot( Value1 ); - Value = Saig_ManSimInfoAnd( Value0, Value1 ); - Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value ); - return Value; -} - -/**Function************************************************************* - - Synopsis [Performs ternary simulation for one design.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes ) -{ - Aig_Obj_t * pObj, * pObjLi, * pObjLo; - int i, f, Entry, iBit = 0; - Saig_ManForEachLo( p, pObj, i ) - Saig_ManSimInfoSet( vSimInfo, pObj, 0, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER ); - for ( f = 0; f <= pCex->iFrame; f++ ) - { - Saig_ManSimInfoSet( vSimInfo, Aig_ManConst1(p), f, SAIG_ONE ); - Saig_ManForEachPi( p, pObj, i ) - Saig_ManSimInfoSet( vSimInfo, pObj, f, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER ); - if ( vRes ) - Vec_IntForEachEntry( vRes, Entry, i ) - Saig_ManSimInfoSet( vSimInfo, Aig_ManCi(p, Entry), f, SAIG_UND ); - Aig_ManForEachNode( p, pObj, i ) - Saig_ManExtendOneEval( vSimInfo, pObj, f ); - Aig_ManForEachCo( p, pObj, i ) - Saig_ManExtendOneEval( vSimInfo, pObj, f ); - if ( f == pCex->iFrame ) - break; - Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) - Saig_ManSimInfoSet( vSimInfo, pObjLo, f+1, Saig_ManSimInfoGet(vSimInfo, pObjLi, f) ); - } - // make sure the output of the property failed - pObj = Aig_ManCo( p, pCex->iPo ); - return Saig_ManSimInfoGet( vSimInfo, pObj, pCex->iFrame ); -} - -/**Function************************************************************* - - Synopsis [Tries to assign ternary value to one of the primary inputs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Saig_ManExtendOne( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, - int iPi, int iFrame, Vec_Int_t * vUndo, Vec_Int_t * vVis, Vec_Int_t * vVis2 ) -{ - Aig_Obj_t * pFanout, * pObj = Aig_ManCi(p, iPi); - int i, k, f, iFanout = -1, Value, Value2, Entry; - // save original value - Value = Saig_ManSimInfoGet( vSimInfo, pObj, iFrame ); - assert( Value == SAIG_ZER || Value == SAIG_ONE ); - Vec_IntPush( vUndo, Aig_ObjId(pObj) ); - Vec_IntPush( vUndo, iFrame ); - Vec_IntPush( vUndo, Value ); - // update original value - Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, SAIG_UND ); - // traverse - Vec_IntClear( vVis ); - Vec_IntPush( vVis, Aig_ObjId(pObj) ); - for ( f = iFrame; f <= pCex->iFrame; f++ ) - { - Vec_IntClear( vVis2 ); - Vec_IntForEachEntry( vVis, Entry, i ) - { - pObj = Aig_ManObj( p, Entry ); - Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, k ) - { - assert( Aig_ObjId(pObj) < Aig_ObjId(pFanout) ); - Value = Saig_ManSimInfoGet( vSimInfo, pFanout, f ); - if ( Value == SAIG_UND ) - continue; - Value2 = Saig_ManExtendOneEval( vSimInfo, pFanout, f ); - if ( Value2 == Value ) - continue; - assert( Value2 == SAIG_UND ); -// assert( Vec_IntFind(vVis, Aig_ObjId(pFanout)) == -1 ); - if ( Aig_ObjIsNode(pFanout) ) - Vec_IntPushOrder( vVis, Aig_ObjId(pFanout) ); - else if ( Saig_ObjIsLi(p, pFanout) ) - Vec_IntPush( vVis2, Aig_ObjId(pFanout) ); - Vec_IntPush( vUndo, Aig_ObjId(pFanout) ); - Vec_IntPush( vUndo, f ); - Vec_IntPush( vUndo, Value ); - } - } - if ( Vec_IntSize(vVis2) == 0 ) - break; - if ( f == pCex->iFrame ) - break; - // transfer - Vec_IntClear( vVis ); - Vec_IntForEachEntry( vVis2, Entry, i ) - { - pObj = Aig_ManObj( p, Entry ); - assert( Saig_ObjIsLi(p, pObj) ); - pFanout = Saig_ObjLiToLo( p, pObj ); - Vec_IntPushOrder( vVis, Aig_ObjId(pFanout) ); - Value = Saig_ManSimInfoGet( vSimInfo, pObj, f ); - Saig_ManSimInfoSet( vSimInfo, pFanout, f+1, Value ); - } - } - // check the output - pObj = Aig_ManCo( p, pCex->iPo ); - Value = Saig_ManSimInfoGet( vSimInfo, pObj, pCex->iFrame ); - assert( Value == SAIG_ONE || Value == SAIG_UND ); - return (int)(Value == SAIG_ONE); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Saig_ManExtendUndo( Aig_Man_t * p, Vec_Ptr_t * vSimInfo, Vec_Int_t * vUndo ) -{ - Aig_Obj_t * pObj; - int i, iFrame, Value; - for ( i = 0; i < Vec_IntSize(vUndo); i += 3 ) - { - pObj = Aig_ManObj( p, Vec_IntEntry(vUndo, i) ); - iFrame = Vec_IntEntry(vUndo, i+1); - Value = Vec_IntEntry(vUndo, i+2); - assert( Saig_ManSimInfoGet(vSimInfo, pObj, iFrame) == SAIG_UND ); - Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value ); - } -} - -/**Function************************************************************* - - Synopsis [Returns the array of PIs for flops that should not be absracted.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_ManExtendCounterExample0( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ) -{ - Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2; - int i, f, Value; -// assert( Aig_ManRegNum(p) > 0 ); - assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Abc_BitWordNum(2*(pCex->iFrame+1)) ); - // start simulation data - Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL ); - assert( Value == SAIG_ONE ); - // select the result - vRes = Vec_IntAlloc( 1000 ); - vResInv = Vec_IntAlloc( 1000 ); - vVis = Vec_IntAlloc( 1000 ); - vVis2 = Vec_IntAlloc( 1000 ); - vUndo = Vec_IntAlloc( 1000 ); - for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ ) - { - Vec_IntClear( vUndo ); - for ( f = pCex->iFrame; f >= 0; f-- ) - if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) ) - { - Saig_ManExtendUndo( p, vSimInfo, vUndo ); - break; - } - if ( f >= 0 ) - Vec_IntPush( vRes, i ); - else - Vec_IntPush( vResInv, i ); - } - Vec_IntFree( vVis ); - Vec_IntFree( vVis2 ); - Vec_IntFree( vUndo ); - // resimulate to make sure it is valid - Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv ); - assert( Value == SAIG_ONE ); - Vec_IntFree( vResInv ); - return vRes; -} - -/**Function************************************************************* - - Synopsis [Returns the array of PIs for flops that should not be absracted.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_ManExtendCounterExample1( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ) -{ - Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2; - int i, f, Value; -// assert( Aig_ManRegNum(p) > 0 ); - assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Abc_BitWordNum(2*(pCex->iFrame+1)) ); - // start simulation data - Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL ); - assert( Value == SAIG_ONE ); - // select the result - vRes = Vec_IntAlloc( 1000 ); - vResInv = Vec_IntAlloc( 1000 ); - vVis = Vec_IntAlloc( 1000 ); - vVis2 = Vec_IntAlloc( 1000 ); - vUndo = Vec_IntAlloc( 1000 ); - for ( i = Saig_ManPiNum(p) - 1; i >= iFirstFlopPi; i-- ) - { - Vec_IntClear( vUndo ); - for ( f = pCex->iFrame; f >= 0; f-- ) - if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) ) - { - Saig_ManExtendUndo( p, vSimInfo, vUndo ); - break; - } - if ( f >= 0 ) - Vec_IntPush( vRes, i ); - else - Vec_IntPush( vResInv, i ); - } - Vec_IntFree( vVis ); - Vec_IntFree( vVis2 ); - Vec_IntFree( vUndo ); - // resimulate to make sure it is valid - Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv ); - assert( Value == SAIG_ONE ); - Vec_IntFree( vResInv ); - return vRes; -} - -/**Function************************************************************* - - Synopsis [Returns the array of PIs for flops that should not be absracted.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_ManExtendCounterExample2( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ) -{ - Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2; - int i, f, Value; -// assert( Aig_ManRegNum(p) > 0 ); - assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Abc_BitWordNum(2*(pCex->iFrame+1)) ); - // start simulation data - Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL ); - assert( Value == SAIG_ONE ); - // select the result - vRes = Vec_IntAlloc( 1000 ); - vResInv = Vec_IntAlloc( 1000 ); - vVis = Vec_IntAlloc( 1000 ); - vVis2 = Vec_IntAlloc( 1000 ); - vUndo = Vec_IntAlloc( 1000 ); - for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ ) - { - if ( i % 2 == 0 ) - continue; - Vec_IntClear( vUndo ); - for ( f = pCex->iFrame; f >= 0; f-- ) - if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) ) - { - Saig_ManExtendUndo( p, vSimInfo, vUndo ); - break; - } - if ( f >= 0 ) - Vec_IntPush( vRes, i ); - else - Vec_IntPush( vResInv, i ); - } - for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ ) - { - if ( i % 2 == 1 ) - continue; - Vec_IntClear( vUndo ); - for ( f = pCex->iFrame; f >= 0; f-- ) - if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) ) - { - Saig_ManExtendUndo( p, vSimInfo, vUndo ); - break; - } - if ( f >= 0 ) - Vec_IntPush( vRes, i ); - else - Vec_IntPush( vResInv, i ); - } - Vec_IntFree( vVis ); - Vec_IntFree( vVis2 ); - Vec_IntFree( vUndo ); - // resimulate to make sure it is valid - Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv ); - assert( Value == SAIG_ONE ); - Vec_IntFree( vResInv ); - return vRes; -} - -/**Function************************************************************* - - Synopsis [Returns the array of PIs for flops that should not be absracted.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_ManExtendCounterExample3( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ) -{ - Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2; - int i, f, Value; -// assert( Aig_ManRegNum(p) > 0 ); - assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Abc_BitWordNum(2*(pCex->iFrame+1)) ); - // start simulation data - Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL ); - assert( Value == SAIG_ONE ); - // select the result - vRes = Vec_IntAlloc( 1000 ); - vResInv = Vec_IntAlloc( 1000 ); - vVis = Vec_IntAlloc( 1000 ); - vVis2 = Vec_IntAlloc( 1000 ); - vUndo = Vec_IntAlloc( 1000 ); - for ( i = Saig_ManPiNum(p) - 1; i >= iFirstFlopPi; i-- ) - { - if ( i % 2 == 0 ) - continue; - Vec_IntClear( vUndo ); - for ( f = pCex->iFrame; f >= 0; f-- ) - if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) ) - { - Saig_ManExtendUndo( p, vSimInfo, vUndo ); - break; - } - if ( f >= 0 ) - Vec_IntPush( vRes, i ); - else - Vec_IntPush( vResInv, i ); - } - for ( i = Saig_ManPiNum(p) - 1; i >= iFirstFlopPi; i-- ) - { - if ( i % 2 == 1 ) - continue; - Vec_IntClear( vUndo ); - for ( f = pCex->iFrame; f >= 0; f-- ) - if ( !Saig_ManExtendOne( p, pCex, vSimInfo, i, f, vUndo, vVis, vVis2 ) ) - { - Saig_ManExtendUndo( p, vSimInfo, vUndo ); - break; - } - if ( f >= 0 ) - Vec_IntPush( vRes, i ); - else - Vec_IntPush( vResInv, i ); - } - Vec_IntFree( vVis ); - Vec_IntFree( vVis2 ); - Vec_IntFree( vUndo ); - // resimulate to make sure it is valid - Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv ); - assert( Value == SAIG_ONE ); - Vec_IntFree( vResInv ); - return vRes; -} - -/**Function************************************************************* - - Synopsis [Returns the array of PIs for flops that should not be absracted.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ) -{ - Vec_Int_t * vRes0 = Saig_ManExtendCounterExample0( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); - Vec_Int_t * vRes1 = Saig_ManExtendCounterExample1( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); - Vec_Int_t * vRes2 = Saig_ManExtendCounterExample2( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); - Vec_Int_t * vRes3 = Saig_ManExtendCounterExample3( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); - Vec_Int_t * vRes = vRes0; -// if ( fVerbose ) - printf( "Removable flops: Order0 =%3d. Order1 =%3d. Order2 =%3d. Order3 =%3d.\n", - Vec_IntSize(vRes0), Vec_IntSize(vRes1), Vec_IntSize(vRes2), Vec_IntSize(vRes3) ); - if ( Vec_IntSize(vRes1) < Vec_IntSize(vRes) ) - vRes = vRes1; - if ( Vec_IntSize(vRes2) < Vec_IntSize(vRes) ) - vRes = vRes2; - if ( Vec_IntSize(vRes3) < Vec_IntSize(vRes) ) - vRes = vRes3; - vRes = Vec_IntDup( vRes ); - Vec_IntFree( vRes0 ); - Vec_IntFree( vRes1 ); - Vec_IntFree( vRes2 ); - Vec_IntFree( vRes3 ); - return vRes; -} - -/**Function************************************************************* - - Synopsis [Returns the array of PIs for flops that should not be absracted.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, int fTryFour, int fVerbose ) -{ - Vec_Int_t * vRes; - Vec_Ptr_t * vSimInfo; - clock_t clk; - if ( Saig_ManPiNum(p) != pCex->nPis ) - { - printf( "Saig_ManExtendCounterExampleTest(): The PI count of AIG (%d) does not match that of cex (%d).\n", - Aig_ManCiNum(p), pCex->nPis ); - return NULL; - } - Aig_ManFanoutStart( p ); - vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Abc_BitWordNum(2*(pCex->iFrame+1)) ); - Vec_PtrCleanSimInfo( vSimInfo, 0, Abc_BitWordNum(2*(pCex->iFrame+1)) ); - -clk = clock(); - if ( fTryFour ) - vRes = Saig_ManExtendCounterExample( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); - else - vRes = Saig_ManExtendCounterExample0( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); - if ( fVerbose ) - { - printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) ); -ABC_PRT( "Time", clock() - clk ); - } - Vec_PtrFree( vSimInfo ); - Aig_ManFanoutStop( p ); - return vRes; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 1ecab451..7ea474f7 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -49,6 +49,7 @@ #include "proof/bbr/bbr.h" #include "map/cov/cov.h" #include "base/cmd/cmd.h" +#include "proof/abs/abs.h" #ifdef _WIN32 //#include <io.h> @@ -350,14 +351,12 @@ static int Abc_CommandAbc9Trace ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Speedup ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Era ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Dch ( Abc_Frame_t * pAbc, int argc, char ** argv ); -//static int Abc_CommandAbc9AbsStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9AbsDerive ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9AbsRefine ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9AbsCba ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9AbsPba ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GlaDerive ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GlaRefine ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9GlaPurify ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GlaShrink ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9GlaCba ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9GlaPba ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -811,14 +810,12 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&speedup", Abc_CommandAbc9Speedup, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&era", Abc_CommandAbc9Era, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&dch", Abc_CommandAbc9Dch, 0 ); -// Cmd_CommandAdd( pAbc, "ABC9", "&abs_start", Abc_CommandAbc9AbsStart, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&abs_derive", Abc_CommandAbc9AbsDerive, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&abs_refine", Abc_CommandAbc9AbsRefine, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&abs_cba", Abc_CommandAbc9AbsCba, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&abs_pba", Abc_CommandAbc9AbsPba, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gla_derive", Abc_CommandAbc9GlaDerive, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gla_refine", Abc_CommandAbc9GlaRefine, 0 ); - Cmd_CommandAdd( pAbc, "ABC9", "&gla_purify", Abc_CommandAbc9GlaPurify, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gla_shrink", Abc_CommandAbc9GlaShrink, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&gla_cba", Abc_CommandAbc9GlaCba, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&gla_pba", Abc_CommandAbc9GlaPba, 0 ); @@ -27245,127 +27242,6 @@ usage: return 1; } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_CommandAbc9AbsStart( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - Gia_ParAbs_t Pars, * pPars = &Pars; - int c; - // set defaults - Gia_ManAbsSetDefaultParams( pPars ); - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FCRrpfvh" ) ) != EOF ) - { - switch ( c ) - { - case 'F': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nFramesBmc = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nFramesBmc < 0 ) - goto usage; - break; -/* - case 'S': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nStableMax = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nStableMax < 0 ) - goto usage; - break; -*/ - case 'C': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nConfMaxBmc = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nConfMaxBmc < 0 ) - goto usage; - break; - case 'R': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nRatio = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nRatio < 0 ) - goto usage; - break; - case 'r': - pPars->fUseBdds ^= 1; - break; - case 'p': - pPars->fUseDprove ^= 1; - break; - case 'f': - pPars->fUseStart ^= 1; - break; - case 'v': - pPars->fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; - } - } - if ( pAbc->pGia == NULL ) - { - Abc_Print( -1, "Abc_CommandAbc9AbsStart(): There is no AIG.\n" ); - return 1; - } - if ( Gia_ManRegNum(pAbc->pGia) == 0 ) - { - Abc_Print( -1, "Abc_CommandAbc9AbsStart(): The AIG is combinational.\n" ); - return 0; - } - if ( !(0 <= pPars->nRatio && pPars->nRatio <= 100) ) - { - Abc_Print( -1, "Abc_CommandAbc9AbsStart(): Wrong value of parameter \"-R <num>\".\n" ); - return 0; - } - Gia_ManCexAbstractionStart( pAbc->pGia, pPars ); - pAbc->Status = pPars->Status; - pAbc->nFrames = pPars->nFramesDone; - Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); - return 0; -usage: - Abc_Print( -2, "usage: &abs_start [-FCR num] [-rpfvh]\n" ); - Abc_Print( -2, "\t initializes flop map using cex-based abstraction\n" ); - Abc_Print( -2, "\t-F num : the max number of timeframes for BMC [default = %d]\n", pPars->nFramesBmc ); -// Abc_Print( -2, "\t-S num : the max number of stable frames for BMC [default = %d]\n", pPars->nStableMax ); - Abc_Print( -2, "\t-C num : the max number of conflicts by SAT solver for BMC [default = %d]\n", pPars->nConfMaxBmc ); - Abc_Print( -2, "\t-R num : the %% of abstracted flops when refinement stops (0<=num<=100) [default = %d]\n", pPars->nRatio ); - Abc_Print( -2, "\t-r : toggle using BDD-based reachability for filtering [default = %s]\n", pPars->fUseBdds? "yes": "no" ); -// Abc_Print( -2, "\t-p : toggle using \"dprove\" for filtering [default = %s]\n", pPars->fUseDprove? "yes": "no" ); - Abc_Print( -2, "\t-p : toggle using \"pdr\" for filtering [default = %s]\n", pPars->fUseDprove? "yes": "no" ); - Abc_Print( -2, "\t-f : toggle starting BMC from a later frame [default = %s]\n", pPars->fUseStart? "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; -} /**Function************************************************************* @@ -27504,6 +27380,8 @@ usage: return 1; } +#if 0 + /**Function************************************************************* Synopsis [] @@ -27737,6 +27615,8 @@ usage: return 1; } +#endif + /**Function************************************************************* Synopsis [] @@ -27896,78 +27776,8 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandAbc9GlaPurify( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - extern void Gia_ManGlaPurify( Gia_Man_t * p, int nPurifyRatio, int fVerbose ); - int fMinCut = 0; - int nPurifyRatio = 0; - int c, fVerbose = 0; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Rmvh" ) ) != EOF ) - { - switch ( c ) - { - case 'R': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); - goto usage; - } - nPurifyRatio = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( nPurifyRatio < 0 ) - goto usage; - break; - case 'm': - fMinCut ^= 1; - break; - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; - } - } - if ( pAbc->pGia == NULL ) - { - Abc_Print( -1, "Abc_CommandAbc9GlaPurify(): There is no AIG.\n" ); - return 1; - } - if ( pAbc->pGia->vGateClasses == NULL ) - { - Abc_Print( -1, "Abc_CommandAbc9GlaPurify(): There is no gate-level abstraction.\n" ); - return 0; - } - Gia_ManGlaPurify( pAbc->pGia, nPurifyRatio, fVerbose ); - return 0; - -usage: - Abc_Print( -2, "usage: &gla_purify [-R num] [-vh]\n" ); - Abc_Print( -2, "\t purifies gate-level abstraction by removing less frequent objects\n" ); -// Abc_Print( -2, "\t-R num : the percetage of rare objects to remove [default = %d]\n", nPurifyRatio ); - Abc_Print( -2, "\t-R num : remove objects with usage count less or equal than this [default = %d]\n", nPurifyRatio ); -// Abc_Print( -2, "\t-m : toggle using min-cut to derive the refinements [default = %s]\n", fMinCut? "yes": "no" ); - Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); - return 1; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ int Abc_CommandAbc9GlaShrink( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_IterImprove( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose ); int fUsePdr = 0; int fUseSat = 1; int fUseBdd = 0; @@ -28029,7 +27839,7 @@ int Abc_CommandAbc9GlaShrink( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9GlaShrink(): There is no gate-level abstraction.\n" ); return 0; } - Gia_IterImprove( pAbc->pGia, nFrameMax, nTimeOut, fUsePdr, fUseSat, fUseBdd, fVerbose ); + Gia_ManShrinkGla( pAbc->pGia, nFrameMax, nTimeOut, fUsePdr, fUseSat, fUseBdd, fVerbose ); return 0; usage: @@ -28045,274 +27855,6 @@ usage: return 1; } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - Saig_ParBmc_t Pars, * pPars = &Pars; - int c, fNaiveCnf = 0; - Saig_ParBmcSetDefaultParams( pPars ); - pPars->nStart = (pAbc->nFrames >= 0) ? pAbc->nFrames : 0; - pPars->nFramesMax = 0; - pPars->nConfLimit = 0; - pPars->nTimeOut = 60; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "SFCMTcvh" ) ) != EOF ) - { - switch ( c ) - { - case 'S': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nStart = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nStart < 0 ) - goto usage; - break; - case 'F': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nFramesMax = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nFramesMax < 0 ) - goto usage; - break; - case 'C': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nConfLimit = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nConfLimit < 0 ) - goto usage; - break; - case 'M': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nFfToAddMax = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nFfToAddMax < 0 ) - goto usage; - break; - case 'T': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nTimeOut = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nTimeOut < 0 ) - goto usage; - break; - case 'c': - fNaiveCnf ^= 1; - break; - case 'v': - pPars->fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; - } - } - if ( pAbc->pGia == NULL ) - { - Abc_Print( -1, "Abc_CommandAbc9AbsCba(): There is no AIG.\n" ); - return 1; - } - if ( Gia_ManRegNum(pAbc->pGia) == 0 ) - { - Abc_Print( -1, "The network is combinational.\n" ); - return 0; - } - if ( Gia_ManPoNum(pAbc->pGia) > 1 ) - { - Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" ); - return 0; - } - if ( pPars->nFramesMax < 0 ) - { - Abc_Print( 1, "The number of frames should be a positive integer.\n" ); - return 0; - } - if ( pPars->nStart > 0 && pPars->nFramesMax > 0 && pPars->nStart >= pPars->nFramesMax ) - { - Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" ); - return 0; - } - pAbc->Status = Gia_ManGlaCbaPerform( pAbc->pGia, pPars, fNaiveCnf ); -// if ( pPars->nStart == 0 ) - pAbc->nFrames = pPars->iFrame; - Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); - return 0; - -usage: - Abc_Print( -2, "usage: &gla_cba [-SFCT num] [-cvh]\n" ); - Abc_Print( -2, "\t refines abstracted object map with CEX-based abstraction\n" ); - Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nStart ); - Abc_Print( -2, "\t-F num : the max number of timeframes to unroll (0=unused) [default = %d]\n", pPars->nFramesMax ); - Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit ); -// Abc_Print( -2, "\t-M num : the max number of flops to add (0 = not used) [default = %d]\n", pPars->nFfToAddMax ); - Abc_Print( -2, "\t-T num : an approximate timeout in seconds (0=unused) [default = %d]\n", pPars->nTimeOut ); - Abc_Print( -2, "\t-c : toggle using naive CNF computation [default = %s]\n", fNaiveCnf? "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; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - Saig_ParBmc_t Pars, * pPars = &Pars; - int c; - int fNewSolver = 0; - Saig_ParBmcSetDefaultParams( pPars ); - pPars->nStart = 0; - pPars->nFramesMax = (pAbc->nFrames >= 0) ? pAbc->nFrames : 10; - pPars->nConfLimit = 0; - pPars->fSkipRand = 0; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTrnvh" ) ) != EOF ) - { - switch ( c ) - { - case 'S': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nStart = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nStart < 0 ) - goto usage; - break; - case 'F': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nFramesMax = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nFramesMax < 0 ) - goto usage; - break; - case 'C': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nConfLimit = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nConfLimit < 0 ) - goto usage; - break; - case 'T': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nTimeOut = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nTimeOut < 0 ) - goto usage; - break; - case 'r': - pPars->fSkipRand ^= 1; - break; - case 'n': - fNewSolver ^= 1; - break; - case 'v': - pPars->fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; - } - } - if ( pAbc->pGia == NULL ) - { - Abc_Print( -1, "Abc_CommandAbc9AbsCba(): There is no AIG.\n" ); - return 1; - } - if ( Gia_ManRegNum(pAbc->pGia) == 0 ) - { - Abc_Print( -1, "The network is combinational.\n" ); - return 0; - } - if ( Gia_ManPoNum(pAbc->pGia) > 1 ) - { - Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" ); - return 0; - } - if ( pPars->nFramesMax < 1 ) - { - Abc_Print( 1, "The number of frames should be a positive integer.\n" ); - return 0; - } - if ( pPars->nStart >= pPars->nFramesMax ) - { - Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" ); - return 0; - } - if ( pPars->nStart ) - Abc_Print( 0, "The starting frame is specified. The resulting abstraction may be unsound.\n" ); - pAbc->Status = Gia_ManGlaPbaPerform( pAbc->pGia, pPars, fNewSolver ); -// if ( pPars->nStart == 0 ) - pAbc->nFrames = pPars->iFrame; - Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); - return 0; - -usage: - Abc_Print( -2, "usage: &gla_pba [-SFCT num] [-rnvh]\n" ); - Abc_Print( -2, "\t refines abstracted object map with proof-based abstraction\n" ); - Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nStart ); - Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax ); - Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit ); - Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut ); - Abc_Print( -2, "\t-r : toggle using random decisiont during SAT solving [default = %s]\n", !pPars->fSkipRand? "yes": "no" ); - Abc_Print( -2, "\t-n : toggle using on-the-fly proof-logging [default = %s]\n", fNewSolver? "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; -} /**Function************************************************************* @@ -28327,9 +27869,9 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) { - Gia_ParVta_t Pars, * pPars = &Pars; + Abs_Par_t Pars, * pPars = &Pars; int c, fStartVta = 0, fNewAlgo = 1; - Gia_VtaSetDefaultParams( pPars ); + Abs_ParSetDefaults( pPars ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "FSCLDETRPBAtrfkadmnscbpqwvh" ) ) != EOF ) { @@ -28533,9 +28075,9 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } if ( fNewAlgo ) - pAbc->Status = Ga2_ManPerform( pAbc->pGia, pPars ); + pAbc->Status = Gia_ManPerformGla( pAbc->pGia, pPars ); else - pAbc->Status = Gia_GlaPerform( pAbc->pGia, pPars, fStartVta ); + pAbc->Status = Gia_ManPerformGlaOld( pAbc->pGia, pPars, fStartVta ); pAbc->nFrames = pPars->iFrame; Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); return 0; @@ -28585,9 +28127,9 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv ) { - Gia_ParVta_t Pars, * pPars = &Pars; + Abs_Par_t Pars, * pPars = &Pars; int c; - Gia_VtaSetDefaultParams( pPars ); + Abs_ParSetDefaults( pPars ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLDETRAtradvh" ) ) != EOF ) { diff --git a/src/base/io/io.c b/src/base/io/io.c index 55965642..aed809b3 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -21,6 +21,7 @@ #include "ioAbc.h" #include "base/main/mainInt.h" #include "aig/saig/saig.h" +#include "proof/abs/abs.h" ABC_NAMESPACE_IMPL_START diff --git a/src/opt/nwk/nwkAig.c b/src/opt/nwk/nwkAig.c index 55cff367..5b0aaf20 100644 --- a/src/opt/nwk/nwkAig.c +++ b/src/opt/nwk/nwkAig.c @@ -105,7 +105,7 @@ Vec_Ptr_t * Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fVerbose -#include "aig/gia/gia.h" +#include "proof/abs/abs.h" /**Function************************************************************* diff --git a/src/proof/abs/abs.c b/src/proof/abs/abs.c new file mode 100644 index 00000000..3ba1abfb --- /dev/null +++ b/src/proof/abs/abs.c @@ -0,0 +1,52 @@ +/**CFile**************************************************************** + + FileName [abs.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Abstraction package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abs.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/abs/abs.h b/src/proof/abs/abs.h new file mode 100644 index 00000000..eeeda583 --- /dev/null +++ b/src/proof/abs/abs.h @@ -0,0 +1,131 @@ +/**CFile**************************************************************** + + FileName [abs.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Abstraction package.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abs.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__proof_abs__Abs_h +#define ABC__proof_abs__Abs_h + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "aig/gia/gia.h" +#include "aig/gia/giaAig.h" +#include "aig/saig/saig.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// abstraction parameters +typedef struct Abs_Par_t_ Abs_Par_t; +struct Abs_Par_t_ +{ + int nFramesMax; // maximum frames + int nFramesStart; // starting frame + int nFramesPast; // overlap frames + int nConfLimit; // conflict limit + int nLearnedMax; // max number of learned clauses + int nLearnedStart; // max number of learned clauses + int nLearnedDelta; // delta increase of learned clauses + int nLearnedPerce; // percentage of clauses to leave + int nTimeOut; // timeout in seconds + int nRatioMin; // stop when less than this % of object is abstracted + int nRatioMax; // restart when the number of abstracted object is more than this + int fUseTermVars; // use terminal variables + int fUseRollback; // use rollback to the starting number of frames + int fPropFanout; // propagate fanout implications + int fAddLayer; // refinement strategy by adding layers + int fUseSkip; // skip proving intermediate timeframes + int fUseSimple; // use simple CNF construction + int fSkipHash; // skip hashing CNF while unrolling + int fUseFullProof; // use full proof for UNSAT cores + int fDumpVabs; // dumps the abstracted model + int fDumpMabs; // dumps the original AIG with abstraction map + int fCallProver; // calls the prover + char * pFileVabs; // dumps the abstracted model into this file + int fVerbose; // verbose flag + int fVeryVerbose; // print additional information + int iFrame; // the number of frames covered + int iFrameProved; // the number of frames proved + int nFramesNoChange; // the number of last frames without changes + int nFramesNoChangeLim; // the number of last frames without changes to dump abstraction +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== abs.c =========================================================*/ +/*=== absDup.c =========================================================*/ +extern Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses ); +extern Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses ); +extern void Gia_ManGlaCollect( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis, Vec_Int_t ** pvFlops, Vec_Int_t ** pvNodes ); +extern void Gia_ManPrintFlopClasses( Gia_Man_t * p ); +extern void Gia_ManPrintObjClasses( Gia_Man_t * p ); +extern void Gia_ManPrintGateClasses( Gia_Man_t * p ); +/*=== absGla.c =========================================================*/ +extern int Gia_ManPerformGla( Gia_Man_t * p, Abs_Par_t * pPars ); +/*=== absGlaOld.c =========================================================*/ +extern int Gia_ManPerformGlaOld( Gia_Man_t * p, Abs_Par_t * pPars, int fStartVta ); +/*=== absIter.c =========================================================*/ +extern Gia_Man_t * Gia_ManShrinkGla( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose ); +/*=== absVta.c =========================================================*/ +extern int Gia_VtaPerform( Gia_Man_t * pAig, Abs_Par_t * pPars ); +/*=== absUtil.c =========================================================*/ +extern void Abs_ParSetDefaults( Abs_Par_t * p ); +extern Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta ); +extern Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames ); +extern Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla ); +extern Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla ); +extern int Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla ); +extern int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla ); + +/*=== absOldCex.c ==========================================================*/ +extern Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect ); +extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose ); +/*=== absOldRef.c ==========================================================*/ +extern int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose ); +/*=== absOldSat.c ==========================================================*/ +extern Vec_Int_t * Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose ); +/*=== absOldSim.c ==========================================================*/ +extern Vec_Int_t * Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fVerbose ); + + +ABC_NAMESPACE_HEADER_END + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/proof/abs/absDup.c b/src/proof/abs/absDup.c new file mode 100644 index 00000000..247137bd --- /dev/null +++ b/src/proof/abs/absDup.c @@ -0,0 +1,445 @@ +/**CFile**************************************************************** + + FileName [absDup.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Abstraction package.] + + Synopsis [Duplication procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: absDup.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abs.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Duplicates the AIG manager recursively.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDupAbsFlops_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj ) +{ + if ( ~pObj->Value ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) ); + Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin1(pObj) ); + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Performs abstraction of the AIG to preserve the included flops.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, nFlops = 0; + Gia_ManFillValue( p ); + // start the new manager + pNew = Gia_ManStart( 5000 ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + // create PIs + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachPi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + // create additional PIs + Gia_ManForEachRo( p, pObj, i ) + if ( !Vec_IntEntry(vFlopClasses, i) ) + pObj->Value = Gia_ManAppendCi(pNew); + // create ROs + Gia_ManForEachRo( p, pObj, i ) + if ( Vec_IntEntry(vFlopClasses, i) ) + pObj->Value = Gia_ManAppendCi(pNew); + // create POs + Gia_ManHashAlloc( pNew ); + Gia_ManForEachPo( p, pObj, i ) + { + Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) ); + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + // create RIs + Gia_ManForEachRi( p, pObj, i ) + if ( Vec_IntEntry(vFlopClasses, i) ) + { + Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) ); + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + nFlops++; + } + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, nFlops ); + // clean up + pNew = Gia_ManSeqCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Returns the array of neighbors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses ) +{ + Vec_Int_t * vAssigned; + Gia_Obj_t * pObj; + int i, Entry; + vAssigned = Vec_IntAlloc( 1000 ); + Vec_IntForEachEntry( vGateClasses, Entry, i ) + { + if ( Entry == 0 ) + continue; + assert( Entry > 0 ); + pObj = Gia_ManObj( p, i ); + Vec_IntPush( vAssigned, Gia_ObjId(p, pObj) ); + if ( Gia_ObjIsAnd(pObj) ) + { + Vec_IntPush( vAssigned, Gia_ObjFaninId0p(p, pObj) ); + Vec_IntPush( vAssigned, Gia_ObjFaninId1p(p, pObj) ); + } + else if ( Gia_ObjIsRo(p, pObj) ) + Vec_IntPush( vAssigned, Gia_ObjFaninId0p(p, Gia_ObjRoToRi(p, pObj)) ); + else assert( Gia_ObjIsConst0(pObj) ); + } + Vec_IntUniqify( vAssigned ); + return vAssigned; +} + +/**Function************************************************************* + + Synopsis [Collects PIs and PPIs of the abstraction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManGlaCollect( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis, Vec_Int_t ** pvFlops, Vec_Int_t ** pvNodes ) +{ + Vec_Int_t * vAssigned; + Gia_Obj_t * pObj; + int i; + assert( Gia_ManPoNum(p) == 1 ); + assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) ); + // create included objects and their fanins + vAssigned = Gia_GlaCollectAssigned( p, vGateClasses ); + // create additional arrays + if ( pvPis ) *pvPis = Vec_IntAlloc( 100 ); + if ( pvPPis ) *pvPPis = Vec_IntAlloc( 100 ); + if ( pvFlops ) *pvFlops = Vec_IntAlloc( 100 ); + if ( pvNodes ) *pvNodes = Vec_IntAlloc( 1000 ); + Gia_ManForEachObjVec( vAssigned, p, pObj, i ) + { + if ( Gia_ObjIsPi(p, pObj) ) + { if ( pvPis ) Vec_IntPush( *pvPis, Gia_ObjId(p,pObj) ); } + else if ( !Vec_IntEntry(vGateClasses, Gia_ObjId(p,pObj)) ) + { if ( pvPPis ) Vec_IntPush( *pvPPis, Gia_ObjId(p,pObj) ); } + else if ( Gia_ObjIsRo(p, pObj) ) + { if ( pvFlops ) Vec_IntPush( *pvFlops, Gia_ObjId(p,pObj) ); } + else if ( Gia_ObjIsAnd(pObj) ) + { if ( pvNodes ) Vec_IntPush( *pvNodes, Gia_ObjId(p,pObj) ); } + else assert( Gia_ObjIsConst0(pObj) ); + } + Vec_IntFree( vAssigned ); +} + +/**Function************************************************************* + + Synopsis [Duplicates the AIG manager recursively.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDupAbsGates_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj ) +{ + if ( ~pObj->Value ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManDupAbsGates_rec( pNew, Gia_ObjFanin0(pObj) ); + Gia_ManDupAbsGates_rec( pNew, Gia_ObjFanin1(pObj) ); + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Performs abstraction of the AIG to preserve the included gates.] + + Description [The array contains 1 for those objects (const, RO, AND) + that are included in the abstraction; 0, otherwise.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses ) +{ + Vec_Int_t * vPis, * vPPis, * vFlops, * vNodes; + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, * pCopy; + int i;//, nFlops = 0; + assert( Gia_ManPoNum(p) == 1 ); + assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) ); + + // create additional arrays + Gia_ManGlaCollect( p, vGateClasses, &vPis, &vPPis, &vFlops, &vNodes ); + + // start the new manager + pNew = Gia_ManStart( 5000 ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + // create constant + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + // create PIs + Gia_ManForEachObjVec( vPis, p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + // create additional PIs + Gia_ManForEachObjVec( vPPis, p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + // create ROs + Gia_ManForEachObjVec( vFlops, p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + // create internal nodes + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +// Gia_ManDupAbsGates_rec( pNew, pObj ); + // create PO + Gia_ManForEachPo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + // create RIs + Gia_ManForEachObjVec( vFlops, p, pObj, i ) + Gia_ObjRoToRi(p, pObj)->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ObjRoToRi(p, pObj)) ); + Gia_ManSetRegNum( pNew, Vec_IntSize(vFlops) ); + // clean up + pNew = Gia_ManSeqCleanup( pTemp = pNew ); + // transfer copy values: (p -> pTemp -> pNew) => (p -> pNew) + if ( Gia_ManObjNum(pTemp) != Gia_ManObjNum(pNew) ) + { +// printf( "Gia_ManDupAbsGates() Internal error: object mismatch.\n" ); + Gia_ManForEachObj( p, pObj, i ) + { + if ( !~pObj->Value ) + continue; + assert( !Abc_LitIsCompl(pObj->Value) ); + pCopy = Gia_ObjCopy( pTemp, pObj ); + if ( !~pCopy->Value ) + { + Vec_IntWriteEntry( vGateClasses, i, 0 ); + pObj->Value = ~0; + continue; + } + assert( !Abc_LitIsCompl(pCopy->Value) ); + pObj->Value = pCopy->Value; + } + } + Gia_ManStop( pTemp ); + + Vec_IntFree( vPis ); + Vec_IntFree( vPPis ); + Vec_IntFree( vFlops ); + Vec_IntFree( vNodes ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Prints stats for the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManPrintFlopClasses( Gia_Man_t * p ) +{ + int Counter0, Counter1; + if ( p->vFlopClasses == NULL ) + return; + if ( Vec_IntSize(p->vFlopClasses) != Gia_ManRegNum(p) ) + { + printf( "Gia_ManPrintFlopClasses(): The number of flop map entries differs from the number of flops.\n" ); + return; + } + Counter0 = Vec_IntCountEntry( p->vFlopClasses, 0 ); + Counter1 = Vec_IntCountEntry( p->vFlopClasses, 1 ); + printf( "Flop-level abstraction: Excluded FFs = %d Included FFs = %d (%.2f %%) ", + Counter0, Counter1, 100.0*Counter1/(Counter0 + Counter1 + 1) ); + if ( Counter0 + Counter1 < Gia_ManRegNum(p) ) + printf( "and there are other FF classes..." ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Prints stats for the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManPrintGateClasses( Gia_Man_t * p ) +{ + Vec_Int_t * vPis, * vPPis, * vFlops, * vNodes; + int nTotal; + if ( p->vGateClasses == NULL ) + return; + if ( Vec_IntSize(p->vGateClasses) != Gia_ManObjNum(p) ) + { + printf( "Gia_ManPrintGateClasses(): The number of flop map entries differs from the number of flops.\n" ); + return; + } + // create additional arrays + Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, &vFlops, &vNodes ); + nTotal = 1 + Vec_IntSize(vFlops) + Vec_IntSize(vNodes); + printf( "Gate-level abstraction: PI = %d PPI = %d FF = %d (%.2f %%) AND = %d (%.2f %%) Obj = %d (%.2f %%)\n", + Vec_IntSize(vPis), Vec_IntSize(vPPis), + Vec_IntSize(vFlops), 100.0*Vec_IntSize(vFlops)/(Gia_ManRegNum(p)+1), + Vec_IntSize(vNodes), 100.0*Vec_IntSize(vNodes)/(Gia_ManAndNum(p)+1), + nTotal, 100.0*nTotal /(Gia_ManRegNum(p)+Gia_ManAndNum(p)+1) ); + Vec_IntFree( vPis ); + Vec_IntFree( vPPis ); + Vec_IntFree( vFlops ); + Vec_IntFree( vNodes ); +} + +/**Function************************************************************* + + Synopsis [Prints stats for the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManPrintObjClasses( Gia_Man_t * p ) +{ + Vec_Int_t * vSeens; // objects seen so far + Vec_Int_t * vAbs = p->vObjClasses; + int i, k, Entry, iStart, iStop = -1, nFrames; + int nObjBits, nObjMask, iObj, iFrame, nWords; + unsigned * pInfo; + int * pCountAll, * pCountUni; + if ( vAbs == NULL ) + return; + nFrames = Vec_IntEntry( vAbs, 0 ); + assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) ); + pCountAll = ABC_ALLOC( int, nFrames + 1 ); + pCountUni = ABC_ALLOC( int, nFrames + 1 ); + // start storage for seen objects + nWords = Abc_BitWordNum( nFrames ); + vSeens = Vec_IntStart( Gia_ManObjNum(p) * nWords ); + // get the bitmasks + nObjBits = Abc_Base2Log( Gia_ManObjNum(p) ); + nObjMask = (1 << nObjBits) - 1; + assert( Gia_ManObjNum(p) <= nObjMask ); + // print info about frames + printf( "Frame Core F0 F1 F2 F3 ...\n" ); + for ( i = 0; i < nFrames; i++ ) + { + iStart = Vec_IntEntry( vAbs, i+1 ); + iStop = Vec_IntEntry( vAbs, i+2 ); + memset( pCountAll, 0, sizeof(int) * (nFrames + 1) ); + memset( pCountUni, 0, sizeof(int) * (nFrames + 1) ); + Vec_IntForEachEntryStartStop( vAbs, Entry, k, iStart, iStop ) + { + iObj = (Entry & nObjMask); + iFrame = (Entry >> nObjBits); + pInfo = (unsigned *)Vec_IntEntryP( vSeens, nWords * iObj ); + if ( Abc_InfoHasBit(pInfo, iFrame) == 0 ) + { + Abc_InfoSetBit( pInfo, iFrame ); + pCountUni[iFrame+1]++; + pCountUni[0]++; + } + pCountAll[iFrame+1]++; + pCountAll[0]++; + } + assert( pCountAll[0] == (iStop - iStart) ); +// printf( "%5d%5d ", pCountAll[0], pCountUni[0] ); + printf( "%3d :", i ); + printf( "%7d", pCountAll[0] ); + if ( i >= 10 ) + { + for ( k = 0; k < 4; k++ ) + printf( "%5d", pCountAll[k+1] ); + printf( " ..." ); + for ( k = i-4; k <= i; k++ ) + printf( "%5d", pCountAll[k+1] ); + } + else + { + for ( k = 0; k <= i; k++ ) + if ( k <= i ) + printf( "%5d", pCountAll[k+1] ); + } +// for ( k = 0; k < nFrames; k++ ) +// if ( k <= i ) +// printf( "%5d", pCountAll[k+1] ); + printf( "\n" ); + } + assert( iStop == Vec_IntSize(vAbs) ); + Vec_IntFree( vSeens ); + ABC_FREE( pCountAll ); + ABC_FREE( pCountUni ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/giaAbsGla2.c b/src/proof/abs/absGla.c index ca424b44..b026c6e3 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/proof/abs/absGla.c @@ -1,10 +1,10 @@ /**CFile**************************************************************** - FileName [gia.c] + FileName [absGla2.c] SystemName [ABC: Logic synthesis and verification system.] - PackageName [Scalable AIG package.] + PackageName [Abstraction package.] Synopsis [Scalable gate-level abstraction.] @@ -14,16 +14,16 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: gia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: absGla2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ -#include "gia.h" -#include "giaAbsRef.h" -//#include "giaAbsRef2.h" #include "sat/cnf/cnf.h" #include "sat/bsat/satSolver2.h" #include "base/main/main.h" +#include "abs.h" +#include "absRef.h" +//#include "absRef2.h" ABC_NAMESPACE_IMPL_START @@ -38,7 +38,7 @@ struct Ga2_Man_t_ { // user data Gia_Man_t * pGia; // working AIG manager - Gia_ParVta_t * pPars; // parameters + Abs_Par_t * pPars; // parameters // markings Vec_Ptr_t * vCnfs; // for each object: CNF0, CNF1 // abstraction @@ -378,7 +378,7 @@ void Ga2_ManComputeTest( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) +Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Abs_Par_t * pPars ) { Ga2_Man_t * p; p = ABC_CALLOC( Ga2_Man_t, 1 ); @@ -415,7 +415,7 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) return p; } -void Ga2_ManDumpStats( Gia_Man_t * pGia, Gia_ParVta_t * pPars, sat_solver2 * pSat, int iFrame, int fUseN ) +void Ga2_ManDumpStats( Gia_Man_t * pGia, Abs_Par_t * pPars, sat_solver2 * pSat, int iFrame, int fUseN ) { FILE * pFile; char pFileName[32]; @@ -1525,7 +1525,7 @@ void Gia_Ga2SendCancel( Ga2_Man_t * p, int fVerbose ) SeeAlso [] ***********************************************************************/ -int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) +int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) { int fUseSecondCore = 1; Ga2_Man_t * p; @@ -1866,7 +1866,7 @@ finish: if ( p->pPars->fVerbose ) Abc_Print( 1, "\n" ); if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) ) - Abc_Print( 1, " Gia_GlaPerform(): CEX verification has failed!\n" ); + Abc_Print( 1, " Gia_ManPerformGlaOld(): CEX verification has failed!\n" ); Abc_Print( 1, "True counter-example detected in frame %d. ", f ); p->pPars->iFrame = f - 1; Vec_IntFreeP( &pAig->vGateClasses ); diff --git a/src/aig/gia/giaAbsGla.c b/src/proof/abs/absGlaOld.c index 0ebb8db7..5ee69739 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/proof/abs/absGlaOld.c @@ -1,10 +1,10 @@ /**CFile**************************************************************** - FileName [giaAbsGla.c] + FileName [absGla.c] SystemName [ABC: Logic synthesis and verification system.] - PackageName [Scalable AIG package.] + PackageName [Abstraction package.] Synopsis [Gate-level abstraction.] @@ -14,16 +14,15 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: giaAbsGla.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: absGla.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ -#include "gia.h" -#include "giaAig.h" -#include "giaAbsRef.h" #include "sat/cnf/cnf.h" #include "sat/bsat/satSolver2.h" #include "base/main/main.h" +#include "abs.h" +#include "absRef.h" ABC_NAMESPACE_IMPL_START @@ -65,7 +64,7 @@ struct Gla_Man_t_ // user data Gia_Man_t * pGia0; // starting AIG manager Gia_Man_t * pGia; // working AIG manager - Gia_ParVta_t* pPars; // parameters + Abs_Par_t * pPars; // parameters // internal data Vec_Int_t * vAbs; // abstracted objects Gla_Obj_t * pObjRoot; // the primary output @@ -823,7 +822,7 @@ Gia_Man_t * Gia_ManDupMapped( Gia_Man_t * p, Vec_Int_t * vMapping ) SeeAlso [] ***********************************************************************/ -Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars ) +Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Abs_Par_t * pPars ) { Gla_Man_t * p; Aig_Man_t * pAig; @@ -1000,7 +999,7 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars ) SeeAlso [] ***********************************************************************/ -Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) +Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia, Abs_Par_t * pPars ) { Gla_Man_t * p; Aig_Man_t * pAig; @@ -1637,10 +1636,10 @@ void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose ) SeeAlso [] ***********************************************************************/ -int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta ) +int Gia_ManPerformGlaOld( Gia_Man_t * pAig, Abs_Par_t * pPars, int fStartVta ) { - extern int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ); - extern void Ga2_ManDumpStats( Gia_Man_t * pGia, Gia_ParVta_t * pPars, sat_solver2 * pSat, int iFrame, int fUseN ); + extern int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars ); + extern void Ga2_ManDumpStats( Gia_Man_t * pGia, Abs_Par_t * pPars, sat_solver2 * pSat, int iFrame, int fUseN ); Gla_Man_t * p; Vec_Int_t * vPPis, * vCore;//, * vCore2 = NULL; Abc_Cex_t * pCex = NULL; @@ -1925,7 +1924,7 @@ finish: ABC_FREE( pAig->pCexSeq ); pAig->pCexSeq = pCex; if ( !Gia_ManVerifyCex( pAig, pCex, 0 ) ) - Abc_Print( 1, " Gia_GlaPerform(): CEX verification has failed!\n" ); + Abc_Print( 1, " Gia_ManPerformGlaOld(): CEX verification has failed!\n" ); Abc_Print( 1, "Counter-example detected in frame %d. ", f ); p->pPars->iFrame = pCex->iFrame - 1; Vec_IntFreeP( &pAig->vGateClasses ); diff --git a/src/aig/gia/giaAbsIter.c b/src/proof/abs/absIter.c index 42f4ed1e..88cbe39d 100644 --- a/src/aig/gia/giaAbsIter.c +++ b/src/proof/abs/absIter.c @@ -1,10 +1,10 @@ /**CFile**************************************************************** - FileName [giaIter.c] + FileName [absIter.c] SystemName [ABC: Logic synthesis and verification system.] - PackageName [Scalable AIG package.] + PackageName [Abstraction package.] Synopsis [Iterative improvement of abstraction.] @@ -14,12 +14,11 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: giaIter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: absIter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ -#include "gia.h" -#include "giaAig.h" +#include "abs.h" ABC_NAMESPACE_IMPL_START @@ -49,7 +48,6 @@ static inline void Gia_ObjRemFromGla( Gia_Man_t * p, Gia_Obj_t * pObj ) { Vec_In ***********************************************************************/ int Gia_IterTryImprove( Gia_Man_t * p, int nTimeOut, int iFrame0 ) { - extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent ); Gia_Man_t * pAbs = Gia_ManDupAbsGates( p, p->vGateClasses ); Aig_Man_t * pAig = Gia_ManToAigSimple( pAbs ); int nStart = 0; @@ -65,7 +63,7 @@ int Gia_IterTryImprove( Gia_Man_t * p, int nTimeOut, int iFrame0 ) Gia_ManStop( pAbs ); return iFrame; } -Gia_Man_t * Gia_IterImprove( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose ) +Gia_Man_t * Gia_ManShrinkGla( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose ) { Gia_Obj_t * pObj; int i, iFrame0, iFrame; diff --git a/src/aig/saig/saigAbsCba.c b/src/proof/abs/absOldCex.c index 8f2cafaa..fec6d152 100644 --- a/src/aig/saig/saigAbsCba.c +++ b/src/proof/abs/absOldCex.c @@ -18,9 +18,7 @@ ***********************************************************************/ -#include "saig.h" -#include "aig/gia/giaAig.h" -#include "aig/ioa/ioa.h" +#include "abs.h" ABC_NAMESPACE_IMPL_START @@ -582,7 +580,7 @@ void Saig_ManCbaShrink( Saig_ManCba_t * p ) } // try reducing the frames pManNew = Saig_ManDupWithCubes( p->pAig, p->vReg2Value ); - Ioa_WriteAiger( pManNew, "aigcube.aig", 0, 0 ); +// Ioa_WriteAiger( pManNew, "aigcube.aig", 0, 0 ); Aig_ManStop( pManNew ); } diff --git a/src/aig/saig/saigAbsStart.c b/src/proof/abs/absOldRef.c index 90efef26..dee28cad 100644 --- a/src/aig/saig/saigAbsStart.c +++ b/src/proof/abs/absOldRef.c @@ -18,7 +18,7 @@ ***********************************************************************/ -#include "saig.h" +#include "abs.h" #include "proof/ssw/ssw.h" #include "proof/fra/fra.h" #include "proof/bbr/bbr.h" @@ -37,6 +37,56 @@ ABC_NAMESPACE_IMPL_START /**Function************************************************************* + Synopsis [Derive a new counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexAbs ) +{ + Abc_Cex_t * pCex; + Aig_Obj_t * pObj; + int i, f; + if ( !Saig_ManVerifyCex( pAbs, pCexAbs ) ) + printf( "Saig_ManCexRemap(): The initial counter-example is invalid.\n" ); +// else +// printf( "Saig_ManCexRemap(): The initial counter-example is correct.\n" ); + // start the counter-example + pCex = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 ); + pCex->iFrame = pCexAbs->iFrame; + pCex->iPo = pCexAbs->iPo; + // copy the bit data + for ( f = 0; f <= pCexAbs->iFrame; f++ ) + { + Saig_ManForEachPi( pAbs, pObj, i ) + { + if ( i == Saig_ManPiNum(p) ) + break; + if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) ) + Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + i ); + } + } + // verify the counter example + if ( !Saig_ManVerifyCex( p, pCex ) ) + { + printf( "Saig_ManCexRemap(): Counter-example is invalid.\n" ); + Abc_CexFree( pCex ); + pCex = NULL; + } + else + { + Abc_Print( 1, "Counter-example verification is successful.\n" ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. \n", pCex->iPo, p->pName, pCex->iFrame ); + } + return pCex; +} + +/**Function************************************************************* + Synopsis [Find the first PI corresponding to the flop.] Description [] @@ -72,7 +122,6 @@ int Saig_ManCexFirstFlopPi( Aig_Man_t * p, Aig_Man_t * pAbs ) ***********************************************************************/ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fUseBdds, int fUseDprove, int fVerbose, int * pnUseStart, int * piRetValue, int * pnFrames ) { - extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent ); Vec_Int_t * vFlopsNew; int i, Entry, RetValue; *piRetValue = -1; @@ -233,71 +282,81 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vFlopC /**Function************************************************************* - Synopsis [Computes the flops to remain after abstraction.] + Synopsis [Transform flop map into flop list.] Description [] SideEffects [] SeeAlso [] - + ***********************************************************************/ -Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ) +Vec_Int_t * Gia_ManClasses2Flops( Vec_Int_t * vFlopClasses ) { - int nUseStart = 0; - Aig_Man_t * pAbs, * pTemp; Vec_Int_t * vFlops; - int Iter;//, clk = clock(), clk2 = clock();//, iFlop; - assert( Aig_ManRegNum(p) > 0 ); - if ( pPars->fVerbose ) - printf( "Performing counter-example-based refinement.\n" ); - Aig_ManSetCioIds( p ); - vFlops = Vec_IntStartNatural( 1 ); -/* - iFlop = Saig_ManFindFirstFlop( p ); - assert( iFlop >= 0 ); - vFlops = Vec_IntAlloc( 1 ); - Vec_IntPush( vFlops, iFlop ); -*/ - // create the resulting AIG - pAbs = Saig_ManDupAbstraction( p, vFlops ); - if ( !pPars->fVerbose ) + int i, Entry; + vFlops = Vec_IntAlloc( 100 ); + Vec_IntForEachEntry( vFlopClasses, Entry, i ) + if ( Entry ) + Vec_IntPush( vFlops, i ); + return vFlops; +} + +/**Function************************************************************* + + Synopsis [Transform flop list into flop map.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManFlops2Classes( Gia_Man_t * pGia, Vec_Int_t * vFlops ) +{ + Vec_Int_t * vFlopClasses; + int i, Entry; + vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) ); + Vec_IntForEachEntry( vFlops, Entry, i ) + Vec_IntWriteEntry( vFlopClasses, Entry, 1 ); + return vFlopClasses; +} + +/**Function************************************************************* + + Synopsis [Refines abstraction using the latch map.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose ) +{ + Aig_Man_t * pNew; + Vec_Int_t * vFlops; + if ( pGia->vFlopClasses == NULL ) { - printf( "Init : " ); - Aig_ManPrintStats( pAbs ); + printf( "Gia_ManCexAbstractionRefine(): Abstraction latch map is missing.\n" ); + return -1; } - printf( "Refining abstraction...\n" ); - for ( Iter = 0; ; Iter++ ) + pNew = Gia_ManToAig( pGia, 0 ); + vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses ); + if ( !Saig_ManCexRefineStep( pNew, vFlops, pGia->vFlopClasses, pCex, nFfToAddMax, fTryFour, fSensePath, fVerbose ) ) { - pTemp = Saig_ManCexRefine( p, pAbs, vFlops, pPars->nFramesBmc, pPars->nConfMaxBmc, pPars->fUseBdds, pPars->fUseDprove, pPars->fVerbose, pPars->fUseStart?&nUseStart:NULL, &pPars->Status, &pPars->nFramesDone ); - if ( pTemp == NULL ) - { - ABC_FREE( p->pSeqModel ); - p->pSeqModel = pAbs->pSeqModel; - pAbs->pSeqModel = NULL; - Aig_ManStop( pAbs ); - break; - } - Aig_ManStop( pAbs ); - pAbs = pTemp; - printf( "ITER %4d : ", Iter ); - if ( !pPars->fVerbose ) - Aig_ManPrintStats( pAbs ); - // output the intermediate result of abstraction - Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 ); -// printf( "Intermediate abstracted model was written into file \"%s\".\n", "gabs.aig" ); - // check if the ratio is reached - if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pAbs))/Aig_ManRegNum(p) < 1.0*pPars->nRatio ) - { - printf( "Refinements is stopped because flop reduction is less than %d%%\n", pPars->nRatio ); - Aig_ManStop( pAbs ); - pAbs = NULL; - Vec_IntFree( vFlops ); - vFlops = NULL; - break; - } + pGia->pCexSeq = pNew->pSeqModel; pNew->pSeqModel = NULL; + Vec_IntFree( vFlops ); + Aig_ManStop( pNew ); + return 0; } - return vFlops; + Vec_IntFree( pGia->vFlopClasses ); + pGia->vFlopClasses = Gia_ManFlops2Classes( pGia, vFlops ); + Vec_IntFree( vFlops ); + Aig_ManStop( pNew ); + return -1; } diff --git a/src/proof/abs/absOldSat.c b/src/proof/abs/absOldSat.c new file mode 100644 index 00000000..14f59667 --- /dev/null +++ b/src/proof/abs/absOldSat.c @@ -0,0 +1,986 @@ +/**CFile**************************************************************** + + FileName [saigRefSat.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [SAT based refinement of a counter-example.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigRefSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abs.h" +#include "sat/cnf/cnf.h" +#include "sat/bsat/satSolver.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// local manager +typedef struct Saig_RefMan_t_ Saig_RefMan_t; +struct Saig_RefMan_t_ +{ + // user data + Aig_Man_t * pAig; // user's AIG + Abc_Cex_t * pCex; // user's CEX + int nInputs; // the number of first inputs to skip + int fVerbose; // verbose flag + // unrolling + Aig_Man_t * pFrames; // unrolled timeframes + Vec_Int_t * vMapPiF2A; // mapping of frame PIs into real PIs +}; + +// performs ternary simulation +extern int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Maps array of frame PI IDs into array of original PI IDs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_RefManReason2Inputs( Saig_RefMan_t * p, Vec_Int_t * vReasons ) +{ + Vec_Int_t * vOriginal, * vVisited; + int i, Entry; + vOriginal = Vec_IntAlloc( Saig_ManPiNum(p->pAig) ); + vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) ); + Vec_IntForEachEntry( vReasons, Entry, i ) + { + int iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry ); + assert( iInput >= 0 && iInput < Aig_ManCiNum(p->pAig) ); + if ( Vec_IntEntry(vVisited, iInput) == 0 ) + Vec_IntPush( vOriginal, iInput ); + Vec_IntAddToEntry( vVisited, iInput, 1 ); + } + Vec_IntFree( vVisited ); + return vOriginal; +} + +/**Function************************************************************* + + Synopsis [Creates the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Saig_RefManReason2Cex( Saig_RefMan_t * p, Vec_Int_t * vReasons ) +{ + Abc_Cex_t * pCare; + int i, Entry, iInput, iFrame; + pCare = Abc_CexDup( p->pCex, p->pCex->nRegs ); + memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) ); + Vec_IntForEachEntry( vReasons, Entry, i ) + { + assert( Entry >= 0 && Entry < Aig_ManCiNum(p->pFrames) ); + iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry ); + iFrame = Vec_IntEntry( p->vMapPiF2A, 2*Entry+1 ); + Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput ); + } + return pCare; +} + +/**Function************************************************************* + + Synopsis [Returns reasons for the property to fail.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_RefManFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPrios, Vec_Int_t * vReasons ) +{ + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return; + Aig_ObjSetTravIdCurrent(p, pObj); + if ( Aig_ObjIsCi(pObj) ) + { + Vec_IntPush( vReasons, Aig_ObjCioId(pObj) ); + return; + } + assert( Aig_ObjIsNode(pObj) ); + if ( pObj->fPhase ) + { + Saig_RefManFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons ); + Saig_RefManFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons ); + } + else + { + int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase; + int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase; + assert( !fPhase0 || !fPhase1 ); + if ( !fPhase0 && fPhase1 ) + Saig_RefManFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons ); + else if ( fPhase0 && !fPhase1 ) + Saig_RefManFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons ); + else + { + int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) ); + int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) ); + if ( iPrio0 <= iPrio1 ) + Saig_RefManFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons ); + else + Saig_RefManFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons ); + } + } +} + +/**Function************************************************************* + + Synopsis [Returns reasons for the property to fail.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_RefManFindReason( Saig_RefMan_t * p ) +{ + Aig_Obj_t * pObj; + Vec_Int_t * vPrios, * vPi2Prio, * vReasons; + int i, CountPrios; + + vPi2Prio = Vec_IntStartFull( Saig_ManPiNum(p->pAig) ); + vPrios = Vec_IntStartFull( Aig_ManObjNumMax(p->pFrames) ); + + // set PI values according to CEX + CountPrios = 0; + Aig_ManConst1(p->pFrames)->fPhase = 1; + Aig_ManForEachCi( p->pFrames, pObj, i ) + { + int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i ); + int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 ); + pObj->fPhase = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ); + // assign priority + if ( Vec_IntEntry(vPi2Prio, iInput) == ~0 ) + Vec_IntWriteEntry( vPi2Prio, iInput, CountPrios++ ); +// Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Vec_IntEntry(vPi2Prio, iInput) ); + Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), i ); + } +// printf( "Priority numbers = %d.\n", CountPrios ); + Vec_IntFree( vPi2Prio ); + + // traverse and set the priority + Aig_ManForEachNode( p->pFrames, pObj, i ) + { + int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase; + int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase; + int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) ); + int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) ); + pObj->fPhase = fPhase0 && fPhase1; + if ( fPhase0 && fPhase1 ) // both are one + Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MaxInt(iPrio0, iPrio1) ); + else if ( !fPhase0 && fPhase1 ) + Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio0 ); + else if ( fPhase0 && !fPhase1 ) + Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio1 ); + else // both are zero + Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MinInt(iPrio0, iPrio1) ); + } + // check the property output + pObj = Aig_ManCo( p->pFrames, 0 ); + assert( (int)Aig_ObjFanin0(pObj)->fPhase == Aig_ObjFaninC0(pObj) ); + + // select the reason + vReasons = Vec_IntAlloc( 100 ); + Aig_ManIncrementTravId( p->pFrames ); + if ( !Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) ) + Saig_RefManFindReason_rec( p->pFrames, Aig_ObjFanin0(pObj), vPrios, vReasons ); + Vec_IntFree( vPrios ); + return vReasons; +} + + +/**Function************************************************************* + + Synopsis [Collect nodes in the unrolled timeframes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManUnrollCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vObjs, Vec_Int_t * vRoots ) +{ + if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) + return; + Aig_ObjSetTravIdCurrent(pAig, pObj); + if ( Aig_ObjIsCo(pObj) ) + Saig_ManUnrollCollect_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots ); + else if ( Aig_ObjIsNode(pObj) ) + { + Saig_ManUnrollCollect_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots ); + Saig_ManUnrollCollect_rec( pAig, Aig_ObjFanin1(pObj), vObjs, vRoots ); + } + if ( vRoots && Saig_ObjIsLo( pAig, pObj ) ) + Vec_IntPush( vRoots, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) ); + Vec_IntPush( vObjs, Aig_ObjId(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Derive unrolled timeframes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, Vec_Int_t ** pvMapPiF2A ) +{ + Aig_Man_t * pFrames; // unrolled timeframes + Vec_Vec_t * vFrameCos; // the list of COs per frame + Vec_Vec_t * vFrameObjs; // the list of objects per frame + Vec_Int_t * vRoots, * vObjs; + Aig_Obj_t * pObj; + int i, f; + // sanity checks + assert( Saig_ManPiNum(pAig) == pCex->nPis ); + assert( Saig_ManRegNum(pAig) == pCex->nRegs ); + assert( pCex->iPo >= 0 && pCex->iPo < Saig_ManPoNum(pAig) ); + + // map PIs of the unrolled frames into PIs of the original design + *pvMapPiF2A = Vec_IntAlloc( 1000 ); + + // collect COs and Objs visited in each frame + vFrameCos = Vec_VecStart( pCex->iFrame+1 ); + vFrameObjs = Vec_VecStart( pCex->iFrame+1 ); + // initialized the topmost frame + pObj = Aig_ManCo( pAig, pCex->iPo ); + Vec_VecPushInt( vFrameCos, pCex->iFrame, Aig_ObjId(pObj) ); + for ( f = pCex->iFrame; f >= 0; f-- ) + { + // collect nodes starting from the roots + Aig_ManIncrementTravId( pAig ); + vRoots = Vec_VecEntryInt( vFrameCos, f ); + Aig_ManForEachObjVec( vRoots, pAig, pObj, i ) + Saig_ManUnrollCollect_rec( pAig, pObj, + Vec_VecEntryInt(vFrameObjs, f), + (Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) ); + } + + // derive unrolled timeframes + pFrames = Aig_ManStart( 10000 ); + pFrames->pName = Abc_UtilStrsav( pAig->pName ); + pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec ); + // initialize the flops + Saig_ManForEachLo( pAig, pObj, i ) + pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, i) ); + // iterate through the frames + for ( f = 0; f <= pCex->iFrame; f++ ) + { + // construct + vObjs = Vec_VecEntryInt( vFrameObjs, f ); + Aig_ManForEachObjVec( vObjs, pAig, pObj, i ) + { + if ( Aig_ObjIsNode(pObj) ) + pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + else if ( Aig_ObjIsCo(pObj) ) + pObj->pData = Aig_ObjChild0Copy(pObj); + else if ( Aig_ObjIsConst1(pObj) ) + pObj->pData = Aig_ManConst1(pFrames); + else if ( Saig_ObjIsPi(pAig, pObj) ) + { + if ( Aig_ObjCioId(pObj) < nInputs ) + { + int iBit = pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj); + pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, iBit) ); + } + else + { + pObj->pData = Aig_ObjCreateCi( pFrames ); + Vec_IntPush( *pvMapPiF2A, Aig_ObjCioId(pObj) ); + Vec_IntPush( *pvMapPiF2A, f ); + } + } + } + if ( f == pCex->iFrame ) + break; + // transfer + vRoots = Vec_VecEntryInt( vFrameCos, f ); + Aig_ManForEachObjVec( vRoots, pAig, pObj, i ) + Saig_ObjLiToLo( pAig, pObj )->pData = pObj->pData; + } + // create output + pObj = Aig_ManCo( pAig, pCex->iPo ); + Aig_ObjCreateCo( pFrames, Aig_Not((Aig_Obj_t *)pObj->pData) ); + Aig_ManSetRegNum( pFrames, 0 ); + // cleanup + Vec_VecFree( vFrameCos ); + Vec_VecFree( vFrameObjs ); + // finallize + Aig_ManCleanup( pFrames ); + // return + return pFrames; +} + +/**Function************************************************************* + + Synopsis [Creates refinement manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Saig_RefMan_t * Saig_RefManStart( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose ) +{ + Saig_RefMan_t * p; + p = ABC_CALLOC( Saig_RefMan_t, 1 ); + p->pAig = pAig; + p->pCex = pCex; + p->nInputs = nInputs; + p->fVerbose = fVerbose; + p->pFrames = Saig_ManUnrollWithCex( pAig, pCex, nInputs, &p->vMapPiF2A ); + return p; +} + +/**Function************************************************************* + + Synopsis [Destroys refinement manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_RefManStop( Saig_RefMan_t * p ) +{ + Aig_ManStopP( &p->pFrames ); + Vec_IntFreeP( &p->vMapPiF2A ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Sets phase bits in the timeframe AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_RefManSetPhases( Saig_RefMan_t * p, Abc_Cex_t * pCare, int fValue1 ) +{ + Aig_Obj_t * pObj; + int i, iFrame, iInput; + Aig_ManConst1( p->pFrames )->fPhase = 1; + Aig_ManForEachCi( p->pFrames, pObj, i ) + { + iInput = Vec_IntEntry( p->vMapPiF2A, 2*i ); + iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 ); + pObj->fPhase = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ); + // update value if it is a don't-care + if ( pCare && !Abc_InfoHasBit( pCare->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ) ) + pObj->fPhase = fValue1; + } + Aig_ManForEachNode( p->pFrames, pObj, i ) + pObj->fPhase = ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) ) + & ( Aig_ObjFanin1(pObj)->fPhase ^ Aig_ObjFaninC1(pObj) ); + Aig_ManForEachCo( p->pFrames, pObj, i ) + pObj->fPhase = ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) ); + pObj = Aig_ManCo( p->pFrames, 0 ); + return pObj->fPhase; +} + +/**Function************************************************************* + + Synopsis [Tries to remove literals from abstraction.] + + Description [The literals are sorted more desirable first.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Vec_t * Saig_RefManOrderLiterals( Saig_RefMan_t * p, Vec_Int_t * vVar2PiId, Vec_Int_t * vAssumps ) +{ + Vec_Vec_t * vLits; + Vec_Int_t * vVar2New; + int i, Entry, iInput, iFrame; + // collect literals + vLits = Vec_VecAlloc( 100 ); + vVar2New = Vec_IntStartFull( Saig_ManPiNum(p->pAig) ); + Vec_IntForEachEntry( vAssumps, Entry, i ) + { + int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) ); + assert( iPiNum >= 0 && iPiNum < Aig_ManCiNum(p->pFrames) ); + iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum ); + iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 ); +// Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput ); + if ( Vec_IntEntry( vVar2New, iInput ) == ~0 ) + Vec_IntWriteEntry( vVar2New, iInput, Vec_VecSize(vLits) ); + Vec_VecPushInt( vLits, Vec_IntEntry( vVar2New, iInput ), Entry ); + } + Vec_IntFree( vVar2New ); + return vLits; +} + + +/**Function************************************************************* + + Synopsis [Generate the care set using SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Saig_RefManCreateCex( Saig_RefMan_t * p, Vec_Int_t * vVar2PiId, Vec_Int_t * vAssumps ) +{ + Abc_Cex_t * pCare; + int i, Entry, iInput, iFrame; + // create counter-example + pCare = Abc_CexDup( p->pCex, p->pCex->nRegs ); + memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) ); + Vec_IntForEachEntry( vAssumps, Entry, i ) + { + int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) ); + assert( iPiNum >= 0 && iPiNum < Aig_ManCiNum(p->pFrames) ); + iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum ); + iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 ); + Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput ); + } + return pCare; +} + +/**Function************************************************************* + + Synopsis [Generate the care set using SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p, int fNewOrder ) +{ + int nConfLimit = 1000000; + Abc_Cex_t * pCare; + Cnf_Dat_t * pCnf; + sat_solver * pSat; + Aig_Obj_t * pObj; + Vec_Vec_t * vLits = NULL; + Vec_Int_t * vAssumps, * vVar2PiId; + int i, k, Entry, RetValue;//, f = 0, Counter = 0; + int nCoreLits, * pCoreLits; + clock_t clk = clock(); + // create CNF + assert( Aig_ManRegNum(p->pFrames) == 0 ); +// pCnf = Cnf_Derive( p->pFrames, 0 ); // too slow + pCnf = Cnf_DeriveSimple( p->pFrames, 0 ); + RetValue = Saig_RefManSetPhases( p, NULL, 0 ); + if ( RetValue ) + { + printf( "Constructed frames are incorrect.\n" ); + Cnf_DataFree( pCnf ); + return NULL; + } + Cnf_DataTranformPolarity( pCnf, 0 ); + // create SAT solver + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + if ( pSat == NULL ) + { + Cnf_DataFree( pCnf ); + return NULL; + } +//Abc_PrintTime( 1, "Preparing", clock() - clk ); + // look for a true counter-example + if ( p->nInputs > 0 ) + { + RetValue = sat_solver_solve( pSat, NULL, NULL, + (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( RetValue == l_False ) + { + printf( "The problem is trivially UNSAT. The CEX is real.\n" ); + // create counter-example + pCare = Abc_CexDup( p->pCex, p->pCex->nRegs ); + memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) ); + return pCare; + } + // the problem is SAT - it is expected + } + // create assumptions + vVar2PiId = Vec_IntStartFull( pCnf->nVars ); + vAssumps = Vec_IntAlloc( Aig_ManCiNum(p->pFrames) ); + Aig_ManForEachCi( p->pFrames, pObj, i ) + { +// RetValue = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ); +// Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !RetValue ) ); + Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 ) ); + Vec_IntWriteEntry( vVar2PiId, pCnf->pVarNums[Aig_ObjId(pObj)], i ); + } + + // reverse the order of assumptions +// if ( fNewOrder ) +// Vec_IntReverseOrder( vAssumps ); + + if ( fNewOrder ) + { + // create literals + vLits = Saig_RefManOrderLiterals( p, vVar2PiId, vAssumps ); + // sort literals + Vec_VecSort( vLits, 1 ); + // save literals + Vec_IntClear( vAssumps ); + Vec_VecForEachEntryInt( vLits, Entry, i, k ) + Vec_IntPush( vAssumps, Entry ); + + for ( i = 0; i < Vec_VecSize(vLits); i++ ) + printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) ); + printf( "\n" ); + + if ( p->fVerbose ) + printf( "Total PIs = %d. Essential PIs = %d.\n", + Saig_ManPiNum(p->pAig) - p->nInputs, Vec_VecSize(vLits) ); + } + + // solve +clk = clock(); + RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), + (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); +//Abc_PrintTime( 1, "Solving", clock() - clk ); + if ( RetValue != l_False ) + { + if ( RetValue == l_True ) + printf( "Internal Error!!! The resulting problem is SAT.\n" ); + else + printf( "Internal Error!!! SAT solver timed out.\n" ); + Cnf_DataFree( pCnf ); + sat_solver_delete( pSat ); + Vec_IntFree( vAssumps ); + Vec_IntFree( vVar2PiId ); + return NULL; + } + assert( RetValue == l_False ); // UNSAT + + // get relevant SAT literals + nCoreLits = sat_solver_final( pSat, &pCoreLits ); + assert( nCoreLits > 0 ); + if ( p->fVerbose ) + printf( "AnalizeFinal selected %d assumptions (out of %d). Conflicts = %d.\n", + nCoreLits, Vec_IntSize(vAssumps), (int)pSat->stats.conflicts ); + + // save literals + Vec_IntClear( vAssumps ); + for ( i = 0; i < nCoreLits; i++ ) + Vec_IntPush( vAssumps, pCoreLits[i] ); + + + // create literals + vLits = Saig_RefManOrderLiterals( p, vVar2PiId, vAssumps ); + // sort literals +// Vec_VecSort( vLits, 0 ); + // save literals + Vec_IntClear( vAssumps ); + Vec_VecForEachEntryInt( vLits, Entry, i, k ) + Vec_IntPush( vAssumps, Entry ); + +// for ( i = 0; i < Vec_VecSize(vLits); i++ ) +// printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) ); +// printf( "\n" ); + + if ( p->fVerbose ) + printf( "Total PIs = %d. Essential PIs = %d.\n", + Saig_ManPiNum(p->pAig) - p->nInputs, Vec_VecSize(vLits) ); +/* + // try assumptions in different order + RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), + (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n", + Vec_IntSize(vAssumps), (RetValue == l_False ? "UNSAT" : "SAT"), (int)pSat->stats.conflicts ); + + // create different sets of assumptions + Counter = Vec_VecSize(vLits); + for ( f = 0; f < Vec_VecSize(vLits); f++ ) + { + Vec_IntClear( vAssumps ); + Vec_VecForEachEntryInt( vLits, Entry, i, k ) + if ( i != f ) + Vec_IntPush( vAssumps, Entry ); + + // try the new assumptions + RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), + (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n", + Vec_IntSize(vAssumps), RetValue == l_False ? "UNSAT" : "SAT", (int)pSat->stats.conflicts ); + if ( RetValue != l_False ) + continue; + + // UNSAT - remove literals + Vec_IntClear( Vec_VecEntryInt(vLits, f) ); + Counter--; + } + + for ( i = 0; i < Vec_VecSize(vLits); i++ ) + printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) ); + printf( "\n" ); + + if ( p->fVerbose ) + printf( "Total PIs = %d. Essential PIs = %d.\n", + Saig_ManPiNum(p->pAig) - p->nInputs, Counter ); + + // save literals + Vec_IntClear( vAssumps ); + Vec_VecForEachEntryInt( vLits, Entry, i, k ) + Vec_IntPush( vAssumps, Entry ); +*/ + // create counter-example + pCare = Saig_RefManCreateCex( p, vVar2PiId, vAssumps ); + + // cleanup + Cnf_DataFree( pCnf ); + sat_solver_delete( pSat ); + Vec_IntFree( vAssumps ); + Vec_IntFree( vVar2PiId ); + Vec_VecFreeP( &vLits ); + + // verify counter-example + RetValue = Saig_RefManSetPhases( p, pCare, 0 ); + if ( RetValue ) + printf( "Reduced CEX verification has failed.\n" ); + RetValue = Saig_RefManSetPhases( p, pCare, 1 ); + if ( RetValue ) + printf( "Reduced CEX verification has failed.\n" ); + return pCare; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_RefManRefineWithSat( Saig_RefMan_t * p, Vec_Int_t * vAigPis ) +{ + int nConfLimit = 1000000; + Cnf_Dat_t * pCnf; + sat_solver * pSat; + Aig_Obj_t * pObj; + Vec_Vec_t * vLits; + Vec_Int_t * vReasons, * vAssumps, * vVisited, * vVar2PiId; + int i, k, f, Entry, RetValue, Counter; + + // create CNF and SAT solver + pCnf = Cnf_DeriveSimple( p->pFrames, 0 ); + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + if ( pSat == NULL ) + { + Cnf_DataFree( pCnf ); + return NULL; + } + + // mark used AIG inputs + vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) ); + Vec_IntForEachEntry( vAigPis, Entry, i ) + { + assert( Entry >= 0 && Entry < Aig_ManCiNum(p->pAig) ); + Vec_IntWriteEntry( vVisited, Entry, 1 ); + } + + // create assumptions + vVar2PiId = Vec_IntStartFull( pCnf->nVars ); + vAssumps = Vec_IntAlloc( Aig_ManCiNum(p->pFrames) ); + Aig_ManForEachCi( p->pFrames, pObj, i ) + { + int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i ); + int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 ); + if ( Vec_IntEntry(vVisited, iInput) == 0 ) + continue; + RetValue = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ); + Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !RetValue ) ); +// Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 ) ); + Vec_IntWriteEntry( vVar2PiId, pCnf->pVarNums[Aig_ObjId(pObj)], i ); + } + Vec_IntFree( vVisited ); + + // try assumptions in different order + RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), + (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n", + Vec_IntSize(vAssumps), (RetValue == l_False ? "UNSAT" : "SAT"), (int)pSat->stats.conflicts ); + +/* + // AnalizeFinal does not work because it implications propagate directly + // and SAT solver does not kick in (the number of conflicts in 0). + + // count the number of lits in the unsat core + { + int nCoreLits, * pCoreLits; + nCoreLits = sat_solver_final( pSat, &pCoreLits ); + assert( nCoreLits > 0 ); + + // count the number of flops + vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) ); + for ( i = 0; i < nCoreLits; i++ ) + { + int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(pCoreLits[i]) ); + int iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum ); + int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 ); + Vec_IntWriteEntry( vVisited, iInput, 1 ); + } + // count the number of entries + Counter = 0; + Vec_IntForEachEntry( vVisited, Entry, i ) + Counter += Entry; + Vec_IntFree( vVisited ); + +// if ( p->fVerbose ) + printf( "AnalizeFinal: Assumptions %d (out of %d). Essential PIs = %d. Conflicts = %d.\n", + nCoreLits, Vec_IntSize(vAssumps), Counter, (int)pSat->stats.conflicts ); + } +*/ + + // derive literals + vLits = Saig_RefManOrderLiterals( p, vVar2PiId, vAssumps ); + for ( i = 0; i < Vec_VecSize(vLits); i++ ) + printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) ); + printf( "\n" ); + + // create different sets of assumptions + Counter = Vec_VecSize(vLits); + for ( f = 0; f < Vec_VecSize(vLits); f++ ) + { + Vec_IntClear( vAssumps ); + Vec_VecForEachEntryInt( vLits, Entry, i, k ) + if ( i != f ) + Vec_IntPush( vAssumps, Entry ); + + // try the new assumptions + RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), + (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n", + Vec_IntSize(vAssumps), RetValue == l_False ? "UNSAT" : "SAT", (int)pSat->stats.conflicts ); + if ( RetValue != l_False ) + continue; + + // UNSAT - remove literals + Vec_IntClear( Vec_VecEntryInt(vLits, f) ); + Counter--; + } + + for ( i = 0; i < Vec_VecSize(vLits); i++ ) + printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) ); + printf( "\n" ); + + // create assumptions + Vec_IntClear( vAssumps ); + Vec_VecForEachEntryInt( vLits, Entry, i, k ) + Vec_IntPush( vAssumps, Entry ); + + // try assumptions in different order + RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), + (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n", + Vec_IntSize(vAssumps), (RetValue == l_False ? "UNSAT" : "SAT"), (int)pSat->stats.conflicts ); + +// if ( p->fVerbose ) +// printf( "Total PIs = %d. Essential PIs = %d.\n", +// Saig_ManPiNum(p->pAig) - p->nInputs, Counter ); + + + // transform assumptions into reasons + vReasons = Vec_IntAlloc( 100 ); + Vec_IntForEachEntry( vAssumps, Entry, i ) + { + int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) ); + assert( iPiNum >= 0 && iPiNum < Aig_ManCiNum(p->pFrames) ); + Vec_IntPush( vReasons, iPiNum ); + } + + // cleanup + Cnf_DataFree( pCnf ); + sat_solver_delete( pSat ); + Vec_IntFree( vAssumps ); + Vec_IntFree( vVar2PiId ); + Vec_VecFreeP( &vLits ); + + return vReasons; +} + +/**Function************************************************************* + + Synopsis [SAT-based refinement of the counter-example.] + + Description [The first parameter (nInputs) indicates how many first + primary inputs to skip without considering as care candidates.] + + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Saig_ManFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fNewOrder, int fVerbose ) +{ + Saig_RefMan_t * p; + Vec_Int_t * vReasons; + Abc_Cex_t * pCare; + clock_t clk = clock(); + + clk = clock(); + p = Saig_RefManStart( pAig, pCex, nInputs, fVerbose ); + vReasons = Saig_RefManFindReason( p ); + +if ( fVerbose ) +Aig_ManPrintStats( p->pFrames ); + +// if ( fVerbose ) + { + Vec_Int_t * vRes = Saig_RefManReason2Inputs( p, vReasons ); + printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ", + Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), + Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); +ABC_PRT( "Time", clock() - clk ); + + Vec_IntFree( vRes ); + +/* + //////////////////////////////////// + Vec_IntFree( vReasons ); + vReasons = Saig_RefManRefineWithSat( p, vRes ); + //////////////////////////////////// + + Vec_IntFree( vRes ); + vRes = Saig_RefManReason2Inputs( p, vReasons ); + printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ", + Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), + Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); + + Vec_IntFree( vRes ); +ABC_PRT( "Time", clock() - clk ); +*/ + } + + pCare = Saig_RefManReason2Cex( p, vReasons ); + Vec_IntFree( vReasons ); + Saig_RefManStop( p ); + +if ( fVerbose ) +Abc_CexPrintStats( pCex ); +if ( fVerbose ) +Abc_CexPrintStats( pCare ); + + return pCare; +} + +/**Function************************************************************* + + Synopsis [Returns the array of PIs for flops that should not be absracted.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose ) +{ + Saig_RefMan_t * p; + Vec_Int_t * vRes, * vReasons; + clock_t clk; + if ( Saig_ManPiNum(pAig) != pCex->nPis ) + { + printf( "Saig_ManExtendCounterExampleTest3(): The PI count of AIG (%d) does not match that of cex (%d).\n", + Aig_ManCiNum(pAig), pCex->nPis ); + return NULL; + } + +clk = clock(); + + p = Saig_RefManStart( pAig, pCex, iFirstFlopPi, fVerbose ); + vReasons = Saig_RefManFindReason( p ); + vRes = Saig_RefManReason2Inputs( p, vReasons ); + +// if ( fVerbose ) + { + printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ", + Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), + Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); +ABC_PRT( "Time", clock() - clk ); + } + +/* + //////////////////////////////////// + Vec_IntFree( vReasons ); + vReasons = Saig_RefManRefineWithSat( p, vRes ); + //////////////////////////////////// + + // derive new result + Vec_IntFree( vRes ); + vRes = Saig_RefManReason2Inputs( p, vReasons ); +// if ( fVerbose ) + { + printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ", + Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), + Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); +ABC_PRT( "Time", clock() - clk ); + } +*/ + + Vec_IntFree( vReasons ); + Saig_RefManStop( p ); + return vRes; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/saig/saigSimExt2.c b/src/proof/abs/absOldSim.c index ca46c0b3..e5c1e938 100644 --- a/src/aig/saig/saigSimExt2.c +++ b/src/proof/abs/absOldSim.c @@ -18,8 +18,7 @@ ***********************************************************************/ -#include "saig.h" -#include "proof/ssw/ssw.h" +#include "abs.h" ABC_NAMESPACE_IMPL_START @@ -28,6 +27,44 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#define SAIG_ZER 1 +#define SAIG_ONE 2 +#define SAIG_UND 3 + +static inline int Saig_ManSimInfoNot( int Value ) +{ + if ( Value == SAIG_ZER ) + return SAIG_ONE; + if ( Value == SAIG_ONE ) + return SAIG_ZER; + return SAIG_UND; +} + +static inline int Saig_ManSimInfoAnd( int Value0, int Value1 ) +{ + if ( Value0 == SAIG_ZER || Value1 == SAIG_ZER ) + return SAIG_ZER; + if ( Value0 == SAIG_ONE && Value1 == SAIG_ONE ) + return SAIG_ONE; + return SAIG_UND; +} + +static inline int Saig_ManSimInfoGet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame ) +{ + unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) ); + return 3 & (pInfo[iFrame >> 4] >> ((iFrame & 15) << 1)); +} + +static inline void Saig_ManSimInfoSet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame, int Value ) +{ + unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) ); + assert( Value >= SAIG_ZER && Value <= SAIG_UND ); + Value ^= Saig_ManSimInfoGet( vSimInfo, pObj, iFrame ); + pInfo[iFrame >> 4] ^= (Value << ((iFrame & 15) << 1)); +} + + + #define SAIG_ZER_NEW 0 // 0 not visited #define SAIG_ONE_NEW 1 // 1 not visited #define SAIG_ZER_OLD 2 // 0 visited @@ -86,7 +123,7 @@ static inline void Saig_ManSimInfo2Set( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, } // performs ternary simulation -extern int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes ); +//extern int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -103,6 +140,76 @@ extern int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSi SeeAlso [] ***********************************************************************/ +int Saig_ManExtendOneEval( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame ) +{ + int Value0, Value1, Value; + Value0 = Saig_ManSimInfoGet( vSimInfo, Aig_ObjFanin0(pObj), iFrame ); + if ( Aig_ObjFaninC0(pObj) ) + Value0 = Saig_ManSimInfoNot( Value0 ); + if ( Aig_ObjIsCo(pObj) ) + { + Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value0 ); + return Value0; + } + assert( Aig_ObjIsNode(pObj) ); + Value1 = Saig_ManSimInfoGet( vSimInfo, Aig_ObjFanin1(pObj), iFrame ); + if ( Aig_ObjFaninC1(pObj) ) + Value1 = Saig_ManSimInfoNot( Value1 ); + Value = Saig_ManSimInfoAnd( Value0, Value1 ); + Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value ); + return Value; +} + +/**Function************************************************************* + + Synopsis [Performs ternary simulation for one design.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes ) +{ + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + int i, f, Entry, iBit = 0; + Saig_ManForEachLo( p, pObj, i ) + Saig_ManSimInfoSet( vSimInfo, pObj, 0, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER ); + for ( f = 0; f <= pCex->iFrame; f++ ) + { + Saig_ManSimInfoSet( vSimInfo, Aig_ManConst1(p), f, SAIG_ONE ); + Saig_ManForEachPi( p, pObj, i ) + Saig_ManSimInfoSet( vSimInfo, pObj, f, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER ); + if ( vRes ) + Vec_IntForEachEntry( vRes, Entry, i ) + Saig_ManSimInfoSet( vSimInfo, Aig_ManCi(p, Entry), f, SAIG_UND ); + Aig_ManForEachNode( p, pObj, i ) + Saig_ManExtendOneEval( vSimInfo, pObj, f ); + Aig_ManForEachCo( p, pObj, i ) + Saig_ManExtendOneEval( vSimInfo, pObj, f ); + if ( f == pCex->iFrame ) + break; + Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) + Saig_ManSimInfoSet( vSimInfo, pObjLo, f+1, Saig_ManSimInfoGet(vSimInfo, pObjLi, f) ); + } + // make sure the output of the property failed + pObj = Aig_ManCo( p, pCex->iPo ); + return Saig_ManSimInfoGet( vSimInfo, pObj, pCex->iFrame ); +} + +/**Function************************************************************* + + Synopsis [Performs ternary simulation for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Saig_ManExtendOneEval2( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame ) { int Value0, Value1, Value; @@ -361,117 +468,6 @@ ABC_PRT( "Time", clock() - clk ); } - - - -/**Function************************************************************* - - Synopsis [Returns the array of PIs for flops that should not be absracted.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Saig_ManDeriveCex( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ) -{ - Abc_Cex_t * pCare; - Aig_Obj_t * pObj; - Vec_Int_t * vRes, * vResInv; - int i, f, Value; -// assert( Aig_ManRegNum(p) > 0 ); - assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Abc_BitWordNum(2*(pCex->iFrame+1)) ); - // start simulation data - Value = Saig_ManSimDataInit2( p, pCex, vSimInfo ); - assert( Value == SAIG_ONE_NEW ); - // derive implications of constants and primary inputs - Saig_ManForEachLo( p, pObj, i ) - Saig_ManSetAndDriveImplications_rec( p, pObj, 0, pCex->iFrame, vSimInfo ); - for ( f = pCex->iFrame; f >= 0; f-- ) - { - Saig_ManSetAndDriveImplications_rec( p, Aig_ManConst1(p), f, pCex->iFrame, vSimInfo ); - for ( i = 0; i < iFirstFlopPi; i++ ) - Saig_ManSetAndDriveImplications_rec( p, Aig_ManCi(p, i), f, pCex->iFrame, vSimInfo ); - } - // recursively compute justification - Saig_ManExplorePaths_rec( p, Aig_ManCo(p, pCex->iPo), pCex->iFrame, pCex->iFrame, vSimInfo ); - - // create CEX - pCare = Abc_CexDup( pCex, pCex->nRegs ); - memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) ); - - // select the result - vRes = Vec_IntAlloc( 1000 ); - vResInv = Vec_IntAlloc( 1000 ); - for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ ) - { - int fFound = 0; - for ( f = pCex->iFrame; f >= 0; f-- ) - { - Value = Saig_ManSimInfo2Get( vSimInfo, Aig_ManCi(p, i), f ); - if ( Saig_ManSimInfo2IsOld( Value ) ) - { - fFound = 1; - Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * f + i ); - } - } - if ( fFound ) - Vec_IntPush( vRes, i ); - else - Vec_IntPush( vResInv, i ); - } - // resimulate to make sure it is valid - Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv ); - assert( Value == SAIG_ONE ); - Vec_IntFree( vResInv ); - Vec_IntFree( vRes ); - - return pCare; -} - -/**Function************************************************************* - - Synopsis [Returns the array of PIs for flops that should not be absracted.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Cex_t * Saig_ManFindCexCareBitsSense( Aig_Man_t * p, Abc_Cex_t * pCex, int iFirstFlopPi, int fVerbose ) -{ - Abc_Cex_t * pCare; - Vec_Ptr_t * vSimInfo; - clock_t clk; - if ( Saig_ManPiNum(p) != pCex->nPis ) - { - printf( "Saig_ManExtendCounterExampleTest2(): The PI count of AIG (%d) does not match that of cex (%d).\n", - Aig_ManCiNum(p), pCex->nPis ); - return NULL; - } - Aig_ManFanoutStart( p ); - vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Abc_BitWordNum(2*(pCex->iFrame+1)) ); - Vec_PtrCleanSimInfo( vSimInfo, 0, Abc_BitWordNum(2*(pCex->iFrame+1)) ); - -clk = clock(); - pCare = Saig_ManDeriveCex( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); - if ( fVerbose ) - { -// printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) ); -Abc_CexPrintStats( pCex ); -Abc_CexPrintStats( pCare ); -ABC_PRT( "Time", clock() - clk ); - } - - Vec_PtrFree( vSimInfo ); - Aig_ManFanoutStop( p ); - return pCare; -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaAbsOut.c b/src/proof/abs/absOut.c index 536ea277..c230acb4 100644 --- a/src/aig/gia/giaAbsOut.c +++ b/src/proof/abs/absOut.c @@ -1,10 +1,10 @@ /**CFile**************************************************************** - FileName [giaAbsOut.c] + FileName [absOut.c] SystemName [ABC: Logic synthesis and verification system.] - PackageName [Scalable AIG package.] + PackageName [Abstraction package.] Synopsis [Abstraction refinement outside of abstraction engines.] @@ -14,13 +14,11 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: giaAbsOut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: absOut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ -#include "gia.h" -#include "giaAig.h" -#include "aig/saig/saig.h" +#include "abs.h" ABC_NAMESPACE_IMPL_START @@ -92,7 +90,6 @@ Abc_Cex_t * Gia_ManCexRemap( Gia_Man_t * p, Abc_Cex_t * pCexAbs, Vec_Int_t * vPi int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose ) { extern void Nwk_ManDeriveMinCut( Gia_Man_t * p, int fVerbose ); -// extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose ); int fAddOneLayer = 1; Abc_Cex_t * pCexNew = NULL; Gia_Man_t * pAbs; @@ -431,11 +428,11 @@ int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int iFra pNew->vGateClasses = Vec_IntDup( p->vGateClasses ); // perform abstraction for the new AIG { - Gia_ParVta_t Pars, * pPars = &Pars; - Gia_VtaSetDefaultParams( pPars ); + Abs_Par_t Pars, * pPars = &Pars; + Abs_ParSetDefaults( pPars ); pPars->nFramesMax = pCex->iFrame - iFrameStart + 1 + iFrameExtra; pPars->fVerbose = fVerbose; - RetValue = Ga2_ManPerform( pNew, pPars ); + RetValue = Gia_ManPerformGla( pNew, pPars ); if ( RetValue == 0 ) // spurious SAT { Vec_IntFreeP( &pNew->vGateClasses ); diff --git a/src/aig/gia/giaAbsPth.c b/src/proof/abs/absPth.c index 3b997443..73f76822 100644 --- a/src/aig/gia/giaAbsPth.c +++ b/src/proof/abs/absPth.c @@ -1,10 +1,10 @@ /**CFile**************************************************************** - FileName [giaAbsPth.c] + FileName [absPth.c] SystemName [ABC: Logic synthesis and verification system.] - PackageName [Scalable AIG package.] + PackageName [Abstraction package.] Synopsis [Interface to pthreads.] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: giaAbsPth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: absPth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ diff --git a/src/aig/gia/giaAbsRef.c b/src/proof/abs/absRef.c index 8a5aedc5..3aea96ee 100644 --- a/src/aig/gia/giaAbsRef.c +++ b/src/proof/abs/absRef.c @@ -1,10 +1,10 @@ /**CFile**************************************************************** - FileName [giaAbsRef.c] + FileName [absRef.c] SystemName [ABC: Logic synthesis and verification system.] - PackageName [Scalable AIG package.] + PackageName [Abstraction package.] Synopsis [Refinement manager.] @@ -14,13 +14,13 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: giaAbsRef.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: absRef.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ -#include "gia.h" -#include "giaAbsRef.h" #include "sat/bsat/satSolver2.h" +#include "abs.h" +#include "absRef.h" ABC_NAMESPACE_IMPL_START diff --git a/src/aig/gia/giaAbsRef.h b/src/proof/abs/absRef.h index e44245be..ca46c776 100644 --- a/src/aig/gia/giaAbsRef.h +++ b/src/proof/abs/absRef.h @@ -1,10 +1,10 @@ /**CFile**************************************************************** - FileName [giaAbsRef.h] + FileName [absRef.h] SystemName [ABC: Logic synthesis and verification system.] - PackageName [Scalable AIG package.] + PackageName [Abstraction package.] Synopsis [Refinement manager.] @@ -14,12 +14,12 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: giaAbsRef.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: absRef.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ -#ifndef ABC__aig__gia__giaAbsRef_h -#define ABC__aig__gia__giaAbsRef_h +#ifndef ABC__proof_abs__AbsRef_h +#define ABC__proof_abs__AbsRef_h //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaAbsRef2.c b/src/proof/abs/absRef2.c index e5bf3b0f..7fb26e5a 100644 --- a/src/aig/gia/giaAbsRef2.c +++ b/src/proof/abs/absRef2.c @@ -1,10 +1,10 @@ /**CFile**************************************************************** - FileName [giaAbsRef2.c] + FileName [absRef2.c] SystemName [ABC: Logic synthesis and verification system.] - PackageName [Scalable AIG package.] + PackageName [Abstraction package.] Synopsis [Refinement manager.] @@ -14,12 +14,12 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: giaAbsRef2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: absRef2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ -#include "gia.h" -#include "giaAbsRef2.h" +#include "abs.h" +#include "absRef2.h" ABC_NAMESPACE_IMPL_START diff --git a/src/aig/gia/giaAbsRef2.h b/src/proof/abs/absRef2.h index f0ad9670..df7774c0 100644 --- a/src/aig/gia/giaAbsRef2.h +++ b/src/proof/abs/absRef2.h @@ -1,10 +1,10 @@ /**CFile**************************************************************** - FileName [giaAbsRef2.h] + FileName [absRef2.h] SystemName [ABC: Logic synthesis and verification system.] - PackageName [Scalable AIG package.] + PackageName [Abstraction package.] Synopsis [Refinement manager.] @@ -14,12 +14,12 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: giaAbsRef2.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: absRef2.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ -#ifndef ABC__aig__gia__giaAbsRef2_h -#define ABC__aig__gia__giaAbsRef2_h +#ifndef ABC__proof_abs__AbsRef2_h +#define ABC__proof_abs__AbsRef2_h //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/abs/absUtil.c b/src/proof/abs/absUtil.c new file mode 100644 index 00000000..60429496 --- /dev/null +++ b/src/proof/abs/absUtil.c @@ -0,0 +1,257 @@ +/**CFile**************************************************************** + + FileName [absUtil.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Abstraction package.] + + Synopsis [Interface to pthreads.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: absUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abs.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [This procedure sets default parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abs_ParSetDefaults( Abs_Par_t * p ) +{ + memset( p, 0, sizeof(Abs_Par_t) ); + p->nFramesMax = 0; // maximum frames + p->nFramesStart = 0; // starting frame + p->nFramesPast = 4; // overlap frames + p->nConfLimit = 0; // conflict limit + p->nLearnedMax = 1000; // max number of learned clauses + p->nLearnedStart = 1000; // max number of learned clauses + p->nLearnedDelta = 200; // max number of learned clauses + p->nLearnedPerce = 70; // max number of learned clauses + p->nTimeOut = 0; // timeout in seconds + p->nRatioMin = 0; // stop when less than this % of object is abstracted + p->nRatioMax = 30; // restart when more than this % of object is abstracted + p->fUseTermVars = 0; // use terminal variables + p->fUseRollback = 0; // use rollback to the starting number of frames + p->fPropFanout = 1; // propagate fanouts during refinement + p->fVerbose = 0; // verbose flag + p->iFrame = -1; // the number of frames covered + p->iFrameProved = -1; // the number of frames proved + p->nFramesNoChangeLim = 1; // the number of frames without change to dump abstraction +} + +/**Function************************************************************* + + Synopsis [Converting VTA vector to GLA vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta ) +{ + Gia_Obj_t * pObj; + Vec_Int_t * vGla; + int nObjMask, nObjs = Gia_ManObjNum(p); + int i, Entry, nFrames = Vec_IntEntry( vVta, 0 ); + assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) ); + // get the bitmask + nObjMask = (1 << Abc_Base2Log(nObjs)) - 1; + assert( nObjs <= nObjMask ); + // go through objects + vGla = Vec_IntStart( nObjs ); + Vec_IntForEachEntryStart( vVta, Entry, i, nFrames+2 ) + { + pObj = Gia_ManObj( p, (Entry & nObjMask) ); + assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsConst0(pObj) ); + Vec_IntAddToEntry( vGla, (Entry & nObjMask), 1 ); + } + Vec_IntWriteEntry( vGla, 0, nFrames ); + return vGla; +} + +/**Function************************************************************* + + Synopsis [Converting GLA vector to VTA vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames ) +{ + Vec_Int_t * vVta; + int nObjBits, nObjMask, nObjs = Gia_ManObjNum(p); + int i, k, j, Entry, Counter, nGlaSize; + //. get the GLA size + nGlaSize = Vec_IntSum(vGla); + // get the bitmask + nObjBits = Abc_Base2Log(nObjs); + nObjMask = (1 << Abc_Base2Log(nObjs)) - 1; + assert( nObjs <= nObjMask ); + // go through objects + vVta = Vec_IntAlloc( 1000 ); + Vec_IntPush( vVta, nFrames ); + Counter = nFrames + 2; + for ( i = 0; i <= nFrames; i++, Counter += i * nGlaSize ) + Vec_IntPush( vVta, Counter ); + for ( i = 0; i < nFrames; i++ ) + for ( k = 0; k <= i; k++ ) + Vec_IntForEachEntry( vGla, Entry, j ) + if ( Entry ) + Vec_IntPush( vVta, (k << nObjBits) | j ); + Counter = Vec_IntEntry(vVta, nFrames+1); + assert( Vec_IntEntry(vVta, nFrames+1) == Vec_IntSize(vVta) ); + return vVta; +} + +/**Function************************************************************* + + Synopsis [Converting GLA vector to FLA vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_FlaConvertToGla_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vGla ) +{ + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return; + Gia_ObjSetTravIdCurrent(p, pObj); + Vec_IntWriteEntry( vGla, Gia_ObjId(p, pObj), 1 ); + if ( Gia_ObjIsRo(p, pObj) ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla ); + Gia_FlaConvertToGla_rec( p, Gia_ObjFanin1(pObj), vGla ); +} + +/**Function************************************************************* + + Synopsis [Converting FLA vector to GLA vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla ) +{ + Vec_Int_t * vGla; + Gia_Obj_t * pObj; + int i; + // mark const0 and relevant CI objects + Gia_ManIncrementTravId( p ); + Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p)); + Gia_ManForEachPi( p, pObj, i ) + Gia_ObjSetTravIdCurrent(p, pObj); + Gia_ManForEachRo( p, pObj, i ) + if ( !Vec_IntEntry(vFla, i) ) + Gia_ObjSetTravIdCurrent(p, pObj); + // label all objects reachable from the PO and selected flops + vGla = Vec_IntStart( Gia_ManObjNum(p) ); + Vec_IntWriteEntry( vGla, 0, 1 ); + Gia_ManForEachPo( p, pObj, i ) + Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla ); + Gia_ManForEachRi( p, pObj, i ) + if ( Vec_IntEntry(vFla, i) ) + Gia_FlaConvertToGla_rec( p, Gia_ObjFanin0(pObj), vGla ); + return vGla; +} + +/**Function************************************************************* + + Synopsis [Converting GLA vector to FLA vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla ) +{ + Vec_Int_t * vFla; + Gia_Obj_t * pObj; + int i; + vFla = Vec_IntStart( Gia_ManRegNum(p) ); + Gia_ManForEachRo( p, pObj, i ) + if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) ) + Vec_IntWriteEntry( vFla, i, 1 ); + return vFla; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla ) +{ + Gia_Obj_t * pObj; + int i, Count = 0; + Gia_ManForEachRo( p, pObj, i ) + if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) ) + Count++; + return Count; +} +int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla ) +{ + Gia_Obj_t * pObj; + int i, Count = 0; + Gia_ManForEachAnd( p, pObj, i ) + if ( Vec_IntEntry(vGla, Gia_ObjId(p, pObj)) ) + Count++; + return Count; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/giaAbsVta.c b/src/proof/abs/absVta.c index 517c1d3d..7e85c661 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/proof/abs/absVta.c @@ -1,10 +1,10 @@ /**CFile**************************************************************** - FileName [giaAbsVta.c] + FileName [absVta.c] SystemName [ABC: Logic synthesis and verification system.] - PackageName [Scalable AIG package.] + PackageName [Abstraction package.] Synopsis [Variable time-frame abstraction.] @@ -14,13 +14,13 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: giaAbsVta.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: absVta.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ -#include "gia.h" #include "sat/bsat/satSolver2.h" #include "base/main/main.h" +#include "abs.h" ABC_NAMESPACE_IMPL_START @@ -47,7 +47,7 @@ struct Vta_Man_t_ { // user data Gia_Man_t * pGia; // AIG manager - Gia_ParVta_t* pPars; // parameters + Abs_Par_t * pPars; // parameters // internal data int nObjs; // the number of objects int nObjsAlloc; // the number of objects allocated @@ -136,40 +136,6 @@ extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame ); /**Function************************************************************* - Synopsis [This procedure sets default parameters.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_VtaSetDefaultParams( Gia_ParVta_t * p ) -{ - memset( p, 0, sizeof(Gia_ParVta_t) ); - p->nFramesMax = 0; // maximum frames - p->nFramesStart = 0; // starting frame - p->nFramesPast = 4; // overlap frames - p->nConfLimit = 0; // conflict limit - p->nLearnedMax = 1000; // max number of learned clauses - p->nLearnedStart = 1000; // max number of learned clauses - p->nLearnedDelta = 200; // max number of learned clauses - p->nLearnedPerce = 70; // max number of learned clauses - p->nTimeOut = 0; // timeout in seconds - p->nRatioMin = 0; // stop when less than this % of object is abstracted - p->nRatioMax = 30; // restart when more than this % of object is abstracted - p->fUseTermVars = 0; // use terminal variables - p->fUseRollback = 0; // use rollback to the starting number of frames - p->fPropFanout = 1; // propagate fanouts during refinement - p->fVerbose = 0; // verbose flag - p->iFrame = -1; // the number of frames covered - p->iFrameProved = -1; // the number of frames proved - p->nFramesNoChangeLim = 1; // the number of frames without change to dump abstraction -} - -/**Function************************************************************* - Synopsis [Converting from one array to per-frame arrays.] Description [] @@ -1014,7 +980,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f ) SeeAlso [] ***********************************************************************/ -Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) +Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Abs_Par_t * pPars ) { Vta_Man_t * p; p = ABC_CALLOC( Vta_Man_t, 1 ); @@ -1524,7 +1490,7 @@ void Gia_VtaPrintMemory( Vta_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) +int Gia_VtaPerformInt( Gia_Man_t * pAig, Abs_Par_t * pPars ) { Vta_Man_t * p; Vec_Int_t * vCore; @@ -1775,7 +1741,7 @@ finish: SeeAlso [] ***********************************************************************/ -int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) +int Gia_VtaPerform( Gia_Man_t * pAig, Abs_Par_t * pPars ) { int RetValue = -1; if ( pAig->vObjClasses == NULL && pPars->fUseRollback ) diff --git a/src/proof/abs/module.make b/src/proof/abs/module.make new file mode 100644 index 00000000..4e652afd --- /dev/null +++ b/src/proof/abs/module.make @@ -0,0 +1,15 @@ +SRC += src/proof/abs/abs.c \ + src/proof/abs/absDup.c \ + src/proof/abs/absGla.c \ + src/proof/abs/absGlaOld.c \ + src/proof/abs/absIter.c \ + src/proof/abs/absOldCex.c \ + src/proof/abs/absOldRef.c \ + src/proof/abs/absOldSat.c \ + src/proof/abs/absOldSim.c \ + src/proof/abs/absOut.c \ + src/proof/abs/absPth.c \ + src/proof/abs/absRef.c \ + src/proof/abs/absRef2.c \ + src/proof/abs/absVta.c \ + src/proof/abs/absUtil.c |