luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

New MFS package.

This commit is contained in:
Alan Mishchenko 2013-04-03 12:39:24 -07:00
parent 23229e03bf
commit e4cf178041
4 changed files with 145 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/opt/sfm/sfm.h
View File

@ -75,7 +75,7 @@ extern int Sfm_ManPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars );
extern Sfm_Man_t * Sfm_ManAlloc( Sfm_Ntk_t * p );
extern void Sfm_ManFree( Sfm_Man_t * p );
/*=== sfmNtk.c ==========================================================*/
extern Sfm_Ntk_t * Sfm_NtkAlloc( int nPis, int nPos, int nNodes, int nEdges );
extern Sfm_Ntk_t * Sfm_NtkAlloc( int nPis, int nPos, int nNodes, Vec_Int_t * vFanins, Vec_Int_t * vFanouts, Vec_Int_t * vEdges, Vec_Int_t * vOpts );
extern void Sfm_NtkFree( Sfm_Ntk_t * p );
/*=== sfmSat.c ==========================================================*/

74
src/opt/sfm/sfmCnf.c
View File

@ -19,6 +19,7 @@
***********************************************************************/
#include "sfmInt.h"
#include "bool/kit/kit.h"
ABC_NAMESPACE_IMPL_START
@ -42,11 +43,80 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
Vec_Int_t * Sfm_TruthToCnf( word Truth )
int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
{
return NULL;
int nCubes = 0;
Vec_StrClear( vCnf );
if ( Truth == 0 || ~Truth == 0 )
{
Vec_StrPush( vCnf, (char)(Truth == 0) );
Vec_StrPush( vCnf, -1 );
return 1;
}
else
{
int i, k, c, RetValue, Literal, Cube, nCubes = 0;
for ( c = 0; c < 2; c ++ )
{
Truth = c ? ~Truth : Truth;
RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 );
assert( RetValue == 0 );
nCubes += Vec_IntSize( vCover );
Vec_IntForEachEntry( vCover, Cube, i )
{
for ( k = 0; k < nVars; k++ )
{
Literal = 3 & (Cube >> (k << 1));
if ( Literal == 1 ) // '0' -> pos lit
Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 0) );
else if ( Literal == 2 ) // '1' -> neg lit
Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 1) );
else if ( Literal != 0 )
assert( 0 );
}
Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) );
Vec_StrPush( vCnf, -1 );
}
}
return nCubes;
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sfm_DeriveCnfs( Vec_Wrd_t * vTruths, Vec_Int_t * vFanins, Vec_Str_t ** pvCnfs, Vec_Int_t ** pvOffsets )
{
Vec_Str_t * vCnfs, * vCnf;
Vec_Int_t * vOffsets, * vCover;
int i, k, nFanins, nClauses = 0;
vCnf = Vec_StrAlloc( 1000 );
vCnfs = Vec_StrAlloc( 1000 );
vOffsets = Vec_IntAlloc( Vec_IntSize(vFanins) );
vCover = Vec_IntAlloc( 1 << 16 );
assert( Vec_WrdSize(vTruths) == Vec_IntSize(vFanins) );
Vec_IntForEachEntry( vFanins, nFanins, i )
{
nClauses += Sfm_TruthToCnf( Vec_WrdEntry(vTruths, i), nFanins, vCover, vCnf );
Vec_IntPush( vOffsets, Vec_StrSize(vCnfs) );
for ( k = 0; k < Vec_StrSize(vCnf); k++ )
Vec_StrPush( vCnfs, Vec_StrEntry(vCnf, k) );
}
Vec_IntPush( vOffsets, Vec_StrSize(vCnfs) );
Vec_StrFree( vCnf );
Vec_IntFree( vCover );
return nClauses;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

13
src/opt/sfm/sfmInt.h
View File

@ -65,7 +65,7 @@ struct Sfm_Obj_t_
{
unsigned Type : 2;
unsigned Id : 30;
unsigned fFixed : 1;
unsigned fOpt : 1;
unsigned fTfo : 1;
unsigned nFanis : 4;
unsigned nFanos : 26;
@ -88,12 +88,21 @@ struct Sfm_Man_t_
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
static inline Sfm_Obj_t * Sfm_ManObj( Sfm_Ntk_t * p, int Id ) { return (Sfm_Obj_t *)Vec_IntEntryP( &p->vObjs, Id ); }
#define Sfm_ManForEachObj( p, pObj, i ) \
for ( i = 0; (i < Vec_IntSize(&p->vObjs) && ((pObj) = Sfm_ManObj(p, i))); i++ )
#define Sfm_ManForEachPi( p, pObj, i ) \
for ( i = 0; (i < Vec_IntSize(&p->vPis) && ((pObj) = Sfm_ManObj(p, Vec_IntEntry(&p->vPis, i)))); i++ )
#define Sfm_ManForEachPo( p, pObj, i ) \
for ( i = 0; (i < Vec_IntSize(&p->vPos) && ((pObj) = Sfm_ManObj(p, Vec_IntEntry(&p->vPos, i)))); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== sfmCnf.c ==========================================================*/
extern Vec_Int_t * Sfm_TruthToCnf( word Truth );
extern int Sfm_DeriveCnfs( Vec_Wrd_t * vTruths, Vec_Int_t * vFanins, Vec_Str_t ** pvCnfs, Vec_Int_t ** pvOffsets );
/*=== sfmCore.c ==========================================================*/
/*=== sfmMan.c ==========================================================*/
/*=== sfmNtk.c ==========================================================*/

64
src/opt/sfm/sfmNtk.c
View File

@ -42,13 +42,71 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
Sfm_Ntk_t * Sfm_NtkAlloc( int nPis, int nPos, int nNodes, int nEdges )
Sfm_Ntk_t * Sfm_NtkAlloc( int nPis, int nPos, int nNodes, Vec_Int_t * vFanins, Vec_Int_t * vFanouts, Vec_Int_t * vEdges, Vec_Int_t * vOpts )
{
Sfm_Ntk_t * p;
int AddOn = 2;
int nSize = (nPis + nPos + nNodes) * (sizeof(Sfm_Obj_t) / sizeof(int) + AddOn) + 2 * nEdges;
Sfm_Obj_t * pObj, * pFan;
int i, k, nObjSize, AddOn = 2;
int nStructSize = sizeof(Sfm_Obj_t) / sizeof(int);
int iFanin, iOffset = 2, iFanOffset = 0;
int nEdges = Vec_IntSize(vEdges);
int nObjs = nPis + nPos + nNodes;
int nSize = 2 + nObjs + nObjs * nStructSize + 2 * nEdges + AddOn * (nObjs - Vec_IntSum(vOpts));
assert( sizeof(Sfm_Obj_t) % sizeof(int) == 0 );
assert( nEdges == Vec_IntSum(vFanins) );
assert( nEdges == Vec_IntSum(vFanouts) );
p = ABC_CALLOC( Sfm_Ntk_t, 1 );
p->pMem = ABC_CALLOC( int, nSize );
for ( i = 0; i < nObjs; i++ )
{
Vec_IntPush( &p->vObjs, iOffset );
pObj = Sfm_ManObj( p, i );
pObj->Id = i;
if ( i < nPis )
{
pObj->Type = 1;
assert( Vec_IntEntry(vFanins, i) == 0 );
assert( Vec_IntEntry(vOpts, i) == 0 );
Vec_IntPush( &p->vPis, iOffset );
}
else
{
pObj->Type = 2;
pObj->fOpt = Vec_IntEntry(vOpts, i);
if ( i >= nPis + nNodes ) // PO
{
pObj->Type = 3;
assert( Vec_IntEntry(vFanins, i) == 1 );
assert( Vec_IntEntry(vFanouts, i) == 0 );
assert( Vec_IntEntry(vOpts, i) == 0 );
Vec_IntPush( &p->vPos, iOffset );
}
for ( k = 0; k < Vec_IntEntry(vFanins, i); k++ )
{
iFanin = Vec_IntEntry( vEdges, iFanOffset++ );
pFan = Sfm_ManObj( p, iFanin );
assert( iFanin < i );
pObj->Fanio[ pObj->nFanis++ ] = iFanin;
pFan->Fanio[ pFan->nFanis + pFan->nFanos++ ] = i;
}
}
// add node size
nObjSize = nStructSize + Vec_IntEntry(vFanins, i) + Vec_IntEntry(vFanouts, i) + AddOn * pObj->fOpt;
nObjSize += (int)( nObjSize & 1 );
assert( (nObjSize & 1) == 0 );
iOffset += nObjSize;
}
assert( iOffSet <= nSize );
assert( iFanOffset == Vec_IntSize(vEdges) );
iFanOffset = 0;
Sfm_ManForEachObj( p, pObj, i )
{
assert( Vec_IntEntry(vFanins, i) == pObj->nFanis );
assert( Vec_IntEntry(vFanouts, i) == pObj->nFanos );
for ( k = 0; k < (int)pObj->nFanis; k++ )
assert( pObj->Fanio[k] == Vec_IntEntry(vEdges, iFanOffset++) );
}
assert( iFanOffset == Vec_IntSize(vEdges) );
return p;
}
void Sfm_NtkFree( Sfm_Ntk_t * p )