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

merge

This commit is contained in:
Yen-Sheng Ho 2017-03-31 07:42:06 -07:00
parent 16ef095f9c 96056c377c
commit 04bd8631e0
7 changed files with 705 additions and 510 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

332
src/base/acb/acb.h
View File

@ -30,6 +30,7 @@
#include "misc/util/utilNam.h"
#include "misc/vec/vecHash.h"
#include "aig/miniaig/abcOper.h"
#include "misc/vec/vecQue.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@ -70,7 +71,6 @@ struct Acb_Ntk_t_
Vec_Str_t vObjType; // type
Vec_Int_t vObjFans; // fanin offsets
Vec_Int_t vFanSto; // fanin storage
Vec_Wec_t vFanouts; // fanouts
// optional
Vec_Int_t vObjCopy; // copy
Vec_Int_t vObjFunc; // function
@ -88,19 +88,20 @@ struct Acb_Ntk_t_
Vec_Int_t vLevelR; // level
Vec_Int_t vPathD; // path
Vec_Int_t vPathR; // path
Vec_Wec_t vClauses;
Vec_Wec_t vCnfs;
Vec_Int_t vCover;
Vec_Flt_t vCounts; // priority counts
Vec_Wec_t vFanouts; // fanouts
Vec_Wec_t vCnfs; // CNF
// other
Vec_Int_t vArray0;
Vec_Int_t vArray1;
Vec_Int_t vArray2;
Vec_Que_t * vQue; // temporary
Vec_Int_t vCover; // temporary
Vec_Int_t vArray0; // temporary
Vec_Int_t vArray1; // temporary
Vec_Int_t vArray2; // temporary
};
// design
struct Acb_Man_t_
{
// design names
char * pName; // design name
char * pSpec; // spec file name
Abc_Nam_t * pStrs; // string manager
@ -185,7 +186,7 @@ static inline int Acb_NtkNodeNum( Acb_Ntk_t * p ) { r
static inline int Acb_NtkSeqNum( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vSeq); }
static inline void Acb_NtkCleanObjCopies( Acb_Ntk_t * p ) { Vec_IntFill(&p->vObjCopy, Vec_StrCap(&p->vObjType), -1); }
static inline void Acb_NtkCleanObjFuncs( Acb_Ntk_t * p ) { Vec_IntFill(&p->vObjFunc, Vec_StrCap(&p->vObjType), 0); }
static inline void Acb_NtkCleanObjFuncs( Acb_Ntk_t * p ) { Vec_IntFill(&p->vObjFunc, Vec_StrCap(&p->vObjType), -1); }
static inline void Acb_NtkCleanObjWeights( Acb_Ntk_t * p ) { Vec_IntFill(&p->vObjWeight,Vec_StrCap(&p->vObjType), 0); }
static inline void Acb_NtkCleanObjTruths( Acb_Ntk_t * p ) { Vec_WrdFill(&p->vObjTruth, Vec_StrCap(&p->vObjType), 0); }
static inline void Acb_NtkCleanObjNames( Acb_Ntk_t * p ) { Vec_IntFill(&p->vObjName, Vec_StrCap(&p->vObjType), 0); }
@ -196,114 +197,127 @@ static inline void Acb_NtkCleanObjLevelD( Acb_Ntk_t * p ) { V
static inline void Acb_NtkCleanObjLevelR( Acb_Ntk_t * p ) { Vec_IntFill(&p->vLevelR, Vec_StrCap(&p->vObjType), 0); }
static inline void Acb_NtkCleanObjPathD( Acb_Ntk_t * p ) { Vec_IntFill(&p->vPathD, Vec_StrCap(&p->vObjType), 0); }
static inline void Acb_NtkCleanObjPathR( Acb_Ntk_t * p ) { Vec_IntFill(&p->vPathR, Vec_StrCap(&p->vObjType), 0); }
static inline void Acb_NtkCleanObjCounts( Acb_Ntk_t * p ) { Vec_FltFill(&p->vCounts, Vec_StrCap(&p->vObjType), 0); }
static inline void Acb_NtkCleanObjFanout( Acb_Ntk_t * p ) { Vec_WecInit(&p->vFanouts, Vec_StrCap(&p->vObjType) ); }
static inline void Acb_NtkCleanObjCnfs( Acb_Ntk_t * p ) { Vec_WecInit(&p->vCnfs, Vec_StrCap(&p->vObjType) ); }
static inline int Acb_NtkHasObjCopies( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjCopy) > 0; }
static inline int Acb_NtkHasObjFuncs( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjFunc) > 0; }
static inline int Acb_NtkHasObjWeights( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjWeight)> 0; }
static inline int Acb_NtkHasObjTruths( Acb_Ntk_t * p ) { return Vec_WrdSize(&p->vObjTruth) > 0; }
static inline int Acb_NtkHasObjNames( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjName) > 0; }
static inline int Acb_NtkHasObjRanges( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjRange) > 0; }
static inline int Acb_NtkHasObjTravs( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjTrav) > 0; }
static inline int Acb_NtkHasObjAttrs( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjAttr) > 0; }
static inline int Acb_NtkHasObjLevelD( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vLevelD) > 0; }
static inline int Acb_NtkHasObjLevelR( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vLevelR) > 0; }
static inline int Acb_NtkHasObjPathD( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vPathD) > 0; }
static inline int Acb_NtkHasObjPathR( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vPathR) > 0; }
static inline int Acb_NtkHasObjCopies( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjCopy) > 0; }
static inline int Acb_NtkHasObjFuncs( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjFunc) > 0; }
static inline int Acb_NtkHasObjWeights( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjWeight)> 0; }
static inline int Acb_NtkHasObjTruths( Acb_Ntk_t * p ) { return Vec_WrdSize(&p->vObjTruth) > 0; }
static inline int Acb_NtkHasObjNames( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjName) > 0; }
static inline int Acb_NtkHasObjRanges( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjRange) > 0; }
static inline int Acb_NtkHasObjTravs( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjTrav) > 0; }
static inline int Acb_NtkHasObjAttrs( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjAttr) > 0; }
static inline int Acb_NtkHasObjLevelD( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vLevelD) > 0; }
static inline int Acb_NtkHasObjLevelR( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vLevelR) > 0; }
static inline int Acb_NtkHasObjPathD( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vPathD) > 0; }
static inline int Acb_NtkHasObjPathR( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vPathR) > 0; }
static inline int Acb_NtkHasObjCounts( Acb_Ntk_t * p ) { return Vec_FltSize(&p->vCounts) > 0; }
static inline int Acb_NtkHasObjFanout( Acb_Ntk_t * p ) { return Vec_WecSize(&p->vFanouts) > 0; }
static inline int Acb_NtkHasObjCnfs( Acb_Ntk_t * p ) { return Vec_WecSize(&p->vCnfs) > 0; }
static inline void Acb_NtkFreeObjCopies( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjCopy); }
static inline void Acb_NtkFreeObjFuncs( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjFunc); }
static inline void Acb_NtkFreeObjWeights( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjWeight); }
static inline void Acb_NtkFreeObjTruths( Acb_Ntk_t * p ) { Vec_WrdErase(&p->vObjTruth); }
static inline void Acb_NtkFreeObjNames( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjName); }
static inline void Acb_NtkFreeObjRanges( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjRange); }
static inline void Acb_NtkFreeObjTravs( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjTrav); }
static inline void Acb_NtkFreeObjAttrs( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjAttr); }
static inline void Acb_NtkFreeObjLevelD( Acb_Ntk_t * p ) { Vec_IntErase(&p->vLevelD); }
static inline void Acb_NtkFreeObjLevelR( Acb_Ntk_t * p ) { Vec_IntErase(&p->vLevelR); }
static inline void Acb_NtkFreeObjPathD( Acb_Ntk_t * p ) { Vec_IntErase(&p->vPathD); }
static inline void Acb_NtkFreeObjPathR( Acb_Ntk_t * p ) { Vec_IntErase(&p->vPathR); }
static inline void Acb_NtkFreeObjCopies( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjCopy); }
static inline void Acb_NtkFreeObjFuncs( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjFunc); }
static inline void Acb_NtkFreeObjWeights( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjWeight); }
static inline void Acb_NtkFreeObjTruths( Acb_Ntk_t * p ) { Vec_WrdErase(&p->vObjTruth); }
static inline void Acb_NtkFreeObjNames( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjName); }
static inline void Acb_NtkFreeObjRanges( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjRange); }
static inline void Acb_NtkFreeObjTravs( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjTrav); }
static inline void Acb_NtkFreeObjAttrs( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjAttr); }
static inline void Acb_NtkFreeObjLevelD( Acb_Ntk_t * p ) { Vec_IntErase(&p->vLevelD); }
static inline void Acb_NtkFreeObjLevelR( Acb_Ntk_t * p ) { Vec_IntErase(&p->vLevelR); }
static inline void Acb_NtkFreeObjPathD( Acb_Ntk_t * p ) { Vec_IntErase(&p->vPathD); }
static inline void Acb_NtkFreeObjPathR( Acb_Ntk_t * p ) { Vec_IntErase(&p->vPathR); }
static inline void Acb_NtkFreeObjCounts( Acb_Ntk_t * p ) { Vec_FltErase(&p->vCounts); }
static inline void Acb_NtkFreeObjFanout( Acb_Ntk_t * p ) { Vec_WecErase(&p->vFanouts); }
static inline void Acb_NtkFreeObjCnfs( Acb_Ntk_t * p ) { Vec_WecErase(&p->vCnfs); }
static inline Acb_ObjType_t Acb_ObjType( Acb_Ntk_t * p, int i ) { assert(i>0); return (Acb_ObjType_t)(int)(unsigned char)Vec_StrEntry(&p->vObjType, i); }
static inline void Acb_ObjCleanType( Acb_Ntk_t * p, int i ) { assert(i>0); Vec_StrWriteEntry( &p->vObjType, i, (char)ABC_OPER_NONE ); }
static inline int Acb_TypeIsSeq( Acb_ObjType_t Type ) { return Type >= ABC_OPER_RAM && Type <= ABC_OPER_DFFRS; }
static inline int Acb_TypeIsUnary( Acb_ObjType_t Type ) { return Type == ABC_OPER_BIT_BUF || Type == ABC_OPER_BIT_INV || Type == ABC_OPER_LOGIC_NOT || Type == ABC_OPER_ARI_MIN || Type == ABC_OPER_ARI_SQRT || Type == ABC_OPER_ARI_ABS || (Type >= ABC_OPER_RED_AND && Type <= ABC_OPER_RED_NXOR); }
static inline int Acb_TypeIsMux( Acb_ObjType_t Type ) { return Type == ABC_OPER_BIT_MUX || Type == ABC_OPER_SEL_NMUX || Type == ABC_OPER_SEL_SEL || Type == ABC_OPER_SEL_PSEL; }
static inline Acb_ObjType_t Acb_ObjType( Acb_Ntk_t * p, int i ) { assert(i>0); return (Acb_ObjType_t)(int)(unsigned char)Vec_StrEntry(&p->vObjType, i); }
static inline void Acb_ObjCleanType( Acb_Ntk_t * p, int i ) { assert(i>0); Vec_StrWriteEntry( &p->vObjType, i, (char)ABC_OPER_NONE ); }
static inline int Acb_TypeIsSeq( Acb_ObjType_t Type ) { return Type >= ABC_OPER_RAM && Type <= ABC_OPER_DFFRS; }
static inline int Acb_TypeIsUnary( Acb_ObjType_t Type ) { return Type == ABC_OPER_BIT_BUF || Type == ABC_OPER_BIT_INV || Type == ABC_OPER_LOGIC_NOT || Type == ABC_OPER_ARI_MIN || Type == ABC_OPER_ARI_SQRT || Type == ABC_OPER_ARI_ABS || (Type >= ABC_OPER_RED_AND && Type <= ABC_OPER_RED_NXOR); }
static inline int Acb_TypeIsMux( Acb_ObjType_t Type ) { return Type == ABC_OPER_BIT_MUX || Type == ABC_OPER_SEL_NMUX || Type == ABC_OPER_SEL_SEL || Type == ABC_OPER_SEL_PSEL; }
static inline int Acb_ObjIsCi( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_CI; }
static inline int Acb_ObjIsCo( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_CO; }
static inline int Acb_ObjIsCio( Acb_Ntk_t * p, int i ) { return Acb_ObjIsCi(p, i) || Acb_ObjIsCo(p, i); }
static inline int Acb_ObjIsFon( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_FON; }
static inline int Acb_ObjIsBox( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_BOX; }
static inline int Acb_ObjIsGate( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_GATE; }
static inline int Acb_ObjIsSlice( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_SLICE; }
static inline int Acb_ObjIsConcat( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_CONCAT; }
static inline int Acb_ObjIsUnary( Acb_Ntk_t * p, int i ) { return Acb_TypeIsUnary(Acb_ObjType(p, i)); }
static inline int Acb_ObjIsCi( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_CI; }
static inline int Acb_ObjIsCo( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_CO; }
static inline int Acb_ObjIsCio( Acb_Ntk_t * p, int i ) { return Acb_ObjIsCi(p, i) || Acb_ObjIsCo(p, i); }
static inline int Acb_ObjIsFon( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_FON; }
static inline int Acb_ObjIsBox( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_BOX; }
static inline int Acb_ObjIsGate( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_GATE; }
static inline int Acb_ObjIsSlice( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_SLICE; }
static inline int Acb_ObjIsConcat( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_CONCAT; }
static inline int Acb_ObjIsUnary( Acb_Ntk_t * p, int i ) { return Acb_TypeIsUnary(Acb_ObjType(p, i)); }
static inline int Acb_ObjFanOffset( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vObjFans, i); }
static inline int * Acb_ObjFanins( Acb_Ntk_t * p, int i ) { return Vec_IntEntryP(&p->vFanSto, Acb_ObjFanOffset(p, i)); }
static inline int Acb_ObjFanin( Acb_Ntk_t * p, int i, int k ) { return Acb_ObjFanins(p, i)[k+1]; }
static inline int Acb_ObjFaninNum( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[0]; }
static inline int Acb_ObjFanoutNum( Acb_Ntk_t * p, int i ) { return Vec_IntSize( Vec_WecEntry(&p->vFanouts, i) ); }
static inline Vec_Int_t * Acb_ObjFanoutVec( Acb_Ntk_t * p, int i ) { return Vec_WecEntry( &p->vFanouts, i ); }
static inline int Acb_ObjFanin0( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[1]; }
static inline int Acb_ObjCioId( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[2]; }
static inline int Acb_ObjFanOffset( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vObjFans, i); }
static inline int * Acb_ObjFanins( Acb_Ntk_t * p, int i ) { return Vec_IntEntryP(&p->vFanSto, Acb_ObjFanOffset(p, i)); }
static inline int Acb_ObjFanin( Acb_Ntk_t * p, int i, int k ) { return Acb_ObjFanins(p, i)[k+1]; }
static inline int Acb_ObjFaninNum( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[0]; }
static inline int Acb_ObjFanoutNum( Acb_Ntk_t * p, int i ) { return Vec_IntSize( Vec_WecEntry(&p->vFanouts, i) ); }
static inline Vec_Int_t * Acb_ObjFanoutVec( Acb_Ntk_t * p, int i ) { return Vec_WecEntry( &p->vFanouts, i ); }
static inline int Acb_ObjFanin0( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[1]; }
static inline int Acb_ObjCioId( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[2]; }
static inline int Acb_ObjCopy( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjCopies(p) ); return Vec_IntGetEntryFull(&p->vObjCopy, i); }
static inline int Acb_ObjFunc( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjFuncs(p) ); return Vec_IntGetEntry(&p->vObjFunc, i); }
static inline int Acb_ObjWeight( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjWeights(p) );return Vec_IntGetEntry(&p->vObjWeight, i); }
static inline word Acb_ObjTruth( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjTruths(p) ); return Vec_WrdGetEntry(&p->vObjTruth, i); }
static inline word * Acb_ObjTruthP( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjTruths(p) ); return Vec_WrdEntryP(&p->vObjTruth, i); }
static inline int Acb_ObjName( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjNames(p) ); return Vec_IntGetEntry(&p->vObjName, i); }
static inline char * Acb_ObjNameStr( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_NtkStr(p, Acb_ObjName(p, i)); }
static inline int Acb_ObjAttr( Acb_Ntk_t * p, int i ) { assert(i>=0); return Acb_NtkHasObjAttrs(p) ? Vec_IntGetEntry(&p->vObjAttr, i) : 0; }
static inline int Acb_ObjAttrSize( Acb_Ntk_t * p, int i ) { assert(i>=0); return Acb_ObjAttr(p, i) ? Vec_IntEntry(&p->vAttrSto, Acb_ObjAttr(p, i)) : 0; }
static inline int * Acb_ObjAttrArray( Acb_Ntk_t * p, int i ) { assert(i>=0); return Acb_ObjAttr(p, i) ? Vec_IntEntryP(&p->vAttrSto, Acb_ObjAttr(p, i)+1) : NULL; }
static inline int Acb_ObjAttrValue( Acb_Ntk_t * p, int i, int x ) { int k, s = Acb_ObjAttrSize(p, i), * a = Acb_ObjAttrArray(p, i); for ( k = 0; k < s; k += 2) if (a[k] == x) return a[k+1]; return 0; }
static inline int Acb_ObjLevelD( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vLevelD, i); }
static inline int Acb_ObjLevelR( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vLevelR, i); }
static inline int Acb_ObjPathD( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vPathD, i); }
static inline int Acb_ObjPathR( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vPathR, i); }
static inline int Acb_ObjCopy( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjCopies(p) ); return Vec_IntEntry(&p->vObjCopy, i); }
static inline int Acb_ObjFunc( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjFuncs(p) ); return Vec_IntEntry(&p->vObjFunc, i); }
static inline int Acb_ObjWeight( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjWeights(p) );return Vec_IntEntry(&p->vObjWeight, i); }
static inline word Acb_ObjTruth( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjTruths(p) ); return Vec_WrdEntry(&p->vObjTruth, i); }
static inline word * Acb_ObjTruthP( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjTruths(p) ); return Vec_WrdEntryP(&p->vObjTruth, i); }
static inline int Acb_ObjName( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjNames(p) ); return Vec_IntEntry(&p->vObjName, i); }
static inline char * Acb_ObjNameStr( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_NtkStr(p, Acb_ObjName(p, i)); }
static inline int Acb_ObjAttr( Acb_Ntk_t * p, int i ) { assert(i>=0); return Acb_NtkHasObjAttrs(p) ? Vec_IntEntry(&p->vObjAttr, i) : 0; }
static inline int Acb_ObjAttrSize( Acb_Ntk_t * p, int i ) { assert(i>=0); return Acb_ObjAttr(p, i) ? Vec_IntEntry(&p->vAttrSto, Acb_ObjAttr(p, i)) : 0; }
static inline int * Acb_ObjAttrArray( Acb_Ntk_t * p, int i ) { assert(i>=0); return Acb_ObjAttr(p, i) ? Vec_IntEntryP(&p->vAttrSto, Acb_ObjAttr(p, i)+1) : NULL; }
static inline int Acb_ObjAttrValue( Acb_Ntk_t * p, int i, int x ) { int k, s = Acb_ObjAttrSize(p, i), * a = Acb_ObjAttrArray(p, i); for ( k = 0; k < s; k += 2) if (a[k] == x) return a[k+1]; return 0; }
static inline int Acb_ObjLevelD( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vLevelD, i); }
static inline int Acb_ObjLevelR( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vLevelR, i); }
static inline int Acb_ObjPathD( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vPathD, i); }
static inline int Acb_ObjPathR( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vPathR, i); }
static inline float Acb_ObjCounts( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_FltEntry(&p->vCounts, i); }
static inline Vec_Int_t * Acb_ObjFanout( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_WecEntry(&p->vFanouts, i); }
static inline Vec_Str_t * Acb_ObjCnfs( Acb_Ntk_t * p, int i ) { assert(i>0); return (Vec_Str_t *)Vec_WecEntry(&p->vCnfs, i); }
static inline void Acb_ObjSetCopy( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjCopy(p, i) == -1); Vec_IntSetEntry( &p->vObjCopy, i, x ); }
static inline void Acb_ObjSetFunc( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjFunc(p, i) == 0); Vec_IntSetEntry( &p->vObjFunc, i, x ); }
static inline void Acb_ObjSetWeight( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjWeight(p, i) == 0); Vec_IntSetEntry( &p->vObjWeight, i, x ); }
static inline void Acb_ObjSetTruth( Acb_Ntk_t * p, int i, word x ) { assert(Acb_ObjTruth(p, i) == 0);Vec_WrdSetEntry( &p->vObjTruth, i, x ); }
static inline void Acb_ObjSetName( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjName(p, i) == 0); Vec_IntSetEntry( &p->vObjName, i, x ); }
static inline void Acb_ObjSetAttrs( Acb_Ntk_t * p, int i, int * a, int s ) { assert(Acb_ObjAttr(p, i) == 0); if ( !a ) return; Vec_IntSetEntry(&p->vObjAttr, i, Vec_IntSize(&p->vAttrSto)); Vec_IntPush(&p->vAttrSto, s); Vec_IntPushArray(&p->vAttrSto, a, s); }
static inline int Acb_ObjSetLevelD( Acb_Ntk_t * p, int i, int x ) { Vec_IntSetEntry( &p->vLevelD, i, x ); return x; }
static inline int Acb_ObjSetLevelR( Acb_Ntk_t * p, int i, int x ) { Vec_IntSetEntry( &p->vLevelR, i, x ); return x; }
static inline int Acb_ObjSetPathD( Acb_Ntk_t * p, int i, int x ) { Vec_IntSetEntry( &p->vPathD, i, x ); return x; }
static inline int Acb_ObjSetPathR( Acb_Ntk_t * p, int i, int x ) { Vec_IntSetEntry( &p->vPathR, i, x ); return x; }
static inline int Acb_ObjUpdateLevelD( Acb_Ntk_t * p, int i, int x ) { Vec_IntUpdateEntry( &p->vLevelD, i, x ); return x; }
static inline int Acb_ObjUpdateLevelR( Acb_Ntk_t * p, int i, int x ) { Vec_IntUpdateEntry( &p->vLevelR, i, x ); return x; }
static inline int Acb_ObjAddToPathD( Acb_Ntk_t * p, int i, int x ) { Vec_IntAddToEntry( &p->vPathD, i, x ); return x; }
static inline int Acb_ObjAddToPathR( Acb_Ntk_t * p, int i, int x ) { Vec_IntAddToEntry( &p->vPathR, i, x ); return x; }
static inline void Acb_ObjSetCopy( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjCopy(p, i) == -1); Vec_IntWriteEntry( &p->vObjCopy, i, x ); }
static inline void Acb_ObjSetFunc( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjFunc(p, i) == -1); Vec_IntWriteEntry( &p->vObjFunc, i, x ); }
static inline void Acb_ObjSetWeight( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjWeight(p, i)== 0); Vec_IntWriteEntry( &p->vObjWeight, i, x ); }
static inline void Acb_ObjSetTruth( Acb_Ntk_t * p, int i, word x ) { assert(Acb_ObjTruth(p, i) == 0); Vec_WrdWriteEntry( &p->vObjTruth, i, x ); }
static inline void Acb_ObjSetName( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjName(p, i) == 0); Vec_IntWriteEntry( &p->vObjName, i, x ); }
static inline void Acb_ObjSetAttrs( Acb_Ntk_t * p, int i, int * a, int s ) { assert(Acb_ObjAttr(p, i) == 0); if ( !a ) return; Vec_IntWriteEntry(&p->vObjAttr, i, Vec_IntSize(&p->vAttrSto)); Vec_IntPush(&p->vAttrSto, s); Vec_IntPushArray(&p->vAttrSto, a, s); }
static inline int Acb_ObjSetLevelD( Acb_Ntk_t * p, int i, int x ) { Vec_IntWriteEntry( &p->vLevelD, i, x ); return x; }
static inline int Acb_ObjSetLevelR( Acb_Ntk_t * p, int i, int x ) { Vec_IntWriteEntry( &p->vLevelR, i, x ); return x; }
static inline int Acb_ObjSetPathD( Acb_Ntk_t * p, int i, int x ) { Vec_IntWriteEntry( &p->vPathD, i, x ); return x; }
static inline int Acb_ObjSetPathR( Acb_Ntk_t * p, int i, int x ) { Vec_IntWriteEntry( &p->vPathR, i, x ); return x; }
static inline float Acb_ObjSetCounts( Acb_Ntk_t * p, int i, float x ) { Vec_FltWriteEntry( &p->vCounts, i, x ); return x; }
static inline int Acb_ObjUpdateLevelD( Acb_Ntk_t * p, int i, int x ) { Vec_IntUpdateEntry( &p->vLevelD, i, x ); return x; }
static inline int Acb_ObjUpdateLevelR( Acb_Ntk_t * p, int i, int x ) { Vec_IntUpdateEntry( &p->vLevelR, i, x ); return x; }
static inline int Acb_ObjAddToPathD( Acb_Ntk_t * p, int i, int x ) { Vec_IntAddToEntry( &p->vPathD, i, x ); return x; }
static inline int Acb_ObjAddToPathR( Acb_Ntk_t * p, int i, int x ) { Vec_IntAddToEntry( &p->vPathR, i, x ); return x; }
static inline int Acb_ObjNtkId( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_ObjIsBox(p, i) ? Acb_ObjFanin(p, i, Acb_ObjFaninNum(p, i)) : 0; }
static inline Acb_Ntk_t * Acb_ObjNtk( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_NtkNtk(p, Acb_ObjNtkId(p, i)); }
static inline int Acb_ObjIsSeq( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_ObjIsBox(p, i) ? Acb_ObjNtk(p, i)->fSeq : Acb_TypeIsSeq(Acb_ObjType(p, i)); }
static inline int Acb_ObjNtkId( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_ObjIsBox(p, i) ? Acb_ObjFanin(p, i, Acb_ObjFaninNum(p, i)) : 0; }
static inline Acb_Ntk_t * Acb_ObjNtk( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_NtkNtk(p, Acb_ObjNtkId(p, i)); }
static inline int Acb_ObjIsSeq( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_ObjIsBox(p, i) ? Acb_ObjNtk(p, i)->fSeq : Acb_TypeIsSeq(Acb_ObjType(p, i)); }
static inline int Acb_ObjRangeId( Acb_Ntk_t * p, int i ) { return Acb_NtkHasObjRanges(p) ? Vec_IntGetEntry(&p->vObjRange, i) : 0; }
static inline int Acb_ObjRange( Acb_Ntk_t * p, int i ) { return Abc_Lit2Var( Acb_ObjRangeId(p, i) ); }
static inline int Acb_ObjLeft( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeLeft(p, Acb_ObjRange(p, i)); }
static inline int Acb_ObjRight( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeRight(p, Acb_ObjRange(p, i)); }
static inline int Acb_ObjSigned( Acb_Ntk_t * p, int i ) { return Abc_LitIsCompl(Acb_ObjRangeId(p, i)); }
static inline int Acb_ObjRangeSize( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeSize(p, Acb_ObjRange(p, i)); }
static inline void Acb_ObjSetRangeSign( Acb_Ntk_t * p, int i, int x ) { assert(Acb_NtkHasObjRanges(p)); Vec_IntSetEntry(&p->vObjRange, i, x); }
static inline void Acb_ObjSetRange( Acb_Ntk_t * p, int i, int x ) { assert(Acb_NtkHasObjRanges(p)); Vec_IntSetEntry(&p->vObjRange, i, Abc_Var2Lit(x,0)); }
static inline void Acb_ObjHashRange( Acb_Ntk_t * p, int i, int l, int r ) { Acb_ObjSetRange( p, i, Acb_NtkHashRange(p, l, r) ); }
static inline int Acb_ObjRangeSign( Acb_Ntk_t * p, int i ) { return Abc_Var2Lit( Acb_ObjRangeSize(p, i), Acb_ObjSigned(p, i) ); }
static inline int Acb_ObjRangeId( Acb_Ntk_t * p, int i ) { return Acb_NtkHasObjRanges(p) ? Vec_IntEntry(&p->vObjRange, i) : 0; }
static inline int Acb_ObjRange( Acb_Ntk_t * p, int i ) { return Abc_Lit2Var( Acb_ObjRangeId(p, i) ); }
static inline int Acb_ObjLeft( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeLeft(p, Acb_ObjRange(p, i)); }
static inline int Acb_ObjRight( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeRight(p, Acb_ObjRange(p, i)); }
static inline int Acb_ObjSigned( Acb_Ntk_t * p, int i ) { return Abc_LitIsCompl(Acb_ObjRangeId(p, i)); }
static inline int Acb_ObjRangeSize( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeSize(p, Acb_ObjRange(p, i)); }
static inline void Acb_ObjSetRangeSign( Acb_Ntk_t * p, int i, int x ) { assert(Acb_NtkHasObjRanges(p)); Vec_IntWriteEntry(&p->vObjRange, i, x); }
static inline void Acb_ObjSetRange( Acb_Ntk_t * p, int i, int x ) { assert(Acb_NtkHasObjRanges(p)); Vec_IntWriteEntry(&p->vObjRange, i, Abc_Var2Lit(x,0)); }
static inline void Acb_ObjHashRange( Acb_Ntk_t * p, int i, int l, int r ) { Acb_ObjSetRange( p, i, Acb_NtkHashRange(p, l, r) ); }
static inline int Acb_ObjRangeSign( Acb_Ntk_t * p, int i ) { return Abc_Var2Lit( Acb_ObjRangeSize(p, i), Acb_ObjSigned(p, i) ); }
static inline int Acb_ObjTravId( Acb_Ntk_t * p, int i ) { return Vec_IntGetEntry(&p->vObjTrav, i); }
static inline int Acb_ObjTravIdDiff( Acb_Ntk_t * p, int i ) { return p->nObjTravs - Vec_IntGetEntry(&p->vObjTrav, i); }
static inline int Acb_ObjIsTravIdCur( Acb_Ntk_t * p, int i ) { return Acb_ObjTravId(p, i) == p->nObjTravs; }
static inline int Acb_ObjIsTravIdPrev( Acb_Ntk_t * p, int i ) { return Acb_ObjTravId(p, i) == p->nObjTravs-1; }
static inline int Acb_ObjIsTravIdDiff( Acb_Ntk_t * p, int i, int d ) { return Acb_ObjTravId(p, i) == p->nObjTravs-d; }
static inline int Acb_ObjSetTravIdCur( Acb_Ntk_t * p, int i ) { int r = Acb_ObjIsTravIdCur(p, i); Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs); return r; }
static inline int Acb_ObjSetTravIdPrev( Acb_Ntk_t * p, int i ) { int r = Acb_ObjIsTravIdPrev(p, i); Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs-1); return r; }
static inline int Acb_ObjSetTravIdDiff( Acb_Ntk_t * p, int i, int d ) { int r = Acb_ObjTravIdDiff(p, i); Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs-d); return r; }
static inline int Acb_NtkTravId( Acb_Ntk_t * p ) { return p->nObjTravs; }
static inline void Acb_NtkIncTravId( Acb_Ntk_t * p ) { if ( !Acb_NtkHasObjTravs(p) ) Acb_NtkCleanObjTravs(p); p->nObjTravs++; }
static inline int Acb_ObjTravId( Acb_Ntk_t * p, int i ) { return Vec_IntEntry(&p->vObjTrav, i); }
static inline int Acb_ObjTravIdDiff( Acb_Ntk_t * p, int i ) { return p->nObjTravs - Vec_IntEntry(&p->vObjTrav, i); }
static inline int Acb_ObjIsTravIdCur( Acb_Ntk_t * p, int i ) { return Acb_ObjTravId(p, i) == p->nObjTravs; }
static inline int Acb_ObjIsTravIdPrev( Acb_Ntk_t * p, int i ) { return Acb_ObjTravId(p, i) == p->nObjTravs-1; }
static inline int Acb_ObjIsTravIdDiff( Acb_Ntk_t * p, int i, int d ) { return Acb_ObjTravId(p, i) == p->nObjTravs-d; }
static inline int Acb_ObjSetTravIdCur( Acb_Ntk_t * p, int i ) { int r = Acb_ObjIsTravIdCur(p, i); Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs); return r; }
static inline int Acb_ObjSetTravIdPrev( Acb_Ntk_t * p, int i ) { int r = Acb_ObjIsTravIdPrev(p, i); Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs-1); return r; }
static inline int Acb_ObjSetTravIdDiff( Acb_Ntk_t * p, int i, int d ) { int r = Acb_ObjTravIdDiff(p, i); Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs-d); return r; }
static inline int Acb_NtkTravId( Acb_Ntk_t * p ) { return p->nObjTravs; }
static inline void Acb_NtkIncTravId( Acb_Ntk_t * p ) { if ( !Acb_NtkHasObjTravs(p) ) Acb_NtkCleanObjTravs(p); p->nObjTravs++; }
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
@ -393,6 +407,13 @@ static inline void Acb_ObjAddFanin( Acb_Ntk_t * p, int iObj, int iFanin )
assert( pFanins[ 1 + pFanins[0] ] == -1 );
pFanins[ 1 + pFanins[0]++ ] = iFanin;
}
static inline void Acb_ObjAddFanins( Acb_Ntk_t * p, int iObj, Vec_Int_t * vFanins )
{
int i, iFanin;
if ( vFanins )
Vec_IntForEachEntry( vFanins, iFanin, i )
Acb_ObjAddFanin( p, iObj, iFanin );
}
static inline void Acb_ObjSetNtkId( Acb_Ntk_t * p, int iObj, int iNtk ) // should be called after fanins are added
{
int * pFanins = Acb_ObjFanins( p, iObj );
@ -438,6 +459,23 @@ static inline int Acb_ObjAlloc( Acb_Ntk_t * p, Acb_ObjType_t Type, int nFans, in
assert( !Acb_ObjIsBox(p, iObj) || nFons > 0 );
for ( i = 0; i < nFons; i++ )
Acb_ObjAddFanin( p, Acb_ObjAlloc(p, ABC_OPER_FON, 1, 0), iObj );
// extend storage
if ( Acb_NtkHasObjCopies(p) ) Vec_IntPush(&p->vObjCopy , -1);
if ( Acb_NtkHasObjFuncs(p) ) Vec_IntPush(&p->vObjFunc , -1);
if ( Acb_NtkHasObjWeights(p)) Vec_IntPush(&p->vObjWeight, 0);
if ( Acb_NtkHasObjTruths(p) ) Vec_WrdPush(&p->vObjTruth , 0);
if ( Acb_NtkHasObjNames(p) ) Vec_IntPush(&p->vObjName , 0);
if ( Acb_NtkHasObjRanges(p) ) Vec_IntPush(&p->vObjRange , 0);
if ( Acb_NtkHasObjTravs(p) ) Vec_IntPush(&p->vObjTrav , 0);
if ( Acb_NtkHasObjAttrs(p) ) Vec_IntPush(&p->vObjAttr , 0);
if ( Acb_NtkHasObjLevelD(p) ) Vec_IntPush(&p->vLevelD , 0);
if ( Acb_NtkHasObjLevelR(p) ) Vec_IntPush(&p->vLevelR , 0);
if ( Acb_NtkHasObjPathD(p) ) Vec_IntPush(&p->vPathD , 0);
if ( Acb_NtkHasObjPathR(p) ) Vec_IntPush(&p->vPathR , 0);
if ( Acb_NtkHasObjCounts(p) ) Vec_FltPush(&p->vCounts , 0);
if ( Acb_NtkHasObjFanout(p) ) Vec_WecPushLevel(&p->vFanouts);
if ( Acb_NtkHasObjCnfs(p) ) Vec_WecPushLevel(&p->vCnfs);
if ( p->vQue ) Vec_QueSetPriority( p->vQue, Vec_FltArrayP(&p->vCounts) );
return iObj;
}
static inline int Acb_ObjDup( Acb_Ntk_t * pNew, Acb_Ntk_t * p, int i )
@ -455,6 +493,25 @@ static inline void Acb_ObjDelete( Acb_Ntk_t * p, int iObj )
Acb_ObjForEachFon( p, iObj, i )
Acb_ObjCleanType( p, i );
}
static inline void Acb_ObjAddFaninFanout( Acb_Ntk_t * p, int iObj )
{
int k, iFanin, * pFanins;
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
Vec_IntPush( Vec_WecEntry(&p->vFanouts, iFanin), iObj );
}
static inline void Acb_ObjRemoveFaninFanout( Acb_Ntk_t * p, int iObj )
{
int k, iFanin, * pFanins;
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
Vec_IntRemove( Vec_WecEntry(&p->vFanouts, iFanin), iObj );
}
static inline void Acb_NtkCreateFanout( Acb_Ntk_t * p )
{
int iObj;
Acb_NtkCleanObjFanout( p );
Acb_NtkForEachObj( p, iObj )
Acb_ObjAddFaninFanout( p, iObj );
}
/**Function*************************************************************
@ -492,7 +549,6 @@ static inline void Acb_NtkFree( Acb_Ntk_t * p )
Vec_StrErase( &p->vObjType );
Vec_IntErase( &p->vObjFans );
Vec_IntErase( &p->vFanSto );
Vec_WecErase( &p->vFanouts );
// optional
Vec_IntErase( &p->vObjCopy );
Vec_IntErase( &p->vObjFunc );
@ -510,7 +566,12 @@ static inline void Acb_NtkFree( Acb_Ntk_t * p )
Vec_IntErase( &p->vLevelR );
Vec_IntErase( &p->vPathD );
Vec_IntErase( &p->vPathR );
Vec_FltErase( &p->vCounts );
Vec_WecErase( &p->vFanouts );
Vec_WecErase( &p->vCnfs );
// other
Vec_QueFreeP( &p->vQue );
Vec_IntErase( &p->vCover );
Vec_IntErase( &p->vArray0 );
Vec_IntErase( &p->vArray1 );
Vec_IntErase( &p->vArray2 );
@ -572,42 +633,6 @@ static inline Vec_Int_t * Acb_NtkCollect( Acb_Ntk_t * p )
Vec_IntPush( vObjs, iObj );
return vObjs;
}
static inline int Acb_NtkIsSeq( Acb_Ntk_t * p )
{
int iObj;
if ( p->fSeq )
return 1;
if ( p->fComb )
return 0;
assert( !p->fSeq && !p->fComb );
Acb_NtkForEachBox( p, iObj )
if ( Acb_ObjIsBox(p, iObj) )
{
if ( Acb_NtkIsSeq( Acb_ObjNtk(p, iObj) ) )
{
p->fSeq = 1;
return 1;
}
}
else if ( Acb_ObjIsSeq(p, iObj) )
{
p->fSeq = 1;
return 1;
}
p->fComb = 1;
return 0;
}
static inline void Acb_NtkPrepareSeq( Acb_Ntk_t * p )
{
int iObj;
assert( Acb_NtkSeqNum(p) == 0 );
if ( !Acb_NtkIsSeq(p) )
return;
Acb_NtkForEachBox( p, iObj )
if ( Acb_ObjIsSeq(p, iObj) )
Vec_IntPush( &p->vSeq, iObj );
// Acb_NtkObjOrder( p, &p->vSeq, NULL );
}
static inline Acb_Ntk_t * Acb_NtkDup( Acb_Man_t * pMan, Acb_Ntk_t * p, Vec_Int_t * vObjs )
{
Acb_Ntk_t * pNew;
@ -684,6 +709,7 @@ static inline int Acb_NtkMemory( Acb_Ntk_t * p )
nMem += (int)Vec_IntMemory(&p->vNtkObjs );
nMem += (int)Vec_IntMemory(&p->vTargets );
// other
nMem += (int)Vec_IntMemory(&p->vCover );
nMem += (int)Vec_IntMemory(&p->vArray0 );
nMem += (int)Vec_IntMemory(&p->vArray1 );
nMem += (int)Vec_IntMemory(&p->vArray2 );
@ -774,12 +800,6 @@ static inline Acb_Man_t * Acb_ManDup( Acb_Man_t * p, Vec_Int_t*(* pFuncOrder)(Ac
pNew->iRoot = Acb_ManNtkNum(pNew);
return pNew;
}
static inline void Acb_ManPrepareSeq( Acb_Man_t * p )
{
Acb_Ntk_t * pNtk; int i;
Acb_ManForEachNtk( p, pNtk, i )
Acb_NtkPrepareSeq( pNtk );
}
static inline void Acb_ManFree( Acb_Man_t * p )
{
Acb_Ntk_t * pNtk; int i;
@ -939,8 +959,16 @@ static inline void Acb_ManPrintStats( Acb_Man_t * p, int nModules, int fVerbose
/*=== acbUtil.c =============================================================*/
extern void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj );
extern void Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp );
extern Vec_Int_t * Acb_ObjCollectTfi( Acb_Ntk_t * p, int iObj, int fTerm );
extern Vec_Int_t * Acb_ObjCollectTfo( Acb_Ntk_t * p, int iObj, int fTerm );
extern int Acb_ObjComputeLevelD( Acb_Ntk_t * p, int iObj );
extern int Acb_NtkComputeLevelD( Acb_Ntk_t * p, Vec_Int_t * vTfo );
extern void Acb_NtkUpdateLevelD( Acb_Ntk_t * p, int iObj );
extern void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj );
extern void Acb_NtkCreateNode( Acb_Ntk_t * p, word uTruth, Vec_Int_t * vSupp );
extern void Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp );
ABC_NAMESPACE_HEADER_END

18
src/base/acb/acbAbc.c
View File

@ -46,15 +46,25 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
Acb_Ntk_t * Acb_NtkFromAbc( Abc_Ntk_t * p )
{
int fTrack = 1;
Acb_Man_t * pMan = Acb_ManAlloc( Abc_NtkSpec(p), 1, NULL, NULL, NULL, NULL );
int i, k, NameId = Abc_NamStrFindOrAdd( pMan->pStrs, Abc_NtkName(p), NULL );
Acb_Ntk_t * pNtk = Acb_NtkAlloc( pMan, NameId, Abc_NtkCiNum(p), Abc_NtkCoNum(p), Abc_NtkObjNum(p) );
Abc_Obj_t * pObj, * pFanin;
assert( Abc_NtkIsSopLogic(p) );
pNtk->nFaninMax = 6;
if ( fTrack ) Vec_IntFill( &pNtk->vArray2, Abc_NtkObjNumMax(p), -1 );
Abc_NtkForEachCi( p, pObj, i )
{
pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_CI, 0, 0 );
if ( fTrack ) Vec_IntWriteEntry( &pNtk->vArray2, pObj->iTemp, Abc_ObjId(pObj) );
}
Abc_NtkForEachNode( p, pObj, i )
{
pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_LUT, Abc_ObjFaninNum(pObj), 0 );
if ( fTrack ) Vec_IntWriteEntry( &pNtk->vArray2, pObj->iTemp, Abc_ObjId(pObj) );
// printf( "%d -> %d\n%s", i, pObj->iTemp, (char *)pObj->pData );
}
Abc_NtkForEachCo( p, pObj, i )
pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_CO, 1, 0 );
Abc_NtkForEachNode( p, pObj, i )
@ -199,8 +209,8 @@ void Acb_ParSetDefault( Acb_Par_t * pPars )
{
memset( pPars, 0, sizeof(Acb_Par_t) );
pPars->nLutSize = 4; // LUT size
pPars->nTfoLevMax = 3; // the maximum fanout levels
pPars->nTfiLevMax = 3; // the maximum fanin levels
pPars->nTfoLevMax = 1; // the maximum fanout levels
pPars->nTfiLevMax = 2; // the maximum fanin levels
pPars->nFanoutMax = 10; // the maximum number of fanouts
pPars->nDivMax = 16; // the maximum divisor count
pPars->nTabooMax = 4; // the minimum MFFC size
@ -208,7 +218,7 @@ void Acb_ParSetDefault( Acb_Par_t * pPars )
pPars->nBTLimit = 0; // the maximum number of conflicts in one SAT run
pPars->nNodesMax = 0; // the maximum number of nodes to try
pPars->iNodeOne = 0; // one particular node to try
pPars->fArea = 0; // performs optimization for area
pPars->fArea = 1; // performs optimization for area
pPars->fMoreEffort = 0; // enables using more effort
pPars->fVerbose = 0; // enable basic stats
pPars->fVeryVerbose = 0; // enable detailed stats
@ -230,7 +240,7 @@ Abc_Ntk_t * Abc_NtkOptMfse( Abc_Ntk_t * pNtk, Acb_Par_t * pPars )
extern void Acb_NtkOpt( Acb_Ntk_t * p, Acb_Par_t * pPars );
Abc_Ntk_t * pNtkNew;
Acb_Ntk_t * p = Acb_NtkFromAbc( pNtk );
//Acb_NtkOpt( p, pPars );
Acb_NtkOpt( p, pPars );
pNtkNew = Acb_NtkToAbc( pNtk, p );
Acb_ManFree( p->pDesign );
return pNtkNew;

397
src/base/acb/acbMfs.c
View File

@ -94,7 +94,8 @@ Vec_Wec_t * Acb_DeriveCnfForWindow( Acb_Ntk_t * p, Vec_Int_t * vWin, int PivotVa
{
if ( Abc_LitIsCompl(iObj) && i < PivotVar )
continue;
vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, iObj );
iObj = Abc_Lit2Var(iObj);
vCnfBase = Acb_ObjCnfs( p, iObj );
if ( Vec_StrSize(vCnfBase) > 0 )
continue;
if ( vCnf == NULL )
@ -163,7 +164,10 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot )
Vec_Int_t * vLits = Vec_IntAlloc( 1000 );
// mark new SAT variables
Vec_IntForEachEntry( vWinObjs, iObj, i )
Acb_ObjSetCopy( p, i, iObj );
{
Acb_ObjSetFunc( p, Abc_Lit2Var(iObj), i );
//printf( "Node %d -> SAT var %d\n", Vec_IntEntry(&p->vArray2, Abc_Lit2Var(iObj)), i );
}
// add clauses for all nodes
Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntForEachEntry( vWinObjs, iObjLit, i )
@ -175,8 +179,8 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot )
// collect SAT variables
Vec_IntClear( vFaninVars );
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iFanin) );
Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iObj) );
Vec_IntPush( vFaninVars, Acb_ObjFunc(p, iFanin) );
Vec_IntPush( vFaninVars, Acb_ObjFunc(p, iObj) );
// derive CNF for the node
Acb_TranslateCnf( vClas, vLits, (Vec_Str_t *)Vec_WecEntry(vCnfs, iObj), vFaninVars, -1 );
}
@ -188,8 +192,8 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot )
// collect SAT variables
Vec_IntClear( vFaninVars );
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iFanin) + (iFanin > PivotVar) * nTfoSize );
Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iObj) + nTfoSize );
Vec_IntPush( vFaninVars, Acb_ObjFunc(p, iFanin) + (Acb_ObjFunc(p, iFanin) > PivotVar) * nTfoSize );
Vec_IntPush( vFaninVars, Acb_ObjFunc(p, iObj) + nTfoSize );
// derive CNF for the node
Acb_TranslateCnf( vClas, vLits, (Vec_Str_t *)Vec_WecEntry(vCnfs, iObj), vFaninVars, PivotVar );
}
@ -204,13 +208,13 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot )
continue;
iObj = Abc_Lit2Var(iObjLit);
// add clauses
Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjCopy(p, iObj), 0), Abc_Var2Lit(Acb_ObjCopy(p, iObj) + nTfoSize, 0), Abc_Var2Lit(nVars, 0) );
Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjFunc(p, iObj), 1), Abc_Var2Lit(Acb_ObjFunc(p, iObj) + nTfoSize, 0), Abc_Var2Lit(nVars, 0) );
Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjCopy(p, iObj), 1), Abc_Var2Lit(Acb_ObjCopy(p, iObj) + nTfoSize, 1), Abc_Var2Lit(nVars, 0) );
Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjFunc(p, iObj), 0), Abc_Var2Lit(Acb_ObjFunc(p, iObj) + nTfoSize, 1), Abc_Var2Lit(nVars, 0) );
Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjCopy(p, iObj), 0), Abc_Var2Lit(Acb_ObjCopy(p, iObj) + nTfoSize, 1), Abc_Var2Lit(nVars, 1) );
Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjFunc(p, iObj), 0), Abc_Var2Lit(Acb_ObjFunc(p, iObj) + nTfoSize, 0), Abc_Var2Lit(nVars, 1) );
Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjCopy(p, iObj), 1), Abc_Var2Lit(Acb_ObjCopy(p, iObj) + nTfoSize, 0), Abc_Var2Lit(nVars, 1) );
Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjFunc(p, iObj), 1), Abc_Var2Lit(Acb_ObjFunc(p, iObj) + nTfoSize, 1), Abc_Var2Lit(nVars, 1) );
Vec_IntPush( vClas, Vec_IntSize(vLits) );
Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars++, 0) );
}
@ -222,7 +226,7 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot )
Vec_IntFree( vFaninVars );
// undo SAT variables
Vec_IntForEachEntry( vWinObjs, iObj, i )
Vec_IntWriteEntry( &p->vObjCopy, iObj, -1 );
Vec_IntWriteEntry( &p->vObjFunc, Abc_Lit2Var(iObj), -1 );
// create CNF structure
pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
pCnf->nVars = nVarsAll;
@ -235,6 +239,7 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot )
// cleanup
Vec_IntFree( vClas );
Vec_IntFree( vLits );
//Cnf_DataPrint( pCnf, 1 );
return pCnf;
}
@ -252,7 +257,7 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot )
***********************************************************************/
sat_solver * Acb_NtkWindow2Solver( Cnf_Dat_t * pCnf, int PivotVar, int nDivs, int nTimes )
{
int n, i, RetValue, nRounds = nTimes <= 2 ? nTimes-1 : nTimes;
int n, i, RetValue, nRounds = nTimes <= 2 ? nTimes-1 : 2;
Vec_Int_t * vFlips = Cnf_DataCollectFlipLits( pCnf, PivotVar );
sat_solver * pSat = sat_solver_new();
sat_solver_setnvars( pSat, nTimes * pCnf->nVars + nRounds * nDivs + 1 );
@ -283,7 +288,7 @@ sat_solver * Acb_NtkWindow2Solver( Cnf_Dat_t * pCnf, int PivotVar, int nDivs, in
{
int BaseA = n * pCnf->nVars;
int BaseB = ((n + 1) % nTimes) * pCnf->nVars;
int BaseC = nTimes * pCnf->nVars + n * nDivs;
int BaseC = nTimes * pCnf->nVars + (n & 1) * nDivs;
for ( i = 0; i < nDivs; i++ )
sat_solver_add_buffer_enable( pSat, BaseA + i, BaseB + i, BaseC + i, 0 );
}
@ -298,6 +303,92 @@ sat_solver * Acb_NtkWindow2Solver( Cnf_Dat_t * pCnf, int PivotVar, int nDivs, in
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acb_NtkPrintVec( Acb_Ntk_t * p, Vec_Int_t * vVec, char * pName )
{
int i;
printf( "%s: ", pName );
for ( i = 0; i < vVec->nSize; i++ )
printf( "%d ", Vec_IntEntry(&p->vArray2, vVec->pArray[i]) );
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Collects divisors in a non-topo order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Acb_NtkDivisors( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo, int nDivsMax )
{
Vec_Int_t * vDivs = Vec_IntAlloc( 100 );
Vec_Int_t * vFront = Vec_IntAlloc( 100 );
int i, k, iFanin, * pFanins;
// mark taboo nodes
Acb_NtkIncTravId( p );
assert( !Acb_ObjIsCio(p, Pivot) );
Acb_ObjSetTravIdCur( p, Pivot );
for ( i = 0; i < nTaboo; i++ )
{
assert( !Acb_ObjIsCio(p, pTaboo[i]) );
if ( Acb_ObjSetTravIdCur( p, pTaboo[i] ) )
assert( 0 );
}
// collect non-taboo fanins of pivot but do not use them as frontier
Acb_ObjForEachFaninFast( p, Pivot, pFanins, iFanin, k )
if ( !Acb_ObjSetTravIdCur( p, iFanin ) )
Vec_IntPush( vDivs, iFanin );
// collect non-taboo fanins of taboo nodes and use them as frontier
for ( i = 0; i < nTaboo; i++ )
Acb_ObjForEachFaninFast( p, pTaboo[i], pFanins, iFanin, k )
if ( !Acb_ObjSetTravIdCur( p, iFanin ) )
{
Vec_IntPush( vDivs, iFanin );
if ( !Acb_ObjIsCio(p, iFanin) )
Vec_IntPush( vFront, iFanin );
}
// select divisors incrementally
while ( Vec_IntSize(vFront) > 0 && Vec_IntSize(vDivs) < nDivsMax )
{
// select the topmost
int iObj, iObjMax = -1, LevelMax = -1;
Vec_IntForEachEntry( vFront, iObj, k )
if ( LevelMax < Acb_ObjLevelD(p, iObj) )
LevelMax = Acb_ObjLevelD(p, (iObjMax = iObj));
assert( iObjMax > 0 );
Vec_IntRemove( vFront, iObjMax );
// expand the topmost
Acb_ObjForEachFaninFast( p, iObjMax, pFanins, iFanin, k )
if ( !Acb_ObjSetTravIdCur( p, iFanin ) )
{
Vec_IntPush( vDivs, iFanin );
if ( !Acb_ObjIsCio(p, iFanin) )
Vec_IntPush( vFront, iFanin );
}
}
Vec_IntFree( vFront );
// sort them by level
Vec_IntSelectSortCost( Vec_IntArray(vDivs), Vec_IntSize(vDivs), &p->vLevelD );
return vDivs;
}
/**Function*************************************************************
Synopsis [Marks TFO of divisors.]
@ -314,7 +405,8 @@ void Acb_ObjMarkTfo_rec( Acb_Ntk_t * p, int iObj, int Pivot, int nTfoLevMax, int
int iFanout, i;
if ( Acb_ObjSetTravIdCur(p, iObj) )
return;
if ( Acb_ObjLevelD(p, iObj) > nTfoLevMax || Acb_ObjFanoutNum(p, iObj) >= nFanMax || iObj == Pivot )
//printf( "Labeling %d.\n", Vec_IntEntry(&p->vArray2, iObj) );
if ( Acb_ObjLevelD(p, iObj) > nTfoLevMax || Acb_ObjFanoutNum(p, iObj) > nFanMax || iObj == Pivot )
return;
Acb_ObjForEachFanout( p, iObj, iFanout, i )
Acb_ObjMarkTfo_rec( p, iFanout, Pivot, nTfoLevMax, nFanMax );
@ -323,6 +415,7 @@ void Acb_ObjMarkTfo( Acb_Ntk_t * p, Vec_Int_t * vDivs, int Pivot, int nTfoLevMax
{
int i, iObj;
Acb_NtkIncTravId( p );
Acb_ObjSetTravIdCur( p, Pivot );
Vec_IntForEachEntry( vDivs, iObj, i )
Acb_ObjMarkTfo_rec( p, iObj, Pivot, nTfoLevMax, nFanMax );
}
@ -341,6 +434,7 @@ void Acb_ObjMarkTfo( Acb_Ntk_t * p, Vec_Int_t * vDivs, int Pivot, int nTfoLevMax
int Acb_ObjLabelTfo_rec( Acb_Ntk_t * p, int iObj, int nTfoLevMax, int nFanMax )
{
int iFanout, i, Diff, fHasNone = 0;
//printf( "Visiting %d\n", Vec_IntEntry(&p->vArray2, iObj) );
if ( (Diff = Acb_ObjTravIdDiff(p, iObj)) <= 2 )
return Diff;
Acb_ObjSetTravIdDiff( p, iObj, 2 );
@ -348,15 +442,15 @@ int Acb_ObjLabelTfo_rec( Acb_Ntk_t * p, int iObj, int nTfoLevMax, int nFanMax )
return 2;
if ( Acb_ObjLevelD(p, iObj) == nTfoLevMax || Acb_ObjFanoutNum(p, iObj) >= nFanMax )
{
if ( Diff == 3 )
Acb_ObjSetTravIdDiff( p, iObj, 1 ); // mark root
if ( Diff == 3 ) // belongs to TFO of TFI
Acb_ObjSetTravIdDiff( p, iObj, 1 ); // root
return Acb_ObjTravIdDiff(p, iObj);
}
Acb_ObjForEachFanout( p, iObj, iFanout, i )
fHasNone |= 2 == Acb_ObjLabelTfo_rec( p, iFanout, nTfoLevMax, nFanMax );
if ( fHasNone && Diff == 3 )
if ( fHasNone && Diff == 3 ) // belongs to TFO of TFI
Acb_ObjSetTravIdDiff( p, iObj, 1 ); // root
else
else if ( !fHasNone )
Acb_ObjSetTravIdDiff( p, iObj, 0 ); // inner
return Acb_ObjTravIdDiff(p, iObj);
}
@ -365,7 +459,7 @@ int Acb_ObjLabelTfo( Acb_Ntk_t * p, int Root, int nTfoLevMax, int nFanMax )
Acb_NtkIncTravId( p ); // none (2) marked (3) unmarked (4)
Acb_NtkIncTravId( p ); // root (1)
Acb_NtkIncTravId( p ); // inner (0)
assert( Acb_ObjTravIdDiff(p, Root) < 3 );
assert( Acb_ObjTravIdDiff(p, Root) > 2 );
return Acb_ObjLabelTfo_rec( p, Root, nTfoLevMax, nFanMax );
}
@ -387,19 +481,20 @@ void Acb_ObjDeriveTfo_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vTfo, Vec_Int_t
return;
if ( Diff == 2 ) // root
{
Vec_IntPush( vRoots, Diff );
Vec_IntPush( vRoots, iObj );
Vec_IntPush( vTfo, iObj );
return;
}
assert( Diff == 1 );
Acb_ObjForEachFanout( p, iObj, iFanout, i )
Acb_ObjDeriveTfo_rec( p, iFanout, vTfo, vRoots );
Vec_IntPush( vTfo, Diff );
Vec_IntPush( vTfo, iObj );
}
void Acb_ObjDeriveTfo( Acb_Ntk_t * p, int Pivot, int nTfoLevMax, int nFanMax, Vec_Int_t ** pvTfo, Vec_Int_t ** pvRoots )
{
int Res = Acb_ObjLabelTfo( p, Pivot, nTfoLevMax, nFanMax );
Vec_Int_t * vTfo = *pvTfo = Vec_IntAlloc( 100 );
Vec_Int_t * vRoots = *pvRoots = Vec_IntAlloc( 100 );
Vec_Int_t * vTfo = *pvTfo = Vec_IntAlloc( 10 );
Vec_Int_t * vRoots = *pvRoots = Vec_IntAlloc( 10 );
if ( Res ) // none or root
return;
Acb_NtkIncTravId( p ); // root (2) inner (1) visited (0)
@ -472,15 +567,18 @@ void Acb_NtkCollectNewTfi2_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vTfiNew )
Acb_NtkCollectNewTfi2_rec( p, iFanin, vTfiNew );
Vec_IntPush( vTfiNew, iObj );
}
Vec_Int_t * Acb_NtkCollectNewTfi( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vDivs, Vec_Int_t * vSide )
Vec_Int_t * Acb_NtkCollectNewTfi( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vDivs, Vec_Int_t * vSide, int * pnDivs )
{
Vec_Int_t * vTfiNew = Vec_IntAlloc( 100 );
int i, Node;
Acb_NtkIncTravId( p );
//Acb_NtkPrintVec( p, vDivs, "vDivs" );
Vec_IntForEachEntry( vDivs, Node, i )
Acb_NtkCollectNewTfi1_rec( p, Node, vTfiNew );
assert( Vec_IntSize(vTfiNew) == Vec_IntSize(vDivs) );
*pnDivs = Vec_IntSize(vTfiNew);
//Acb_NtkPrintVec( p, vTfiNew, "vTfiNew" );
Acb_NtkCollectNewTfi1_rec( p, Pivot, vTfiNew );
//Acb_NtkPrintVec( p, vTfiNew, "vTfiNew" );
assert( Vec_IntEntryLast(vTfiNew) == Pivot );
Vec_IntPop( vTfiNew );
Vec_IntForEachEntry( vSide, Node, i )
@ -505,95 +603,32 @@ Vec_Int_t * Acb_NtkCollectWindow( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vTfi, Ve
Vec_Int_t * vWin = Vec_IntAlloc( 100 );
int i, k, iObj, iFanin, * pFanins;
assert( Vec_IntEntryLast(vTfi) == Pivot );
// mark leaves
// mark nodes
Acb_NtkIncTravId( p );
Vec_IntForEachEntry( vTfi, iObj, i )
Acb_ObjSetTravIdCur(p, iObj);
Acb_NtkIncTravId( p );
Vec_IntForEachEntry( vTfi, iObj, i )
if ( !Acb_ObjIsCi(p, iObj) )
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
if ( !Acb_ObjIsTravIdCur(p, iFanin) )
Acb_ObjSetTravIdCur(p, iObj);
// add TFI
Vec_IntForEachEntry( vTfi, iObj, i )
Vec_IntPush( vWin, Abc_Var2Lit( iObj, Acb_ObjIsTravIdCur(p, iObj)) );
{
int fIsTfiInput = 0;
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
if ( !Acb_ObjIsTravIdCur(p, iFanin) ) // fanin is not in TFI
fIsTfiInput = 1; // mark as leaf
Vec_IntPush( vWin, Abc_Var2Lit(iObj, Acb_ObjIsCi(p, iObj) || fIsTfiInput) );
}
// mark roots
Acb_NtkIncTravId( p );
Vec_IntForEachEntry( vRoots, iObj, i )
Acb_ObjSetTravIdCur(p, iObj);
// add TFO
Vec_IntForEachEntry( vTfo, iObj, i )
Vec_IntPush( vWin, Abc_Var2Lit( iObj, Acb_ObjIsTravIdCur(p, iObj)) );
{
assert( !Acb_ObjIsCo(p, iObj) );
Vec_IntPush( vWin, Abc_Var2Lit(iObj, Acb_ObjIsTravIdCur(p, iObj)) );
}
return vWin;
}
/**Function*************************************************************
Synopsis [Collects divisors in a non-topo order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Acb_NtkDivisors( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo, int nDivsMax )
{
Vec_Int_t * vDivs = Vec_IntAlloc( 100 );
Vec_Int_t * vFront = Vec_IntAlloc( 100 );
int i, k, iFanin, * pFanins;
// mark taboo nodes
Acb_NtkIncTravId( p );
assert( !Acb_ObjIsCio(p, Pivot) );
Acb_ObjSetTravIdCur( p, Pivot );
for ( i = 0; i < nTaboo; i++ )
{
assert( !Acb_ObjIsCio(p, pTaboo[i]) );
if ( Acb_ObjSetTravIdCur( p, pTaboo[i] ) )
assert( 0 );
}
// collect non-taboo fanins of pivot but do not use them as frontier
Acb_ObjForEachFaninFast( p, Pivot, pFanins, iFanin, k )
if ( !Acb_ObjSetTravIdCur( p, iFanin ) )
Vec_IntPush( vDivs, iFanin );
// collect non-tabook fanins of taboo nodes and use them as frontier
for ( i = 0; i < nTaboo; i++ )
Acb_ObjForEachFaninFast( p, pTaboo[i], pFanins, iFanin, k )
if ( !Acb_ObjSetTravIdCur( p, iFanin ) )
{
Vec_IntPush( vDivs, iFanin );
if ( !Acb_ObjIsCio(p, iFanin) )
Vec_IntPush( vFront, iFanin );
}
// select divisors incrementally
while ( Vec_IntSize(vFront) > 0 && Vec_IntSize(vDivs) < nDivsMax )
{
// select the topmost
int iObj, iObjMax = -1, LevelMax = -1;
Vec_IntForEachEntry( vFront, iObj, k )
if ( LevelMax < Acb_ObjLevelD(p, iObj) )
LevelMax = Acb_ObjLevelD(p, (iObjMax = iObj));
assert( iObjMax > 0 );
Vec_IntRemove( vFront, iObjMax );
// expand the topmost
Acb_ObjForEachFaninFast( p, iObjMax, pFanins, iFanin, k )
if ( !Acb_ObjSetTravIdCur( p, iFanin ) )
{
Vec_IntPush( vDivs, iFanin );
if ( !Acb_ObjIsCio(p, iFanin) )
Vec_IntPush( vFront, iFanin );
}
}
Vec_IntFree( vFront );
// sort them by level
Vec_IntSelectSortCost( Vec_IntArray(vDivs), Vec_IntSize(vDivs), &p->vLevelD );
return vDivs;
}
/**Function*************************************************************
Synopsis []
@ -607,20 +642,26 @@ Vec_Int_t * Acb_NtkDivisors( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo,
***********************************************************************/
Vec_Int_t * Acb_NtkWindow( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo, int nDivsMax, int nTfoLevs, int nFanMax, int * pnDivs )
{
int fVerbose = 0;
int nTfoLevMax = Acb_ObjLevelD(p, Pivot) + nTfoLevs;
Vec_Int_t * vWin, * vDivs, * vTfo, * vRoots, * vSide, * vTfi;
// collect divisors by traversing limited TFI
vDivs = Acb_NtkDivisors( p, Pivot, pTaboo, nTaboo, nDivsMax );
if ( fVerbose ) Acb_NtkPrintVec( p, vDivs, "vDivs" );
// mark limited TFO of the divisors
Acb_ObjMarkTfo( p, vDivs, Pivot, nTfoLevMax, nFanMax );
// collect TFO and roots
Acb_ObjDeriveTfo( p, Pivot, nTfoLevMax, nFanMax, &vTfo, &vRoots );
if ( fVerbose ) Acb_NtkPrintVec( p, vTfo, "vTfo" );
if ( fVerbose ) Acb_NtkPrintVec( p, vRoots, "vRoots" );
// collect side inputs of the TFO
vSide = Acb_NtkCollectTfoSideInputs( p, Pivot, vTfo );
if ( fVerbose ) Acb_NtkPrintVec( p, vSide, "vSide" );
// mark limited TFO of the divisors
Acb_ObjMarkTfo( p, vDivs, Pivot, nTfoLevMax, nFanMax );
// collect new TFI
vTfi = Acb_NtkCollectNewTfi( p, Pivot, vDivs, vSide );
vTfi = Acb_NtkCollectNewTfi( p, Pivot, vDivs, vSide, pnDivs );
if ( fVerbose ) Acb_NtkPrintVec( p, vTfi, "vTfi" );
Vec_IntFree( vSide );
Vec_IntFree( vDivs );
// collect all nodes
@ -634,34 +675,6 @@ Vec_Int_t * Acb_NtkWindow( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo, i
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Acb_NtkFindSupp( sat_solver * pSat, Acb_Ntk_t * p, Vec_Int_t * vWin, Vec_Int_t * vDivs, int nBTLimit )
{
int i, iObj, nDivsNew;
// reload divisors in terms of SAT variables
Vec_IntForEachEntry( vDivs, iObj, i )
Vec_IntWriteEntry( vDivs, i, Acb_ObjCopy(p, iObj) );
// try solving
nDivsNew = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vDivs), Vec_IntSize(vDivs), nBTLimit );
Vec_IntShrink( vDivs, nDivsNew );
// reload divisors in terms of network variables
Vec_IntForEachEntry( vDivs, iObj, i )
Vec_IntWriteEntry( vDivs, i, Vec_IntEntry(vWin, iObj) );
return Vec_IntSize(vDivs);
}
/**Function*************************************************************
Synopsis [Computes function of the node]
@ -704,7 +717,6 @@ word Acb_ComputeFunction( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_
// compute cube and add clause
nFinal = sat_solver_final( pSat, &pFinal );
Vec_IntFill( vTempLits, 1, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
uCube = ~(word)0;
for ( i = 0; i < nFinal; i++ )
if ( pFinal[i] != pLits[0] )
Vec_IntPush( vTempLits, pFinal[i] );
@ -716,7 +728,8 @@ word Acb_ComputeFunction( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_
Vec_IntForEachEntry( vDivVars, iVar, i )
Vec_IntPush( vTempLits, Abc_LitNot(sat_solver_var_literal(pSat, iVar)) );
}
Vec_IntForEachEntry( vTempLits, iLit, i )
uCube = ~(word)0;
Vec_IntForEachEntryStart( vTempLits, iLit, i, 1 )
{
iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(iLit) ); assert( iVar >= 0 );
uCube &= Abc_LitIsCompl(iLit) ? s_Truths6[iVar] : ~s_Truths6[iVar];
@ -736,7 +749,7 @@ word Acb_ComputeFunction( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_
/**Function*************************************************************
Synopsis [Collects the taboo nodes.]
Synopsis [Collects the taboo nodes (nodes that cannot be divisors).]
Description []
@ -820,6 +833,12 @@ int Acb_NtkCollectTaboo( Acb_Ntk_t * p, int Pivot, int nTabooMax, int * pTaboo )
SeeAlso []
***********************************************************************/
static inline void Vec_IntVars2Vars( Vec_Int_t * p, int Shift )
{
int i;
for ( i = 0; i < p->nSize; i++ )
p->pArray[i] += Shift;
}
static inline void Vec_IntVars2Lits( Vec_Int_t * p, int Shift, int fCompl )
{
int i;
@ -830,7 +849,7 @@ static inline void Vec_IntLits2Vars( Vec_Int_t * p, int Shift )
{
int i;
for ( i = 0; i < p->nSize; i++ )
p->pArray[i] = Abc_Lit2Var( p->pArray[i] ) - Shift;
p->pArray[i] = Abc_Lit2Var( p->pArray[i] ) + Shift;
}
static inline void Vec_IntRemap( Vec_Int_t * p, Vec_Int_t * vMap )
{
@ -839,21 +858,53 @@ static inline void Vec_IntRemap( Vec_Int_t * p, Vec_Int_t * vMap )
p->pArray[i] = Vec_IntEntry(vMap, p->pArray[i]);
}
void Acb_NtkOptNode( Acb_Ntk_t * p, int Pivot, int nTabooMax, int nDivMax, int nTfoLevs, int nFanMax, int nLutSize )
void Acb_WinPrint( Acb_Ntk_t * p, Vec_Int_t * vWin, int Pivot, int nDivs )
{
int i, Node;
printf( "Window for node %d with %d divisors:\n", Vec_IntEntry(&p->vArray2, Pivot), nDivs );
Vec_IntForEachEntry( vWin, Node, i )
{
if ( i == nDivs )
printf( " | " );
if ( Abc_Lit2Var(Node) == Pivot )
printf( "(%d) ", Vec_IntEntry(&p->vArray2, Pivot) );
else
printf( "%s%d ", Abc_LitIsCompl(Node) ? "*":"", Vec_IntEntry(&p->vArray2, Abc_Lit2Var(Node)) );
}
printf( "\n" );
}
Vec_Int_t * Acb_NtkFindSupp( Acb_Ntk_t * p, sat_solver * pSat2, int nVars, int nDivs )
{
int nSuppNew;
Vec_Int_t * vSupp = Vec_IntStartNatural( nDivs );
Vec_IntReverseOrder( vSupp );
Vec_IntVars2Lits( vSupp, 2*nVars, 0 );
nSuppNew = sat_solver_minimize_assumptions( pSat2, Vec_IntArray(vSupp), Vec_IntSize(vSupp), 0 );
Vec_IntShrink( vSupp, nSuppNew );
Vec_IntLits2Vars( vSupp, -2*nVars );
return vSupp;
}
void Acb_NtkOptNode( Acb_Ntk_t * p, int Pivot, int nTabooMax, int nDivMax, int nTfoLevs, int nFanMax, int nLutSize, int fVerbose )
{
Cnf_Dat_t * pCnf;
Vec_Int_t * vWin, * vSupp = NULL;
sat_solver * pSat1 = NULL, * pSat2 = NULL, * pSat3 = NULL;
int c, nSuppNew, PivotVar, nDivs = 0;
int c, PivotVar, nDivs = 0; word uTruth;
int pTaboo[16], nTaboo = Acb_NtkCollectTaboo( p, Pivot, nTabooMax, pTaboo );
if ( nTaboo == 0 )
return;
assert( nTabooMax == 0 || nTaboo <= nTabooMax );
assert( nTaboo <= 16 );
// compute divisor and window for these nodes
// compute divisors and window for this target node with these taboo nodes
vWin = Acb_NtkWindow( p, Pivot, pTaboo, nTaboo, nDivMax, nTfoLevs, nFanMax, &nDivs );
PivotVar = Vec_IntFind(vWin, Abc_Var2Lit(Pivot, 0));
PivotVar = Vec_IntFind( vWin, Abc_Var2Lit(Pivot, 0) );
if ( fVerbose )
printf( "Node %d: Window contains %d objects and %d divisors. ", Vec_IntEntry(&p->vArray2, Pivot), Vec_IntSize(vWin), nDivs );
// Acb_WinPrint( p, vWin, Pivot, nDivs );
// return;
// derive CNF and SAT solvers
pCnf = Acb_NtkWindow2Cnf( p, vWin, Pivot );
@ -865,66 +916,84 @@ void Acb_NtkOptNode( Acb_Ntk_t * p, int Pivot, int nTabooMax, int nDivMax, int n
int status = sat_solver_solve( pSat1, &Lit, &Lit + 1, 0, 0, 0, 0 );
if ( status == l_False )
{
if ( fVerbose )
printf( "Found constant %d.\n", c );
Acb_NtkUpdateNode( p, Pivot, c ? ~(word)0 : 0, NULL );
goto cleanup;
}
assert( status == l_True );
}
// check for one-node implementation
pSat2 = Acb_NtkWindow2Solver( pCnf, PivotVar, nDivs, 2 );
//pSat6 = Acb_NtkWindow2Solver( pCnf, PivotVar, nDivs, 6 );
// try solving the original support
vSupp = Vec_IntStartNatural( nDivs );
Vec_IntVars2Lits( vSupp, 2*pCnf->nVars, 0 );
nSuppNew = sat_solver_minimize_assumptions( pSat2, Vec_IntArray(vSupp), Vec_IntSize(vSupp), 0 );
Vec_IntShrink( vSupp, nSuppNew );
Vec_IntLits2Vars( vSupp, -2*pCnf->nVars );
if ( nSuppNew <= nLutSize )
vSupp = Acb_NtkFindSupp( p, pSat2, pCnf->nVars, nDivs );
if ( Vec_IntSize(vSupp) <= nLutSize )
{
int FreeVar = sat_solver_nvars( pSat1 ) - 1;
word uTruth;
Vec_IntVars2Lits( vSupp, pCnf->nVars, 0 );
uTruth = Acb_ComputeFunction( pSat1, PivotVar, FreeVar, vSupp );
Vec_IntLits2Vars( vSupp, -pCnf->nVars );
if ( fVerbose )
printf( "Found %d inputs: ", Vec_IntSize(vSupp) );
uTruth = Acb_ComputeFunction( pSat1, PivotVar, sat_solver_nvars(pSat1)-1, vSupp );
if ( fVerbose )
Extra_PrintHex( stdout, (unsigned *)&uTruth, Vec_IntSize(vSupp) );
if ( fVerbose )
printf( "\n" );
// create support in terms of nodes
Vec_IntRemap( vSupp, vWin );
Vec_IntLits2Vars( vSupp, 0 );
Acb_NtkUpdateNode( p, Pivot, uTruth, vSupp );
goto cleanup;
}
if ( fVerbose )
printf( "\n" );
// cleanup
cleanup:
if ( pSat1 ) sat_solver_delete( pSat1 );
if ( pSat2 ) sat_solver_delete( pSat2 );
if ( pSat3 ) sat_solver_delete( pSat3 );
Cnf_DataFree( pCnf );
Vec_IntFree( vWin );
Vec_IntFree( vSupp );
Vec_IntFreeP( &vSupp );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acb_NtkOpt( Acb_Ntk_t * p, Acb_Par_t * pPars )
{
int iObj;
if ( pPars->fVerbose )
printf( "Performing %s-oriented optimization with DivMax = %d. TfoLev = %d. LutSize = %d.\n",
pPars->fArea ? "area" : "delay", pPars->nDivMax, pPars->nTfoLevMax, pPars->nLutSize );
Acb_NtkCreateFanout( p ); // fanout data structure
Acb_NtkCleanObjFuncs( p ); // SAT variables
Acb_NtkCleanObjCnfs( p ); // CNF representations
if ( pPars->fArea )
{
int iObj;
Acb_NtkUpdateLevelD( p, -1 ); // compute forward logic level
Acb_NtkForEachNode( p, iObj )
Acb_NtkOptNode( p, iObj, pPars->nTabooMax, pPars->nDivMax, pPars->nTfoLevMax, pPars->nFanoutMax, pPars->nLutSize );
{
//if ( iObj != 433 )
// continue;
Acb_NtkOptNode( p, iObj, pPars->nTabooMax, pPars->nDivMax, pPars->nTfoLevMax, pPars->nFanoutMax, pPars->nLutSize, pPars->fVerbose );
}
}
else
{
Acb_NtkUpdateTiming( p, -1 );
while ( 1 )
Acb_NtkUpdateTiming( p, -1 ); // compute delay information
while ( Vec_QueTopPriority(p->vQue) > 0 )
{
int iObj = 0;
Acb_NtkOptNode( p, iObj, 0, pPars->nDivMax, pPars->nTfoLevMax, pPars->nFanoutMax, pPars->nLutSize );
int iObj = Vec_QuePop(p->vQue);
//if ( iObj != 28 )
// continue;
Acb_NtkOptNode( p, iObj, 0, pPars->nDivMax, pPars->nTfoLevMax, pPars->nFanoutMax, pPars->nLutSize, pPars->fVerbose );
}
}
}

250
src/base/acb/acbUtil.c
View File

@ -33,38 +33,7 @@ ABC_NAMESPACE_IMPL_START
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acb_ObjAddFanout( Acb_Ntk_t * p, int iObj )
{
int k, iFanin, * pFanins;
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
Vec_IntPush( Vec_WecEntry(&p->vFanouts, iFanin), iObj );
}
void Acb_ObjRemoveFanout( Acb_Ntk_t * p, int iObj )
{
int k, iFanin, * pFanins;
Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k )
Vec_IntRemove( Vec_WecEntry(&p->vFanouts, iFanin), iObj );
}
void Acb_NtkCreateFanout( Acb_Ntk_t * p )
{
int iObj;
Vec_WecInit( &p->vFanouts, Acb_NtkObjNumMax(p) );
Acb_NtkForEachObj( p, iObj )
Acb_ObjAddFanout( p, iObj );
}
/**Function*************************************************************
Synopsis []
Synopsis [Collecting TFI and TFO.]
Description []
@ -86,9 +55,14 @@ void Acb_ObjCollectTfi_rec( Acb_Ntk_t * p, int iObj, int fTerm )
}
Vec_Int_t * Acb_ObjCollectTfi( Acb_Ntk_t * p, int iObj, int fTerm )
{
int i;
Vec_IntClear( &p->vArray0 );
Acb_NtkIncTravId( p );
Acb_ObjCollectTfi_rec( p, iObj, fTerm );
if ( iObj > 0 )
Acb_ObjCollectTfi_rec( p, iObj, fTerm );
else
Acb_NtkForEachCo( p, iObj, i )
Acb_ObjCollectTfi_rec( p, iObj, fTerm );
return &p->vArray0;
}
@ -105,16 +79,20 @@ void Acb_ObjCollectTfo_rec( Acb_Ntk_t * p, int iObj, int fTerm )
}
Vec_Int_t * Acb_ObjCollectTfo( Acb_Ntk_t * p, int iObj, int fTerm )
{
int i;
Vec_IntClear( &p->vArray1 );
Acb_NtkIncTravId( p );
Acb_ObjCollectTfo_rec( p, iObj, fTerm );
if ( iObj > 0 )
Acb_ObjCollectTfo_rec( p, iObj, fTerm );
else
Acb_NtkForEachCi( p, iObj, i )
Acb_ObjCollectTfo_rec( p, iObj, fTerm );
return &p->vArray1;
}
/**Function*************************************************************
Synopsis []
Synopsis [Computing and updating direct and reverse logic level.]
Description []
@ -132,19 +110,12 @@ int Acb_ObjComputeLevelD( Acb_Ntk_t * p, int iObj )
}
int Acb_NtkComputeLevelD( Acb_Ntk_t * p, Vec_Int_t * vTfo )
{
// it is assumed that vTfo contains CO nodes and level of new nodes was already updated
int i, iObj, Level = 0;
if ( vTfo == NULL )
{
if ( !Acb_NtkHasObjLevelD( p ) )
Acb_NtkCleanObjLevelD( p );
Acb_NtkForEachObj( p, iObj )
Acb_ObjComputeLevelD( p, iObj );
}
else
{
// it is assumed that vTfo contains CO nodes and level of new nodes was already updated
Vec_IntForEachEntry( vTfo, iObj, i )
Acb_ObjComputeLevelD( p, iObj );
}
Vec_IntForEachEntryReverse( vTfo, iObj, i )
Acb_ObjComputeLevelD( p, iObj );
Acb_NtkForEachCo( p, iObj, i )
Level = Abc_MaxInt( Level, Acb_ObjLevelD(p, iObj) );
p->LevelMax = Level;
@ -160,28 +131,27 @@ int Acb_ObjComputeLevelR( Acb_Ntk_t * p, int iObj )
}
int Acb_NtkComputeLevelR( Acb_Ntk_t * p, Vec_Int_t * vTfi )
{
// it is assumed that vTfi contains CI nodes
int i, iObj, Level = 0;
if ( vTfi == NULL )
{
Acb_NtkCleanObjLevelR( p );
Acb_NtkForEachObjReverse( p, iObj )
Acb_ObjComputeLevelR( p, iObj );
}
else
{
// it is assumed that vTfi contains CI nodes
Vec_IntForEachEntryReverse( vTfi, iObj, i )
Acb_ObjComputeLevelR( p, iObj );
}
if ( !Acb_NtkHasObjLevelD( p ) )
Acb_NtkCleanObjLevelD( p );
Vec_IntForEachEntryReverse( vTfi, iObj, i )
Acb_ObjComputeLevelR( p, iObj );
Acb_NtkForEachCi( p, iObj, i )
Level = Abc_MaxInt( Level, Acb_ObjLevelR(p, iObj) );
assert( p->LevelMax == Level );
return Level;
}
void Acb_NtkUpdateLevelD( Acb_Ntk_t * p, int Pivot )
{
Vec_Int_t * vTfo = Acb_ObjCollectTfo( p, Pivot, 1 );
Acb_NtkComputeLevelD( p, vTfo );
}
/**Function*************************************************************
Synopsis []
Synopsis [Computing and updating direct and reverse path count.]
Description []
@ -192,9 +162,11 @@ int Acb_NtkComputeLevelR( Acb_Ntk_t * p, Vec_Int_t * vTfi )
***********************************************************************/
int Acb_ObjSlack( Acb_Ntk_t * p, int iObj )
{
assert( !Acb_ObjIsCio(p, iObj) + p->LevelMax >= Acb_ObjLevelD(p, iObj) + Acb_ObjLevelR(p, iObj) );
return !Acb_ObjIsCio(p, iObj) + p->LevelMax - Acb_ObjLevelD(p, iObj) - Acb_ObjLevelR(p, iObj);
int LevelSum = Acb_ObjLevelD(p, iObj) + Acb_ObjLevelR(p, iObj);
assert( !Acb_ObjIsCio(p, iObj) + p->LevelMax >= LevelSum );
return !Acb_ObjIsCio(p, iObj) + p->LevelMax - LevelSum;
}
int Acb_ObjComputePathD( Acb_Ntk_t * p, int iObj )
{
int * pFanins, iFanin, k, Path = 0;
@ -207,26 +179,13 @@ int Acb_ObjComputePathD( Acb_Ntk_t * p, int iObj )
int Acb_NtkComputePathsD( Acb_Ntk_t * p, Vec_Int_t * vTfo )
{
int i, iObj, Path = 0;
if ( vTfo == NULL )
{
Acb_NtkCleanObjPathD( p );
Acb_NtkForEachCi( p, iObj, i )
if ( Acb_ObjLevelR(p, iObj) == p->LevelMax )
Acb_ObjSetPathD( p, iObj, 1 );
Acb_NtkForEachObj( p, iObj )
if ( !Acb_ObjIsCi(p, iObj) && !Acb_ObjSlack(p, iObj) )
Acb_ObjComputePathD( p, iObj );
}
else
{
// it is assumed that vTfo contains CO nodes
assert( Acb_ObjSlack(p, Vec_IntEntry(vTfo, 0)) );
Vec_IntForEachEntry( vTfo, iObj, i )
if ( !Acb_ObjSlack(p, iObj) )
Acb_ObjComputePathD( p, iObj );
else
Acb_ObjSetPathD( p, iObj, 0 );
}
// it is assumed that vTfo contains CO nodes
//assert( Acb_ObjSlack(p, Vec_IntEntry(vTfo, 0)) );
Vec_IntForEachEntryReverse( vTfo, iObj, i )
if ( !Acb_ObjSlack(p, iObj) )
Acb_ObjComputePathD( p, iObj );
else
Acb_ObjSetPathD( p, iObj, 0 );
Acb_NtkForEachCo( p, iObj, i )
Path += Acb_ObjPathD(p, iObj);
p->nPaths = Path;
@ -245,55 +204,39 @@ int Acb_ObjComputePathR( Acb_Ntk_t * p, int iObj )
int Acb_NtkComputePathsR( Acb_Ntk_t * p, Vec_Int_t * vTfi )
{
int i, iObj, Path = 0;
if ( vTfi == NULL )
{
Acb_NtkCleanObjPathR( p );
Acb_NtkForEachCo( p, iObj, i )
if ( Acb_ObjLevelD(p, iObj) == p->LevelMax )
Acb_ObjSetPathR( p, iObj, 1 );
Acb_NtkForEachObjReverse( p, iObj )
if ( !Acb_ObjIsCo(p, iObj) && !Acb_ObjSlack(p, iObj) )
Acb_ObjComputePathR( p, iObj );
}
else
{
// it is assumed that vTfi contains CI nodes
assert( Acb_ObjSlack(p, Vec_IntEntry(vTfi, 0)) );
Vec_IntForEachEntryReverse( vTfi, iObj, i )
if ( !Acb_ObjSlack(p, iObj) )
Acb_ObjComputePathR( p, iObj );
else
Acb_ObjSetPathR( p, iObj, 0 );
}
// it is assumed that vTfi contains CI nodes
//assert( Acb_ObjSlack(p, Vec_IntEntry(vTfi, 0)) );
Vec_IntForEachEntryReverse( vTfi, iObj, i )
if ( !Acb_ObjSlack(p, iObj) )
Acb_ObjComputePathR( p, iObj );
else
Acb_ObjSetPathR( p, iObj, 0 );
Acb_NtkForEachCi( p, iObj, i )
Path += Acb_ObjPathR(p, iObj);
assert( p->nPaths == Path );
return Path;
}
int Acb_NtkComputePaths( Acb_Ntk_t * p )
{
Acb_NtkComputeLevelD( p, NULL );
Acb_NtkComputeLevelR( p, NULL );
Acb_NtkComputePathsD( p, NULL );
Acb_NtkComputePathsR( p, NULL );
Vec_Int_t * vTfi = Acb_ObjCollectTfi( p, -1, 1 );
Vec_Int_t * vTfo = Acb_ObjCollectTfo( p, -1, 1 );
Acb_NtkComputeLevelD( p, vTfi );
Acb_NtkComputeLevelR( p, vTfo );
Acb_NtkComputePathsD( p, vTfi );
Acb_NtkComputePathsR( p, vTfo );
return p->nPaths;
}
void Abc_NtkComputePaths( Abc_Ntk_t * p )
{
extern Acb_Ntk_t * Acb_NtkFromAbc( Abc_Ntk_t * p );
Acb_Ntk_t * pNtk = Acb_NtkFromAbc( p );
Acb_NtkCreateFanout( pNtk );
printf( "Computed %d paths.\n", Acb_NtkComputePaths(pNtk) );
Acb_ManFree( pNtk->pDesign );
}
/**Function*************************************************************
Synopsis []
@ -305,42 +248,47 @@ void Abc_NtkComputePaths( Abc_Ntk_t * p )
SeeAlso []
***********************************************************************/
int Acb_ObjPath( Acb_Ntk_t * p, int iObj )
{
return Acb_ObjPathD(p, iObj) + Acb_ObjPathR(p, iObj);
}
void Acb_ObjUpdateTiming( Acb_Ntk_t * p, int iObj )
void Acb_ObjUpdatePriority( Acb_Ntk_t * p, int iObj )
{
int nPaths;
if ( p->vQue == NULL )
{
Acb_NtkCleanObjCounts( p );
p->vQue = Vec_QueAlloc( 1000 );
Vec_QueSetPriority( p->vQue, Vec_FltArrayP(&p->vCounts) );
}
nPaths = Acb_ObjPathD(p, iObj) + Acb_ObjPathR(p, iObj);
if ( nPaths == 0 )
return;
Acb_ObjSetCounts( p, iObj, (float)nPaths );
if ( Vec_QueIsMember( p->vQue, iObj ) )
Vec_QueUpdate( p->vQue, iObj );
else
Vec_QuePush( p->vQue, iObj );
}
void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj )
{
int i, Entry;
if ( iObj > 0 )
int i, Entry, LevelMax = p->LevelMax;
// assuming that level of the new nodes is up to date
Vec_Int_t * vTfi = Acb_ObjCollectTfi( p, iObj, 1 );
Vec_Int_t * vTfo = Acb_ObjCollectTfo( p, iObj, 1 );
Acb_NtkComputeLevelD( p, vTfo );
Acb_NtkComputeLevelR( p, vTfi );
if ( iObj > 0 && LevelMax > p->LevelMax ) // reduced level
{
// assuming that level of the new nodes is up to date
Vec_Int_t * vTfi = Acb_ObjCollectTfi( p, iObj, 1 );
Vec_Int_t * vTfo = Acb_ObjCollectTfo( p, iObj, 1 );
Acb_NtkComputeLevelD( p, vTfo );
Acb_NtkComputeLevelR( p, vTfi );
Acb_NtkComputePathsD( p, vTfo );
Acb_NtkComputePathsR( p, vTfi );
Vec_IntForEachEntry( vTfi, Entry, i )
Acb_ObjUpdateTiming( p, Entry );
Vec_IntForEachEntry( vTfo, Entry, i )
Acb_ObjUpdateTiming( p, Entry );
}
else
{
Acb_NtkComputeLevelD( p, NULL );
Acb_NtkComputeLevelR( p, NULL );
Acb_NtkComputePathsD( p, NULL );
Acb_NtkComputePathsR( p, NULL );
Acb_NtkForEachNode( p, Entry )
Acb_ObjUpdateTiming( p, Entry );
vTfi = Acb_ObjCollectTfi( p, -1, 1 );
vTfo = Acb_ObjCollectTfo( p, -1, 1 );
Vec_QueClear( p->vQue );
// add backup here
}
Acb_NtkComputePathsD( p, vTfo );
Acb_NtkComputePathsR( p, vTfi );
Vec_IntForEachEntry( vTfi, Entry, i )
Acb_ObjUpdatePriority( p, Entry );
Vec_IntForEachEntry( vTfo, Entry, i )
Acb_ObjUpdatePriority( p, Entry );
}
/**Function*************************************************************
Synopsis []
@ -352,20 +300,28 @@ void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj )
SeeAlso []
***********************************************************************/
void Acb_NtkCreateNode( Acb_Ntk_t * p, word uTruth, Vec_Int_t * vSupp )
{
int Pivot = Acb_ObjAlloc( p, ABC_OPER_LUT, Vec_IntSize(vSupp), 0 );
Acb_ObjSetTruth( p, Pivot, uTruth );
Acb_ObjAddFanins( p, Pivot, vSupp );
Acb_ObjAddFaninFanout( p, Pivot );
Acb_ObjComputeLevelD( p, Pivot );
}
void Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp )
{
int i, iFanin;
Vec_WrdSetEntry( &p->vObjTruth, Pivot, uTruth );
Acb_ObjRemoveFanout( p, Pivot );
Acb_ObjRemoveFanins( p, Pivot );
Vec_IntForEachEntry( vSupp, iFanin, i )
Acb_ObjAddFanin( p, Pivot, iFanin );
Acb_ObjAddFanout( p, Pivot );
Acb_NtkUpdateTiming( p, Pivot );
Vec_IntErase( Vec_WecEntry(&p->vCnfs, Pivot) );
Acb_ObjRemoveFaninFanout( p, Pivot );
Acb_ObjRemoveFanins( p, Pivot );
Acb_ObjAddFanins( p, Pivot, vSupp );
Acb_ObjAddFaninFanout( p, Pivot );
if ( p->vQue == NULL )
Acb_NtkUpdateLevelD( p, Pivot );
else
Acb_NtkUpdateTiming( p, Pivot );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

212
src/base/wlc/wlcGraft.c
View File

@ -302,33 +302,37 @@ Wlc_Ntk_t * Wlc_NtkGraftMulti( Wlc_Ntk_t * p, int fVerbose )
***********************************************************************/
void Sbc_Mult( word a, word b, word r[2] )
{
word pL = (a & 0xFFFFFFFF) * (b & 0xFFFFFFFF);
word pM1 = (a & 0xFFFFFFFF) * (b >> 32);
word pM2 = (a >> 32) * (b & 0xFFFFFFFF);
word Msk = 0xFFFFFFFF;
word pL = (a & Msk) * (b & Msk);
word pM1 = (a & Msk) * (b >> 32);
word pM2 = (a >> 32) * (b & Msk);
word pH = (a >> 32) * (b >> 32);
word Car = (pM1 & 0xFFFFFFFF) + (pM2 & 0xFFFFFFFF) + (pL >> 32);
r[0] = pL;
word Car = (pM1 & Msk) + (pM2 & Msk) + (pL >> 32);
r[0] = a * b;
r[1] = pH + (pM1 >> 32) + (pM2 >> 32) + (Car >> 32);
}
void Sbc_SimMult( word A[64], word B[64], word R[64][2] )
void Sbc_SimMult( word A[64], word B[64], word R[128], int nIns )
{
word a, b, r[2]; int i, k;
word a, b, r[2], Mask = Abc_Tt6Mask(nIns); int i, k;
for ( i = 0; i < 64; i++ )
A[i] = B[i] = R[0][i] = R[1][i] = 0;
A[i] = B[i] = R[i] = R[i+64] = 0;
Gia_ManRandom(1);
for ( i = 0; i < 64; i++ )
{
a = Gia_ManRandom(0);
b = Gia_ManRandom(0);
a = i ? (Mask & Gia_ManRandomW(0)) : 0;
b = i ? (Mask & Gia_ManRandomW(0)) : 0;
Sbc_Mult( a, b, r );
for ( k = 0; k < 64; k++ )
{
if ( (a >> k) & 1 ) A[k] |= (1 << i);
if ( (b >> k) & 1 ) B[k] |= (1 << i);
if ( (r[0] >> k) & 1 ) R[0][k] |= (1 << i);
if ( (r[1] >> k) & 1 ) R[1][k] |= (1 << i);
if ( (a >> k) & 1 ) A[k] |= ((word)1 << i);
if ( (b >> k) & 1 ) B[k] |= ((word)1 << i);
if ( (r[0] >> k) & 1 ) R[k] |= ((word)1 << i);
if ( (r[1] >> k) & 1 ) R[k+64] |= ((word)1 << i);
}
}
// for ( i = 0; i < 128; i++ )
// for ( k = 0; k < 64; k++, printf( "\n" ) )
// printf( "%d", (R[i] >> k) & 1 );
}
/**Function*************************************************************
@ -345,69 +349,181 @@ void Sbc_SimMult( word A[64], word B[64], word R[64][2] )
Vec_Int_t * Sbc_ManDetectMult( Gia_Man_t * p, Vec_Int_t * vIns )
{
int nWords = 1;
Vec_Int_t * vNodes = Vec_IntStart( Vec_IntSize(vIns) );
Vec_Int_t * vGia2Out = Vec_IntStartFull( Gia_ManObjNum(p) );
Gia_Obj_t * pObj; int i, Entry, nIns = Vec_IntSize(vIns)/2;
word A[64], B[64], R[64][2], * pInfoObj;
word A[64], B[64], R[128], * pInfoObj; word Temp;
// create hash table
Vec_Mem_t * vTtMem = Vec_MemAlloc( nWords, 10 );
Vec_MemHashAlloc( vTtMem, 1000 );
Sbc_SimMult( A, B, R, nIns );
for ( i = 0; i < 2*nIns; i++ )
{
Vec_MemHashInsert( vTtMem, R+i );
//printf( "Out %2d : ", i );
//Extra_PrintHex( stdout, (unsigned *)(R+i), 6 ); printf( "\n" );
}
assert( Vec_MemEntryNum(vTtMem) == 2*nIns );
// alloc simulation info
Vec_Mem_t * vTtMem = Vec_MemAlloc( nWords, 10 );
Vec_MemHashAlloc( vTtMem, 10000 );
Vec_WrdFreeP( &p->vSims );
p->vSims = Vec_WrdStart( Gia_ManObjNum(p) * nWords );
p->nSimWords = nWords;
// prepare simulation manager
pInfoObj = Wlc_ObjSim( p, 0 );
Vec_MemHashInsert( vTtMem, pInfoObj );
// mark inputs
Gia_ManIncrementTravId( p );
Gia_ObjSetTravIdCurrentId( p, 0 );
Gia_ManForEachCi( p, pObj, i )
{
Gia_ObjSetTravIdCurrent( p, pObj );
// set internal nodes
assert( Vec_IntSize(vIns) % 2 );
Sbc_SimMult( A, B, R );
Gia_ManIncrementTravId( p );
//Wlc_ObjSimPi( p, Gia_ObjId(p, pObj) );
}
// assign inputs
assert( Vec_IntSize(vIns) % 2 == 0 );
Gia_ManForEachObjVec( vIns, p, pObj, i )
{
Gia_ObjSetTravIdCurrent( p, pObj );
pInfoObj = Wlc_ObjSim( p, Gia_ObjId(p, pObj) );
*pInfoObj = i < nIns ? A[i] : B[nIns-i];
*pInfoObj = i < nIns ? A[i] : B[i - nIns];
}
// perform simulation
Gia_ManForEachObj1( p, pObj, i )
{
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
continue;
if ( Gia_ObjIsAnd(pObj) )
Wlc_ObjSimAnd( p, i );
else if ( Gia_ObjIsCo(pObj) )
Wlc_ObjSimCo( p, i );
else assert( 0 );
// mark each first node
// mark direct polarity
pInfoObj = Wlc_ObjSim( p, i );
Entry = *Vec_MemHashLookup( vTtMem, pInfoObj );
if ( Entry > 0 )
if ( Entry >= 0 )
{
if ( Vec_IntEntry(vNodes, Entry) == 0 ) // new
Vec_IntWriteEntry( vNodes, Entry, Abc_Var2Lit(i, 0) );
Vec_IntWriteEntry( vGia2Out, i, Abc_Var2Lit(Entry, 0) );
continue;
}
// mark negated polarity
Temp = *pInfoObj;
Abc_TtNot( pInfoObj, nWords );
Entry = *Vec_MemHashLookup( vTtMem, pInfoObj );
Abc_TtNot( pInfoObj, nWords );
if ( Entry > 0 )
assert( Temp == *pInfoObj );
if ( Entry >= 0 )
{
if ( Vec_IntEntry(vNodes, Entry) == 0 ) // new
Vec_IntWriteEntry( vNodes, Entry, Abc_Var2Lit(i, 1) );
Vec_IntWriteEntry( vGia2Out, i, Abc_Var2Lit(Entry, 1) );
continue;
}
}
Gia_ManForEachCo( p, pObj, i )
{
pInfoObj = Wlc_ObjSim( p, Gia_ObjId(p, pObj) );
//printf( "Out %2d : Driver = %5d(%d)", i, Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninC0(pObj) );
//Extra_PrintHex( stdout, (unsigned *)pInfoObj, 6 ); printf( "\n" );
}
// cleanup
Vec_MemHashFree( vTtMem );
Vec_MemFreeP( &vTtMem );
Vec_WrdFreeP( &p->vSims );
p->nSimWords = 0;
return vNodes;
//Vec_WrdFreeP( &p->vSims );
//p->nSimWords = 0;
return vGia2Out;
}
Vec_Int_t * Sbc_ManWlcNodes2( Wlc_Ntk_t * pNtk, Gia_Man_t * p, Vec_Int_t * vGiaLits )
{
Wlc_Obj_t * pObj; int i, k, iGiaLit, iFirst, nBits;
Vec_Int_t * vRes = Vec_IntAlloc( 100 );
Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
Vec_IntForEachEntry( vGiaLits, iGiaLit, i )
if ( iGiaLit != -1 )
Vec_IntWriteEntry( vMap, Abc_Lit2Var(iGiaLit), Abc_Var2Lit(i, Abc_LitIsCompl(iGiaLit)) );
Wlc_NtkForEachObj( pNtk, pObj, i )
{
iFirst = Vec_IntEntry( &pNtk->vCopies, i );
nBits = Wlc_ObjRange(pObj);
for ( k = 0; k < nBits; k++ )
{
int iLitGia = Vec_IntEntry( &pNtk->vBits, iFirst + k );
int iLitOut = Vec_IntEntry( vMap, Abc_Lit2Var(iLitGia) );
if ( iLitOut == -1 )
continue;
Vec_IntWriteEntry( vMap, Abc_Lit2Var(iLitGia), -1 );
iLitOut = Abc_LitNotCond( iLitOut, Abc_LitIsCompl(iLitGia) );
printf( "Matched out %d in phase %d with object %d (%s) bit %d (out of %d).\n", Abc_Lit2Var(iLitOut), Abc_LitIsCompl(iLitOut), i, Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k, nBits );
Vec_IntPushUnique( vRes, i );
}
}
Vec_IntFree( vMap );
Vec_IntSort( vRes, 0 );
// consider the last one
pObj = Wlc_NtkObj( pNtk, Vec_IntEntryLast(vRes) );
iFirst = Vec_IntEntry( &pNtk->vCopies, Wlc_ObjId(pNtk, pObj) );
nBits = Wlc_ObjRange(pObj);
printf( "Considering object %d (%s):\n", Wlc_ObjId(pNtk, pObj), Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)) );
for ( k = 0; k < nBits; k++ )
{
int iLitGia = Vec_IntEntry( &pNtk->vBits, iFirst + k );
int iLitOutP = Vec_IntFind( vGiaLits, iLitGia );
int iLitOutN = Vec_IntFind( vGiaLits, Abc_LitNot(iLitGia) );
printf( "Matching bit %d with output %d / %d.\n", k, iLitOutP, iLitOutN );
// print simulation signature
{
word * pInfoObj = Wlc_ObjSim( p, Abc_Lit2Var(iLitGia) );
Extra_PrintHex( stdout, (unsigned *)pInfoObj, 6 ); printf( "\n" );
}
}
return vRes;
}
int Sbc_ManWlcNodes( Wlc_Ntk_t * pNtk, Gia_Man_t * p, Vec_Int_t * vGia2Out, int nOuts )
{
Wlc_Obj_t * pObj;
int i, k, iLitGia, iLitOut, iFirst, nBits, iObjFound = -1;
Vec_Int_t * vMatched = Vec_IntAlloc( 100 );
Wlc_NtkForEachObj( pNtk, pObj, i )
{
iFirst = Vec_IntEntry( &pNtk->vCopies, i );
nBits = Wlc_ObjRange(pObj);
Vec_IntClear( vMatched );
for ( k = 0; k < nBits; k++ )
{
iLitGia = Vec_IntEntry( &pNtk->vBits, iFirst + k );
iLitOut = Vec_IntEntry( vGia2Out, Abc_Lit2Var(iLitGia) );
if ( iLitOut == -1 )
continue;
iLitOut = Abc_LitNotCond( iLitOut, Abc_LitIsCompl(iLitGia) );
printf( "Matched node %5d (%10s) bit %3d (out of %3d) with output %3d(%d).\n",
i, Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k, nBits, Abc_Lit2Var(iLitOut), Abc_LitIsCompl(iLitOut) );
Vec_IntPushOrder( vMatched, Abc_Lit2Var(iLitOut) );
}
if ( Vec_IntSize(vMatched) > 0 )
printf( "\n" );
if ( Vec_IntSize(vMatched) == nOuts )
{
if ( iObjFound == -1 )
iObjFound = i;
printf( "Found object %d with all bits matched.\n", i );
/*
for ( k = nBits-2; k < nBits; k++ )
{
iLitGia = Vec_IntEntry( &pNtk->vBits, iFirst + k );
{
word * pInfoObj = Wlc_ObjSim( p, Abc_Lit2Var(iLitGia) );
Extra_PrintHex( stdout, (unsigned *)pInfoObj, 6 ); printf( "\n" );
}
}
*/
break;
}
}
Vec_IntFree( vMatched );
return iObjFound;
}
/**Function*************************************************************
@ -421,17 +537,31 @@ Vec_Int_t * Sbc_ManDetectMult( Gia_Man_t * p, Vec_Int_t * vIns )
SeeAlso []
***********************************************************************/
void Sbc_ManDetectMultTest( Gia_Man_t * p )
void Sbc_ManDetectMultTest( Wlc_Ntk_t * pNtk, int fVerbose )
{
extern Vec_Int_t * Sdb_StoComputeCutsDetect( Gia_Man_t * pGia );
Gia_Man_t * p = Wlc_NtkBitBlast( pNtk, NULL, -1, 0, 0, 0, 0, 1 );
Vec_Int_t * vIns, * vGia2Out;
int iObjFound = -1;
// Gia_Obj_t * pObj; int i;
// Gia_ManForEachCo( p, pObj, i )
// printf( "Output %2d - driver %5d (%d)\n", i, Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninC0(pObj) );
Vec_Int_t * vIns = Sdb_StoComputeCutsDetect( p );
Vec_Int_t * vNodes = Sbc_ManDetectMult( p, vIns );
vIns = Sdb_StoComputeCutsDetect( p );
if ( vIns == NULL || Vec_IntSize(vIns) == 0 || (Vec_IntSize(vIns) % 2) != 0 )
{
printf( "Input identification did not work out.\n" );
return;
}
Vec_IntPrint( vNodes );
vGia2Out = Sbc_ManDetectMult( p, vIns );
Vec_IntFree( vNodes );
iObjFound = Sbc_ManWlcNodes( pNtk, p, vGia2Out, Vec_IntSize(vIns) );
Vec_IntFree( vGia2Out );
Vec_IntFree( vIns );
Gia_ManStop( p );
}
////////////////////////////////////////////////////////////////////////

4
src/proof/acec/acec2Mult.c
View File

@ -880,7 +880,7 @@ int Sdb_StoDiffExactlyOne2( Vec_Int_t * vAll, int * pCut )
}
Vec_Int_t * Sdb_StoFindInputs( Vec_Wec_t * vCuts, int Front )
{
int fVerbose = 1;
int fVerbose = 0;
Vec_Int_t * vCut, * vCounts;
Vec_Int_t * vRes = Vec_IntAlloc( 100 );
Vec_Int_t * vResA = Vec_IntAlloc( 100 );
@ -906,6 +906,8 @@ Vec_Int_t * Sdb_StoFindInputs( Vec_Wec_t * vCuts, int Front )
Vec_IntForEachEntry( vCounts, Entry, k )
if ( Entry )
MinValue = Abc_MinInt( MinValue, Entry );
if ( MinValue == ABC_INFINITY )
return vRes;
Min = Vec_IntFind( vCounts, MinValue );
Vec_IntPush( vResA, Min );
Vec_IntWriteEntry( vCounts, Min, 0 );

2
src/sat/cnf/cnfMan.c
View File

@ -251,7 +251,7 @@ void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable )
for ( i = 0; i < p->nClauses; i++ )
{
for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) );
fprintf( pFile, "%s%d ", Abc_LitIsCompl(*pLit) ? "-":"", fReadable? Abc_Lit2Var(*pLit) : Abc_Lit2Var(*pLit)+1 );
fprintf( pFile, "\n" );
}
fprintf( pFile, "\n" );