#include "sfmInt.h"

Functions
ABC_NAMESPACE_IMPL_START void	Sfm_CheckConsistency (Vec_Wec_t vFanins, int nPis, int nPos, Vec_Str_t vFixed)
	DECLARATIONS ///. More...

void	Sfm_CreateFanout (Vec_Wec_t vFanins, Vec_Wec_t vFanouts)

static int	Sfm_ObjLevelNew (Vec_Int_t vArray, Vec_Int_t vLevels, int fAddLevel)

void	Sfm_CreateLevel (Vec_Wec_t vFanins, Vec_Int_t vLevels, Vec_Str_t *vEmpty)

static int	Sfm_ObjLevelNewR (Vec_Int_t vArray, Vec_Int_t vLevelsR, int fAddLevel)

void	Sfm_CreateLevelR (Vec_Wec_t vFanouts, Vec_Int_t vLevelsR, Vec_Str_t *vEmpty)

Sfm_Ntk_t *	Sfm_NtkConstruct (Vec_Wec_t vFanins, int nPis, int nPos, Vec_Str_t vFixed, Vec_Str_t vEmpty, Vec_Wrd_t vTruths)

void	Sfm_NtkPrepare (Sfm_Ntk_t *p)

void	Sfm_NtkFree (Sfm_Ntk_t *p)

void	Sfm_NtkRemoveFanin (Sfm_Ntk_t *p, int iNode, int iFanin)

void	Sfm_NtkAddFanin (Sfm_Ntk_t *p, int iNode, int iFanin)

void	Sfm_NtkDeleteObj_rec (Sfm_Ntk_t *p, int iNode)

void	Sfm_NtkUpdateLevel_rec (Sfm_Ntk_t *p, int iNode)

void	Sfm_NtkUpdateLevelR_rec (Sfm_Ntk_t *p, int iNode)

void	Sfm_NtkUpdate (Sfm_Ntk_t *p, int iNode, int f, int iFaninNew, word uTruth)

Vec_Int_t *	Sfm_NodeReadFanins (Sfm_Ntk_t *p, int i)

word *	Sfm_NodeReadTruth (Sfm_Ntk_t *p, int i)

int	Sfm_NodeReadFixed (Sfm_Ntk_t *p, int i)

int	Sfm_NodeReadUsed (Sfm_Ntk_t *p, int i)

Function Documentation

ABC_NAMESPACE_IMPL_START void Sfm_CheckConsistency	(	Vec_Wec_t *	vFanins,
		int	nPis,
		int	nPos,
		Vec_Str_t *	vFixed
	)

DECLARATIONS ///.

CFile****************************************************************

FileName [sfmNtk.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based optimization using internal don't-cares.]

Synopsis [Logic network.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:: sfmNtk.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sfmNtk.c.

 {
     Vec_Int_t * vArray;
     int i, k, Fanin;
     // check entries
     Vec_WecForEachLevel( vFanins, vArray, i )
     {
         // PIs have no fanins
         if ( i < nPis )
             assert( Vec_IntSize(vArray) == 0 && Vec_StrEntry(vFixed, i) == (char)0 );
         // nodes are in a topo order; POs cannot be fanins
         Vec_IntForEachEntry( vArray, Fanin, k )
 //            assert( Fanin < i && Fanin + nPos < Vec_WecSize(vFanins) );
             assert( Fanin + nPos < Vec_WecSize(vFanins) );
         // POs have one fanout
         if ( i + nPos >= Vec_WecSize(vFanins) )
             assert( Vec_IntSize(vArray) == 1 && Vec_StrEntry(vFixed, i) == (char)0 );
     }
 }

void Sfm_CreateFanout	(	Vec_Wec_t *	vFanins,
		Vec_Wec_t *	vFanouts
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 76 of file sfmNtk.c.

 {
     Vec_Int_t * vArray;
     int i, k, Fanin;
     // count fanouts
     Vec_WecInit( vFanouts, Vec_WecSize(vFanins) );
     Vec_WecForEachLevel( vFanins, vArray, i )
         Vec_IntForEachEntry( vArray, Fanin, k )
             Vec_WecEntry( vFanouts, Fanin )->nSize++;
     // allocate fanins
     Vec_WecForEachLevel( vFanouts, vArray, i )
     {
         k = vArray->nSize; vArray->nSize = 0;
         Vec_IntGrow( vArray, k );
     }
     // add fanouts
     Vec_WecForEachLevel( vFanins, vArray, i )
         Vec_IntForEachEntry( vArray, Fanin, k )
             Vec_IntPush( Vec_WecEntry( vFanouts, Fanin ), i );
     // verify
     Vec_WecForEachLevel( vFanouts, vArray, i )
         assert( Vec_IntSize(vArray) == Vec_IntCap(vArray) );
 }

void Sfm_CreateLevel	(	Vec_Wec_t *	vFanins,
		Vec_Int_t *	vLevels,
		Vec_Str_t *	vEmpty
	)

Definition at line 118 of file sfmNtk.c.

 {
     Vec_Int_t * vArray;
     int i;
     assert( Vec_IntSize(vLevels) == 0 );
     Vec_IntFill( vLevels, Vec_WecSize(vFanins), 0 );
     Vec_WecForEachLevel( vFanins, vArray, i )
         Vec_IntWriteEntry( vLevels, i, Sfm_ObjLevelNew(vArray, vLevels, Sfm_ObjAddsLevelArray(vEmpty, i)) );
 }

void Sfm_CreateLevelR	(	Vec_Wec_t *	vFanouts,
		Vec_Int_t *	vLevelsR,
		Vec_Str_t *	vEmpty
	)

Definition at line 146 of file sfmNtk.c.

 {
     Vec_Int_t * vArray;
     int i;
     assert( Vec_IntSize(vLevelsR) == 0 );
     Vec_IntFill( vLevelsR, Vec_WecSize(vFanouts), 0 );
     Vec_WecForEachLevelReverse( vFanouts, vArray, i )
         Vec_IntWriteEntry( vLevelsR, i, Sfm_ObjLevelNewR(vArray, vLevelsR, Sfm_ObjAddsLevelArray(vEmpty, i)) );
 }

Vec_Int_t* Sfm_NodeReadFanins	(	Sfm_Ntk_t *	p,
		int	i
	)

Function*************************************************************

Synopsis [Public APIs of this network.]

Description []

SideEffects []

SeeAlso []

Definition at line 358 of file sfmNtk.c.

 {
     return Vec_WecEntry( &p->vFanins, i );
 }

int Sfm_NodeReadFixed	(	Sfm_Ntk_t *	p,
		int	i
	)

Definition at line 366 of file sfmNtk.c.

 {
     return (int)Vec_StrEntry( p->vFixed, i );
 }

word* Sfm_NodeReadTruth	(	Sfm_Ntk_t *	p,
		int	i
	)

Definition at line 362 of file sfmNtk.c.

 {
     return Vec_WrdEntryP( p->vTruths, i );
 }

int Sfm_NodeReadUsed	(	Sfm_Ntk_t *	p,
		int	i
	)

Definition at line 370 of file sfmNtk.c.

 {
     return (Sfm_ObjFaninNum(p, i) > 0) || (Sfm_ObjFanoutNum(p, i) > 0);
 }

void Sfm_NtkAddFanin	(	Sfm_Ntk_t *	p,
		int	iNode,
		int	iFanin
	)

Definition at line 269 of file sfmNtk.c.

 {
     if ( iFanin < 0 )
         return;
     assert( Sfm_ObjIsNode(p, iNode) );
     assert( !Sfm_ObjIsPo(p, iFanin) );
     assert( Vec_IntFind( Sfm_ObjFiArray(p, iNode), iFanin ) == -1 );
     assert( Vec_IntFind( Sfm_ObjFoArray(p, iFanin), iNode ) == -1 );
     Vec_IntPush( Sfm_ObjFiArray(p, iNode), iFanin );
     Vec_IntPush( Sfm_ObjFoArray(p, iFanin), iNode );
 }

Sfm_Ntk_t* Sfm_NtkConstruct	(	Vec_Wec_t *	vFanins,
		int	nPis,
		int	nPos,
		Vec_Str_t *	vFixed,
		Vec_Str_t *	vEmpty,
		Vec_Wrd_t *	vTruths
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 167 of file sfmNtk.c.

 {
     Sfm_Ntk_t * p;
     Sfm_CheckConsistency( vFanins, nPis, nPos, vFixed );
     p = ABC_CALLOC( Sfm_Ntk_t, 1 );
     p->nObjs    = Vec_WecSize( vFanins );
     p->nPis     = nPis;
     p->nPos     = nPos;
     p->nNodes   = p->nObjs - p->nPis - p->nPos;
     // user data
     p->vFixed   = vFixed;
     p->vEmpty   = vEmpty;
     p->vTruths  = vTruths;
     p->vFanins  = *vFanins;
     ABC_FREE( vFanins );
     // attributes
     Sfm_CreateFanout( &p->vFanins, &p->vFanouts );
     Sfm_CreateLevel( &p->vFanins, &p->vLevels, vEmpty );
     Sfm_CreateLevelR( &p->vFanouts, &p->vLevelsR, vEmpty );
     Vec_IntFill( &p->vCounts,   p->nObjs,  0 );
     Vec_IntFill( &p->vTravIds,  p->nObjs,  0 );
     Vec_IntFill( &p->vTravIds2, p->nObjs,  0 );
     Vec_IntFill( &p->vId2Var,   2*p->nObjs, -1 );
     Vec_IntFill( &p->vVar2Id,   2*p->nObjs, -1 );
     p->vCover   = Vec_IntAlloc( 1 << 16 );
     p->vCnfs    = Sfm_CreateCnf( p );
     return p;
 }

void Sfm_NtkDeleteObj_rec	(	Sfm_Ntk_t *	p,
		int	iNode
	)

Definition at line 280 of file sfmNtk.c.

 {
     int i, iFanin;
     if ( Sfm_ObjFanoutNum(p, iNode) > 0 || Sfm_ObjIsPi(p, iNode) || Sfm_ObjIsFixed(p, iNode) )
         return;
     assert( Sfm_ObjIsNode(p, iNode) );
     Sfm_ObjForEachFanin( p, iNode, iFanin, i )
     {
         int RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode );  assert( RetValue );
         Sfm_NtkDeleteObj_rec( p, iFanin );
     }
     Vec_IntClear( Sfm_ObjFiArray(p, iNode) );
     Vec_WrdWriteEntry( p->vTruths, iNode, (word)0 );
 }

void Sfm_NtkFree ( Sfm_Ntk_t * p )

Definition at line 213 of file sfmNtk.c.

 {
     // user data
     Vec_StrFree( p->vFixed );
     Vec_StrFreeP( &p->vEmpty );
     Vec_WrdFree( p->vTruths );
     Vec_WecErase( &p->vFanins );
     // attributes
     Vec_WecErase( &p->vFanouts );
     ABC_FREE( p->vLevels.pArray );
     ABC_FREE( p->vLevelsR.pArray );
     ABC_FREE( p->vCounts.pArray );
     ABC_FREE( p->vTravIds.pArray );
     ABC_FREE( p->vTravIds2.pArray );
     ABC_FREE( p->vId2Var.pArray );
     ABC_FREE( p->vVar2Id.pArray );
     Vec_WecFree( p->vCnfs );
     Vec_IntFree( p->vCover );
     // other data
     Vec_IntFreeP( &p->vNodes );
     Vec_IntFreeP( &p->vDivs  );
     Vec_IntFreeP( &p->vRoots );
     Vec_IntFreeP( &p->vTfo   );
     Vec_WrdFreeP( &p->vDivCexes );
     Vec_IntFreeP( &p->vOrder );
     Vec_IntFreeP( &p->vDivVars );
     Vec_IntFreeP( &p->vDivIds );
     Vec_IntFreeP( &p->vLits  );
     Vec_IntFreeP( &p->vValues );
     Vec_WecFreeP( &p->vClauses );
     Vec_IntFreeP( &p->vFaninMap );
     if ( p->pSat  ) sat_solver_delete( p->pSat );
     ABC_FREE( p );
 }

void Sfm_NtkPrepare ( Sfm_Ntk_t * p )

Definition at line 195 of file sfmNtk.c.

 {
     p->nLevelMax = Vec_IntFindMax(&p->vLevels) + p->pPars->nGrowthLevel;
     p->vNodes    = Vec_IntAlloc( 1000 );
     p->vDivs     = Vec_IntAlloc( 100 );
     p->vRoots    = Vec_IntAlloc( 1000 );
     p->vTfo      = Vec_IntAlloc( 1000 );
     p->vDivCexes = Vec_WrdStart( p->pPars->nWinSizeMax );
     p->vOrder    = Vec_IntAlloc( 100 );
     p->vDivVars  = Vec_IntAlloc( 100 );
     p->vDivIds   = Vec_IntAlloc( 1000 );
     p->vLits     = Vec_IntAlloc( 100 );
     p->vValues   = Vec_IntAlloc( 100 );
     p->vClauses  = Vec_WecAlloc( 100 );
     p->vFaninMap = Vec_IntAlloc( 10 );
     p->pSat      = sat_solver_new();
     sat_solver_setnvars( p->pSat, p->pPars->nWinSizeMax );
 }

void Sfm_NtkRemoveFanin	(	Sfm_Ntk_t *	p,
		int	iNode,
		int	iFanin
	)

Function*************************************************************

Synopsis [Performs resubstitution for the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 259 of file sfmNtk.c.

 {
     int RetValue;
     assert( Sfm_ObjIsNode(p, iNode) );
     assert( !Sfm_ObjIsPo(p, iFanin) );
     RetValue = Vec_IntRemove( Sfm_ObjFiArray(p, iNode), iFanin );
     assert( RetValue );
     RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode );
     assert( RetValue );
 }

void Sfm_NtkUpdate	(	Sfm_Ntk_t *	p,
		int	iNode,
		int	f,
		int	iFaninNew,
		word	uTruth
	)

Definition at line 314 of file sfmNtk.c.

 {
     int iFanin = Sfm_ObjFanin( p, iNode, f );
     assert( Sfm_ObjIsNode(p, iNode) );
     assert( iFanin != iFaninNew );
     if ( uTruth == 0 || ~uTruth == 0 )
     {
         Sfm_ObjForEachFanin( p, iNode, iFanin, f )
         {
             int RetValue = Vec_IntRemove( Sfm_ObjFoArray(p, iFanin), iNode );  assert( RetValue );
             Sfm_NtkDeleteObj_rec( p, iFanin );
         }
         Vec_IntClear( Sfm_ObjFiArray(p, iNode) );
     }
     else
     {
         // replace old fanin by new fanin
         Sfm_NtkRemoveFanin( p, iNode, iFanin );
         Sfm_NtkAddFanin( p, iNode, iFaninNew );
         // recursively remove MFFC
         Sfm_NtkDeleteObj_rec( p, iFanin );
     }
     // update logic level
     Sfm_NtkUpdateLevel_rec( p, iNode );
     if ( iFaninNew != -1 )
         Sfm_NtkUpdateLevelR_rec( p, iFaninNew );
     if ( Sfm_ObjFanoutNum(p, iFanin) > 0 )
         Sfm_NtkUpdateLevelR_rec( p, iFanin );
     // update truth table
     Vec_WrdWriteEntry( p->vTruths, iNode, uTruth );
     Sfm_TruthToCnf( uTruth, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
 }

void Sfm_NtkUpdateLevel_rec	(	Sfm_Ntk_t *	p,
		int	iNode
	)

Definition at line 294 of file sfmNtk.c.

 {
     int i, iFanout;
     int LevelNew = Sfm_ObjLevelNew( Sfm_ObjFiArray(p, iNode), &p->vLevels, Sfm_ObjAddsLevel(p, iNode) );
     if ( LevelNew == Sfm_ObjLevel(p, iNode) )
         return;
     Sfm_ObjSetLevel( p, iNode, LevelNew );
     Sfm_ObjForEachFanout( p, iNode, iFanout, i )
         Sfm_NtkUpdateLevel_rec( p, iFanout );
 }

void Sfm_NtkUpdateLevelR_rec	(	Sfm_Ntk_t *	p,
		int	iNode
	)

Definition at line 304 of file sfmNtk.c.

 {
     int i, iFanin;
     int LevelNew = Sfm_ObjLevelNewR( Sfm_ObjFoArray(p, iNode), &p->vLevelsR, Sfm_ObjAddsLevel(p, iNode) );
     if ( LevelNew == Sfm_ObjLevelR(p, iNode) )
         return;
     Sfm_ObjSetLevelR( p, iNode, LevelNew );
     Sfm_ObjForEachFanin( p, iNode, iFanin, i )
         Sfm_NtkUpdateLevelR_rec( p, iFanin );
 }

static int Sfm_ObjLevelNew	(	Vec_Int_t *	vArray,
		Vec_Int_t *	vLevels,
		int	fAddLevel
	)

inlinestatic

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 111 of file sfmNtk.c.

 {
     int k, Fanin, Level = 0;
     Vec_IntForEachEntry( vArray, Fanin, k )
         Level = Abc_MaxInt( Level, Vec_IntEntry(vLevels, Fanin) );
     return Level + fAddLevel;
 }

static int Sfm_ObjLevelNewR	(	Vec_Int_t *	vArray,
		Vec_Int_t *	vLevelsR,
		int	fAddLevel
	)

inlinestatic

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 139 of file sfmNtk.c.

 {
     int k, Fanout, LevelR = 0;
     Vec_IntForEachEntry( vArray, Fanout, k )
         LevelR = Abc_MaxInt( LevelR, Vec_IntEntry(vLevelsR, Fanout) );
     return LevelR + fAddLevel;
 }

Functions

Function Documentation