luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

shared EI/EO not handled yet

This commit is contained in:
Allen Ho 2024-03-01 16:05:41 +08:00
parent c74144c6eb
commit 6f5656c188
7 changed files with 1240 additions and 737 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
src/aig/gia/gia.h
View File

@ -1789,6 +1789,29 @@ extern void Tas_ManSatPrintStats( Tas_Man_t * p );
extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
extern int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs );
/*=== giaBound.c ===========================================================*/
typedef struct Bnd_Man_t_ Bnd_Man_t;
extern Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl );
extern void Bnd_ManStop();
//for fraig
extern void Bnd_ManMap( int iLit, int id, int spec );
extern void Bnd_ManMerge( int id1, int id2, int phaseDiff );
extern void Bnd_ManFinalizeMappings();
extern void Bnd_ManPrintMappings();
// for eco
extern int Bnd_ManCheckBound( Gia_Man_t *p );
extern void Bnd_ManFindBound( Gia_Man_t *p );
extern Gia_Man_t* Bnd_ManGenSpecOut( Gia_Man_t *p );
extern Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t *p );
extern Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPatch );
extern void Bnd_ManSetEqOut( int eq );
extern void Bnd_ManSetEqRes( int eq );
extern void Bnd_ManPrintStats();
// util
extern Gia_Man_t* Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec_Bit_t* vEI_phase, Vec_Bit_t* vEO_phase );
ABC_NAMESPACE_HEADER_END

1043
src/aig/gia/giaBound.c Normal file
View File

File diff suppressed because it is too large Load Diff

600
src/aig/gia/giaDup.c
View File

