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 2016-08-05 11:08:12 -07:00
parent af20a8177b
commit 2792979594
6 changed files with 323 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -114,11 +114,12 @@ int Gia_WriteDotAigLevel( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds,
return Level;
}
*/
int Gia_WriteDotAigLevel( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds, Vec_Int_t * vRecord, Vec_Int_t ** pvLevel, Vec_Int_t ** pvMarks, Vec_Int_t ** pvRemap )
int Gia_WriteDotAigLevel( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds, Vec_Int_t * vRecord, Vec_Int_t ** pvLevel, Vec_Int_t ** pvMarks, Vec_Int_t ** pvRemap, Vec_Int_t ** pvRemap2 )
{
Vec_Int_t * vLevel = Vec_IntStart( Gia_ManObjNum(p) );
Vec_Int_t * vMarks = Vec_IntStart( Gia_ManObjNum(p) );
Vec_Int_t * vRemap = Vec_IntStartNatural( Gia_ManObjNum(p) );
Vec_Int_t * vRemap2 = Vec_IntStartNatural( Gia_ManObjNum(p) );
int i, k, Id, Entry, LevelMax = 0;
Vec_IntWriteEntry( vMarks, 0, -1 );
@ -141,6 +142,7 @@ int Gia_WriteDotAigLevel( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds,
Vec_IntWriteEntry( vLevel, pFanins[4], Level+1 );
Vec_IntWriteEntry( vMarks, pFanins[4], Entry );
Vec_IntWriteEntry( vRemap, pFanins[3], pFanins[4] );
Vec_IntWriteEntry( vRemap2, pFanins[4], pFanins[3] );
//printf( "Making FA output %d.\n", pFanins[4] );
}
else if ( Attr == 1 )
@ -154,7 +156,8 @@ int Gia_WriteDotAigLevel( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds,
Vec_IntWriteEntry( vLevel, pFanins[1], Level+1 );
Vec_IntWriteEntry( vMarks, pFanins[1], Entry );
Vec_IntWriteEntry( vRemap, pFanins[0], pFanins[1] );
//printf( "Making HA output %d.\n", pFanins[1] );
Vec_IntWriteEntry( vRemap2, pFanins[1], pFanins[0] );
//printf( "Making HA output %d %d.\n", pFanins[0], pFanins[1] );
}
else // if ( Attr == 3 || Attr == 0 )
{
@ -171,6 +174,7 @@ int Gia_WriteDotAigLevel( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds,
*pvLevel = vLevel;
*pvMarks = vMarks;
*pvRemap = vRemap;
*pvRemap2 = vRemap2;
return LevelMax;
}
@ -188,7 +192,7 @@ int Gia_WriteDotAigLevel( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds,
***********************************************************************/
void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int fAdders )
{
Vec_Int_t * vFadds = NULL, * vHadds = NULL, * vRecord = NULL, * vMarks = NULL, * vRemap = NULL;
Vec_Int_t * vFadds = NULL, * vHadds = NULL, * vRecord = NULL, * vMarks = NULL, * vRemap = NULL, * vRemap2 = NULL;
FILE * pFile;
Gia_Obj_t * pNode;//, * pTemp, * pPrev;
int LevelMax, Prev, Level, i;
@ -218,10 +222,10 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int
if ( fAdders )
{
Vec_IntFreeP( &pMan->vLevels );
vFadds = Gia_ManDetectFullAdders( pMan, 0 );
vFadds = Gia_ManDetectFullAdders( pMan, 0, NULL );
vHadds = Gia_ManDetectHalfAdders( pMan, 0 );
vRecord = Gia_PolynFindOrder( pMan, vFadds, vHadds, 0, 0 );
LevelMax = 1 + Gia_WriteDotAigLevel( pMan, vFadds, vHadds, vRecord, &pMan->vLevels, &vMarks, &vRemap );
LevelMax = 1 + Gia_WriteDotAigLevel( pMan, vFadds, vHadds, vRecord, &pMan->vLevels, &vMarks, &vRemap, &vRemap2 );
}
else
LevelMax = 1 + Gia_ManLevelNum( pMan );
@ -364,7 +368,7 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int
*/
if ( vMarks && Vec_IntEntry(vMarks, i) > 0 )
{
fprintf( pFile, " Node%d [label = \"%d_%d\"", i, Vec_IntFind(vRemap, i), i );
fprintf( pFile, " Node%d [label = \"%d_%d\"", i, Vec_IntEntry(vRemap2, i), i );
if ( Abc_Lit2Att2(Vec_IntEntry(vMarks, i)) == 2 )
fprintf( pFile, ", shape = doubleoctagon" );
else

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

@ -53,7 +53,7 @@ ABC_NAMESPACE_HEADER_START
/*=== acecCore.c ========================================================*/
extern int Gia_PolynCec( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Cec_ParCec_t * pPars );
/*=== acecFadds.c ========================================================*/
extern Vec_Int_t * Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose );
extern Vec_Int_t * Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose, Vec_Int_t ** vCutsXor2 );
extern Vec_Int_t * Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose );
/*=== acecOrder.c ========================================================*/
extern Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose, int fVeryVerbose );

