diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-12-02 21:12:57 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-12-02 21:12:57 -0800 |
commit | 1bf289c774eca7ead1edfba51c0e86255e2730e7 (patch) | |
tree | 4ba76c9bfbb2e01339b377fd0d1fb3a713fcc02e /src/proof/acec/acecCo.c | |
parent | 2ff522df455bf4835981d2348bb4c2cc3565073e (diff) | |
download | abc-1bf289c774eca7ead1edfba51c0e86255e2730e7.tar.gz abc-1bf289c774eca7ead1edfba51c0e86255e2730e7.tar.bz2 abc-1bf289c774eca7ead1edfba51c0e86255e2730e7.zip |
Changes to arithmetic logic detection.
Diffstat (limited to 'src/proof/acec/acecCo.c')
-rw-r--r-- | src/proof/acec/acecCo.c | 146 |
1 files changed, 109 insertions, 37 deletions
diff --git a/src/proof/acec/acecCo.c b/src/proof/acec/acecCo.c index 1b73c36f..39f092b2 100644 --- a/src/proof/acec/acecCo.c +++ b/src/proof/acec/acecCo.c @@ -90,38 +90,30 @@ Vec_Int_t * Gia_PolynAddHaRoots( Gia_Man_t * pGia ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vAddCos, Vec_Int_t ** pvIns, Vec_Int_t ** pvOuts ) +Vec_Wec_t * Gia_PolynComputeMap( Vec_Int_t * vAdds, int nObjs ) { - Vec_Int_t * vOrder = Vec_IntAlloc( 1000 ); - Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(pGia) ); - Vec_Int_t * vRoots = Vec_IntAlloc( 5 * Gia_ManCoNum(pGia) ); - Vec_Int_t * vLeaves = Vec_IntAlloc( 2 * Gia_ManCiNum(pGia) ); - Vec_Wec_t * vMap = Vec_WecStart( Gia_ManObjNum(pGia) ); - int i, k, Index, Driver, Entry1, Entry2 = -1; // map nodes driven by adders into adder indexes - for ( i = 0; 5*i < Vec_IntSize(vAdds); i++ ) + Vec_Wec_t * vMap = Vec_WecStart( nObjs ); int i; + for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ ) { - Entry1 = Vec_IntEntry( vAdds, 5*i + 3 ); - Entry2 = Vec_IntEntry( vAdds, 5*i + 4 ); + int Entry1 = Vec_IntEntry( vAdds, 6*i + 3 ); + int Entry2 = Vec_IntEntry( vAdds, 6*i + 4 ); Vec_WecPush( vMap, Entry1, i ); Vec_WecPush( vMap, Entry1, Entry2 ); Vec_WecPush( vMap, Entry2, i ); Vec_WecPush( vMap, Entry2, Entry1 ); } - // collect roots - Gia_ManForEachCoDriverId( pGia, Driver, i ) - { - Vec_IntPush( vRoots, Driver ); - Vec_BitWriteEntry( vIsRoot, Driver, 1 ); - } - // collect additional outputs - Vec_IntForEachEntry( vAddCos, Driver, i ) - { - Vec_IntPush( vRoots, Driver ); + return vMap; +} +Vec_Int_t * Gia_PolynCoreOrder_int( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Wec_t * vMap, Vec_Int_t * vRoots, Vec_Int_t ** pvIns ) +{ + Vec_Int_t * vOrder = Vec_IntAlloc( 1000 ); + Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(pGia) ); + int i, k, Index, Driver, Entry1, Entry2 = -1; + // mark roots + Vec_IntForEachEntry( vRoots, Driver, i ) Vec_BitWriteEntry( vIsRoot, Driver, 1 ); - } - // detect full adder tree - *pvOuts = Vec_IntDup( vRoots ); + // collect boxes while ( 1 ) { // iterate through boxes driving this one @@ -143,9 +135,9 @@ Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * Vec_IntRemove( vRoots, Entry1 ); Vec_IntRemove( vRoots, Entry2 ); // set new marks - Entry1 = Vec_IntEntry( vAdds, 5*Index + 0 ); - Entry2 = Vec_IntEntry( vAdds, 5*Index + 1 ); - Driver = Vec_IntEntry( vAdds, 5*Index + 2 ); + Entry1 = Vec_IntEntry( vAdds, 6*Index + 0 ); + Entry2 = Vec_IntEntry( vAdds, 6*Index + 1 ); + Driver = Vec_IntEntry( vAdds, 6*Index + 2 ); Vec_BitWriteEntry( vIsRoot, Entry1, 1 ); Vec_BitWriteEntry( vIsRoot, Entry2, 1 ); Vec_BitWriteEntry( vIsRoot, Driver, 1 ); @@ -158,19 +150,99 @@ Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * break; } // collect remaining leaves - Vec_BitForEachEntryStart( vIsRoot, Driver, i, 1 ) - if ( Driver ) - Vec_IntPush( vLeaves, i ); - *pvIns = vLeaves; - // cleanup + if ( pvIns ) + { + *pvIns = Vec_IntAlloc( Vec_BitSize(vIsRoot) ); + Vec_BitForEachEntryStart( vIsRoot, Driver, i, 1 ) + if ( Driver ) + Vec_IntPush( *pvIns, i ); + } Vec_BitFree( vIsRoot ); + return vOrder; +} +Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vAddCos, Vec_Int_t ** pvIns, Vec_Int_t ** pvOuts ) +{ + Vec_Int_t * vOrder; + Vec_Wec_t * vMap = Gia_PolynComputeMap( vAdds, Gia_ManObjNum(pGia) ); + Vec_Int_t * vRoots = Vec_IntAlloc( Gia_ManCoNum(pGia) ); + int i, Driver; + // collect roots + Gia_ManForEachCoDriverId( pGia, Driver, i ) + Vec_IntPush( vRoots, Driver ); + // collect additional outputs + if ( vAddCos ) + Vec_IntForEachEntry( vAddCos, Driver, i ) + Vec_IntPush( vRoots, Driver ); + // remember roots + if ( pvOuts ) + *pvOuts = Vec_IntDup( vRoots ); + // create order + vOrder = Gia_PolynCoreOrder_int( pGia, vAdds, vMap, vRoots, pvIns ); Vec_IntFree( vRoots ); Vec_WecFree( vMap ); + printf( "Collected %d boxes.\n", Vec_IntSize(vOrder) ); return vOrder; } /**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_PolyCollectRoots_rec( Vec_Int_t * vAdds, Vec_Wec_t * vMap, Vec_Bit_t * vMarks, int iBox, Vec_Int_t * vRoots ) +{ + int k; + for ( k = 0; k < 3; k++ ) + { + int i, Index, Sum, Carry = Vec_IntEntry( vAdds, 6*iBox+k ); + Vec_Int_t * vLevel = Vec_WecEntry( vMap, Carry ); + if ( Carry == 0 ) + continue; + Vec_IntForEachEntryDouble( vLevel, Index, Sum, i ) + if ( Vec_IntEntry(vAdds, 6*Index+4) == Carry && !Vec_BitEntry(vMarks, Sum) ) + { + Vec_IntPush( vRoots, Sum ); + Gia_PolyCollectRoots_rec( vAdds, vMap, vMarks, Index, vRoots ); + } + } +} +void Gia_PolyCollectRoots( Vec_Int_t * vAdds, Vec_Wec_t * vMap, Vec_Bit_t * vMarks, int iBox, Vec_Int_t * vRoots ) +{ + Vec_IntClear( vRoots ); + Vec_IntPush( vRoots, Vec_IntEntry(vAdds, 6*iBox+3) ); + Vec_IntPush( vRoots, Vec_IntEntry(vAdds, 6*iBox+4) ); + Gia_PolyCollectRoots_rec( vAdds, vMap, vMarks, iBox, vRoots ); +} +Vec_Wec_t * Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vRootBoxes ) +{ + extern Vec_Bit_t * Acec_ManPoolGetPointed( Gia_Man_t * p, Vec_Int_t * vAdds ); + Vec_Bit_t * vMarks = Acec_ManPoolGetPointed( pGia, vAdds ); + Vec_Wec_t * vMap = Gia_PolynComputeMap( vAdds, Gia_ManObjNum(pGia) ); + Vec_Wec_t * vRes = Vec_WecStart( Vec_IntSize(vRootBoxes) ); + Vec_Int_t * vRoots = Vec_IntAlloc( 64 ); + Vec_Int_t * vOrder; + int i, iBox; + Vec_IntForEachEntry( vRootBoxes, iBox, i ) + { + Gia_PolyCollectRoots( vAdds, vMap, vMarks, iBox, vRoots ); + vOrder = Gia_PolynCoreOrder_int( pGia, vAdds, vMap, vRoots, NULL ); + Vec_IntAppend( Vec_WecEntry(vRes, i), vOrder ); + Vec_IntFree( vOrder ); + } + Vec_BitFree( vMarks ); + Vec_IntFree( vRoots ); + Vec_WecFree( vMap ); + return vRes; +} + +/**Function************************************************************* + Synopsis [Collect internal node order.] Description [] @@ -197,15 +269,15 @@ Vec_Int_t * Gia_PolynCoreCollect( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t Vec_IntForEachEntryReverse( vOrder, Index, i ) { // mark inputs - Entry1 = Vec_IntEntry( vAdds, 5*Index + 0 ); - Entry2 = Vec_IntEntry( vAdds, 5*Index + 1 ); - Entry3 = Vec_IntEntry( vAdds, 5*Index + 2 ); + Entry1 = Vec_IntEntry( vAdds, 6*Index + 0 ); + Entry2 = Vec_IntEntry( vAdds, 6*Index + 1 ); + Entry3 = Vec_IntEntry( vAdds, 6*Index + 2 ); Vec_BitWriteEntry( vVisited, Entry1, 1 ); Vec_BitWriteEntry( vVisited, Entry2, 1 ); Vec_BitWriteEntry( vVisited, Entry3, 1 ); // traverse from outputs - Entry1 = Vec_IntEntry( vAdds, 5*Index + 3 ); - Entry2 = Vec_IntEntry( vAdds, 5*Index + 4 ); + Entry1 = Vec_IntEntry( vAdds, 6*Index + 3 ); + Entry2 = Vec_IntEntry( vAdds, 6*Index + 4 ); Gia_PolynCoreCollect_rec( pGia, Entry1, vNodes, vVisited ); Gia_PolynCoreCollect_rec( pGia, Entry2, vNodes, vVisited ); } @@ -325,7 +397,7 @@ Gia_Man_t * Gia_PolynCoreDetectTest_int( Gia_Man_t * pGia, Vec_Int_t * vAddCos, //Gia_ManShow( pGia, vNodes, 0 ); printf( "Detected %d FAs/HAs. Roots = %d. Leaves = %d. Nodes = %d. Adds = %d. ", - Vec_IntSize(vAdds)/5, Vec_IntSize(vLeaves), Vec_IntSize(vRoots), Vec_IntSize(vNodes), Vec_IntSize(vOrder) ); + Vec_IntSize(vAdds)/6, Vec_IntSize(vLeaves), Vec_IntSize(vRoots), Vec_IntSize(vNodes), Vec_IntSize(vOrder) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Gia_PolynCorePrintCones( pGia, vLeaves, fVerbose ); |