Skip to content

A
abc
Commit bd995ee2 by Alan Mishchenko
Options

Version abc80212

parent d9760b04
Showing with 58 additions and 22 deletions
src/aig/aig/aig.h
......@@ -522,7 +522,7 @@ extern Vec_Ptr_t * Aig_ManSupportsInverse( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Ptr_t ** pvPartSupps );
extern Vec_Ptr_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize );
extern Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize );
extern Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int fVerbose );
extern Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose );
/*=== aigRepr.c =========================================================*/
extern void Aig_ManReprStart( Aig_Man_t * p, int nIdMax );
extern void Aig_ManReprStop( Aig_Man_t * p );
......
src/aig/aig/aigPart.c
......@@ -904,11 +904,11 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int fVerbose )
Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose )
{
// extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
// extern void * Abc_FrameGetGlobalFrame();
extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax );
extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax );
Vec_Ptr_t * vOutsTotal, * vOuts;
Aig_Man_t * pAigTotal, * pAigPart, * pAig;
......@@ -972,7 +972,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int fVer
i+1, Vec_PtrSize(vParts), Aig_ManPiNum(pAigPart), Aig_ManPoNum(pAigPart),
Aig_ManNodeNum(pAigPart), Aig_ManLevelNum(pAigPart) );
// compute equivalence classes (to be stored in pNew->pReprs)
pAig = Fra_FraigChoice( pAigPart, 1000 );
pAig = Fra_FraigChoice( pAigPart, nConfMax, nLevelMax );
Aig_ManStop( pAig );
// reset the pData pointers
Aig_ManForEachObj( pAigPart, pObj, k )
......
src/aig/aig/aigRepr.c
......@@ -429,7 +429,6 @@ void Aig_ManMarkValidChoices( Aig_Man_t * p )
pRepr = Aig_ObjFindRepr( p, pObj );
if ( pRepr == NULL )
continue;
assert( pObj->nRefs == 0 );
// skip constant and PI classes
if ( !Aig_ObjIsNode(pRepr) )
{
......@@ -444,6 +443,7 @@ void Aig_ManMarkValidChoices( Aig_Man_t * p )
}
//printf( "Node %d is represented by node %d.\n", pObj->Id, pRepr->Id );
// add choice to the choice node
assert( pObj->nRefs == 0 );
p->pEquivs[pObj->Id] = p->pEquivs[pRepr->Id];
p->pEquivs[pRepr->Id] = pObj;
}
......
src/aig/dar/dar.h
......@@ -92,7 +92,7 @@ extern Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig );
extern Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose );
extern Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
extern Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
extern Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose );
#ifdef __cplusplus
}
......
src/aig/dar/darScript.c
......@@ -353,7 +353,7 @@ Vec_Ptr_t * Dar_ManChoiceSynthesisExt()
SeeAlso []
***********************************************************************/
Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )
Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose )
{
Aig_Man_t * pMan, * pTemp;
Vec_Ptr_t * vAigs;
......@@ -374,7 +374,7 @@ if ( fVerbose )
PRT( "Synthesis time", clock() - clk );
}
clk = clock();
pMan = Aig_ManChoicePartitioned( vAigs, 300, fVerbose );
pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
Vec_PtrForEachEntry( vAigs, pTemp, i )
Aig_ManStop( pTemp );
Vec_PtrFree( vAigs );
......
src/aig/fra/fra.h
......@@ -73,6 +73,7 @@ struct Fra_Par_t_
int fConeBias; // bias variables in the cone (good for unsat runs)
int nBTLimitNode; // conflict limit at a node
int nBTLimitMiter; // conflict limit at an output
int nLevelMax; // the max level to consider seriously
int nFramesP; // the number of timeframes to in the prefix
int nFramesK; // the number of timeframes to unroll
int nMaxImps; // the maximum number of implications to consider
......@@ -266,7 +267,7 @@ extern void Fra_FraigSweep( Fra_Man_t * pManAig );
extern int Fra_FraigMiterStatus( Aig_Man_t * p );
extern int Fra_FraigMiterAssertedOutput( Aig_Man_t * p );
extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax );
extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax );
extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
/*=== fraHot.c ========================================================*/
extern Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim );
......
src/aig/fra/fraCore.c
......@@ -303,6 +303,7 @@ void Fra_FraigSweep( Fra_Man_t * p )
// Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObjNew;
int i, Pos = 0;
int nBTracksOld;
// fraig latch outputs
Aig_ManForEachLoSeq( p->pManAig, pObj, i )
{
......@@ -315,6 +316,7 @@ void Fra_FraigSweep( Fra_Man_t * p )
// fraig internal nodes
// if ( !p->pPars->fDontShowBar )
// pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pManAig) );
nBTracksOld = p->pPars->nBTLimitNode;
Aig_ManForEachNode( p->pManAig, pObj, i )
{
// if ( pProgress )
......@@ -327,7 +329,12 @@ void Fra_FraigSweep( Fra_Man_t * p )
if ( p->pManFraig->pData )
continue;
// perform fraiging
if ( p->pPars->nLevelMax && (int)pObj->Level > p->pPars->nLevelMax )
p->pPars->nBTLimitNode = 5;
Fra_FraigNode( p, pObj );
if ( p->pPars->nLevelMax && (int)pObj->Level > p->pPars->nLevelMax )
p->pPars->nBTLimitNode = nBTracksOld;
// check implications
if ( p->pPars->fUseImps )
Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
}
......@@ -382,7 +389,7 @@ clk = clock();
// finalize the fraiged manager
Fra_ManFinalizeComb( p );
if ( p->pPars->fChoicing )
{
{
int clk2 = clock();
Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
pManAigNew = Aig_ManDupRepr( p->pManAig, 1 );
......@@ -419,7 +426,7 @@ p->timeTotal = clock() - clk;
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax )
Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax )
{
Fra_Par_t Pars, * pPars = &Pars;
Fra_ParamsDefault( pPars );
......@@ -430,6 +437,7 @@ Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax )
pPars->fProve = 0;
pPars->fVerbose = 0;
pPars->fDontShowBar = 1;
pPars->nLevelMax = nLevelMax;
return Fra_FraigPerform( pManAig, pPars );
}
......
src/aig/fra/fraSec.c
......@@ -211,8 +211,8 @@ PRT( "Time", clock() - clk );
}
// perform retiming
// if ( fRetimeFirst && pNew->nRegs )
if ( pNew->nRegs )
if ( fRetimeFirst && pNew->nRegs )
// if ( pNew->nRegs )
{
clk = clock();
pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
......
src/aig/ivy/ivyFraig.c
......@@ -2009,9 +2009,9 @@ Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld )
if ( Ivy_ObjClassNodeRepr(pObjOld) == NULL || // this is a unique node
(!p->pParams->fDoSparse && Ivy_ObjClassNodeRepr(pObjOld) == p->pManAig->pConst1) ) // this is a sparse node
{
assert( Ivy_Regular(pFanin0New) != Ivy_Regular(pFanin1New) );
assert( pObjNew != Ivy_Regular(pFanin0New) );
assert( pObjNew != Ivy_Regular(pFanin1New) );
// assert( Ivy_Regular(pFanin0New) != Ivy_Regular(pFanin1New) );
// assert( pObjNew != Ivy_Regular(pFanin0New) );
// assert( pObjNew != Ivy_Regular(pFanin1New) );
return pObjNew;
}
// get the fraiged representative
......
src/base/abci/abc.c
......@@ -7675,8 +7675,9 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int fBalance, fVerbose, fUpdateLevel, c;
int nConfMax, nLevelMax;
extern Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose );
extern Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
......@@ -7685,12 +7686,36 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fBalance = 1;
fUpdateLevel = 1;
nConfMax = 1000;
nLevelMax = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "blvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "CLblvh" ) ) != EOF )
{
switch ( c )
{
case 'C':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nConfMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nConfMax < 0 )
goto usage;
break;
case 'L':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
nLevelMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nLevelMax < 0 )
goto usage;
break;
case 'b':
fBalance ^= 1;
break;
......@@ -7716,7 +7741,7 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "This command works only for strashed networks.\n" );
return 1;
}
pNtkRes = Abc_NtkDChoice( pNtk, fBalance, fUpdateLevel, fVerbose );
pNtkRes = Abc_NtkDChoice( pNtk, fBalance, fUpdateLevel, nConfMax, nLevelMax, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
......@@ -7727,8 +7752,10 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: dchoice [-blvh]\n" );
fprintf( pErr, "usage: dchoice [-C num] [-L num] [-blvh]\n" );
fprintf( pErr, "\t performs partitioned choicing using a new AIG package\n" );
fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfMax );
fprintf( pErr, "\t-L num : the max level of nodes to consider (0 = not used) [default = %d]\n", nLevelMax );
fprintf( pErr, "\t-b : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" );
fprintf( pErr, "\t-l : toggle updating level [default = %s]\n", fUpdateLevel? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
......
src/base/abci/abcDar.c
......@@ -720,7 +720,7 @@ clk = clock();
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose )
Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose )
{
Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig;
......@@ -728,7 +728,7 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in
pMan = Abc_NtkToDar( pNtk, 0 );
if ( pMan == NULL )
return NULL;
pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, fVerbose );
pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, nConfMax, nLevelMax, fVerbose );
Aig_ManStop( pTemp );
pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
Aig_ManStop( pMan );
......
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