263
src/proof/acec/acecCover.c Normal file
View File

@ -0,0 +1,263 @@
/**CFile****************************************************************
FileName [acecCover.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: acecCover.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "acecInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_AcecMark_rec( Gia_Man_t * p, int iObj, int fFirst )
{
Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
if ( pObj->fMark0 && !fFirst )
return;
assert( Gia_ObjIsAnd(pObj) );
pObj->fMark1 = 1;
Gia_AcecMark_rec( p, Gia_ObjFaninId0(pObj, iObj), 0 );
Gia_AcecMark_rec( p, Gia_ObjFaninId1(pObj, iObj), 0 );
}
void Gia_AcecMarkFadd( Gia_Man_t * p, int * pSigs )
{
// if ( Gia_ManObj(p, pSigs[3])->fMark1 || Gia_ManObj(p, pSigs[4])->fMark1 )
// return;
Gia_ManObj( p, pSigs[0] )->fMark0 = 1;
Gia_ManObj( p, pSigs[1] )->fMark0 = 1;
Gia_ManObj( p, pSigs[2] )->fMark0 = 1;
// assert( !Gia_ManObj(p, pSigs[3])->fMark1 );
// assert( !Gia_ManObj(p, pSigs[4])->fMark1 );
Gia_AcecMark_rec( p, pSigs[3], 1 );
Gia_AcecMark_rec( p, pSigs[4], 1 );
}
void Gia_AcecMarkHadd( Gia_Man_t * p, int * pSigs )
{
Gia_Obj_t * pObj = Gia_ManObj( p, pSigs[0] );
int iFan0 = Gia_ObjFaninId0( pObj, pSigs[0] );
int iFan1 = Gia_ObjFaninId1( pObj, pSigs[0] );
Gia_ManObj( p, iFan0 )->fMark0 = 1;
Gia_ManObj( p, iFan1 )->fMark0 = 1;
Gia_AcecMark_rec( p, pSigs[0], 1 );
Gia_AcecMark_rec( p, pSigs[1], 1 );
}
/**Function*************************************************************
Synopsis [Collect XORs reachable from the last output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_AcecCollectXors_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Bit_t * vMap, Vec_Int_t * vXors )
{
if ( !Gia_ObjIsXor(pObj) )//|| Vec_BitEntry(vMap, Gia_ObjId(p, pObj)) )
return;
Vec_IntPush( vXors, Gia_ObjId(p, pObj) );
Gia_AcecCollectXors_rec( p, Gia_ObjFanin0(pObj), vMap, vXors );
Gia_AcecCollectXors_rec( p, Gia_ObjFanin1(pObj), vMap, vXors );
}
Vec_Int_t * Gia_AcecCollectXors( Gia_Man_t * p, Vec_Bit_t * vMap )
{
Vec_Int_t * vXors = Vec_IntAlloc( 100 );
Gia_Obj_t * pObj = Gia_ObjFanin0( Gia_ManCo(p, Gia_ManCoNum(p)-1) );
Gia_AcecCollectXors_rec( p, pObj, vMap, vXors );
return vXors;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_AcecExplore( Gia_Man_t * p, int fVerbose )
{
Vec_Int_t * vNodes = Vec_IntAlloc( 100 );
Vec_Int_t * vFadds, * vHadds, * vXors;
Vec_Bit_t * vMap = Vec_BitStart( Gia_ManObjNum(p) );
Gia_Obj_t * pObj;
int i, nSupp, nCone, nHadds = 0;
assert( p->pMuxes != NULL );
vFadds = Gia_ManDetectFullAdders( p, fVerbose, NULL );
vHadds = Gia_ManDetectHalfAdders( p, fVerbose );
pObj = Gia_ManObj( p, 352 );
printf( "Xor = %d.\n", Gia_ObjIsXor(pObj) );
printf( "Fanin0 = %d. Fanin1 = %d.\n", Gia_ObjFaninId0(pObj, 352), Gia_ObjFaninId1(pObj, 352) );
printf( "Fan00 = %d. Fan01 = %d. Fan10 = %d. Fan11 = %d.\n",
Gia_ObjFaninId0(Gia_ObjFanin0(pObj), Gia_ObjFaninId0(pObj, 352)),
Gia_ObjFaninId1(Gia_ObjFanin0(pObj), Gia_ObjFaninId0(pObj, 352)),
Gia_ObjFaninId0(Gia_ObjFanin1(pObj), Gia_ObjFaninId1(pObj, 352)),
Gia_ObjFaninId1(Gia_ObjFanin1(pObj), Gia_ObjFaninId1(pObj, 352)) );
// create a map of all HADD/FADD outputs
for ( i = 0; i < Vec_IntSize(vHadds)/2; i++ )
{
int * pSigs = Vec_IntEntryP(vHadds, 2*i);
Vec_BitWriteEntry( vMap, pSigs[0], 1 );
Vec_BitWriteEntry( vMap, pSigs[1], 1 );
}
for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ )
{
int * pSigs = Vec_IntEntryP(vFadds, 5*i);
Vec_BitWriteEntry( vMap, pSigs[3], 1 );
Vec_BitWriteEntry( vMap, pSigs[4], 1 );
}
Gia_ManCleanMark01( p );
// mark outputs
Gia_ManForEachCo( p, pObj, i )
Gia_ObjFanin0(pObj)->fMark0 = 1;
// collect XORs
vXors = Gia_AcecCollectXors( p, vMap );
Vec_BitFree( vMap );
printf( "Collected XORs: " );
Vec_IntPrint( vXors );
// mark their fanins
Gia_ManForEachObjVec( vXors, p, pObj, i )
{
pObj->fMark1 = 1;
Gia_ObjFanin0(pObj)->fMark0 = 1;
Gia_ObjFanin1(pObj)->fMark0 = 1;
}
// mark FADDs
for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ )
Gia_AcecMarkFadd( p, Vec_IntEntryP(vFadds, 5*i) );
// iterate through HADDs and find those that fit in
while ( 1 )
{
int fChange = 0;
for ( i = 0; i < Vec_IntSize(vHadds)/2; i++ )
{
int * pSigs = Vec_IntEntryP(vHadds, 2*i);
if ( !Gia_ManObj(p, pSigs[0])->fMark0 || !Gia_ManObj(p, pSigs[1])->fMark0 )
continue;
if ( Gia_ManObj(p, pSigs[0])->fMark1 || Gia_ManObj(p, pSigs[1])->fMark1 )
continue;
Gia_AcecMarkHadd( p, pSigs );
fChange = 1;
nHadds++;
}
if ( !fChange )
break;
}
// print inputs to the adder network
Gia_ManForEachAnd( p, pObj, i )
if ( pObj->fMark0 && !pObj->fMark1 )
{
nSupp = Gia_ManSuppSize( p, &i, 1 );
nCone = Gia_ManConeSize( p, &i, 1 );
printf( "Node %5d : Supp = %5d. Cone = %5d.\n", i, nSupp, nCone );
Vec_IntPush( vNodes, i );
}
printf( "Fadds = %d. Hadds = %d. Root nodes found = %d.\n", Vec_IntSize(vFadds)/5, nHadds, Vec_IntSize(vNodes) );
Gia_ManCleanMark01( p );
Gia_ManForEachObjVec( vNodes, p, pObj, i )
pObj->fMark0 = 1;
Vec_IntFree( vFadds );
Vec_IntFree( vHadds );
Vec_IntFree( vNodes );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_AcecCover( Gia_Man_t * p )
{
int fVerbose = 1;
int i, k, Entry;
Gia_Obj_t * pObj;
Vec_Int_t * vCutsXor2 = NULL;
Vec_Int_t * vFadds = Gia_ManDetectFullAdders( p, fVerbose, &vCutsXor2 );
// mark FADDs
Gia_ManCleanMark01( p );
for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ )
Gia_AcecMarkFadd( p, Vec_IntEntryP(vFadds, 5*i) );
k = 0;
Vec_IntForEachEntry( vCutsXor2, Entry, i )
{
if ( i % 3 != 2 )
continue;
pObj = Gia_ManObj( p, Entry );
if ( pObj->fMark1 )
continue;
printf( "%d ", Entry );
}
printf( "\n" );
Gia_ManCleanMark01( p );
Vec_IntFree( vFadds );
Vec_IntFree( vCutsXor2 );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

54
src/proof/acec/acecFadds.c
View File

@ -59,6 +59,7 @@ Vec_Int_t * Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose )
{
if ( !Gia_ObjIsXor(pObj) )
continue;
Count = 0;
iFan0 = Gia_ObjFaninId0(pObj, i);
iFan1 = Gia_ObjFaninId1(pObj, i);
if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 0), Abc_Var2Lit(iFan1, 0))) )
@ -69,6 +70,7 @@ Vec_Int_t * Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose )
Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++;
if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 1), Abc_Var2Lit(iFan1, 0))) )
Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++;
Counts[Count]++;
}
}
else
@ -116,7 +118,10 @@ Vec_Int_t * Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose )
printf( "\n" );
Vec_IntForEachEntryDouble( vHadds, iXor, iAnd, i )
printf( "%3d : %5d %5d\n", i, iXor, iAnd );
{
pObj = Gia_ManObj( p, iXor );
printf( "%3d : %5d %5d -> %5d %5d\n", i, Gia_ObjFaninId0(pObj, iXor), Gia_ObjFaninId1(pObj, iXor), iXor, iAnd );
}
}
return vHadds;
}
@ -255,6 +260,8 @@ int Dtc_ObjComputeTruth( Gia_Man_t * p, int iObj, int * pCut, int * pTruth )
Dtc_ObjCleanTruth_rec( Gia_ManObj(p, iObj) );
if ( pTruth )
*pTruth = Truth;
if ( Truth == 0x66 || Truth == 0x99 )
return 3;
if ( Truth == 0x96 || Truth == 0x69 )
return 1;
if ( Truth == 0xE8 || Truth == 0xD4 || Truth == 0xB2 || Truth == 0x71 ||
@ -262,11 +269,13 @@ int Dtc_ObjComputeTruth( Gia_Man_t * p, int iObj, int * pCut, int * pTruth )
return 2;
return 0;
}
void Dtc_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_Int_t * vCuts, Vec_Int_t * vCutsXor, Vec_Int_t * vCutsMaj )
void Dtc_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_Int_t * vCuts, Vec_Int_t * vCutsXor2, Vec_Int_t * vCutsXor, Vec_Int_t * vCutsMaj )
{
int fVerbose = 0;
Vec_Int_t * vTemp;
int i, k, c, Type, * pCut0, * pCut1, pCut[4];
if ( fVerbose )
printf( "Object %d = :\n", iObj );
Vec_IntFill( vCuts, 2, 1 );
Vec_IntPush( vCuts, iObj );
Dtc_ForEachCut( pList0, pCut0, i )
@ -277,8 +286,28 @@ void Dtc_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I
if ( Dtc_ManCutCheckEqual(vCuts, pCut) )
continue;
Vec_IntAddToEntry( vCuts, 0, 1 );
if ( fVerbose )
printf( "%d : ", pCut[0] );
for ( c = 0; c <= pCut[0]; c++ )
{
Vec_IntPush( vCuts, pCut[c] );
if ( fVerbose && c )
printf( "%d ", pCut[c] );
}
if ( fVerbose )
printf( "\n" );
if ( pCut[0] == 2 )
{
int Value = Dtc_ObjComputeTruth( p, iObj, pCut, NULL );
assert( Value == 3 || Value == 0 );
if ( Value == 3 )
{
Vec_IntPush( vCutsXor2, pCut[1] );
Vec_IntPush( vCutsXor2, pCut[2] );
Vec_IntPush( vCutsXor2, iObj );
}
continue;
}
if ( pCut[0] != 3 )
continue;
Type = Dtc_ObjComputeTruth( p, iObj, pCut, NULL );
@ -298,11 +327,12 @@ void Dtc_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I
Vec_IntPush( vTemp, iObj );
}
}
void Dtc_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvCutsXor, Vec_Int_t ** pvCutsMaj, int fVerbose )
void Dtc_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvCutsXor2, Vec_Int_t ** pvCutsXor, Vec_Int_t ** pvCutsMaj, int fVerbose )
{
Gia_Obj_t * pObj;
int * pList0, * pList1, i, nCuts = 0;
Vec_Int_t * vTemp = Vec_IntAlloc( 1000 );
Vec_Int_t * vCutsXor2 = Vec_IntAlloc( Gia_ManAndNum(p) );
Vec_Int_t * vCutsXor = Vec_IntAlloc( Gia_ManAndNum(p) );
Vec_Int_t * vCutsMaj = Vec_IntAlloc( Gia_ManAndNum(p) );
Vec_Int_t * vCuts = Vec_IntAlloc( 30 * Gia_ManAndNum(p) );
@ -319,7 +349,7 @@ void Dtc_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvCutsXor, Vec_Int_t ** pvC
{
pList0 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId0(pObj, i)) );
pList1 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId1(pObj, i)) );
Dtc_ManCutMerge( p, i, pList0, pList1, vTemp, vCutsXor, vCutsMaj );
Dtc_ManCutMerge( p, i, pList0, pList1, vTemp, vCutsXor2, vCutsXor, vCutsMaj );
Vec_IntWriteEntry( vCuts, i, Vec_IntSize(vCuts) );
Vec_IntAppend( vCuts, vTemp );
nCuts += Vec_IntEntry( vTemp, 0 );
@ -329,6 +359,10 @@ void Dtc_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvCutsXor, Vec_Int_t ** pvC
Gia_ManAndNum(p), nCuts, 1.0*nCuts/Gia_ManAndNum(p), 1.0*Vec_IntSize(vCuts)/Gia_ManAndNum(p) );
Vec_IntFree( vTemp );
Vec_IntFree( vCuts );
if ( pvCutsXor2 )
*pvCutsXor2 = vCutsXor2;
else
Vec_IntFree( vCutsXor2 );
*pvCutsXor = vCutsXor;
*pvCutsMaj = vCutsMaj;
}
@ -375,6 +409,12 @@ void Dtc_ManPrintFadds( Vec_Int_t * vFadds )
printf( "%6d ", Vec_IntEntry(vFadds, 5*i+3) );
printf( "%6d ", Vec_IntEntry(vFadds, 5*i+4) );
printf( "\n" );
if ( i == 100 )
{
printf( "Skipping other FADDs.\n" );
break;
}
}
}
int Dtc_ManCompare( int * pCut0, int * pCut1 )
@ -394,10 +434,10 @@ int Dtc_ManCompare2( int * pCut0, int * pCut1 )
return 0;
}
// returns array of 5-tuples containing inputs/sum/cout of each full adder
Vec_Int_t * Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose )
Vec_Int_t * Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose, Vec_Int_t ** pvCutsXor2 )
{
Vec_Int_t * vCutsXor, * vCutsMaj, * vFadds;
Dtc_ManComputeCuts( p, &vCutsXor, &vCutsMaj, fVerbose );
Dtc_ManComputeCuts( p, pvCutsXor2, &vCutsXor, &vCutsMaj, fVerbose );
qsort( Vec_IntArray(vCutsXor), Vec_IntSize(vCutsXor)/4, 16, (int (*)(const void *, const void *))Dtc_ManCompare );
qsort( Vec_IntArray(vCutsMaj), Vec_IntSize(vCutsMaj)/4, 16, (int (*)(const void *, const void *))Dtc_ManCompare );
vFadds = Dtc_ManFindCommonCuts( p, vCutsXor, vCutsMaj );
@ -762,7 +802,7 @@ Gia_Man_t * Gia_ManDupWithNaturalBoxes( Gia_Man_t * p, int nFaddMin, int fVerbos
assert( Gia_ManBoxNum(p) == 0 );
// detect FADDs
vFadds = Gia_ManDetectFullAdders( p, fVerbose );
vFadds = Gia_ManDetectFullAdders( p, fVerbose, NULL );
assert( Vec_IntSize(vFadds) % 5 == 0 );
// map MAJ into its FADD
vMap = Gia_ManCreateMap( p, vFadds );

2
src/proof/acec/acecOrder.c
View File

@ -198,7 +198,7 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t
***********************************************************************/
Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose, int fVeryVerbose )
{
Vec_Int_t * vFadds = Gia_ManDetectFullAdders( pGia, fVeryVerbose );
Vec_Int_t * vFadds = Gia_ManDetectFullAdders( pGia, fVeryVerbose, NULL );
Vec_Int_t * vHadds = Gia_ManDetectHalfAdders( pGia, fVeryVerbose );
Vec_Int_t * vRecord = Gia_PolynFindOrder( pGia, vFadds, vHadds, fVerbose, fVeryVerbose );
Vec_Int_t * vOrder = Vec_IntAlloc( Gia_ManAndNum(pGia) );

1
src/proof/acec/module.make
View File

@ -1,4 +1,5 @@
SRC += src/proof/acec/acecCore.c \
src/proof/acec/acecCover.c \
src/proof/acec/acecFadds.c \
src/proof/acec/acecOrder.c \
src/proof/acec/acecPolyn.c \