Skip to content

A
abc
Commit ff6f0943 by Alan Mishchenko
Options

Version abc80314

parent 6205eaae
Showing with 522 additions and 136 deletions
abc.dsp
......@@ -194,6 +194,10 @@ SOURCE=.\src\base\abci\abcBalance.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcBidec.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcBmc.c
# End Source File
# Begin Source File
......
src/aig/bdc/bdcCore.c
......@@ -48,11 +48,11 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
p->pPars = pPars;
p->nWords = Kit_TruthWordNum( pPars->nVarsMax );
p->nDivsLimit = 200;
// memory
p->vMemory = Vec_IntStart( 1 << 16 );
// internal nodes
p->nNodesAlloc = 512;
p->pNodes = ALLOC( Bdc_Fun_t, p->nNodesAlloc );
// memory
p->vMemory = Vec_IntStart( 4 * p->nWords * p->nNodesAlloc );
// set up hash table
p->nTableSize = (1 << p->pPars->nVarsMax);
p->pTable = ALLOC( Bdc_Fun_t *, p->nTableSize );
......@@ -85,6 +85,18 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
***********************************************************************/
void Bdc_ManFree( Bdc_Man_t * p )
{
if ( p->pPars->fVerbose )
{
printf( "Bi-decomposition stats: Calls = %d. Nodes = %d. Reuse = %d.\n",
p->numCalls, p->numNodes, p->numReuse );
printf( "ANDs = %d. ORs = %d. Weak = %d. Muxes = %d. Memory = %.2f K\n",
p->numAnds, p->numOrs, p->numWeaks, p->numMuxes, 4.0 * Vec_IntSize(p->vMemory) / (1<<10) );
PRT( "Cache", p->timeCache );
PRT( "Check", p->timeCheck );
PRT( "Muxes", p->timeMuxes );
PRT( "Supps", p->timeSupps );
PRT( "TOTAL", p->timeTotal );
}
Vec_IntFree( p->vMemory );
Vec_IntFree( p->vSpots );
Vec_PtrFree( p->vTruths );
......@@ -118,7 +130,8 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
// add constant 1
pNode = Bdc_FunNew( p );
pNode->Type = BDC_TYPE_CONST1;
pNode->puFunc = NULL;
pNode->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords);
Kit_TruthFill( pNode->puFunc, p->nVars );
pNode->uSupp = 0;
Bdc_TableAdd( p, pNode );
// add variables
......@@ -192,6 +205,7 @@ void Bdc_ManDecPrint( Bdc_Man_t * p )
int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax )
{
Bdc_Isf_t Isf, * pIsf = &Isf;
int clk = clock();
assert( nVars <= p->pPars->nVarsMax );
// set current manager parameters
p->nVars = nVars;
......@@ -213,8 +227,14 @@ int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int n
Bdc_SuppMinimize( p, pIsf );
// call decomposition
p->pRoot = Bdc_ManDecompose_rec( p, pIsf );
p->timeTotal += clock() - clk;
p->numCalls++;
p->numNodes += p->nNodesNew;
if ( p->pRoot == NULL )
return -1;
if ( !Bdc_ManNodeVerify( p, pIsf, p->pRoot ) )
printf( "Bdc_ManDecompose(): Internal verification failed.\n" );
// assert( Bdc_ManNodeVerify( p, pIsf, p->pRoot ) );
return p->nNodesNew;
}
......
src/aig/bdc/bdcDec.c
......@@ -30,6 +30,82 @@
/**Function*************************************************************
Synopsis [Minimizes the support of the ISF.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bdc_SuppMinimize2( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
{
int v, clk;
if ( p->pPars->fVerbose )
clk = clock();
// compute support
pIsf->uSupp = Kit_TruthSupport( pIsf->puOn, p->nVars ) |
Kit_TruthSupport( pIsf->puOff, p->nVars );
// go through the support variables
for ( v = 0; v < p->nVars; v++ )
{
if ( (pIsf->uSupp & (1 << v)) == 0 )
continue;
Kit_TruthExistNew( p->puTemp1, pIsf->puOn, p->nVars, v );
Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, v );
if ( !Kit_TruthIsDisjoint( p->puTemp1, p->puTemp2, p->nVars ) )
continue;
// if ( !Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) )
// continue;
// remove the variable
Kit_TruthCopy( pIsf->puOn, p->puTemp1, p->nVars );
Kit_TruthCopy( pIsf->puOff, p->puTemp2, p->nVars );
// Kit_TruthExist( pIsf->puOn, p->nVars, v );
// Kit_TruthExist( pIsf->puOff, p->nVars, v );
pIsf->uSupp &= ~(1 << v);
}
if ( p->pPars->fVerbose )
p->timeSupps += clock() - clk;
}
/**Function*************************************************************
Synopsis [Minimizes the support of the ISF.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
{
int v, clk;
if ( p->pPars->fVerbose )
clk = clock();
// go through the support variables
pIsf->uSupp = 0;
for ( v = 0; v < p->nVars; v++ )
{
if ( !Kit_TruthVarInSupport( pIsf->puOn, p->nVars, v ) &&
!Kit_TruthVarInSupport( pIsf->puOff, p->nVars, v ) )
continue;
if ( Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) )
{
Kit_TruthExist( pIsf->puOn, p->nVars, v );
Kit_TruthExist( pIsf->puOff, p->nVars, v );
continue;
}
pIsf->uSupp |= (1 << v);
}
if ( p->pPars->fVerbose )
p->timeSupps += clock() - clk;
}
/**Function*************************************************************
Synopsis [Updates the ISF of the right after the left was decompoosed.]
Description []
......@@ -418,12 +494,16 @@ Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL
// check if there is any reuse for the components
if ( WeightOrL + WeightOrR > WeightAndL + WeightAndR )
{
p->numReuse++;
p->numOrs++;
Bdc_IsfCopy( pIsfL, p->pIsfOL );
Bdc_IsfCopy( pIsfR, p->pIsfOR );
return BDC_TYPE_OR;
}
if ( WeightOrL + WeightOrR < WeightAndL + WeightAndR )
{
p->numReuse++;
p->numAnds++;
Bdc_IsfCopy( pIsfL, p->pIsfAL );
Bdc_IsfCopy( pIsfR, p->pIsfAR );
return BDC_TYPE_AND;
......@@ -432,10 +512,16 @@ Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL
// compare the two-component costs
if ( WeightOr > WeightAnd )
{
if ( WeightOr < BDC_SCALE )
p->numWeaks++;
p->numOrs++;
Bdc_IsfCopy( pIsfL, p->pIsfOL );
Bdc_IsfCopy( pIsfR, p->pIsfOR );
return BDC_TYPE_OR;
}
if ( WeightAnd < BDC_SCALE )
p->numWeaks++;
p->numAnds++;
Bdc_IsfCopy( pIsfL, p->pIsfAL );
Bdc_IsfCopy( pIsfR, p->pIsfAR );
return BDC_TYPE_AND;
......@@ -456,6 +542,9 @@ int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bd
{
int Var, VarMin, nSuppMin, nSuppCur;
unsigned uSupp0, uSupp1;
int clk;
if ( p->pPars->fVerbose )
clk = clock();
VarMin = -1;
nSuppMin = 1000;
for ( Var = 0; Var < p->nVars; Var++ )
......@@ -473,7 +562,7 @@ int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bd
{
nSuppMin = nSuppCur;
VarMin = Var;
// break;
break;
}
}
if ( VarMin >= 0 )
......@@ -485,6 +574,8 @@ int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bd
Bdc_SuppMinimize( p, pIsfL );
Bdc_SuppMinimize( p, pIsfR );
}
if ( p->pPars->fVerbose )
p->timeMuxes += clock() - clk;
return VarMin;
}
......@@ -582,6 +673,7 @@ Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
Bdc_Fun_t * pFunc, * pFunc0, * pFunc1;
Bdc_Isf_t IsfL, * pIsfL = &IsfL;
Bdc_Isf_t IsfB, * pIsfR = &IsfB;
int iVar, clk;
/*
printf( "Init function (%d):\n", LocalCounter );
Extra_PrintBinary( stdout, pIsf->puOn, 1<<4 );printf("\n");
......@@ -589,13 +681,27 @@ Extra_PrintBinary( stdout, pIsf->puOff, 1<<4 );printf("\n");
*/
// check computed results
assert( Kit_TruthIsDisjoint(pIsf->puOn, pIsf->puOff, p->nVars) );
if ( pFunc = Bdc_TableLookup( p, pIsf ) )
if ( p->pPars->fVerbose )
clk = clock();
pFunc = Bdc_TableLookup( p, pIsf );
if ( p->pPars->fVerbose )
p->timeCache += clock() - clk;
if ( pFunc )
return pFunc;
// decide on the decomposition type
if ( p->pPars->fVerbose )
clk = clock();
Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR );
if ( p->pPars->fVerbose )
p->timeCheck += clock() - clk;
if ( Type == BDC_TYPE_MUX )
{
int iVar = Bdc_DecomposeStepMux( p, pIsf, pIsfL, pIsfR );
if ( p->pPars->fVerbose )
clk = clock();
iVar = Bdc_DecomposeStepMux( p, pIsf, pIsfL, pIsfR );
if ( p->pPars->fVerbose )
p->timeMuxes += clock() - clk;
p->numMuxes++;
pFunc0 = Bdc_ManDecompose_rec( p, pIsfL );
pFunc1 = Bdc_ManDecompose_rec( p, pIsfR );
if ( pFunc0 == NULL || pFunc1 == NULL )
......@@ -625,9 +731,6 @@ Extra_PrintBinary( stdout, pIsf->puOff, 1<<4 );printf("\n");
// create new gate
pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, Type );
}
if ( pFunc == NULL )
return NULL;
assert( Bdc_ManNodeVerify( p, pIsf, pFunc ) );
return pFunc;
}
......
src/aig/bdc/bdcInt.h
......@@ -106,6 +106,20 @@ struct Bdc_Man_t_
Bdc_Isf_t * pIsfAR, IsfAR;
// internal memory manager
Vec_Int_t * vMemory; // memory for internal truth tables
// statistics
int numCalls;
int numNodes;
int numMuxes;
int numAnds;
int numOrs;
int numWeaks;
int numReuse;
// runtime
int timeCache;
int timeCheck;
int timeMuxes;
int timeSupps;
int timeTotal;
};
// working with complemented attributes of objects
......@@ -132,11 +146,12 @@ static inline void Bdc_IsfNot( Bdc_Isf_t * p ) { unsign
/*=== bdcDec.c ==========================================================*/
extern Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
extern void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
extern int Bdc_ManNodeVerify( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Fun_t * pFunc );
/*=== bdcTable.c ==========================================================*/
extern Bdc_Fun_t * Bdc_TableLookup( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
extern void Bdc_TableAdd( Bdc_Man_t * p, Bdc_Fun_t * pFunc );
extern void Bdc_TableClear( Bdc_Man_t * p );
extern void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
extern int Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTruth );
#ifdef __cplusplus
......
src/aig/bdc/bdcTable.c
......@@ -30,39 +30,6 @@
/**Function*************************************************************
Synopsis [Minimizes the support of the ISF.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
{
int v;
// compute support
pIsf->uSupp = Kit_TruthSupport( pIsf->puOn, p->nVars ) |
Kit_TruthSupport( pIsf->puOff, p->nVars );
// go through the support variables
for ( v = 0; v < p->nVars; v++ )
{
if ( (pIsf->uSupp & (1 << v)) == 0 )
continue;
Kit_TruthExistNew( p->puTemp1, pIsf->puOn, p->nVars, v );
Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, v );
if ( !Kit_TruthIsDisjoint( p->puTemp1, p->puTemp2, p->nVars ) )
continue;
// remove the variable
Kit_TruthCopy( pIsf->puOn, p->puTemp1, p->nVars );
Kit_TruthCopy( pIsf->puOff, p->puTemp2, p->nVars );
pIsf->uSupp &= ~(1 << v);
}
}
/**Function*************************************************************
Synopsis [Checks containment of the function in the ISF.]
Description []
......
src/aig/dar/darRefact.c
......@@ -21,6 +21,9 @@
#include "darInt.h"
#include "kit.h"
#include "bdc.h"
#include "bdcInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
......@@ -44,6 +47,9 @@ struct Ref_Man_t_
Kit_Graph_t * pGraphBest; // the best factored form
int GainBest; // the best gain
int LevelBest; // the level of node with the best gain
// bi-decomposition
Bdc_Par_t DecPars; // decomposition parameters
Bdc_Man_t * pManDec; // decomposition manager
// node statistics
int nNodesInit; // the initial number of nodes
int nNodesTried; // the number of nodes tried
......@@ -111,6 +117,11 @@ Ref_Man_t * Dar_ManRefStart( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
p->vMemory = Vec_IntAlloc( 1 << 16 );
p->vCutNodes = Vec_PtrAlloc( 256 );
p->vLeavesBest = Vec_PtrAlloc( pPars->nLeafMax );
// alloc bi-decomposition manager
p->DecPars.nVarsMax = pPars->nLeafMax;
p->DecPars.fVerbose = pPars->fVerbose;
p->DecPars.fVeryVerbose = 0;
// p->pManDec = Bdc_ManAlloc( &p->DecPars );
return p;
}
......@@ -151,6 +162,8 @@ void Dar_ManRefPrintStats( Ref_Man_t * p )
***********************************************************************/
void Dar_ManRefStop( Ref_Man_t * p )
{
if ( p->pManDec )
Bdc_ManFree( p->pManDec );
if ( p->pPars->fVerbose )
Dar_ManRefPrintStats( p );
Vec_VecFree( p->vCuts );
......@@ -381,6 +394,13 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
if ( RetValue > -1 )
{
pGraphCur = Kit_SopFactor( p->vMemory, 0, Vec_PtrSize(vCut), p->vMemory );
/*
{
int RetValue;
RetValue = Bdc_ManDecompose( p->pManDec, pTruth, NULL, Vec_PtrSize(vCut), NULL, 1000 );
printf( "Graph = %d. Bidec = %d.\n", Kit_GraphNodeNum(pGraphCur), RetValue );
}
*/
nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required );
if ( nNodesAdded > -1 )
{
......@@ -403,9 +423,17 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
// try negative phase
Kit_TruthNot( pTruth, pTruth, Vec_PtrSize(vCut) );
RetValue = Kit_TruthIsop( pTruth, Vec_PtrSize(vCut), p->vMemory, 0 );
// Kit_TruthNot( pTruth, pTruth, Vec_PtrSize(vCut) );
if ( RetValue > -1 )
{
pGraphCur = Kit_SopFactor( p->vMemory, 1, Vec_PtrSize(vCut), p->vMemory );
/*
{
int RetValue;
RetValue = Bdc_ManDecompose( p->pManDec, pTruth, NULL, Vec_PtrSize(vCut), NULL, 1000 );
printf( "Graph = %d. Bidec = %d.\n", Kit_GraphNodeNum(pGraphCur), RetValue );
}
*/
nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required );
if ( nNodesAdded > -1 )
{
......@@ -426,6 +454,7 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
Kit_GraphFree( pGraphCur );
}
}
return p->GainBest;
}
......
src/aig/kit/kit.h
......@@ -564,6 +564,7 @@ extern void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVa
extern void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthCofactor0New( unsigned * pOut, unsigned * pIn, int nVars, int iVar );
extern void Kit_TruthCofactor1New( unsigned * pOut, unsigned * pIn, int nVars, int iVar );
extern int Kit_TruthVarIsVacuous( unsigned * pOnset, unsigned * pOffset, int nVars, int iVar );
extern void Kit_TruthExist( unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthExistNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthExistSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
......
src/aig/kit/kitTruth.c
......@@ -520,6 +520,64 @@ void Kit_TruthCofactor1New( unsigned * pOut, unsigned * pIn, int nVars, int iVar
}
}
/**Function*************************************************************
Synopsis [Computes negative cofactor of the function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_TruthVarIsVacuous( unsigned * pOnset, unsigned * pOffset, int nVars, int iVar )
{
int nWords = Kit_TruthWordNum( nVars );
int i, k, Step;
assert( iVar < nVars );
switch ( iVar )
{
case 0:
for ( i = 0; i < nWords; i++ )
if ( ((pOnset[i] & (pOffset[i] >> 1)) | (pOffset[i] & (pOnset[i] >> 1))) & 0x55555555 )
return 0;
return 1;
case 1:
for ( i = 0; i < nWords; i++ )
if ( ((pOnset[i] & (pOffset[i] >> 2)) | (pOffset[i] & (pOnset[i] >> 2))) & 0x33333333 )
return 0;
return 1;
case 2:
for ( i = 0; i < nWords; i++ )
if ( ((pOnset[i] & (pOffset[i] >> 4)) | (pOffset[i] & (pOnset[i] >> 4))) & 0x0F0F0F0F )
return 0;
return 1;
case 3:
for ( i = 0; i < nWords; i++ )
if ( ((pOnset[i] & (pOffset[i] >> 8)) | (pOffset[i] & (pOnset[i] >> 8))) & 0x00FF00FF )
return 0;
return 1;
case 4:
for ( i = 0; i < nWords; i++ )
if ( ((pOnset[i] & (pOffset[i] >> 16)) || (pOffset[i] & (pOnset[i] >> 16))) & 0x0000FFFF )
return 0;
return 1;
default:
Step = (1 << (iVar - 5));
for ( k = 0; k < nWords; k += 2*Step )
{
for ( i = 0; i < Step; i++ )
if ( (pOnset[i] & pOffset[Step+i]) | (pOffset[i] & pOnset[Step+i]) )
return 0;
pOnset += 2*Step;
pOffset += 2*Step;
}
return 1;
}
}
/**Function*************************************************************
......
src/base/abci/abc.c
......@@ -93,6 +93,7 @@ static int Abc_CommandSop ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandBdd ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandReorder ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBidec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandOrder ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMuxes ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -275,6 +276,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "bdd", Abc_CommandBdd, 0 );
Cmd_CommandAdd( pAbc, "Various", "aig", Abc_CommandAig, 0 );
Cmd_CommandAdd( pAbc, "Various", "reorder", Abc_CommandReorder, 0 );
Cmd_CommandAdd( pAbc, "Various", "bidec", Abc_CommandBidec, 1 );
Cmd_CommandAdd( pAbc, "Various", "order", Abc_CommandOrder, 0 );
Cmd_CommandAdd( pAbc, "Various", "muxes", Abc_CommandMuxes, 1 );
Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 );
......@@ -5202,6 +5204,69 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandBidec( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int c;
int fVerbose;
extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
// get the new network
if ( !Abc_NtkIsAigLogic(pNtk) )
{
fprintf( pErr, "Bi-decomposition only works when node functions are AIGs (run \"aig\").\n" );
return 1;
}
Abc_NtkBidecResyn( pNtk, fVerbose );
return 0;
usage:
fprintf( pErr, "usage: bidec [-vh]\n" );
fprintf( pErr, "\t applies bi-decomposition to local functions of the nodes\n" );
fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandOrder( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr, * pFile;
......
src/base/abci/abcBidec.c 0 → 100644
/**CFile****************************************************************
FileName [abcBidec.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Interface to bi-decomposition.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abcBidec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
#include "bdc.h"
#include "bdcInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj ) { return Hop_NotCond( Bdc_Regular(pObj)->pCopy, Bdc_IsComplement(pObj) ); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Resynthesizes nodes using bi-decomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare )
{
unsigned * pTruth;
Bdc_Fun_t * pFunc;
int i;
assert( nVars <= 16 );
// derive truth table
pTruth = Abc_ConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 );
if ( Hop_IsComplement(pRoot) )
Extra_TruthNot( pTruth, pTruth, nVars );
// decompose truth table
Bdc_ManDecompose( p, pTruth, puCare, nVars, NULL, 1000 );
// convert back into HOP
Bdc_FunWithId( p, 0 )->pCopy = Hop_ManConst1( pHop );
for ( i = 0; i < nVars; i++ )
Bdc_FunWithId( p, i+1 )->pCopy = Hop_ManPi( pHop, i );
for ( i = nVars + 1; i < p->nNodes; i++ )
{
pFunc = Bdc_FunWithId( p, i );
pFunc->pCopy = Hop_And( pHop, Bdc_FunCopyHop(pFunc->pFan0), Bdc_FunCopyHop(pFunc->pFan1) );
}
return Bdc_FunCopyHop(p->pRoot);
}
/**Function*************************************************************
Synopsis [Resynthesizes nodes using bi-decomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose )
{
Bdc_Par_t Pars = {0}, * pPars = &Pars;
Bdc_Man_t * p;
Abc_Obj_t * pObj;
Vec_Int_t * vTruth;
int i, nGainTotal = 0, nNodes1, nNodes2;
int clk = clock();
assert( Abc_NtkIsLogic(pNtk) );
if ( !Abc_NtkToAig(pNtk) )
return;
pPars->nVarsMax = Abc_NtkGetFaninMax( pNtk );
pPars->fVerbose = fVerbose;
if ( pPars->nVarsMax > 15 )
{
if ( fVerbose )
printf( "Resynthesis is not performed for nodes with more than 15 inputs.\n" );
pPars->nVarsMax = 15;
}
vTruth = Vec_IntAlloc( 0 );
p = Bdc_ManAlloc( pPars );
Abc_NtkForEachNode( pNtk, pObj, i )
{
if ( Abc_ObjFaninNum(pObj) > 15 )
continue;
nNodes1 = Hop_DagSize(pObj->pData);
pObj->pData = Abc_NodeIfNodeResyn( p, pNtk->pManFunc, pObj->pData, Abc_ObjFaninNum(pObj), vTruth, NULL );
nNodes2 = Hop_DagSize(pObj->pData);
nGainTotal += nNodes1 - nNodes2;
}
Bdc_ManFree( p );
Vec_IntFree( vTruth );
if ( fVerbose )
{
printf( "Total gain in AIG nodes = %d. ", nGainTotal );
PRT( "Total runtime", clock() - clk );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/base/abci/abcIf.c
......@@ -34,7 +34,7 @@ static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_O
static Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk );
extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose );
extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk );
extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
......@@ -86,7 +86,7 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
return NULL;
If_ManStop( pIfMan );
if ( pPars->fBidec && pPars->nLutSize <= 8 )
Abc_NtkBidecResyn( pNtkNew );
Abc_NtkBidecResyn( pNtkNew, 0 );
// duplicate EXDC
if ( pNtk->pExdc )
......@@ -256,7 +256,7 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
pNodeNew = Abc_NtkCreateNode( pNtkNew );
pCutBest = If_ObjCutBest( pIfObj );
// if ( pIfMan->pPars->pLutLib && pIfMan->pPars->pLutLib->fVarPinDelays )
// If_CutRotatePins( pIfMan, pCutBest );
If_CutRotatePins( pIfMan, pCutBest );
if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
{
If_CutForEachLeafReverse( pIfMan, pCutBest, pIfLeaf, i )
......@@ -551,86 +551,6 @@ Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk )
}
#include "bdc.h"
#include "bdcInt.h"
static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj ) { return Hop_NotCond( Bdc_Regular(pObj)->pCopy, Bdc_IsComplement(pObj) ); }
/**Function*************************************************************
Synopsis [Resynthesizes nodes using bi-decomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth )
{
unsigned * pTruth;
Bdc_Fun_t * pFunc;
int i;
// derive truth table
pTruth = Abc_ConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 );
if ( Hop_IsComplement(pRoot) )
Extra_TruthNot( pTruth, pTruth, nVars );
// decompose truth table
Bdc_ManDecompose( p, pTruth, NULL, nVars, NULL, 1000 );
// convert back into HOP
Bdc_FunWithId( p, 0 )->pCopy = Hop_ManConst1( pHop );
for ( i = 0; i < nVars; i++ )
Bdc_FunWithId( p, i+1 )->pCopy = Hop_ManPi( pHop, i );
for ( i = nVars + 1; i < p->nNodes; i++ )
{
pFunc = Bdc_FunWithId( p, i );
pFunc->pCopy = Hop_And( pHop, Bdc_FunCopyHop(pFunc->pFan0), Bdc_FunCopyHop(pFunc->pFan1) );
}
return Bdc_FunCopyHop(p->pRoot);
}
/**Function*************************************************************
Synopsis [Resynthesizes nodes using bi-decomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk )
{
Bdc_Par_t Pars = {0}, * pPars = &Pars;
Bdc_Man_t * p;
Abc_Obj_t * pObj;
Vec_Int_t * vTruth;
int i, nGainTotal = 0, nNodes1, nNodes2;
int clk = clock();
pPars->nVarsMax = Abc_NtkGetFaninMax( pNtk );
if ( pPars->nVarsMax > 8 )
{
printf( "Resynthesis is not performed.\n" );
return;
}
vTruth = Vec_IntAlloc( 0 );
p = Bdc_ManAlloc( pPars );
Abc_NtkForEachNode( pNtk, pObj, i )
{
nNodes1 = Hop_DagSize(pObj->pData);
pObj->pData = Abc_NodeIfNodeResyn( p, pNtk->pManFunc, pObj->pData, Abc_ObjFaninNum(pObj), vTruth );
nNodes2 = Hop_DagSize(pObj->pData);
nGainTotal += nNodes1 - nNodes2;
}
// printf( "LUTs = %d. Total gain in AIG nodes = %d. ", Abc_NtkNodeNum(pNtk), nGainTotal );
// PRT( "Time", clock() - clk );
Bdc_ManFree( p );
Vec_IntFree( vTruth );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
......
src/base/abci/module.make
......@@ -2,6 +2,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcAttach.c \
src/base/abci/abcAuto.c \
src/base/abci/abcBalance.c \
src/base/abci/abcBidec.c \
src/base/abci/abcBmc.c \
src/base/abci/abcCas.c \
src/base/abci/abcClpBdd.c \
......
src/map/if/ifTime.c
......@@ -238,7 +238,7 @@ void If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut )
float PinDelays[32];
// int PinPerm[32];
int i;
assert( p->pPars->pLutLib && p->pPars->pLutLib->fVarPinDelays && p->pPars->fTruth );
// assert( p->pPars->pLutLib && p->pPars->pLutLib->fVarPinDelays && p->pPars->fTruth );
If_CutForEachLeaf( p, pCut, pLeaf, i )
PinDelays[i] = If_ObjCutBest(pLeaf)->Delay;
If_CutTruthPermute( p->puTemp[0], If_CutTruth(pCut), If_CutLeaveNum(pCut), PinDelays, If_CutLeaves(pCut) );
......
src/map/if/ifTruth.c
......@@ -146,16 +146,18 @@ void If_CutTruthPermute( unsigned * pOut, unsigned * pIn, int nVars, float * pDe
for ( i = 0; i < nVars - 1; i++ )
{
if ( pDelays[i] >= pDelays[i+1] )
// if ( pDelays[i] <= pDelays[i+1] )
continue;
tTemp = pDelays[i]; pDelays[i] = pDelays[i+1]; pDelays[i+1] = tTemp;
Temp = pVars[i]; pVars[i] = pVars[i+1]; pVars[i+1] = Temp;
if ( pOut && pIn )
If_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
pTemp = pOut; pOut = pIn; pIn = pTemp;
fChange = 1;
Counter++;
}
}
if ( Counter & 1 )
if ( pOut && pIn && (Counter & 1) )
If_TruthCopy( pOut, pIn, nVars );
}
......
src/opt/lpk/lpkCore.c
......@@ -500,6 +500,7 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
Lpk_Man_t * p;
Abc_Obj_t * pObj;
double Delta;
// int * pnFanouts, nObjMax;
int i, Iter, nNodes, nNodesPrev, clk = clock();
assert( Abc_NtkIsLogic(pNtk) );
......@@ -554,6 +555,14 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
p->nTotalNodes = Abc_NtkNodeNum(pNtk);
}
/*
// save the number of fanouts of all objects
nObjMax = Abc_NtkObjNumMax( pNtk );
pnFanouts = ALLOC( int, nObjMax );
memset( pnFanouts, 0, sizeof(int) * nObjMax );
Abc_NtkForEachObj( pNtk, pObj, i )
pnFanouts[pObj->Id] = Abc_ObjFanoutNum(pObj);
*/
// iterate over the network
nNodesPrev = p->nNodesTotal;
......@@ -604,6 +613,18 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
break;
}
Abc_NtkStopReverseLevels( pNtk );
/*
// report the fanout changes
Abc_NtkForEachObj( pNtk, pObj, i )
{
if ( i >= nObjMax )
continue;
if ( Abc_ObjFanoutNum(pObj) - pnFanouts[pObj->Id] == 0 )
continue;
printf( "%d ", Abc_ObjFanoutNum(pObj) - pnFanouts[pObj->Id] );
}
printf( "\n" );
*/
if ( pPars->fVerbose )
{
......
src/opt/mfs/mfsCore.c
......@@ -100,7 +100,10 @@ p->timeSat += clock() - clk;
***********************************************************************/
int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
int clk;
Hop_Obj_t * pObj;
extern Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare );
int nGain, clk;
p->nNodesTried++;
// prepare data structure for this node
Mfs_ManClean( p );
......@@ -128,6 +131,16 @@ clk = clock();
// solve the SAT problem
Abc_NtkMfsSolveSat( p, pNode );
p->timeSat += clock() - clk;
// minimize the local function of the node using bi-decomposition
assert( p->nFanins == Abc_ObjFaninNum(pNode) );
pObj = Abc_NodeIfNodeResyn( p->pManDec, pNode->pNtk->pManFunc, pNode->pData, p->nFanins, p->vTruth, p->uCare );
nGain = Hop_DagSize(pNode->pData) - Hop_DagSize(pObj);
if ( nGain >= 0 )
{
p->nNodesDec++;
p->nNodesGained += nGain;
pNode->pData = pObj;
}
return 1;
}
......@@ -146,6 +159,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
{
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters );
Bdc_Par_t Pars = {0}, * pDecPars = &Pars;
ProgressBar * pProgress;
Mfs_Man_t * p;
Abc_Obj_t * pObj;
......@@ -157,8 +171,8 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
nFaninMax = Abc_NtkGetFaninMax(pNtk);
if ( nFaninMax > MFS_FANIN_MAX )
{
printf( "Some nodes have more than %d fanins. Quitting.\n", MFS_FANIN_MAX );
return 1;
printf( "Nodes with more than %d fanins will node be processed.\n", MFS_FANIN_MAX );
nFaninMax = MFS_FANIN_MAX;
}
// perform the network sweep
Abc_NtkSweep( pNtk, 0 );
......@@ -186,11 +200,16 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
{
if ( p->pCare != NULL )
printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) );
else
printf( "Performing optimization without constraints.\n" );
// else
// printf( "Performing optimization without constraints.\n" );
}
if ( !pPars->fResub )
printf( "Currently don't-cares are not used but the stats are printed.\n" );
{
pDecPars->nVarsMax = nFaninMax;
pDecPars->fVerbose = pPars->fVerbose;
p->vTruth = Vec_IntAlloc( 0 );
p->pManDec = Bdc_ManAlloc( pDecPars );
}
// label the register outputs
if ( p->pCare )
......@@ -211,15 +230,26 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
{
if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
continue;
if ( Abc_ObjFaninNum(pObj) > MFS_FANIN_MAX )
continue;
if ( !p->pPars->fVeryVerbose )
Extra_ProgressBarUpdate( pProgress, i, NULL );
if ( pPars->fResub )
Abc_NtkMfsResub( p, pObj );
else
else if ( Abc_ObjFaninNum(pObj) > 1 && Abc_ObjFaninNum(pObj) <= 12 )
Abc_NtkMfsNode( p, pObj );
}
Extra_ProgressBarStop( pProgress );
Abc_NtkStopReverseLevels( pNtk );
// perform the sweeping
if ( !pPars->fResub )
{
extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose );
Abc_NtkSweep( pNtk, 0 );
Abc_NtkBidecResyn( pNtk, 0 );
}
p->nTotalNodesEnd = Abc_NtkNodeNum(pNtk);
p->nTotalEdgesEnd = Abc_NtkGetTotalFanins(pNtk);
......
src/opt/mfs/mfsInt.h
......@@ -35,12 +35,13 @@ extern "C" {
#include "cnf.h"
#include "satSolver.h"
#include "satStore.h"
#include "bdc.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
#define MFS_FANIN_MAX 10
#define MFS_FANIN_MAX 12
typedef struct Mfs_Man_t_ Mfs_Man_t;
struct Mfs_Man_t_
......@@ -64,6 +65,11 @@ struct Mfs_Man_t_
int nCexes; // the numbe rof current counter-examples
int nSatCalls;
int nSatCexes;
// used for bidecomposition
Vec_Int_t * vTruth;
Bdc_Man_t * pManDec;
int nNodesDec;
int nNodesGained;
// solving data
Aig_Man_t * pAigWin; // window AIG with constraints
Cnf_Dat_t * pCnf; // the CNF for the window
......
src/opt/mfs/mfsMan.c
......@@ -131,6 +131,8 @@ void Mfs_ManPrint( Mfs_Man_t * p )
1.0 * (p->nMintsTotal-p->nMintsCare) / p->nMintsTotal );
// printf( "Average ratio of sequential DCs in the global space = %5.2f.\n",
// 1.0-(p->dTotalRatios/p->nNodesTried) );
printf( "Nodes resyn = %d. Ratio = %5.2f. Total AIG node gain = %d.\n",
p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained );
}
/*
PRTP( "Win", p->timeWin , p->timeTotal );
......@@ -158,6 +160,10 @@ void Mfs_ManStop( Mfs_Man_t * p )
{
if ( p->pPars->fVerbose )
Mfs_ManPrint( p );
if ( p->vTruth )
Vec_IntFree( p->vTruth );
if ( p->pManDec )
Bdc_ManFree( p->pManDec );
if ( p->pCare )
Aig_ManStop( p->pCare );
if ( p->vSuppsInv )
......
src/opt/mfs/mfsSat.c
......@@ -110,6 +110,18 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
Extra_PrintBinary( stdout, p->uCare, (1<<p->nFanins) );
printf( "\n" );
}
// map the care
if ( p->nFanins > 4 )
return;
if ( p->nFanins == 4 )
p->uCare[0] = p->uCare[0] | (p->uCare[0] << 16);
if ( p->nFanins == 3 )
p->uCare[0] = p->uCare[0] | (p->uCare[0] << 8) | (p->uCare[0] << 16) | (p->uCare[0] << 24);
if ( p->nFanins == 2 )
p->uCare[0] = p->uCare[0] | (p->uCare[0] << 4) | (p->uCare[0] << 8) | (p->uCare[0] << 12) |
(p->uCare[0] << 16) | (p->uCare[0] << 20) | (p->uCare[0] << 24) | (p->uCare[0] << 28);
assert( p->nFanins != 1 );
}
////////////////////////////////////////////////////////////////////////
......
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