Skip to content

A
abc
Commit 28e065b0 by Alan Mishchenko
Options

Counter-example depth minimization.

parent b7d670ec
Showing with 130 additions and 15 deletions
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 );
......
src/aig/gia/giaDup.c
......@@ -385,6 +385,36 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p )
/**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.]
Description [The array of initial state contains the init state
......@@ -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 );
......@@ -651,6 +682,60 @@ Gia_Man_t * Gia_ManDupAppendNew( Gia_Man_t * pOne, Gia_Man_t * pTwo )
/**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.]
Description []
......
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) );
......
src/base/abci/abc.c
......@@ -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");
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 \
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment