mirror of https://github.com/YosysHQ/abc.git
Generation of plain AIG after mapping.
This commit is contained in:
parent
debbf4d807
commit
940cf7f98b
|
|
@ -2071,6 +2071,10 @@ SOURCE=.\src\opt\dau\dauEnum.c
|
|||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\opt\dau\dauGia.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\opt\dau\dauInt.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
|
|
|||
|
|
@ -248,6 +248,7 @@ struct Jf_Par_t_
|
|||
int fCutMin;
|
||||
int fUseTts;
|
||||
int fGenCnf;
|
||||
int fPureAig;
|
||||
int fVerbose;
|
||||
int fVeryVerbose;
|
||||
int nLutSizeMax;
|
||||
|
|
|
|||
|
|
@ -24,6 +24,7 @@
|
|||
#include "misc/extra/extra.h"
|
||||
#include "bool/kit/kit.h"
|
||||
#include "misc/util/utilTruth.h"
|
||||
#include "opt/dau/dau.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
|
@ -1426,6 +1427,82 @@ void Jf_ManDeriveMapping( Jf_Man_t * p )
|
|||
// Gia_ManMappingVerify( p->pGia );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derive GIA without mapping.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Gia_Man_t * Jf_ManDeriveGia( Jf_Man_t * p )
|
||||
{
|
||||
Gia_Man_t * pNew;
|
||||
Gia_Obj_t * pObj;
|
||||
Vec_Int_t * vCopies = Vec_IntStartFull( Gia_ManObjNum(p->pGia) );
|
||||
Vec_Int_t * vCover = Vec_IntAlloc( 1 << 16 );
|
||||
Vec_Int_t * vLeaves = Vec_IntAlloc( 16 );
|
||||
int i, k, iLit, Class, * pCut;
|
||||
word uTruth;
|
||||
assert( p->pPars->fCutMin );
|
||||
// create new manager
|
||||
pNew = Gia_ManStart( Gia_ManObjNum(p->pGia) );
|
||||
pNew->pName = Abc_UtilStrsav( p->pGia->pName );
|
||||
pNew->pSpec = Abc_UtilStrsav( p->pGia->pSpec );
|
||||
// map primary inputs
|
||||
Vec_IntWriteEntry( vCopies, 0, 0 );
|
||||
Gia_ManForEachCi( p->pGia, pObj, i )
|
||||
Vec_IntWriteEntry( vCopies, Gia_ObjId(p->pGia, pObj), Gia_ManAppendCi(pNew) );
|
||||
// iterate through nodes used in the mapping
|
||||
Gia_ManHashStart( pNew );
|
||||
Gia_ManForEachAnd( p->pGia, pObj, i )
|
||||
{
|
||||
if ( Gia_ObjIsBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 )
|
||||
continue;
|
||||
pCut = Jf_ObjCutBest( p, i );
|
||||
// printf( "Best cut of node %d: ", i ); Jf_CutPrint(pCut);
|
||||
Class = Jf_CutFuncClass( pCut );
|
||||
uTruth = p->pPars->fUseTts ? *Vec_MemReadEntry(p->vTtMem, Class) : Sdm_ManReadDsdTruth(p->pDsd, Class);
|
||||
assert( p->pDsd == NULL || Sdm_ManReadDsdVarNum(p->pDsd, Class) == Jf_CutSize(pCut) );
|
||||
if ( Jf_CutSize(pCut) == 0 )
|
||||
{
|
||||
assert( Class == 0 );
|
||||
Vec_IntWriteEntry( vCopies, i, Jf_CutFunc(pCut) );
|
||||
continue;
|
||||
}
|
||||
if ( Jf_CutSize(pCut) == 1 )
|
||||
{
|
||||
assert( Class == 1 );
|
||||
iLit = Abc_LitNotCond( Jf_CutLit(pCut, 1) , Jf_CutFuncCompl(pCut) );
|
||||
iLit = Abc_Lit2LitL( Vec_IntArray(vCopies), iLit );
|
||||
Vec_IntWriteEntry( vCopies, i, iLit );
|
||||
continue;
|
||||
}
|
||||
// collect leaves
|
||||
Vec_IntClear( vLeaves );
|
||||
Jf_CutForEachLit( pCut, iLit, k )
|
||||
Vec_IntPush( vLeaves, Abc_Lit2LitL(Vec_IntArray(vCopies), iLit) );
|
||||
// create GIA
|
||||
iLit = Dsm_ManDeriveGia( pNew, uTruth, vLeaves, vCover );
|
||||
iLit = Abc_LitNotCond( iLit, Jf_CutFuncCompl(pCut) );
|
||||
Vec_IntWriteEntry( vCopies, i, iLit );
|
||||
}
|
||||
Gia_ManForEachCo( p->pGia, pObj, i )
|
||||
{
|
||||
iLit = Vec_IntEntry( vCopies, Gia_ObjFaninId0p(p->pGia, pObj) );
|
||||
Gia_ManAppendCo( pNew, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) );
|
||||
}
|
||||
Vec_IntFree( vCopies );
|
||||
Vec_IntFree( vLeaves );
|
||||
Vec_IntFree( vCover );
|
||||
Gia_ManHashStop( pNew );
|
||||
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p->pGia) );
|
||||
return pNew;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
|
@ -1451,6 +1528,7 @@ void Jf_ManSetDefaultPars( Jf_Par_t * pPars )
|
|||
pPars->fCutMin = 0;
|
||||
pPars->fUseTts = 0;
|
||||
pPars->fGenCnf = 0;
|
||||
pPars->fPureAig = 0;
|
||||
pPars->fVerbose = 0;
|
||||
pPars->fVeryVerbose = 0;
|
||||
pPars->nLutSizeMax = JF_LEAF_MAX;
|
||||
|
|
@ -1491,7 +1569,9 @@ Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
|
|||
Jf_ManPropagateEla( p, 0 ); Jf_ManPrintStats( p, "Area " );
|
||||
Jf_ManPropagateEla( p, 1 ); Jf_ManPrintStats( p, "Edge " );
|
||||
}
|
||||
if ( p->pPars->fCutMin )
|
||||
if ( p->pPars->fPureAig )
|
||||
pNew = Jf_ManDeriveGia(p);
|
||||
else if ( p->pPars->fCutMin )
|
||||
pNew = Jf_ManDeriveMappingGia(p);
|
||||
else
|
||||
Jf_ManDeriveMapping(p);
|
||||
|
|
|
|||
|
|
@ -29874,11 +29874,10 @@ int Abc_CommandAbc9Jf( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
{
|
||||
char Buffer[200];
|
||||
Jf_Par_t Pars, * pPars = &Pars;
|
||||
Gia_Man_t * pNew;
|
||||
int c;
|
||||
Gia_Man_t * pNew; int c;
|
||||
Jf_ManSetDefaultPars( pPars );
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "KCRDWaekmtcvwh" ) ) != EOF )
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "KCRDWaekmtcgvwh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
|
|
@ -29961,6 +29960,9 @@ int Abc_CommandAbc9Jf( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
case 'c':
|
||||
pPars->fGenCnf ^= 1;
|
||||
break;
|
||||
case 'g':
|
||||
pPars->fPureAig ^= 1;
|
||||
break;
|
||||
case 'v':
|
||||
pPars->fVerbose ^= 1;
|
||||
break;
|
||||
|
|
@ -29999,7 +30001,7 @@ usage:
|
|||
sprintf(Buffer, "best possible" );
|
||||
else
|
||||
sprintf(Buffer, "%d", pPars->DelayTarget );
|
||||
Abc_Print( -2, "usage: &jf [-KCRDW num] [-akmtcvwh]\n" );
|
||||
Abc_Print( -2, "usage: &jf [-KCRDW num] [-akmtcgvwh]\n" );
|
||||
Abc_Print( -2, "\t performs technology mapping of the network\n" );
|
||||
Abc_Print( -2, "\t-K num : LUT size for the mapping (2 <= K <= %d) [default = %d]\n", pPars->nLutSizeMax, pPars->nLutSize );
|
||||
Abc_Print( -2, "\t-C num : the max number of priority cuts (1 <= C <= %d) [default = %d]\n", pPars->nCutNumMax, pPars->nCutNum );
|
||||
|
|
@ -30012,6 +30014,7 @@ usage:
|
|||
Abc_Print( -2, "\t-m : toggles cut minimization [default = %s]\n", pPars->fCutMin? "yes": "no" );
|
||||
Abc_Print( -2, "\t-t : toggles truth tables for minimization [default = %s]\n", pPars->fUseTts? "yes": "no" );
|
||||
Abc_Print( -2, "\t-c : toggles mapping for CNF generation [default = %s]\n", pPars->fGenCnf? "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" );
|
||||
Abc_Print( -2, "\t-h : prints the command usage\n");
|
||||
|
|
|
|||
|
|
@ -87,6 +87,9 @@ extern int Dau_DsdCountAnds( char * pDsd );
|
|||
extern void Dau_DsdTruthCompose_rec( word * pFunc, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word * pRes, int nVars, int nWordsR );
|
||||
extern int Dau_DsdCheck1Step( word * pTruth, int nVarsInit );
|
||||
|
||||
/*=== dauGia.c ==========================================================*/
|
||||
extern int Dsm_ManDeriveGia( void * p, word uTruth, Vec_Int_t * vLeaves, Vec_Int_t * vCover );
|
||||
|
||||
/*=== dauMerge.c ==========================================================*/
|
||||
extern void Dau_DsdRemoveBraces( char * pDsd, int * pMatches );
|
||||
extern char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1, int nVars );
|
||||
|
|
|
|||
|
|
@ -1021,7 +1021,7 @@ static inline int Dau_DsdWritePrime( Dau_Dsd_t * p, word * pTruth, int * pVars,
|
|||
int nNonDecSize;
|
||||
// compose the result
|
||||
Dau_DsdWriteString( p, "<" );
|
||||
Dau_DsdWriteVar( p, pVars[vBest], 0 );
|
||||
Dau_DsdWriteVar( p, vBest, 0 );
|
||||
// split decomposition
|
||||
Abc_TtCofactor1p( pCofTemp, pTruth, nWords, vBest );
|
||||
nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, p->fWriteTruth, pRes );
|
||||
|
|
|
|||
|
|
@ -0,0 +1,225 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [dauGia.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [DAG-aware unmapping.]
|
||||
|
||||
Synopsis [Coverting DSD into GIA.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: dauGia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "dauInt.h"
|
||||
#include "aig/gia/gia.h"
|
||||
#include "misc/util/utilTruth.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derives GIA for the truth table.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Dau_DsdToGiaCompose_rec( Gia_Man_t * pGia, word Func, int * pFanins, int nVars )
|
||||
{
|
||||
int t0, t1;
|
||||
if ( Func == 0 )
|
||||
return 0;
|
||||
if ( Func == ~(word)0 )
|
||||
return 1;
|
||||
assert( nVars > 0 );
|
||||
if ( --nVars == 0 )
|
||||
{
|
||||
assert( Func == s_Truths6[0] || Func == s_Truths6Neg[0] );
|
||||
return Abc_LitNotCond( pFanins[0], (int)(Func == s_Truths6Neg[0]) );
|
||||
}
|
||||
if ( !Abc_Tt6HasVar(Func, nVars) )
|
||||
return Dau_DsdToGiaCompose_rec( pGia, Func, pFanins, nVars );
|
||||
t0 = Dau_DsdToGiaCompose_rec( pGia, Abc_Tt6Cofactor0(Func, nVars), pFanins, nVars );
|
||||
t1 = Dau_DsdToGiaCompose_rec( pGia, Abc_Tt6Cofactor1(Func, nVars), pFanins, nVars );
|
||||
return Gia_ManHashMux( pGia, pFanins[nVars], t1, t0 );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derives GIA for the DSD formula.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches, int * pLits, Vec_Int_t * vCover )
|
||||
{
|
||||
int fCompl = 0;
|
||||
if ( **p == '!' )
|
||||
(*p)++, fCompl = 1;
|
||||
if ( **p >= 'a' && **p <= 'f' ) // var
|
||||
{
|
||||
assert( **p - 'a' >= 0 && **p - 'a' < 6 );
|
||||
return Abc_LitNotCond( pLits[**p - 'a'], fCompl );
|
||||
}
|
||||
if ( **p == '(' ) // and/or
|
||||
{
|
||||
char * q = pStr + pMatches[ *p - pStr ];
|
||||
int Res = 1, Lit;
|
||||
assert( **p == '(' && *q == ')' );
|
||||
for ( (*p)++; *p < q; (*p)++ )
|
||||
{
|
||||
Lit = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits, vCover );
|
||||
Res = Gia_ManHashAnd( pGia, Res, Lit );
|
||||
}
|
||||
assert( *p == q );
|
||||
return Abc_LitNotCond( Res, fCompl );
|
||||
}
|
||||
if ( **p == '[' ) // xor
|
||||
{
|
||||
char * q = pStr + pMatches[ *p - pStr ];
|
||||
int Res = 0, Lit;
|
||||
assert( **p == '[' && *q == ']' );
|
||||
for ( (*p)++; *p < q; (*p)++ )
|
||||
{
|
||||
Lit = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits, vCover );
|
||||
Res = Gia_ManHashXor( pGia, Res, Lit );
|
||||
}
|
||||
assert( *p == q );
|
||||
return Abc_LitNotCond( Res, fCompl );
|
||||
}
|
||||
if ( **p == '<' ) // mux
|
||||
{
|
||||
int nVars = 0;
|
||||
int Temp[3], * pTemp = Temp, Res;
|
||||
int Fanins[6], * pLits2;
|
||||
char * pOld = *p;
|
||||
char * q = pStr + pMatches[ *p - pStr ];
|
||||
// read fanins
|
||||
if ( *(q+1) == '{' )
|
||||
{
|
||||
char * q2;
|
||||
*p = q+1;
|
||||
q2 = pStr + pMatches[ *p - pStr ];
|
||||
assert( **p == '{' && *q2 == '}' );
|
||||
for ( nVars = 0, (*p)++; *p < q2; (*p)++, nVars++ )
|
||||
Fanins[nVars] = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits, vCover );
|
||||
assert( *p == q2 );
|
||||
pLits2 = Fanins;
|
||||
}
|
||||
else
|
||||
pLits2 = pLits;
|
||||
// read MUX
|
||||
*p = pOld;
|
||||
q = pStr + pMatches[ *p - pStr ];
|
||||
assert( **p == '<' && *q == '>' );
|
||||
// verify internal variables
|
||||
if ( nVars )
|
||||
for ( ; pOld < q; pOld++ )
|
||||
if ( *pOld >= 'a' && *pOld <= 'z' )
|
||||
assert( *pOld - 'a' < nVars );
|
||||
// derive MUX components
|
||||
for ( (*p)++; *p < q; (*p)++ )
|
||||
*pTemp++ = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits2, vCover );
|
||||
assert( pTemp == Temp + 3 );
|
||||
assert( *p == q );
|
||||
if ( *(q+1) == '{' ) // and/or
|
||||
{
|
||||
char * q = pStr + pMatches[ ++(*p) - pStr ];
|
||||
assert( **p == '{' && *q == '}' );
|
||||
*p = q;
|
||||
}
|
||||
Res = Gia_ManHashMux( pGia, Temp[0], Temp[1], Temp[2] );
|
||||
return Abc_LitNotCond( Res, fCompl );
|
||||
}
|
||||
if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
|
||||
{
|
||||
word Func;
|
||||
int Fanins[6], Res;
|
||||
Vec_Int_t vLeaves;
|
||||
char * q;
|
||||
int i, nVars = Abc_TtReadHex( &Func, *p );
|
||||
*p += Abc_TtHexDigitNum( nVars );
|
||||
q = pStr + pMatches[ *p - pStr ];
|
||||
assert( **p == '{' && *q == '}' );
|
||||
for ( i = 0, (*p)++; *p < q; (*p)++, i++ )
|
||||
Fanins[i] = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits, vCover );
|
||||
assert( i == nVars );
|
||||
assert( *p == q );
|
||||
// Res = Dau_DsdToGiaCompose_rec( pGia, Func, Fanins, nVars );
|
||||
vLeaves.nCap = nVars;
|
||||
vLeaves.nSize = nVars;
|
||||
vLeaves.pArray = Fanins;
|
||||
Res = Kit_TruthToGia( pGia, (unsigned *)&Func, nVars, vCover, &vLeaves, 1 );
|
||||
return Abc_LitNotCond( Res, fCompl );
|
||||
}
|
||||
assert( 0 );
|
||||
return 0;
|
||||
}
|
||||
int Dau_DsdToGia( Gia_Man_t * pGia, char * p, int * pLits, Vec_Int_t * vCover )
|
||||
{
|
||||
int Res;
|
||||
if ( *p == '0' && *(p+1) == 0 )
|
||||
Res = 0;
|
||||
else if ( *p == '1' && *(p+1) == 0 )
|
||||
Res = 1;
|
||||
else
|
||||
Res = Dau_DsdToGia_rec( pGia, p, &p, Dau_DsdComputeMatches(p), pLits, vCover );
|
||||
assert( *++p == 0 );
|
||||
return Res;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Convert TT to GIA via DSD.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Dsm_ManDeriveGia( void * p, word uTruth, Vec_Int_t * vLeaves, Vec_Int_t * vCover )
|
||||
{
|
||||
Gia_Man_t * pGia = (Gia_Man_t *)p;
|
||||
char pDsd[1000];
|
||||
int nSizeNonDec;
|
||||
// static int Counter = 0; Counter++;
|
||||
nSizeNonDec = Dau_DsdDecompose( &uTruth, Vec_IntSize(vLeaves), 1, 1, pDsd );
|
||||
// printf( "%s\n", pDsd );
|
||||
return Dau_DsdToGia( pGia, pDsd, Vec_IntArray(vLeaves), vCover );
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -3,5 +3,6 @@ SRC += src/opt/dau/dauCanon.c \
|
|||
src/opt/dau/dauDivs.c \
|
||||
src/opt/dau/dauDsd.c \
|
||||
src/opt/dau/dauEnum.c \
|
||||
src/opt/dau/dauGia.c \
|
||||
src/opt/dau/dauMerge.c \
|
||||
src/opt/dau/dauTree.c
|
||||
|
|
|
|||
Loading…
Reference in New Issue