mirror of https://github.com/YosysHQ/abc.git
Added generation of values of internal nodes for GIA manager.
This commit is contained in:
Alan Mishchenko
parent
8daf610eba
commit
a8e59b2c42
|
|
@ -3407,6 +3407,10 @@ SOURCE=.\src\aig\gia\giaCCof.c
|
||||||
# End Source File
|
# End Source File
|
||||||
# Begin Source File
|
# Begin Source File
|
||||||
|
|
||||||
|
SOURCE=.\src\aig\gia\giaCex.c
|
||||||
|
# End Source File
|
||||||
|
# Begin Source File
|
||||||
|
|
||||||
SOURCE=.\src\aig\gia\giaCof.c
|
SOURCE=.\src\aig\gia\giaCof.c
|
||||||
# End Source File
|
# End Source File
|
||||||
# Begin Source File
|
# Begin Source File
|
||||||
|
|
|
||||||
|
|
@ -154,6 +154,7 @@ struct Gia_Man_t_
|
||||||
void * pLutLib; // LUT library
|
void * pLutLib; // LUT library
|
||||||
word nHashHit; // hash table hit
|
word nHashHit; // hash table hit
|
||||||
word nHashMiss; // hash table miss
|
word nHashMiss; // hash table miss
|
||||||
|
unsigned * pData2; // storage for object values
|
||||||
int fVerbose; // verbose reports
|
int fVerbose; // verbose reports
|
||||||
// truth table computation for small functions
|
// truth table computation for small functions
|
||||||
int nTtVars; // truth table variables
|
int nTtVars; // truth table variables
|
||||||
|
|
@ -740,6 +741,12 @@ extern void Gia_WriteAigerSimple( Gia_Man_t * pInit, char * pFile
|
||||||
/*=== giaBidec.c ===========================================================*/
|
/*=== giaBidec.c ===========================================================*/
|
||||||
extern unsigned * Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vTruth, Vec_Int_t * vVisited );
|
extern unsigned * Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vTruth, Vec_Int_t * vVisited );
|
||||||
extern Gia_Man_t * Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose );
|
extern Gia_Man_t * Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose );
|
||||||
|
/*=== giaCex.c ============================================================*/
|
||||||
|
extern int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
|
||||||
|
extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs );
|
||||||
|
extern void Gia_ManCounterExampleValueStart( Gia_Man_t * pGia, Abc_Cex_t * pCex );
|
||||||
|
extern void Gia_ManCounterExampleValueStop( Gia_Man_t * pGia );
|
||||||
|
extern int Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, int Id, int iFrame );
|
||||||
/*=== giaCsatOld.c ============================================================*/
|
/*=== giaCsatOld.c ============================================================*/
|
||||||
extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
|
extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
|
||||||
/*=== giaCsat.c ============================================================*/
|
/*=== giaCsat.c ============================================================*/
|
||||||
|
|
@ -959,8 +966,6 @@ extern int Gia_ManHasDangling( Gia_Man_t * p );
|
||||||
extern int Gia_ManMarkDangling( Gia_Man_t * p );
|
extern int Gia_ManMarkDangling( Gia_Man_t * p );
|
||||||
extern Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p );
|
extern Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p );
|
||||||
extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
|
extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
|
||||||
extern int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
|
|
||||||
extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs );
|
|
||||||
extern void Gia_ManInvertConstraints( Gia_Man_t * pAig );
|
extern void Gia_ManInvertConstraints( Gia_Man_t * pAig );
|
||||||
extern void Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj );
|
extern void Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj );
|
||||||
extern unsigned * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj );
|
extern unsigned * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj );
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,250 @@
|
||||||
|
/**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"
|
||||||
|
|
||||||
|
ABC_NAMESPACE_IMPL_START
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// DECLARATIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// FUNCTION DEFINITIONS ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Resimulates the counter-example.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut )
|
||||||
|
{
|
||||||
|
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
|
||||||
|
int RetValue, i, k, iBit = 0;
|
||||||
|
Gia_ManCleanMark0(pAig);
|
||||||
|
Gia_ManForEachRo( pAig, pObj, i )
|
||||||
|
pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
|
||||||
|
for ( i = 0; i <= p->iFrame; i++ )
|
||||||
|
{
|
||||||
|
Gia_ManForEachPi( pAig, pObj, k )
|
||||||
|
pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
|
||||||
|
Gia_ManForEachAnd( pAig, pObj, k )
|
||||||
|
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
|
||||||
|
(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
|
||||||
|
Gia_ManForEachCo( pAig, pObj, k )
|
||||||
|
pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
|
||||||
|
if ( i == p->iFrame )
|
||||||
|
break;
|
||||||
|
Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
|
||||||
|
{
|
||||||
|
pObjRo->fMark0 = pObjRi->fMark0;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
assert( iBit == p->nBits );
|
||||||
|
if ( fDualOut )
|
||||||
|
RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0;
|
||||||
|
else
|
||||||
|
RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
|
||||||
|
Gia_ManCleanMark0(pAig);
|
||||||
|
return RetValue;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Resimulates the counter-example.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs )
|
||||||
|
{
|
||||||
|
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
|
||||||
|
int RetValue, i, k, iBit = 0;
|
||||||
|
assert( Gia_ManPiNum(pAig) == p->nPis );
|
||||||
|
Gia_ManCleanMark0(pAig);
|
||||||
|
// Gia_ManForEachRo( pAig, pObj, i )
|
||||||
|
// pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
|
||||||
|
iBit = p->nRegs;
|
||||||
|
for ( i = 0; i <= p->iFrame; i++ )
|
||||||
|
{
|
||||||
|
Gia_ManForEachPi( pAig, pObj, k )
|
||||||
|
pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
|
||||||
|
Gia_ManForEachAnd( pAig, pObj, k )
|
||||||
|
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
|
||||||
|
(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
|
||||||
|
Gia_ManForEachCo( pAig, pObj, k )
|
||||||
|
pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
|
||||||
|
Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
|
||||||
|
pObjRo->fMark0 = pObjRi->fMark0;
|
||||||
|
}
|
||||||
|
assert( iBit == p->nBits );
|
||||||
|
// figure out the number of failed output
|
||||||
|
RetValue = -1;
|
||||||
|
// for ( i = Gia_ManPoNum(pAig) - 1; i >= nOutputs; i-- )
|
||||||
|
for ( i = nOutputs; i < Gia_ManPoNum(pAig); i++ )
|
||||||
|
{
|
||||||
|
if ( Gia_ManPo(pAig, i)->fMark0 )
|
||||||
|
{
|
||||||
|
RetValue = i;
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
Gia_ManCleanMark0(pAig);
|
||||||
|
return RetValue;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Starts the process of returning values for internal nodes.]
|
||||||
|
|
||||||
|
Description [Should be called when pCex is available, before probing
|
||||||
|
any object for its value using Gia_ManCounterExampleValueLookup().]
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
void Gia_ManCounterExampleValueStart( Gia_Man_t * pGia, Abc_Cex_t * pCex )
|
||||||
|
{
|
||||||
|
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
|
||||||
|
int Val0, Val1, nObjs, i, k, iBit = 0;
|
||||||
|
assert( Gia_ManRegNum(pGia) > 0 ); // makes sense only for sequential AIGs
|
||||||
|
assert( pGia->pData2 == NULL ); // if this fail, there may be a memory leak
|
||||||
|
// allocate memory to store simulation bits for internal nodes
|
||||||
|
pGia->pData2 = ABC_CALLOC( unsigned, Abc_BitWordNum( (pCex->iFrame + 1) * Gia_ManObjNum(pGia) ) );
|
||||||
|
// the register values in the counter-example should be zero
|
||||||
|
Gia_ManForEachRo( pGia, pObj, k )
|
||||||
|
assert( Abc_InfoHasBit(pCex->pData, iBit++) == 0 );
|
||||||
|
// iterate through the timeframes
|
||||||
|
nObjs = Gia_ManObjNum(pGia);
|
||||||
|
for ( i = 0; i <= pCex->iFrame; i++ )
|
||||||
|
{
|
||||||
|
// no need to set constant-0 node
|
||||||
|
// set primary inputs according to the counter-example
|
||||||
|
Gia_ManForEachPi( pGia, pObj, k )
|
||||||
|
if ( Abc_InfoHasBit(pCex->pData, iBit++) )
|
||||||
|
Abc_InfoSetBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjId(pGia, pObj) );
|
||||||
|
// compute values for each node
|
||||||
|
Gia_ManForEachAnd( pGia, pObj, k )
|
||||||
|
{
|
||||||
|
Val0 = Abc_InfoHasBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjFaninId0p(pGia, pObj) );
|
||||||
|
Val1 = Abc_InfoHasBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjFaninId1p(pGia, pObj) );
|
||||||
|
if ( (Val0 ^ Gia_ObjFaninC0(pObj)) & (Val1 ^ Gia_ObjFaninC1(pObj)) )
|
||||||
|
Abc_InfoSetBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjId(pGia, pObj) );
|
||||||
|
}
|
||||||
|
// derive values for combinational outputs
|
||||||
|
Gia_ManForEachCo( pGia, pObj, k )
|
||||||
|
{
|
||||||
|
Val0 = Abc_InfoHasBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjFaninId0p(pGia, pObj) );
|
||||||
|
if ( Val0 ^ Gia_ObjFaninC0(pObj) )
|
||||||
|
Abc_InfoSetBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjId(pGia, pObj) );
|
||||||
|
}
|
||||||
|
if ( i == pCex->iFrame )
|
||||||
|
continue;
|
||||||
|
// transfer values to the register output of the next frame
|
||||||
|
Gia_ManForEachRiRo( pGia, pObjRi, pObjRo, k )
|
||||||
|
if ( Abc_InfoHasBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjId(pGia, pObjRi) ) )
|
||||||
|
Abc_InfoSetBit( (unsigned *)pGia->pData2, nObjs * (i+1) + Gia_ObjId(pGia, pObjRo) );
|
||||||
|
}
|
||||||
|
assert( iBit == pCex->nBits );
|
||||||
|
// check that the counter-example is correct, that is, the corresponding output is asserted
|
||||||
|
assert( Abc_InfoHasBit( (unsigned *)pGia->pData2, nObjs * pCex->iFrame + Gia_ObjId(Gia_ManCo(pGia, pCex->iPo)) ) );
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Stops the process of returning values for internal nodes.]
|
||||||
|
|
||||||
|
Description [Should be called when probing is no longer needed]
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
void Gia_ManCounterExampleValueStop( Gia_Man_t * pGia )
|
||||||
|
{
|
||||||
|
assert( pGia->pData2 != NULL ); // if this fail, we try to call this procedure more than once
|
||||||
|
ABC_FREE( pGia->pData2 );
|
||||||
|
pGia->pData2 = NULL;
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Returns the value of the given object in the given timeframe.]
|
||||||
|
|
||||||
|
Description [Should be called to probe the value of an object with
|
||||||
|
the given ID (iFrame is a 0-based number of a time frame - should not
|
||||||
|
exceed the number of timeframes in the original counter-example).]
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
int Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, int Id, int iFrame )
|
||||||
|
{
|
||||||
|
assert( Id >= 0 && Id < Gia_ManObjNum(pGia) );
|
||||||
|
return Abc_InfoHasBit( (unsigned *)pGia->pData2, Gia_ManObjNum(pGia) * iFrame + Id );
|
||||||
|
}
|
||||||
|
|
||||||
|
/**Function*************************************************************
|
||||||
|
|
||||||
|
Synopsis [Procedure to test the above code.]
|
||||||
|
|
||||||
|
Description []
|
||||||
|
|
||||||
|
SideEffects []
|
||||||
|
|
||||||
|
SeeAlso []
|
||||||
|
|
||||||
|
***********************************************************************/
|
||||||
|
void Gia_ManCounterExampleValueTest( Gia_Man_t * pGia, Abc_Cex_t * pCex )
|
||||||
|
{
|
||||||
|
Gia_Obj_t * pObj = Gia_ManObj( pGia, Gia_ManObjNum(pGia)/2 );
|
||||||
|
int iFrame = Abc_MaxInt( 0, pCex->iFrame - 1 );
|
||||||
|
printf( "\nUsing counter-example, which asserts output %d in frame %d.\n", pCex->iPo, pCex->iFrame );
|
||||||
|
Gia_ManCounterExampleValueStart( pGia, pCex );
|
||||||
|
printf( "Value of object %d in frame %d is %d.\n", Gia_ObjId(pGia, pObj), iFrame,
|
||||||
|
Gia_ManCounterExampleValueLookup(pGia, Gia_ObjId(pGia, pObj), iFrame) );
|
||||||
|
Gia_ManCounterExampleValueStop( pGia );
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
/// END OF FILE ///
|
||||||
|
////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
|
||||||
|
ABC_NAMESPACE_IMPL_END
|
||||||
|
|
||||||
|
|
@ -93,6 +93,7 @@ void Gia_ManStop( Gia_Man_t * p )
|
||||||
Vec_IntFreeP( &p->vMapping );
|
Vec_IntFreeP( &p->vMapping );
|
||||||
Vec_IntFree( p->vCis );
|
Vec_IntFree( p->vCis );
|
||||||
Vec_IntFree( p->vCos );
|
Vec_IntFree( p->vCos );
|
||||||
|
ABC_FREE( p->pData2 );
|
||||||
ABC_FREE( p->pTravIds );
|
ABC_FREE( p->pTravIds );
|
||||||
ABC_FREE( p->pPlacement );
|
ABC_FREE( p->pPlacement );
|
||||||
ABC_FREE( p->pSwitching );
|
ABC_FREE( p->pSwitching );
|
||||||
|
|
|
||||||
|
|
@ -1181,97 +1181,6 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj )
|
||||||
*/
|
*/
|
||||||
}
|
}
|
||||||
|
|
||||||
/**Function*************************************************************
|
|
||||||
|
|
||||||
Synopsis [Resimulates the counter-example.]
|
|
||||||
|
|
||||||
Description []
|
|
||||||
|
|
||||||
SideEffects []
|
|
||||||
|
|
||||||
SeeAlso []
|
|
||||||
|
|
||||||
***********************************************************************/
|
|
||||||
int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut )
|
|
||||||
{
|
|
||||||
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
|
|
||||||
int RetValue, i, k, iBit = 0;
|
|
||||||
Gia_ManCleanMark0(pAig);
|
|
||||||
Gia_ManForEachRo( pAig, pObj, i )
|
|
||||||
pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
|
|
||||||
for ( i = 0; i <= p->iFrame; i++ )
|
|
||||||
{
|
|
||||||
Gia_ManForEachPi( pAig, pObj, k )
|
|
||||||
pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
|
|
||||||
Gia_ManForEachAnd( pAig, pObj, k )
|
|
||||||
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
|
|
||||||
(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
|
|
||||||
Gia_ManForEachCo( pAig, pObj, k )
|
|
||||||
pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
|
|
||||||
if ( i == p->iFrame )
|
|
||||||
break;
|
|
||||||
Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
|
|
||||||
{
|
|
||||||
pObjRo->fMark0 = pObjRi->fMark0;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
assert( iBit == p->nBits );
|
|
||||||
if ( fDualOut )
|
|
||||||
RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0;
|
|
||||||
else
|
|
||||||
RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
|
|
||||||
Gia_ManCleanMark0(pAig);
|
|
||||||
return RetValue;
|
|
||||||
}
|
|
||||||
|
|
||||||
/**Function*************************************************************
|
|
||||||
|
|
||||||
Synopsis [Resimulates the counter-example.]
|
|
||||||
|
|
||||||
Description []
|
|
||||||
|
|
||||||
SideEffects []
|
|
||||||
|
|
||||||
SeeAlso []
|
|
||||||
|
|
||||||
***********************************************************************/
|
|
||||||
int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs )
|
|
||||||
{
|
|
||||||
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
|
|
||||||
int RetValue, i, k, iBit = 0;
|
|
||||||
assert( Gia_ManPiNum(pAig) == p->nPis );
|
|
||||||
Gia_ManCleanMark0(pAig);
|
|
||||||
// Gia_ManForEachRo( pAig, pObj, i )
|
|
||||||
// pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
|
|
||||||
iBit = p->nRegs;
|
|
||||||
for ( i = 0; i <= p->iFrame; i++ )
|
|
||||||
{
|
|
||||||
Gia_ManForEachPi( pAig, pObj, k )
|
|
||||||
pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
|
|
||||||
Gia_ManForEachAnd( pAig, pObj, k )
|
|
||||||
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
|
|
||||||
(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
|
|
||||||
Gia_ManForEachCo( pAig, pObj, k )
|
|
||||||
pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
|
|
||||||
Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
|
|
||||||
pObjRo->fMark0 = pObjRi->fMark0;
|
|
||||||
}
|
|
||||||
assert( iBit == p->nBits );
|
|
||||||
// figure out the number of failed output
|
|
||||||
RetValue = -1;
|
|
||||||
// for ( i = Gia_ManPoNum(pAig) - 1; i >= nOutputs; i-- )
|
|
||||||
for ( i = nOutputs; i < Gia_ManPoNum(pAig); i++ )
|
|
||||||
{
|
|
||||||
if ( Gia_ManPo(pAig, i)->fMark0 )
|
|
||||||
{
|
|
||||||
RetValue = i;
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
Gia_ManCleanMark0(pAig);
|
|
||||||
return RetValue;
|
|
||||||
}
|
|
||||||
|
|
||||||
/**Function*************************************************************
|
/**Function*************************************************************
|
||||||
|
|
||||||
Synopsis [Complements the constraint outputs.]
|
Synopsis [Complements the constraint outputs.]
|
||||||
|
|
|
||||||
|
|
@ -9,6 +9,7 @@ SRC += src/aig/gia/gia.c \
|
||||||
src/aig/gia/giaAiger.c \
|
src/aig/gia/giaAiger.c \
|
||||||
src/aig/gia/giaBidec.c \
|
src/aig/gia/giaBidec.c \
|
||||||
src/aig/gia/giaCCof.c \
|
src/aig/gia/giaCCof.c \
|
||||||
|
src/aig/gia/giaCex.c \
|
||||||
src/aig/gia/giaCof.c \
|
src/aig/gia/giaCof.c \
|
||||||
src/aig/gia/giaCSatOld.c \
|
src/aig/gia/giaCSatOld.c \
|
||||||
src/aig/gia/giaCSat.c \
|
src/aig/gia/giaCSat.c \
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue