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

Version abc70624

This commit is contained in:
Alan Mishchenko 2007-06-24 08:01:00 -07:00
parent d47752011d
commit d6804597a3
17 changed files with 6383 additions and 144 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
abc.dsp
View File

@ -822,6 +822,10 @@ SOURCE=.\src\aig\dar\darCheck.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\dar\darCnf.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\dar\darCore.c
# End Source File
# Begin Source File
@ -834,6 +838,10 @@ SOURCE=.\src\aig\dar\darData.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\dar\darData2.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\dar\darDfs.c
# End Source File
# Begin Source File
@ -866,6 +874,10 @@ SOURCE=.\src\aig\dar\darTable.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\dar\darTruth.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\dar\darUtil.c
# End Source File
# End Group

73
src/aig/dar/dar.h
View File

@ -49,12 +49,13 @@ typedef struct Dar_Par_t_ Dar_Par_t;
typedef struct Dar_Man_t_ Dar_Man_t;
typedef struct Dar_Obj_t_ Dar_Obj_t;
typedef struct Dar_Cut_t_ Dar_Cut_t;
typedef struct Dar_Cnf_t_ Dar_Cnf_t;
typedef struct Dar_MmFixed_t_ Dar_MmFixed_t;
typedef struct Dar_MmFlex_t_ Dar_MmFlex_t;
typedef struct Dar_MmStep_t_ Dar_MmStep_t;
// the maximum number of cuts stored at a node
#define DAR_CUT_BASE 32
#define DAR_CUT_BASE 64
// object types
typedef enum {
@ -82,11 +83,14 @@ struct Dar_Par_t_
struct Dar_Cut_t_ // 8 words
{
unsigned uSign;
unsigned uTruth : 16;
unsigned nLeaves : 3;
int pLeaves[4];
unsigned char pIndices[4];
float aFlow;
unsigned uTruth : 16; // the truth table of the cut function
unsigned Cost : 6; // the cost of the cut in terms of CNF clauses
unsigned FanRefs : 4; // the average number of fanin references
unsigned NoRefs : 3; // the average number of fanin references
unsigned nLeaves : 3; // the number of leaves
int pLeaves[4]; // the array of leaves
// unsigned char pIndices[4];
float Area; // the area flow or exact area of the cut
};
// the AIG node
@ -130,31 +134,59 @@ struct Dar_Man_t_
Dar_Cut_t BaseCuts[DAR_CUT_BASE];
int nBaseCuts;
int nCutsUsed;
int nCutsFiltered;
// current rewriting step
int nNodesInit; // the original number of nodes
Vec_Ptr_t * vLeavesBest; // the best set of leaves
int OutBest; // the best output (in the library)
int GainBest; // the best gain
int LevelBest; // the level of node with the best gain
int ClassBest; // the equivalence class of the best replacement
int nTotalSubgs; // the total number of subgraphs tried
int ClassTimes[222];// the runtimes for each class
int ClassGains[222];// the gains for each class
int ClassSubgs[222];// the graphs for each class
// various data members
Dar_MmFixed_t * pMemObjs; // memory manager for objects
Dar_MmFlex_t * pMemCuts; // memory manager for cuts
Vec_Int_t * vRequired; // the required times
int nLevelMax; // maximum number of levels
void * pData; // the temporary data
int nTravIds; // the current traversal ID
int fCatchExor; // enables EXOR nodes
// CNF mapping
char * pSopSizes; // sizes of SOPs for 4-variable functions
char ** pSops; // the SOPs for 4-variable functions
int aArea; // the area of the mapping
// rewriting statistics
int nCutsBad;
int nCutsGood;
// timing statistics
int timeCuts;
int timeEval;
int timeOther;
int timeTotal;
int time1;
int time2;
};
// the CNF asserting outputs of AIG to be 1
struct Dar_Cnf_t_
{
Dar_Man_t * pMan; // the AIG manager, for which CNF is computed
int nLiterals; // the number of CNF literals
int nClauses; // the number of CNF clauses
int ** pClauses; // the CNF clauses
int * pVarNums; // the number of CNF variable for each node ID (-1 if unused)
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#define DAR_MIN(a,b) (((a) < (b))? (a) : (b))
#define DAR_MAX(a,b) (((a) > (b))? (a) : (b))
#define DAR_INFINITY (100000000)
#ifndef PRT
#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
@ -187,6 +219,7 @@ static inline int Dar_ManLatchNum( Dar_Man_t * p ) { return p->nO
static inline int Dar_ManNodeNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_AND]+p->nObjs[DAR_AIG_EXOR]; }
static inline int Dar_ManGetCost( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_AND]+3*p->nObjs[DAR_AIG_EXOR]; }
static inline int Dar_ManObjNum( Dar_Man_t * p ) { return p->nCreated - p->nDeleted; }
static inline int Dar_ManObjIdMax( Dar_Man_t * p ) { return Vec_PtrSize(p->vObjs); }
static inline Dar_Type_t Dar_ObjType( Dar_Obj_t * pObj ) { return (Dar_Type_t)pObj->Type; }
static inline int Dar_ObjIsNone( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_NONE; }
@ -241,6 +274,8 @@ static inline int Dar_ObjFanoutC( Dar_Obj_t * pObj, Dar_Obj_t * pFanout
if ( Dar_ObjFanin1(pFanout) == pObj ) return Dar_ObjFaninC1(pObj);
assert(0); return -1;
}
static inline Dar_Cut_t * Dar_ObjBestCut( Dar_Obj_t * pObj ) { return (Dar_Cut_t *)pObj->pNext; }
static inline void Dar_ObjSetBestCut( Dar_Obj_t * pObj, Dar_Cut_t * pCut ) { pObj->pNext = (Dar_Obj_t *)pCut; }
// create the ghost of the new node
static inline Dar_Obj_t * Dar_ObjCreateGhost( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1, Dar_Type_t Type )
@ -278,9 +313,10 @@ static inline Dar_Obj_t * Dar_ManFetchMemory( Dar_Man_t * p )
static inline void Dar_ManRecycleMemory( Dar_Man_t * p, Dar_Obj_t * pEntry )
{
extern void Dar_MmFixedEntryRecycle( Dar_MmFixed_t * p, char * pEntry );
p->nDeleted++;
assert( pEntry->nRefs == 0 );
pEntry->Type = DAR_AIG_NONE; // distinquishes a dead node from a live node
Dar_MmFixedEntryRecycle( p->pMemObjs, (char *)pEntry );
p->nDeleted++;
}
@ -297,6 +333,12 @@ static inline void Dar_ManRecycleMemory( Dar_Man_t * p, Dar_Obj_t * pEntry )
// iterator over all objects, including those currently not used
#define Dar_ManForEachObj( p, pObj, i ) \
Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
// iterator over all cuts of the node
#define Dar_ObjForEachCut( pObj, pCut, i ) \
for ( pCut = pObj->pData, i = 0; i < (int)pObj->nCuts; i++, pCut++ ) if ( i==0 ) {} else
// iterator over leaves of the cut
#define Dar_CutForEachLeaf( p, pCut, pLeaf, i ) \
for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = Dar_ManObj(p, (pCut)->pLeaves[i])); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
@ -307,15 +349,25 @@ extern Dar_Man_t * Dar_ManBalance( Dar_Man_t * p, int fUpdateLevel );
extern Dar_Obj_t * Dar_NodeBalanceBuildSuper( Dar_Man_t * p, Vec_Ptr_t * vSuper, Dar_Type_t Type, int fUpdateLevel );
/*=== darCheck.c ========================================================*/
extern int Dar_ManCheck( Dar_Man_t * p );
/*=== darCnf.c ========================================================*/
extern Dar_Cnf_t * Dar_ManDeriveCnf( Dar_Man_t * p );
extern Dar_Cut_t * Dar_ObjFindBestCut( Dar_Obj_t * pObj );
extern void Dar_CutAssignAreaFlow( Dar_Man_t * p, Dar_Cut_t * pCut );
extern void Dar_CutAssignArea( Dar_Man_t * p, Dar_Cut_t * pCut );
extern void Dar_CnfFree( Dar_Cnf_t * pCnf );
/*=== darCore.c ========================================================*/
extern int Dar_ManRewrite( Dar_Man_t * p );
extern int Dar_ManComputeCuts( Dar_Man_t * p );
/*=== darCut.c ========================================================*/
extern void Dar_ManSetupPis( Dar_Man_t * p );
extern void Dar_ObjComputeCuts_rec( Dar_Man_t * p, Dar_Obj_t * pObj );
extern Dar_Cut_t * Dar_ObjComputeCuts_rec( Dar_Man_t * p, Dar_Obj_t * pObj );
extern Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Dar_Obj_t * pObj );
extern void Dar_ManCutsFree( Dar_Man_t * p );
/*=== darData.c ========================================================*/
extern Vec_Int_t * Dar_LibReadNodes();
extern Vec_Int_t * Dar_LibReadOuts();
/*=== darData2.c ========================================================*/
extern void Dar_LibReadMsops( char ** ppSopSizes, char *** ppSops );
/*=== darDfs.c ==========================================================*/
extern Vec_Ptr_t * Dar_ManDfs( Dar_Man_t * p );
extern int Dar_ManCountLevels( Dar_Man_t * p );
@ -327,7 +379,7 @@ extern Dar_Obj_t * Dar_Compose( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Obj_t
/*=== darLib.c ==========================================================*/
extern void Dar_LibStart();
extern void Dar_LibStop();
extern int Dar_LibEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCut, int Required );
extern void Dar_LibEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCut, int Required );
extern Dar_Obj_t * Dar_LibBuildBest( Dar_Man_t * p );
/*=== darMan.c ==========================================================*/
extern Dar_Man_t * Dar_ManStart();
@ -335,6 +387,7 @@ extern Dar_Man_t * Dar_ManDup( Dar_Man_t * p );
extern void Dar_ManStop( Dar_Man_t * p );
extern int Dar_ManCleanup( Dar_Man_t * p );
extern void Dar_ManPrintStats( Dar_Man_t * p );
extern void Dar_ManPrintRuntime( Dar_Man_t * p );
/*=== darMem.c ==========================================================*/
extern void Dar_ManStartMemory( Dar_Man_t * p );
extern void Dar_ManStopMemory( Dar_Man_t * p );
@ -372,12 +425,14 @@ extern void Dar_TableProfile( Dar_Man_t * p );
/*=== darUtil.c =========================================================*/
extern Dar_Par_t * Dar_ManDefaultParams();
extern void Dar_ManIncrementTravId( Dar_Man_t * p );
extern int Dar_ManLevels( Dar_Man_t * p );
extern void Dar_ManCleanData( Dar_Man_t * p );
extern void Dar_ObjCleanData_rec( Dar_Obj_t * pObj );
extern void Dar_ObjCollectMulti( Dar_Obj_t * pFunc, Vec_Ptr_t * vSuper );
extern int Dar_ObjIsMuxType( Dar_Obj_t * pObj );
extern int Dar_ObjRecognizeExor( Dar_Obj_t * pObj, Dar_Obj_t ** ppFan0, Dar_Obj_t ** ppFan1 );
extern Dar_Obj_t * Dar_ObjRecognizeMux( Dar_Obj_t * pObj, Dar_Obj_t ** ppObjT, Dar_Obj_t ** ppObjE );
extern Dar_Obj_t * Dar_ObjReal_rec( Dar_Obj_t * pObj );
extern void Dar_ObjPrintEqn( FILE * pFile, Dar_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
extern void Dar_ObjPrintVerilog( FILE * pFile, Dar_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
extern void Dar_ObjPrintVerbose( Dar_Obj_t * pObj, int fHaig );

679
src/aig/dar/darCnf.c Normal file
View File

@ -0,0 +1,679 @@
/**CFile****************************************************************
FileName [darCnf.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [DAG-aware AIG rewriting.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: darCnf.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "dar.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Dereferences the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Dar_CurDeref2( Dar_Man_t * p, Dar_Cut_t * pCut )
{
Dar_Obj_t * pLeaf;
int i;
Dar_CutForEachLeaf( p, pCut, pLeaf, i )
{
assert( pLeaf->nRefs > 0 );
pLeaf->nRefs--;
}
}
/**Function*************************************************************
Synopsis [References the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Dar_CurRef2( Dar_Man_t * p, Dar_Cut_t * pCut )
{
Dar_Obj_t * pLeaf;
int i;
Dar_CutForEachLeaf( p, pCut, pLeaf, i )
pLeaf->nRefs++;
}
/**Function*************************************************************
Synopsis [Computes area of the first level.]
Description [The cut need to be derefed.]
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_CutDeref( Dar_Man_t * p, Dar_Cut_t * pCut )
{
Dar_Obj_t * pLeaf;
int i;
Dar_CutForEachLeaf( p, pCut, pLeaf, i )
{
assert( pLeaf->nRefs > 0 );
if ( --pLeaf->nRefs > 0 || !Dar_ObjIsAnd(pLeaf) )
continue;
Dar_CutDeref( p, Dar_ObjBestCut(pLeaf) );
}
}
/**Function*************************************************************
Synopsis [Computes area of the first level.]
Description [The cut need to be derefed.]
SideEffects []
SeeAlso []
***********************************************************************/
int Dar_CutRef( Dar_Man_t * p, Dar_Cut_t * pCut )
{
Dar_Obj_t * pLeaf;
int i, Area = pCut->Cost;
Dar_CutForEachLeaf( p, pCut, pLeaf, i )
{
assert( pLeaf->nRefs >= 0 );
if ( pLeaf->nRefs++ > 0 || !Dar_ObjIsAnd(pLeaf) )
continue;
Area += Dar_CutRef( p, Dar_ObjBestCut(pLeaf) );
}
return Area;
}
/**Function*************************************************************
Synopsis [Computes exact area of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dar_CutArea( Dar_Man_t * p, Dar_Cut_t * pCut )
{
int Area = Dar_CutRef( p, pCut );
Dar_CutDeref( p, pCut );
return Area;
}
/**Function*************************************************************
Synopsis [Returns 1 if the second cut is better.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dar_CutCompare( Dar_Cut_t * pC0, Dar_Cut_t * pC1 )
{
if ( pC0->Area < pC1->Area - 0.0001 )
return -1;
if ( pC0->Area > pC1->Area + 0.0001 ) // smaller area flow is better
return 1;
/*
if ( pC0->NoRefs < pC1->NoRefs )
return -1;
if ( pC0->NoRefs > pC1->NoRefs ) // fewer non-referenced fanins is better
return 1;
*/
// if ( pC0->FanRefs / pC0->nLeaves > pC1->FanRefs / pC1->nLeaves )
// return -1;
// if ( pC0->FanRefs / pC0->nLeaves < pC1->FanRefs / pC1->nLeaves )
return 1; // larger average fanin ref-counter is better
// return 0;
}
/**Function*************************************************************
Synopsis [Returns the cut with the smallest area flow.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dar_Cut_t * Dar_ObjFindBestCut( Dar_Obj_t * pObj )
{
Dar_Cut_t * pCut, * pCutBest;
int i;
pCutBest = NULL;
Dar_ObjForEachCut( pObj, pCut, i )
if ( pCutBest == NULL || Dar_CutCompare(pCutBest, pCut) == 1 )
pCutBest = pCut;
return pCutBest;
}
/**Function*************************************************************
Synopsis [Computes area flow of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_CutAssignAreaFlow( Dar_Man_t * p, Dar_Cut_t * pCut )
{
Dar_Obj_t * pLeaf;
int i;
pCut->Area = (float)pCut->Cost;
pCut->NoRefs = 0;
pCut->FanRefs = 0;
Dar_CutForEachLeaf( p, pCut, pLeaf, i )
{
if ( !Dar_ObjIsNode(pLeaf) )
continue;
if ( pLeaf->nRefs == 0 )
{
pCut->Area += Dar_ObjBestCut(pLeaf)->Area;
// pCut->NoRefs++;
}
else
{
pCut->Area += Dar_ObjBestCut(pLeaf)->Area / pLeaf->nRefs;
// if ( pCut->FanRefs + pLeaf->nRefs > 15 )
// pCut->FanRefs = 15;
// else
// pCut->FanRefs += pLeaf->nRefs;
}
}
}
/**Function*************************************************************
Synopsis [Computes area flow of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_CutAssignArea( Dar_Man_t * p, Dar_Cut_t * pCut )
{
Dar_Obj_t * pLeaf;
int i;
pCut->Area = (float)pCut->Cost;
pCut->NoRefs = 0;
pCut->FanRefs = 0;
Dar_CutForEachLeaf( p, pCut, pLeaf, i )
{
if ( !Dar_ObjIsNode(pLeaf) )
continue;
if ( pLeaf->nRefs == 0 )
{
pCut->Area += Dar_ObjBestCut(pLeaf)->Cost;
pCut->NoRefs++;
}
else
{
if ( pCut->FanRefs + pLeaf->nRefs > 15 )
pCut->FanRefs = 15;
else
pCut->FanRefs += pLeaf->nRefs;
}
}
}
/**Function*************************************************************
Synopsis [Computes area, references, and nodes used in the mapping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dar_ManScanMapping_rec( Dar_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vMapped )
{
Dar_Obj_t * pLeaf;
Dar_Cut_t * pCutBest;
int aArea, i;
if ( pObj->nRefs++ || Dar_ObjIsPi(pObj) || Dar_ObjIsConst1(pObj) )
return 0;
assert( Dar_ObjIsAnd(pObj) );
// collect the node first to derive pre-order
if ( vMapped )
{
// printf( "%d ", Dar_ObjBestCut(pObj)->Cost );
Vec_PtrPush( vMapped, pObj );
}
// visit the transitive fanin of the selected cut
pCutBest = Dar_ObjBestCut(pObj);
aArea = pCutBest->Cost;
Dar_CutForEachLeaf( p, pCutBest, pLeaf, i )
aArea += Dar_ManScanMapping_rec( p, pLeaf, vMapped );
return aArea;
}
/**Function*************************************************************
Synopsis [Computes area, references, and nodes used in the mapping.]
Description [Collects the nodes in reverse topological order in array
p->vMapping.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Dar_ManScanMapping( Dar_Man_t * p, int fCollect )
{
Vec_Ptr_t * vMapped = NULL;
Dar_Obj_t * pObj;
int i;
// clean all references
Dar_ManForEachObj( p, pObj, i )
pObj->nRefs = 0;
// allocate the array
if ( fCollect )
vMapped = Vec_PtrAlloc( 1000 );
// collect nodes reachable from POs in the DFS order through the best cuts
p->aArea = 0;
Dar_ManForEachPo( p, pObj, i )
p->aArea += Dar_ManScanMapping_rec( p, Dar_ObjFanin0(pObj), vMapped );
printf( "Variables = %d. Clauses = %6d.\n", vMapped? Vec_PtrSize(vMapped) : 0, p->aArea );
return vMapped;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dar_ManMapForCnf( Dar_Man_t * p )
{
Dar_Obj_t * pObj;
Dar_Cut_t * pCut;
int i, k;
// visit the nodes in the topological order and update their best cuts
Dar_ManForEachObj( p, pObj, i )
{
if ( !Dar_ObjIsNode(pObj) )
continue;
// if ( pObj->nRefs )
// continue;
// if the node is used, dereference its cut
if ( pObj->nRefs )
Dar_CutDeref( p, Dar_ObjBestCut(pObj) );
// evaluate the cuts of this node
Dar_ObjForEachCut( pObj, pCut, k )
// Dar_CutAssignArea( p, pCut );
// Dar_CutAssignAreaFlow( p, pCut );
pCut->Area = (float)Dar_CutArea( p, pCut );
// find a new good cut
Dar_ObjSetBestCut( pObj, Dar_ObjFindBestCut(pObj) );
// if the node is used, reference its cut
if ( pObj->nRefs )
Dar_CutRef( p, Dar_ObjBestCut(pObj) );
}
return 1;
}
/**Function*************************************************************
Synopsis [Returns the number of literals in the SOP.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dar_SopCountLiterals( char * pSop, int nCubes )
{
int nLits = 0, Cube, i, b;
for ( i = 0; i < nCubes; i++ )
{
Cube = pSop[i];
for ( b = 3; b >= 0; b-- )
{
if ( Cube % 3 != 2 )
nLits++;
Cube = Cube / 3;
}
}
return nLits;
}
/**Function*************************************************************
Synopsis [Writes the cube and returns the number of literals in it.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dar_SopWriteCube( char Cube, int * pVars, int fCompl, int * pLiterals )
{
int nLits = 4, b;
for ( b = 3; b >= 0; b-- )
{
if ( Cube % 3 == 0 )
*pLiterals++ = 2 * pVars[b] + 1 ^ fCompl;
else if ( Cube % 3 == 1 )
*pLiterals++ = 2 * pVars[b] + fCompl;
else
nLits--;
Cube = Cube / 3;
}
return nLits;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dar_Cnf_t * Dar_ManWriteCnf( Dar_Man_t * p, Vec_Ptr_t * vMapped )
{
Dar_Cnf_t * pCnf;
Dar_Obj_t * pObj;
Dar_Cut_t * pCut;
int OutVar, pVars[4], * pLits, ** pClas;
unsigned uTruth;
int i, k, nLiterals, nClauses, nCubes, Number;
// count the number of literals and clauses
nLiterals = 1 + Dar_ManPoNum( p );
nClauses = 1 + Dar_ManPoNum( p );
Vec_PtrForEachEntry( vMapped, pObj, i )
{
assert( Dar_ObjIsNode(pObj) );
pCut = Dar_ObjBestCut( pObj );
// positive polarity of the cut
uTruth = pCut->uTruth;
nLiterals += Dar_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
nClauses += p->pSopSizes[uTruth];
// negative polarity of the cut
uTruth = 0xFFFF & ~pCut->uTruth;
nLiterals += Dar_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
nClauses += p->pSopSizes[uTruth];
}
// allocate CNF
pCnf = ALLOC( Dar_Cnf_t, 1 );
memset( pCnf, 0, sizeof(Dar_Cnf_t) );
pCnf->nLiterals = nLiterals;
pCnf->nClauses = nClauses;
pCnf->pClauses = ALLOC( int *, nClauses );
pCnf->pClauses[0] = ALLOC( int, nLiterals );
pCnf->pVarNums = ALLOC( int, 1+Dar_ManObjIdMax(p) );
// set variable numbers
Number = 0;
memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Dar_ManObjIdMax(p)) );
Vec_PtrForEachEntry( vMapped, pObj, i )
pCnf->pVarNums[pObj->Id] = Number++;
Dar_ManForEachPi( p, pObj, i )
pCnf->pVarNums[pObj->Id] = Number++;
pCnf->pVarNums[Dar_ManConst1(p)->Id] = Number++;
// assign the clauses
pLits = pCnf->pClauses[0];
pClas = pCnf->pClauses;
Vec_PtrForEachEntry( vMapped, pObj, i )
{
pCut = Dar_ObjBestCut( pObj );
// write variables of this cut
OutVar = pCnf->pVarNums[ pObj->Id ];
for ( k = 0; k < (int)pCut->nLeaves; k++ )
{
pVars[k] = pCnf->pVarNums[ pCut->pLeaves[k] ];
assert( pVars[k] <= Dar_ManObjIdMax(p) );
}
// positive polarity of the cut
uTruth = pCut->uTruth;
nCubes = p->pSopSizes[uTruth];
// write the cubes
for ( k = 0; k < nCubes; k++ )
{
*pClas++ = pLits;
*pLits++ = 2 * pVars[OutVar] + 1;
pLits += Dar_SopWriteCube( p->pSops[uTruth][k], pVars, 0, pLits );
}
// negative polarity of the cut
uTruth = 0xFFFF & ~pCut->uTruth;
nCubes = p->pSopSizes[uTruth];
// write the cubes
for ( k = 0; k < nCubes; k++ )
{
*pClas++ = pLits;
*pLits++ = 2 * pVars[OutVar];
pLits += Dar_SopWriteCube( p->pSops[uTruth][k], pVars, 1, pLits );
}
}
// write the output literals
Dar_ManForEachPo( p, pObj, i )
{
OutVar = pCnf->pVarNums[ Dar_ObjFanin0(pObj)->Id ];
*pClas++ = pLits;
*pLits++ = 2 * pVars[OutVar] + Dar_ObjFaninC0(pObj);
}
// write the constant literal
OutVar = pCnf->pVarNums[ Dar_ManConst1(p)->Id ];
assert( OutVar <= Dar_ManObjIdMax(p) );
*pClas++ = pLits;
*pLits++ = 2 * pVars[OutVar];
// verify that the correct number of literals and clauses was written
assert( pLits - pCnf->pClauses[0] == nLiterals );
assert( pClas - pCnf->pClauses == nClauses );
return pCnf;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_CnfFree( Dar_Cnf_t * pCnf )
{
if ( pCnf == NULL )
return;
free( pCnf->pClauses[0] );
free( pCnf->pClauses );
free( pCnf->pVarNums );
free( pCnf );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_ManExploreMapping( Dar_Man_t * p )
{
extern int Dar_ManLargeCutEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCutR, Dar_Cut_t * pCutL, int Leaf );
int nNew, Gain, nGain = 0, nVars = 0;
Dar_Obj_t * pObj, * pLeaf;
Dar_Cut_t * pCutBest, * pCut;
int i, k, a, b, Counter;
Dar_ManForEachObj( p, pObj, i )
{
if ( !Dar_ObjIsNode(pObj) )
continue;
if ( pObj->nRefs == 0 )
continue;
pCutBest = Dar_ObjBestCut(pObj);
Dar_CutForEachLeaf( p, pCutBest, pLeaf, k )
{
if ( !Dar_ObjIsNode(pLeaf) )
continue;
assert( pLeaf->nRefs != 0 );
if ( pLeaf->nRefs != 1 )
continue;
pCut = Dar_ObjBestCut(pLeaf);
/*
// find how many common variable they have
Counter = 0;
for ( a = 0; a < (int)pCut->nLeaves; a++ )
{
for ( b = 0; b < (int)pCutBest->nLeaves; b++ )
if ( pCut->pLeaves[a] == pCutBest->pLeaves[b] )
break;
if ( b == (int)pCutBest->nLeaves )
continue;
Counter++;
}
printf( "%d ", Counter );
*/
// find the new truth table after collapsing these two cuts
nNew = Dar_ManLargeCutEval( p, pObj, pCutBest, pCut, pLeaf->Id );
// printf( "%d+%d=%d:%d(%d) ", pCutBest->Cost, pCut->Cost,
// pCutBest->Cost+pCut->Cost, nNew, pCutBest->Cost+pCut->Cost-nNew );
Gain = pCutBest->Cost+pCut->Cost-nNew;
if ( Gain > 0 )
{
nGain += Gain;
nVars++;
}
}
}
printf( "Total gain = %d. Vars = %d.\n", nGain, nVars );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dar_Cnf_t * Dar_ManDeriveCnf( Dar_Man_t * p )
{
Dar_Cnf_t * pCnf = NULL;
Vec_Ptr_t * vMapped;
int i, nIters = 2;
int clk;
// derive SOPs for all 4-variable functions
clk = clock();
Dar_LibReadMsops( &p->pSopSizes, &p->pSops );
PRT( "setup", clock() - clk );
// generate cuts for all nodes, assign cost, and find best cuts
// (used pObj->pNext for storing the best cut of the node!)
clk = clock();
Dar_ManComputeCuts( p );
PRT( "cuts ", clock() - clk );
// iteratively improve area flow
for ( i = 0; i < nIters; i++ )
{
clk = clock();
Dar_ManScanMapping( p, 0 );
Dar_ManMapForCnf( p );
PRT( "iter ", clock() - clk );
}
// write the file
vMapped = Dar_ManScanMapping( p, 1 );
clk = clock();
Dar_ManExploreMapping( p );
PRT( "exten", clock() - clk );
// pCnf = Dar_ManWriteCnf( p, vMapped );
Vec_PtrFree( vMapped );
// clean up
Dar_ManCutsFree( p );
return pCnf;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

80
src/aig/dar/darCore.c
View File

@ -42,9 +42,10 @@
int Dar_ManRewrite( Dar_Man_t * p )
{
ProgressBar * pProgress;
Dar_Cut_t * pCutSet;
Dar_Obj_t * pObj, * pObjNew;
int i, k, nNodesOld, nNodeBefore, nNodeAfter, Required;
int clk = 0, clkStart = clock();
int clk = 0, clkStart;
// remove dangling nodes
Dar_ManCleanup( p );
// set elementary cuts for the PIs
@ -52,6 +53,8 @@ int Dar_ManRewrite( Dar_Man_t * p )
// if ( p->pPars->fUpdateLevel )
// Dar_NtkStartReverseLevels( p );
// resynthesize each node once
clkStart = clock();
p->nNodesInit = Dar_ManNodeNum(p);
nNodesOld = Vec_PtrSize( p->vObjs );
pProgress = Extra_ProgressBarStart( stdout, nNodesOld );
Dar_ManForEachObj( p, pObj, i )
@ -61,13 +64,30 @@ int Dar_ManRewrite( Dar_Man_t * p )
continue;
if ( i > nNodesOld )
break;
if ( pObj->Id == 654 )
{
int x = 0;
}
// compute cuts for the node
Dar_ObjComputeCuts_rec( p, pObj );
clk = clock();
pCutSet = Dar_ObjComputeCuts_rec( p, pObj );
p->timeCuts += clock() - clk;
// go through the cuts of this node
Required = 1000000;
p->GainBest = -1;
for ( k = 1; k < (int)pObj->nCuts; k++ )
Dar_LibEval( p, pObj, (Dar_Cut_t *)pObj->pData + k, Required );
{
/*
if ( pObj->Id == 654 )
{
int m;
for ( m = 0; m < 4; m++ )
printf( "%d ", pCutSet[k].pLeaves[m] );
printf( "\n" );
}
*/
Dar_LibEval( p, pObj, pCutSet + k, Required );
}
// check the best gain
if ( !(p->GainBest > 0 || p->GainBest == 0 && p->pPars->fUseZeros) )
continue;
@ -75,13 +95,21 @@ int Dar_ManRewrite( Dar_Man_t * p )
nNodeBefore = Dar_ManNodeNum( p );
pObjNew = Dar_LibBuildBest( p );
pObjNew = Dar_NotCond( pObjNew, pObjNew->fPhase ^ pObj->fPhase );
// remove the old nodes
assert( (int)Dar_Regular(pObjNew)->Level <= Required );
// replace the node
Dar_ObjReplace( p, pObj, pObjNew, 1 );
// remove the old cuts
pObj->pData = NULL;
// compare the gains
nNodeAfter = Dar_ManNodeNum( p );
assert( p->GainBest == nNodeBefore - nNodeAfter );
assert( (int)pObjNew->Level <= Required );
assert( p->GainBest <= nNodeBefore - nNodeAfter );
// count gains of this class
p->ClassGains[p->ClassBest] += nNodeBefore - nNodeAfter;
}
p->timeTotal = clock() - clkStart;
p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
Extra_ProgressBarStop( pProgress );
Dar_ManCutsFree( p );
// put the nodes into the DFS order and reassign their IDs
@ -99,6 +127,46 @@ int Dar_ManRewrite( Dar_Man_t * p )
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dar_ManComputeCuts( Dar_Man_t * p )
{
Dar_Obj_t * pObj;
int i, clk = 0, clkStart = clock();
int nCutsMax = 0, nCutsTotal = 0;
// remove dangling nodes
Dar_ManCleanup( p );
// set elementary cuts for the PIs
Dar_ManSetupPis( p );
// compute cuts for each nodes in the topological order
Dar_ManForEachObj( p, pObj, i )
{
if ( !Dar_ObjIsNode(pObj) )
continue;
Dar_ObjComputeCuts( p, pObj );
nCutsTotal += pObj->nCuts - 1;
nCutsMax = DAR_MAX( nCutsMax, (int)pObj->nCuts - 1 );
}
// print statistics on the number of non-trivial cuts
printf( "Node = %6d. Cut = %8d. Max = %3d. Ave = %.2f. Filter = %8d. Created = %8d.\n",
Dar_ManNodeNum(p), nCutsTotal, nCutsMax, (float)nCutsTotal/Dar_ManNodeNum(p),
p->nCutsFiltered, p->nCutsFiltered+nCutsTotal+Dar_ManNodeNum(p)+Dar_ManPiNum(p) );
PRT( "Time", clock() - clkStart );
// free the cuts
// Dar_ManCutsFree( p );
return 1;
}
////////////////////////////////////////////////////////////////////////

77
src/aig/dar/darCut.c
View File

@ -69,15 +69,12 @@ int Dar_CutFilter( Dar_Man_t * p, Dar_Cut_t * pCut )
{
Dar_Cut_t * pTemp;
int i, k;
assert( p->pBaseCuts[p->nBaseCuts] == pCut );
for ( i = 0; i < p->nBaseCuts; i++ )
assert( p->pBaseCuts[p->nCutsUsed] == pCut );
for ( i = 0; i < p->nCutsUsed; i++ )
{
pTemp = p->pBaseCuts[i];
if ( pTemp->nLeaves > pCut->nLeaves )
{
// do not fiter the first cut
if ( i == 0 )
continue;
// skip the non-contained cuts
if ( (pTemp->uSign & pCut->uSign) != pCut->uSign )
continue;
@ -89,11 +86,12 @@ int Dar_CutFilter( Dar_Man_t * p, Dar_Cut_t * pCut )
// p->nCuts--;
// i--;
// remove contained cut
for ( k = i; k < p->nBaseCuts; k++ )
for ( k = i; k < p->nCutsUsed; k++ )
p->pBaseCuts[k] = p->pBaseCuts[k+1];
p->pBaseCuts[p->nBaseCuts] = pTemp;
p->nBaseCuts--;
p->pBaseCuts[p->nCutsUsed] = pTemp;
p->nCutsUsed--;
i--;
p->nCutsFiltered++;
}
}
else
@ -103,7 +101,10 @@ int Dar_CutFilter( Dar_Man_t * p, Dar_Cut_t * pCut )
continue;
// check containment seriously
if ( Dar_CutCheckDominance( pTemp, pCut ) )
{
p->nCutsFiltered++;
return 1;
}
}
}
return 0;
@ -215,14 +216,14 @@ static inline int Dar_CutMergeOrdered( Dar_Cut_t * pC, Dar_Cut_t * pC0, Dar_Cut_
int Dar_CutMerge( Dar_Cut_t * pCut, Dar_Cut_t * pCut0, Dar_Cut_t * pCut1 )
{
// merge the nodes
if ( pCut0->nLeaves < pCut1->nLeaves )
if ( pCut0->nLeaves <= pCut1->nLeaves )
{
if ( !Dar_CutMergeOrdered( pCut, pCut1, pCut0 ) )
return 0;
}
else
{
if ( !Dar_CutMergeOrdered( pCut, pCut1, pCut0 ) )
if ( !Dar_CutMergeOrdered( pCut, pCut0, pCut1 ) )
return 0;
}
pCut->uSign = pCut0->uSign | pCut1->uSign;
@ -332,7 +333,6 @@ static inline unsigned Dar_CutTruthShrink( unsigned uTruth, int nVars, unsigned
uTruth = Dar_CutTruthSwapAdjacentVars( uTruth, k );
Var++;
}
assert( Var == nVars );
return uTruth;
}
@ -396,11 +396,12 @@ int Dar_CutSuppMinimize( Dar_Cut_t * pCut )
if ( !(uPhase & (1 << i)) )
continue;
pCut->pLeaves[k] = pCut->pLeaves[i];
pCut->pIndices[k] = pCut->pIndices[i];
// pCut->pIndices[k] = pCut->pIndices[i];
pCut->uSign |= (1 << (pCut->pLeaves[i] & 31));
k++;
}
assert( k == nLeaves );
pCut->nLeaves = nLeaves;
return 1;
}
@ -419,9 +420,10 @@ void Dar_ObjSetupTrivial( Dar_Obj_t * pObj )
{
Dar_Cut_t * pCut;
pCut = pObj->pData;
pCut->Cost = 0;
pCut->nLeaves = 1;
pCut->pLeaves[0] = pObj->Id;
pCut->pIndices[0] = 0;
// pCut->pIndices[0] = 0;
pCut->uSign = (1 << (pObj->Id & 31));
pCut->uTruth = 0xAAAA;
}
@ -481,19 +483,21 @@ void Dar_ManCutsFree( Dar_Man_t * p )
SeeAlso []
***********************************************************************/
void Dar_ObjComputeCuts( Dar_Man_t * p, Dar_Obj_t * pObj )
Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Dar_Obj_t * pObj )
{
Dar_Cut_t * pCut0 = Dar_ObjFanin0(pObj)->pData;
Dar_Cut_t * pCut1 = Dar_ObjFanin1(pObj)->pData;
Dar_Cut_t * pStop0 = pCut0 + Dar_ObjFanin0(pObj)->nCuts;
Dar_Cut_t * pStop1 = pCut1 + Dar_ObjFanin1(pObj)->nCuts;
Dar_Cut_t * pCut;
Dar_Obj_t * pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) );
Dar_Obj_t * pFanin1 = Dar_ObjReal_rec( Dar_ObjChild1(pObj) );
Dar_Cut_t * pStart0 = Dar_Regular(pFanin0)->pData;
Dar_Cut_t * pStart1 = Dar_Regular(pFanin1)->pData;
Dar_Cut_t * pStop0 = pStart0 + Dar_Regular(pFanin0)->nCuts;
Dar_Cut_t * pStop1 = pStart1 + Dar_Regular(pFanin1)->nCuts;
Dar_Cut_t * pCut0, * pCut1, * pCut;
int i;
assert( pObj->pData == NULL );
// make sure fanins cuts are computed
p->nCutsUsed = 0;
for ( ; pCut0 < pStop0; pCut0++ )
for ( ; pCut1 < pStop1; pCut1++ )
for ( pCut0 = pStart0; pCut0 < pStop0; pCut0++ )
for ( pCut1 = pStart1; pCut1 < pStop1; pCut1++ )
{
// get storage for the next cut
if ( p->nCutsUsed == p->nBaseCuts )
@ -506,10 +510,24 @@ void Dar_ObjComputeCuts( Dar_Man_t * p, Dar_Obj_t * pObj )
if ( Dar_CutFilter( p, pCut ) )
continue;
// compute truth table
pCut->uTruth = 0xFFFF & Dar_CutTruth( pCut, pCut0, pCut1, Dar_ObjFaninC0(pObj), Dar_ObjFaninC1(pObj) );
pCut->uTruth = 0xFFFF & Dar_CutTruth( pCut, pCut0, pCut1, Dar_IsComplement(pFanin0), Dar_IsComplement(pFanin1) );
// minimize support of the cut
if ( Dar_CutSuppMinimize( pCut ) )
Dar_CutFilter( p, pCut );
{
if ( Dar_CutFilter( p, pCut ) )
continue;
}
// CNF mapping: assign the cut cost if needed
if ( p->pSopSizes )
{
pCut->Cost = p->pSopSizes[pCut->uTruth] + p->pSopSizes[0xFFFF & ~pCut->uTruth];
Dar_CutAssignAreaFlow( p, pCut );
}
// increment the number of cuts
p->nCutsUsed++;
}
// get memory for the cuts of this node
pObj->nCuts = p->nCutsUsed + 1;
@ -519,6 +537,11 @@ void Dar_ObjComputeCuts( Dar_Man_t * p, Dar_Obj_t * pObj )
// copy non-elementary cuts
for ( i = 0; i < p->nCutsUsed; i++ )
*++pCut = *(p->pBaseCuts[i]);
// CNF mapping: assign the best cut if needed
if ( p->pSopSizes )
Dar_ObjSetBestCut( pObj, Dar_ObjFindBestCut(pObj) );
return pObj->pData;
}
/**Function*************************************************************
@ -532,13 +555,15 @@ void Dar_ObjComputeCuts( Dar_Man_t * p, Dar_Obj_t * pObj )
SeeAlso []
***********************************************************************/
void Dar_ObjComputeCuts_rec( Dar_Man_t * p, Dar_Obj_t * pObj )
Dar_Cut_t * Dar_ObjComputeCuts_rec( Dar_Man_t * p, Dar_Obj_t * pObj )
{
if ( pObj->pData )
return;
return pObj->pData;
if ( Dar_ObjIsBuf(pObj) )
return Dar_ObjComputeCuts_rec( p, Dar_ObjFanin0(pObj) );
Dar_ObjComputeCuts_rec( p, Dar_ObjFanin0(pObj) );
Dar_ObjComputeCuts_rec( p, Dar_ObjFanin1(pObj) );
Dar_ObjComputeCuts( p, pObj );
return Dar_ObjComputeCuts( p, pObj );
}
////////////////////////////////////////////////////////////////////////

6
src/aig/dar/darData.c
View File

@ -9476,7 +9476,7 @@ Vec_Int_t * Dar_LibReadOuts()
SeeAlso []
***********************************************************************/
void Dat_NtkGenerateArrays( Abc_Ntk_t * pNtk )
void Dar_NtkGenerateArrays( Abc_Ntk_t * pNtk )
{
extern int Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
@ -9596,6 +9596,10 @@ void Dat_NtkGenerateArrays( Abc_Ntk_t * pNtk )
//#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

4783
src/aig/dar/darData2.c Normal file
View File

File diff suppressed because it is too large Load Diff

171
src/aig/dar/darLib.c
View File

@ -41,12 +41,11 @@ struct Dar_LibObj_t_ // library object (2 words)
struct Dar_LibDat_t_ // library object data
{
Dar_Obj_t * pFunc; // the corresponding AIG node
int Level;
int TravId;
float aFlow;
unsigned char Area;
unsigned char nLats[3];
Dar_Obj_t * pFunc; // the corresponding AIG node if it exists
int Level; // level of this node after it is constructured
int TravId; // traversal ID of the library object data
unsigned char Area; // area of the node
unsigned char nLats[3]; // the number of latches on the input/output stem
};
struct Dar_Lib_t_ // library
@ -140,6 +139,7 @@ void Dar_LibFree( Dar_Lib_t * p )
{
free( p->pObjs );
free( p->pDatas );
free( p->pNodesMem );
free( p->pSubgrMem );
free( p->pPerms4 );
free( p->puCanons );
@ -211,7 +211,7 @@ void Dar_LibSetup_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class )
void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts )
{
Dar_LibObj_t * pObj;
int uTruth, Class, Out, i, k;
int nNodesTotal, uTruth, Class, Out, i, k;
assert( p->iObj == p->nObjs );
// count the number of representatives of each class
@ -243,9 +243,9 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts )
p->pSubgr[Class][ p->nSubgr[Class]++ ] = Out;
}
// clear truth tables
// create traversal IDs
for ( i = 0; i < p->iObj; i++ )
Dar_LibObj( p, Out )->Num = 0xff;
Dar_LibObj(p, i)->Num = 0xff;
// count nodes in each class
for ( i = 0; i < 222; i++ )
for ( k = 0; k < p->nSubgr[i]; k++ )
@ -263,10 +263,21 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts )
p->pNodesTotal += p->nNodes[i];
p->nNodes[i] = 0;
}
// create traversal IDs
for ( i = 0; i < p->iObj; i++ )
Dar_LibObj(p, i)->Num = 0xff;
// add the nodes to storage
nNodesTotal = 0;
for ( i = 0; i < 222; i++ )
for ( k = 0; k < p->nSubgr[i]; k++ )
{
for ( k = 0; k < p->nSubgr[i]; k++ )
Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i );
nNodesTotal += p->nNodes[i];
}
assert( nNodesTotal == p->pNodesTotal );
// prepare the number of the PI nodes
for ( i = 0; i < 4; i++ )
Dar_LibObj(p, i)->Num = i;
}
/**Function*************************************************************
@ -289,7 +300,7 @@ Dar_Lib_t * Dar_LibRead()
vObjs = Dar_LibReadNodes();
vOuts = Dar_LibReadOuts();
// create library
p = Dar_LibAlloc( Vec_IntSize(vObjs)/2 + 4, 5000 );
p = Dar_LibAlloc( Vec_IntSize(vObjs)/2 + 4, 6000 );
// create nodes
for ( i = 0; i < vObjs->nSize; i += 2 )
Dar_LibAddNode( p, vObjs->pArray[i] >> 1, vObjs->pArray[i+1] >> 1,
@ -371,7 +382,7 @@ int Dar_LibCutMatch( Dar_Man_t * p, Dar_Cut_t * pCut )
p->nCutsBad++;
return 0;
}
pFanin = Dar_NotCond(pFanin, ((uPhase & (1<<i)) > 0) );
pFanin = Dar_NotCond(pFanin, ((uPhase >> i) & 1) );
// Vec_PtrWriteEntry( p->vFaninsCur, i, pFanin );
s_DarLib->pDatas[i].pFunc = pFanin;
s_DarLib->pDatas[i].Level = Dar_Regular(pFanin)->Level;
@ -396,18 +407,20 @@ int Dar_LibCutMatch( Dar_Man_t * p, Dar_Cut_t * pCut )
int Dar_NodeDeref_rec( Dar_Man_t * p, Dar_Obj_t * pNode )
{
Dar_Obj_t * pFanin;
int Counter = 1;
int Counter = 0;
if ( Dar_ObjIsPi(pNode) )
return 0;
return Counter;
pFanin = Dar_ObjFanin0( pNode );
assert( pFanin->nRefs > 0 );
if ( --pFanin->nRefs == 0 )
Counter += Dar_NodeDeref_rec( p, pFanin );
pFanin = Dar_ObjFanin0( pNode );
if ( Dar_ObjIsBuf(pNode) )
return Counter;
pFanin = Dar_ObjFanin1( pNode );
assert( pFanin->nRefs > 0 );
if ( --pFanin->nRefs == 0 )
Counter += Dar_NodeDeref_rec( p, pFanin );
return Counter;
return 1 + Counter;
}
/**Function*************************************************************
@ -424,17 +437,19 @@ int Dar_NodeDeref_rec( Dar_Man_t * p, Dar_Obj_t * pNode )
int Dar_NodeRef_rec( Dar_Man_t * p, Dar_Obj_t * pNode )
{
Dar_Obj_t * pFanin;
int Counter = 1;
int Counter = 0;
if ( Dar_ObjIsPi(pNode) )
return 0;
return Counter;
Dar_ObjSetTravIdCurrent( p, pNode );
pFanin = Dar_ObjFanin0( pNode );
if ( pFanin->nRefs++ == 0 )
Counter += Dar_NodeRef_rec( p, pFanin );
if ( Dar_ObjIsBuf(pNode) )
return Counter;
pFanin = Dar_ObjFanin1( pNode );
if ( pFanin->nRefs++ == 0 )
Counter += Dar_NodeRef_rec( p, pFanin );
return Counter;
return 1 + Counter;
}
/**Function*************************************************************
@ -465,6 +480,34 @@ int Dar_LibCutMarkMffc( Dar_Man_t * p, Dar_Obj_t * pRoot )
return nNodes1;
}
/**Function*************************************************************
Synopsis [Evaluates one cut.]
Description [Returns the best gain.]
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_LibObjPrint_rec( Dar_LibObj_t * pObj )
{
if ( pObj->fTerm )
{
printf( "%c", 'a' + pObj - s_DarLib->pObjs );
return;
}
printf( "(" );
Dar_LibObjPrint_rec( Dar_LibObj(s_DarLib, pObj->Fan0) );
if ( pObj->fCompl0 )
printf( "\'" );
Dar_LibObjPrint_rec( Dar_LibObj(s_DarLib, pObj->Fan1) );
if ( pObj->fCompl0 )
printf( "\'" );
printf( ")" );
}
/**Function*************************************************************
@ -480,43 +523,32 @@ int Dar_LibCutMarkMffc( Dar_Man_t * p, Dar_Obj_t * pRoot )
void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class )
{
Dar_LibObj_t * pObj;
Dar_LibDat_t * pData;
Dar_Obj_t * pFanin0, * pFanin1, * pGhost;
Dar_LibDat_t * pData, * pData0, * pData1;
Dar_Obj_t * pGhost, * pFanin0, * pFanin1;
int i;
for ( i = 0; i < 4; i++ )
{
pObj = Dar_LibObj(s_DarLib, i);
pObj->Num = i;
}
for ( i = 0; i < s_DarLib->nNodes[Class]; i++ )
{
// get one class node, assign its temporary number and set its data
pObj = Dar_LibObj(s_DarLib, s_DarLib->pNodes[Class][i]);
pObj->Num = 4 + i;
pData = s_DarLib->pDatas + pObj->Num;
pData->pFunc = NULL;
pData->TravId = 0xFFFF;
/*
// get the first fanin
pFan = Dar_LibObj(p, pObj->Fan0);
s_DarLib->pDatas[i].Level = s_DarLib->pDatas[pFan->Num].Level;
pFan = Dar_LibObj(p, pObj->Fan1);
if ( s_DarLib->pDatas[i].Level < s_DarLib->pDatas[pFan->Num].Level )
s_DarLib->pDatas[i].Level = s_DarLib->pDatas[pFan->Num].Level;
s_DarLib->pDatas[i].Level++;
*/
pFanin0 = s_DarLib->pDatas[ Dar_LibObj(s_DarLib, pObj->Fan0)->Num ].pFunc;
if ( pFanin0 == NULL )
// explore the fanins
pData0 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan0)->Num;
pData1 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan1)->Num;
pData->Level = 1 + DAR_MAX(pData0->Level, pData1->Level);
if ( pData0->pFunc == NULL || pData1->pFunc == NULL )
continue;
pFanin1 = s_DarLib->pDatas[ Dar_LibObj(s_DarLib, pObj->Fan1)->Num ].pFunc;
if ( pFanin1 == NULL )
continue;
pFanin0 = Dar_NotCond( pFanin0, pObj->fCompl0 );
pFanin1 = Dar_NotCond( pFanin1, pObj->fCompl1 );
pFanin0 = Dar_NotCond( pData0->pFunc, pObj->fCompl0 );
pFanin1 = Dar_NotCond( pData1->pFunc, pObj->fCompl1 );
pGhost = Dar_ObjCreateGhost( p, pFanin0, pFanin1, DAR_AIG_AND );
pData->pFunc = Dar_TableLookup( p, pGhost );
// clear the node if it is part of MFFC
if ( pData->pFunc != NULL && Dar_ObjIsTravIdCurrent(p, pData->pFunc) )
pData->pFunc = NULL;
//if ( Class == 7 )
//printf( "Evaling node %d at data %d\n", pData->pFunc? pData->pFunc->Id : -1, pObj->Num );
}
}
@ -537,6 +569,7 @@ int Dar_LibEval_rec( Dar_LibObj_t * pObj, int Out, int nNodesSaved, int Required
int Area;
if ( pObj->fTerm )
return 0;
assert( pObj->Num > 3 );
pData = s_DarLib->pDatas + pObj->Num;
if ( pData->pFunc )
return 0;
@ -565,41 +598,64 @@ int Dar_LibEval_rec( Dar_LibObj_t * pObj, int Out, int nNodesSaved, int Required
SeeAlso []
***********************************************************************/
int Dar_LibEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCut, int Required )
void Dar_LibEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCut, int Required )
{
Dar_LibObj_t * pObj;
int i, k, Class, nNodesSaved, nNodesAdded, nNodesGained;
int i, k, Class, nNodesSaved, nNodesAdded, nNodesGained, clk;
if ( pCut->nLeaves != 4 )
return;
clk = clock();
/*
for ( k = 0; k < 4; k++ )
if ( pCut->pLeaves[k] > 4 )
return;
*/
// check if the cut exits
if ( !Dar_LibCutMatch(p, pCut) )
return p->GainBest;
return;
// mark MFFC of the node
nNodesSaved = Dar_LibCutMarkMffc( p, pRoot );
// evaluate the cut
Class = s_DarLib->pMap[pCut->uTruth];
Dar_LibEvalAssignNums( p, Class );
//if ( pRoot->Id == 654 )
//printf( "\n" );
// profile outputs by their savings
p->nTotalSubgs += s_DarLib->nSubgr[Class];
p->ClassSubgs[Class] += s_DarLib->nSubgr[Class];
for ( i = 0; i < s_DarLib->nSubgr[Class]; i++ )
{
pObj = Dar_LibObj(s_DarLib, s_DarLib->pSubgr[Class][i]);
if ( pRoot->Id == 654 )
{
// Dar_LibObjPrint_rec( pObj );
// printf( "\n" );
}
nNodesAdded = Dar_LibEval_rec( pObj, i, nNodesSaved, Required );
nNodesGained = nNodesSaved - nNodesAdded;
if ( nNodesGained <= 0 )
continue;
if ( nNodesGained <= p->GainBest )
if ( nNodesGained < p->GainBest ||
(nNodesGained == p->GainBest && s_DarLib->pDatas[pObj->Num].Level >= p->GainBest) )
continue;
// remember this possibility
Vec_PtrClear( p->vLeavesBest );
for ( k = 0; k < 4; k++ )
Vec_PtrPush( p->vLeavesBest, s_DarLib->pDatas[k].pFunc );
p->OutBest = s_DarLib->pSubgr[Class][i];
p->GainBest = nNodesGained;
p->OutBest = s_DarLib->pSubgr[Class][i];
p->LevelBest = s_DarLib->pDatas[pObj->Num].Level;
p->GainBest = nNodesGained;
p->ClassBest = Class;
}
return p->GainBest;
clk = clock() - clk;
p->ClassTimes[Class] += clk;
p->timeEval += clk;
}
/**Function*************************************************************
Synopsis [Reconstructs the best cut.]
Synopsis [Clears the fields of the nodes used in this cut.]
Description []
@ -608,13 +664,14 @@ int Dar_LibEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCut, int Require
SeeAlso []
***********************************************************************/
void Dar_LibBuildClear_rec( Dar_LibObj_t * pObj )
void Dar_LibBuildClear_rec( Dar_LibObj_t * pObj, int * pCounter )
{
if ( pObj->fTerm )
return;
pObj->Num = (*pCounter)++;
s_DarLib->pDatas[ pObj->Num ].pFunc = NULL;
Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, pObj->Fan0) );
Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, pObj->Fan1) );
Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, pObj->Fan0), pCounter );
Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, pObj->Fan1), pCounter );
}
/**Function*************************************************************
@ -638,7 +695,9 @@ Dar_Obj_t * Dar_LibBuildBest_rec( Dar_Man_t * p, Dar_LibObj_t * pObj )
pFanin1 = Dar_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, pObj->Fan1) );
pFanin0 = Dar_NotCond( pFanin0, pObj->fCompl0 );
pFanin1 = Dar_NotCond( pFanin1, pObj->fCompl1 );
return pData->pFunc = Dar_And( p, pFanin0, pFanin1 );
pData->pFunc = Dar_And( p, pFanin0, pFanin1 );
//printf( "Adding node %d for data %d\n", pData->pFunc->Id, pObj->Num );
return pData->pFunc;
}
/**Function*************************************************************
@ -654,10 +713,10 @@ Dar_Obj_t * Dar_LibBuildBest_rec( Dar_Man_t * p, Dar_LibObj_t * pObj )
***********************************************************************/
Dar_Obj_t * Dar_LibBuildBest( Dar_Man_t * p )
{
int i;
int i, Counter = 4;
for ( i = 0; i < 4; i++ )
s_DarLib->pDatas[i].pFunc = Vec_PtrEntry( p->vLeavesBest, i );
Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, p->OutBest) );
Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, p->OutBest), &Counter );
return Dar_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, p->OutBest) );
}

39
src/aig/dar/darMan.c
View File

@ -107,6 +107,13 @@ void Dar_ManStop( Dar_Man_t * p )
if ( p->vRequired ) Vec_IntFree( p->vRequired );
if ( p->vLeavesBest ) Vec_PtrFree( p->vLeavesBest );
free( p->pTable );
// free CNF mapping data
if ( p->pSopSizes )
{
free( p->pSopSizes );
free( p->pSops[1] );
free( p->pSops );
}
free( p );
}
@ -164,6 +171,38 @@ void Dar_ManPrintStats( Dar_Man_t * p )
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Stops the AIG manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_ManPrintRuntime( Dar_Man_t * p )
{
int i, Gain;
printf( "Good cuts = %d. Bad cuts = %d.\n", p->nCutsGood, p->nCutsBad );
PRT( "Cuts ", p->timeCuts );
PRT( "Eval ", p->timeEval );
PRT( "Other ", p->timeOther );
PRT( "TOTAL ", p->timeTotal );
Gain = p->nNodesInit - Dar_ManNodeNum(p);
for ( i = 0; i < 222; i++ )
{
if ( p->ClassGains[i] == 0 && p->ClassTimes[i] == 0 )
continue;
printf( "%3d : ", i );
printf( "G = %6d (%5.2f %%) ", p->ClassGains[i], Gain? 100.0*p->ClassGains[i]/Gain : 0.0 );
printf( "S = %8d (%5.2f %%) ", p->ClassSubgs[i], p->nTotalSubgs? 100.0*p->ClassSubgs[i]/p->nTotalSubgs : 0.0 );
printf( "R = %7d ", p->ClassGains[i]? p->ClassSubgs[i]/p->ClassGains[i] : 9999999 );
PRTP( "T", p->ClassTimes[i], p->timeEval );
}
}
////////////////////////////////////////////////////////////////////////

10
src/aig/dar/darObj.c
View File

@ -122,9 +122,15 @@ void Dar_ObjConnect( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pFan0, Dar_Obj
pObj->pFanin1 = pFan1;
// increment references of the fanins and add their fanouts
if ( pFan0 != NULL )
{
assert( Dar_ObjFanin0(pObj)->Type > 0 );
Dar_ObjRef( Dar_ObjFanin0(pObj) );
}
if ( pFan1 != NULL )
{
assert( Dar_ObjFanin1(pObj)->Type > 0 );
Dar_ObjRef( Dar_ObjFanin1(pObj) );
}
// set level and phase
if ( pFan1 != NULL )
{
@ -270,10 +276,12 @@ void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew, in
// the object cannot be the same
assert( pObjOld != pObjNewR );
// make sure object is not pointing to itself
// assert( pObjOld != Dar_ObjFanin0(pObjNewR) );
assert( pObjOld != Dar_ObjFanin0(pObjNewR) );
assert( pObjOld != Dar_ObjFanin1(pObjNewR) );
// recursively delete the old node - but leave the object there
pObjNewR->nRefs++;
Dar_ObjDelete_rec( p, pObjOld, 0 );
pObjNewR->nRefs--;
// if the new object is complemented or already used, create a buffer
p->nObjs[pObjOld->Type]--;
if ( Dar_IsComplement(pObjNew) || Dar_ObjRefs(pObjNew) > 0 || (fNodesOnly && !Dar_ObjIsNode(pObjNew)) )

94
src/aig/dar/darSeq.c
View File

@ -87,11 +87,13 @@ void Dar_ManDfsSeq_rec( Dar_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vNodes )
if ( Dar_ObjIsTravIdCurrent( p, pObj ) )
return;
Dar_ObjSetTravIdCurrent( p, pObj );
if ( Dar_ObjIsPi(pObj) )
if ( Dar_ObjIsPi(pObj) || Dar_ObjIsConst1(pObj) )
return;
Dar_ManDfsSeq_rec( p, Dar_ObjFanin0(pObj), vNodes );
Dar_ManDfsSeq_rec( p, Dar_ObjFanin1(pObj), vNodes );
Vec_PtrPush( vNodes, pObj );
// if ( (Dar_ObjFanin0(pObj) == NULL || Dar_ObjIsBuf(Dar_ObjFanin0(pObj))) &&
// (Dar_ObjFanin1(pObj) == NULL || Dar_ObjIsBuf(Dar_ObjFanin1(pObj))) )
Vec_PtrPush( vNodes, pObj );
}
/**Function*************************************************************
@ -218,8 +220,8 @@ Vec_Ptr_t * Dar_ManDfsUnreach( Dar_Man_t * p )
}
while ( k < i );
if ( Vec_PtrSize(vNodes) > 0 )
printf( "Found %d unreachable.\n", Vec_PtrSize(vNodes) );
// if ( Vec_PtrSize(vNodes) > 0 )
// printf( "Found %d unreachable.\n", Vec_PtrSize(vNodes) );
return vNodes;
/*
@ -278,31 +280,11 @@ int Dar_ManRemoveUnmarked( Dar_Man_t * p )
RetValue = Vec_PtrSize(vNodes);
Vec_PtrForEachEntry( vNodes, pObj, i )
Dar_ObjDelete( p, pObj );
printf( "Removes %d dangling.\n", Vec_PtrSize(vNodes) );
// printf( "Removed %d dangling.\n", Vec_PtrSize(vNodes) );
Vec_PtrFree( vNodes );
return RetValue;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Dar_Obj_t * Dar_ObjReal_rec( Dar_Obj_t * pObj )
{
Dar_Obj_t * pObjNew, * pObjR = Dar_Regular(pObj);
if ( !Dar_ObjIsBuf(pObjR) )
return pObj;
pObjNew = Dar_ObjReal_rec( Dar_ObjChild0(pObjR) );
return Dar_NotCond( pObjNew, Dar_IsComplement(pObj) );
}
/**Function*************************************************************
Synopsis [Rehashes the nodes.]
@ -317,11 +299,39 @@ static inline Dar_Obj_t * Dar_ObjReal_rec( Dar_Obj_t * pObj )
int Dar_ManSeqRehashOne( Dar_Man_t * p, Vec_Ptr_t * vNodes, Vec_Ptr_t * vUnreach )
{
Dar_Obj_t * pObj, * pObjNew, * pFanin0, * pFanin1;
int i, RetValue = 0;
int i, RetValue = 0, Counter = 0, Counter2 = 0;
// mark the unreachable nodes
Dar_ManIncrementTravId( p );
Vec_PtrForEachEntry( vUnreach, pObj, i )
Dar_ObjSetTravIdCurrent(p, pObj);
/*
// count the number of unreachable object connections
// that is the number of unreachable objects connected to main objects
Dar_ManForEachObj( p, pObj, i )
{
if ( Dar_ObjIsTravIdCurrent(p, pObj) )
continue;
pFanin0 = Dar_ObjFanin0(pObj);
if ( pFanin0 == NULL )
continue;
if ( Dar_ObjIsTravIdCurrent(p, pFanin0) )
pFanin0->fMarkA = 1;
pFanin1 = Dar_ObjFanin1(pObj);
if ( pFanin1 == NULL )
continue;
if ( Dar_ObjIsTravIdCurrent(p, pFanin1) )
pFanin1->fMarkA = 1;
}
// count the objects
Dar_ManForEachObj( p, pObj, i )
Counter2 += pObj->fMarkA, pObj->fMarkA = 0;
printf( "Connections = %d.\n", Counter2 );
*/
// go through the nodes while skipping unreachable
Vec_PtrForEachEntry( vNodes, pObj, i )
{
@ -345,6 +355,7 @@ int Dar_ManSeqRehashOne( Dar_Man_t * p, Vec_Ptr_t * vNodes, Vec_Ptr_t * vUnreach
pObjNew = Dar_Latch( p, pObjNew, 0 );
Dar_ObjReplace( p, pObj, pObjNew, 1 );
RetValue = 1;
Counter++;
continue;
}
if ( Dar_ObjIsNode(pObj) )
@ -356,9 +367,11 @@ int Dar_ManSeqRehashOne( Dar_Man_t * p, Vec_Ptr_t * vNodes, Vec_Ptr_t * vUnreach
pObjNew = Dar_And( p, pFanin0, pFanin1 );
Dar_ObjReplace( p, pObj, pObjNew, 1 );
RetValue = 1;
Counter++;
continue;
}
}
// printf( "Rehashings = %d.\n", Counter++ );
return RetValue;
}
@ -423,30 +436,42 @@ void Dar_ManRemoveBuffers( Dar_Man_t * p )
int Dar_ManSeqStrash( Dar_Man_t * p, int nLatches, int * pInits )
{
Vec_Ptr_t * vNodes, * vUnreach;
Dar_Obj_t * pObj;
int i;
int RetValue = 1;
// Dar_Obj_t * pObj, * pFanin;
// int i;
int Iter, RetValue = 1;
// create latches out of the additional PI/PO pairs
Dar_ManSeqStrashConvert( p, nLatches, pInits );
// iteratively rehash the network
while ( RetValue )
for ( Iter = 0; RetValue; Iter++ )
{
Dar_ManPrintStats( p );
// Dar_ManPrintStats( p );
/*
Dar_ManForEachObj( p, pObj, i )
{
assert( pObj->Type > 0 );
pFanin = Dar_ObjFanin0(pObj);
assert( pFanin == NULL || pFanin->Type > 0 );
pFanin = Dar_ObjFanin1(pObj);
assert( pFanin == NULL || pFanin->Type > 0 );
}
*/
// mark nodes unreachable from the PIs
vUnreach = Dar_ManDfsUnreach( p );
if ( Iter == 0 && Vec_PtrSize(vUnreach) > 0 )
printf( "Unreachable objects = %d.\n", Vec_PtrSize(vUnreach) );
// collect nodes reachable from the POs
vNodes = Dar_ManDfsSeq( p );
// remove nodes unreachable from the POs
Dar_ManRemoveUnmarked( p );
if ( Iter == 0 )
Dar_ManRemoveUnmarked( p );
// continue rehashing as long as there are changes
RetValue = Dar_ManSeqRehashOne( p, vNodes, vUnreach );
Vec_PtrFree( vNodes );
Vec_PtrFree( vUnreach );
}
// perform the final cleanup
Dar_ManIncrementTravId( p );
vNodes = Dar_ManDfsSeq( p );
@ -454,6 +479,7 @@ int Dar_ManSeqStrash( Dar_Man_t * p, int nLatches, int * pInits )
Vec_PtrFree( vNodes );
// remove buffers if they are left
// Dar_ManRemoveBuffers( p );
// clean up
if ( !Dar_ManCheck( p ) )
{

350
src/aig/dar/darTruth.c Normal file
View File

@ -0,0 +1,350 @@
/**CFile****************************************************************
FileName [darTruth.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [DAG-aware AIG rewriting.]
Synopsis [Computes the truth table of a cut.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - April 28, 2007.]
Revision [$Id: darTruth.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
#include "dar.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes truth table of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_ManCollectCut_rec( Dar_Man_t * p, Dar_Obj_t * pNode, Vec_Int_t * vNodes )
{
if ( pNode->fMarkA )
return;
pNode->fMarkA = 1;
assert( Dar_ObjIsAnd(pNode) || Dar_ObjIsExor(pNode) );
Dar_ManCollectCut_rec( p, Dar_ObjFanin0(pNode), vNodes );
Dar_ManCollectCut_rec( p, Dar_ObjFanin1(pNode), vNodes );
Vec_IntPush( vNodes, pNode->Id );
}
/**Function*************************************************************
Synopsis [Computes truth table of the cut.]
Description [Does not modify the array of leaves. Uses array vTruth to store
temporary truth tables. The returned pointer should be used immediately.]
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_ManCollectCut( Dar_Man_t * p, Dar_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
{
int i, Leaf;
// collect and mark the leaves
Vec_IntClear( vNodes );
Vec_IntForEachEntry( vLeaves, Leaf, i )
{
Vec_IntPush( vNodes, Leaf );
Dar_ManObj(p, Leaf)->fMarkA = 1;
}
// collect and mark the nodes
Dar_ManCollectCut_rec( p, pRoot, vNodes );
// clean the nodes
Vec_IntForEachEntry( vNodes, Leaf, i )
Dar_ManObj(p, Leaf)->fMarkA = 0;
}
/**Function*************************************************************
Synopsis [Returns the pointer to the truth table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Dar_ObjGetTruthStore( int ObjNum, Vec_Int_t * vTruth )
{
return ((unsigned *)Vec_IntArray(vTruth)) + 8 * ObjNum;
}
/**Function*************************************************************
Synopsis [Computes truth table of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_ManCutTruthOne( Dar_Man_t * p, Dar_Obj_t * pNode, Vec_Int_t * vTruth, int nWords )
{
unsigned * pTruth, * pTruth0, * pTruth1;
int i;
pTruth = Dar_ObjGetTruthStore( pNode->Level, vTruth );
pTruth0 = Dar_ObjGetTruthStore( Dar_ObjFanin0(pNode)->Level, vTruth );
pTruth1 = Dar_ObjGetTruthStore( Dar_ObjFanin1(pNode)->Level, vTruth );
if ( Dar_ObjIsExor(pNode) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = pTruth0[i] ^ pTruth1[i];
else if ( !Dar_ObjFaninC0(pNode) && !Dar_ObjFaninC1(pNode) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = pTruth0[i] & pTruth1[i];
else if ( !Dar_ObjFaninC0(pNode) && Dar_ObjFaninC1(pNode) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = pTruth0[i] & ~pTruth1[i];
else if ( Dar_ObjFaninC0(pNode) && !Dar_ObjFaninC1(pNode) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = ~pTruth0[i] & pTruth1[i];
else // if ( Dar_ObjFaninC0(pNode) && Dar_ObjFaninC1(pNode) )
for ( i = 0; i < nWords; i++ )
pTruth[i] = ~pTruth0[i] & ~pTruth1[i];
}
/**Function*************************************************************
Synopsis [Computes truth table of the cut.]
Description [Does not modify the array of leaves. Uses array vTruth to store
temporary truth tables. The returned pointer should be used immediately.]
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Dar_ManCutTruth( Dar_Man_t * p, Dar_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth )
{
static unsigned uTruths[8][8] = { // elementary truth tables
{ 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
{ 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
{ 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
{ 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
{ 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 },
{ 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF },
{ 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF },
{ 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF }
};
int i, Leaf;
// collect the cut
// Dar_ManCollectCut( p, pRoot, vLeaves, vNodes );
// set the node numbers
Vec_IntForEachEntry( vNodes, Leaf, i )
Dar_ManObj(p, Leaf)->Level = i;
// alloc enough memory
Vec_IntClear( vTruth );
Vec_IntGrow( vTruth, 8 * Vec_IntSize(vNodes) );
// set the elementary truth tables
Vec_IntForEachEntry( vLeaves, Leaf, i )
memcpy( Dar_ObjGetTruthStore(i, vTruth), uTruths[i], 8 * sizeof(unsigned) );
// compute truths for other nodes
Vec_IntForEachEntryStart( vNodes, Leaf, i, Vec_IntSize(vLeaves) )
Dar_ManCutTruthOne( p, Dar_ManObj(p, Leaf), vTruth, 8 );
return Dar_ObjGetTruthStore( pRoot->Level, vTruth );
}
static inline int Kit_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
static inline void Kit_TruthNot( unsigned * pOut, unsigned * pIn, int nVars )
{
int w;
for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = ~pIn[w];
}
/**Function*************************************************************
Synopsis [Computes the cost based on two ISOPs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dar_ManLargeCutEvalIsop( unsigned * pTruth, int nVars, Vec_Int_t * vMemory )
{
extern int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth );
int RetValue, nClauses;
// compute ISOP for the positive phase
RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 0 );
if ( RetValue == -1 )
return DAR_INFINITY;
assert( RetValue == 0 || RetValue == 1 );
nClauses = Vec_IntSize( vMemory );
// compute ISOP for the negative phase
Kit_TruthNot( pTruth, pTruth, nVars );
RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 0 );
if ( RetValue == -1 )
return DAR_INFINITY;
Kit_TruthNot( pTruth, pTruth, nVars );
assert( RetValue == 0 || RetValue == 1 );
nClauses += Vec_IntSize( vMemory );
return nClauses;
}
/**Function*************************************************************
Synopsis [Computes truth table of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_ManLargeCutCollect_rec( Dar_Man_t * p, Dar_Obj_t * pNode, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
{
if ( Dar_ObjIsTravIdCurrent(p, pNode) )
return;
if ( Dar_ObjIsTravIdPrevious(p, pNode) )
{
Vec_IntPush( vLeaves, pNode->Id );
// Vec_IntPush( vNodes, pNode->Id );
Dar_ObjSetTravIdCurrent( p, pNode );
return;
}
assert( Dar_ObjIsAnd(pNode) || Dar_ObjIsExor(pNode) );
Dar_ObjSetTravIdCurrent( p, pNode );
Dar_ManLargeCutCollect_rec( p, Dar_ObjFanin0(pNode), vLeaves, vNodes );
Dar_ManLargeCutCollect_rec( p, Dar_ObjFanin1(pNode), vLeaves, vNodes );
Vec_IntPush( vNodes, pNode->Id );
}
/**Function*************************************************************
Synopsis [Collect leaves and nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dar_ManLargeCutCollect( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCutR, Dar_Cut_t * pCutL, int Leaf,
Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
{
Vec_Int_t * vTemp;
Dar_Obj_t * pObj;
int Node, i;
Dar_ManIncrementTravId( p );
Dar_CutForEachLeaf( p, pCutR, pObj, i )
if ( pObj->Id != Leaf )
Dar_ObjSetTravIdCurrent( p, pObj );
Dar_CutForEachLeaf( p, pCutL, pObj, i )
Dar_ObjSetTravIdCurrent( p, pObj );
// collect the internal nodes and leaves
Dar_ManIncrementTravId( p );
vTemp = Vec_IntAlloc( 100 );
Dar_ManLargeCutCollect_rec( p, pRoot, vLeaves, vTemp );
Vec_IntForEachEntry( vLeaves, Node, i )
Vec_IntPush( vNodes, Node );
Vec_IntForEachEntry( vTemp, Node, i )
Vec_IntPush( vNodes, Node );
Vec_IntFree( vTemp );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dar_ManLargeCutEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCutR, Dar_Cut_t * pCutL, int Leaf )
{
Vec_Int_t * vLeaves, * vNodes, * vTruth, * vMemory;
unsigned * pTruth;
int RetValue;
// Dar_Obj_t * pObj;
vMemory = Vec_IntAlloc( 1 << 16 );
vTruth = Vec_IntAlloc( 1 << 16 );
vLeaves = Vec_IntAlloc( 100 );
vNodes = Vec_IntAlloc( 100 );
Dar_ManLargeCutCollect( p, pRoot, pCutR, pCutL, Leaf, vLeaves, vNodes );
/*
// collect the nodes
Dar_CutForEachLeaf( p, pCutR, pObj, i )
{
if ( pObj->Id == Leaf )
continue;
if ( pObj->fMarkA )
continue;
pObj->fMarkA = 1;
Vec_IntPush( vLeaves, pObj->Id );
Vec_IntPush( vNodes, pObj->Id );
}
Dar_CutForEachLeaf( p, pCutL, pObj, i )
{
if ( pObj->fMarkA )
continue;
pObj->fMarkA = 1;
Vec_IntPush( vLeaves, pObj->Id );
Vec_IntPush( vNodes, pObj->Id );
}
// collect and mark the nodes
Dar_ManCollectCut_rec( p, pRoot, vNodes );
// clean the nodes
Vec_IntForEachEntry( vNodes, Leaf, i )
Dar_ManObj(p, Leaf)->fMarkA = 0;
*/
pTruth = Dar_ManCutTruth( p, pRoot, vLeaves, vNodes, vTruth );
RetValue = Dar_ManLargeCutEvalIsop( pTruth, Vec_IntSize(vLeaves), vMemory );
Vec_IntFree( vLeaves );
Vec_IntFree( vNodes );
Vec_IntFree( vTruth );
Vec_IntFree( vMemory );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

40
src/aig/dar/darUtil.c
View File

@ -65,6 +65,26 @@ void Dar_ManIncrementTravId( Dar_Man_t * p )
p->nTravIds++;
}
/**Function*************************************************************
Synopsis [Collect the latches.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dar_ManLevels( Dar_Man_t * p )
{
Dar_Obj_t * pObj;
int i, LevelMax = 0;
Dar_ManForEachPo( p, pObj, i )
LevelMax = DAR_MAX( LevelMax, (int)Dar_ObjFanin0(pObj)->Level );
return LevelMax;
}
/**Function*************************************************************
Synopsis [Cleans the data pointers for the nodes.]
@ -316,6 +336,26 @@ Dar_Obj_t * Dar_ObjRecognizeMux( Dar_Obj_t * pNode, Dar_Obj_t ** ppNodeT, Dar_Ob
return NULL;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Dar_Obj_t * Dar_ObjReal_rec( Dar_Obj_t * pObj )
{
Dar_Obj_t * pObjNew, * pObjR = Dar_Regular(pObj);
if ( !Dar_ObjIsBuf(pObjR) )
return pObj;
pObjNew = Dar_ObjReal_rec( Dar_ObjChild0(pObjR) );
return Dar_NotCond( pObjNew, Dar_IsComplement(pObj) );
}
/**Function*************************************************************

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

@ -26,6 +26,7 @@
#include "fpga.h"
#include "if.h"
#include "res.h"
//#include "dar.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@ -330,7 +331,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
// Kit_TruthCountMintermsPrecomp();
// Kit_DsdPrecompute4Vars();
// Dar_LibStart();
Dar_LibStart();
}
/**Function*************************************************************
@ -346,7 +347,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
***********************************************************************/
void Abc_End()
{
// Dar_LibStop();
Dar_LibStop();
Abc_NtkFraigStoreClean();
// Rwt_Man4ExplorePrint();
@ -6048,7 +6049,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
*/
// Abc_Ntk4VarTable( pNtk );
// Dat_NtkGenerateArrays( pNtk );
// Dar_NtkGenerateArrays( pNtk );
// Dar_ManDeriveCnfTest2();
if ( !Abc_NtkIsStrash(pNtk) )
{
@ -7301,6 +7303,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
int fExdc;
int c;
int fPartition = 0;
extern void Abc_NtkFraigPartitionedTime( Abc_Ntk_t * pNtk, void * pParams );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@ -10535,6 +10538,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
char ** pArgvNew;
int nArgcNew;
int c;
int fRetime;
int fSat;
int fVerbose;
int nFrames;
@ -10544,6 +10548,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit, int nFrames );
extern int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose );
extern void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
pNtk = Abc_FrameReadNtk(pAbc);
@ -10551,6 +10556,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fRetime = 0; // verification after retiming
fSat = 0;
fVerbose = 0;
nFrames = 5;
@ -10558,7 +10564,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
nConfLimit = 10000;
nInsLimit = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FTCIsvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FTCIsrvh" ) ) != EOF )
{
switch ( c )
{
@ -10606,6 +10612,9 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nInsLimit < 0 )
goto usage;
break;
case 'r':
fRetime ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -10629,7 +10638,9 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
// perform equivalence checking
if ( fSat )
if ( fRetime )
Abc_NtkSecRetime( pNtk1, pNtk2 );
else if ( fSat )
Abc_NtkSecSat( pNtk1, pNtk2, nConfLimit, nInsLimit, nFrames );
else
Abc_NtkSecFraig( pNtk1, pNtk2, nSeconds, nFrames, fVerbose );
@ -10639,9 +10650,10 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: sec [-F num] [-T num] [-C num] [-I num] [-svh] <file1> <file2>\n" );
fprintf( pErr, "usage: sec [-F num] [-T num] [-C num] [-I num] [-srvh] <file1> <file2>\n" );
fprintf( pErr, "\t performs bounded sequential equivalence checking\n" );
fprintf( pErr, "\t-s : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
fprintf( pErr, "\t-r : toggles retiming verification [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );

76
src/base/abci/abcDar.c
View File

@ -53,7 +53,10 @@ Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk )
pObj->pCopy = (Abc_Obj_t *)Dar_ObjCreatePi(pMan);
// perform the conversion of the internal nodes (assumes DFS ordering)
Abc_NtkForEachNode( pNtk, pObj, i )
{
pObj->pCopy = (Abc_Obj_t *)Dar_And( pMan, (Dar_Obj_t *)Abc_ObjChild0Copy(pObj), (Dar_Obj_t *)Abc_ObjChild1Copy(pObj) );
// printf( "%d->%d ", pObj->Id, ((Dar_Obj_t *)pObj->pCopy)->Id );
}
// create the POs
Abc_NtkForEachCo( pNtk, pObj, i )
Dar_ObjCreatePo( pMan, (Dar_Obj_t *)Abc_ObjChild0Copy(pObj) );
@ -87,7 +90,10 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan )
// rebuild the AIG
vNodes = Dar_ManDfs( pMan );
Vec_PtrForEachEntry( vNodes, pObj, i )
pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Dar_ObjChild0Copy(pObj), (Abc_Obj_t *)Dar_ObjChild1Copy(pObj) );
if ( Dar_ObjIsBuf(pObj) )
pObj->pData = (Abc_Obj_t *)Dar_ObjChild0Copy(pObj);
else
pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Dar_ObjChild0Copy(pObj), (Abc_Obj_t *)Dar_ObjChild1Copy(pObj) );
Vec_PtrFree( vNodes );
// connect the PO nodes
Dar_ManForEachPo( pMan, pObj, i )
@ -193,6 +199,52 @@ int * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk )
return pArray;
}
/**Function*************************************************************
Synopsis [Performs verification after retiming.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
{
int fRemove1, fRemove2;
Dar_Man_t * pMan1, * pMan2;
int * pArray;
fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0, 0));
fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0, 0));
pMan1 = Abc_NtkToDar( pNtk1 );
pMan2 = Abc_NtkToDar( pNtk2 );
Dar_ManPrintStats( pMan1 );
Dar_ManPrintStats( pMan2 );
pArray = Abc_NtkGetLatchValues(pNtk1);
Dar_ManSeqStrash( pMan1, Abc_NtkLatchNum(pNtk1), pArray );
free( pArray );
pArray = Abc_NtkGetLatchValues(pNtk2);
Dar_ManSeqStrash( pMan2, Abc_NtkLatchNum(pNtk2), pArray );
free( pArray );
Dar_ManPrintStats( pMan1 );
Dar_ManPrintStats( pMan2 );
Dar_ManStop( pMan1 );
Dar_ManStop( pMan2 );
if ( fRemove1 ) Abc_NtkDelete( pNtk1 );
if ( fRemove2 ) Abc_NtkDelete( pNtk2 );
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
@ -208,7 +260,7 @@ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
{
Abc_Ntk_t * pNtkAig;
Dar_Man_t * pMan;//, * pTemp;
int * pArray;
// int * pArray;
assert( Abc_NtkIsStrash(pNtk) );
// convert to the AIG manager
@ -223,15 +275,29 @@ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
}
// perform balance
Dar_ManPrintStats( pMan );
/*
pArray = Abc_NtkGetLatchValues(pNtk);
Dar_ManSeqStrash( pMan, Abc_NtkLatchNum(pNtk), pArray );
free( pArray );
*/
// Dar_ManDumpBlif( pMan, "aig_temp.blif" );
// pMan->pPars = Dar_ManDefaultParams();
// Dar_ManRewrite( pMan );
Dar_ManRewrite( pMan );
Dar_ManPrintStats( pMan );
Dar_ManPrintRuntime( pMan );
// Dar_ManComputeCuts( pMan );
/*
{
extern Dar_Cnf_t * Dar_ManDeriveCnf( Dar_Man_t * p );
extern void Dar_CnfFree( Dar_Cnf_t * pCnf );
Dar_Cnf_t * pCnf;
pCnf = Dar_ManDeriveCnf( pMan );
Dar_CnfFree( pCnf );
}
*/
// convert from the AIG manager
if ( Dar_ManLatchNum(pMan) )
pNtkAig = Abc_NtkFromDarSeq( pNtk, pMan );
@ -250,6 +316,8 @@ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
return pNtkAig;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -131,7 +131,7 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p )
for ( i = 1; i < vTokens->nSize; i++ )
Io_ReadCreatePo( pNtk, vTokens->pArray[i] );
}
else
else
{
// check if the input/output names are given
if ( Abc_NtkPiNum(pNtk) == 0 )

11
src/opt/rwr/rwrEva.c
View File

@ -159,6 +159,17 @@ p->timeRes += clock() - clk;
if ( GainBest == -1 )
return -1;
/*
if ( GainBest > 0 )
{
printf( "Class %d ", p->pMap[uTruthBest] );
printf( "Gain = %d. Node %d : ", GainBest, pNode->Id );
Vec_PtrForEachEntry( p->vFanins, pFanin, i )
printf( "%d ", Abc_ObjRegular(pFanin)->Id );
Dec_GraphPrint( stdout, p->pGraph, NULL, NULL );
printf( "\n" );
}
*/
// printf( "%d", nNodesSaveCur - GainBest );
/*