@ -30,12 +30,8 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
Vec_Ptr_t* vBmiter2Spec;
Vec_Ptr_t* vBmiter2Impl;
Vec_Int_t* vPatch2Impl;
Vec_Bit_t* vImpl2Spec_phase;
Vec_Int_t* vBI_patch;
Vec_Int_t* vBO_patch;
extern Bnd_Man_t* pBnd;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@ -5674,9 +5670,9 @@ Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum)
Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose )
{
Vec_Int_t * vLits;
// Vec_Int_t * vLits;
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, iLit;
@ -5694,7 +5690,7 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose,
assert( Gia_ManRegNum(p2) == 0 );
assert( Gia_ManCiNum(p1) == Gia_ManCiNum(p2) );
assert( Gia_ManCoNum(p1) == Gia_ManCoNum(p2) );
vLits = Vec_IntAlloc( Gia_ManBufNum(p1) );
// vLits = Vec_IntAlloc( Gia_ManBufNum(p1) );
if ( fVerbose )
printf( "Creating a boundary miter with %d inputs, %d outputs, and %d buffers.\n",
Gia_ManCiNum(p1), Gia_ManCoNum(p1), Gia_ManBufNum(p1) );
@ -5705,58 +5701,44 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose,
Gia_ManConst0(p1)->Value = 0;
Gia_ManConst0(p2)->Value = 0;
// allocate vImpl2Spec_phase;
vImpl2Spec_phase = Vec_BitAlloc( Gia_ManObjNum(p2) );
Vec_BitFill( vImpl2Spec_phase, Gia_ManObjNum(p2), 0 );
// allocate vBmiter2Impl and vBmiter2Spec
Vec_Int_t* pVec_Int;
vBmiter2Impl = Vec_PtrAlloc( (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) );
Vec_PtrFill( vBmiter2Impl, (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)), 0 );
Vec_PtrForEachEntry( Vec_Int_t*, vBmiter2Impl, pVec_Int, i)
for( int i = 0; i < Gia_ManCiNum(p1); i++ )
{
Vec_PtrSetEntry(vBmiter2Impl, i, Vec_IntAlloc(2) );
}
vBmiter2Spec = Vec_PtrAlloc( (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) );
Vec_PtrFill( vBmiter2Spec, (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)), 0 );
Vec_PtrForEachEntry( Vec_Int_t*, vBmiter2Spec, pVec_Int, i)
{
Vec_PtrSetEntry(vBmiter2Spec, i, Vec_IntAlloc(2) );
int iLit = Gia_ManCi(p1, i)->Value = Gia_ManCi(p2, i) -> Value = Gia_ManAppendCi(pNew);
pObj = Gia_ManCi(p1, i);
Bnd_ManMap( iLit, Gia_ObjId( p1, pObj ), 1 );
pObj = Gia_ManCi(p2, i);
Bnd_ManMap( iLit, Gia_ObjId( p2, pObj) , 0 );
}
Gia_ManForEachCi( p1, pObj, i )
{
pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew );
Vec_IntPush( Vec_PtrEntry(vBmiter2Spec, pObj->Value >> 1), Gia_ObjId(p1, pObj) );
Vec_IntPush( Vec_PtrEntry(vBmiter2Impl, pObj->Value >> 1), Gia_ObjId(p1, pObj) ); // same pi id in impl and spec
}
// TODO: record the corresponding impl node of each lit
// record the corresponding impl node of each lit
Gia_ManForEachAnd( p2, pObj, i )
{
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Vec_IntPush( Vec_PtrEntry(vBmiter2Impl, pObj->Value >> 1), Gia_ObjId(p2, pObj) );
Bnd_ManMap( pObj -> Value, Gia_ObjId(p2, pObj), 0 );
}
// TODO: record hashed equivalent nodes
Gia_ManForEachAnd( p1, pObj, i ) {
// record hashed equivalent nodes
Gia_ManForEachAnd( p1, pObj, i )
{
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Vec_IntPush( Vec_PtrEntry(vBmiter2Spec, pObj->Value >> 1), Gia_ObjId(p1, pObj) );
Bnd_ManMap( pObj -> Value, Gia_ObjId(p1, pObj), 1 );
}
Gia_ManForEachCo( p2, pObj, i )
{
int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1;
Vec_IntPush( Vec_PtrEntry(vBmiter2Impl, id), Gia_ObjId(p2, pObj) );
iLit = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
}
Gia_ManForEachCo( p1, pObj, i )
{
int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1;
Vec_IntPush( Vec_PtrEntry(vBmiter2Spec, id), Gia_ObjId(p1, pObj) );
iLit = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
}
Vec_IntForEachEntry( vLits, iLit, i )
Gia_ManAppendCo( pNew, iLit );
Vec_IntFree( vLits );
// Vec_IntForEachEntry( vLits, iLit, i )
// Gia_ManAppendCo( pNew, iLit );
// Vec_IntFree( vLits );
Gia_ManHashStop( pNew );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
@ -5896,538 +5878,6 @@ Gia_Man_t * Gia_ManMiterFromBMiter( Gia_Man_t * p, int nPo )
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManPatch( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum)
{
Vec_Int_t * vLits;
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, iLit;
if ( Gia_ManBufNum(p1) == 0 ) {
printf( "The first AIG should have a boundary.\n" );
return NULL;
}
if ( Gia_ManBufNum(p2) == 0 ) {
printf( "The second AIG should have a boundary.\n" );
return NULL;
}
assert( Gia_ManBufNum(p1) > 0 );
assert( Gia_ManBufNum(p2) > 0 );
assert( Gia_ManBufNum(p1) == Gia_ManBufNum(p2) );
assert( Gia_ManRegNum(p1) == 0 );
assert( Gia_ManRegNum(p2) == 0 );
assert( Gia_ManCiNum(p1) == Gia_ManCiNum(p2) );
assert( Gia_ManCoNum(p1) == Gia_ManCoNum(p2) );
if ( fVerbose )
printf( "Mapping spec to patch with %d inputs, %d outputs, and %d buffers.\n",
Gia_ManCiNum(p1), Gia_ManCoNum(p1), Gia_ManBufNum(p1) );
pNew = Gia_ManStart( Gia_ManObjNum(p2) );
pNew->pName = ABC_ALLOC( char, strlen(p1->pName) + 10 );
sprintf( pNew->pName, "%s_patch", p1->pName );
Gia_ManHashStart( pNew );
Gia_ManConst0(p1)->Value = 0;
Gia_ManConst0(p2)->Value = 0;
// add patch aig first
// record lit -> patch id
Vec_Int_t* vVar2Patch = Vec_IntAlloc( Gia_ManObjNum(p2) );
Vec_IntFill( vVar2Patch, Gia_ManObjNum(p2), -1 );
Gia_ManForEachCi( p2, pObj, i )
{
pObj->Value = Gia_ManCi(p1, i)->Value = Gia_ManAppendCi( pNew );
Vec_IntSetEntry( vVar2Patch, pObj->Value >> 1, Gia_ObjId( p2, pObj ) );
}
Gia_ManForEachAnd( p2, pObj, i )
{
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
printf( "\t%d: %d %d\n", Gia_ObjId( p2, pObj), Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Vec_IntSetEntry( vVar2Patch, pObj->Value >> 1, Gia_ObjId( p2, pObj ) );
}
// alloc vCompl;
Vec_Bit_t * vComplBuf = Vec_BitAlloc(Gia_ManBufNum(p1));
Vec_Bit_t * vCompl = Vec_BitAlloc(Gia_ManObjNum(p1));
Vec_BitFill( vCompl, Gia_ManObjNum(p1), 0 );
Gia_ManForEachBuf( p2, pObj, i )
{
printf("\tbuf compl %d: %d\n", Gia_ObjId(p2, pObj), Gia_ObjFaninC0(pObj));
Vec_BitPush( vComplBuf, Gia_ObjFaninC0(pObj) );
}
int cnt = 0;
Gia_ManForEachBuf( p1, pObj, i )
{
printf("\tbuf compl %d: %d\n", Gia_ObjId(p1, pObj), Gia_ObjFaninC0(pObj));
if ( Vec_BitEntry( vComplBuf, cnt ) || Gia_ObjFaninC0(pObj) )
{
Vec_BitSetEntry( vCompl, Gia_ObjId( p1, pObj ), 1 );
printf("\tset\n");
}
cnt++;
}
// mark the box in spec
Vec_Int_t* vFlagSpec = Vec_IntAlloc( Gia_ManObjNum(p1) ); // 1: bi, 2: inside the box, 3: bo
Vec_IntFill( vFlagSpec, Gia_ManObjNum(p1), 0 );
int cnt_buf = 0;
Gia_ManForEachBuf( p1, pObj, i )
{
if ( cnt_buf < biNum )
{
Vec_IntSetEntry( vFlagSpec, Gia_ObjId(p1, Gia_ObjFanin0(pObj) ), 1 );
}
else
{
Vec_IntSetEntry( vFlagSpec, Gia_ObjId(p1, Gia_ObjFanin0(pObj) ), 3 );
}
cnt_buf ++;
}
int fanin0, fanin1;
Gia_ManForEachAnd( p1, pObj, i )
{
if ( Vec_IntEntry( vFlagSpec, Gia_ObjId(p1, pObj) ) != 0 ) continue ;
fanin0 = Vec_IntEntry( vFlagSpec, Gia_ObjId(p1, Gia_ObjFanin0(pObj) ) );
fanin1 = Vec_IntEntry( vFlagSpec, Gia_ObjId(p1, Gia_ObjFanin1(pObj) ) );
if ( fanin0 == 1 || fanin0 == 2 || fanin1 == 1 || fanin1 == 2 )
Vec_IntSetEntry( vFlagSpec, Gia_ObjId(p1, pObj ), 2 );
}
// compute spec2impl
Vec_Int_t* vSpec2Impl = Vec_IntAlloc( Gia_ManObjNum(p1) );
Vec_IntFill( vSpec2Impl, Gia_ManObjNum(p1), -1 );
Vec_Int_t* vSpec, *vImpl;
int j, id;
for ( i = 0; i < Vec_PtrSize( vBmiter2Spec ); i++ )
{
vSpec = Vec_PtrEntry( vBmiter2Spec, i );
vImpl = Vec_PtrEntry( vBmiter2Impl, i );
Vec_IntForEachEntry( vSpec, id, j )
{
if ( Vec_IntEntry( vSpec2Impl, id ) == -1 && Vec_IntSize( vImpl ) > 0 )
{
Vec_IntSetEntry( vSpec2Impl, id, Vec_IntEntry( vImpl, 0 ) );
}
}
}
// print
// printf("spec 2 impl:\n");
// Vec_IntForEachEntry( vSpec2Impl, id, i )
// {
// printf( "\t%d:\t %d\n", i, id );
// }
// alloc patch2impl
vPatch2Impl = Vec_IntAlloc( Gia_ManObjNum(p2) );
Vec_IntFill( vPatch2Impl, Gia_ManObjNum(p2), -1 );
Vec_IntSetEntry( vPatch2Impl, 0, 0 );
Gia_ManForEachCi( p2, pObj, i )
{
Vec_IntSetEntry( vVar2Patch, pObj->Value >> 1, pObj->Value >> 1);
Vec_IntSetEntry( vPatch2Impl, pObj->Value>>1, Vec_IntEntry( vSpec2Impl, pObj->Value>>1) );
}
// set the litral on the boundary of spec as in patch and record patch2impl
Vec_Int_t* vBufLit = Vec_IntAlloc( Gia_ManBufNum( p2 ) );
vBI_patch = Vec_IntAlloc( Gia_ManBufNum(p2) );
vBO_patch = Vec_IntAlloc( Gia_ManBufNum(p2) );
cnt_buf = 0;
Gia_ManForEachBuf( p2, pObj, i )
{
// TODO: check compl
Vec_IntPush( vBufLit, Gia_ObjFanin0( pObj ) -> Value );
if ( cnt_buf < biNum )
{
Vec_IntPush( vBI_patch, Gia_ObjFanin0( pObj) -> Value >> 1 );
}
else
{
Vec_IntPush( vBO_patch, Gia_ObjFanin0( pObj) -> Value >> 1 );
}
cnt_buf++;
}
Vec_Int_t* vSpec2Patch = Vec_IntAlloc( Gia_ManObjNum(p1) );
Vec_IntFill( vSpec2Patch, Gia_ManObjNum(p1), -1 );
cnt_buf = 0;
Gia_Obj_t * pObj2;
Gia_ManForEachBuf( p1, pObj, i )
{
// TODO: compl?
pObj2 = Gia_ObjFanin0(pObj);
pObj2 -> Value = Vec_IntEntry( vBufLit, cnt_buf );
Vec_IntSetEntry( vSpec2Patch, Gia_ObjId( p1, pObj2 ), Vec_IntEntry( vVar2Patch, pObj2->Value>>1 ) );
// printf( "spec node %d -> patch node %d\n", Gia_ObjId( p1, pObj2 ), Vec_IntEntry( vVar2Patch, pObj2->Value>>1 ) );
Vec_IntSetEntry( vPatch2Impl, pObj2 -> Value>>1, Vec_IntEntry( vSpec2Impl, Gia_ObjId(p1, pObj2) ) );
pObj->Value = pObj2->Value;
cnt_buf++;
}
// hash the area outside the box in spec and record patch2impl
int lit0, lit1;
Gia_ManForEachAnd( p1, pObj, i ) {
printf( "spec node %d(%d) = %d %d\n", Gia_ObjId( p1, pObj ), Vec_IntEntry( vFlagSpec, Gia_ObjId(p1, pObj)), Gia_ObjId( p1, Gia_ObjFanin0(pObj) ), Gia_ObjId( p1, Gia_ObjFanin1(pObj) ) );
if ( Vec_IntEntry( vFlagSpec, Gia_ObjId(p1, pObj) ) > 1 ) continue;
if ( Gia_ObjIsBuf(pObj) ) continue;
lit0 = Gia_ObjFanin0Copy(pObj);
lit1 = Gia_ObjFanin1Copy(pObj);
if ( Vec_BitEntry( vCompl, Gia_ObjId(p1, Gia_ObjFanin0(pObj) ) ) ) lit0 ^= 1;
if ( Vec_BitEntry( vCompl, Gia_ObjId(p1, Gia_ObjFanin1(pObj) ) ) ) lit1 ^= 1;
pObj->Value = Gia_ManHashAnd( pNew, lit0, lit1 );
assert( (pObj->Value>>1) < Vec_IntSize( vVar2Patch) );
assert( Vec_IntEntry( vVar2Patch, pObj->Value>>1 ) != -1 );
Vec_IntSetEntry( vSpec2Patch, Gia_ObjId( p1, pObj ), Vec_IntEntry( vVar2Patch, pObj->Value>>1 ) );
printf( "spec node %d -> patch node %d\n", Gia_ObjId( p1, pObj ), Vec_IntEntry( vVar2Patch, pObj->Value>>1 ) );
Vec_IntSetEntry( vPatch2Impl, pObj->Value >> 1, Vec_IntEntry( vSpec2Impl, Gia_ObjId(p1, pObj) ) );
}
// print
printf("patch 2 impl:\n");
Vec_IntForEachEntry( vPatch2Impl, id, i )
{
printf( "\t%d:\t %d\n", i, id );
}
// handle co
Gia_ManForEachCo( p2, pObj, i )
{
int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1;
}
// TODO: also check spec CO
// Gia_ManForEachCo( p1, pObj, i )
// {
// int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1;
// Vec_IntPush( Vec_PtrEntry(vBmiter2Spec, id), Gia_ObjId(p1, pObj) );
// }
Gia_ManHashStop( pNew );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManPatchImpl( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum)
{
Vec_Int_t * vLits;
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj, *pObj2;
int i, j, iLit, id, id2;
assert( Gia_ManRegNum(p1) == 0 );
assert( Gia_ManRegNum(p2) == 0 );
assert( Gia_ManCiNum(p1) == Gia_ManCiNum(p2) );
assert( Gia_ManCoNum(p1) == Gia_ManCoNum(p2) );
if ( fVerbose )
printf( "Mapping spec to patch with %d inputs, %d outputs, and %d buffers.\n",
Gia_ManCiNum(p1), Gia_ManCoNum(p1), Gia_ManBufNum(p1) );
pNew = Gia_ManStart( Gia_ManObjNum(p2) );
pNew->pName = ABC_ALLOC( char, strlen(p1->pName) + 10 );
sprintf( pNew->pName, "%s_patch", p1->pName );
Gia_ManHashStart( pNew );
Gia_ManConst0(p1)->Value = 0;
Gia_ManConst0(p2)->Value = 0;
// p1: patch
// p2: impl
// compute extended box
Gia_ManStaticFanoutStart( p1 );
Vec_Ptr_t* vBO = Vec_PtrAlloc(16);
Vec_Ptr_t* vBI = Vec_PtrAlloc(16);
Vec_Ptr_t* vAO = Vec_PtrAlloc(16);
Vec_Ptr_t* vAI = Vec_PtrAlloc(16);
Vec_Ptr_t* vQ = Vec_PtrAlloc(16);
Vec_Int_t* vFlag = Vec_IntAlloc( Gia_ManObjNum(p1) );
Vec_IntFill( vFlag, Gia_ManObjNum(p1), 0 );
Vec_IntForEachEntry( vBO_patch, id, i )
{
if ( Vec_IntEntry( vPatch2Impl, id ) == -1 ) // if no match on the boundary
Vec_PtrPush( vQ, p1->pObjs+id );
else
Vec_PtrPush( vBO, p1->pObjs+id );
}
while( Vec_PtrSize(vQ) > 0 )
{
pObj = Vec_PtrPop(vQ);
id = Gia_ObjId( p1, pObj );
if ( Vec_IntEntry( vFlag, id ) == 1 ) continue;
Vec_IntSetEntry( vFlag, id, 1 );
printf("%d\n", id);
if ( Vec_IntEntry( vPatch2Impl, id ) != -1 ) // matched
{
Vec_PtrPush( vAO, pObj );
}
else
{
for( j = 0; j < Gia_ObjFanoutNum(p1, pObj); j++ )
{
Vec_PtrPush( vQ, Gia_ObjFanout(p1, pObj, j) );
printf("\t%d\n", Gia_ObjId( p1, Gia_ObjFanout(p1, pObj, j) ) );
}
}
}
// set flag 2 for FOC
Vec_IntForEachEntry( vBO_patch, id, i )
{
Vec_PtrPush( vQ, p1->pObjs+id );
}
while( Vec_PtrSize(vQ) > 0 )
{
pObj = Vec_PtrPop(vQ);
id = Gia_ObjId( p1, pObj );
if ( Vec_IntEntry( vFlag, Gia_ObjId(p1, pObj) ) == 2 ) continue;
Vec_IntSetEntry( vFlag, Gia_ObjId(p1, pObj), 2 );
for( j = 0; j < Gia_ObjFanoutNum(p1, pObj); j++ )
{
Vec_PtrPush( vQ, Gia_ObjFanout(p1, pObj, j) );
}
}
// set flag 3 for BO
Vec_IntForEachEntry( vBO_patch, id, i )
{
Vec_IntSetEntry( vFlag, id, 3 );
}
// traverse down from unmated BI and AO
Vec_IntForEachEntry( vBI_patch, id, i )
{
if ( Vec_IntEntry( vPatch2Impl, id ) == -1 ) // if no match on the boundary
Vec_PtrPush( vQ, p1->pObjs+id );
else
Vec_PtrPush( vBI, p1->pObjs+id );
}
Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i )
{
Vec_PtrPush( vQ, pObj );
}
// traverse down
printf("traverse down\n");
while ( Vec_PtrSize(vQ) != 0 )
{
pObj = Vec_PtrPop(vQ);
id = Gia_ObjId( p1, pObj );
if ( Vec_IntEntry( vFlag, id ) == 4 ) continue;
printf("%d\n", id);
if ( Vec_IntEntry( vPatch2Impl, id ) != -1 && Vec_IntEntry( vFlag, id ) < 2 ) // matched
{
Vec_PtrPush( vAI, pObj );
printf("matched\n");
}
else if ( Vec_IntEntry( vFlag, id ) < 3 )
{
if ( Gia_ObjFaninNum(p1, pObj) > 0 )
{
Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) );
printf("\t%d\n", Gia_ObjId( p1, Gia_ObjFanin0(pObj) ) );
}
if ( Gia_ObjFaninNum(p1, pObj) > 1 )
{
Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) );
printf("\t%d\n", Gia_ObjId( p1, Gia_ObjFanin1(pObj) ) );
}
}
printf("2impl / flag: %d / %d\n", Vec_IntEntry( vPatch2Impl, id ), Vec_IntEntry( vFlag, id ) );
Vec_IntSetEntry( vFlag, id, 4 );
}
// print
printf( "matched BI:");
Vec_PtrForEachEntry( Gia_Obj_t*, vBI, pObj, i ) printf( " %d(%d)", Gia_ObjId( p1, pObj ), Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj)) );
printf("\nAI:");
Vec_PtrForEachEntry( Gia_Obj_t*, vAI, pObj, i ) printf( " %d(%d)", Gia_ObjId( p1, pObj ), Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj)) );
printf("\nmateched BO:");
Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i ) printf( " %d(%d)", Gia_ObjId( p1, pObj ), Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj)) );
printf("\nAO:");
Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i ) printf( " %d(%d)", Gia_ObjId( p1, pObj ), Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj)) );
printf("\n");
// create patched impl
// mark fanin cone of Extended Input in impl
Vec_Int_t* vFlag_impl = Vec_IntAlloc( Gia_ManObjNum(p2) );
Vec_IntFill( vFlag_impl, Gia_ManObjNum(p2), 0 );
Vec_PtrForEachEntry( Gia_Obj_t*, vBI, pObj, i )
{
Vec_PtrPush( vQ, p2->pObjs + Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj) ) );
}
Vec_PtrForEachEntry( Gia_Obj_t*, vAI, pObj, i )
{
Vec_PtrPush( vQ, p2->pObjs + Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj) ) );
}
while ( Vec_PtrSize(vQ) != 0 )
{
pObj = Vec_PtrPop(vQ);
id = Gia_ObjId( p2, pObj );
if ( Vec_IntEntry( vFlag_impl, id ) == 1 ) continue;
Vec_IntSetEntry( vFlag_impl, id, 1 );
if ( Gia_ObjFaninNum(p2, pObj) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) );
if ( Gia_ObjFaninNum(p2, pObj) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) );
}
// add pi
Gia_ManForEachCi( p2, pObj, i )
{
pObj->Value = Gia_ManCi(p1, i)->Value = Gia_ManAppendCi( pNew );
}
// add fanin cone of EI in impl
int cnt = 0;
Gia_ManForEachAnd( p2, pObj, i )
{
if ( Vec_IntEntry( vFlag_impl, Gia_ObjId(p2, pObj) ) == 0 ) continue;
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
printf( "%d\n", pObj->Value>>1 );
cnt ++;
}
printf( "%d node added in the fanin cone of EI\n", cnt );
// set literal and flag of EI in patch
// TODO: input phase
Vec_PtrForEachEntry( Gia_Obj_t*, vBI, pObj, i )
{
id = Gia_ObjId( p1, pObj );
pObj -> Value = ( p2 -> pObjs + Vec_IntEntry( vPatch2Impl, id ) ) -> Value;
Vec_IntSetEntry( vFlag, id, 5 );
}
Vec_PtrForEachEntry( Gia_Obj_t*, vAI, pObj, i )
{
id = Gia_ObjId( p1, pObj );
pObj -> Value = ( p2 -> pObjs + Vec_IntEntry( vPatch2Impl, id ) ) -> Value;
Vec_IntSetEntry( vFlag, id, 5 );
}
// mark fanin cone of EO in patch (to flag 5)
Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i )
Vec_PtrPush( vQ, pObj );
Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i )
Vec_PtrPush( vQ, pObj );
while ( Vec_PtrSize(vQ) != 0 )
{
pObj = Vec_PtrPop(vQ);
id = Gia_ObjId( p1, pObj );
if ( Vec_IntEntry( vFlag, id ) >= 5 ) continue;
Vec_IntSetEntry( vFlag, id, 6 );
if ( Gia_ObjFaninNum(p1, pObj) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) );
if ( Gia_ObjFaninNum(p1, pObj) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) );
}
// add fanin cone of EO to EI in patch
cnt = 0;
Gia_ManForEachAnd( p1, pObj, i )
{
if ( Vec_IntEntry( vFlag, Gia_ObjId(p1, pObj) ) != 6 ) continue;
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
printf( "%d\n", pObj->Value>>1 );
cnt ++;
}
printf( "%d node added in the extended boundary\n", cnt );
// set literal and flag(1) of EO in impl
Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i )
{
id = Gia_ObjId( p1, pObj );
id2 = Vec_IntEntry( vPatch2Impl, id );
pObj2 = p2 -> pObjs + id2;
pObj2 -> Value = pObj -> Value;
if ( Vec_BitEntry( vImpl2Spec_phase, id2 ) ) pObj2 -> Value ^= 1;
Vec_IntSetEntry( vFlag_impl, id2, 1 );
}
Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i )
{
id = Gia_ObjId( p1, pObj );
id2 = Vec_IntEntry( vPatch2Impl, id );
pObj2 = p2 -> pObjs + id2;
pObj2 -> Value = pObj -> Value;
printf( "id %d matched to id %d in impl, phase %d\n", id, id2, Vec_BitEntry( vImpl2Spec_phase, id2 ) );
if ( Vec_BitEntry( vImpl2Spec_phase, id2 ) ) pObj2 -> Value ^= 1;
Vec_IntSetEntry( vFlag_impl, id2, 1 );
}
// add flag 0 in impl
cnt = 0;
Gia_ManForEachAnd( p2, pObj, i )
{
if ( Vec_IntEntry( vFlag_impl, Gia_ObjId(p2, pObj) ) != 0 ) continue;
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
printf( "%d\n", pObj->Value>>1 );
cnt++;
}
printf( "%d node added in the fanout cone\n", cnt );
// handle co
cnt = 0;
Gia_ManForEachCo( p2, pObj, i )
{
id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1;
printf( "%d\n", id );
cnt ++;
}
Gia_ManStaticFanoutStop( p1 );
Gia_ManHashStop( pNew );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

