From 28e065b0aebc08990ca8208b4982edafe66fb0fd Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 22 May 2013 11:02:56 -0700 Subject: Counter-example depth minimization. --- src/aig/gia/gia.h | 5 +- src/aig/gia/giaDup.c | 93 +++++++++- src/aig/gia/giaMan.c | 6 +- src/base/abci/abc.c | 42 +++-- src/sat/bmc/bmcCexDepth.c | 421 ++++++++++++++++++++++++++++++++++++++++++++++ src/sat/bmc/module.make | 1 + 6 files changed, 552 insertions(+), 16 deletions(-) create mode 100644 src/sat/bmc/bmcCexDepth.c (limited to 'src') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 12d255a4..c890b165 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -343,6 +343,7 @@ static inline int Gia_ManObjIsConst0( Gia_Man_t * p, Gia_Obj_t * pObj){ static inline int Gia_Obj2Lit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_Var2Lit(Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj)); } static inline Gia_Obj_t * Gia_Lit2Obj( Gia_Man_t * p, int iLit ) { return Gia_NotCond(Gia_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit)); } +static inline int Gia_ManCiLit( Gia_Man_t * p, int CiId ) { return Gia_Obj2Lit( p, Gia_ManCi(p, CiId) ); } static inline int Gia_ManIdToCioId( Gia_Man_t * p, int Id ) { return Gia_ObjCioId( Gia_ManObj(p, Id) ); } static inline int Gia_ManCiIdToId( Gia_Man_t * p, int CiId ) { return Gia_ObjId( p, Gia_ManCi(p, CiId) ); } @@ -897,13 +898,15 @@ extern Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupOutputGroup( Gia_Man_t * p, int iOutStart, int iOutStop ); extern Gia_Man_t * Gia_ManDupOutputVec( Gia_Man_t * p, Vec_Int_t * vOutPres ); extern Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p ); +extern Gia_Man_t * Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis ); extern Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState ); -extern Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * pAig, int nFrames ); +extern Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * pAig, Abc_Cex_t * pCex, int nFrames ); extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm ); extern void Gia_ManDupAppend( Gia_Man_t * p, Gia_Man_t * pTwo ); extern void Gia_ManDupAppendShare( Gia_Man_t * p, Gia_Man_t * pTwo ); extern Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo ); +extern Gia_Man_t * Gia_ManDupAppendCones( Gia_Man_t * p, Gia_Man_t ** ppCones, int nCones, int fOnlyRegs ); extern Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass ); extern Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 2c7fd59b..d533dc1f 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -383,6 +383,36 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p ) return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates AIG while putting first PIs, then nodes, then POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + assert( Gia_ManRegNum(p) == 0 ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = (i < Gia_ManCiNum(p) - nLastPis) ? ~0 : Gia_ManAppendCi(pNew); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + return pNew; +} + /**Function************************************************************* Synopsis [Duplicates AIG while complementing the flops.] @@ -438,16 +468,17 @@ Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState ) SeeAlso [] ***********************************************************************/ -void Gia_ManCycle( Gia_Man_t * p, int nFrames ) +void Gia_ManCycle( Gia_Man_t * p, Abc_Cex_t * pCex, int nFrames ) { Gia_Obj_t * pObj, * pObjRi, * pObjRo; int i, k; Gia_ManRandom( 1 ); + assert( pCex == NULL || nFrames <= pCex->iFrame ); // iterate for the given number of frames for ( i = 0; i < nFrames; i++ ) { Gia_ManForEachPi( p, pObj, k ) - pObj->fMark0 = (1 & Gia_ManRandom(0)); + pObj->fMark0 = pCex ? Abc_InfoHasBit(pCex->pData, pCex->nRegs+i*pCex->nPis+k) : (1 & Gia_ManRandom(0)); Gia_ManForEachAnd( p, pObj, k ) pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); @@ -457,14 +488,14 @@ void Gia_ManCycle( Gia_Man_t * p, int nFrames ) pObjRo->fMark0 = pObjRi->fMark0; } } -Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * p, int nFrames ) +Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * p, Abc_Cex_t * pCex, int nFrames ) { Gia_Man_t * pNew; Vec_Bit_t * vInits; Gia_Obj_t * pObj; int i; Gia_ManCleanMark0(p); - Gia_ManCycle( p, nFrames ); + Gia_ManCycle( p, pCex, nFrames ); vInits = Vec_BitAlloc( Gia_ManRegNum(p) ); Gia_ManForEachRo( p, pObj, i ) Vec_BitPush( vInits, pObj->fMark0 ); @@ -649,6 +680,60 @@ Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo ) return pNew; } +/**Function************************************************************* + + Synopsis [Appends logic cones as additional property outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupAppendCones( Gia_Man_t * p, Gia_Man_t ** ppCones, int nCones, int fOnlyRegs ) +{ + Gia_Man_t * pNew, * pOne; + Gia_Obj_t * pObj; + int i, k; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManHashAlloc( pNew ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachPo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + for ( k = 0; k < nCones; k++ ) + { + pOne = ppCones[k]; + assert( Gia_ManPoNum(pOne) == 1 ); + assert( Gia_ManRegNum(pOne) == 0 ); + if ( fOnlyRegs ) + assert( Gia_ManPiNum(pOne) == Gia_ManRegNum(p) ); + else + assert( Gia_ManPiNum(pOne) == Gia_ManCiNum(p) ); + Gia_ManConst0(pOne)->Value = 0; + Gia_ManForEachPi( pOne, pObj, i ) + pObj->Value = Gia_ManCiLit( pNew, fOnlyRegs ? Gia_ManPiNum(p) + i : i ); + Gia_ManForEachAnd( pOne, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachPo( pOne, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + Gia_ManForEachRi( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + pNew = Gia_ManCleanup( pOne = pNew ); + Gia_ManStop( pOne ); + return pNew; +} + + /**Function************************************************************* Synopsis [Duplicates while adding self-loops to the registers.] diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 8670993d..5738595b 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -245,11 +245,15 @@ void Gia_ManPrintTents( Gia_Man_t * p ) printf( "Tents: " ); for ( t = 1; nSizePrev < Vec_IntSize(vObjs); t++ ) { + int nPis = 0; nSizeCurr = Vec_IntSize(vObjs); Vec_IntForEachEntryStartStop( vObjs, iObjId, i, nSizePrev, nSizeCurr ) + { + nPis += Gia_ObjIsPi(p, Gia_ManObj(p, iObjId)); if ( Gia_ObjIsRo(p, Gia_ManObj(p, iObjId)) ) Gia_ManPrintTents_rec( p, Gia_ObjRoToRi(p, Gia_ManObj(p, iObjId)), vObjs ); - printf( "%d=%d ", t, nSizeCurr - nSizePrev ); + } + printf( "%d=%d(%d) ", t, nSizeCurr - nSizePrev, nPis ); nSizePrev = nSizeCurr; } printf( " Unused=%d\n", Gia_ManObjNum(p) - Vec_IntSize(vObjs) ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d28a59ea..f8404f19 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -21460,7 +21460,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) } } vStatuses = Abc_FrameDeriveStatusArray( vSeqModelVec ); - Abc_FrameReplacePoStatuses( pAbc, &vStatuses ); + Abc_FrameReplacePoStatuses( pAbc, &vStatuses ); if ( vSeqModelVec ) Abc_FrameReplaceCexVec( pAbc, &vSeqModelVec ); else @@ -23013,11 +23013,11 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) // run the procedure pAbc->Status = Abc_NtkDarPdr( pNtk, pPars ); pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame; + Abc_FrameReplacePoStatuses( pAbc, &pPars->vOutMap ); if ( pNtk->vSeqModelVec ) Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec ); else Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); - Abc_FrameReplacePoStatuses( pAbc, &pPars->vOutMap ); return 0; usage: @@ -30250,9 +30250,9 @@ usage: int Abc_CommandAbc9Cycle( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pTemp; - int c, nFrames = 10, fVerbose = 0; + int c, nFrames = 10, fUseCex = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Fcvh" ) ) != EOF ) { switch ( c ) { @@ -30267,6 +30267,9 @@ int Abc_CommandAbc9Cycle( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nFrames < 0 ) goto usage; break; + case 'c': + fUseCex ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -30281,15 +30284,16 @@ int Abc_CommandAbc9Cycle( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Cycle(): There is no AIG.\n" ); return 1; } - pTemp = Gia_ManDupCycled( pAbc->pGia, nFrames ); + pTemp = Gia_ManDupCycled( pAbc->pGia, fUseCex ? pAbc->pCex : NULL, nFrames ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: - Abc_Print( -2, "usage: &cycle [-F num] [-vh]\n" ); + Abc_Print( -2, "usage: &cycle [-F num] [-cvh]\n" ); Abc_Print( -2, "\t cycles sequential circuit for the given number of timeframes\n" ); Abc_Print( -2, "\t to derive a new initial state (which may be on the envelope)\n" ); Abc_Print( -2, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames ); + Abc_Print( -2, "\t-c : toggle using PI values from the current CEX [default = %s]\n", fUseCex? "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; @@ -31934,6 +31938,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pTemp = NULL; int c, fVerbose = 0; + int nFrames = 3; int fSwitch = 0; // extern Gia_Man_t * Gia_VtaTest( Gia_Man_t * p ); // extern int Gia_ManSuppSizeTest( Gia_Man_t * p ); @@ -31947,13 +31952,26 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern int Gia_ManVerify( Gia_Man_t * pGia ); // extern Gia_Man_t * Gia_ManOptimizeRing( Gia_Man_t * p ); // extern void Gia_ManCollectSeqTest( Gia_Man_t * p ); - extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose ); +// extern Gia_Man_t * Gia_SweeperFraigTest( Gia_Man_t * p, int nWords, int nConfs, int fVerbose ); + extern Gia_Man_t * Bmc_CexDepthTest( Gia_Man_t * p, Abc_Cex_t * pCex, int nFrames, int fVerbose ); + extern Gia_Man_t * Bmc_CexTarget( Gia_Man_t * p, int nFrames ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Fsvh" ) ) != EOF ) { switch ( c ) { + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nFrames = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFrames < 0 ) + goto usage; + break; case 's': fSwitch ^= 1; break; @@ -32001,12 +32019,16 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // Gia_ManVerifyWithBoxes( pAbc->pGia ); // Gia_ManCollectSeqTest( pAbc->pGia ); // pTemp = Gia_ManOptimizeRing( pAbc->pGia ); - pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 ); +// pTemp = Gia_SweeperFraigTest( pAbc->pGia, 4, 1000, 0 ); +// Abc_FrameUpdateGia( pAbc, pTemp ); + pTemp = Bmc_CexDepthTest( pAbc->pGia, pAbc->pCex, nFrames, fVerbose ); +// pTemp = Bmc_CexTarget( pAbc->pGia, nFrames ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: - Abc_Print( -2, "usage: &test [-svh]\n" ); + Abc_Print( -2, "usage: &test [-F num] [-svh]\n" ); Abc_Print( -2, "\t testing various procedures\n" ); + Abc_Print( -2, "\t-F num: the number of timeframes [default = %d]\n", nFrames ); Abc_Print( -2, "\t-s : toggle enable (yes) vs. disable (no) [default = %s]\n", fSwitch? "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"); diff --git a/src/sat/bmc/bmcCexDepth.c b/src/sat/bmc/bmcCexDepth.c new file mode 100644 index 00000000..b28a7ba7 --- /dev/null +++ b/src/sat/bmc/bmcCexDepth.c @@ -0,0 +1,421 @@ +/**CFile**************************************************************** + + FileName [bmcCexDepth.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT-based bounded model checking.] + + Synopsis [CEX depth minimization.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: bmcCexDepth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "bmc.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern Abc_Cex_t * Bmc_CexInnerStates( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t ** ppCexImpl, int fVerbose ); +extern Abc_Cex_t * Bmc_CexCareBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexImpl, Abc_Cex_t * pCexEss, int fFindAll, int fVerbose ); +extern int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +/**Function************************************************************* + + Synopsis [Existentially quantified given variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupExist( Gia_Man_t * p, int iVar ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i; + assert( iVar >= 0 && iVar < Gia_ManPiNum(p) ); + assert( Gia_ManPoNum(p) == 1 ); + assert( Gia_ManRegNum(p) == 0 ); + Gia_ManFillValue( p ); + // find the cofactoring variable + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManHashAlloc( pNew ); + // compute negative cofactor + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 1 ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachPo( p, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + // compute the positive cofactor + Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 0 ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + // create OR gate + Gia_ManForEachPo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashOr(pNew, pObj->Value, Gia_ObjFanin0Copy(pObj)) ); + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Performs targe enlargement of the given size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Bmc_CexTargetEnlarge( Gia_Man_t * p, int nFrames ) +{ + Gia_Man_t * pNew, * pOne; + Gia_Obj_t * pObj, * pObjRo; + int i, k; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManHashAlloc( pNew ); + Gia_ManConst0(p)->Value = 0; + for ( k = 0; k < nFrames; k++ ) + Gia_ManForEachPi( p, pObj, i ) + Gia_ManAppendCi( pNew ); + Gia_ManForEachRo( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + for ( k = 0; k < nFrames; k++ ) + { + Gia_ManForEachPi( p, pObj, i ) + pObj->Value = Gia_ManCiLit( pNew, (nFrames - 1 - k) * Gia_ManPiNum(p) + i ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachRi( p, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + Gia_ManForEachRiRo( p, pObj, pObjRo, i ) + pObjRo->Value = pObj->Value; + } + pObj = Gia_ManPo( p, 0 ); + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pOne = pNew ); + Gia_ManStop( pOne ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Create target with quantified inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Bmc_CexTarget( Gia_Man_t * p, int nFrames ) +{ + Gia_Man_t * pNew, * pTemp; + int i, Limit = nFrames * Gia_ManPiNum(p); + pNew = Bmc_CexTargetEnlarge( p, nFrames ); + for ( i = 0; i < Limit; i++ ) + { + printf( "%3d : ", i ); + if ( i % Gia_ManPiNum(p) == 0 ) + Gia_ManPrintStats( pNew, 0, 0, 0 ); + pNew = Gia_ManDupExist( pTemp = pNew, i ); + Gia_ManStop( pTemp ); + } + Gia_ManPrintStats( pNew, 0, 0, 0 ); + pNew = Gia_ManDupLastPis( pTemp = pNew, Gia_ManRegNum(p) ); + Gia_ManStop( pTemp ); + Gia_ManPrintStats( pNew, 0, 0, 0 ); + pTemp = Gia_ManDupAppendCones( p, &pNew, 1, 1 ); + Gia_ManStop( pNew ); + Gia_AigerWrite( pTemp, "miter3.aig", 0, 0 ); + return pTemp; +} + +/**Function************************************************************* + + Synopsis [Computes CE-induced network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Bmc_CexBuildNetwork2( Gia_Man_t * p, Abc_Cex_t * pCex, int fStart ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, * pObjRo, * pObjRi; + int fCompl0, fCompl1; + int i, k, iBit; + assert( pCex->nRegs == 0 ); + assert( pCex->nPis == Gia_ManCiNum(p) ); + assert( fStart <= pCex->iFrame ); + // start the manager + pNew = Gia_ManStart( 1000 ); + pNew->pName = Abc_UtilStrsav( "unate" ); + // set const0 + Gia_ManConst0(p)->fMark0 = 0; // value + Gia_ManConst0(p)->fMark1 = 1; // care + Gia_ManConst0(p)->Value = ~0; + // set init state + Gia_ManForEachRi( p, pObj, k ) + { + pObj->fMark0 = Abc_InfoHasBit( pCex->pData, pCex->nRegs + fStart * Gia_ManCiNum(p) + Gia_ManPiNum(p) + k ); + pObj->fMark1 = 0; + pObj->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObj->fMark0 ); + } + Gia_ManHashAlloc( pNew ); + iBit = pCex->nRegs + fStart * Gia_ManCiNum(p); + for ( i = fStart; i <= pCex->iFrame; i++ ) + { + // primary inputs + Gia_ManForEachPi( p, pObj, k ) + { + pObj->fMark0 = Abc_InfoHasBit( pCex->pData, iBit++ ); + pObj->fMark1 = 1; + pObj->Value = ~0; + } + iBit += Gia_ManRegNum(p); + // transfer + Gia_ManForEachRiRo( p, pObjRi, pObjRo, k ) + { + pObjRo->fMark0 = pObjRi->fMark0; + pObjRo->fMark1 = pObjRi->fMark1; + pObjRo->Value = pObjRi->Value; + } + // internal nodes + Gia_ManForEachAnd( p, pObj, k ) + { + fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj); + pObj->fMark0 = fCompl0 & fCompl1; + if ( pObj->fMark0 ) + pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 & Gia_ObjFanin1(pObj)->fMark1; + else if ( !fCompl0 && !fCompl1 ) + pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1; + else if ( !fCompl0 ) + pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1; + else if ( !fCompl1 ) + pObj->fMark1 = Gia_ObjFanin1(pObj)->fMark1; + else assert( 0 ); + pObj->Value = ~0; + if ( pObj->fMark1 ) + continue; + if ( pObj->fMark0 ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); + else if ( !fCompl0 && !fCompl1 ) + pObj->Value = Gia_ManHashOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); + else if ( !fCompl0 ) + pObj->Value = Gia_ObjFanin0(pObj)->Value; + else if ( !fCompl1 ) + pObj->Value = Gia_ObjFanin1(pObj)->Value; + else assert( 0 ); + assert( pObj->Value > 0 ); + } + // combinational outputs + Gia_ManForEachCo( p, pObj, k ) + { + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1; + pObj->Value = Gia_ObjFanin0(pObj)->Value; + } + } + Gia_ManHashStop( pNew ); + assert( iBit == pCex->nBits ); + // create primary output + pObj = Gia_ManPo(p, pCex->iPo); + assert( pObj->fMark0 == 1 ); + assert( pObj->fMark1 == 0 ); + assert( pObj->Value > 0 ); + Gia_ManAppendCo( pNew, pObj->Value ); + // cleanup + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} +Gia_Man_t * Bmc_CexBuildNetwork2_( Gia_Man_t * p, Abc_Cex_t * pCex, int fStart ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, * pObjRo, * pObjRi; + int fCompl0, fCompl1; + int i, k, iBit; + assert( pCex->nRegs == 0 ); + assert( pCex->nPis == Gia_ManCiNum(p) ); + assert( fStart <= pCex->iFrame ); + // start the manager + pNew = Gia_ManStart( 1000 ); + pNew->pName = Abc_UtilStrsav( "unate" ); + // set const0 + Gia_ManConst0(p)->fMark0 = 0; // value + Gia_ManConst0(p)->Value = 1; + // set init state + Gia_ManForEachRi( p, pObj, k ) + { + pObj->fMark0 = Abc_InfoHasBit( pCex->pData, pCex->nRegs + fStart * Gia_ManCiNum(p) + Gia_ManPiNum(p) + k ); + pObj->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObj->fMark0 ); + } + Gia_ManHashAlloc( pNew ); + iBit = pCex->nRegs + fStart * Gia_ManCiNum(p); + for ( i = fStart; i <= pCex->iFrame; i++ ) + { + // primary inputs + Gia_ManForEachPi( p, pObj, k ) + { + pObj->fMark0 = Abc_InfoHasBit( pCex->pData, iBit++ ); + pObj->Value = 1; + } + iBit += Gia_ManRegNum(p); + // transfer + Gia_ManForEachRiRo( p, pObjRi, pObjRo, k ) + { + pObjRo->fMark0 = pObjRi->fMark0; + pObjRo->Value = pObjRi->Value; + } + // internal nodes + Gia_ManForEachAnd( p, pObj, k ) + { + fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj); + pObj->fMark0 = fCompl0 & fCompl1; + if ( pObj->fMark0 ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); + else if ( !fCompl0 && !fCompl1 ) + pObj->Value = Gia_ManHashOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); + else if ( !fCompl0 ) + pObj->Value = Gia_ObjFanin0(pObj)->Value; + else if ( !fCompl1 ) + pObj->Value = Gia_ObjFanin1(pObj)->Value; + else assert( 0 ); + } + // combinational outputs + Gia_ManForEachCo( p, pObj, k ) + { + pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); + pObj->Value = Gia_ObjFanin0(pObj)->Value; + } + } + Gia_ManHashStop( pNew ); + assert( iBit == pCex->nBits ); + // create primary output + pObj = Gia_ManPo(p, pCex->iPo); + assert( pObj->fMark0 == 1 ); + assert( pObj->Value > 0 ); + Gia_ManAppendCo( pNew, pObj->Value ); + // cleanup + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + +Gia_Man_t * Bmc_CexBuildNetwork2Test( Gia_Man_t * p, Abc_Cex_t * pCex, int nFramesMax ) +{ + Gia_Man_t * pNew, * pTemp; + Vec_Ptr_t * vCones; + clock_t clk = clock(); + int i; + nFramesMax = Abc_MinInt( nFramesMax, pCex->iFrame ); + printf( "Processing CEX in frame %d (max frames %d).\n", pCex->iFrame, nFramesMax ); + vCones = Vec_PtrAlloc( nFramesMax ); + for ( i = pCex->iFrame; i > pCex->iFrame - nFramesMax; i-- ) + { + printf( "Frame %5d : ", i ); + pNew = Bmc_CexBuildNetwork2_( p, pCex, i ); + Gia_ManPrintStats( pNew, 0, 0, 0 ); + Vec_PtrPush( vCones, pNew ); + } + pNew = Gia_ManDupAppendCones( p, (Gia_Man_t **)Vec_PtrArray(vCones), Vec_PtrSize(vCones), 1 ); + Gia_AigerWrite( pNew, "miter2.aig", 0, 0 ); +//Bmc_CexDumpAogStats( pNew, clock() - clk ); + Vec_PtrForEachEntry( Gia_Man_t *, vCones, pTemp, i ) + Gia_ManStop( pTemp ); + Vec_PtrFree( vCones ); + printf( "GIA with additional properties is written into \"miter2.aig\".\n" ); +// printf( "CE-induced network is written into file \"unate.aig\".\n" ); + Abc_PrintTime( 1, "Time", clock() - clk ); +// Gia_ManStop( pNew ); + return pNew; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Bmc_CexDepthTest( Gia_Man_t * p, Abc_Cex_t * pCex, int nFrames, int fVerbose ) +{ + Gia_Man_t * pNew; + clock_t clk = clock(); + Abc_Cex_t * pCexImpl = NULL; + Abc_Cex_t * pCexStates = Bmc_CexInnerStates( p, pCex, &pCexImpl, fVerbose ); + Abc_Cex_t * pCexCare = Bmc_CexCareBits( p, pCexStates, pCexImpl, NULL, 1, fVerbose ); +// Abc_Cex_t * pCexEss, * pCexMin; + + if ( !Bmc_CexVerify( p, pCex, pCexCare ) ) + printf( "Counter-example care-set verification has failed.\n" ); + +// pCexEss = Bmc_CexEssentialBits( p, pCexStates, pCexCare, fVerbose ); +// pCexMin = Bmc_CexCareBits( p, pCexStates, pCexImpl, pCexEss, 0, fVerbose ); + +// if ( !Bmc_CexVerify( p, pCex, pCexMin ) ) +// printf( "Counter-example min-set verification has failed.\n" ); + +// Bmc_CexDumpStats( p, pCex, pCexCare, pCexEss, pCexMin, clock() - clk ); + + Abc_PrintTime( 1, "Time", clock() - clk ); + pNew = Bmc_CexBuildNetwork2Test( p, pCexStates, nFrames ); +// Bmc_CexPerformUnrollingTest( p, pCex ); + + Abc_CexFreeP( &pCexStates ); + Abc_CexFreeP( &pCexImpl ); + Abc_CexFreeP( &pCexCare ); +// Abc_CexFreeP( &pCexEss ); +// Abc_CexFreeP( &pCexMin ); + return pNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make index fd50ec23..1ac04203 100644 --- a/src/sat/bmc/module.make +++ b/src/sat/bmc/module.make @@ -2,6 +2,7 @@ SRC += src/sat/bmc/bmcBmc.c \ src/sat/bmc/bmcBmc2.c \ src/sat/bmc/bmcBmc3.c \ src/sat/bmc/bmcCexCut.c \ + src/sat/bmc/bmcCexDepth.c \ src/sat/bmc/bmcCexMin1.c \ src/sat/bmc/bmcCexMin2.c \ src/sat/bmc/bmcCexTools.c \ -- cgit v1.2.3