mirror of https://github.com/YosysHQ/abc.git
Adding procedures to find the care bits of a counter-example.
This commit is contained in:
Alan Mishchenko
parent
67e84b719d
commit
e7a5a74b4c
|
|
@ -3547,6 +3547,10 @@ 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
|
||||
|
|
|
|||
|
|
@ -14,6 +14,7 @@ SRC += src/aig/saig/saigAbs.c \
|
|||
src/aig/saig/saigOutDec.c \
|
||||
src/aig/saig/saigPba.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 \
|
||||
|
|
|
|||
|
|
@ -175,6 +175,8 @@ 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 Abc_Cex_t * Saig_ManRefineCexSat( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, 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 );
|
||||
|
|
|
|||
|
|
@ -0,0 +1,429 @@
|
|||
/**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 "saig.h"
|
||||
#include "cnf.h"
|
||||
#include "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 * vMapPiA3F; // mapping of frame PIs into real PIs
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**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_ObjIsPo(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 ** pvMapPiA3F )
|
||||
{
|
||||
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
|
||||
*pvMapPiA3F = 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_ManPo( 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_Int_t *)Vec_VecEntry( vFrameCos, f );
|
||||
Aig_ManForEachNodeVec( pAig, vRoots, pObj, i )
|
||||
Saig_ManUnrollCollect_rec( pAig, pObj,
|
||||
(Vec_Int_t *)Vec_VecEntry(vFrameObjs, f),
|
||||
(Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) );
|
||||
}
|
||||
|
||||
// derive unrolled timeframes
|
||||
pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * (pCex->iFrame+1) );
|
||||
pFrames->pName = Aig_UtilStrsav( pAig->pName );
|
||||
pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec );
|
||||
// initialize the flops of
|
||||
Saig_ManForEachLo( pAig, pObj, i )
|
||||
pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Aig_InfoHasBit(pCex->pData, i) );
|
||||
// iterate through the frames
|
||||
for ( f = 0; f <= pCex->iFrame; f++ )
|
||||
{
|
||||
// construct
|
||||
vObjs = (Vec_Int_t *)Vec_VecEntry( vFrameObjs, f );
|
||||
Aig_ManForEachNodeVec( pAig, vObjs, pObj, i )
|
||||
{
|
||||
if ( Aig_ObjIsNode(pObj) )
|
||||
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||
else if ( Aig_ObjIsPo(pObj) )
|
||||
pObj->pData = Aig_ObjChild0Copy(pObj);
|
||||
else if ( Aig_ObjIsConst1(pObj) )
|
||||
pObj->pData = Aig_ManConst1(pFrames);
|
||||
else if ( Saig_ObjIsPi(pAig, pObj) )
|
||||
{
|
||||
if ( Aig_ObjPioNum(pObj) < nInputs )
|
||||
{
|
||||
int iBit = pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj);
|
||||
pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Aig_InfoHasBit(pCex->pData, iBit) );
|
||||
}
|
||||
else
|
||||
{
|
||||
pObj->pData = Aig_ObjCreatePi( pFrames );
|
||||
Vec_IntPush( *pvMapPiA3F, Aig_ObjPioNum(pObj) );
|
||||
Vec_IntPush( *pvMapPiA3F, f );
|
||||
}
|
||||
}
|
||||
}
|
||||
if ( f == pCex->iFrame )
|
||||
break;
|
||||
// transfer
|
||||
vRoots = (Vec_Int_t *)Vec_VecEntry( vFrameCos, f );
|
||||
Aig_ManForEachNodeVec( pAig, vRoots, pObj, i )
|
||||
Saig_ObjLiToLo( pAig, pObj )->pData = pObj->pData;
|
||||
}
|
||||
// create output
|
||||
pObj = Aig_ManPo( pAig, pCex->iPo );
|
||||
Aig_ObjCreatePo( pFrames, Aig_Not((Aig_Obj_t *)pObj->pData) );
|
||||
// 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;
|
||||
return p;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Destroys refinement manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Saig_RefManStop( Saig_RefMan_t * p )
|
||||
{
|
||||
Aig_ManStopP( &p->pFrames );
|
||||
Vec_IntFreeP( &p->vMapPiA3F );
|
||||
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_ManForEachPi( p->pFrames, pObj, i )
|
||||
{
|
||||
iInput = Vec_IntEntry( p->vMapPiA3F, 2*i );
|
||||
iFrame = Vec_IntEntry( p->vMapPiA3F, 2*i+1 );
|
||||
pObj->fPhase = Aig_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
|
||||
// update value if it is a don't-care
|
||||
if ( pCare && !Aig_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_ManForEachPo( p->pFrames, pObj, i )
|
||||
pObj->fPhase = ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) );
|
||||
pObj = Aig_ManPo( p->pFrames, 0 );
|
||||
return pObj->fPhase;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Generate the care set using SAT solver.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p )
|
||||
{
|
||||
int nConfLimit = 1000000;
|
||||
Abc_Cex_t * pCare;
|
||||
Cnf_Dat_t * pCnf;
|
||||
sat_solver * pSat;
|
||||
Aig_Obj_t * pObj;
|
||||
Vec_Int_t * vAssumps, * vVar2PiId;
|
||||
int i, f, iInput, iFrame, RetValue, Counter;
|
||||
int nCoreLits, * pCoreLits;
|
||||
// create CNF
|
||||
assert( Aig_ManRegNum(p->pFrames) == 0 );
|
||||
pCnf = Cnf_Derive( 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;
|
||||
}
|
||||
// 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) * Aig_BitWordNum(pCare->nBits) );
|
||||
return pCare;
|
||||
}
|
||||
// the problem is SAT - it is expected
|
||||
}
|
||||
// create assumptions
|
||||
vVar2PiId = Vec_IntStartFull( pCnf->nVars );
|
||||
vAssumps = Vec_IntAlloc( Aig_ManPiNum(p->pFrames) );
|
||||
Aig_ManForEachPi( p->pFrames, pObj, i )
|
||||
{
|
||||
iInput = Vec_IntEntry( p->vMapPiA3F, 2*i );
|
||||
iFrame = Vec_IntEntry( p->vMapPiA3F, 2*i+1 );
|
||||
// RetValue = Aig_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 );
|
||||
}
|
||||
// solve
|
||||
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 ( 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;
|
||||
}
|
||||
// get relevant SAT literals
|
||||
nCoreLits = sat_solver_final( pSat, &pCoreLits );
|
||||
assert( nCoreLits > 0 );
|
||||
if ( p->fVerbose )
|
||||
printf( "Analize final selected %d assumptions out of %d.\n", nCoreLits, Vec_IntSize(vAssumps) );
|
||||
// create counter-example
|
||||
pCare = Abc_CexDup( p->pCex, p->pCex->nRegs );
|
||||
memset( pCare->pData, 0, sizeof(unsigned) * Aig_BitWordNum(pCare->nBits) );
|
||||
// set new values
|
||||
for ( i = 0; i < nCoreLits; i++ )
|
||||
{
|
||||
int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(pCoreLits[i]) );
|
||||
assert( iPiNum >= 0 && iPiNum < Aig_ManPiNum(p->pFrames) );
|
||||
iInput = Vec_IntEntry( p->vMapPiA3F, 2*iPiNum );
|
||||
iFrame = Vec_IntEntry( p->vMapPiA3F, 2*iPiNum+1 );
|
||||
Aig_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput );
|
||||
}
|
||||
|
||||
// further reduce the CEX
|
||||
Counter = 0;
|
||||
for ( i = p->nInputs; i < Saig_ManPiNum(p->pAig); i++ )
|
||||
{
|
||||
for ( f = 0; f <= pCare->iFrame; f++ )
|
||||
if ( Aig_InfoHasBit( pCare->pData, pCare->nRegs + pCare->nPis * f + i ) )
|
||||
break;
|
||||
if ( f == pCare->iFrame + 1 )
|
||||
continue;
|
||||
Counter++;
|
||||
|
||||
// try removing this input
|
||||
}
|
||||
if ( p->fVerbose )
|
||||
printf( "Essential primary inputs %d out of %d.\n", Counter, Saig_ManPiNum(p->pAig) - p->nInputs );
|
||||
|
||||
|
||||
// cleanup
|
||||
Cnf_DataFree( pCnf );
|
||||
sat_solver_delete( pSat );
|
||||
Vec_IntFree( vAssumps );
|
||||
Vec_IntFree( vVar2PiId );
|
||||
// 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 [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_ManRefineCexSat( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose )
|
||||
{
|
||||
Abc_Cex_t * pCare = NULL;
|
||||
int clk = clock();
|
||||
Saig_RefMan_t * p = Saig_RefManStart( pAig, pCex, nInputs, fVerbose );
|
||||
p->pFrames = Saig_ManUnrollWithCex( pAig, pCex, nInputs, &p->vMapPiA3F );
|
||||
if ( p->fVerbose )
|
||||
Aig_ManPrintStats( p->pFrames );
|
||||
|
||||
if ( p->fVerbose )
|
||||
Abc_PrintTime( 1, "Frames", clock() - clk );
|
||||
|
||||
clk = clock();
|
||||
pCare = Saig_RefManRunSat( p );
|
||||
Saig_RefManStop( p );
|
||||
|
||||
if ( p->fVerbose )
|
||||
Abc_PrintTime( 1, "Filter", clock() - clk );
|
||||
|
||||
if ( p->fVerbose )
|
||||
Abc_CexPrintStats( pCex );
|
||||
if ( p->fVerbose )
|
||||
Abc_CexPrintStats( pCare );
|
||||
return pCare;
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -8763,20 +8763,19 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
Aig_ManStop( pAig );
|
||||
}
|
||||
*/
|
||||
/*
|
||||
|
||||
{
|
||||
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
|
||||
extern Abc_Cex_t * Saig_PhaseTranslateCex( Aig_Man_t * p, Abc_Cex_t * pCex );
|
||||
if ( pAbc->pCex && pNtk )
|
||||
{
|
||||
Abc_Cex_t * pNew;
|
||||
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
|
||||
pNew = Saig_PhaseTranslateCex( pAig, pAbc->pCex );
|
||||
pNew = Saig_ManRefineCexSat( pAig, pAbc->pCex, 0, 0 );
|
||||
Aig_ManStop( pAig );
|
||||
Abc_FrameReplaceCex( pAbc, &pNew );
|
||||
}
|
||||
}
|
||||
*/
|
||||
|
||||
|
||||
return 0;
|
||||
usage:
|
||||
|
|
|
|||
Loading…
Reference in New Issue