Skip to content

A
abc
Commit 7457b8a6 by Alan Mishchenko
Options

Updates to arithmetic verification.

parent 153b71c1
Showing with 55 additions and 30 deletions
src/proof/acec/acecCl.c
......@@ -350,9 +350,15 @@ 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 i, k, iStart, iLit, Driver, Count = 0;
// determine how much to shift
Driver = Gia_ObjFaninId0p( p, Gia_ManCo(p, 0) );
Vec_WecForEachLevel( pBox->vRootLits, vLevel, iStart )
if ( Abc_Lit2Var(Vec_IntEntry(vLevel,0)) == Driver )
break;
assert( iStart < Gia_ManCoNum(p) );
//Vec_WecPrintLits( pBox->vRootLits );
Vec_WecForEachLevelStart( pBox->vRootLits, vLevel, i, iStart )
{
int In[3] = {0}, Out[2];
assert( Vec_IntSize(vLevel) > 0 );
......@@ -370,9 +376,11 @@ Vec_Int_t * Acec_RewriteTop( Gia_Man_t * p, Acec_Box_t * pBox )
Vec_IntPush( Vec_WecEntry(pBox->vRootLits, i+1), Out[1] );
else
Vec_IntPush( Vec_WecPushLevel(pBox->vRootLits), Out[1] );
Count++;
}
assert( Vec_IntSize(vRes) >= Gia_ManCoNum(p) );
Vec_IntShrink( vRes, Gia_ManCoNum(p) );
printf( "Added %d adders for replace CLAs. ", Count );
return vRes;
}
Gia_Man_t * Acec_RewriteReplace( Gia_Man_t * p, Vec_Int_t * vRes )
......@@ -384,7 +392,6 @@ Gia_Man_t * Acec_RewriteReplace( Gia_Man_t * p, Vec_Int_t * vRes )
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 )
......@@ -394,22 +401,26 @@ Gia_Man_t * Acec_RewriteReplace( Gia_Man_t * p, Vec_Int_t * vRes )
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 );
Gia_Obj_t * pRepr = Gia_ManObj( p, Abc_Lit2Var(iLit) );
pObj->Value = Gia_ManAppendCo( pNew, pRepr->Value );
}
// set correct phase
Gia_ManSetPhase( p );
Gia_ManSetPhase( pNew );
Gia_ManForEachCo( pNew, pObj, i )
if ( Gia_ObjPhase(pObj) != Gia_ObjPhase(Gia_ManCo(p, i)) )
Gia_ObjFlipFaninC0( pObj );
// remove dangling nodes
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 );
Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, 0, 0, fVerbose );
Vec_Int_t * vResult;
Vec_BitFreeP( &vIgnore );
if ( pBox == NULL ) // cannot match
......@@ -418,8 +429,10 @@ Gia_Man_t * Acec_ManDecla( Gia_Man_t * pGia, int fBooth, int fVerbose )
return Gia_ManDup( pGia );
}
vResult = Acec_RewriteTop( pGia, pBox );
Acec_BoxFreeP( &pBox );
pNew = Acec_RewriteReplace( pGia, vResult );
Vec_IntFree( vResult );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return pNew;
}
......
src/proof/acec/acecCore.c
......@@ -328,12 +328,12 @@ void Acec_MatchCheckShift( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Vec_Wec_t * vLi
}
//printf( "Input literals:\n" );
//Vec_WecPrintLits( vLits0 );
printf( "Equiv classes:\n" );
Vec_WecPrintLits( vRes0 );
//printf( "Equiv classes:\n" );
//Vec_WecPrintLits( vRes0 );
//printf( "Input literals:\n" );
//Vec_WecPrintLits( vLits1 );
printf( "Equiv classes:\n" );
Vec_WecPrintLits( vRes1 );
//printf( "Equiv classes:\n" );
//Vec_WecPrintLits( vRes1 );
//Acec_VerifyClasses( pGia0, vLits0, vRes0 );
//Acec_VerifyClasses( pGia1, vLits1, vRes1 );
Vec_WecFree( vRes0 );
......@@ -353,10 +353,10 @@ int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
//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 );
//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 );
......@@ -438,8 +438,8 @@ int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
Cec_ParCec_t ParsCec, * pCecPars = &ParsCec;
Vec_Bit_t * vIgnore0 = pPars->fBooth ? Acec_BoothFindPPG(pGia0) : NULL;
Vec_Bit_t * vIgnore1 = pPars->fBooth ? Acec_BoothFindPPG(pGia1) : NULL;
Acec_Box_t * pBox0 = Acec_DeriveBox( pGia0, vIgnore0, pPars->fVerbose );
Acec_Box_t * pBox1 = Acec_DeriveBox( pGia1, vIgnore1, pPars->fVerbose );
Acec_Box_t * pBox0 = Acec_DeriveBox( pGia0, vIgnore0, 0, 0, pPars->fVerbose );
Acec_Box_t * pBox1 = Acec_DeriveBox( pGia1, vIgnore1, 0, 0, pPars->fVerbose );
Vec_BitFreeP( &vIgnore0 );
Vec_BitFreeP( &vIgnore1 );
if ( pBox0 == NULL || pBox1 == NULL ) // cannot match
......
src/proof/acec/acecInt.h
......@@ -75,7 +75,7 @@ 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 Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fFilterIn, int fFilterOut, int fVerbose );
extern void Acec_BoxFreeP( Acec_Box_t ** ppBox );
/*=== acecUtil.c ========================================================*/
extern void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose );
......
src/proof/acec/acecNorm.c
......@@ -201,7 +201,7 @@ Gia_Man_t * Acec_InsertBox( Acec_Box_t * pBox, int fAll )
Gia_Man_t * Acec_Normalize( Gia_Man_t * pGia, int fBooth, int fVerbose )
{
Vec_Bit_t * vIgnore = fBooth ? Acec_BoothFindPPG( pGia ) : NULL;
Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, fVerbose );
Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, 0, 0, fVerbose );
Gia_Man_t * pNew = Acec_InsertBox( pBox, 1 );
Acec_BoxFreeP( &pBox );
Vec_BitFreeP( &vIgnore );
......
src/proof/acec/acecTree.c
......@@ -127,6 +127,10 @@ 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 )
{
// special case of the first bit
// if ( i == 0 )
// continue;
/*
if ( Vec_IntEntry(vAdds, 6*Box+3) == 24 && Vec_IntEntry(vAdds, 6*Box+4) == 22 )
{
......@@ -415,7 +419,7 @@ Vec_Int_t * Acec_TreeFindPoints( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * v
int i;
for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
{
if ( vIgnore && (Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+3)) || Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+4))) )
if ( vIgnore && (Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+3)) && Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+4))) )
continue;
Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+0), i, 0 );
Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+1), i, 0 );
......@@ -468,7 +472,7 @@ void Acec_TreeFindTrees_rec( Vec_Int_t * vAdds, Vec_Int_t * vMap, int iObj, int
Acec_TreeFindTrees2_rec( vAdds, vMap, In, Acec_TreeWhichPoint(vAdds, In, iObj) == 4 ? Rank-1 : Rank, vTree, vFound );
Acec_TreeFindTrees2_rec( vAdds, vMap, Out, Rank, vTree, vFound );
}
Vec_Wec_t * Acec_TreeFindTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * vIgnore )
Vec_Wec_t * Acec_TreeFindTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * vIgnore, int fFilterIn, int fFilterOut )
{
Vec_Wec_t * vTrees = Vec_WecAlloc( 10 );
Vec_Int_t * vMap = Acec_TreeFindPoints( p, vAdds, vIgnore );
......@@ -495,7 +499,10 @@ 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 );
if ( fFilterIn )
Acec_TreeFilterTrees2( p, vAdds, vTrees );
else if ( fFilterOut )
Acec_TreeFilterTrees( p, vAdds, vTrees );
// sort by size
Vec_WecSort( vTrees, 1 );
return vTrees;
......@@ -511,7 +518,7 @@ void Acec_TreeFindTreesTest( Gia_Man_t * p )
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
clk = Abc_Clock();
vTrees = Acec_TreeFindTrees( p, vAdds, NULL );
vTrees = Acec_TreeFindTrees( p, vAdds, NULL, 0, 0 );
printf( "Collected %d trees with %d adders in them. ", Vec_WecSize(vTrees), Vec_WecSizeSize(vTrees)/2 );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Vec_WecPrint( vTrees, 0 );
......@@ -572,7 +579,7 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree
Vec_Bit_t * vIsLeaf = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(p) );
Vec_Int_t * vLevel, * vMap;
int i, j, k, Box, Rank, Count = 0;
int i, j, k, Box, Rank;//, Count = 0;
Acec_Box_t * pBox = ABC_CALLOC( Acec_Box_t, 1 );
pBox->pGia = p;
......@@ -583,6 +590,11 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree
// collect boxes; mark inputs/outputs
Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
{
// if ( 37 == Box && 6 == Rank )
// {
// printf( "Skipping one adder...\n" );
// continue;
// }
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 );
......@@ -677,7 +689,7 @@ void Acec_CreateBoxTest( Gia_Man_t * p )
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
clk = Abc_Clock();
vTrees = Acec_TreeFindTrees( p, vAdds, NULL );
vTrees = Acec_TreeFindTrees( p, vAdds, NULL, 0, 0 );
printf( "Collected %d trees with %d adders in them. ", Vec_WecSize(vTrees), Vec_WecSizeSize(vTrees)/2 );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
//Vec_WecPrint( vTrees, 0 );
......@@ -707,11 +719,11 @@ void Acec_CreateBoxTest( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fVerbose )
Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fFilterIn, int fFilterOut, int fVerbose )
{
Acec_Box_t * pBox = NULL;
Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, fVerbose );
Vec_Wec_t * vTrees = Acec_TreeFindTrees( p, vAdds, vIgnore );
Vec_Wec_t * vTrees = Acec_TreeFindTrees( p, vAdds, vIgnore, fFilterIn, fFilterOut );
if ( vTrees && Vec_WecSize(vTrees) > 0 )
{
pBox = Acec_CreateBox( p, vAdds, Vec_WecEntry(vTrees, 0) );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment