Skip to content

A
abc
Commit ec298486 by Alan Mishchenko
Options

False path detection.

parent 34366b8a
Showing with 217 additions and 56 deletions
src/aig/gia/giaFalse.c
......@@ -20,6 +20,7 @@
#include "gia.h"
#include "misc/vec/vecQue.h"
#include "misc/vec/vecWec.h"
#include "sat/bsat/satStore.h"
ABC_NAMESPACE_IMPL_START
......@@ -35,7 +36,7 @@ ABC_NAMESPACE_IMPL_START
/**Function*************************************************************
Synopsis [Compute slacks measured using the number of AIG levels.]
Synopsis [Reconstruct the AIG after detecting false paths.]
Description []
......@@ -44,17 +45,60 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManComputeSlacks( Gia_Man_t * p )
void Gia_ManFalseRebuildOne( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vHook, int fVerbose, int fVeryVerbose )
{
Gia_Obj_t * pObj, * pPrev = NULL;
int i, iObjValue, iPrevValue = -1;
if ( fVerbose )
{
printf( "Eliminating path: " );
Vec_IntPrint( vHook );
}
Gia_ManForEachObjVec( vHook, p, pObj, i )
{
if ( fVeryVerbose )
Gia_ObjPrint( p, pObj );
iObjValue = pObj->Value;
pObj->Value = i ? Gia_ManHashAnd(pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj)) : 0;
if ( pPrev )
pPrev->Value = iPrevValue;
iPrevValue = iObjValue;
pPrev = pObj;
}
}
Gia_Man_t * Gia_ManFalseRebuild( Gia_Man_t * p, Vec_Wec_t * vHooks, int fVerbose, int fVeryVerbose )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, nLevels = Gia_ManLevelNum( p );
Vec_Int_t * vLevelR = Gia_ManReverseLevel( p );
Vec_Int_t * vSlacks = Vec_IntAlloc( Gia_ManObjNum(p) );
Gia_ManForEachObj( p, pObj, i )
Vec_IntPush( vSlacks, nLevels - Gia_ObjLevelId(p, i) - Vec_IntEntry(vLevelR, i) );
assert( Vec_IntSize(vSlacks) == Gia_ManObjNum(p) );
Vec_IntFree( vLevelR );
return vSlacks;
int i, Counter = 0;
pNew = Gia_ManStart( 4 * Gia_ManObjNum(p) / 3 );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManConst0(p)->Value = 0;
Gia_ManHashAlloc( pNew );
Gia_ManForEachObj1( p, pObj, i )
{
if ( Gia_ObjIsAnd(pObj) )
{
if ( Vec_WecLevelSize(vHooks, i) > 0 )
{
if ( fVerbose )
printf( "Path %d : ", Counter++ );
Gia_ManFalseRebuildOne( pNew, p, Vec_WecEntry(vHooks, i), fVerbose, fVeryVerbose );
}
else
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
else if ( Gia_ObjIsCi(pObj) )
pObj->Value = Gia_ManAppendCi( pNew );
else if ( Gia_ObjIsCo(pObj) )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
}
Gia_ManHashStop( pNew );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
......@@ -68,26 +112,25 @@ Vec_Int_t * Gia_ManComputeSlacks( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
void Gia_ManCollectPath_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSlacks, Vec_Int_t * vPath )
void Gia_ManCollectPath_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPath )
{
if ( Gia_ObjIsAnd(pObj) )
{
int Slack = Vec_IntEntry(vSlacks, Gia_ObjId(p, pObj));
int Slack0 = Vec_IntEntry(vSlacks, Gia_ObjFaninId0p(p, pObj));
int Slack1 = Vec_IntEntry(vSlacks, Gia_ObjFaninId1p(p, pObj));
assert( Slack == Slack0 || Slack == Slack1 );
if ( Slack == Slack0 )
Gia_ManCollectPath_rec( p, Gia_ObjFanin0(pObj), vSlacks, vPath );
if ( Gia_ObjLevel(p, Gia_ObjFanin0(pObj)) > Gia_ObjLevel(p, Gia_ObjFanin1(pObj)) )
Gia_ManCollectPath_rec( p, Gia_ObjFanin0(pObj), vPath );
else if ( Gia_ObjLevel(p, Gia_ObjFanin0(pObj)) < Gia_ObjLevel(p, Gia_ObjFanin1(pObj)) )
Gia_ManCollectPath_rec( p, Gia_ObjFanin1(pObj), vPath );
// else if ( rand() & 1 )
// Gia_ManCollectPath_rec( p, Gia_ObjFanin0(pObj), vPath );
else
Gia_ManCollectPath_rec( p, Gia_ObjFanin1(pObj), vSlacks, vPath );
Gia_ManCollectPath_rec( p, Gia_ObjFanin1(pObj), vPath );
}
Vec_IntPush( vPath, Gia_ObjId(p, pObj) );
}
Vec_Int_t * Gia_ManCollectPath( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSlacks )
Vec_Int_t * Gia_ManCollectPath( Gia_Man_t * p, Gia_Obj_t * pObj )
{
Vec_Int_t * vPath = Vec_IntAlloc( p->nLevels );
assert( Gia_ObjIsCo(pObj) );
Gia_ManCollectPath_rec( p, Gia_ObjFanin0(pObj), vSlacks, vPath );
Gia_ManCollectPath_rec( p, Gia_ObjFanin0(pObj), vPath );
return vPath;
}
......@@ -102,19 +145,22 @@ Vec_Int_t * Gia_ManCollectPath( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSl
SeeAlso []
***********************************************************************/
void Gia_ManCheckFalseOne( Gia_Man_t * p, int iOut, int nTimeOut, Vec_Int_t * vSlacks )
void Gia_ManCheckFalseOne( Gia_Man_t * p, int iOut, int nTimeOut, Vec_Wec_t * vHooks, int fVerbose, int fVeryVerbose )
{
sat_solver * pSat;
Gia_Obj_t * pObj = Gia_ManCo( p, iOut );
Gia_Obj_t * pObj;
Gia_Obj_t * pPivot = Gia_ManCo( p, iOut );
Vec_Int_t * vLits = Vec_IntAlloc( p->nLevels );
Vec_Int_t * vPath = Gia_ManCollectPath( p, pObj, vSlacks );
int i, Shift[2], status, nLits, * pLits;
Vec_Int_t * vPath = Gia_ManCollectPath( p, pPivot );
int nLits = 0, * pLits = NULL;
int i, Shift[2], status;
abctime clkStart = Abc_Clock();
// collect objects and assign SAT variables
int iFanin = Gia_ObjFaninId0p( p, pObj );
int iFanin = Gia_ObjFaninId0p( p, pPivot );
Vec_Int_t * vObjs = Gia_ManCollectNodesCis( p, &iFanin, 1 );
Gia_ManForEachObjVec( vObjs, p, pObj, i )
pObj->Value = Vec_IntSize(vObjs) - 1 - i;
assert( Gia_ObjIsCo(pPivot) );
// create SAT solver
pSat = sat_solver_new();
sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
......@@ -139,74 +185,85 @@ void Gia_ManCheckFalseOne( Gia_Man_t * p, int iOut, int nTimeOut, Vec_Int_t * vS
Gia_ObjFanin0(pObj)->Value + Shift[1], Gia_ObjFanin1(pObj)->Value + Shift[1],
Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj) );
}
printf( "PO %6d : ", iOut );
// call the SAT solver
status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( status == l_False )
{
int iBeg, iEnd;
nLits = sat_solver_final( pSat, &pLits );
iBeg = Abc_Lit2Var(pLits[nLits-1]);
iEnd = Abc_Lit2Var(pLits[0]);
if ( iEnd - iBeg < 20 )
{
// check if nodes on the path are already used
for ( i = iBeg; i <= iEnd; i++ )
if ( Vec_WecLevelSize(vHooks, Vec_IntEntry(vPath, i)) > 0 )
break;
if ( i > iEnd )
{
Vec_Int_t * vHook = Vec_WecEntry(vHooks, Vec_IntEntry(vPath, iEnd));
for ( i = iBeg; i <= iEnd; i++ )
Vec_IntPush( vHook, Vec_IntEntry(vPath, i) );
}
}
}
if ( fVerbose )
{
printf( "PO %6d : Level = %3d ", iOut, Gia_ObjLevel(p, pPivot) );
if ( status == l_Undef )
printf( "Timeout reached after %d seconds. ", nTimeOut );
else if ( status == l_True )
printf( "There is no false path. " );
else
{
assert( status == l_False );
// call analize_final
nLits = sat_solver_final( pSat, &pLits );
printf( "False path contains %d nodes (out of %d): ", nLits, Vec_IntSize(vLits) );
printf( "top = %d ", Vec_IntEntry(vPath, Abc_Lit2Var(pLits[0])) );
if ( fVeryVerbose )
for ( i = 0; i < nLits; i++ )
printf( "%d ", Abc_Lit2Var(pLits[i]) );
printf( " " );
}
Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
}
sat_solver_delete( pSat );
Vec_IntFree( vObjs );
Vec_IntFree( vPath );
Vec_IntFree( vLits );
}
void Gia_ManCheckFalse( Gia_Man_t * p, int nSlackMax, int nTimeOut )
Gia_Man_t * Gia_ManCheckFalse( Gia_Man_t * p, int nSlackMax, int nTimeOut, int fVerbose, int fVeryVerbose )
{
Gia_Man_t * pNew;
Vec_Wec_t * vHooks;
Vec_Que_t * vPrio;
Vec_Flt_t * vWeights;
Vec_Int_t * vSlacks;
Gia_Obj_t * pObj;
int i;
vSlacks = Gia_ManComputeSlacks(p);
//Vec_IntPrint( vSlacks );
srand( 111 );
Gia_ManLevelNum( p );
// create PO weights
vWeights = Vec_FltAlloc( Gia_ManCoNum(p) );
Gia_ManForEachCo( p, pObj, i )
Vec_FltPush( vWeights, p->nLevels - Vec_IntEntry(vSlacks, Gia_ObjId(p, pObj)) );
Vec_FltPush( vWeights, Gia_ObjLevel(p, pObj) );
// put POs into the queue
vPrio = Vec_QueAlloc( Gia_ManCoNum(p) );
Vec_QueSetPriority( vPrio, Vec_FltArrayP(vWeights) );
Gia_ManForEachCo( p, pObj, i )
Vec_QuePush( vPrio, i );
// work on each PO in the queue
vHooks = Vec_WecStart( Gia_ManObjNum(p) );
while ( Vec_QueTopPriority(vPrio) >= p->nLevels - nSlackMax )
Gia_ManCheckFalseOne( p, Vec_QuePop(vPrio), nTimeOut, vSlacks );
Gia_ManCheckFalseOne( p, Vec_QuePop(vPrio), nTimeOut, vHooks, fVerbose, fVeryVerbose );
if ( fVerbose )
printf( "Collected %d non-overlapping false paths.\n", Vec_WecSizeUsed(vHooks) );
// reconstruct the AIG
pNew = Gia_ManFalseRebuild( p, vHooks, fVerbose, fVeryVerbose );
// cleanup
Vec_IntFree( vSlacks );
Vec_WecFree( vHooks );
Vec_FltFree( vWeights );
Vec_QueFree( vPrio );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManCheckFalseTest( Gia_Man_t * p, int nSlackMax )
{
Gia_ManCheckFalse( p, nSlackMax, 0 );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/aig/gia/giaUtil.c
......@@ -621,6 +621,30 @@ Vec_Int_t * Gia_ManRequiredLevel( Gia_Man_t * p )
/**Function*************************************************************
Synopsis [Compute slacks measured using the number of AIG levels.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManComputeSlacks( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, nLevels = Gia_ManLevelNum( p );
Vec_Int_t * vLevelR = Gia_ManReverseLevel( p );
Vec_Int_t * vSlacks = Vec_IntAlloc( Gia_ManObjNum(p) );
Gia_ManForEachObj( p, pObj, i )
Vec_IntPush( vSlacks, nLevels - Gia_ObjLevelId(p, i) - Vec_IntEntry(vLevelR, i) );
assert( Vec_IntSize(vSlacks) == Gia_ManObjNum(p) );
Vec_IntFree( vLevelR );
return vSlacks;
}
/**Function*************************************************************
Synopsis [Assigns levels.]
Description []
......
src/base/abci/abc.c
......@@ -355,6 +355,7 @@ static int Abc_CommandAbc9Balance ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Syn2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Syn3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Syn4 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9False ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Miter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Miter2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Append ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -920,6 +921,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&syn2", Abc_CommandAbc9Syn2, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&syn3", Abc_CommandAbc9Syn3, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&syn4", Abc_CommandAbc9Syn4, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&false", Abc_CommandAbc9False, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&miter", Abc_CommandAbc9Miter, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&miter2", Abc_CommandAbc9Miter2, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&append", Abc_CommandAbc9Append, 0 );
......@@ -27790,6 +27792,84 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9False( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_ManCheckFalse( Gia_Man_t * p, int nSlackMax, int nTimeOut, int fVerbose, int fVeryVerbose );
Gia_Man_t * pTemp;
int nSlackMax = 0;
int nTimeOut = 0;
int c, fVerbose = 0;
int fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "STvwh" ) ) != EOF )
{
switch ( c )
{
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by a char string.\n" );
goto usage;
}
nSlackMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nSlackMax < 0 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by a char string.\n" );
goto usage;
}
nTimeOut = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nTimeOut < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
case 'w':
fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9False(): There is no AIG.\n" );
return 1;
}
pTemp = Gia_ManCheckFalse( pAbc->pGia, nSlackMax, nTimeOut, fVerbose, fVeryVerbose );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &false [-ST num] [-vwh]\n" );
Abc_Print( -2, "\t detecting and elimintation false paths\n" );
Abc_Print( -2, "\t-S num : maximum slack to idetify false paths [default = %d]\n", nSlackMax );
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nTimeOut );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing additional information [default = %s]\n", fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pFile;
......@@ -34003,7 +34083,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern Gia_Man_t * Llb_ReachableStatesGia( Gia_Man_t * p );
// extern Gia_Man_t * Unm_ManTest( Gia_Man_t * pGia );
// extern void Agi_ManTest( Gia_Man_t * pGia );
extern void Gia_ManCheckFalseTest( Gia_Man_t * p, int nSlackMax );
// extern void Gia_ManCheckFalseTest( Gia_Man_t * p, int nSlackMax );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Fsvh" ) ) != EOF )
......@@ -34083,7 +34163,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// Agi_ManTest( pAbc->pGia );
// Gia_ManResubTest( pAbc->pGia );
// Jf_ManTestCnf( pAbc->pGia );
Gia_ManCheckFalseTest( pAbc->pGia, nFrames );
// Gia_ManCheckFalseTest( pAbc->pGia, nFrames );
return 0;
usage:
Abc_Print( -2, "usage: &test [-F num] [-svh]\n" );
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