Commit 3a7b3d27 authored by Alan Mishchenko's avatar Alan Mishchenko

Experimental cost function in technology mapping.

parent 2325cd77
......@@ -339,6 +339,7 @@ struct Jf_Par_t_
int fCutMin;
int fFuncDsd;
int fGenCnf;
int fGenLit;
int fCnfObjIds;
int fAddOrCla;
int fCnfMapping;
......
......@@ -24,6 +24,7 @@
#include "misc/extra/extra.h"
#include "sat/cnf/cnf.h"
#include "opt/dau/dau.h"
#include "bool/kit/kit.h"
ABC_NAMESPACE_IMPL_START
......@@ -557,8 +558,8 @@ static inline int Mf_CutComputeTruth6( Mf_Man_t * p, Mf_Cut_t * pCut0, Mf_Cut_t
assert( (int)(t & 1) == 0 );
truthId = Vec_MemHashInsert(p->vTtMem, &t);
pCutR->iFunc = Abc_Var2Lit( truthId, fCompl );
if ( p->pPars->fGenCnf && truthId == Vec_IntSize(&p->vCnfSizes) )
Vec_IntPush( &p->vCnfSizes, Abc_Tt6CnfSize(t, pCutR->nLeaves) );
if ( (p->pPars->fGenCnf || p->pPars->fGenLit) && truthId == Vec_IntSize(&p->vCnfSizes) )
Vec_IntPush( &p->vCnfSizes, p->pPars->fGenCnf ? Abc_Tt6CnfSize(t, pCutR->nLeaves) : Kit_TruthLitNum((unsigned *)&t, pCutR->nLeaves, &p->vCnfMem) );
// p->nCutMux += Mf_ManTtIsMux( t );
assert( (int)pCutR->nLeaves <= nOldSupp );
// Mf_ManTruthCanonicize( &t, pCutR->nLeaves );
......@@ -588,8 +589,8 @@ static inline int Mf_CutComputeTruth( Mf_Man_t * p, Mf_Cut_t * pCut0, Mf_Cut_t *
//Kit_DsdPrintFromTruth( uTruth, pCutR->nLeaves ), printf("\n" ), printf("\n" );
truthId = Vec_MemHashInsert(p->vTtMem, uTruth);
pCutR->iFunc = Abc_Var2Lit( truthId, fCompl );
if ( p->pPars->fGenCnf && truthId == Vec_IntSize(&p->vCnfSizes) && LutSize <= 8 )
Vec_IntPush( &p->vCnfSizes, Abc_Tt8CnfSize(uTruth, pCutR->nLeaves) );
if ( (p->pPars->fGenCnf || p->pPars->fGenLit) && truthId == Vec_IntSize(&p->vCnfSizes) && LutSize <= 8 )
Vec_IntPush( &p->vCnfSizes, p->pPars->fGenCnf ? Abc_Tt8CnfSize(uTruth, pCutR->nLeaves) : Kit_TruthLitNum((unsigned *)uTruth, pCutR->nLeaves, &p->vCnfMem) );
assert( (int)pCutR->nLeaves <= nOldSupp );
return (int)pCutR->nLeaves < nOldSupp;
}
......@@ -612,8 +613,8 @@ static inline int Mf_CutComputeTruthMux6( Mf_Man_t * p, Mf_Cut_t * pCut0, Mf_Cut
assert( (int)(t & 1) == 0 );
truthId = Vec_MemHashInsert(p->vTtMem, &t);
pCutR->iFunc = Abc_Var2Lit( truthId, fCompl );
if ( p->pPars->fGenCnf && truthId == Vec_IntSize(&p->vCnfSizes) )
Vec_IntPush( &p->vCnfSizes, Abc_Tt6CnfSize(t, pCutR->nLeaves) );
if ( (p->pPars->fGenCnf || p->pPars->fGenLit) && truthId == Vec_IntSize(&p->vCnfSizes) )
Vec_IntPush( &p->vCnfSizes, p->pPars->fGenCnf ? Abc_Tt6CnfSize(t, pCutR->nLeaves) : Kit_TruthLitNum((unsigned *)&t, pCutR->nLeaves, &p->vCnfMem) );
assert( (int)pCutR->nLeaves <= nOldSupp );
return (int)pCutR->nLeaves < nOldSupp;
}
......@@ -642,8 +643,8 @@ static inline int Mf_CutComputeTruthMux( Mf_Man_t * p, Mf_Cut_t * pCut0, Mf_Cut_
assert( (uTruth[0] & 1) == 0 );
truthId = Vec_MemHashInsert(p->vTtMem, uTruth);
pCutR->iFunc = Abc_Var2Lit( truthId, fCompl );
if ( p->pPars->fGenCnf && truthId == Vec_IntSize(&p->vCnfSizes) && LutSize <= 8 )
Vec_IntPush( &p->vCnfSizes, Abc_Tt8CnfSize(uTruth, pCutR->nLeaves) );
if ( (p->pPars->fGenCnf || p->pPars->fGenLit) && truthId == Vec_IntSize(&p->vCnfSizes) && LutSize <= 8 )
Vec_IntPush( &p->vCnfSizes, p->pPars->fGenCnf ? Abc_Tt8CnfSize(uTruth, pCutR->nLeaves) : Kit_TruthLitNum((unsigned *)uTruth, pCutR->nLeaves, &p->vCnfMem) );
assert( (int)pCutR->nLeaves <= nOldSupp );
return (int)pCutR->nLeaves < nOldSupp;
}
......@@ -699,6 +700,8 @@ static inline void Mf_CutPrint( Mf_Man_t * p, Mf_Cut_t * pCut )
{
if ( p->pPars->fGenCnf )
printf( "CNF = %2d ", Vec_IntEntry(&p->vCnfSizes, Abc_Lit2Var(pCut->iFunc)) );
if ( p->pPars->fGenLit )
printf( "Lit = %2d ", Vec_IntEntry(&p->vCnfSizes, Abc_Lit2Var(pCut->iFunc)) );
Dau_DsdPrintFromTruth( Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut->iFunc)), pCut->nLeaves );
}
else
......@@ -998,7 +1001,7 @@ static inline int Mf_CutArea( Mf_Man_t * p, int nLeaves, int iFunc )
{
if ( nLeaves < 2 )
return 0;
if ( p->pPars->fGenCnf )
if ( p->pPars->fGenCnf || p->pPars->fGenLit )
return Vec_IntEntry(&p->vCnfSizes, Abc_Lit2Var(iFunc));
if ( p->pPars->fOptEdge )
return nLeaves + p->pPars->nAreaTuner;
......@@ -1202,7 +1205,7 @@ int Mf_ManSetMapRefs( Mf_Man_t * p )
Mf_ObjMapRefInc( p, pCut[k] );
p->pPars->Edge += Mf_CutSize(pCut);
p->pPars->Area++;
if ( p->pPars->fGenCnf )
if ( p->pPars->fGenCnf || p->pPars->fGenLit )
p->pPars->Clause += Mf_CutArea(p, Mf_CutSize(pCut), Mf_CutFunc(pCut));
}
// blend references
......@@ -1394,7 +1397,7 @@ Mf_Man_t * Mf_ManAlloc( Gia_Man_t * pGia, Jf_Par_t * pPars )
p->pLfObjs = ABC_CALLOC( Mf_Obj_t, Gia_ManObjNum(pGia) );
p->iCur = 2;
Vec_PtrGrow( &p->vPages, 256 );
if ( pPars->fGenCnf )
if ( pPars->fGenCnf || pPars->fGenLit )
{
Vec_IntGrow( &p->vCnfSizes, 10000 );
Vec_IntPush( &p->vCnfSizes, 1 );
......@@ -1410,7 +1413,7 @@ Mf_Man_t * Mf_ManAlloc( Gia_Man_t * pGia, Jf_Par_t * pPars )
}
void Mf_ManFree( Mf_Man_t * p )
{
assert( !p->pPars->fGenCnf || Vec_IntSize(&p->vCnfSizes) == Vec_MemEntryNum(p->vTtMem) );
assert( !p->pPars->fGenCnf || !p->pPars->fGenLit || Vec_IntSize(&p->vCnfSizes) == Vec_MemEntryNum(p->vTtMem) );
if ( p->pPars->fCutMin )
Vec_MemHashFree( p->vTtMem );
if ( p->pPars->fCutMin )
......@@ -1453,6 +1456,7 @@ void Mf_ManSetDefaultPars( Jf_Par_t * pPars )
pPars->fCoarsen = 1;
pPars->fCutMin = 0;
pPars->fGenCnf = 0;
pPars->fGenLit = 0;
pPars->fPureAig = 0;
pPars->fVerbose = 0;
pPars->fVeryVerbose = 0;
......@@ -1469,6 +1473,8 @@ void Mf_ManPrintStats( Mf_Man_t * p, char * pTitle )
printf( "Edge =%9lu ", (long)p->pPars->Edge );
if ( p->pPars->fGenCnf )
printf( "CNF =%9lu ", (long)p->pPars->Clause );
if ( p->pPars->fGenLit )
printf( "FFL =%9lu ", (long)p->pPars->Clause );
Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
fflush( stdout );
}
......@@ -1483,6 +1489,7 @@ void Mf_ManPrintInit( Mf_Man_t * p )
printf( "CutMin = %d ", p->pPars->fCutMin );
printf( "Coarse = %d ", p->pPars->fCoarsen );
printf( "CNF = %d ", p->pPars->fGenCnf );
printf( "FFL = %d ", p->pPars->fGenLit );
printf( "\n" );
printf( "Computing cuts...\r" );
fflush( stdout );
......@@ -1656,7 +1663,7 @@ Gia_Man_t * Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
{
Mf_Man_t * p;
Gia_Man_t * pNew, * pCls;
if ( pPars->fGenCnf )
if ( pPars->fGenCnf || pPars->fGenLit )
pPars->fCutMin = 1;
if ( Gia_ManHasChoices(pGia) )
pPars->fCutMin = 1, pPars->fCoarsen = 0;
......@@ -1685,8 +1692,8 @@ Gia_Man_t * Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
pNew = Mf_ManDeriveMapping( p );
if ( p->pPars->fGenCnf )
pGia->pData = Mf_ManDeriveCnf( p, p->pPars->fCnfObjIds, p->pPars->fAddOrCla );
// if ( p->pPars->fGenCnf )
// Mf_ManProfileTruths( p );
//if ( p->pPars->fGenCnf || p->pPars->fGenLit )
// Mf_ManProfileTruths( p );
Gia_ManMappingVerify( pNew );
Mf_ManPrintQuit( p, pNew );
Mf_ManFree( p );
......
......@@ -39541,7 +39541,7 @@ int Abc_CommandAbc9Mf( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_Man_t * pNew; int c;
Mf_ManSetDefaultPars( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "KCFARLEDWaekmcgvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "KCFARLEDWaekmclgvwh" ) ) != EOF )
{
switch ( c )
{
......@@ -39665,6 +39665,9 @@ int Abc_CommandAbc9Mf( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'c':
pPars->fGenCnf ^= 1;
break;
case 'l':
pPars->fGenLit ^= 1;
break;
case 'g':
pPars->fPureAig ^= 1;
break;
......@@ -39717,6 +39720,7 @@ usage:
Abc_Print( -2, "\t-k : toggles coarsening the subject graph [default = %s]\n", pPars->fCoarsen? "yes": "no" );
Abc_Print( -2, "\t-m : toggles cut minimization [default = %s]\n", pPars->fCutMin? "yes": "no" );
Abc_Print( -2, "\t-c : toggles mapping for CNF generation [default = %s]\n", pPars->fGenCnf? "yes": "no" );
Abc_Print( -2, "\t-l : toggles mapping for literals [default = %s]\n", pPars->fGenLit? "yes": "no" );
Abc_Print( -2, "\t-g : toggles generating AIG without mapping [default = %s]\n", pPars->fPureAig? "yes": "no" );
Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggles very verbose output [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
......@@ -568,6 +568,7 @@ extern unsigned Kit_GraphToTruth( Kit_Graph_t * pGraph );
extern Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
extern Kit_Graph_t * Kit_TruthToGraph2( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory );
extern int Kit_GraphLeafDepth_rec( Kit_Graph_t * pGraph, Kit_Node_t * pNode, Kit_Node_t * pLeaf );
extern int Kit_TruthLitNum( unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
/*=== kitHop.c ==========================================================*/
//extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
//extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
......
......@@ -496,6 +496,31 @@ int * Kit_TruthTest( char * pFileName )
return pResult;
}
/**Function*************************************************************
Synopsis [Derives the factored form from the truth table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_TruthLitNum( unsigned * pTruth, int nVars, Vec_Int_t * vMemory )
{
Kit_Graph_t * pGraph;
int RetValue, nLits;
RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 1 );
if ( RetValue == -1 || Vec_IntSize(vMemory) > (1<<16) )
return -1;
assert( RetValue == 0 || RetValue == 1 );
pGraph = Kit_SopFactor( vMemory, RetValue, nVars, vMemory );
nLits = 1 + Kit_GraphNodeNum( pGraph );
Kit_GraphFree( pGraph );
return nLits;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
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