summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/acec/acecCl.c55
-rw-r--r--src/proof/acec/acecCo.c146
-rw-r--r--src/proof/acec/acecPa.c282
-rw-r--r--src/proof/acec/acecPool.c132
-rw-r--r--src/proof/acec/acecRe.c163
-rw-r--r--src/proof/acec/module.make5
6 files changed, 724 insertions, 59 deletions
diff --git a/src/proof/acec/acecCl.c b/src/proof/acec/acecCl.c
new file mode 100644
index 00000000..32be3b30
--- /dev/null
+++ b/src/proof/acec/acecCl.c
@@ -0,0 +1,55 @@
+/**CFile****************************************************************
+
+ FileName [acecCl.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [CEC for arithmetic circuits.]
+
+ Synopsis [Core procedures.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: acecCl.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acecInt.h"
+#include "misc/vec/vecWec.h"
+#include "misc/extra/extra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
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 );
diff --git a/src/proof/acec/acecPa.c b/src/proof/acec/acecPa.c
new file mode 100644
index 00000000..11d68d37
--- /dev/null
+++ b/src/proof/acec/acecPa.c
@@ -0,0 +1,282 @@
+/**CFile****************************************************************
+
+ FileName [acecPa.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [CEC for arithmetic circuits.]
+
+ Synopsis [Core procedures.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: acecPa.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acecInt.h"
+#include "misc/vec/vecWec.h"
+#include "misc/extra/extra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pas_ManVerifyPhaseOne_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+ int Truth0, Truth1;
+ if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+ return pObj->Value;
+ Gia_ObjSetTravIdCurrent(p, pObj);
+ assert( Gia_ObjIsAnd(pObj) );
+ assert( !Gia_ObjIsXor(pObj) );
+ Truth0 = Pas_ManVerifyPhaseOne_rec( p, Gia_ObjFanin0(pObj) );
+ Truth1 = Pas_ManVerifyPhaseOne_rec( p, Gia_ObjFanin1(pObj) );
+ Truth0 = Gia_ObjFaninC0(pObj) ? 0xFF & ~Truth0 : Truth0;
+ Truth1 = Gia_ObjFaninC1(pObj) ? 0xFF & ~Truth1 : Truth1;
+ return (pObj->Value = Truth0 & Truth1);
+}
+void Pas_ManVerifyPhaseOne( Gia_Man_t * p, Vec_Int_t * vAdds, int iBox, Vec_Bit_t * vPhase )
+{
+ Gia_Obj_t * pObj;
+ unsigned TruthXor, TruthMaj, Truths[3] = { 0xAA, 0xCC, 0xF0 };
+ int k, iObj, fFadd = Vec_IntEntry(vAdds, 6*iBox+2) > 0;
+
+ if ( !fFadd )
+ return;
+
+ Gia_ManIncrementTravId( p );
+ for ( k = 0; k < 3; k++ )
+ {
+ iObj = Vec_IntEntry( vAdds, 6*iBox+k );
+ if ( iObj == 0 )
+ continue;
+ pObj = Gia_ManObj( p, iObj );
+ pObj->Value = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~Truths[k] : Truths[k];
+ Gia_ObjSetTravIdCurrent( p, pObj );
+ }
+
+ iObj = Vec_IntEntry( vAdds, 6
generated by cgit v1.2.3 (git 2.25.1) at 2025-06-03 14:43:41 +0000
s, 6*iBox+4 );
+ TruthMaj = Pas_ManVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
+ TruthMaj = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~TruthMaj : TruthMaj;
+
+ if ( fFadd ) // FADD
+ {
+ if ( TruthXor != 0x96 )
+ printf( "Fadd %d sum is wrong.\n", iBox );
+ if ( TruthMaj != 0xE8 )
+ printf( "Fadd %d carry is wrong.\n", iBox );
+ }
+ else
+ {
+ if ( TruthXor != 0x66 )
+ printf( "Hadd %d sum is wrong.\n", iBox );
+ if ( TruthMaj != 0x88 )
+ printf( "Hadd %d carry is wrong.\n", iBox );
+ }
+}
+void Pas_ManVerifyPhase( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vOrder, Vec_Bit_t * vPhase )
+{
+ int k, iBox;
+ Vec_IntForEachEntry( vOrder, iBox, k )
+ Pas_ManVerifyPhaseOne( p, vAdds, iBox, vPhase );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pas_ManPhase_rec( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, Gia_Obj_t * pObj, int fPhase, Vec_Bit_t * vPhase, Vec_Bit_t * vConstPhase )
+{
+ int k, iBox, iXor, Sign, fXorPhase;
+ assert( pObj != Gia_ManConst0(p) );
+ if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+ return;
+ Gia_ObjSetTravIdCurrent(p, pObj);
+ if ( fPhase )
+ Vec_BitWriteEntry( vPhase, Gia_ObjId(p, pObj), fPhase );
+ if ( !Gia_ObjIsAnd(pObj) )
+ return;
+ iBox = Vec_IntEntry( vMap, Gia_ObjId(p, pObj) );
+ if ( iBox == -1 )
+ return;
+ iXor = Vec_IntEntry( vAdds, 6*iBox+3 );
+ Sign = Vec_IntEntry( vAdds, 6*iBox+5 );
+ fXorPhase = ((Sign >> 3) & 1);
+ // remember complemented HADD
+ if ( Vec_IntEntry(vAdds, 6*iBox+2) == 0 && fPhase )
+ Vec_BitWriteEntry( vConstPhase, iBox, 1 );
+ for ( k = 0; k < 3; k++ )
+ {
+ int iObj = Vec_IntEntry( vAdds, 6*iBox+k );
+ int fPhaseThis = ((Sign >> k) & 1) ^ fPhase;
+ fXorPhase ^= fPhaseThis;
+ if ( iObj == 0 )
+ continue;
+ Pas_ManPhase_rec( p, vAdds, vMap, Gia_ManObj(p, iObj), fPhaseThis, vPhase, vConstPhase );
+ }
+ Vec_BitWriteEntry( vPhase, iXor, fXorPhase );
+}
+Vec_Bit_t * Pas_ManPhase( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, Vec_Int_t * vRoots, Vec_Bit_t ** pvConstPhase )
+{
+ Vec_Bit_t * vPhase = Vec_BitStart( Vec_IntSize(vMap) );
+ Vec_Bit_t * vConstPhase = Vec_BitStart( Vec_IntSize(vAdds)/6 );
+ int i, iRoot;
+ Gia_ManIncrementTravId( p );
+ Vec_IntForEachEntry( vRoots, iRoot, i )
+ Pas_ManPhase_rec( p, vAdds, vMap, Gia_ManObj(p, iRoot), 1, vPhase, vConstPhase );
+ *pvConstPhase = vConstPhase;
+ return vPhase;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Pas_ManComputeCuts( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vOrder, Vec_Int_t * vIns, Vec_Int_t * vOuts )
+{
+ Vec_Bit_t * vUnique = Vec_BitStart( Gia_ManObjNum(p) );
+ Vec_Bit_t * vUsed = Vec_BitStart( Gia_ManObjNum(p) );
+ Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
+ Vec_Int_t * vRoots = Vec_IntAlloc( 100 );
+ Vec_Bit_t * vPhase, * vConstPhase;
+ int i, k, Entry, nTrees;
+
+ // map carries into adder indexes and mark driven nodes
+ Vec_IntForEachEntry( vOrder, i, k )
+ {
+ int Carry = Vec_IntEntry(vAdds, 6*i+4);
+ if ( Vec_BitEntry(vUnique, Carry) )
+ printf( "Carry %d participates more than once.\n", Carry );
+ Vec_BitWriteEntry( vUnique, Carry, 1 );
+ Vec_IntWriteEntry( vMap, Carry, i );
+ // mark driven
+ Vec_BitWriteEntry( vUsed, Vec_IntEntry(vAdds, 6*i+0), 1 );
+ Vec_BitWriteEntry( vUsed, Vec_IntEntry(vAdds, 6*i+1), 1 );
+ Vec_BitWriteEntry( vUsed, Vec_IntEntry(vAdds, 6*i+2), 1 );
+ }
+ // collect carries that do not drive other adders
+ for ( i = 0; i < Gia_ManObjNum(p); i++ )
+ if ( Vec_BitEntry(vUnique, i) && !Vec_BitEntry(vUsed, i) )
+ Vec_IntPush( vRoots, i );
+ nTrees = Vec_IntSize( vRoots );
+
+ Vec_IntPrint( vRoots );
+
+ // compute phases
+ if ( Vec_IntSize(vRoots) > 0 )
+ {
+ int nCompls = 0;
+
+ vPhase = Pas_ManPhase( p, vAdds, vMap, vRoots, &vConstPhase );
+ Pas_ManVerifyPhase( p, vAdds, vOrder, vPhase );
+
+ printf( "Outputs: " );
+ Vec_IntForEachEntry( vOuts, Entry, i )
+ printf( "%d(%d) ", Entry, Vec_BitEntry(vPhase, Entry) );
+ printf( "\n" );
+
+ printf( "Inputs: " );
+ Vec_IntForEachEntry( vIns, Entry, i )
+ {
+ printf( "%d(%d) ", Entry, Vec_BitEntry(vPhase, Entry) );
+ nCompls += Vec_BitEntry(vPhase, Entry);
+ }
+ printf( " Compl = %d\n", nCompls );
+
+ Vec_BitFreeP( &vPhase );
+ Vec_BitFreeP( &vConstPhase );
+ }
+
+ Vec_IntFree( vRoots );
+ Vec_IntFree( vMap );
+ Vec_BitFree( vUnique );
+ Vec_BitFree( vUsed );
+ return nTrees;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Pas_ManComputeCutsTest( Gia_Man_t * p )
+{
+ extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose );
+ extern 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 );
+
+ extern int Ree_ManCountFadds( Vec_Int_t * vAdds );
+ extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose );
+ abctime clk = Abc_Clock();
+ Vec_Int_t * vAdds = Ree_ManComputeCuts( p, 1 );
+ Vec_Int_t * vIns, * vOuts;
+ Vec_Int_t * vOrder = Gia_PolynCoreOrder( p, vAdds, NULL, &vIns, &vOuts );
+ int nTrees, nFadds = Ree_ManCountFadds( vAdds );
+ //Ree_ManPrintAdders( vAdds, 1 );
+ printf( "Detected %d FAs and %d HAs. Collected %d adders. ", nFadds, Vec_IntSize(vAdds)/6-nFadds, Vec_IntSize(vOrder) );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ // detect trees
+ clk = Abc_Clock();
+ nTrees = Pas_ManComputeCuts( p, vAdds, vOrder, vIns, vOuts );
+ Vec_IntFree( vAdds );
+ Vec_IntFree( vOrder );
+ Vec_IntFree( vIns );
+ Vec_IntFree( vOuts );
+
+ printf( "Detected %d adder trees. ", nTrees );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/acecPool.c b/src/proof/acec/acecPool.c
new file mode 100644
index 00000000..294066fa
--- /dev/null
+++ b/src/proof/acec/acecPool.c
@@ -0,0 +1,132 @@
+/**CFile****************************************************************
+
+ FileName [acecPool.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [CEC for arithmetic circuits.]
+
+ Synopsis [Core procedures.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: acecPool.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acecInt.h"
+#include "misc/vec/vecWec.h"
+#include "misc/extra/extra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Bit_t * Acec_ManPoolGetPointed( Gia_Man_t * p, Vec_Int_t * vAdds )
+{
+ Vec_Bit_t * vMarks = Vec_BitStart( Gia_ManObjNum(p) );
+ int i, k;
+ for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+ for ( k = 0; k < 3; k++ )
+ Vec_BitWriteEntry( vMarks, Vec_IntEntry(vAdds, 6*i+k), 1 );
+ return vMarks;
+}
+
+Vec_Int_t * Acec_ManPoolTopMost( Gia_Man_t * p, Vec_Int_t * vAdds )
+{
+ int i, k, iTop, fVerbose = 0;
+ Vec_Int_t * vTops = Vec_IntAlloc( 1000 );
+ Vec_Bit_t * vMarks = Acec_ManPoolGetPointed( p, vAdds );
+
+ for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+ if ( !Vec_BitEntry(vMarks, Vec_IntEntry(vAdds, 6*i+3)) &&
+ !Vec_BitEntry(vMarks, Vec_IntEntry(vAdds, 6*i+4)) )
+ Vec_IntPush( vTops, i );
+
+ if ( fVerbose )
+ Vec_IntForEachEntry( vTops, iTop, i )
+ {
+ printf( "%4d : ", iTop );
+ for ( k = 0; k < 3; k++ )
+ printf( "%4d ", Vec_IntEntry(vAdds, 6*iTop+k) );
+ printf( " -> " );
+ for ( k = 3; k < 5; k++ )
+ printf( "%4d ", Vec_IntEntry(vAdds, 6*iTop+k) );
+ printf( "\n" );
+ }
+
+ Vec_BitFree( vMarks );
+ return vTops;
+}
+void Acec_ManPool( Gia_Man_t * p )
+{
+ extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose );
+ extern Vec_Wec_t * Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vRootBoxes );
+
+ extern int Ree_ManCountFadds( Vec_Int_t * vAdds );
+ extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose );
+ extern void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds );
+ extern void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds );
+ Vec_Int_t * vTops, * vTree;
+ Vec_Wec_t * vTrees;
+
+ abctime clk = Abc_Clock();
+ Vec_Int_t * vAdds = Ree_ManComputeCuts( p, 1 );
+ int i, nFadds = Ree_ManCountFadds( vAdds );
+ printf( "Detected %d FAs and %d HAs. ", nFadds, Vec_IntSize(vAdds)/6-nFadds );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+
+ clk = Abc_Clock();
+ Ree_ManRemoveTrivial( p, vAdds );
+ Ree_ManRemoveContained( p, vAdds );
+ nFadds = Ree_ManCountFadds( vAdds );
+ printf( "Detected %d FAs and %d HAs. ", nFadds, Vec_IntSize(vAdds)/6-nFadds );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+
+ //Ree_ManPrintAdders( vAdds, 1 );
+
+ // detect topmost nodes
+ vTops = Acec_ManPoolTopMost( p, vAdds );
+ printf( "Detected %d topmost adder%s.\n", Vec_IntSize(vTops), Vec_IntSize(vTops) > 1 ? "s":"" );
+
+ // collect adder trees
+ vTrees = Gia_PolynCoreOrderArray( p, vAdds, vTops );
+ Vec_WecForEachLevel( vTrees, vTree, i )
+ printf( "Adder %5d : Tree with %5d nodes.\n", Vec_IntEntry(vTops, i), Vec_IntSize(vTree) );
+
+ Vec_WecFree( vTrees );
+ Vec_IntFree( vAdds );
+ Vec_IntFree( vTops );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/acecRe.c b/src/proof/acec/acecRe.c
index 1f10d249..e2340dba 100644
--- a/src/proof/acec/acecRe.c
+++ b/src/proof/acec/acecRe.c
@@ -69,6 +69,18 @@ void Ree_TruthPrecompute()
}
printf( "\n" );
}
+void Ree_TruthPrecompute2()
+{
+ int i, b;
+ for ( i = 0; i < 8; i++ )
+ {
+ word Truth = 0xE8;
+ for ( b = 0; b < 3; b++ )
+ if ( (i >> b) & 1 )
+ Truth = Abc_Tt6Flip( Truth, b );
+ printf( "%d = %X\n", i, 0xFF & (int)Truth );
+ }
+}
/**Function*************************************************************
@@ -239,7 +251,7 @@ void Ree_ManCutPrint( int * pCut, int Count, word Truth )
void Ree_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_Int_t * vCuts, Hash_IntMan_t * pHash, Vec_Int_t * vData )
{
int fVerbose = 0;
- int i, k, c, Value, Truth, TruthC, * pCut0, * pCut1, pCut[5], Count = 0;
+ int i, k, c, Value, Truth, TruthC, * pCut0, * pCut1, pCut[6], Count = 0;
if ( fVerbose )
printf( "Object %d\n", iObj );
Vec_IntFill( vCuts, 2, 1 );
@@ -290,7 +302,7 @@ void Ree_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I
***********************************************************************/
Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData )
{
- int i, j, k, iObj, iObj2, Value, Truth, CountX, CountM, Index = 0;
+ int i, j, k, iObj, iObj2, Value, Truth, Truth2, CountX, CountM, Index = 0;
int nEntries = Hash_IntManEntryNum(p);
Vec_Int_t * vAdds = Vec_IntAlloc( 1000 );
Vec_Int_t * vXors = Vec_IntStart( nEntries + 1 );
@@ -325,9 +337,9 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData )
if ( Index == -1 )
continue;
if ( Truth == 0x66 || Truth == 0x99 || Truth == 0x69 || Truth == 0x96 )
- Vec_WecPush( vXorMap, Index, iObj );
+ Vec_IntPushTwo( Vec_WecEntry(vXorMap, Index), iObj, Truth );
else
- Vec_WecPush( vMajMap, Index, iObj );
+ Vec_IntPushTwo( Vec_WecEntry(vMajMap, Index), iObj, Truth );
}
Vec_IntFree( vIndex );
// create pairs
@@ -336,11 +348,22 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData )
Vec_Int_t * vXorOne = Vec_WecEntry( vXorMap, i );
Vec_Int_t * vMajOne = Vec_WecEntry( vMajMap, i );
Hash_IntObj_t * pObj = Hash_IntObj( p, Value );
- Vec_IntForEachEntry( vXorOne, iObj, j )
- Vec_IntForEachEntry( vMajOne, iObj2, k )
+ Vec_IntForEachEntryDouble( vXorOne, iObj, Truth, j )
+ Vec_IntForEachEntryDouble( vMajOne, iObj2, Truth2, k )
{
+ int SignAnd[8] = {0x88, 0x44, 0x22, 0x11, 0xEE, 0xDD, 0xBB, 0x77};
+ int SignMaj[8] = {0xE8, 0xD4, 0xB2, 0x71, 0x8E, 0x4D, 0x2B, 0x17};
+ int n, SignXor = (Truth == 0x99 || Truth == 0x69) << 3;
+ for ( n = 0; n < 8; n++ )
+ if ( Truth2 == SignMaj[n] )
+ break;
+ if ( n == 8 )
+ for ( n = 0; n < 8; n++ )
+ if ( Truth2 == SignAnd[n] )
+ break;
+ assert( n < 8 );
Vec_IntPushThree( vAdds, pObj->iData0, pObj->iData1, pObj->iData2 );
- Vec_IntPushTwo( vAdds, iObj, iObj2 );
+ Vec_IntPushThree( vAdds, iObj, iObj2, SignXor | n );
}
}
Vec_IntFree( vIndexRev );
@@ -384,7 +407,7 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose )
vAdds = Ree_ManDeriveAdds( pHash, vData );
if ( fVerbose )
printf( "Adds = %d. Total = %d. Hashed = %d. Hashed/Adds = %.2f.\n",
- Vec_IntSize(vAdds)/5, Vec_IntSize(vData)/3, Hash_IntManEntryNum(pHash), 5.0*Hash_IntManEntryNum(pHash)/Vec_IntSize(vAdds) );
+ Vec_IntSize(vAdds)/6, Vec_IntSize(vData)/3, Hash_IntManEntryNum(pHash), 6.0*Hash_IntManEntryNum(pHash)/Vec_IntSize(vAdds) );
Vec_IntFree( vData );
Hash_IntManStop( pHash );
return vAdds;
@@ -392,6 +415,52 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose )
/**Function*************************************************************
+ Synopsis [Highlight nodes inside FAs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ree_CollectInsiders_rec( Gia_Man_t * pGia, int iObj, Vec_Bit_t * vVisited, Vec_Bit_t * vInsiders )
+{
+ if ( Vec_BitEntry(vVisited, iObj) )
+ return;
+ Vec_BitSetEntry( vVisited, iObj, 1 );
+ Ree_CollectInsiders_rec( pGia, Gia_ObjFaninId0p(pGia, Gia_ManObj(pGia, iObj)), vVisited, vInsiders );
+ Ree_CollectInsiders_rec( pGia, Gia_ObjFaninId1p(pGia, Gia_ManObj(pGia, iObj)), vVisited, vInsiders );
+ Vec_BitSetEntry( vInsiders, iObj, 1 );
+}
+Vec_Bit_t * Ree_CollectInsiders( Gia_Man_t * pGia, Vec_Int_t * vAdds )
+{
+ Vec_Bit_t * vVisited = Vec_BitStart( Gia_ManObjNum(pGia) );
+ Vec_Bit_t * vInsiders = Vec_BitStart( Gia_ManObjNum(pGia) );
+ int i, Entry1, Entry2, Entry3;
+ for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+ {
+ if ( Vec_IntEntry(vAdds, 6*i+2) == 0 ) // HADD
+ continue;
+ // mark inputs
+ Entry1 = Vec_IntEntry( vAdds, 6*i + 0 );
+ Entry2 = Vec_IntEntry( vAdds, 6*i + 1 );
+ Entry3 = Vec_IntEntry( vAdds, 6*i + 2 );
+ Vec_BitWriteEntry( vVisited, Entry1, 1 );
+ Vec_BitWriteEntry( vVisited, Entry2, 1 );
+ Vec_BitWriteEntry( vVisited, Entry3, 1 );
+ // traverse from outputs
+ Entry1 = Vec_IntEntry( vAdds, 6*i + 3 );
+ Entry2 = Vec_IntEntry( vAdds, 6*i + 4 );
+ Ree_CollectInsiders_rec( pGia, Entry1, vVisited, vInsiders );
+ Ree_CollectInsiders_rec( pGia, Entry2, vVisited, vInsiders );
+ }
+ Vec_BitFree( vVisited );
+ return vInsiders;
+}
+
+/**Function*************************************************************
+
Synopsis []
Description []
@@ -401,28 +470,80 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose )
SeeAlso []
***********************************************************************/
-void Ree_ManComputeCutsTest( Gia_Man_t * p )
+// removes HAs whose AND2 is part of XOR2 without additional fanout
+void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds )
+{
+ Gia_Obj_t * pObjX, * pObjM;
+ int i, k = 0;
+ ABC_FREE( p->pRefs );
+ Gia_ManCreateRefs( p );
+ for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+ {
+ if ( Vec_IntEntry(vAdds, 6*i+2) == 0 ) // HADD
+ {
+ pObjX = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*i+3) );
+ pObjM = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*i+4) );
+ if ( (pObjM == Gia_ObjFanin0(pObjX) || pObjM == Gia_ObjFanin1(pObjX)) && Gia_ObjRefNum(p, pObjM) == 1 )
+ continue;
+ }
+ memmove( Vec_IntArray(vAdds) + 6*k++, Vec_IntArray(vAdds) + 6*i, 6*sizeof(int) );
+ }
+ assert( k <= i );
+ Vec_IntShrink( vAdds, 6*k );
+}
+// removes HAs fully contained inside FAs
+void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds )
+{
+ Vec_Bit_t * vInsiders = Ree_CollectInsiders( p, vAdds );
+ int i, k = 0;
+ for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+ {
+ if ( Vec_IntEntry(vAdds, 6*i+2) == 0 ) // HADD
+ if ( Vec_BitEntry(vInsiders, Vec_IntEntry(vAdds, 6*i+3)) && Vec_BitEntry(vInsiders, Vec_IntEntry(vAdds, 6*i+4)) )
+ continue;
+ memmove( Vec_IntArray(vAdds) + 6*k++, Vec_IntArray(vAdds) + 6*i, 6*sizeof(int) );
+ }
+ assert( k <= i );
+ Vec_IntShrink( vAdds, 6*k );
+ Vec_BitFree( vInsiders );
+}
+
+int Ree_ManCountFadds( Vec_Int_t * vAdds )
{
- abctime clk = Abc_Clock();
- Vec_Int_t * vAdds = Ree_ManComputeCuts( p, 1 );
int i, Count = 0;
- for ( i = 0; 5*i < Vec_IntSize(vAdds); i++ )
+ for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+ if ( Vec_IntEntry(vAdds, 6*i+2) != 0 )
+ Count++;
+ return Count;
+}
+void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose )
+{
+ int i;
+ for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
{
- if ( Vec_IntEntry(vAdds, 5*i+2) == 0 )
+ //if ( Vec_IntEntry(vAdds, 6*i+2) == 0 )
+ // continue;
+ if ( !fVerbose )
continue;
- Count++;
- continue;
printf( "%6d : ", i );
- printf( "%6d ", Vec_IntEntry(vAdds, 5*i+0) );
- printf( "%6d ", Vec_IntEntry(vAdds, 5*i+1) );
- printf( "%6d ", Vec_IntEntry(vAdds, 5*i+2) );
+ printf( "%6d ", Vec_IntEntry(vAdds, 6*i+0) );
+ printf( "%6d ", Vec_IntEntry(vAdds, 6*i+1) );
+ printf( "%6d ", Vec_IntEntry(vAdds, 6*i+2) );
printf( " -> " );
- printf( "%6d ", Vec_IntEntry(vAdds, 5*i+3) );
- printf( "%6d ", Vec_IntEntry(vAdds, 5*i+4) );
+ printf( "%6d ", Vec_IntEntry(vAdds, 6*i+3) );
+ printf( "%6d ", Vec_IntEntry(vAdds, 6*i+4) );
+ printf( " (%d)", Vec_IntEntry(vAdds, 6*i+5) );
printf( "\n" );
}
+}
+void Ree_ManComputeCutsTest( Gia_Man_t * p )
+{
+ abctime clk = Abc_Clock();
+ Vec_Int_t * vAdds = Ree_ManComputeCuts( p, 1 );
+ int nFadds = Ree_ManCountFadds( vAdds );
+ Ree_ManPrintAdders( vAdds, 1 );
+ printf( "Detected %d FAs and %d HAs. ", nFadds, Vec_IntSize(vAdds)/6-nFadds );
Vec_IntFree( vAdds );
- printf( "Detected %d FAs and %d HAs. ", Count, Vec_IntSize(vAdds)/5-Count );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
diff --git a/src/proof/acec/module.make b/src/proof/acec/module.make
index e66bf6e8..df6db695 100644
--- a/src/proof/acec/module.make
+++ b/src/proof/acec/module.make
@@ -1,7 +1,10 @@
-SRC += src/proof/acec/acecCore.c \
+SRC += src/proof/acec/acecCl.c \
+ src/proof/acec/acecCore.c \
src/proof/acec/acecCo.c \
src/proof/acec/acecRe.c \
+ src/proof/acec/acecPa.c \
src/proof/acec/acecPo.c \
+ src/proof/acec/acecPool.c \
src/proof/acec/acecCover.c \
src/proof/acec/acecFadds.c \
src/proof/acec/acecOrder.c \
generated by cgit v1.2.3 (git 2.25.1) at 2025-06-03 14:43:41 +0000