3
src/aig/gia/module.make
View File

@ -109,4 +109,5 @@ SRC += src/aig/gia/giaAig.c \
src/aig/gia/giaTsim.c \
src/aig/gia/giaTtopt.cpp \
src/aig/gia/giaUnate.c \
src/aig/gia/giaUtil.c
src/aig/gia/giaUtil.c \
src/aig/gia/giaBound.c

168
src/base/abci/abc.c
View File

@ -51695,13 +51695,14 @@ usage:
***********************************************************************/
int Abc_CommandAbc9BMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum);
extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose );
Gia_Man_t * pTemp, * pSecond;
char * FileName = NULL;
FILE * pFile = NULL;
int c, fVerbose = 0;
int bi = 0;
Extra_UtilGetoptReset();
// TODO: use a flag to block Bnd_Man
while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF )
{
switch ( c )
@ -51752,7 +51753,7 @@ int Abc_CommandAbc9BMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9BMiter(): Cannot read the file name on the command line.\n" );
return 0;
}
pTemp = Gia_ManBoundaryMiter( pAbc->pGia, pSecond, fVerbose, bi);
pTemp = Gia_ManBoundaryMiter( pAbc->pGia, pSecond, fVerbose );
Gia_ManStop( pSecond );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
@ -51852,7 +51853,7 @@ int Abc_CommandAbc9RecoverBoundary( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_Obj_t* pObj;
Gia_Man_t * pSpec = NULL;
char ** pArgvNew;
int i, nArgcNew, nPo;
int nArgcNew, nPo;
int nBInput = -1;
char *FileName;
Extra_UtilGetoptReset();
@ -51955,29 +51956,34 @@ usage:
return 1;
}
extern Bnd_Man_t* pBnd;
int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_ManPatch( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum);
extern Gia_Man_t * Gia_ManPatchImpl( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum);
Gia_Man_t * pTemp, * pSecond, *pImpl, *pPatched;
extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
extern void Cec4_ManSetParams( Cec_ParFra_t * pPars );
extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose );
Gia_Man_t *pImpl, *pImpl_out = 0, *pSpec_out = 0, *pMiter, *pPatch, *pPatched, *pTemp, *pBmiter;;
char * FileName = NULL;
char * FileName2 = NULL;
FILE * pFile = NULL;
int c, fVerbose = 0;
int bi = 0;
int c, fVerbose = 0, success = 1;
// params
Gps_Par_t Pars, * pPars = &Pars;
memset( pPars, 0, sizeof(Gps_Par_t) );
Cec_ParCec_t ParsCec, *pParsCec = &ParsCec;
Cec_ManCecSetDefaultParams( pParsCec );
Cec_ParFra_t ParsFra, *pParsFra = &ParsFra;
Cec4_ManSetParams( pParsFra );
pParsFra -> fBMiterInfo = 1;
// TODO: save return value and return at the end of the function
// parse options
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
case 'I':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
goto usage;
}
bi = atoi(argv[globalUtilOptind++]);
break;
case 'v':
fVerbose ^= 1;
break;
@ -51999,7 +52005,10 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
// get the input file name
// params
// read impl
FileName = argv[globalUtilOptind];
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
@ -52010,44 +52019,103 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
fclose( pFile );
// get the input file name 2
FileName2 = argv[globalUtilOptind+1];
if ( (pFile = fopen( FileName2, "r" )) == NULL )
{
Abc_Print( -1, "Cannot open input file \"%s\". ", FileName2 );
if ( (FileName2 = Extra_FileGetSimilarName( FileName2, ".aig", ".blif", ".pla", ".eqn", ".bench" )) )
Abc_Print( 1, "Did you mean \"%s\"?", FileName2 );
Abc_Print( 1, "\n" );
return 1;
}
fclose( pFile );
// map spec to patch
pSecond = Gia_AigerRead( FileName, 0, 1, 0 );
if ( pSecond == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9StrEco(): Cannot read the file name on the command line.\n" );
return 0;
}
pTemp = Gia_ManPatch( pAbc->pGia, pSecond, fVerbose, bi);
// Gia_ManStop( pSecond );
// Abc_FrameUpdateGia( pAbc, pTemp );
// return 0;
// generated patched impl
pImpl = Gia_AigerRead( FileName2, 0, 0, 0 );
pImpl = Gia_AigerRead( FileName, 0, 0, 0 );
if ( pImpl == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9StrEco(): Cannot read the file name on the command line.\n" );
return 0;
}
pPatched = Gia_ManPatchImpl( pTemp, pImpl, fVerbose, bi);
Gia_ManStop( pSecond );
// read patch
FileName = argv[globalUtilOptind+1];
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", ".blif", ".pla", ".eqn", ".bench" )) )
Abc_Print( 1, "Did you mean \"%s\"?", FileName );
Abc_Print( 1, "\n" );
return 1;
}
fclose( pFile );
pPatch = Gia_AigerRead( FileName, 0, 1, 0 );
if ( pPatch == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9StrEco(): Cannot read the file name on the command line.\n" );
return 0;
}
// verify if spec eq impl
pMiter = Gia_ManMiter( pAbc->pGia, pImpl, 0, 1, 0, 0, 0 );
assert( Cec_ManVerify( pMiter, pParsCec ) );
Gia_ManStop(pMiter);
// start boundary manager
pBnd = Bnd_ManStart( pAbc->pGia, pImpl );
// check boundary
if ( 0 == Bnd_ManCheckBound( pAbc -> pGia ) )
{
Abc_Print( -1, "Abc_CommandAbc9StrEco(): The given boundary is invalid.\n" );
success = 0;
}
if ( success )
{
// create bmiter, run fraig
pBmiter = Gia_ManBoundaryMiter( pAbc -> pGia, pImpl, 0 );
pTemp = Cec4_ManSimulateTest( pBmiter, pParsFra );
Gia_ManStop(pBmiter);
Gia_ManStop(pTemp);
// find
Bnd_ManFindBound( pAbc -> pGia );
// create spec_out and
pSpec_out = Bnd_ManGenSpecOut( pAbc -> pGia );
if ( !pSpec_out ) success = 0;
pImpl_out = Bnd_ManGenImplOut( pImpl );
if ( !pImpl_out ) success = 0;
Gia_AigerWrite( pSpec_out, "spec_out.aig", 0, 0, 0 );
Gia_AigerWrite( pImpl_out, "impl_out.aig", 0, 0, 0 );
Gia_ManPrintStats( pSpec_out, pPars );
Gia_ManPrintStats( pImpl_out, pPars );
}
if ( success )
{
// check if spec_out and imnpl_out are equivalent
printf("Checking the equivalence of spec_out and impl_out\n");
pMiter = Gia_ManMiter( pSpec_out, pImpl_out, 0, 1, 0, 0, 0 );
Bnd_ManSetEqOut( Cec_ManVerify( pMiter, pParsCec ) );
Gia_ManStop( pMiter );
// generate patched
pPatched = Bnd_ManGenPatched( pImpl_out, pAbc->pGia, pPatch );
// check if patched is equiv to patch
printf("Checking the equivalence of patch and patched\n");
pMiter = Gia_ManMiter( pPatch, pPatched, 0, 1, 0, 0, 0 );
Bnd_ManSetEqRes( Cec_ManVerify( pMiter, pParsCec ) );
Gia_ManStop( pMiter );
}
Bnd_ManPrintStats();
Gia_ManStop( pImpl );
Gia_ManStop( pTemp );
Abc_FrameUpdateGia( pAbc, pPatched );
Gia_ManStop( pPatch );
if ( pSpec_out ) Gia_ManStop( pSpec_out );
if ( pImpl_out ) Gia_ManStop( pImpl_out );
if ( success )
{
Abc_FrameUpdateGia( pAbc, pPatched );
}
Bnd_ManStop();
return 0;
usage:

