summaryrefslogtreecommitdiffstats
path: root/src/proof/acec
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2017-01-30 08:39:26 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2017-01-30 08:39:26 -0800
commite21c7d72f3f43f38e5af10a38602de6f6ce9a20e (patch)
tree5588d95ce29d853efe311c7c63caf0a64f63d971 /src/proof/acec
parent3020d57ea67f7f897c93524b9c3025767db3933b (diff)
downloadabc-e21c7d72f3f43f38e5af10a38602de6f6ce9a20e.tar.gz
abc-e21c7d72f3f43f38e5af10a38602de6f6ce9a20e.tar.bz2
abc-e21c7d72f3f43f38e5af10a38602de6f6ce9a20e.zip
Updates to arithmetic verification.
Diffstat (limited to 'src/proof/acec')
-rw-r--r--src/proof/acec/acecInt.h1
-rw-r--r--src/proof/acec/acecMult.c66
-rw-r--r--src/proof/acec/acecStruct.c271
-rw-r--r--src/proof/acec/acecXor.c67
4 files changed, 400 insertions, 5 deletions
diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h
index 381ab8d1..c4c8061e 100644
--- a/src/proof/acec/acecInt.h
+++ b/src/proof/acec/acecInt.h
@@ -76,6 +76,7 @@ extern Vec_Wec_t * Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdd
/*=== acecMult.c ========================================================*/
extern Vec_Int_t * Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec_t * vRootLits );
extern Vec_Bit_t * Acec_BoothFindPPG( Gia_Man_t * p );
+extern Vec_Bit_t * Acec_MultMarkPPs( Gia_Man_t * p );
/*=== acecNorm.c ========================================================*/
extern void Acec_InsertFadd( Gia_Man_t * pNew, int In[3], int Out[2] );
extern Gia_Man_t * Acec_InsertBox( Acec_Box_t * pBox, int fAll );
diff --git a/src/proof/acec/acecMult.c b/src/proof/acec/acecMult.c
index ba9405ac..c63fdde2 100644
--- a/src/proof/acec/acecMult.c
+++ b/src/proof/acec/acecMult.c
@@ -435,6 +435,72 @@ Vec_Int_t * Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec
/**Function*************************************************************
+ Synopsis [Mark nodes whose function is exactly that of a Booth PP.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Bit_t * Acec_MultMarkPPs( Gia_Man_t * p )
+{
+ word Saved[32] = {
+ ABC_CONST(0xF335ACC0F335ACC0),
+ ABC_CONST(0x35C035C035C035C0),
+ ABC_CONST(0xD728D728D728D728),
+ ABC_CONST(0xFD80FD80FD80FD80),
+ ABC_CONST(0xACC0ACC0ACC0ACC0),
+ ABC_CONST(0x7878787878787878),
+ ABC_CONST(0x2828282828282828),
+ ABC_CONST(0xD0D0D0D0D0D0D0D0),
+ ABC_CONST(0x8080808080808080),
+ ABC_CONST(0x8888888888888888),
+ ABC_CONST(0xAAAAAAAAAAAAAAAA),
+ ABC_CONST(0x5555555555555555),
+
+ ABC_CONST(0xD5A8D5A8D5A8D5A8),
+ ABC_CONST(0x2A572A572A572A57),
+ ABC_CONST(0xF3C0F3C0F3C0F3C0),
+ ABC_CONST(0x5858585858585858),
+ ABC_CONST(0xA7A7A7A7A7A7A7A7),
+ ABC_CONST(0x2727272727272727),
+ ABC_CONST(0xD8D8D8D8D8D8D8D8)
+ };
+
+ Vec_Bit_t * vRes = Vec_BitStart( Gia_ManObjNum(p) );
+ Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
+ Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
+ int i, iObj, nProds = 0;
+ Gia_ManCleanMark0(p);
+ Gia_ManForEachAndId( p, iObj )
+ {
+ word Truth = Gia_ObjComputeTruth6Cis( p, Abc_Var2Lit(iObj, 0), vSupp, vTemp );
+ if ( Vec_IntSize(vSupp) > 6 )
+ continue;
+ vSupp->nSize = Abc_Tt6MinBase( &Truth, vSupp->pArray, vSupp->nSize );
+ if ( Vec_IntSize(vSupp) > 5 )
+ continue;
+ for ( i = 0; i < 32 && Saved[i]; i++ )
+ {
+ if ( Truth == Saved[i] || Truth == ~Saved[i] )
+ {
+ Vec_BitWriteEntry( vRes, iObj, 1 );
+ nProds++;
+ break;
+ }
+ }
+ }
+ Gia_ManCleanMark0(p);
+ printf( "Collected %d pps.\n", nProds );
+ Vec_IntFree( vSupp );
+ Vec_WrdFree( vTemp );
+ return vRes;
+}
+
+/**Function*************************************************************
+
Synopsis []
Description []
diff --git a/src/proof/acec/acecStruct.c b/src/proof/acec/acecStruct.c
new file mode 100644
index 00000000..6702e13b
--- /dev/null
+++ b/src/proof/acec/acecStruct.c
@@ -0,0 +1,271 @@
+/**CFile****************************************************************
+
+ FileName [acecStruct.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: acecStruct.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_Int_t * Acec_StructDetectXorRoots( Gia_Man_t * p )
+{
+ Vec_Int_t * vXors = Vec_IntAlloc( 100 );
+ Vec_Bit_t * vXorIns = Vec_BitStart( Gia_ManObjNum(p) );
+ Gia_Obj_t * pFan0, * pFan1, * pObj;
+ int i, k = 0, Entry;
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
+ continue;
+ Vec_IntPush( vXors, i );
+ Vec_BitWriteEntry( vXorIns, Gia_ObjId(p, Gia_Regular(pFan0)), 1 );
+ Vec_BitWriteEntry( vXorIns, Gia_ObjId(p, Gia_Regular(pFan1)), 1 );
+ }
+ // collect XORs that not inputs of other XORs
+ Vec_IntForEachEntry( vXors, Entry, i )
+ if ( !Vec_BitEntry(vXorIns, Entry) )
+ Vec_IntWriteEntry( vXors, k++, Entry );
+ Vec_IntShrink( vXors, k );
+ Vec_BitFree( vXorIns );
+ return vXors;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Acec_StructAssignRanks( Gia_Man_t * p, Vec_Int_t * vXorRoots )
+{
+ Vec_Int_t * vDoubles = Vec_IntAlloc( 100 );
+ Gia_Obj_t * pFan0, * pFan1, * pObj;
+ int i, k, Fanins[2], Entry, Rank;
+ // map roots into their ranks
+ Vec_Int_t * vRanks = Vec_IntStartFull( Gia_ManObjNum(p) );
+ Vec_IntForEachEntry( vXorRoots, Entry, i )
+ Vec_IntWriteEntry( vRanks, Entry, i );
+ // map nodes into their ranks
+ Gia_ManForEachAndReverse( p, pObj, i )
+ {
+ if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
+ continue;
+ Rank = Vec_IntEntry( vRanks, i );
+ // skip XORs that are not part of any tree
+ if ( Rank == -1 )
+ continue;
+ // iterate through XOR inputs
+ Fanins[0] = Gia_ObjId(p, Gia_Regular(pFan0));
+ Fanins[1] = Gia_ObjId(p, Gia_Regular(pFan1));
+ for ( k = 0; k < 2; k++ )
+ {
+ Entry = Vec_IntEntry( vRanks, Fanins[k] );
+ if ( Entry == Rank ) // the same tree -- allow fanout in this tree
+ continue;
+ if ( Entry == -1 )
+ Vec_IntWriteEntry( vRanks, Fanins[k], Rank );
+ else
+ Vec_IntPush( vDoubles, Fanins[k] );
+ if ( Entry != -1 && Gia_ObjIsAnd(Gia_ManObj(p, Fanins[k])))
+ printf( "Xor node %d belongs to Tree %d and Tree %d.\n", Fanins[k], Entry, Rank );
+ }
+ }
+ // remove duplicated entries
+ Vec_IntForEachEntry( vDoubles, Entry, i )
+ Vec_IntWriteEntry( vRanks, Entry, -1 );
+ Vec_IntFree( vDoubles );
+ return vRanks;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Wec_t * Acec_FindTreeLeaves( Gia_Man_t * p, Vec_Int_t * vXorRoots, Vec_Int_t * vRanks )
+{
+ Vec_Bit_t * vMapXors = Vec_BitStart( Gia_ManObjNum(p) );
+ Vec_Wec_t * vTreeLeaves = Vec_WecStart( Vec_IntSize(vXorRoots) );
+ Gia_Obj_t * pFan0, * pFan1, * pObj;
+ int i, k, Fanins[2], Rank;
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
+ continue;
+ Vec_BitWriteEntry( vMapXors, i, 1 );
+ Rank = Vec_IntEntry( vRanks, i );
+ // skip XORs that are not part of any tree
+ if ( Rank == -1 )
+ continue;
+ // iterate through XOR inputs
+ Fanins[0] = Gia_ObjId(p, Gia_Regular(pFan0));
+ Fanins[1] = Gia_ObjId(p, Gia_Regular(pFan1));
+ for ( k = 0; k < 2; k++ )
+ {
+ if ( Vec_BitEntry(vMapXors, Fanins[k]) )
+ {
+ assert( Rank == Vec_IntEntry(vRanks, Fanins[k]) );
+ continue;
+ }
+ Vec_WecPush( vTreeLeaves, Rank, Fanins[k] );
+ }
+ }
+ Vec_BitFree( vMapXors );
+ return vTreeLeaves;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Acec_FindShadows( Gia_Man_t * p, Vec_Int_t * vRanks )
+{
+ Vec_Int_t * vShadows = Vec_IntDup( vRanks );
+ Gia_Obj_t * pObj; int i, Shad0, Shad1;
+ Gia_ManForEachCi( p, pObj, i )
+ Vec_IntWriteEntry( vShadows, Gia_ObjId(p, pObj), -1 );
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ if ( Vec_IntEntry(vShadows, i) >= 0 )
+ continue;
+ Shad0 = Vec_IntEntry(vShadows, Gia_ObjFaninId0(pObj, i));
+ Shad1 = Vec_IntEntry(vShadows, Gia_ObjFaninId1(pObj, i));
+ if ( Shad0 == Shad1 && Shad0 != -1 )
+ Vec_IntWriteEntry(vShadows, i, Shad0);
+ }
+ return vShadows;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Acec_CollectSupp_rec( Gia_Man_t * p, int iNode, int Rank, Vec_Int_t * vRanks )
+{
+ Gia_Obj_t * pObj;
+ int nSize;
+ if ( Gia_ObjIsTravIdCurrentId(p, iNode) )
+ return 0;
+ Gia_ObjSetTravIdCurrentId(p, iNode);
+ pObj = Gia_ManObj(p, iNode);
+ assert( Gia_ObjIsAnd(pObj) );
+ if ( Vec_IntEntry(vRanks, iNode) == Rank )
+ return 1;
+ nSize = Acec_CollectSupp_rec( p, Gia_ObjFaninId0(pObj, iNode), Rank, vRanks );
+ nSize += Acec_CollectSupp_rec( p, Gia_ObjFaninId1(pObj, iNode), Rank, vRanks );
+ return nSize;
+}
+Vec_Wec_t * Acec_FindNexts( Gia_Man_t * p, Vec_Int_t * vRanks, Vec_Int_t * vShadows, Vec_Wec_t * vTreeLeaves )
+{
+ Vec_Wec_t * vNexts = Vec_WecStart( Vec_WecSize(vTreeLeaves) );
+ Vec_Int_t * vTree;
+ int i, k, Node, Fanins[2], Shad0, Shad1, Rank, nSupp;
+ Vec_WecForEachLevel( vTreeLeaves, vTree, i )
+ Vec_IntForEachEntry( vTree, Node, k )
+ {
+ Gia_Obj_t * pObj = Gia_ManObj(p, Node);
+ if ( !Gia_ObjIsAnd(pObj) )
+ continue;
+ Fanins[0] = Gia_ObjFaninId0(pObj, Node);
+ Fanins[1] = Gia_ObjFaninId1(pObj, Node);
+ Shad0 = Vec_IntEntry(vShadows, Fanins[0]);
+ Shad1 = Vec_IntEntry(vShadows, Fanins[1]);
+ if ( Shad0 != Shad1 || Shad0 == -1 )
+ continue;
+ // check support size of Node in terms of the shadow of its fanins
+ Rank = Vec_IntEntry( vRanks, Node );
+ assert( Rank != Shad0 );
+ Gia_ManIncrementTravId( p );
+ nSupp = Acec_CollectSupp_rec( p, Node, Shad0, vRanks );
+ assert( nSupp > 1 );
+ if ( nSupp > 3 )
+ continue;
+ Vec_IntPushUniqueOrder( Vec_WecEntry(vNexts, Shad0), Rank );
+ }
+ return vNexts;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Acec_StructTest( Gia_Man_t * p )
+{
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/acecXor.c b/src/proof/acec/acecXor.c
index acbde1a0..71e0b7b3 100644
--- a/src/proof/acec/acecXor.c
+++ b/src/proof/acec/acecXor.c
@@ -44,6 +44,35 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
+void Acec_CheckXors( Gia_Man_t * p, Vec_Int_t * vXors )
+{
+ Gia_Obj_t * pFan0, * pFan1;
+ Vec_Int_t * vCount2 = Vec_IntAlloc( Gia_ManObjNum(p) );
+ int i, Entry, Count = 0;
+ for ( i = 0; 4*i < Vec_IntSize(vXors); i++ )
+ if ( Vec_IntEntry(vXors, 4*i+3) == 0 )
+ Vec_IntAddToEntry( vCount2, Vec_IntEntry(vXors, 4*i), 1 );
+ Vec_IntForEachEntry( vCount2, Entry, i )
+ if ( Entry > 1 )
+ printf( "*** Obj %d has %d two-input XOR cuts.\n", i, Entry ), Count++;
+ else if ( Entry == 1 && Gia_ObjRecognizeExor(Gia_ManObj(p, i), &pFan0, &pFan1) )
+ printf( "*** Obj %d cannot be recognized as XOR.\n", i );
+ if ( Count == 0 )
+ printf( "*** There no multiple two-input XOR cuts.\n" );
+ Vec_IntFree( vCount2 );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Vec_Int_t * Acec_OrderTreeRoots( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vXorRoots, Vec_Int_t * vRanks )
{
Vec_Int_t * vOrder = Vec_IntAlloc( Vec_IntSize(vXorRoots) );
@@ -151,7 +180,6 @@ Vec_Int_t * Acec_FindXorRoots( Gia_Man_t * p, Vec_Int_t * vXors )
if ( !Vec_BitEntry(vMapXorIns, Vec_IntEntry(vXors, 4*i)) )
Vec_IntPushUniqueOrder( vXorRoots, Vec_IntEntry(vXors, 4*i) );
Vec_BitFree( vMapXorIns );
-//Vec_IntRemove( vXorRoots, 54 );
return vXorRoots;
}
// collects XOR trees belonging to each of XOR roots
@@ -184,8 +212,9 @@ Vec_Int_t * Acec_RankTrees( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vXorRo
Vec_IntWriteEntry( vRanks, Node, Rank );
else
Vec_IntPush( vDoubles, Node );
- //if ( Entry != -1 )
- //printf( "Xor node %d belongs to Tree %d and Tree %d.\n", Node, Entry, Rank );
+
+ if ( Entry != -1 && Gia_ObjIsAnd(Gia_ManObj(p, Node)))
+ printf( "Xor node %d belongs to Tree %d and Tree %d.\n", Node, Entry, Rank );
}
}
// remove duplicated entries
@@ -211,6 +240,7 @@ Vec_Wec_t * Acec_FindXorLeaves( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vA
for ( k = 1; k < 4; k++ )
{
int Fanin = Vec_IntEntry(vXors, 4*i+k);
+ //int RankFanin = Vec_IntEntry(vRanks, Fanin);
if ( Fanin == 0 )
continue;
if ( Vec_BitEntry(vMapXors, Fanin) )
@@ -218,6 +248,8 @@ Vec_Wec_t * Acec_FindXorLeaves( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vA
assert( Rank == Vec_IntEntry(vRanks, Fanin) );
continue;
}
+// if ( Vec_BitEntry(vMapXors, Fanin) && Rank == RankFanin )
+// continue;
if ( Vec_IntEntry(vMapMajs, Fanin) == -1 ) // no adder driving this input
Vec_WecPush( vXorLeaves, Rank, Fanin );
else if ( Vec_IntEntry(vRanks, Xor) > 0 ) // save adder box
@@ -230,7 +262,26 @@ Vec_Wec_t * Acec_FindXorLeaves( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vA
*pvAddBoxes = vAddBoxes;
return vXorLeaves;
}
+void Acec_CheckBoothPPs( Gia_Man_t * p, Vec_Wec_t * vLitLeaves )
+{
+ Vec_Bit_t * vMarked = Acec_MultMarkPPs( p );
+ Vec_Int_t * vLevel;
+ int i, k, iLit;
+ Vec_WecForEachLevel( vLitLeaves, vLevel, i )
+ {
+ int CountPI = 0, CountB = 0, CountNB = 0;
+ Vec_IntForEachEntry( vLevel, iLit, k )
+ if ( !Gia_ObjIsAnd(Gia_ManObj(p, Abc_Lit2Var(iLit))) )
+ CountPI++;
+ else if ( Vec_BitEntry( vMarked, Abc_Lit2Var(iLit) ) )
+ CountB++;
+ else
+ CountNB++;
+ printf( "Rank %2d : Lits = %5d PI = %d Booth = %5d Non-Booth = %5d\n", i, Vec_IntSize(vLevel), CountPI, CountB, CountNB );
+ }
+ Vec_BitFree( vMarked );
+}
Acec_Box_t * Acec_FindBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vAddBoxes, Vec_Wec_t * vXorLeaves, Vec_Int_t * vXorRoots )
{
extern Vec_Int_t * Acec_TreeCarryMap( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes );
@@ -315,6 +366,8 @@ Acec_Box_t * Acec_FindBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vAddBox
Vec_IntSort( vLevel, 0 );
Vec_WecForEachLevel( pBox->vRootLits, vLevel, i )
Vec_IntSort( vLevel, 1 );
+
+ //Acec_CheckBoothPPs( p, pBox->vLeafLits );
return pBox;
}
@@ -331,9 +384,13 @@ Acec_Box_t * Acec_ProduceBox( Gia_Man_t * p, int fVerbose )
Gia_ManLevelNum(p);
+ //Acec_CheckXors( p, vXors );
+
//Ree_ManPrintAdders( vAdds, 1 );
- printf( "Detected %d full-adders and %d half-adders. Found %d XOR-cuts. ", Ree_ManCountFadds(vAdds), Vec_IntSize(vAdds)/6-Ree_ManCountFadds(vAdds), Vec_IntSize(vXors)/4 );
- Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ if ( fVerbose )
+ printf( "Detected %d full-adders and %d half-adders. Found %d XOR-cuts. ", Ree_ManCountFadds(vAdds), Vec_IntSize(vAdds)/6-Ree_ManCountFadds(vAdds), Vec_IntSize(vXors)/4 );
+ if ( fVerbose )
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
vXorRoots = Acec_OrderTreeRoots( p, vAdds, vTemp = vXorRoots, vRanks );
Vec_IntFree( vTemp );