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

str_eco ver1

This commit is contained in:
Allen Ho 2024-02-01 07:25:46 +08:00
parent 284b9d6a9c
commit c74144c6eb
3 changed files with 767 additions and 365 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -30,9 +30,12 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
Vec_Int_t* vMarkBmiter;
Vec_Int_t* vIdBI;
Vec_Int_t* vIdBO;
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;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@ -5702,186 +5705,55 @@ 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 vMarkBmiter
vMarkBmiter = Vec_IntAlloc( (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) );
Vec_IntFill( vMarkBmiter, (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)), 0 );
printf( "allocated size: %d\n", Vec_IntSize(vMarkBmiter) );
// 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)
{
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) );
}
Gia_ManForEachCi( p1, pObj, i )
{
int id = pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew );
Vec_IntSetEntry( vMarkBmiter, id >> 1, 4 );
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
Gia_ManForEachAnd( p2, pObj, i )
{
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Vec_IntUpdateEntry( vMarkBmiter, pObj->Value >> 1, 3 );
Vec_IntPush( Vec_PtrEntry(vBmiter2Impl, pObj->Value >> 1), Gia_ObjId(p2, pObj) );
}
// TODO: find nodes in spec
Vec_Int_t * vTypeSpec = Vec_IntAlloc( 16 );
Vec_IntFill( vTypeSpec, Gia_ManObjNum(p1), 0 );
int n = Gia_ManBufNum(p1) / 2;
if(biNum > 0){
n = biNum;
}
Gia_ManStaticFanoutStart( p1 );
Vec_Ptr_t * vQ = Vec_PtrAlloc(16);
Vec_Ptr_t * vBO = Vec_PtrAlloc(16);
Gia_Obj_t * pObj2;
int c1 = 0;
int c2 = 0;
int count = 0;
vIdBI = Vec_IntAlloc(16);
vIdBO = Vec_IntAlloc(16);
Gia_ManForEachBuf( p1, pObj, i )
{
if ( count < n )
{
Vec_IntSetEntry( vTypeSpec, Gia_ObjId( p1, pObj ), 1 );
c1++;
count ++;
Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) );
Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) );
while ( Vec_PtrSize(vQ) != 0 )
{
pObj2 = Vec_PtrPop(vQ);
if ( Vec_IntEntry( vTypeSpec, Gia_ObjId(p1, pObj2) ) != 0 ) continue;
c1 ++;
Vec_IntSetEntry( vTypeSpec, Gia_ObjId(p1, pObj2), 1 );
if ( Gia_ObjFaninNum(p1, pObj2) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj2) );
if ( Gia_ObjFaninNum(p1, pObj2) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj2) );
}
}
else
{
Vec_IntSetEntry( vTypeSpec, Gia_ObjId( p1, pObj ), 2 );
Vec_PtrPush( vBO, pObj );
c2 ++;
int j;
// pObj = Gia_ObjFanin0(pObj);
Gia_ObjForEachFanoutStatic(p1, pObj, pObj2, j)
{
Vec_PtrPush( vQ, pObj2 );
}
while ( Vec_PtrSize(vQ) != 0 )
{
pObj2 = Vec_PtrPop(vQ);
if ( Vec_IntEntry( vTypeSpec, Gia_ObjId(p1, pObj2) ) != 0 ) continue;
Vec_IntSetEntry( vTypeSpec, Gia_ObjId(p1, pObj2), 2 );
c2 ++;
for( int j = 0; j < Gia_ObjFanoutNum(p1, pObj2); j++ )
{
Vec_PtrPush( vQ, Gia_ObjFanout(p1, pObj2, j) );
}
}
}
}
Vec_Int_t* vFlag = Vec_IntAlloc( Gia_ManObjNum(p1) );
Vec_IntFill( vFlag, Gia_ManObjNum(p1), 0 );
int id;
int count_node = 0;
// count nodes
Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i )
{
Vec_PtrPush( vQ, pObj );
}
while( Vec_PtrSize(vQ) > 0 )
{
pObj = Vec_PtrPop(vQ);
id = Gia_ObjId( p1, pObj );
if ( Vec_IntEntry( vFlag, Gia_ObjId(p1, pObj) ) != 0 ) continue;
Vec_IntSetEntry( vFlag, Gia_ObjId(p1, pObj), 1 );
count_node ++;
if ( Vec_IntEntry( vTypeSpec, id ) == 1 )
{
continue;
}
else
{
if ( Gia_ObjFaninNum(p1, pObj) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) );
if ( Gia_ObjFaninNum(p1, pObj) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) );
}
}
printf( "BI: %d, BO: %d, Box Size: %d\n", n, Gia_ManBufNum(p1)-n, count_node );
Gia_ManStaticFanoutStop( p1 );
printf( "spec: fanin: %d / fanout: %d / total %d\n", c1, c2, Gia_ManObjNum(p1) );
// TODO: record hashed equivalent nodes
count = 0;
Gia_ManForEachAnd( p1, pObj, i ) {
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
if ( Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) > 0 )
{
if ( Vec_IntGetEntry( vMarkBmiter, pObj->Value >> 1 ) == 3 ) // eq node in impl
{
Vec_IntUpdateEntry( vMarkBmiter, pObj->Value >> 1, 3 + Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) );
}
else
{
Vec_IntUpdateEntry( vMarkBmiter, pObj->Value >> 1, Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) );
}
}
if ( Gia_ObjIsBuf(pObj) )
{
Vec_IntPush( vLits, pObj->Value );
if ( count < n )
{
Vec_IntPush( vIdBI, (pObj->Value) >> 1 );
}
else
{
Vec_IntPush( vIdBO, (pObj->Value) >> 1 );
}
count ++;
}
Vec_IntPush( Vec_PtrEntry(vBmiter2Spec, pObj->Value >> 1), Gia_ObjId(p1, pObj) );
}
int e, c3=0, c4=0, c5=0;
c1 = 0; c2 = 0;
Vec_IntForEachEntry( vMarkBmiter, e, i )
{
switch (e)
{
case 1: c1++; break;
case 2: c2++; break;
case 3: c3++; break;
case 4: c4++; break;
case 5: c5++; break;
default:
break;
}
}
printf("(strash) impl: eq_fanin: %d / eq_fanout: %d / total: %d\n", c4, c5, c3+c4+c5);
Gia_ManForEachCo( p2, pObj, i )
{
int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) << 1;
Vec_IntSetEntry( vMarkBmiter, id, 5 );
int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1;
Vec_IntPush( Vec_PtrEntry(vBmiter2Impl, id), Gia_ObjId(p2, pObj) );
}
Gia_ManForEachCo( p1, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
{
int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1;
Vec_IntPush( Vec_PtrEntry(vBmiter2Spec, id), Gia_ObjId(p1, pObj) );
}
Vec_IntForEachEntry( vLits, iLit, i )
Gia_ManAppendCo( pNew, iLit );
Vec_IntFree( vLits );
@ -6024,6 +5896,538 @@ 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 ///
////////////////////////////////////////////////////////////////////////

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

@ -598,6 +598,7 @@ static int Abc_CommandAbc9AddFlop ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9BMiter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GenHie ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9RecoverBoundary ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9StrEco ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -1378,6 +1379,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&bmiter", Abc_CommandAbc9BMiter, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gen_hie", Abc_CommandAbc9GenHie, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&rb", Abc_CommandAbc9RecoverBoundary, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&str_eco", Abc_CommandAbc9StrEco, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 );
{
@ -51953,6 +51955,111 @@ usage:
return 1;
}
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;
char * FileName = NULL;
char * FileName2 = NULL;
FILE * pFile = NULL;
int c, fVerbose = 0;
int bi = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != 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;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9StrEco(): There is no AIG.\n" );
return 0;
}
if ( argc != globalUtilOptind + 2 )
{
printf("%d\n", argc-globalUtilOptind);
Abc_Print( -1, "Abc_CommandAbc9StrEco(): AIG should be given on the command line.\n" );
return 0;
}
// get the input file name
FileName = argv[globalUtilOptind];
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 );
// 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 );
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 );
Gia_ManStop( pImpl );
Gia_ManStop( pTemp );
Abc_FrameUpdateGia( pAbc, pPatched );
return 0;
usage:
Abc_Print( -2, "usage: &str_eco -I <biNum> [-vh] <file> <file2>\n" );
Abc_Print( -2, "\t creates the boundary miter\n" );
Abc_Print( -2, "\t-I <biNum>: number of boundary inputs\n" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<file> : the implementation file\n");
return 1;
}
/**Function*************************************************************
Synopsis []

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

@ -147,6 +147,8 @@ static inline void Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj )
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;
////////////////////////////////////////////////////////////////////////
@ -1788,6 +1790,8 @@ 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 );
@ -1890,45 +1894,24 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) )
{
// printf( "*node %d (%d) merged into node %d (%d)\n", id_obj, Vec_IntEntry( vMarkBmiter, id_obj ), id_repr, Vec_IntEntry( vMarkBmiter, id_repr) );
if ( pPars->fBMiterInfo )
{
if ( Vec_IntEntry( vMarkBmiter, id_repr ) == 3 )
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)
{
switch ( Vec_IntEntry( vMarkBmiter, id_obj ) )
{
case 1:
case 4:
Vec_IntUpdateEntry( vMarkBmiter, id_repr, 4 );
break;
case 2:
case 5:
Vec_IntUpdateEntry( vMarkBmiter, id_repr, 5 );
break;
default:
break;
}
Vec_IntPush(vIds_spec_repr, eId);
}
else
Vec_IntForEachEntry( vIds_impl_obj, eId, j)
{
if ( Vec_IntEntry(vMarkBmiter, id_obj ) == 3 )
switch ( Vec_IntEntry( vMarkBmiter, id_repr ) )
{
case 1:
case 4:
Vec_IntUpdateEntry( vMarkBmiter, id_obj, 4 );
break;
case 2:
case 5:
Vec_IntUpdateEntry( vMarkBmiter, id_obj, 5 );
break;
default:
break;
}
Vec_IntPush(vIds_impl_repr, eId);
}
// TODO
Vec_IntSetEntry( vMarkBmiter, id_obj, Vec_IntEntry( vMarkBmiter, id_repr) );
Vec_IntClear(vIds_spec_obj);
Vec_IntClear(vIds_impl_obj);
}
assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) );
Gia_ObjSetProved( p, i );
@ -1939,178 +1922,101 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) )
{
if (pPars->fBMiterInfo){
// printf( "node %d (%d) merged into node %d (%d)\n", id_obj, Vec_IntEntry( vMarkBmiter, id_obj ), id_repr, Vec_IntEntry( vMarkBmiter, id_repr ) );
if ( Vec_IntEntry( vMarkBmiter, id_repr ) == 3 )
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)
{
switch ( Vec_IntEntry( vMarkBmiter, id_obj ) )
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 )
{
case 1:
case 4:
Vec_IntUpdateEntry( vMarkBmiter, id_repr, 4 );
break;
case 2:
case 5:
Vec_IntUpdateEntry( vMarkBmiter, id_repr, 5 );
break;
default:
break;
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
else if ( Vec_IntSize( vIds_spec_repr ) == Vec_IntSize( vIds_spec_obj) && Vec_IntSize( vIds_impl_obj ) == 0 ) // new match
{
if ( Vec_IntEntry(vMarkBmiter, id_obj ) == 3 )
switch ( Vec_IntEntry( vMarkBmiter, id_repr ) )
if ( pObj->fPhase ^ pRepr -> fPhase )
{
Vec_IntForEachEntry( vIds_impl_repr, eId, j )
{
case 1:
case 4:
Vec_IntUpdateEntry( vMarkBmiter, id_obj, 4 );
break;
case 2:
case 5:
Vec_IntUpdateEntry( vMarkBmiter, id_obj, 5 );
break;
default:
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) );
}
printf("new match flip\n");
}
}
// TODO
Vec_IntSetEntry( vMarkBmiter, id_obj, Vec_IntEntry( vMarkBmiter, id_repr) );
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);
}
pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase );
}
}
if ( pPars->fBMiterInfo )
{
// check bi, bo
Vec_Ptr_t* vAO = Vec_PtrAlloc( 16 ); // additioal output boundary
Vec_Ptr_t* vAI = Vec_PtrAlloc( 16 ); // additional input boundary
Vec_Ptr_t* vMI = Vec_PtrAlloc(16); // missing input boundary
Vec_Ptr_t* vMO = Vec_PtrAlloc(16); // missing input boundary
Vec_Ptr_t* vQ = Vec_PtrAlloc(16); // queue for fanout traversal
int val;
int cnt_TO = 0;
int cnt_TI = 0;
int cnt_SIDE = 0;
int cnt_MI = 0;
int cnt_MO = 0;
Vec_Int_t* vFlag = Vec_IntAlloc( p->nObjs );
Vec_IntFill( vFlag, p->nObjs, 0 );
printf("BI:");
Vec_IntForEachEntry( vIdBI, val, i )
// print
Vec_Int_t* vIds_spec, *vIds_impl;
int k, id;
for( int j=0; j < Vec_PtrSize(vBmiter2Spec); j++ )
{
printf( " %d (%d)", val, Vec_IntEntry( vMarkBmiter, val) );
if ( Vec_IntEntry( vMarkBmiter, val) <= 3 )
{
Vec_PtrPush(vMI, &((p->pObjs)[val]) );
}
else cnt_MI ++;
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");
}
printf("\nBO:");
Vec_IntForEachEntry( vIdBO, val, i )
{
printf( " %d (%d)", val, Vec_IntEntry( vMarkBmiter, val) );
if ( Vec_IntEntry( vMarkBmiter, val) <= 3 )
{
Vec_PtrPush(vQ, &((p->pObjs)[val]) );
Vec_PtrPush(vMO, &((p->pObjs)[val]) );
Vec_IntSetEntry( vFlag, val, 2 );
}
else cnt_MO ++;
}
printf("\n");
// find extended output boundary
Gia_ManStaticFanoutStart( p );
Gia_Obj_t * pObj2;
cnt_TO -= Vec_PtrSize(vQ);
while ( Vec_PtrSize(vQ) != 0 )
{
pObj2 = Vec_PtrPop(vQ);
if ( Vec_IntEntry( vFlag, Gia_ObjId(p, pObj2) ) == 1 ) continue;
Vec_IntSetEntry( vFlag, Gia_ObjId(p, pObj2), 1 );
cnt_TO ++;
val = Vec_IntEntry(vMarkBmiter, Gia_ObjId(p, pObj2));
if ( val == 5 || Gia_ObjIsCo( pObj2 ) ) // boundary found
{
Vec_PtrPush( vAO, pObj2 );
continue;
}
for( int j = 0; j < Gia_ObjFanoutNum(p, pObj2); j++ )
{
Vec_PtrPush( vQ, Gia_ObjFanout(p, pObj2, j) );
}
}
Gia_ManStaticFanoutStop(p);
// find extneded input boundary
Vec_PtrForEachEntry( Gia_Obj_t*, vMO, pObj, i )
{
Vec_IntSetEntry( vFlag, Gia_ObjId(p, pObj), 2 );
}
int id;
Vec_PtrForEachEntry( Gia_Obj_t*, vMI, pObj, i ) Vec_PtrPush( vQ, pObj );
Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i ) Vec_PtrPush( vQ, pObj );
cnt_TI -= Vec_PtrSize(vQ);
while ( Vec_PtrSize(vQ) > 0 )
{
pObj = Vec_PtrPop(vQ);
id = Gia_ObjId( p, pObj );
if ( Vec_IntEntry( vFlag, id ) == 2 ) continue;
printf( "backtrace to node %d\n", id );
if ( Vec_IntEntry(vMarkBmiter, id ) != 2 ) cnt_TI ++;
Vec_IntSetEntry( vFlag, id, 2 );
if ( Vec_IntEntry( vMarkBmiter, id ) >= 3 || Gia_ObjIsCi( pObj ) ) // matched
{
if ( Vec_IntEntry( vMarkBmiter, id ) < 5 || Gia_ObjIsCi( pObj ) )
{
Vec_PtrPush( vAI, pObj );
}
continue;
}
else
{
if ( Gia_ObjFaninNum(p, pObj) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) );
if ( Gia_ObjFaninNum(p, pObj) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) );
}
}
// print result
printf("extended BO with %d extra nodes:", cnt_TO);
Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i )
{
printf( " %d", Gia_ObjId(p, pObj) );
}
printf("\n");
printf("extended BI with %d extra nodes:", cnt_TI);
Vec_PtrForEachEntry( Gia_Obj_t*, vAI, pObj, i )
{
printf( " %d", Gia_ObjId(p, pObj) );
}
printf("\n");
printf("matched BI: %d / matched BO: %d / AI: %d / AO: %d / Extra nodes: %d\n", cnt_MI, cnt_MO, Vec_PtrSize(vAI), Vec_PtrSize(vAO), cnt_TO + cnt_TI );
}
if ( p->iPatsPi > 0 )
{
abctime clk2 = Abc_Clock();
@ -2155,7 +2061,6 @@ finalize:
Gia_ManRemoveWrongChoices( p );
return p->pCexSeq ? 0 : 1;
}
extern Vec_Int_t * vMarkBmiter;
Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )
{
Gia_Man_t * pNew = NULL;
@ -2163,22 +2068,8 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )
// TODO
if (pPars -> fBMiterInfo){
int e, i, c1=0, c2=0, c3=0, c4=0, c5=0;
Vec_IntForEachEntry( vMarkBmiter, e, i )
{
switch (e)
{
case 1: c1++; break;
case 2: c2++; break;
case 3: c3++; break;
case 4: c4++; break;
case 5: c5++; break;
default:
break;
}
}
printf("(fraig) impl: eq_fanin: %d / eq_fanout: %d / total: %d\n", c4, c5, c3+c4+c5);
}
return pNew;
}
void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose )