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

correct fanout count

This commit is contained in:
Allen Ho 2023-11-23 19:33:05 +08:00
parent 67a2b97cf0
commit a316847341
2 changed files with 73 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -5703,8 +5703,9 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose,
pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew );
// TODO: record the corresponding impl node of each lit
vLitBmiter = Vec_IntAlloc( Gia_ManObjNum(p2) );
Vec_IntFill( vLitBmiter, Gia_ManObjNum(p2) + Gia_ManObjNum(p1), 0 );
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 )
{
@ -5776,7 +5777,7 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose,
Gia_ManStaticFanoutStop( p1 );
printf( "category %d %d %d\n", c1, c2, Gia_ManObjNum(p1) );
printf( "spec: fanin: %d / fanout: %d / total %d\n", c1, c2, Gia_ManObjNum(p1) );
// TODO: record hashed equivalent nodes
@ -5798,17 +5799,30 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose,
Vec_IntPush( vLits, pObj->Value );
}
// int e;
// Vec_IntForEachEntry( vLitBmiter, e, i )
// {
// printf( "%d ", e );
// }
// printf("\n");
int e, c3=0, c4=0, c5=0;
c1 = 0; c2 = 0;
Vec_IntForEachEntry( vLitBmiter, e, i )
{
if ( i%2 ) continue;
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 )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
//Gia_ManForEachCo( p1, pObj, i )
// Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManForEachCo( p1, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Vec_IntForEachEntry( vLits, iLit, i )
Gia_ManAppendCo( pNew, iLit );
Vec_IntFree( vLits );

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

@ -1882,8 +1882,46 @@ 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;
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) );
if ( Vec_IntEntry( vLitBmiter, lit_repr ) == 3 )
{
switch ( Vec_IntEntry( vLitBmiter, lit_obj ) )
{
case 1:
case 4:
Vec_IntUpdateEntry( vLitBmiter, lit_repr, 4 );
break;
case 2:
case 5:
Vec_IntUpdateEntry( vLitBmiter, lit_repr, 5 );
break;
default:
break;
}
}
else
{
if ( Vec_IntEntry(vLitBmiter, lit_obj ) == 3 )
switch ( Vec_IntEntry( vLitBmiter, lit_repr ) )
{
case 1:
case 4:
Vec_IntUpdateEntry( vLitBmiter, lit_obj, 4 );
break;
case 2:
case 5:
Vec_IntUpdateEntry( vLitBmiter, lit_obj, 5 );
break;
default:
break;
}
}
assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) );
Gia_ObjSetProved( p, i );
if ( Gia_ObjId(p, pRepr) == 0 )
@ -1893,17 +1931,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){
if ( Vec_IntEntry( vLitBmiter, pRepr->Value ) == 3 )
// printf( "node %d (%d) merged into node %d (%d)\n", lit_obj, Vec_IntEntry( vLitBmiter, lit_obj ), lit_repr, Vec_IntEntry( vLitBmiter, lit_repr ) );
if ( Vec_IntEntry( vLitBmiter, lit_repr ) == 3 )
{
switch ( Vec_IntEntry( vLitBmiter, pObj -> Value ) )
switch ( Vec_IntEntry( vLitBmiter, lit_obj ) )
{
case 1:
case 4:
Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 4 );
Vec_IntUpdateEntry( vLitBmiter, lit_repr, 4 );
break;
case 2:
case 5:
Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 5 );
Vec_IntUpdateEntry( vLitBmiter, lit_repr, 5 );
break;
default:
break;
@ -1911,16 +1950,16 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
}
else
{
if ( Vec_IntEntry(vLitBmiter, pObj->Value ) == 3 )
switch ( Vec_IntEntry( vLitBmiter, pRepr -> Value ) )
if ( Vec_IntEntry(vLitBmiter, lit_obj ) == 3 )
switch ( Vec_IntEntry( vLitBmiter, lit_repr ) )
{
case 1:
case 4:
Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 4 );
Vec_IntUpdateEntry( vLitBmiter, lit_obj, 4 );
break;
case 2:
case 5:
Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 5 );
Vec_IntUpdateEntry( vLitBmiter, lit_obj, 5 );
break;
default:
break;
@ -1998,7 +2037,7 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )
break;
}
}
printf("category %d %d %d %d %d\n", c1, c2, c3+c4+c5, c4, c5);
printf("(fraig) impl: eq_fanin: %d / eq_fanout: %d / total: %d\n", c4, c5, c3+c4+c5);
}
return pNew;
}