mirror of https://github.com/YosysHQ/abc.git
New choice computation.
This commit is contained in:
parent
e033a62282
commit
288d64d033
|
|
@ -18,9 +18,11 @@
|
|||
|
||||
***********************************************************************/
|
||||
|
||||
#include "gia.h"
|
||||
#include "giaAig.h"
|
||||
#include "base/main/main.h"
|
||||
#include "base/cmd/cmd.h"
|
||||
#include "proof/dch/dch.h"
|
||||
#include "opt/dau/dau.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
|
@ -344,6 +346,35 @@ void Gia_ManPerformFlow( int fIsMapped, int nAnds, int nLevels, int nLutSize, in
|
|||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Duplicates the AIG manager.]
|
||||
|
||||
Description [This duplicator works for AIGs with choices.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Ptr_t * Gia_ManOrderPios( Aig_Man_t * p, Gia_Man_t * pOrder )
|
||||
{
|
||||
Vec_Ptr_t * vPios;
|
||||
Gia_Obj_t * pObj;
|
||||
int i;
|
||||
assert( Aig_ManCiNum(p) == Gia_ManCiNum(pOrder) );
|
||||
assert( Aig_ManCoNum(p) == Gia_ManCoNum(pOrder) );
|
||||
vPios = Vec_PtrAlloc( Aig_ManCiNum(p) + Aig_ManCoNum(p) );
|
||||
Gia_ManForEachObj( pOrder, pObj, i )
|
||||
{
|
||||
if ( Gia_ObjIsCi(pObj) )
|
||||
Vec_PtrPush( vPios, Aig_ManCi(p, Gia_ObjCioId(pObj)) );
|
||||
else if ( Gia_ObjIsCo(pObj) )
|
||||
Vec_PtrPush( vPios, Aig_ManCo(p, Gia_ObjCioId(pObj)) );
|
||||
}
|
||||
return vPios;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
|
@ -355,9 +386,98 @@ void Gia_ManPerformFlow( int fIsMapped, int nAnds, int nLevels, int nLutSize, in
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Gia_Man_t * Gia_ManAigSynch2( Gia_Man_t * p, int fVerbose )
|
||||
Gia_Man_t * Gia_ManAigSynch2Choices( Gia_Man_t * pGia1, Gia_Man_t * pGia2, Gia_Man_t * pGia3, Dch_Pars_t * pPars )
|
||||
{
|
||||
return NULL;
|
||||
Aig_Man_t * pMan, * pTemp;
|
||||
Gia_Man_t * pGia, * pMiter;
|
||||
// derive miter
|
||||
Vec_Ptr_t * vPios, * vGias = Vec_PtrAlloc( 3 );
|
||||
if ( pGia3 ) Vec_PtrPush( vGias, pGia3 );
|
||||
if ( pGia2 ) Vec_PtrPush( vGias, pGia2 );
|
||||
if ( pGia1 ) Vec_PtrPush( vGias, pGia1 );
|
||||
pMiter = Gia_ManChoiceMiter( vGias );
|
||||
Vec_PtrFree( vGias );
|
||||
// transform into an AIG
|
||||
pMan = Gia_ManToAigSkip( pMiter, 3 );
|
||||
Gia_ManStop( pMiter );
|
||||
// compute choices
|
||||
pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
|
||||
Aig_ManStop( pTemp );
|
||||
// reconstruct the network
|
||||
vPios = Gia_ManOrderPios( pMan, pGia1 );
|
||||
pMan = Aig_ManDupDfsGuided( pTemp = pMan, vPios );
|
||||
Aig_ManStop( pTemp );
|
||||
Vec_PtrFree( vPios );
|
||||
// convert to GIA
|
||||
pGia = Gia_ManFromAigChoices( pMan );
|
||||
Aig_ManStop( pMan );
|
||||
return pGia;
|
||||
}
|
||||
Gia_Man_t * Gia_ManAigSynch2( Gia_Man_t * pInit, void * pPars0, int nLutSize )
|
||||
{
|
||||
extern Gia_Man_t * Gia_ManLutBalance( Gia_Man_t * p, int nLutSize, int fUseMuxes, int fRecursive, int fOptArea, int fVerbose );
|
||||
Dch_Pars_t * pParsDch = (Dch_Pars_t *)pPars0;
|
||||
Gia_Man_t * pGia1, * pGia2, * pGia3, * pNew, * pTemp;
|
||||
int fVerbose = pParsDch->fVerbose;
|
||||
Jf_Par_t Pars, * pPars = &Pars;
|
||||
Lf_ManSetDefaultPars( pPars );
|
||||
pPars->fCutMin = 1;
|
||||
pPars->fCoarsen = 1;
|
||||
pPars->nRelaxRatio = 20;
|
||||
pPars->nAreaTuner = 1;
|
||||
pPars->nCutNum = 4;
|
||||
pPars->fVerbose = fVerbose;
|
||||
if ( fVerbose ) Gia_ManPrintStats( pInit, NULL );
|
||||
pGia1 = Gia_ManDup( pInit );
|
||||
if ( Gia_ManAndNum(pGia1) == 0 )
|
||||
{
|
||||
Gia_ManTransferTiming( pGia1, pInit );
|
||||
return pGia1;
|
||||
}
|
||||
if ( pGia1->pManTime && pGia1->vLevels == NULL )
|
||||
Gia_ManLevelWithBoxes( pGia1 );
|
||||
// unmap if mapped
|
||||
if ( Gia_ManHasMapping(pInit) )
|
||||
{
|
||||
Gia_ManTransferMapping( pGia1, pInit );
|
||||
pGia1 = (Gia_Man_t *)Dsm_ManDeriveGia( pTemp = pGia1, 0 );
|
||||
Gia_ManStop( pTemp );
|
||||
}
|
||||
// perform LUT balancing
|
||||
pGia2 = Gia_ManLutBalance( pGia1, nLutSize, 1, 1, 1, 0 );
|
||||
// perform balancing
|
||||
pGia2 = Gia_ManAreaBalance( pTemp = pGia2, 0, ABC_INFINITY, 0, 0 );
|
||||
if ( fVerbose ) Gia_ManPrintStats( pGia2, NULL );
|
||||
Gia_ManStop( pTemp );
|
||||
// perform mapping
|
||||
pGia2 = Lf_ManPerformMapping( pTemp = pGia2, pPars );
|
||||
if ( fVerbose ) Gia_ManPrintStats( pGia2, NULL );
|
||||
if ( pTemp != pGia2 )
|
||||
Gia_ManStop( pTemp );
|
||||
// perform balancing
|
||||
if ( pParsDch->fLightSynth )
|
||||
pGia3 = Gia_ManAreaBalance( pGia2, 0, ABC_INFINITY, 0, 0 );
|
||||
else
|
||||
{
|
||||
pGia2 = Gia_ManAreaBalance( pTemp = pGia2, 0, ABC_INFINITY, 0, 0 );
|
||||
if ( fVerbose ) Gia_ManPrintStats( pGia2, NULL );
|
||||
Gia_ManStop( pTemp );
|
||||
// perform DSD balancing
|
||||
pGia3 = Gia_ManPerformDsdBalance( pGia2, 6, 8, 0, 0 );
|
||||
}
|
||||
if ( fVerbose ) Gia_ManPrintStats( pGia3, NULL );
|
||||
// perform choice computation
|
||||
pNew = Gia_ManAigSynch2Choices( pGia1, pGia2, pGia3, pParsDch );
|
||||
Gia_ManStop( pGia1 );
|
||||
Gia_ManStop( pGia2 );
|
||||
Gia_ManStop( pGia3 );
|
||||
// copy names
|
||||
ABC_FREE( pNew->pName );
|
||||
ABC_FREE( pNew->pSpec );
|
||||
pNew->pName = Abc_UtilStrsav(pInit->pName);
|
||||
pNew->pSpec = Abc_UtilStrsav(pInit->pSpec);
|
||||
Gia_ManTransferTiming( pNew, pInit );
|
||||
return pNew;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -28453,16 +28453,66 @@ usage:
|
|||
***********************************************************************/
|
||||
int Abc_CommandAbc9Synch2( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
extern Gia_Man_t * Gia_ManAigSynch2( Gia_Man_t * p, int fVerbose );
|
||||
extern Gia_Man_t * Gia_ManAigSynch2( Gia_Man_t * p, void * pPars, int nLutSize );
|
||||
Gia_Man_t * pTemp;
|
||||
int c, fVerbose = 0;
|
||||
Dch_Pars_t Pars, * pPars = &Pars;
|
||||
int c, nLutSize = 6;
|
||||
// set defaults
|
||||
Dch_ManSetDefaultParams( pPars );
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "WCSKfvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'W':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nWords = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nWords < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'C':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nBTLimit = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nBTLimit < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'S':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nSatVarMax = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nSatVarMax < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'K':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-K\" should be followed by a char string.\n" );
|
||||
goto usage;
|
||||
}
|
||||
nLutSize = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( nLutSize < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'f':
|
||||
pPars->fLightSynth ^= 1;
|
||||
break;
|
||||
case 'v':
|
||||
fVerbose ^= 1;
|
||||
pPars->fVerbose ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
|
|
@ -28472,18 +28522,23 @@ int Abc_CommandAbc9Synch2( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
}
|
||||
if ( pAbc->pGia == NULL )
|
||||
{
|
||||
Abc_Print( -1, "Abc_CommandAbc9Synch2(): There is no AIG.\n" );
|
||||
Abc_Print( -1, "Abc_CommandAbc9Dch(): There is no AIG.\n" );
|
||||
return 1;
|
||||
}
|
||||
pTemp = Gia_ManAigSynch2( pAbc->pGia, fVerbose );
|
||||
pTemp = Gia_ManAigSynch2( pAbc->pGia, pPars, nLutSize );
|
||||
Abc_FrameUpdateGia( pAbc, pTemp );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
Abc_Print( -2, "usage: &synch2 [-vh]\n" );
|
||||
Abc_Print( -2, "\t performs synthesis and computes structural choices\n" );
|
||||
Abc_Print( -2, "\t-v : toggles printing additional information [default = %s]\n", fVerbose? "yes": "no" );
|
||||
Abc_Print( -2, "\t-h : print the command usage\n");
|
||||
Abc_Print( -2, "usage: &synch2 [-WCSK num] [-fvh]\n" );
|
||||
Abc_Print( -2, "\t computes structural choices using a new approach\n" );
|
||||
Abc_Print( -2, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
|
||||
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
|
||||
Abc_Print( -2, "\t-S num : the max number of SAT variables [default = %d]\n", pPars->nSatVarMax );
|
||||
Abc_Print( -2, "\t-K num : the target LUT size for downstream mapping [default = %d]\n", nLutSize );
|
||||
Abc_Print( -2, "\t-f : toggle using lighter logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" );
|
||||
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
|
||||
Abc_Print( -2, "\t-h : print the command usage\n");
|
||||
return 1;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -394,14 +394,14 @@ void Ift_TtComparisonConstr( word * pTruth, int nVars, int fMore, int fEqual )
|
|||
{
|
||||
word Cond[4], Equa[4], Temp[4];
|
||||
word s_TtElems[8][4] = {
|
||||
ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),
|
||||
ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),
|
||||
ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),
|
||||
ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),
|
||||
ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),
|
||||
ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),
|
||||
ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),
|
||||
ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF)
|
||||
{ ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA) },
|
||||
{ ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC) },
|
||||
{ ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0) },
|
||||
{ ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00) },
|
||||
{ ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000) },
|
||||
{ ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000) },
|
||||
{ ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF) },
|
||||
{ ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF) }
|
||||
};
|
||||
int i, nWords = Abc_TtWordNum(2*nVars);
|
||||
assert( nVars > 0 && nVars <= 4 );
|
||||
|
|
@ -528,7 +528,7 @@ int Ift_NtkAddClauses( Ift_Ntk_t * p, int * pValues, sat_solver * pSat )
|
|||
int nSatVars = sat_solver_nvars(pSat);
|
||||
for ( i = 0; i < p->nObjs-1; i++ )
|
||||
p->Nodes[i].Var = nSatVars++;
|
||||
p->Nodes[p->nObjs-1].Var = -ABC_INFINITY;
|
||||
p->Nodes[p->nObjs-1].Var = 0xFFFF;
|
||||
sat_solver_setnvars( pSat, nSatVars );
|
||||
// verify variable values
|
||||
for ( i = 0; i < p->nVars; i++ )
|
||||
|
|
|
|||
Loading…
Reference in New Issue