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

extended box report;

This commit is contained in:
Allen Ho 2023-12-10 21:30:46 +08:00
parent 9bb5333f62
commit 284b9d6a9c
3 changed files with 160 additions and 72 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -30,7 +30,7 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
Vec_Int_t* vLitBmiter;
Vec_Int_t* vMarkBmiter;
Vec_Int_t* vIdBI;
Vec_Int_t* vIdBO;
@ -5701,18 +5701,24 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose,
Gia_ManHashStart( pNew );
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) );
Gia_ManForEachCi( p1, pObj, i )
pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew );
{
int id = pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew );
Vec_IntSetEntry( vMarkBmiter, id >> 1, 4 );
}
// TODO: record the corresponding impl node of each lit
vLitBmiter = Vec_IntAlloc( (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) * 2 );
Vec_IntFill( vLitBmiter, (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) * 2, 0 );
printf( "allocated size: %d\n", Vec_IntSize(vLitBmiter) );
Gia_ManForEachAnd( p2, pObj, i )
{
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 3 );
Vec_IntUpdateEntry( vMarkBmiter, pObj->Value >> 1, 3 );
}
// TODO: find nodes in spec
@ -5726,11 +5732,11 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose,
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;
int val;
int count = 0;
vIdBI = Vec_IntAlloc(16);
vIdBO = Vec_IntAlloc(16);
@ -5759,6 +5765,7 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose,
else
{
Vec_IntSetEntry( vTypeSpec, Gia_ObjId( p1, pObj ), 2 );
Vec_PtrPush( vBO, pObj );
c2 ++;
int j;
@ -5782,6 +5789,37 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose,
}
}
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) );
@ -5794,13 +5832,13 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose,
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
if ( Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) > 0 )
{
if ( Vec_IntGetEntry( vLitBmiter, pObj->Value ) == 3 ) // eq node in impl
if ( Vec_IntGetEntry( vMarkBmiter, pObj->Value >> 1 ) == 3 ) // eq node in impl
{
Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 3 + Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) );
Vec_IntUpdateEntry( vMarkBmiter, pObj->Value >> 1, 3 + Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) );
}
else
{
Vec_IntUpdateEntry( vLitBmiter, pObj->Value, Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) );
Vec_IntUpdateEntry( vMarkBmiter, pObj->Value >> 1, Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) );
}
}
if ( Gia_ObjIsBuf(pObj) )
@ -5822,9 +5860,8 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose,
int e, c3=0, c4=0, c5=0;
c1 = 0; c2 = 0;
Vec_IntForEachEntry( vLitBmiter, e, i )
Vec_IntForEachEntry( vMarkBmiter, e, i )
{
if ( i%2 ) continue;
switch (e)
{
case 1: c1++; break;
@ -5839,7 +5876,10 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose,
printf("(strash) impl: eq_fanin: %d / eq_fanout: %d / total: %d\n", c4, c5, c3+c4+c5);
Gia_ManForEachCo( p2, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
{
int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) << 1;
Vec_IntSetEntry( vMarkBmiter, id, 5 );
}
Gia_ManForEachCo( p1, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Vec_IntForEachEntry( vLits, iLit, i )

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

@ -37921,7 +37921,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500, nMaxNodes = 0;
Cec4_ManSetParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "OJWRILDCNPMrmdckngxysopwqvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMrmdckngxysopwqvh" ) ) != EOF )
{
switch ( c )
{
@ -37969,18 +37969,6 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nItersMax < 0 )
goto usage;
break;
case 'O':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
goto usage;
}
pPars->nPO = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nPO < 1 )
goto usage;
break;
case 'L':
if ( globalUtilOptind >= argc )
{

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

@ -144,7 +144,7 @@ static inline int Cec4_ObjSetSatId( Gia_Man_t * p, Gia_Obj_t * pObj, int 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* vLitBmiter;
extern Vec_Int_t* vMarkBmiter;
extern Vec_Int_t* vIdBI;
extern Vec_Int_t* vIdBO;
@ -1885,25 +1885,25 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
if ( pRepr == NULL )
continue;
}
int lit_obj = Gia_ObjId( p, pObj ) << 1;
int lit_repr = Gia_ObjId( p, pRepr ) << 1;
int id_obj = Gia_ObjId( p, pObj );
int id_repr = Gia_ObjId( p, pRepr );
if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) )
{
printf( "*node %d (%d) merged into node %d (%d)\n", lit_obj >> 1, Vec_IntEntry( vLitBmiter, lit_obj ), lit_repr >> 1, Vec_IntEntry( vLitBmiter, lit_repr) );
// 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( vLitBmiter, lit_repr ) == 3 )
if ( Vec_IntEntry( vMarkBmiter, id_repr ) == 3 )
{
switch ( Vec_IntEntry( vLitBmiter, lit_obj ) )
switch ( Vec_IntEntry( vMarkBmiter, id_obj ) )
{
case 1:
case 4:
Vec_IntUpdateEntry( vLitBmiter, lit_repr, 4 );
Vec_IntUpdateEntry( vMarkBmiter, id_repr, 4 );
break;
case 2:
case 5:
Vec_IntUpdateEntry( vLitBmiter, lit_repr, 5 );
Vec_IntUpdateEntry( vMarkBmiter, id_repr, 5 );
break;
default:
break;
@ -1911,16 +1911,16 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
}
else
{
if ( Vec_IntEntry(vLitBmiter, lit_obj ) == 3 )
switch ( Vec_IntEntry( vLitBmiter, lit_repr ) )
if ( Vec_IntEntry(vMarkBmiter, id_obj ) == 3 )
switch ( Vec_IntEntry( vMarkBmiter, id_repr ) )
{
case 1:
case 4:
Vec_IntUpdateEntry( vLitBmiter, lit_obj, 4 );
Vec_IntUpdateEntry( vMarkBmiter, id_obj, 4 );
break;
case 2:
case 5:
Vec_IntUpdateEntry( vLitBmiter, lit_obj, 5 );
Vec_IntUpdateEntry( vMarkBmiter, id_obj, 5 );
break;
default:
break;
@ -1928,7 +1928,7 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
}
}
// TODO
Vec_IntSetEntry( vLitBmiter, lit_obj, Vec_IntEntry( vLitBmiter, lit_repr) );
Vec_IntSetEntry( vMarkBmiter, id_obj, Vec_IntEntry( vMarkBmiter, id_repr) );
}
assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) );
Gia_ObjSetProved( p, i );
@ -1939,18 +1939,18 @@ 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", lit_obj >> 1, Vec_IntEntry( vLitBmiter, lit_obj ), lit_repr >> 1, Vec_IntEntry( vLitBmiter, lit_repr ) );
if ( Vec_IntEntry( vLitBmiter, lit_repr ) == 3 )
// 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 )
{
switch ( Vec_IntEntry( vLitBmiter, lit_obj ) )
switch ( Vec_IntEntry( vMarkBmiter, id_obj ) )
{
case 1:
case 4:
Vec_IntUpdateEntry( vLitBmiter, lit_repr, 4 );
Vec_IntUpdateEntry( vMarkBmiter, id_repr, 4 );
break;
case 2:
case 5:
Vec_IntUpdateEntry( vLitBmiter, lit_repr, 5 );
Vec_IntUpdateEntry( vMarkBmiter, id_repr, 5 );
break;
default:
break;
@ -1958,16 +1958,16 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
}
else
{
if ( Vec_IntEntry(vLitBmiter, lit_obj ) == 3 )
switch ( Vec_IntEntry( vLitBmiter, lit_repr ) )
if ( Vec_IntEntry(vMarkBmiter, id_obj ) == 3 )
switch ( Vec_IntEntry( vMarkBmiter, id_repr ) )
{
case 1:
case 4:
Vec_IntUpdateEntry( vLitBmiter, lit_obj, 4 );
Vec_IntUpdateEntry( vMarkBmiter, id_obj, 4 );
break;
case 2:
case 5:
Vec_IntUpdateEntry( vLitBmiter, lit_obj, 5 );
Vec_IntUpdateEntry( vMarkBmiter, id_obj, 5 );
break;
default:
break;
@ -1975,7 +1975,7 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
}
}
// TODO
Vec_IntSetEntry( vLitBmiter, lit_obj, Vec_IntEntry( vLitBmiter, lit_repr) );
Vec_IntSetEntry( vMarkBmiter, id_obj, Vec_IntEntry( vMarkBmiter, id_repr) );
}
pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase );
}
@ -1986,67 +1986,128 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
{
// check bi, bo
Vec_Ptr_t* vBO = Vec_PtrAlloc( 16 );
Vec_Ptr_t * vQ = Vec_PtrAlloc(16);
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 )
{
printf( " %d (%d)", val, Vec_IntEntry( vLitBmiter, val << 1) );
printf( " %d (%d)", val, Vec_IntEntry( vMarkBmiter, val) );
if ( Vec_IntEntry( vMarkBmiter, val) <= 3 )
{
Vec_PtrPush(vMI, &((p->pObjs)[val]) );
}
else cnt_MI ++;
}
printf("\nBO:");
Vec_IntForEachEntry( vIdBO, val, i )
{
printf( " %d (%d)", val, Vec_IntEntry( vLitBmiter, val << 1) );
if ( Vec_IntEntry( vLitBmiter, val << 1) != 5 )
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 bound
// find extended output boundary
Gia_ManStaticFanoutStart( p );
Vec_Int_t* vFlag = Vec_IntAlloc( p->nObjs );
Vec_IntFill( vFlag, p->nObjs, 0 );
Gia_Obj_t * pObj2;
int cnt_node = 0;
int cnt_newBo = 0;
cnt_TO -= Vec_PtrSize(vQ);
while ( Vec_PtrSize(vQ) != 0 )
{
pObj2 = Vec_PtrPop(vQ);
if ( Vec_IntEntry( vFlag, Gia_ObjId(p, pObj2) ) != 0 ) continue;
cnt_node ++;
if ( Vec_IntEntry( vFlag, Gia_ObjId(p, pObj2) ) == 1 ) continue;
Vec_IntSetEntry( vFlag, Gia_ObjId(p, pObj2), 1 );
cnt_TO ++;
val = Vec_IntEntry(vLitBmiter, Gia_ObjId(p, pObj2) << 1);
val = Vec_IntEntry(vMarkBmiter, Gia_ObjId(p, pObj2));
if ( val == 5 || Gia_ObjIsCo( pObj2 ) ) // boundary found
{
cnt_newBo ++;
Vec_PtrPush( vBO, pObj2 );
Vec_PtrPush( vAO, pObj2 );
continue;
}
for( int j = 0; j < Gia_ObjFanoutNum(p, pObj2); j++ )
{
Vec_PtrPush( vQ, Gia_ObjFanout(p, pObj2, j) );
printf( "add fanout\n");
}
}
Gia_ManStaticFanoutStop(p);
printf("extended BO with %d extra nodes:", cnt_node);
Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i )
// 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 );
}
@ -2094,7 +2155,7 @@ finalize:
Gia_ManRemoveWrongChoices( p );
return p->pCexSeq ? 0 : 1;
}
extern Vec_Int_t * vLitBmiter;
extern Vec_Int_t * vMarkBmiter;
Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )
{
Gia_Man_t * pNew = NULL;
@ -2103,9 +2164,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( vLitBmiter, e, i )
Vec_IntForEachEntry( vMarkBmiter, e, i )
{
if ( i%2 ) continue;
switch (e)
{
case 1: c1++; break;