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

Updates to arithmetic verification.

This commit is contained in:
Alan Mishchenko 2017-01-30 08:39:26 -08:00
parent 3020d57ea6
commit e21c7d72f3
7 changed files with 407 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -5551,6 +5551,10 @@ SOURCE=.\src\proof\acec\acecSt.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\acec\acecStruct.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\acec\acecTree.c
# End Source File
# Begin Source File

4
src/aig/gia/giaUtil.c
View File

@ -937,8 +937,8 @@ int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ppFan0, Gia_Obj_t ** pp
return 0;
if ( Gia_ObjFaninC0(p0) == Gia_ObjFaninC0(p1) || Gia_ObjFaninC1(p0) == Gia_ObjFaninC1(p1) )
return 0;
*ppFan0 = Gia_ObjChild0(p0);
*ppFan1 = Gia_ObjChild1(p0);
if ( ppFan0 ) *ppFan0 = Gia_ObjChild0(p0);
if ( ppFan1 ) *ppFan1 = Gia_ObjChild1(p0);
return 1;
}

2
src/base/io/io.c
View File

@ -2150,7 +2150,7 @@ int IoCommandWriteCnf2( Abc_Frame_t * pAbc, int argc, char **argv )
extern void Mf_ManDumpCnf( Gia_Man_t * p, char * pFileName, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
FILE * pFile;
char * pFileName;
int nLutSize = 6;
int nLutSize = 8;
int fNewAlgo = 1;
int fCnfObjIds = 0;
int fAddOrCla = 1;

1
src/proof/acec/acecInt.h
View File

@ -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 );

66
src/proof/acec/acecMult.c
View File

@ -433,6 +433,72 @@ Vec_Int_t * Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec
return vInputs;
}
/**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 []

271
src/proof/acec/acecStruct.c Normal file
View File

@ -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

67
src/proof/acec/acecXor.c
View File

@ -33,6 +33,35 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
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 []
@ -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 );