21
src/misc/vec/vecBit.h
View File

@ -626,6 +626,27 @@ static inline void Vec_BitReset( Vec_Bit_t * p )
p->pArray[i] = 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_BitPrint( Vec_Bit_t * p )
{
int i, Entry;
printf( "Vector has %d entries: {", Vec_BitSize(p) );
Vec_BitForEachEntry( p, Entry, i )
printf( " %d", Entry );
printf( " }\n" );
}
ABC_NAMESPACE_HEADER_END
#endif

119
src/proof/cec/cecSatG2.c
View File

@ -143,14 +143,6 @@ static inline int Cec4_ObjSatId( Gia_Man_t * p, Gia_Obj_t * pObj )
static inline int Cec4_ObjSetSatId( Gia_Man_t * p, Gia_Obj_t * pObj, int Num ) { assert(Cec4_ObjSatId(p, pObj) == -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), Num); Vec_IntPush(&p->vSuppVars, Gia_ObjId(p, pObj)); if ( Gia_ObjIsCi(pObj) ) Vec_IntPushTwo(&p->vCopiesTwo, Gia_ObjId(p, pObj), Num); assert(Vec_IntSize(&p->vVarMap) == Num); Vec_IntPush(&p->vVarMap, Gia_ObjId(p, pObj)); return Num; }
static inline void Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(Cec4_ObjSatId(p, pObj) != -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), -1); }
extern Vec_Int_t* vMarkBmiter;
extern Vec_Int_t* vIdBI;
extern Vec_Int_t* vIdBO;
extern Vec_Ptr_t* vBmiter2Spec;
extern Vec_Ptr_t* vBmiter2Impl;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -1791,9 +1783,9 @@ void Gia_ManRemoveWrongChoices( Gia_Man_t * p )
//Abc_Print( 1, "Removed %d wrong choices.\n", Counter );
}
extern Vec_Bit_t* vImpl2Spec_phase;
int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** ppNew, int fSimOnly )
{
Cec4_Man_t * pMan = Cec4_ManCreate( p, pPars );
Gia_Obj_t * pObj, * pRepr;
int i, fSimulate = 1;
@ -1894,25 +1886,11 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) )
{
if ( pPars->fBMiterInfo )
if ( pPars->fBMiterInfo )
{
int eId, j;
Vec_Int_t *vIds_spec_repr, *vIds_impl_repr, *vIds_spec_obj, *vIds_impl_obj;
vIds_spec_repr = Vec_PtrEntry( vBmiter2Spec, id_repr );
vIds_impl_repr = Vec_PtrEntry( vBmiter2Impl, id_repr );
vIds_spec_obj = Vec_PtrEntry( vBmiter2Spec, id_obj );
vIds_impl_obj = Vec_PtrEntry( vBmiter2Impl, id_obj );
Vec_IntForEachEntry( vIds_spec_obj, eId, j)
{
Vec_IntPush(vIds_spec_repr, eId);
}
Vec_IntForEachEntry( vIds_impl_obj, eId, j)
{
Vec_IntPush(vIds_impl_repr, eId);
}
Vec_IntClear(vIds_spec_obj);
Vec_IntClear(vIds_impl_obj);
Bnd_ManMerge( id_repr, id_obj, pObj->fPhase ^ pRepr->fPhase );
}
assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) );
Gia_ObjSetProved( p, i );
if ( Gia_ObjId(p, pRepr) == 0 )
@ -1923,73 +1901,8 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
{
if (pPars->fBMiterInfo){
int eId, j;
Vec_Int_t *vIds_spec_repr, *vIds_impl_repr, *vIds_spec_obj, *vIds_impl_obj;
vIds_spec_repr = Vec_PtrEntry( vBmiter2Spec, id_repr );
vIds_impl_repr = Vec_PtrEntry( vBmiter2Impl, id_repr );
vIds_spec_obj = Vec_PtrEntry( vBmiter2Spec, id_obj );
vIds_impl_obj = Vec_PtrEntry( vBmiter2Impl, id_obj );
Vec_IntForEachEntry( vIds_spec_obj, eId, j)
{
Vec_IntPush(vIds_spec_repr, eId);
}
Vec_IntForEachEntry( vIds_impl_obj, eId, j)
{
Vec_IntPush(vIds_impl_repr, eId);
}
// handle phase before cleaning
printf( "proven %d merged into %d (phase : %d)\n", Gia_ObjId(p, pObj), Gia_ObjId(p,pRepr), pObj->fPhase ^ pRepr -> fPhase );
if ( Vec_IntSize(vIds_spec_repr) == 0 ) // no match
{
if ( pObj->fPhase ^ pRepr -> fPhase )
{
Vec_IntForEachEntry( vIds_impl_obj, eId, j )
{
Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) );
printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) );
}
}
}
else if ( Vec_IntSize( vIds_spec_repr ) == Vec_IntSize( vIds_spec_obj) && Vec_IntSize( vIds_impl_obj ) == 0 ) // new match
{
if ( pObj->fPhase ^ pRepr -> fPhase )
{
Vec_IntForEachEntry( vIds_impl_repr, eId, j )
{
Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) );
printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) );
}
printf("new match flip\n");
}
}
else if ( Vec_IntSize( vIds_spec_repr ) > 0 && Vec_IntSize( vIds_impl_obj ) > 0 ) // matched, merge impl
{
if ( ( pObj->fPhase ^ pRepr -> fPhase) ^ ( Vec_BitEntry( vImpl2Spec_phase, Vec_IntEntry(vIds_impl_repr, 0)) ^ Vec_BitEntry( vImpl2Spec_phase, Vec_IntEntry(vIds_impl_obj, 0)) ) )
{
if ( Vec_IntSize( vIds_spec_repr ) == Vec_IntSize( vIds_spec_obj) ) // unmatched repr, matched obj, set repr bits
{
Vec_IntForEachEntry( vIds_impl_repr, eId, j )
{
if ( j >= Vec_IntSize( vIds_impl_repr)-Vec_IntSize(vIds_impl_obj) ) break;
Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) );
printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) );
}
}
else // set obj bits
{
Vec_IntForEachEntry( vIds_impl_obj, eId, j )
{
Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) );
printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) );
}
}
}
}
Vec_IntClear(vIds_spec_obj);
Vec_IntClear(vIds_impl_obj);
Bnd_ManMerge( id_repr, id_obj, pObj->fPhase ^ pRepr->fPhase );
// printf( "proven %d merged into %d (phase : %d)\n", Gia_ObjId(p, pObj), Gia_ObjId(p,pRepr), pObj->fPhase ^ pRepr -> fPhase );
}
pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase );
@ -2001,20 +1914,8 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
if ( pPars->fBMiterInfo )
{
// print
Vec_Int_t* vIds_spec, *vIds_impl;
int k, id;
for( int j=0; j < Vec_PtrSize(vBmiter2Spec); j++ )
{
printf("node %d: ", j);
vIds_spec = Vec_PtrEntry( vBmiter2Spec, j);
vIds_impl = Vec_PtrEntry( vBmiter2Impl, j);
Vec_IntForEachEntry(vIds_spec, id, k)
printf("%d ", id);
printf("| ");
Vec_IntForEachEntry(vIds_impl, id, k)
printf("%d ", id);
printf("\n");
}
Bnd_ManFinalizeMappings();
// Bnd_ManPrintMappings();
}
if ( p->iPatsPi > 0 )
@ -2066,10 +1967,6 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )
Gia_Man_t * pNew = NULL;
Cec4_ManPerformSweeping( p, pPars, &pNew, 0 );
// TODO
if (pPars -> fBMiterInfo){
}
return pNew;
}
void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose )