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-15 20:59:59 +07:00
parent 1b86911c4f
commit 153b71c140
13 changed files with 505 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abcexe.dsp
View File

@ -88,6 +88,10 @@ LINK32=link.exe
# PROP Default_Filter "cpp;c;cxx;rc;def;r;odl;idl;hpj;bat"
# Begin Source File
SOURCE=.\src\proof\acec\acecTree.c
# End Source File
# Begin Source File
SOURCE=.\src\base\main\main.c
# End Source File
# End Group

2
src/aig/gia/gia.h
View File

@ -1242,6 +1242,8 @@ extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias );
extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes );
extern Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis );
extern Gia_Man_t * Gia_ManDupAndCones( Gia_Man_t * p, int * pAnds, int nAnds, int fTrimPis );
extern Gia_Man_t * Gia_ManDupAndConesLimit( Gia_Man_t * p, int * pAnds, int nAnds, int Level );
extern Gia_Man_t * Gia_ManDupAndConesLimit2( Gia_Man_t * p, int * pAnds, int nAnds, int Level );
extern Gia_Man_t * Gia_ManDupOneHot( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupLevelized( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupFromVecs( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs );

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

@ -3045,6 +3045,71 @@ Gia_Man_t * Gia_ManDupAndCones( Gia_Man_t * p, int * pAnds, int nAnds, int fTrim
Vec_PtrFree( vRoots );
return pNew;
}
void Gia_ManDupAndConesLimit_rec( Gia_Man_t * pNew, Gia_Man_t * p, int iObj, int Level )
{
Gia_Obj_t * pObj = Gia_ManObj(p, iObj);
if ( ~pObj->Value )
return;
if ( !Gia_ObjIsAnd(pObj) || Gia_ObjLevel(p, pObj) < Level )
{
pObj->Value = Gia_ManAppendCi( pNew );
//printf( "PI %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj );
return;
}
Gia_ManDupAndConesLimit_rec( pNew, p, Gia_ObjFaninId0(pObj, iObj), Level );
Gia_ManDupAndConesLimit_rec( pNew, p, Gia_ObjFaninId1(pObj, iObj), Level );
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
//printf( "Obj %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj );
}
Gia_Man_t * Gia_ManDupAndConesLimit( Gia_Man_t * p, int * pAnds, int nAnds, int Level )
{
Gia_Man_t * pNew;
int i;
pNew = Gia_ManStart( 1000 );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManLevelNum( p );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
for ( i = 0; i < nAnds; i++ )
Gia_ManDupAndConesLimit_rec( pNew, p, pAnds[i], Level );
for ( i = 0; i < nAnds; i++ )
Gia_ManAppendCo( pNew, Gia_ManObj(p, pAnds[i])->Value );
return pNew;
}
void Gia_ManDupAndConesLimit2_rec( Gia_Man_t * pNew, Gia_Man_t * p, int iObj, int Level )
{
Gia_Obj_t * pObj = Gia_ManObj(p, iObj);
if ( ~pObj->Value )
return;
if ( !Gia_ObjIsAnd(pObj) || Level <= 0 )
{
pObj->Value = Gia_ManAppendCi( pNew );
//printf( "PI %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj );
return;
}
Gia_ManDupAndConesLimit2_rec( pNew, p, Gia_ObjFaninId0(pObj, iObj), Level-1 );
Gia_ManDupAndConesLimit2_rec( pNew, p, Gia_ObjFaninId1(pObj, iObj), Level-1 );
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
//printf( "Obj %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj );
}
Gia_Man_t * Gia_ManDupAndConesLimit2( Gia_Man_t * p, int * pAnds, int nAnds, int Level )
{
Gia_Man_t * pNew;
int i;
pNew = Gia_ManStart( 1000 );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
for ( i = 0; i < nAnds; i++ )
Gia_ManDupAndConesLimit2_rec( pNew, p, pAnds[i], Level );
for ( i = 0; i < nAnds; i++ )
Gia_ManAppendCo( pNew, Gia_ManObj(p, pAnds[i])->Value );
return pNew;
}
/**Function*************************************************************

13
src/aig/gia/giaShow.c
View File

@ -1014,16 +1014,23 @@ void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold, Vec_In
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ShowMapAdds( Gia_Man_t * p, Vec_Int_t * vAdds, int fFadds )
Vec_Int_t * Gia_ShowMapAdds( Gia_Man_t * p, Vec_Int_t * vAdds, int fFadds, Vec_Int_t * vBold )
{
Vec_Int_t * vMapAdds = Vec_IntStartFull( Gia_ManObjNum(p) ); int i;
Vec_Bit_t * vIsBold = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Int_t * vMapAdds = Vec_IntStartFull( Gia_ManObjNum(p) ); int i, Entry;
if ( vBold )
Vec_IntForEachEntry( vBold, Entry, i )
Vec_BitWriteEntry( vIsBold, Entry, 1 );
for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
{
if ( fFadds && Vec_IntEntry(vAdds, 6*i+2) == 0 )
continue;
if ( Vec_BitEntry(vIsBold, Vec_IntEntry(vAdds, 6*i+3)) || Vec_BitEntry(vIsBold, Vec_IntEntry(vAdds, 6*i+4)) )
continue;
Vec_IntWriteEntry( vMapAdds, Vec_IntEntry(vAdds, 6*i+3), i );
Vec_IntWriteEntry( vMapAdds, Vec_IntEntry(vAdds, 6*i+4), i );
}
Vec_BitFree( vIsBold );
return vMapAdds;
}
Vec_Int_t * Gia_ShowMapXors( Gia_Man_t * p, Vec_Int_t * vXors )
@ -1105,7 +1112,7 @@ Vec_Int_t * Gia_ShowCollectObjs( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * v
***********************************************************************/
void Gia_ShowProcess( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold, Vec_Int_t * vAdds, Vec_Int_t * vXors, int fFadds )
{
Vec_Int_t * vMapAdds = Gia_ShowMapAdds( p, vAdds, fFadds );
Vec_Int_t * vMapAdds = Gia_ShowMapAdds( p, vAdds, fFadds, vBold );
Vec_Int_t * vMapXors = Gia_ShowMapXors( p, vXors );
Vec_Int_t * vOrder = Gia_ShowCollectObjs( p, vAdds, vXors, vMapAdds, vMapXors );
Gia_WriteDotAig( p, pFileName, vBold, vAdds, vXors, vMapAdds, vMapXors, vOrder );

54
src/base/abci/abc.c
View File

@ -482,6 +482,7 @@ static int Abc_CommandAbc9ATree ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Polyn ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Acec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Anorm ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Decla ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Esop ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Exorcism ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Mfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -1126,6 +1127,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&polyn", Abc_CommandAbc9Polyn, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&acec", Abc_CommandAbc9Acec, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&anorm", Abc_CommandAbc9Anorm, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&decla", Abc_CommandAbc9Decla, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&esop", Abc_CommandAbc9Esop, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&exorcism", Abc_CommandAbc9Exorcism, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mfs", Abc_CommandAbc9Mfs, 0 );
@ -40788,6 +40790,57 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Decla( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
int c, fBooth = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "bvh" ) ) != EOF )
{
switch ( c )
{
case 'b':
fBooth ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Decla(): There is no AIG.\n" );
return 0;
}
pTemp = Acec_ManDecla( pAbc->pGia, fBooth, fVerbose );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &decla [-bvh]\n" );
Abc_Print( -2, "\t removes carry look ahead adders\n" );
Abc_Print( -2, "\t-b : toggles working with Booth multipliers [default = %s]\n", fBooth? "yes": "no" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
@ -42690,7 +42743,6 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// Jf_ManTestCnf( pAbc->pGia );
// Gia_ManCheckFalseTest( pAbc->pGia, nFrames );
// Gia_ParTest( pAbc->pGia, nWords, nProcs );
Acec_MultFindPPsTest( pAbc->pGia );
// printf( "\nThis command is currently disabled.\n\n" );
return 0;

12
src/misc/vec/vecWec.h
View File

@ -561,6 +561,18 @@ static inline void Vec_WecPrint( Vec_Wec_t * p, int fSkipSingles )
printf( " }\n" );
}
}
static inline void Vec_WecPrintLits( Vec_Wec_t * p )
{
Vec_Int_t * vVec;
int i, k, iLit;
Vec_WecForEachLevel( p, vVec, i )
{
printf( " %4d : %2d {", i, Vec_IntSize(vVec) );
Vec_IntForEachEntry( vVec, iLit, k )
printf( " %c%d", Abc_LitIsCompl(iLit) ? '-' : '+', Abc_Lit2Var(iLit) );
printf( " }\n" );
}
}
/**Function*************************************************************

2
src/proof/acec/acec.h
View File

@ -66,6 +66,8 @@ struct Acec_ParCec_t_
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== acecCl.c ========================================================*/
extern Gia_Man_t * Acec_ManDecla( Gia_Man_t * pGia, int fBooth, int fVerbose );
/*=== acecCore.c ========================================================*/
extern void Acec_ManCecSetDefaultParams( Acec_ParCec_t * p );
extern int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars );

88
src/proof/acec/acecCl.c
View File

@ -335,6 +335,94 @@ Gia_Man_t * Acec_DetectAdditional( Gia_Man_t * p, int fVerbose )
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Acec_RewriteTop( Gia_Man_t * p, Acec_Box_t * pBox )
{
Vec_Int_t * vRes = Vec_IntAlloc( Gia_ManCoNum(p) + 1 );
Vec_Int_t * vLevel;
int i, k, iLit;
Vec_WecPrintLits( pBox->vRootLits );
Vec_WecForEachLevel( pBox->vRootLits, vLevel, i )
{
int In[3] = {0}, Out[2];
assert( Vec_IntSize(vLevel) > 0 );
assert( Vec_IntSize(vLevel) <= 3 );
if ( Vec_IntSize(vLevel) == 1 )
{
Vec_IntPush( vRes, Vec_IntEntry(vLevel, 0) );
continue;
}
Vec_IntForEachEntry( vLevel, iLit, k )
In[k] = iLit;
Acec_InsertFadd( p, In, Out );
Vec_IntPush( vRes, Out[0] );
if ( i+1 < Vec_WecSize(pBox->vRootLits) )
Vec_IntPush( Vec_WecEntry(pBox->vRootLits, i+1), Out[1] );
else
Vec_IntPush( Vec_WecPushLevel(pBox->vRootLits), Out[1] );
}
assert( Vec_IntSize(vRes) >= Gia_ManCoNum(p) );
Vec_IntShrink( vRes, Gia_ManCoNum(p) );
return vRes;
}
Gia_Man_t * Acec_RewriteReplace( Gia_Man_t * p, Vec_Int_t * vRes )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj; int i;
assert( Gia_ManCoNum(p) == Vec_IntSize(vRes) );
// create new manager
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManSetPhase( p );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachCo( p, pObj, i )
{
int iLit = Vec_IntEntry( vRes, i );
int Phase1 = Gia_ObjPhase(pObj);
int Phase2 = Abc_LitIsCompl(iLit) ^ Gia_ObjPhase(Gia_ManObj(p, Abc_Lit2Var(iLit)));
int iLitNew = Abc_Var2Lit( Abc_Lit2Var(iLit), Phase1 ^ Phase2 );
pObj->Value = Gia_ManAppendCo( pNew, iLitNew );
}
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
Gia_Man_t * Acec_ManDecla( Gia_Man_t * pGia, int fBooth, int fVerbose )
{
int status = -1;
abctime clk = Abc_Clock();
Gia_Man_t * pNew = NULL;
Vec_Bit_t * vIgnore = fBooth ? Acec_BoothFindPPG(pGia) : NULL;
Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, fVerbose );
Vec_Int_t * vResult;
Vec_BitFreeP( &vIgnore );
if ( pBox == NULL ) // cannot match
{
printf( "Cannot find arithmetic boxes.\n" );
return Gia_ManDup( pGia );
}
vResult = Acec_RewriteTop( pGia, pBox );
pNew = Acec_RewriteReplace( pGia, vResult );
Vec_IntFree( vResult );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

124
src/proof/acec/acecCore.c
View File

@ -30,6 +30,8 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define TRUTH_UNUSED 0x1234567812345678
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -59,6 +61,79 @@ void Acec_ManCecSetDefaultParams( Acec_ParCec_t * p )
p->iOutFail = -1; // the number of failed output
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acec_VerifyClasses( Gia_Man_t * p, Vec_Wec_t * vLits, Vec_Wec_t * vReprs )
{
Vec_Ptr_t * vFunc = Vec_PtrAlloc( Vec_WecSize(vLits) );
Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
Vec_Int_t * vLevel;
int i, j, k, Entry, Entry2, nOvers = 0, nErrors = 0;
Vec_WecForEachLevel( vLits, vLevel, i )
{
Vec_Wrd_t * vTruths = Vec_WrdAlloc( Vec_IntSize(vLevel) );
Vec_IntForEachEntry( vLevel, Entry, k )
{
word Truth = Gia_ObjComputeTruth6Cis( p, Entry, vSupp, vTemp );
if ( Vec_IntSize(vSupp) > 6 )
{
nOvers++;
Vec_WrdPush( vTruths, TRUTH_UNUSED );
continue;
}
vSupp->nSize = Abc_Tt6MinBase( &Truth, vSupp->pArray, vSupp->nSize );
if ( Vec_IntSize(vSupp) > 5 )
{
nOvers++;
Vec_WrdPush( vTruths, TRUTH_UNUSED );
continue;
}
Vec_WrdPush( vTruths, Truth );
}
Vec_PtrPush( vFunc, vTruths );
}
if ( nOvers )
printf( "Detected %d oversize support nodes.\n", nOvers );
Vec_IntFree( vSupp );
Vec_WrdFree( vTemp );
// verify the classes
Vec_WecForEachLevel( vReprs, vLevel, i )
{
Vec_Wrd_t * vTruths = (Vec_Wrd_t *)Vec_PtrEntry( vFunc, i );
Vec_IntForEachEntry( vLevel, Entry, k )
Vec_IntForEachEntryStart( vLevel, Entry2, j, k+1 )
{
word Truth = Vec_WrdEntry( vTruths, k );
word Truth2 = Vec_WrdEntry( vTruths, j );
if ( Entry == Entry2 )
{
nErrors++;
if ( Truth != Truth2 && Truth != TRUTH_UNUSED && Truth2 != TRUTH_UNUSED )
printf( "Rank %d: Lit %d and %d do not pass verification.\n", i, k, j );
}
if ( Entry == Abc_LitNot(Entry2) )
{
nErrors++;
if ( Truth != ~Truth2 && Truth != TRUTH_UNUSED && Truth2 != TRUTH_UNUSED )
printf( "Rank %d: Lit %d and %d do not pass verification.\n", i, k, j );
}
}
}
if ( nErrors )
printf( "Total errors in equivalence classes = %d.\n", nErrors );
Vec_VecFree( (Vec_Vec_t *)vFunc );
}
/**Function*************************************************************
Synopsis []
@ -148,13 +223,15 @@ void Acec_MatchBoxesSort( int * pArray, int nSize, int * pCostLits )
}
void Acec_MatchPrintEquivLits( Gia_Man_t * p, Vec_Wec_t * vLits, int * pCostLits, int fVerbose )
{
Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
Vec_Int_t * vSupp;
Vec_Wrd_t * vTemp;
Vec_Int_t * vLevel;
int i, k, Entry;
printf( "Leaf literals and their classes:\n" );
Vec_WecForEachLevel( vLits, vLevel, i )
{
if ( Vec_IntSize(vLevel) == 0 )
continue;
printf( "Rank %2d : %2d ", i, Vec_IntSize(vLevel) );
Vec_IntForEachEntry( vLevel, Entry, k )
printf( "%s%d(%d) ", Abc_LitIsCompl(Entry) ? "-":"+", Abc_Lit2Var(Entry), Abc_Lit2LitL(pCostLits, Entry) );
@ -162,13 +239,25 @@ void Acec_MatchPrintEquivLits( Gia_Man_t * p, Vec_Wec_t * vLits, int * pCostLits
}
if ( !fVerbose )
return;
vSupp = Vec_IntAlloc( 100 );
vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
Vec_WecForEachLevel( vLits, vLevel, i )
{
if ( i != 20 )
//if ( i != 20 )
// continue;
if ( Vec_IntSize(vLevel) == 0 )
continue;
Vec_IntForEachEntry( vLevel, Entry, k )
{
word Truth = Gia_ObjComputeTruth6Cis( p, Entry, vSupp, vTemp );
/*
{
int iObj = Abc_Lit2Var(Entry);
Gia_Man_t * pGia0 = Gia_ManDupAndCones( p, &iObj, 1, 1 );
Gia_ManShow( pGia0, NULL, 0, 0, 0 );
Gia_ManStop( pGia0 );
}
*/
printf( "Rank = %4d : ", i );
printf( "Obj = %4d ", Abc_Lit2Var(Entry) );
if ( Vec_IntSize(vSupp) > 6 )
@ -218,7 +307,7 @@ int Acec_MatchCountCommon( Vec_Wec_t * vLits1, Vec_Wec_t * vLits2, int Shift )
Vec_IntFree( vRes );
return nCommon;
}
void Acec_MatchCheckShift( Vec_Wec_t * vLits0, Vec_Wec_t * vLits1, Vec_Int_t * vMap0, Vec_Int_t * vMap1, Vec_Wec_t * vRoots0, Vec_Wec_t * vRoots1 )
void Acec_MatchCheckShift( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Vec_Wec_t * vLits0, Vec_Wec_t * vLits1, Vec_Int_t * vMap0, Vec_Int_t * vMap1, Vec_Wec_t * vRoots0, Vec_Wec_t * vRoots1 )
{
Vec_Wec_t * vRes0 = Acec_MatchCopy( vLits0, vMap0 );
Vec_Wec_t * vRes1 = Acec_MatchCopy( vLits1, vMap1 );
@ -229,14 +318,24 @@ void Acec_MatchCheckShift( Vec_Wec_t * vLits0, Vec_Wec_t * vLits1, Vec_Int_t * v
{
Vec_WecInsertLevel( vLits0, 0 );
Vec_WecInsertLevel( vRoots0, 0 );
printf( "Shifted one level up.\n" );
}
else if ( nCommonMinus > nCommonPlus && nCommonMinus > nCommon )
{
Vec_WecInsertLevel( vLits1, 0 );
Vec_WecInsertLevel( vRoots1, 0 );
printf( "Shifted one level down.\n" );
}
Vec_WecPrint( vRes0, 0 );
Vec_WecPrint( vRes1, 0 );
//printf( "Input literals:\n" );
//Vec_WecPrintLits( vLits0 );
printf( "Equiv classes:\n" );
Vec_WecPrintLits( vRes0 );
//printf( "Input literals:\n" );
//Vec_WecPrintLits( vLits1 );
printf( "Equiv classes:\n" );
Vec_WecPrintLits( vRes1 );
//Acec_VerifyClasses( pGia0, vLits0, vRes0 );
//Acec_VerifyClasses( pGia1, vLits1, vRes1 );
Vec_WecFree( vRes0 );
Vec_WecFree( vRes1 );
}
@ -250,10 +349,14 @@ int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
Acec_MatchBoxesSort( Vec_IntArray(vLevel), Vec_IntSize(vLevel), Vec_IntArray(vMap0) );
Vec_WecForEachLevel( pBox1->vLeafLits, vLevel, i )
Acec_MatchBoxesSort( Vec_IntArray(vLevel), Vec_IntSize(vLevel), Vec_IntArray(vMap1) );
Acec_MatchCheckShift( pBox0->vLeafLits, pBox1->vLeafLits, vMap0, vMap1, pBox0->vRootLits, pBox1->vRootLits );
Acec_MatchCheckShift( pBox0->pGia, pBox1->pGia, pBox0->vLeafLits, pBox1->vLeafLits, vMap0, vMap1, pBox0->vRootLits, pBox1->vRootLits );
//Acec_MatchPrintEquivLits( pBox0->pGia, pBox0->vLeafLits, Vec_IntArray(vMap0), 0 );
//Acec_MatchPrintEquivLits( pBox1->pGia, pBox1->vLeafLits, Vec_IntArray(vMap1), 0 );
printf( "Outputs:\n" );
Vec_WecPrintLits( pBox0->vRootLits );
printf( "Outputs:\n" );
Vec_WecPrintLits( pBox1->vRootLits );
// reorder nodes to have the same order
assert( pBox0->vShared == NULL );
@ -350,8 +453,11 @@ int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
printf( "Matching of adder trees in LHS and RHS succeeded. " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// remove the last output
//Gia_ManPatchCoDriver( pGia0n, Gia_ManCoNum(pGia0n)-1, 0 );
//Gia_ManPatchCoDriver( pGia1n, Gia_ManCoNum(pGia1n)-1, 0 );
Gia_ManPatchCoDriver( pGia0n, Gia_ManCoNum(pGia0n)-1, 0 );
Gia_ManPatchCoDriver( pGia1n, Gia_ManCoNum(pGia1n)-1, 0 );
Gia_ManPatchCoDriver( pGia0n, Gia_ManCoNum(pGia0n)-2, 0 );
Gia_ManPatchCoDriver( pGia1n, Gia_ManCoNum(pGia1n)-2, 0 );
}
// solve regular CEC problem
Cec_ManCecSetDefaultParams( pCecPars );

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

@ -71,8 +71,10 @@ extern Vec_Wec_t * Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdd
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 );
/*=== 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 );
/*=== acecTree.c ========================================================*/
extern void Acec_PrintAdders( Vec_Wec_t * vBoxes, Vec_Int_t * vAdds );
extern Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fVerbose );
extern void Acec_BoxFreeP( Acec_Box_t ** ppBox );
/*=== acecUtil.c ========================================================*/

5
src/proof/acec/acecRe.c
View File

@ -450,6 +450,7 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose
Hash_IntManStop( pHash );
Ree_ManRemoveTrivial( p, vAdds );
Ree_ManRemoveContained( p, vAdds );
//Ree_ManPrintAdders( vAdds, 1 );
return vAdds;
}
@ -523,6 +524,10 @@ void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds )
{
pObjX = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*i+3) );
pObjM = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*i+4) );
// rule out if MAJ is a fanout of XOR
//if ( pObjX == Gia_ObjFanin0(pObjM) || pObjX == Gia_ObjFanin1(pObjM) )
// continue;
// rule out if MAJ is a fanin of XOR and has no other fanouts
if ( (pObjM == Gia_ObjFanin0(pObjX) || pObjM == Gia_ObjFanin1(pObjX)) && Gia_ObjRefNum(p, pObjM) == 1 )
continue;
}

138
src/proof/acec/acecTree.c
View File

@ -64,6 +64,30 @@ void Acec_BoxFreeP( Acec_Box_t ** ppBox )
*ppBox = NULL;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acec_VerifyBoxLeaves( Acec_Box_t * pBox, Vec_Bit_t * vIgnore )
{
Vec_Int_t * vLevel;
int i, k, iLit, Count = 0;
if ( vIgnore == NULL )
return;
Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i )
Vec_IntForEachEntry( vLevel, iLit, k )
if ( Gia_ObjIsAnd(Gia_ManObj(pBox->pGia, Abc_Lit2Var(iLit))) && !Vec_BitEntry(vIgnore, Abc_Lit2Var(iLit)) )
printf( "Internal node %d of rank %d is not part of PPG.\n", Abc_Lit2Var(iLit), i ), Count++;
printf( "Detected %d suspicious leaves.\n", Count );
}
/**Function*************************************************************
Synopsis [Filters trees by removing TFO of roots.]
@ -103,6 +127,18 @@ void Acec_TreeFilterOne( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree )
// remove those that overlap with roots
Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
{
/*
if ( Vec_IntEntry(vAdds, 6*Box+3) == 24 && Vec_IntEntry(vAdds, 6*Box+4) == 22 )
{
printf( "**** removing special one \n" );
continue;
}
if ( Vec_IntEntry(vAdds, 6*Box+3) == 48 && Vec_IntEntry(vAdds, 6*Box+4) == 49 )
{
printf( "**** removing special one \n" );
continue;
}
*/
if ( Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+3)) || Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+4)) )
{
printf( "Removing box %d=(%d,%d) of rank %d.\n", Box, Vec_IntEntry(vAdds, 6*Box+3), Vec_IntEntry(vAdds, 6*Box+4), Rank );
@ -123,6 +159,73 @@ void Acec_TreeFilterTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vTrees
Acec_TreeFilterOne( p, vAdds, vLevel );
}
/**Function*************************************************************
Synopsis [Filters trees by removing TFO of roots.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acec_TreeMarkTFI_rec( Gia_Man_t * p, int Id, Vec_Bit_t * vMarked )
{
Gia_Obj_t * pObj = Gia_ManObj(p, Id);
if ( Vec_BitEntry(vMarked, Id) )
return;
Vec_BitWriteEntry( vMarked, Id, 1 );
if ( !Gia_ObjIsAnd(pObj) )
return;
Acec_TreeMarkTFI_rec( p, Gia_ObjFaninId0(pObj, Id), vMarked );
Acec_TreeMarkTFI_rec( p, Gia_ObjFaninId1(pObj, Id), vMarked );
}
void Acec_TreeFilterOne2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree )
{
Vec_Bit_t * vIsLeaf = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Bit_t * vMarked = Vec_BitStart( Gia_ManObjNum(p) ) ;
Gia_Obj_t * pObj;
int i, k = 0, Box, Rank;
// mark leaves
Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
{
Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+0), 1 );
Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+1), 1 );
Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+2), 1 );
}
Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
{
Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+3), 0 );
Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+4), 0 );
}
// mark TFI of leaves
Gia_ManForEachAnd( p, pObj, i )
if ( Vec_BitEntry(vIsLeaf, i) )
Acec_TreeMarkTFI_rec( p, i, vMarked );
// remove those that overlap with the marked TFI
Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
{
if ( Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+3)) || Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+4)) )
{
printf( "Removing box %d=(%d,%d) of rank %d.\n", Box, Vec_IntEntry(vAdds, 6*Box+3), Vec_IntEntry(vAdds, 6*Box+4), Rank );
continue;
}
Vec_IntWriteEntry( vTree, k++, Box );
Vec_IntWriteEntry( vTree, k++, Rank );
}
Vec_IntShrink( vTree, k );
Vec_BitFree( vIsLeaf );
Vec_BitFree( vMarked );
}
void Acec_TreeFilterTrees2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vTrees )
{
Vec_Int_t * vLevel;
int i;
Vec_WecForEachLevel( vTrees, vLevel, i )
Acec_TreeFilterOne2( p, vAdds, vLevel );
}
/**Function*************************************************************
Synopsis []
@ -392,7 +495,7 @@ Vec_Wec_t * Acec_TreeFindTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * vI
Vec_BitFree( vFound );
Vec_IntFree( vMap );
// filter trees
//Acec_TreeFilterTrees( p, vAdds, vTrees );
Acec_TreeFilterTrees( p, vAdds, vTrees );
// sort by size
Vec_WecSort( vTrees, 1 );
return vTrees;
@ -437,20 +540,11 @@ void Acec_PrintAdders( Vec_Wec_t * vBoxes, Vec_Int_t * vAdds )
{
printf( " %4d : %2d {", i, Vec_IntSize(vLevel) );
Vec_IntForEachEntry( vLevel, iBox, k )
{
printf( " %s%d=(%d,%d)", Vec_IntEntry(vAdds, 6*iBox+2) == 0 ? "*":"", iBox,
Vec_IntEntry(vAdds, 6*iBox+3), Vec_IntEntry(vAdds, 6*iBox+4) );
printf( " }\n" );
}
}
void Vec_WecPrintLits( Vec_Wec_t * p )
{
Vec_Int_t * vVec;
int i, k, Entry;
Vec_WecForEachLevel( p, vVec, i )
{
printf( " %4d : %2d {", i, Vec_IntSize(vVec) );
Vec_IntForEachEntry( vVec, Entry, k )
printf( " %c%d", Abc_LitIsCompl(Entry) ? '-' : '+', Abc_Lit2Var(Entry) );
//printf( "(%d,%d,%d)", Vec_IntEntry(vAdds, 6*iBox+0), Vec_IntEntry(vAdds, 6*iBox+1), Vec_IntEntry(vAdds, 6*iBox+2) );
}
printf( " }\n" );
}
}
@ -505,7 +599,10 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree
Vec_WecForEachLevelReverse( pBox->vAdds, vLevel, i )
Vec_IntForEachEntry( vLevel, Box, k )
if ( !Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+4) ) )
{
//printf( "Pushing phase of output %d of box %d\n", Vec_IntEntry(vAdds, 6*Box+4), Box );
Acec_TreePhases_rec( p, vAdds, vMap, Vec_IntEntry(vAdds, 6*Box+4), Vec_IntEntry(vAdds, 6*Box+2) != 0, vVisit );
}
Acec_TreeVerifyPhases( p, vAdds, pBox->vAdds );
Acec_TreeVerifyPhases2( p, vAdds, pBox->vAdds );
Vec_BitFree( vVisit );
@ -521,7 +618,14 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree
Vec_WecPush( pBox->vLeafLits, i, Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), Acec_SignBit2(vAdds, Box, k)) );
for ( k = 3; k < 5; k++ )
if ( !Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+k) ) )
{
//if ( Vec_IntEntry(vAdds, 6*Box+k) == 10942 )
//{
// printf( "++++++++++++ Skipping special\n" );
// continue;
//}
Vec_WecPush( pBox->vRootLits, k == 4 ? i + 1 : i, Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), Acec_SignBit2(vAdds, Box, k)) );
}
if ( Vec_IntEntry(vAdds, 6*Box+2) == 0 && Acec_SignBit2(vAdds, Box, 2) )
Vec_WecPush( pBox->vLeafLits, i, 1 );
}
@ -531,8 +635,9 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree
Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i )
Vec_IntSort( vLevel, 0 );
Vec_WecForEachLevel( pBox->vRootLits, vLevel, i )
Vec_IntSort( vLevel, 0 );
Vec_IntSort( vLevel, 1 );
//return pBox;
/*
// push literals forward
//Vec_WecPrint( pBox->vLeafLits, 0 );
Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i )
@ -555,6 +660,7 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree
}
}
printf( "Pushed forward %d input literals.\n", Count );
*/
//Vec_WecPrint( pBox->vLeafLits, 0 );
return pBox;
}
@ -607,13 +713,17 @@ Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fVerbose )
Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, fVerbose );
Vec_Wec_t * vTrees = Acec_TreeFindTrees( p, vAdds, vIgnore );
if ( vTrees && Vec_WecSize(vTrees) > 0 )
{
pBox = Acec_CreateBox( p, vAdds, Vec_WecEntry(vTrees, 0) );
Acec_VerifyBoxLeaves( pBox, vIgnore );
}
if ( pBox )//&& fVerbose )
printf( "Processing tree %d: Ranks = %d. Adders = %d. Leaves = %d. Roots = %d.\n",
0, Vec_WecSize(pBox->vAdds), Vec_WecSizeSize(pBox->vAdds),
Vec_WecSizeSize(pBox->vLeafLits), Vec_WecSizeSize(pBox->vRootLits) );
if ( pBox && fVerbose )
Acec_PrintBox( pBox, vAdds );
//Acec_PrintAdders( pBox0->vAdds, vAdds );
//Acec_MultDetectInputs( p, pBox->vLeafLits, pBox->vRootLits );
Vec_WecFreeP( &vTrees );
Vec_IntFree( vAdds );

23
src/proof/acec/acecUtil.c
View File

@ -90,6 +90,29 @@ void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose )
Vec_IntFree( vXors );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupTopMostRange( Gia_Man_t * p )
{
Gia_Man_t * pNew;
Vec_Int_t * vTops = Vec_IntAlloc( 10 );
int i;
for ( i = 45; i < 52; i++ )
Vec_IntPush( vTops, Gia_ObjId( p, Gia_ObjFanin0(Gia_ManCo(p, i)) ) );
pNew = Gia_ManDupAndConesLimit( p, Vec_IntArray(vTops), Vec_IntSize(vTops), 100 );
Vec_IntFree( vTops );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////