wlc.h File Reference

#include "aig/gia/gia.h"
#include "misc/extra/extra.h"
#include "misc/util/utilNam.h"
#include "misc/mem/mem.h"
#include "misc/util/utilTruth.h"
#include "base/main/mainInt.h"

Include dependency graph for wlc.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	Wlc_Obj_t_
struct	Wlc_Ntk_t_
struct	Wlc_Par_t_
struct	Wlc_BstPar_t_
struct	Wla_Man_t_

Macros
#define	Wlc_NtkForEachObj(p, pObj, i)
	MACRO DEFINITIONS ///.
#define	Wlc_NtkForEachObjReverse(p, pObj, i)
#define	Wlc_NtkForEachObjVec(vVec, p, pObj, i)
#define	Wlc_NtkForEachPi(p, pPi, i)
#define	Wlc_NtkForEachPo(p, pPo, i)
#define	Wlc_NtkForEachCi(p, pCi, i)
#define	Wlc_NtkForEachCo(p, pCo, i)
#define	Wlc_NtkForEachFf(p, pFf, i)
#define	Wlc_NtkForEachFf2(p, pFf, i)
#define	Wlc_ObjForEachFanin(pObj, iFanin, i)
#define	Wlc_ObjForEachFaninObj(p, pObj, pFanin, i)
#define	Wlc_ObjForEachFaninReverse(pObj, iFanin, i)

Typedefs
typedef struct Wlc_Obj_t_	Wlc_Obj_t
	BASIC TYPES ///.
typedef struct Wlc_Ntk_t_	Wlc_Ntk_t
typedef struct Wlc_Par_t_	Wlc_Par_t
typedef struct Wlc_BstPar_t_	Wlc_BstPar_t
typedef struct Wla_Man_t_	Wla_Man_t

Enumerations
enum	Wlc_ObjType_t {   WLC_OBJ_NONE = 0 , WLC_OBJ_PI , WLC_OBJ_PO , WLC_OBJ_FO ,   WLC_OBJ_FI , WLC_OBJ_FF , WLC_OBJ_CONST , WLC_OBJ_BUF ,   WLC_OBJ_MUX , WLC_OBJ_SHIFT_R , WLC_OBJ_SHIFT_RA , WLC_OBJ_SHIFT_L ,   WLC_OBJ_SHIFT_LA , WLC_OBJ_ROTATE_R , WLC_OBJ_ROTATE_L , WLC_OBJ_BIT_NOT ,   WLC_OBJ_BIT_AND , WLC_OBJ_BIT_OR , WLC_OBJ_BIT_XOR , WLC_OBJ_BIT_NAND ,   WLC_OBJ_BIT_NOR , WLC_OBJ_BIT_NXOR , WLC_OBJ_BIT_SELECT , WLC_OBJ_BIT_CONCAT ,   WLC_OBJ_BIT_ZEROPAD , WLC_OBJ_BIT_SIGNEXT , WLC_OBJ_LOGIC_NOT , WLC_OBJ_LOGIC_IMPL ,   WLC_OBJ_LOGIC_AND , WLC_OBJ_LOGIC_OR , WLC_OBJ_LOGIC_XOR , WLC_OBJ_COMP_EQU ,   WLC_OBJ_COMP_NOTEQU , WLC_OBJ_COMP_LESS , WLC_OBJ_COMP_MORE , WLC_OBJ_COMP_LESSEQU ,   WLC_OBJ_COMP_MOREEQU , WLC_OBJ_REDUCT_AND , WLC_OBJ_REDUCT_OR , WLC_OBJ_REDUCT_XOR ,   WLC_OBJ_REDUCT_NAND , WLC_OBJ_REDUCT_NOR , WLC_OBJ_REDUCT_NXOR , WLC_OBJ_ARI_ADD ,   WLC_OBJ_ARI_SUB , WLC_OBJ_ARI_MULTI , WLC_OBJ_ARI_DIVIDE , WLC_OBJ_ARI_REM ,   WLC_OBJ_ARI_MODULUS , WLC_OBJ_ARI_POWER , WLC_OBJ_ARI_MINUS , WLC_OBJ_ARI_SQRT ,   WLC_OBJ_ARI_SQUARE , WLC_OBJ_TABLE , WLC_OBJ_READ , WLC_OBJ_WRITE ,   WLC_OBJ_ARI_ADDSUB , WLC_OBJ_SEL , WLC_OBJ_DEC , WLC_OBJ_LUT ,   WLC_OBJ_NUMBER }
	INCLUDES ///. More...

Functions
int	Wlc_NtkAbsCore (Wlc_Ntk_t *p, Wlc_Par_t *pPars)
	FUNCTION DECLARATIONS ///.
int	Wlc_NtkPdrAbs (Wlc_Ntk_t *p, Wlc_Par_t *pPars)
int	Wlc_NtkAbsCore2 (Wlc_Ntk_t *p, Wlc_Par_t *pPars)
Gia_Man_t *	Wlc_NtkBitBlast (Wlc_Ntk_t *p, Wlc_BstPar_t *pPars)
void	Wlc_SetNtk (Abc_Frame_t *pAbc, Wlc_Ntk_t *pNtk)
Vec_Int_t *	Wlc_NtkCollectMemory (Wlc_Ntk_t *p, int fClean)
void	Wlc_NtkPrintMemory (Wlc_Ntk_t *p)
Wlc_Ntk_t *	Wlc_NtkMemAbstractTest (Wlc_Ntk_t *p)
int	Wlc_NtkMemAbstract (Wlc_Ntk_t *p, int nIterMax, int fDumpAbs, int fPdrVerbose, int fVerbose)
Wlc_Ntk_t *	Wlc_NtkAbstractMem (Wlc_Ntk_t *p, int nFrames, int fVerbose)
Wlc_Ntk_t *	Wlc_ReadNdr (char *pFileName)
void	Wlc_WriteNdr (Wlc_Ntk_t *pNtk, char *pFileName)
Wlc_Ntk_t *	Wlc_NtkFromNdr (void *pData)
void *	Wlc_NtkToNdr (Wlc_Ntk_t *pNtk)
void	Wlc_ManSetDefaultParams (Wlc_Par_t *pPars)
	FUNCTION DEFINITIONS ///.
char *	Wlc_ObjTypeName (Wlc_Obj_t *p)
Wlc_Ntk_t *	Wlc_NtkAlloc (char *pName, int nObjsAlloc)
int	Wlc_ObjAlloc (Wlc_Ntk_t *p, int Type, int Signed, int End, int Beg)
int	Wlc_ObjCreate (Wlc_Ntk_t *p, int Type, int Signed, int End, int Beg, Vec_Int_t *vFanins)
void	Wlc_ObjSetCi (Wlc_Ntk_t *p, Wlc_Obj_t *pObj)
void	Wlc_ObjSetCo (Wlc_Ntk_t *p, Wlc_Obj_t *pObj, int fFlopInput)
char *	Wlc_ObjName (Wlc_Ntk_t *p, int iObj)
void	Wlc_ObjUpdateType (Wlc_Ntk_t *p, Wlc_Obj_t *pObj, int Type)
void	Wlc_ObjAddFanins (Wlc_Ntk_t *p, Wlc_Obj_t *pObj, Vec_Int_t *vFanins)
int	Wlc_ObjDup (Wlc_Ntk_t *pNew, Wlc_Ntk_t *p, int iObj, Vec_Int_t *vFanins)
void	Wlc_NtkFree (Wlc_Ntk_t *p)
int	Wlc_NtkCreateLevels (Wlc_Ntk_t *p)
int	Wlc_NtkCreateLevelsRev (Wlc_Ntk_t *p)
int	Wlc_NtkRemapLevels (Wlc_Ntk_t *p, Vec_Int_t *vObjs, int nLevels)
int	Wlc_NtkCountRealPis (Wlc_Ntk_t *p)
void	Wlc_NtkPrintNode (Wlc_Ntk_t *p, Wlc_Obj_t *pObj)
void	Wlc_NtkPrintNodeArray (Wlc_Ntk_t *p, Vec_Int_t *vArray)
void	Wlc_NtkPrintNodes (Wlc_Ntk_t *p, int Type)
void	Wlc_NtkPrintStats (Wlc_Ntk_t *p, int fDistrib, int fTwoSides, int fVerbose)
void	Wlc_NtkPrintObjects (Wlc_Ntk_t *p)
void	Wlc_NtkTransferNames (Wlc_Ntk_t *pNew, Wlc_Ntk_t *p)
char *	Wlc_NtkNewName (Wlc_Ntk_t *p, int iCoId, int fSeq)
Wlc_Ntk_t *	Wlc_NtkDupDfs (Wlc_Ntk_t *p, int fMarked, int fSeq)
Wlc_Ntk_t *	Wlc_NtkDupDfsAbs (Wlc_Ntk_t *p, Vec_Int_t *vPisOld, Vec_Int_t *vPisNew, Vec_Int_t *vFlops)
Wlc_Ntk_t *	Wlc_NtkDupDfsSimple (Wlc_Ntk_t *p)
void	Wlc_NtkCleanMarks (Wlc_Ntk_t *p)
void	Wlc_NtkMarkCone (Wlc_Ntk_t *p, int iCoId, int Range, int fSeq, int fAllPis)
void	Wlc_NtkProfileCones (Wlc_Ntk_t *p)
Wlc_Ntk_t *	Wlc_NtkDupSingleNodes (Wlc_Ntk_t *p)
void	Wlc_NtkShortNames (Wlc_Ntk_t *p)
int	Wlc_NtkDcFlopNum (Wlc_Ntk_t *p)
void	Wlc_NtkSetRefs (Wlc_Ntk_t *p)
int	Wlc_NtkCountObjBits (Wlc_Ntk_t *p, Vec_Int_t *vPisNew)
Wlc_Ntk_t *	Wlc_ReadSmtBuffer (char *pFileName, char *pBuffer, char *pLimit, int fOldParser, int fPrintTree)
Wlc_Ntk_t *	Wlc_ReadSmt (char *pFileName, int fOldParser, int fPrintTree)
Vec_Ptr_t *	Wlc_NtkSimulate (Wlc_Ntk_t *p, Vec_Int_t *vNodes, int nWords, int nFrames)
void	Wlc_NtkDeleteSim (Vec_Ptr_t *p)
int	Wlc_StdinProcessSmt (Abc_Frame_t *pAbc, char *pCmd)
char *	Wlc_PrsConvertInitValues (Wlc_Ntk_t *p)
Wlc_Ntk_t *	Wlc_ReadVer (char *pFileName, char *pStr, int fInter)
Vec_Int_t *	Wlc_NtkCollectAddMult (Wlc_Ntk_t *p, Wlc_BstPar_t *pPar, int *pCountA, int *CountM)
int	Wlc_NtkPairIsUifable (Wlc_Ntk_t *p, Wlc_Obj_t *pObj, Wlc_Obj_t *pObj2)
Vec_Int_t *	Wlc_NtkCollectMultipliers (Wlc_Ntk_t *p)
Vec_Int_t *	Wlc_NtkFindUifableMultiplierPairs (Wlc_Ntk_t *p)
Wlc_Ntk_t *	Wlc_NtkAbstractNodes (Wlc_Ntk_t *pNtk, Vec_Int_t *vNodes)
Wlc_Ntk_t *	Wlc_NtkUifNodePairs (Wlc_Ntk_t *pNtk, Vec_Int_t *vPairs)
void	Wlc_WinProfileArith (Wlc_Ntk_t *p)
void	Wlc_WriteVer (Wlc_Ntk_t *p, char *pFileName, int fAddCos, int fNoFlops)

Macro Definition Documentation

Wlc_NtkForEachCi

#define Wlc_NtkForEachCi	(		p,
			pCi,
			i )

Value:

    for ( i = 0; (i < Wlc_NtkCiNum(p)) && (((pCi) = Wlc_NtkCi(p, i)), 1); i++ )

Definition at line 366 of file wlc.h.

#define Wlc_NtkForEachCi( p, pCi, i )                                               \
    for ( i = 0; (i < Wlc_NtkCiNum(p)) && (((pCi) = Wlc_NtkCi(p, i)), 1); i++ )

Wlc_NtkForEachCo

#define Wlc_NtkForEachCo	(		p,
			pCo,
			i )

Value:

    for ( i = 0; (i < Wlc_NtkCoNum(p)) && (((pCo) = Wlc_NtkCo(p, i)), 1); i++ )

Definition at line 368 of file wlc.h.

#define Wlc_NtkForEachCo( p, pCo, i )                                               \
    for ( i = 0; (i < Wlc_NtkCoNum(p)) && (((pCo) = Wlc_NtkCo(p, i)), 1); i++ )

Wlc_NtkForEachFf

#define Wlc_NtkForEachFf	(		p,
			pFf,
			i )

Value:

    for ( i = 0; (i < Vec_IntSize(&p->vFfs)) && (((pFf) = Wlc_NtkFf(p, i)), 1); i++ )

Definition at line 370 of file wlc.h.

#define Wlc_NtkForEachFf( p, pFf, i )                                               \
    for ( i = 0; (i < Vec_IntSize(&p->vFfs)) && (((pFf) = Wlc_NtkFf(p, i)), 1); i++ )

Wlc_NtkForEachFf2

#define Wlc_NtkForEachFf2	(		p,
			pFf,
			i )

Value:

    for ( i = 0; (i < Vec_IntSize(&p->vFfs2)) && (((pFf) = Wlc_NtkFf2(p, i)), 1); i++ )

Definition at line 372 of file wlc.h.

#define Wlc_NtkForEachFf2( p, pFf, i )                                              \
    for ( i = 0; (i < Vec_IntSize(&p->vFfs2)) && (((pFf) = Wlc_NtkFf2(p, i)), 1); i++ )

Wlc_NtkForEachObj

#define Wlc_NtkForEachObj	(		p,
			pObj,
			i )

Value:

    for ( i = 1; (i < Wlc_NtkObjNumMax(p)) && (((pObj) = Wlc_NtkObj(p, i)), 1); i++ )

MACRO DEFINITIONS ///.

ITERATORS ///

Definition at line 356 of file wlc.h.

#define Wlc_NtkForEachObj( p, pObj, i )                                             \
    for ( i = 1; (i < Wlc_NtkObjNumMax(p)) && (((pObj) = Wlc_NtkObj(p, i)), 1); i++ )

Wlc_NtkForEachObjReverse

#define Wlc_NtkForEachObjReverse	(		p,
			pObj,
			i )

Value:

    for ( i = Wlc_NtkObjNumMax(p) - 1; (i > 0) && (((pObj) = Wlc_NtkObj(p, i)), 1); i-- )

Definition at line 358 of file wlc.h.

#define Wlc_NtkForEachObjReverse( p, pObj, i )                                      \
    for ( i = Wlc_NtkObjNumMax(p) - 1; (i > 0) && (((pObj) = Wlc_NtkObj(p, i)), 1); i-- )

Wlc_NtkForEachObjVec

#define Wlc_NtkForEachObjVec	(		vVec,
			p,
			pObj,
			i )

Value:

    for ( i = 0; (i < Vec_IntSize(vVec)) && (((pObj) = Wlc_NtkObj(p, Vec_IntEntry(vVec, i))), 1); i++ )

Definition at line 360 of file wlc.h.

#define Wlc_NtkForEachObjVec( vVec, p, pObj, i )                                    \
    for ( i = 0; (i < Vec_IntSize(vVec)) && (((pObj) = Wlc_NtkObj(p, Vec_IntEntry(vVec, i))), 1); i++ )

Wlc_NtkForEachPi

#define Wlc_NtkForEachPi	(		p,
			pPi,
			i )

Value:

    for ( i = 0; (i < Wlc_NtkPiNum(p)) && (((pPi) = Wlc_NtkPi(p, i)), 1); i++ )

Definition at line 362 of file wlc.h.

#define Wlc_NtkForEachPi( p, pPi, i )                                               \
    for ( i = 0; (i < Wlc_NtkPiNum(p)) && (((pPi) = Wlc_NtkPi(p, i)), 1); i++ )

Wlc_NtkForEachPo

#define Wlc_NtkForEachPo	(		p,
			pPo,
			i )

Value:

    for ( i = 0; (i < Wlc_NtkPoNum(p)) && (((pPo) = Wlc_NtkPo(p, i)), 1); i++ )

Definition at line 364 of file wlc.h.

#define Wlc_NtkForEachPo( p, pPo, i )                                               \
    for ( i = 0; (i < Wlc_NtkPoNum(p)) && (((pPo) = Wlc_NtkPo(p, i)), 1); i++ )

Wlc_ObjForEachFanin

#define Wlc_ObjForEachFanin	(		pObj,
			iFanin,
			i )

Value:

    for ( i = 0; (i < Wlc_ObjFaninNum(pObj)) && (((iFanin) = Wlc_ObjFaninId(pObj, i)), 1); i++ )

Definition at line 375 of file wlc.h.

#define Wlc_ObjForEachFanin( pObj, iFanin, i )                                      \
    for ( i = 0; (i < Wlc_ObjFaninNum(pObj)) && (((iFanin) = Wlc_ObjFaninId(pObj, i)), 1); i++ )

Wlc_ObjForEachFaninObj

#define Wlc_ObjForEachFaninObj	(		p,
			pObj,
			pFanin,
			i )

Value:

    for ( i = 0; (i < Wlc_ObjFaninNum(pObj)) && (((pFanin) = Wlc_NtkObj(p, Wlc_ObjFaninId(pObj, i))), 1); i++ )

Definition at line 377 of file wlc.h.

#define Wlc_ObjForEachFaninObj( p, pObj, pFanin, i )                                \
    for ( i = 0; (i < Wlc_ObjFaninNum(pObj)) && (((pFanin) = Wlc_NtkObj(p, Wlc_ObjFaninId(pObj, i))), 1); i++ )

Wlc_ObjForEachFaninReverse

#define Wlc_ObjForEachFaninReverse	(		pObj,
			iFanin,
			i )

Value:

    for ( i = Wlc_ObjFaninNum(pObj) - 1; (i >= 0) && (((iFanin) = Wlc_ObjFaninId(pObj, i)), 1); i-- )

Definition at line 379 of file wlc.h.

#define Wlc_ObjForEachFaninReverse( pObj, iFanin, i )                               \
    for ( i = Wlc_ObjFaninNum(pObj) - 1; (i >= 0) && (((iFanin) = Wlc_ObjFaninId(pObj, i)), 1); i-- )

Typedef Documentation

Wla_Man_t

typedef struct Wla_Man_t_ Wla_Man_t

Definition at line 250 of file wlc.h.

Wlc_BstPar_t

typedef struct Wlc_BstPar_t_ Wlc_BstPar_t

Definition at line 207 of file wlc.h.

Wlc_Ntk_t

typedef struct Wlc_Ntk_t_ Wlc_Ntk_t

Definition at line 135 of file wlc.h.

Wlc_Obj_t

typedef struct Wlc_Obj_t_ Wlc_Obj_t

BASIC TYPES ///.

Definition at line 118 of file wlc.h.

Wlc_Par_t

typedef struct Wlc_Par_t_ Wlc_Par_t

Definition at line 178 of file wlc.h.

Enumeration Type Documentation

Wlc_ObjType_t

enum Wlc_ObjType_t

INCLUDES ///.

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

FileName [wlc.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Verilog parser.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - August 22, 2014.]

Revision [

Id

wlc.h,v 1.00 2014/09/12 00:00:00 alanmi Exp

] PARAMETERS ///

Enumerator
WLC_OBJ_NONE
WLC_OBJ_PI
WLC_OBJ_PO
WLC_OBJ_FO
WLC_OBJ_FI
WLC_OBJ_FF
WLC_OBJ_CONST
WLC_OBJ_BUF
WLC_OBJ_MUX
WLC_OBJ_SHIFT_R
WLC_OBJ_SHIFT_RA
WLC_OBJ_SHIFT_L
WLC_OBJ_SHIFT_LA
WLC_OBJ_ROTATE_R
WLC_OBJ_ROTATE_L
WLC_OBJ_BIT_NOT
WLC_OBJ_BIT_AND
WLC_OBJ_BIT_OR
WLC_OBJ_BIT_XOR
WLC_OBJ_BIT_NAND
WLC_OBJ_BIT_NOR
WLC_OBJ_BIT_NXOR
WLC_OBJ_BIT_SELECT
WLC_OBJ_BIT_CONCAT
WLC_OBJ_BIT_ZEROPAD
WLC_OBJ_BIT_SIGNEXT
WLC_OBJ_LOGIC_NOT
WLC_OBJ_LOGIC_IMPL
WLC_OBJ_LOGIC_AND
WLC_OBJ_LOGIC_OR
WLC_OBJ_LOGIC_XOR
WLC_OBJ_COMP_EQU
WLC_OBJ_COMP_NOTEQU
WLC_OBJ_COMP_LESS
WLC_OBJ_COMP_MORE
WLC_OBJ_COMP_LESSEQU
WLC_OBJ_COMP_MOREEQU
WLC_OBJ_REDUCT_AND
WLC_OBJ_REDUCT_OR
WLC_OBJ_REDUCT_XOR
WLC_OBJ_REDUCT_NAND
WLC_OBJ_REDUCT_NOR
WLC_OBJ_REDUCT_NXOR
WLC_OBJ_ARI_ADD
WLC_OBJ_ARI_SUB
WLC_OBJ_ARI_MULTI
WLC_OBJ_ARI_DIVIDE
WLC_OBJ_ARI_REM
WLC_OBJ_ARI_MODULUS
WLC_OBJ_ARI_POWER
WLC_OBJ_ARI_MINUS
WLC_OBJ_ARI_SQRT
WLC_OBJ_ARI_SQUARE
WLC_OBJ_TABLE
WLC_OBJ_READ
WLC_OBJ_WRITE
WLC_OBJ_ARI_ADDSUB
WLC_OBJ_SEL
WLC_OBJ_DEC
WLC_OBJ_LUT
WLC_OBJ_NUMBER

Definition at line 44 of file wlc.h.

             { 
    WLC_OBJ_NONE = 0,      // 00: unknown
    WLC_OBJ_PI,            // 01: primary input 
    WLC_OBJ_PO,            // 02: primary output
    WLC_OBJ_FO,            // 03: flop output
    WLC_OBJ_FI,            // 04: flop input (unused)
    WLC_OBJ_FF,            // 05: flop
    WLC_OBJ_CONST,         // 06: constant
    WLC_OBJ_BUF,           // 07: buffer
    WLC_OBJ_MUX,           // 08: multiplexer
    WLC_OBJ_SHIFT_R,       // 09: shift right
    WLC_OBJ_SHIFT_RA,      // 10: shift right (arithmetic)
    WLC_OBJ_SHIFT_L,       // 11: shift left
    WLC_OBJ_SHIFT_LA,      // 12: shift left (arithmetic)
    WLC_OBJ_ROTATE_R,      // 13: rotate right
    WLC_OBJ_ROTATE_L,      // 14: rotate left
    WLC_OBJ_BIT_NOT,       // 15: bitwise NOT
    WLC_OBJ_BIT_AND,       // 16: bitwise AND
    WLC_OBJ_BIT_OR,        // 17: bitwise OR
    WLC_OBJ_BIT_XOR,       // 18: bitwise XOR
    WLC_OBJ_BIT_NAND,      // 19: bitwise NAND
    WLC_OBJ_BIT_NOR,       // 20: bitwise OR
    WLC_OBJ_BIT_NXOR,      // 21: bitwise NXOR
    WLC_OBJ_BIT_SELECT,    // 22: bit selection
    WLC_OBJ_BIT_CONCAT,    // 23: bit concatenation
    WLC_OBJ_BIT_ZEROPAD,   // 24: zero padding
    WLC_OBJ_BIT_SIGNEXT,   // 25: sign extension
    WLC_OBJ_LOGIC_NOT,     // 26: logic NOT
    WLC_OBJ_LOGIC_IMPL,    // 27: logic implication
    WLC_OBJ_LOGIC_AND,     // 28: logic AND
    WLC_OBJ_LOGIC_OR,      // 29: logic OR
    WLC_OBJ_LOGIC_XOR,     // 30: logic XOR
    WLC_OBJ_COMP_EQU,      // 31: compare equal
    WLC_OBJ_COMP_NOTEQU,   // 32: compare not equal
    WLC_OBJ_COMP_LESS,     // 33: compare less
    WLC_OBJ_COMP_MORE,     // 34: compare more
    WLC_OBJ_COMP_LESSEQU,  // 35: compare less or equal
    WLC_OBJ_COMP_MOREEQU,  // 36: compare more or equal
    WLC_OBJ_REDUCT_AND,    // 37: reduction AND
    WLC_OBJ_REDUCT_OR,     // 38: reduction OR
    WLC_OBJ_REDUCT_XOR,    // 39: reduction XOR
    WLC_OBJ_REDUCT_NAND,   // 40: reduction NAND
    WLC_OBJ_REDUCT_NOR,    // 41: reduction NOR
    WLC_OBJ_REDUCT_NXOR,   // 42: reduction NXOR
    WLC_OBJ_ARI_ADD,       // 43: arithmetic addition
    WLC_OBJ_ARI_SUB,       // 44: arithmetic subtraction
    WLC_OBJ_ARI_MULTI,     // 45: arithmetic multiplier
    WLC_OBJ_ARI_DIVIDE,    // 46: arithmetic division
    WLC_OBJ_ARI_REM,       // 47: arithmetic remainder
    WLC_OBJ_ARI_MODULUS,   // 48: arithmetic modulus
    WLC_OBJ_ARI_POWER,     // 49: arithmetic power
    WLC_OBJ_ARI_MINUS,     // 50: arithmetic minus
    WLC_OBJ_ARI_SQRT,      // 51: integer square root
    WLC_OBJ_ARI_SQUARE,    // 52: integer square
    WLC_OBJ_TABLE,         // 53: bit table
    WLC_OBJ_READ,          // 54: read port
    WLC_OBJ_WRITE,         // 55: write port
    WLC_OBJ_ARI_ADDSUB,    // 56: adder-subtractor
    WLC_OBJ_SEL,           // 57: positionally encoded selector
    WLC_OBJ_DEC,           // 58: decoder
    WLC_OBJ_LUT,           // 59: lookup table
    WLC_OBJ_NUMBER         // 59: unused
} Wlc_ObjType_t;

Function Documentation

Wlc_ManSetDefaultParams()

void Wlc_ManSetDefaultParams ( Wlc_Par_t * pPars )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 114 of file wlcNtk.c.

{
    memset( pPars, 0, sizeof(Wlc_Par_t) );
    pPars->nBitsAdd      = ABC_INFINITY;   // adder bit-width
    pPars->nBitsMul      = ABC_INFINITY;   // multiplier bit-widht 
    pPars->nBitsMux      = ABC_INFINITY;   // MUX bit-width
    pPars->nBitsFlop     = ABC_INFINITY;   // flop bit-width
    pPars->nIterMax      =         1000;   // the max number of iterations
    pPars->nLimit        = ABC_INFINITY;   // the max number of signals
    pPars->fXorOutput    =            1;   // XOR outputs of word-level miter
    pPars->fCheckClauses =            1;   // Check clauses in the reloaded trace                    
    pPars->fPushClauses  =            0;   // Push clauses in the reloaded trace                    
    pPars->fMFFC         =            1;   // Refine the entire MFFC of a PPI 
    pPars->fPdra         =            0;   // Use pdr -nct 
    pPars->fLoadTrace    =            1;   // Load previous PDR traces 
    pPars->fProofRefine  =            0;   // Use proof-based refinement
    pPars->fHybrid       =            1;   // Use a hybrid of CBR and PBR
    pPars->fCheckCombUnsat =          0;   // Check if ABS becomes comb. unsat
    pPars->fAbs2         =            0;   // Use UFAR style createAbs
    pPars->fProofUsePPI  =            0;   // Use PPI values in PBR
    pPars->fUseBmc3      =            0;   // Run BMC3 in parallel
    pPars->fShrinkAbs    =            0;   // Shrink Abs with BMC
    pPars->fShrinkScratch=            0;   // Restart pdr from scratch after shrinking
    pPars->fVerbose      =            0;   // verbose output`
    pPars->fPdrVerbose   =            0;   // show verbose PDR output
}

Here is the call graph for this function:

Wlc_NtkAbsCore()

int Wlc_NtkAbsCore ( Wlc_Ntk_t * p, Wlc_Par_t * pPars )

extern

FUNCTION DECLARATIONS ///.

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

Synopsis [Performs abstraction.]

Description [Derives initial abstraction based on user-specified parameter values, which tell what is the smallest bit-width of a primitive that is being abstracted away. Currently only add/sub, mul/div, mux, and flop are supported with individual parameters. The second step is to refine the initial abstraction until the point when the property is proved.]

SideEffects []

SeeAlso []

Definition at line 1786 of file wlcAbs.c.

{
    abctime clk = Abc_Clock();
    Vec_Int_t * vBlacks = NULL;
    int nIters, nNodes, nDcFlops, RetValue = -1;
    // start the bitmap to mark objects that cannot be abstracted because of refinement
    // currently, this bitmap is empty because abstraction begins without refinement
    Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) );
    // set up parameters to run PDR
    Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
    Pdr_ManSetDefaultParams( pPdrPars );
    //pPdrPars->fUseAbs    = 1;   // use 'pdr -t'  (on-the-fly abstraction)
    //pPdrPars->fCtgs      = 1;   // use 'pdr -nc' (improved generalization)
    //pPdrPars->fSkipDown  = 0;   // use 'pdr -nc' (improved generalization)
    //pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this
    pPdrPars->fVerbose   = pPars->fPdrVerbose;
    pPdrPars->fVeryVerbose = 0;
    // perform refinement iterations
    for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
    {
        Aig_Man_t * pAig;
        Abc_Cex_t * pCex;
        Vec_Int_t * vPisNew, * vRefine;  
        Gia_Man_t * pGia, * pTemp;
        Wlc_Ntk_t * pAbs;
 
        if ( pPars->fVerbose )
            printf( "\nIteration %d:\n", nIters );
 
        // get abstracted GIA and the set of pseudo-PIs (vPisNew)
        if ( pPars->fAbs2 )
        {
            if ( vBlacks == NULL )
                vBlacks = Wlc_NtkGetBlacks( p, pPars );
            else
                Wlc_NtkUpdateBlacks( p, pPars, &vBlacks, vUnmark, NULL );
            pAbs = Wlc_NtkAbs2( p, vBlacks, NULL );
            vPisNew = Vec_IntDup( vBlacks );
        }
        else
        {
            if ( nIters == 1 && pPars->nLimit < ABC_INFINITY )
                Wlc_NtkSetUnmark( p, pPars, vUnmark );
 
            pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, NULL, pPars->fVerbose );
        }
        pGia = Wlc_NtkBitBlast( pAbs, NULL );
 
        // if the abstraction has flops with DC-init state,
        // new PIs were introduced by bit-blasting at the end of the PI list
        // here we move these variables to be *before* PPIs, because
        // PPIs are supposed to be at the end of the PI list for refinement
        nDcFlops = Wlc_NtkDcFlopNum(pAbs);
        if ( nDcFlops > 0 ) // DC-init flops are present
        {
            pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops );
            Gia_ManStop( pTemp );
        }
        // if the word-level outputs have to be XORs, this is a place to do it
        if ( pPars->fXorOutput )
        {
            pGia = Gia_ManTransformMiter2( pTemp = pGia );
            Gia_ManStop( pTemp );
        }
        if ( pPars->fVerbose )
        {
            printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(vPisNew) ); 
            Gia_ManPrintStats( pGia, NULL );
        }
        Wlc_NtkFree( pAbs );
 
        // try to prove abstracted GIA by converting it to AIG and calling PDR
        pAig = Gia_ManToAigSimple( pGia );
        RetValue = Pdr_ManSolve( pAig, pPdrPars );
        pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
        Aig_ManStop( pAig );
 
        // consider outcomes
        if ( pCex == NULL ) 
        {
            assert( RetValue ); // proved or undecided
            Gia_ManStop( pGia );
            Vec_IntFree( vPisNew );
            break;
        }
 
        // perform refinement
        vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
        Gia_ManStop( pGia );
        Vec_IntFree( vPisNew );
        if ( vRefine == NULL ) // real CEX
        {
            Abc_CexFree( pCex ); // return CEX in the future
            break;
        }
 
        // update the set of objects to be un-abstracted
        nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark );
        if ( pPars->fVerbose )
            printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes );
        Vec_IntFree( vRefine );
        Abc_CexFree( pCex );
    }
    Vec_IntFreeP( &vBlacks );
    Vec_BitFreeP( &vUnmark );
    // report the result
    if ( pPars->fVerbose )
        printf( "\n" );
    printf( "Abstraction " );
    if ( RetValue == 0 )
        printf( "resulted in a real CEX" );
    else if ( RetValue == 1 )
        printf( "is successfully proved" );
    else 
        printf( "timed out" );
    printf( " after %d iterations. ", nIters );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    return RetValue;
}

Here is the call graph for this function:

Wlc_NtkAbsCore2()

int Wlc_NtkAbsCore2 ( Wlc_Ntk_t * p, Wlc_Par_t * pPars )

extern

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

Synopsis [Performs abstraction.]

Description [Derives initial abstraction based on user-specified parameter values, which tell what is the smallest bit-width of a primitive that is being abstracted away. Currently only add/sub, mul/div, mux, and flop are supported with individual parameters. The second step is to refine the initial abstraction until the point when the property is proved.]

SideEffects []

SeeAlso []

Definition at line 302 of file wlcAbs2.c.

{
    abctime clk = Abc_Clock();
    int nIters, nNodes, nDcFlops, RetValue = -1;
    // start the bitmap to mark objects that cannot be abstracted because of refinement
    // currently, this bitmap is empty because abstraction begins without refinement
    Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) );
    // set up parameters to run PDR
    Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
    Pdr_ManSetDefaultParams( pPdrPars );
    pPdrPars->fUseAbs    = 1;   // use 'pdr -t'  (on-the-fly abstraction)
    pPdrPars->fCtgs      = 1;   // use 'pdr -nc' (improved generalization)
    pPdrPars->fSkipDown  = 0;   // use 'pdr -nc' (improved generalization)
    //pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this
    pPdrPars->fVerbose   = pPars->fPdrVerbose;
    // perform refinement iterations
    for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
    {
        Aig_Man_t * pAig;
        Abc_Cex_t * pCex;
        Vec_Int_t * vPisNew, * vRefine;  
        Gia_Man_t * pGia, * pTemp;
        Wlc_Ntk_t * pAbs;
 
        if ( pPars->fVerbose )
            printf( "\nIteration %d:\n", nIters );
 
        // get abstracted GIA and the set of pseudo-PIs (vPisNew)
        pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, pPars->fVerbose );
        pGia = Wlc_NtkBitBlast( pAbs, NULL );
 
        // if the abstraction has flops with DC-init state,
        // new PIs were introduced by bit-blasting at the end of the PI list
        // here we move these variables to be *before* PPIs, because
        // PPIs are supposed to be at the end of the PI list for refinement
        nDcFlops = Wlc_NtkDcFlopNum(pAbs);
        if ( nDcFlops > 0 ) // DC-init flops are present
        {
            pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops );
            Gia_ManStop( pTemp );
        }
        // if the word-level outputs have to be XORs, this is a place to do it
        if ( pPars->fXorOutput )
        {
            pGia = Gia_ManTransformMiter2( pTemp = pGia );
            Gia_ManStop( pTemp );
        }
        if ( pPars->fVerbose )
        {
            printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(vPisNew) ); 
            Gia_ManPrintStats( pGia, NULL );
        }
        Wlc_NtkFree( pAbs );
 
        // try to prove abstracted GIA by converting it to AIG and calling PDR
        pAig = Gia_ManToAigSimple( pGia );
        RetValue = Pdr_ManSolve( pAig, pPdrPars );
        pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
        Aig_ManStop( pAig );
 
        // consider outcomes
        if ( pCex == NULL ) 
        {
            assert( RetValue ); // proved or undecided
            Gia_ManStop( pGia );
            Vec_IntFree( vPisNew );
            break;
        }
 
        // perform refinement
        vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
        Gia_ManStop( pGia );
        Vec_IntFree( vPisNew );
        if ( vRefine == NULL ) // real CEX
        {
            Abc_CexFree( pCex ); // return CEX in the future
            break;
        }
 
        // update the set of objects to be un-abstracted
        nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark );
        if ( pPars->fVerbose )
            printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes );
        Vec_IntFree( vRefine );
        Abc_CexFree( pCex );
    }
    Vec_BitFree( vUnmark );
    // report the result
    if ( pPars->fVerbose )
        printf( "\n" );
    printf( "Abstraction " );
    if ( RetValue == 0 )
        printf( "resulted in a real CEX" );
    else if ( RetValue == 1 )
        printf( "is successfully proved" );
    else 
        printf( "timed out" );
    printf( " after %d iterations. ", nIters );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    return RetValue;
}

Here is the call graph for this function:

Wlc_NtkAbstractMem()

Wlc_Ntk_t * Wlc_NtkAbstractMem ( Wlc_Ntk_t * p, int nFrames, int fVerbose )

extern

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

Synopsis [Perform abstraction.]

Description []

SideEffects []

SeeAlso []

Definition at line 1383 of file wlcMem.c.

{
    Vec_Int_t * vMemObjsAll   = Wlc_NtkCollectMemory( p, 0 );
    Vec_Int_t * vMemObjsClean = Wlc_NtkCollectMemory( p, 1 );
    Vec_Int_t * vReachReadCi  = Wlc_NtkFindReachablePiFo( p, vMemObjsClean, nFrames );
    Wlc_Ntk_t * pNew, * pTemp;
    Wlc_Obj_t * pObj;
    Vec_Int_t * vFanins  = Vec_IntAlloc( 100 );
    int i, Po0, Po1, iObjNew;
 
    assert( nFrames == 0 );
 
    // mark memory nodes
    Wlc_NtkCleanMarks( p );
    Wlc_NtkForEachObjVec( vMemObjsAll, p, pObj, i )
        pObj->Mark = 1;
 
    // start new network
    Wlc_NtkCleanCopy( p );
    pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc + Vec_IntSize(vMemObjsClean) * nFrames * 10 );
    pNew->fSmtLib   = p->fSmtLib;
    pNew->fAsyncRst = p->fAsyncRst;
    pNew->fMemPorts = p->fMemPorts;
    pNew->fEasyFfs  = p->fEasyFfs;
    pNew->vInits    = Vec_IntAlloc( 100 );
 
    // duplicate PIs
    Wlc_NtkForEachPi( p, pObj, i )
        if ( !pObj->Mark )
            Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
 
    // create new PIs
    assert( Vec_IntSize(vReachReadCi) % 3 == 0 );
    for ( i = 0; i < Vec_IntSize(vReachReadCi)/3; i++ )
    {
        pObj = Wlc_NtkObj( p, Vec_IntEntry( vReachReadCi, 3*i ) );
        assert( Wlc_ObjIsRead(pObj) );
        iObjNew = Wlc_NtkDupOneObject( pNew, p, pObj, WLC_OBJ_PI, vFanins );
        Vec_IntWriteEntry( vReachReadCi, 3*i+2, iObjNew );
    }
    //Vec_IntPrint( vReachReadCi );
 
    // duplicate flop outputs
    Wlc_NtkForEachCi( p, pObj, i )
        if ( !Wlc_ObjIsPi(pObj) && !pObj->Mark )
        {
            Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
            Vec_IntPush( pNew->vInits, Vec_IntEntry(p->vInits, i-Wlc_NtkPiNum(p)) );
        }
 
/*
    // create flops for memory objects
    Wlc_NtkForEachObjVec( vMemFanins, p, pObj, i )
        for ( k = 0; k < nFrames; k++ )
            Wlc_NtkDupOneObject( pNew, p, pObj, WLC_OBJ_FO, vFanins );
*/
 
    // create buffers for read ports
    Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, i )
    {
        if ( !Wlc_ObjIsRead(pObj) )
            continue;
        iObjNew = Wlc_ObjAlloc( pNew, WLC_OBJ_BUF, pObj->Signed, pObj->End, pObj->Beg );
        Wlc_ObjSetCopy( p, Wlc_ObjId(p, pObj), iObjNew );
    }
 
    // duplicate objects
    Wlc_NtkForEachObj( p, pObj, i )
        if ( !Wlc_ObjIsCi(pObj) && !pObj->Mark )
            Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
 
    // create memory constraints
    Wlc_NtkCreateMemoryConstr( pNew, p, vMemObjsClean, vReachReadCi );
 
    // create outpus
    if ( Vec_IntSize(&p->vPoPairs) )
    {
        // create miter for the PO pairs
        Vec_IntForEachEntryDouble( &p->vPoPairs, Po0, Po1, i )
        {
            int iCopy0 = Wlc_ObjCopy(p, Wlc_ObjId(p, Wlc_NtkPo(p, Po0)));
            int iCopy1 = Wlc_ObjCopy(p, Wlc_ObjId(p, Wlc_NtkPo(p, Po1)));
            int iObj = Wlc_ObjAlloc( pNew, WLC_OBJ_COMP_NOTEQU, 0, 0, 0 );
            Wlc_Obj_t * pObjNew = Wlc_NtkObj( pNew, iObj );
            Vec_IntFillTwo( vFanins, 1, iCopy0, iCopy1 );
            Wlc_ObjAddFanins( pNew, pObjNew, vFanins );
            Wlc_ObjSetCo( pNew, pObjNew, 0 );
        }
        printf( "Memory abstraction created %d miter outputs.\n", Wlc_NtkPoNum(pNew) );
        Wlc_NtkForEachCo( p, pObj, i )
            if ( pObj->fIsFi && !pObj->Mark )
                Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
    }
    else
    {
        // duplicate POs
        Wlc_NtkForEachPo( p, pObj, i )
            if ( !pObj->Mark )
                Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
        // duplicate FIs
        Wlc_NtkForEachCo( p, pObj, i )
            if ( !Wlc_ObjIsPo(pObj) && !pObj->Mark )
                Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
    }
 
/*
    // create new flop inputs
    Wlc_NtkForEachObjVec( vMemFanins, p, pObj, i )
        for ( k = 0; k < nFrames; k++ )
            Wlc_NtkDupOneBuffer( pNew, p, pObj, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj))-(nFrames-1-k), vFanins, 1 );
*/
 
    // append init states
    pNew->pInits = Wlc_PrsConvertInitValues( pNew );
    if ( p->pSpec )
        pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    if ( Wlc_NtkHasNameId(p) )
        Wlc_NtkTransferNames( pNew, p );
    Vec_IntFree( vFanins );
    Vec_IntFree( vMemObjsAll );
    Vec_IntFree( vMemObjsClean );
    Vec_IntFree( vReachReadCi );
    Wlc_NtkCleanMarks( p );
    // derive topological order
//printf( "Objects before = %d.\n", Wlc_NtkObjNum(pNew) );
    pNew = Wlc_NtkDupDfs( pTemp = pNew, 0, 1 );
    Wlc_NtkFree( pTemp );
//printf( "Objects after = %d.\n", Wlc_NtkObjNum(pNew) );
    return pNew;
}

Here is the call graph for this function:

Wlc_NtkAbstractNodes()

Wlc_Ntk_t * Wlc_NtkAbstractNodes ( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit )

extern

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

Synopsis [Abstracts nodes by replacing their outputs with new PIs.]

Description [If array is NULL, abstract all multipliers.]

SideEffects []

SeeAlso []

Definition at line 182 of file wlcUif.c.

{
    Vec_Int_t * vNodes = vNodesInit;
    Wlc_Ntk_t * pNew;
    Wlc_Obj_t * pObj;
    int i, k, iObj, iFanin;
    // get multipliers if not given
    if ( vNodes == NULL )
        vNodes = Wlc_NtkCollectMultipliers( p );
    if ( vNodes == NULL )
        return NULL;
    // mark nodes
    Wlc_NtkForEachObjVec( vNodes, p, pObj, i )
        pObj->Mark = 1;
    // iterate through the nodes in the DFS order
    Wlc_NtkCleanCopy( p );
    Wlc_NtkForEachObj( p, pObj, i )
    {
        if ( i == Vec_IntSize(&p->vCopies) )
            break;
        if ( pObj->Mark ) {
            // clean
            pObj->Mark = 0;
            // add fresh PI with the same number of bits
            iObj = Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 );
        }
        else {
            // update fanins 
            Wlc_ObjForEachFanin( pObj, iFanin, k )
                Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin);
            // node to remain
            iObj = i;
        }
        Wlc_ObjSetCopy( p, i, iObj );
    }
    // POs do not change in this procedure
    if ( vNodes != vNodesInit )
        Vec_IntFree( vNodes );
    // reconstruct topological order
    pNew = Wlc_NtkDupDfs( p, 0, 1 );
    return pNew;
}

Here is the call graph for this function:

Wlc_NtkAlloc()

Wlc_Ntk_t * Wlc_NtkAlloc ( char * pName, int nObjsAlloc )

extern

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

Synopsis [Working with models.]

Description []

SideEffects []

SeeAlso []

Definition at line 152 of file wlcNtk.c.

{
    Wlc_Ntk_t * p;
    p = ABC_CALLOC( Wlc_Ntk_t, 1 );
    p->pName = pName ? Extra_FileNameGeneric( pName ) : NULL;
    Vec_IntGrow( &p->vPis, 111 );
    Vec_IntGrow( &p->vPos, 111 );
    Vec_IntGrow( &p->vCis, 111 );
    Vec_IntGrow( &p->vCos, 111 );
    Vec_IntGrow( &p->vFfs, 111 );
    p->pMemFanin = Mem_FlexStart();
    p->nObjsAlloc = nObjsAlloc;  
    p->pObjs = ABC_CALLOC( Wlc_Obj_t, p->nObjsAlloc );
    p->iObj = 1;
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_NtkBitBlast()

Gia_Man_t * Wlc_NtkBitBlast ( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1349 of file wlcBlast.c.

{
    int fVerbose = 0;
    int fUseOldMultiplierBlasting = 0;
    int fSkipBitRange = 0;
    Tim_Man_t * pManTime = NULL;
    If_LibBox_t * pBoxLib = NULL;
    Vec_Ptr_t * vTables = NULL;
    Vec_Int_t * vFf2Ci = Vec_IntAlloc( 100 );
    Vec_Int_t * vRegClasses = NULL;
    Gia_Man_t * pTemp, * pNew, * pExtra = NULL;
    Wlc_Obj_t * pObj, * pObj2;
    Vec_Int_t * vBits = &p->vBits, * vTemp0, * vTemp1, * vTemp2, * vRes, * vAddOutputs = NULL, * vAddObjs = NULL;
    int nBits = Wlc_NtkPrepareBits( p );
    int nRange, nRange0, nRange1, nRange2, nRange3;
    int i, k, b, iFanin, iLit, nAndPrev, * pFans0, * pFans1, * pFans2, * pFans3;
    int nFFins = 0, nFFouts = 0, curPi = 0, curPo = 0, nFf2Regs = 0;
    int nBitCis = 0, nBitCos = 0, fAdded = 0;
    Wlc_BstPar_t Par, * pPar = &Par;
    Wlc_BstParDefault( pPar );
    pPar = pParIn ? pParIn : pPar;
    Vec_IntClear( vBits );
    Vec_IntGrow( vBits, nBits );
    vTemp0 = Vec_IntAlloc( 1000 );
    vTemp1 = Vec_IntAlloc( 1000 );
    vTemp2 = Vec_IntAlloc( 1000 );
    vRes   = Vec_IntAlloc( 1000 );
    // clean AND-gate counters
    memset( p->nAnds, 0, sizeof(int) * WLC_OBJ_NUMBER );
    // create AIG manager
    pNew = Gia_ManStart( 5 * Wlc_NtkObjNum(p) + 1000 );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->fGiaSimple = pPar->fGiaSimple;
    if ( !pPar->fGiaSimple )
        Gia_ManHashAlloc( pNew );
    if ( pPar->fAddOutputs )
        vAddOutputs = Vec_IntAlloc( 100 );
    if ( pPar->fAddOutputs )
        vAddObjs = Vec_IntAlloc( 100 );
    // prepare for AIG with boxes
    if ( pPar->vBoxIds )
    {
        int nNewCis = 0, nNewCos = 0;
        assert( Vec_IntSize(&p->vFfs2) == 0 );
        Wlc_NtkForEachObj( p, pObj, i )
            pObj->Mark = 0;
        // count bit-width of regular CIs/COs
        Wlc_NtkForEachCi( p, pObj, i )
            nBitCis += Wlc_ObjRange( pObj );
        Wlc_NtkForEachCo( p, pObj, i )
            nBitCos += Wlc_ObjRange( pObj );
        // count bit-width of additional CIs/COs due to selected multipliers
        assert( Vec_IntSize(pPar->vBoxIds) > 0 );
        Wlc_NtkForEachObjVec( pPar->vBoxIds, p, pObj, i )
        {
            // currently works only for multipliers
            assert( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_ADD );
            nNewCis += Wlc_ObjRange( pObj );
            nNewCos += Wlc_ObjRange( Wlc_ObjFanin0(p, pObj) );
            nNewCos += Wlc_ObjRange( Wlc_ObjFanin1(p, pObj) );
            if ( Wlc_ObjFaninNum(pObj) > 2 )
            nNewCos += Wlc_ObjRange( Wlc_ObjFanin2(p, pObj) );
            pObj->Mark = 1;
        }
        // create hierarchy manager
        pManTime = Tim_ManStart( nBitCis + nNewCis, nBitCos + nNewCos );
        curPi = nBitCis;
        curPo = 0;
        // create AIG manager for logic of the boxes
        pExtra = Gia_ManStart( Wlc_NtkObjNum(p) );
        Gia_ManHashAlloc( pExtra );
        assert( !pPar->fGiaSimple );
        // create box library
        pBoxLib = If_LibBoxStart();
    }
    if ( Vec_IntSize(&p->vFfs2) > 0 )
    {
        Vec_Int_t * vSignature;
        int nNewCis = 0, nNewCos = 0;
        assert( pPar->vBoxIds == 0 );
        // count bit-width of regular CIs/COs
        Wlc_NtkForEachCi( p, pObj, i )
            nBitCis += Wlc_ObjRange( pObj );
        Wlc_NtkForEachCo( p, pObj, i )
            nBitCos += Wlc_ObjRange( pObj );
        // count bit-width of additional CIs/COs due to selected multipliers
        Wlc_NtkForEachFf2( p, pObj, i )
        {
            // currently works only for multipliers
            assert( pObj->Type == WLC_OBJ_FF );
            assert( Wlc_ObjRange(pObj) == Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) );
            nNewCis += Wlc_ObjRange(pObj);
            nNewCos += 2*Wlc_ObjRange(pObj) + 3;
            nFf2Regs+= Wlc_ObjRange(pObj);
        }
        // create hierarchy manager
        pManTime = Tim_ManStart( nBitCis + nNewCis + nFf2Regs, nBitCos + nNewCos + nFf2Regs );
        curPi = nBitCis + nFf2Regs;
        curPo = 0;
        // create AIG manager for logic of the boxes
        pExtra = Gia_ManStart( Wlc_NtkObjNum(p) );
        Gia_ManHashAlloc( pExtra );
        assert( !pPar->fGiaSimple );
        // create register classes
        vRegClasses = Vec_IntAlloc(0);
        vSignature = Vec_IntAlloc( 100 );
        Vec_IntPushTwo( vSignature, -1, -1 );
        Wlc_NtkForEachFf2( p, pObj, i )
        {
            int iClk0,  iClk  = Wlc_ObjFaninId( pObj, 1 );
            int iAsyn0, iAsyn = Wlc_ObjFaninId( pObj, 5 );
            nRange = Wlc_ObjRange(pObj);
            Vec_IntForEachEntryDouble( vSignature, iClk0, iAsyn0, k )
                if ( iClk == iClk0 && iAsyn == iAsyn0 )
                {
                    for ( b = 0; b < nRange; b++ )
                        Vec_IntPush( vRegClasses, k/2 );
                    break;
                }
            if ( k < Vec_IntSize(vSignature) )
                continue;
            for ( b = 0; b < nRange; b++ )
                Vec_IntPush( vRegClasses, k/2 );
            Vec_IntPushTwo( vSignature, iClk, iAsyn );
        }
        assert( Vec_IntSize(vRegClasses) == nFf2Regs );
        Vec_IntFree( vSignature );
        // create box library
        pBoxLib = If_LibBoxStart();
    }
    //printf( "Init state: %s\n", p->pInits );
 
    // blast in the topological order
    Wlc_NtkForEachObj( p, pObj, i )
    {
        //char * pName1 = Wlc_ObjName(p, i);
        //char * pName2 = Wlc_ObjFaninNum(pObj) ? Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) : NULL;
 
        nAndPrev = Gia_ManAndNum(pNew);
        nRange  = Wlc_ObjRange( pObj );
        nRange0 = Wlc_ObjFaninNum(pObj) > 0 ? Wlc_ObjRange( Wlc_ObjFanin0(p, pObj) ) : -1;
        nRange1 = Wlc_ObjFaninNum(pObj) > 1 ? Wlc_ObjRange( Wlc_ObjFanin1(p, pObj) ) : -1;
        nRange2 = Wlc_ObjFaninNum(pObj) > 2 ? Wlc_ObjRange( Wlc_ObjFanin2(p, pObj) ) : -1;
        nRange3 = Wlc_ObjFaninNum(pObj) > 3 ? Wlc_ObjRange( Wlc_ObjFanin(p, pObj, 3) ) : -1;
        pFans0  = pObj->Type != WLC_OBJ_FF && Wlc_ObjFaninNum(pObj) > 0 ? Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId0(pObj)) ) : NULL;
        pFans1  = pObj->Type != WLC_OBJ_FF && Wlc_ObjFaninNum(pObj) > 1 ? Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId1(pObj)) ) : NULL;
        pFans2  = pObj->Type != WLC_OBJ_FF && Wlc_ObjFaninNum(pObj) > 2 ? Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId2(pObj)) ) : NULL;
        pFans3  = pObj->Type != WLC_OBJ_FF && Wlc_ObjFaninNum(pObj) > 3 ? Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId(pObj,3)) ) : NULL;
        Vec_IntClear( vRes );
        assert( nRange > 0 );
        if ( pPar->vBoxIds && pObj->Mark )
        {
            If_Box_t * pBox;
            char Buffer[100];
            float * pTable;
            int CarryIn = 0;
 
            pObj->Mark = 0;
            assert( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB );
 
            // account for carry-in
            if ( Wlc_ObjFaninNum(pObj) == 3 )
                assert( nRange2 == 1 );
            else
                nRange2 = 0;
 
            // create new box
            if ( vTables == NULL ) {
                Tim_ManSetDelayTables( pManTime, (vTables = Vec_PtrAlloc(100)) );
                Vec_PtrPush( vTables, NULL );
            }
            Tim_ManCreateBox( pManTime, curPo, nRange0 + nRange1 + nRange2, curPi, nRange, Vec_PtrSize(vTables), 0 );
            Tim_ManBoxSetCopy( pManTime, Tim_ManBoxNum(pManTime)-1, Tim_ManBoxNum(pManTime)-1 );
            curPi += nRange;
            curPo += nRange0 + nRange1 + nRange2;
 
            // create delay table
            pTable = ABC_ALLOC( float, 3 + nRange * (nRange0 + nRange1 + nRange2) );
            pTable[0] = Vec_PtrSize(vTables);
            pTable[1] = nRange0 + nRange1 + nRange2;
            pTable[2] = nRange;
            for ( k = 0; k < nRange * (nRange0 + nRange1 + nRange2); k++ )
                pTable[3 + k] = 1.0;
            Vec_PtrPush( vTables, pTable );
 
            // create combinational outputs in the normal manager
            for ( k = 0; k < nRange0; k++ )
                Gia_ManAppendCo( pNew, pFans0[k] );
            for ( k = 0; k < nRange1; k++ )
                Gia_ManAppendCo( pNew, pFans1[k] );
            for ( k = 0; k < nRange2; k++ )
                Gia_ManAppendCo( pNew, pFans2[0] );
 
            // make sure there is enough primary inputs in the manager
            for ( k = Gia_ManPiNum(pExtra); k < nRange0 + nRange1 + nRange2; k++ )
                Gia_ManAppendCi( pExtra );
            // create combinational inputs
            Vec_IntClear( vTemp0 );
            for ( k = 0; k < nRange0; k++ )
                Vec_IntPush( vTemp0, Gia_Obj2Lit(pExtra, Gia_ManPi(pExtra, k)) );
            Vec_IntClear( vTemp1 );
            for ( k = 0; k < nRange1; k++ )
                Vec_IntPush( vTemp1, Gia_Obj2Lit(pExtra, Gia_ManPi(pExtra, nRange0+k)) );
            if ( nRange2 == 1 )
                CarryIn = Gia_Obj2Lit(pExtra, Gia_ManPi(pExtra, nRange0+nRange1));
 
            // get new fanin arrays
            pFans0 = Vec_IntArray( vTemp0 );
            pFans1 = Vec_IntArray( vTemp1 );
 
            // bit-blast in the external manager
            if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB ) 
            {
                int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
                int * pArg0 = Wlc_VecLoadFanins( vRes,   pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
                int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
                if ( pObj->Type == WLC_OBJ_ARI_ADD )
                    Wlc_BlastAdder( pExtra, pArg0, pArg1, nRange, CarryIn ); // result is in pFan0 (vRes)
                else 
                    Wlc_BlastSubtract( pExtra, pArg0, pArg1, nRange, 1 ); // result is in pFan0 (vRes)
                Vec_IntShrink( vRes, nRange );
            }
            else if ( fUseOldMultiplierBlasting )
            {                
                int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
                int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
                int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
                Wlc_BlastMultiplier2( pExtra, pArg0, pArg1, nRange, vTemp2, vRes );
                Vec_IntShrink( vRes, nRange );
            }
            else
            {
                int fSigned = Wlc_ObjIsSignedFanin01(p, pObj);
                int nRangeMax = Abc_MaxInt(nRange0, nRange1);
                int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, fSigned );
                int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, fSigned );
                Wlc_BlastMultiplier( pExtra, pArg0, pArg1, nRangeMax, nRangeMax, vTemp2, vRes, fSigned );
                if ( nRange > nRangeMax + nRangeMax )
                    Vec_IntFillExtra( vRes, nRange, fSigned ? Vec_IntEntryLast(vRes) : 0 );
                else
                    Vec_IntShrink( vRes, nRange );
                assert( Vec_IntSize(vRes) == nRange );
            }
            // create outputs in the external manager
            for ( k = 0; k < nRange; k++ )
                Gia_ManAppendCo( pExtra, Vec_IntEntry(vRes, k) );
 
            // create combinational inputs in the normal manager
            Vec_IntClear( vRes );
            for ( k = 0; k < nRange; k++ )
                Vec_IntPush( vRes, Gia_ManAppendCi(pNew) );
 
            // add box to the library
            sprintf( Buffer, "%s%03d", pObj->Type == WLC_OBJ_ARI_ADD ? "add":"mul", 1+If_LibBoxNum(pBoxLib) );
            pBox = If_BoxStart( Abc_UtilStrsav(Buffer), 1+If_LibBoxNum(pBoxLib), nRange0 + nRange1 + nRange2, nRange, 0, 0, 0 ); 
            If_LibBoxAdd( pBoxLib, pBox );
            for ( k = 0; k < pBox->nPis * pBox->nPos; k++ )
                pBox->pDelays[k] = 1;
        }
        else if ( Wlc_ObjIsCi(pObj) || pObj->Type == WLC_OBJ_FF ) // assuming that FFs are ordered immediately after PIs
        {
            if ( pObj->Type == WLC_OBJ_FF )
                Vec_IntPush( vFf2Ci, Gia_ManCiNum(pNew) );
            if ( Wlc_ObjRangeIsReversed(pObj) )
            {
                for ( k = 0; k < nRange; k++ )
                    Vec_IntPush( vRes, -1 );
                for ( k = 0; k < nRange; k++ )
                    Vec_IntWriteEntry( vRes, Vec_IntSize(vRes)-1-k, Gia_ManAppendCi(pNew) );
            }
            else
            {
                for ( k = 0; k < nRange; k++ )
                    Vec_IntPush( vRes, Gia_ManAppendCi(pNew) );
            }
            if ( pObj->Type == WLC_OBJ_FO )
                nFFouts += Vec_IntSize(vRes);
            if ( pObj->Type == WLC_OBJ_FF )
            {
                // complement flop output whose init state is 1
            }
        }
        else if ( pObj->Type == WLC_OBJ_BUF )
        {
            int nRangeMax = Abc_MaxInt( nRange0, nRange );
            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin0(p, pObj) );
            for ( k = 0; k < nRange; k++ )
                Vec_IntPush( vRes, pArg0[k] );
        }
        else if ( pObj->Type == WLC_OBJ_CONST )
        {
            word * pTruth = (word *)Wlc_ObjFanins(pObj);
            for ( k = 0; k < nRange; k++ )
                Vec_IntPush( vRes, Abc_TtGetBit(pTruth, k) );
        }
        else if ( pObj->Type == WLC_OBJ_MUX )
        {
            // It is strange and disturbing that Verilog standard treats these statements differently:
            // Statement 1:   
            //     assign o = i ? b : a;
            // Statement 2:
            //     always @( i or a or b )
            //       begin
            //         case ( i )
            //           0 : o = a ;
            //           1 : o = b ;
            //         endcase
            //       end
            // If a is signed and b is unsigned,  Statement 1 does not sign-extend a, while Statement 2 does.
            // The signedness of o does not matter.
            //
            // Below we (somewhat arbitrarily) distinguish these two by assuming that 
            // Statement 1 has three fanins, while Statement 2 has more than three fanins.
            //
            int fSigned = 1;
            assert( nRange0 >= 1 && Wlc_ObjFaninNum(pObj) >= 3 );
            assert( 1 + (1 << nRange0) == Wlc_ObjFaninNum(pObj) );
            Wlc_ObjForEachFanin( pObj, iFanin, k )
                if ( k > 0 )
                    fSigned &= Wlc_NtkObj(p, iFanin)->Signed;
            if ( pParIn->fBlastNew && nRange0 <= 16 )
            {
                char * pNums = Wlc_NtkMuxTreeString( nRange0 );
                Vec_Int_t ** pvDecs = Wlc_NtkMuxTree3DecsDerive( pNew, pFans0, nRange0, pNums );
                for ( b = 0; b < nRange; b++ )
                {
                    Vec_IntClear( vTemp0 );
                    Wlc_ObjForEachFanin( pObj, iFanin, k ) {
                        if ( k > 0 )
                        {
                            nRange1 = Wlc_ObjRange( Wlc_NtkObj(p, iFanin) );
                            pFans1  = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, iFanin) );
                            if ( Wlc_ObjFaninNum(pObj) == 3 ) // Statement 1
                                Vec_IntPush( vTemp0, b < nRange1 ? pFans1[b] : (fSigned? pFans1[nRange1-1] : 0) );
                            else // Statement 2
                                Vec_IntPush( vTemp0, b < nRange1 ? pFans1[b] : (Wlc_NtkObj(p, iFanin)->Signed? pFans1[nRange1-1] : 0) );
                        }
                    }
                    assert( (1 << nRange0) == Vec_IntSize(vTemp0) );
                    Vec_IntPush( vRes, Wlc_NtkMuxTree3(pNew, vTemp0, pNums, pvDecs) );
                }
                Wlc_NtkMuxTree3DecsFree( pvDecs, pNums );
            }
            else
            {
                Vec_IntClear( vTemp1 );
                if ( pPar->fDecMuxes )
                {
                    for ( k = 0; k < (1 << nRange0); k++ )
                    {
                        int iLitAnd = 1;
                        for ( b = 0; b < nRange0; b++ )
                            iLitAnd = Gia_ManHashAnd( pNew, iLitAnd, Abc_LitNotCond(pFans0[b], ((k >> b) & 1) == 0) );
                        Vec_IntPush( vTemp1, iLitAnd );
                    }
                }
                for ( b = 0; b < nRange; b++ )
                {
                    Vec_IntClear( vTemp0 );
                    Wlc_ObjForEachFanin( pObj, iFanin, k )
                        if ( k > 0 )
                        {
                            nRange1 = Wlc_ObjRange( Wlc_NtkObj(p, iFanin) );
                            pFans1  = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, iFanin) );
                            if ( Wlc_ObjFaninNum(pObj) == 3 ) // Statement 1
                                Vec_IntPush( vTemp0, b < nRange1 ? pFans1[b] : (fSigned? pFans1[nRange1-1] : 0) );
                            else // Statement 2
                                Vec_IntPush( vTemp0, b < nRange1 ? pFans1[b] : (Wlc_NtkObj(p, iFanin)->Signed? pFans1[nRange1-1] : 0) );
                        }
                    if ( pPar->fDecMuxes )
                        Vec_IntPush( vRes, Wlc_NtkMuxTree2(pNew, pFans0, nRange0, vTemp0, vTemp1, vTemp2) );
                    else
                        Vec_IntPush( vRes, Wlc_NtkMuxTree_rec(pNew, pFans0, nRange0, vTemp0, 0) );
                }
            }
        }
        else if ( pObj->Type == WLC_OBJ_SEL )
        {
            assert( nRange0 == Wlc_ObjFaninNum(pObj)-1 );
            Vec_IntClear( vTemp1 );
            for ( k = 0; k < nRange0; k++ )
                Vec_IntPush( vTemp1, pFans0[k] );
            for ( b = 0; b < nRange; b++ )
            {
                Vec_IntClear( vTemp0 );
                Wlc_ObjForEachFanin( pObj, iFanin, k )
                    if ( k > 0 )
                    {
                        Wlc_Obj_t * pFanin = Wlc_NtkObj(p, iFanin);
                        assert( nRange == Wlc_ObjRange(pFanin) );
                        pFans1 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, iFanin) );
                        Vec_IntPush( vTemp0, pFans1[b] );
                    }
                Vec_IntPush( vRes, Wlc_NtkMuxTree2(pNew, NULL, 0, vTemp0, vTemp1, vTemp2) );
            }
        }
        else if ( pObj->Type == WLC_OBJ_SHIFT_R || pObj->Type == WLC_OBJ_SHIFT_RA ||
                  pObj->Type == WLC_OBJ_SHIFT_L || pObj->Type == WLC_OBJ_SHIFT_LA )
        {
            int nRangeMax = Abc_MaxInt( nRange, nRange0 );
            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin0(p, pObj) );
            if ( pObj->Type == WLC_OBJ_SHIFT_R || pObj->Type == WLC_OBJ_SHIFT_RA )
                Wlc_BlastShiftRight( pNew, pArg0, nRangeMax, pFans1, nRange1, Wlc_ObjIsSignedFanin0(p, pObj) && pObj->Type == WLC_OBJ_SHIFT_RA, vRes );
            else
                Wlc_BlastShiftLeft( pNew, pArg0, nRangeMax, pFans1, nRange1, 0, vRes );
            Vec_IntShrink( vRes, nRange );
        }
        else if ( pObj->Type == WLC_OBJ_ROTATE_R )
        {
            assert( nRange0 == nRange );
            Wlc_BlastRotateRight( pNew, pFans0, nRange0, pFans1, nRange1, vRes );
        }
        else if ( pObj->Type == WLC_OBJ_ROTATE_L )
        {
            assert( nRange0 == nRange );
            Wlc_BlastRotateLeft( pNew, pFans0, nRange0, pFans1, nRange1, vRes );
        }
        else if ( pObj->Type == WLC_OBJ_BIT_NOT )
        {
            int nRangeMax = Abc_MaxInt( nRange, nRange0 );
            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin0(p, pObj) );
            for ( k = 0; k < nRange; k++ )
                Vec_IntPush( vRes, Abc_LitNot(pArg0[k]) );
        }
        else if ( pObj->Type == WLC_OBJ_BIT_AND || pObj->Type == WLC_OBJ_BIT_NAND )
        {
            int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
            for ( k = 0; k < nRange; k++ )
                Vec_IntPush( vRes, Abc_LitNotCond(Gia_ManHashAnd(pNew, pArg0[k], pArg1[k]), pObj->Type == WLC_OBJ_BIT_NAND) );
        }
        else if ( pObj->Type == WLC_OBJ_BIT_OR || pObj->Type == WLC_OBJ_BIT_NOR )
        {
            int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
            for ( k = 0; k < nRange; k++ )
                Vec_IntPush( vRes, Abc_LitNotCond(Gia_ManHashOr(pNew, pArg0[k], pArg1[k]), pObj->Type == WLC_OBJ_BIT_NOR) );
        }
        else if ( pObj->Type == WLC_OBJ_BIT_XOR || pObj->Type == WLC_OBJ_BIT_NXOR )
        {
            int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
            for ( k = 0; k < nRange; k++ )
                Vec_IntPush( vRes, Abc_LitNotCond(Gia_ManHashXor(pNew, pArg0[k], pArg1[k]), pObj->Type == WLC_OBJ_BIT_NXOR) );
        }
        else if ( pObj->Type == WLC_OBJ_BIT_SELECT )
        {
            Wlc_Obj_t * pFanin = Wlc_ObjFanin0(p, pObj);
            int End = Wlc_ObjRangeEnd(pObj);
            int Beg = Wlc_ObjRangeBeg(pObj);
            if ( End >= Beg )
            {
                assert( nRange == End - Beg + 1 );
                assert( pFanin->Beg <= Beg && End <= pFanin->End );
                for ( k = Beg; k <= End; k++ )
                    Vec_IntPush( vRes, pFans0[k - pFanin->Beg] );
            }
            else
            {
                assert( nRange == Beg - End + 1 );
                assert( pFanin->End <= End && Beg <= pFanin->Beg );
                for ( k = End; k <= Beg; k++ )
                    Vec_IntPush( vRes, pFans0[k - pFanin->End] );
            }
        }
        else if ( pObj->Type == WLC_OBJ_BIT_CONCAT )
        {
            int iFanin, nTotal = 0;
            Wlc_ObjForEachFanin( pObj, iFanin, k )
                nTotal += Wlc_ObjRange( Wlc_NtkObj(p, iFanin) );
            assert( nRange == nTotal );
            Wlc_ObjForEachFaninReverse( pObj, iFanin, k )
            {
                nRange0 = Wlc_ObjRange( Wlc_NtkObj(p, iFanin) );
                pFans0 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, iFanin) );
                for ( b = 0; b < nRange0; b++ )
                    Vec_IntPush( vRes, pFans0[b] );
            }
        }
        else if ( pObj->Type == WLC_OBJ_BIT_ZEROPAD || pObj->Type == WLC_OBJ_BIT_SIGNEXT )
        {
            int Pad = pObj->Type == WLC_OBJ_BIT_ZEROPAD ? 0 : pFans0[nRange0-1];
            assert( nRange0 <= nRange );
            for ( k = 0; k < nRange0; k++ )
                Vec_IntPush( vRes, pFans0[k] );
            for (      ; k < nRange; k++ )
                Vec_IntPush( vRes, Pad );
        }
        else if ( pObj->Type == WLC_OBJ_LOGIC_NOT )
        {
            iLit = Wlc_BlastReduction( pNew, pFans0, nRange0, WLC_OBJ_REDUCT_OR );
            Vec_IntFill( vRes, 1, Abc_LitNot(iLit) );
            for ( k = 1; k < nRange; k++ )
                Vec_IntPush( vRes, 0 );
        }
        else if ( pObj->Type == WLC_OBJ_LOGIC_IMPL )
        {
            int iLit0 = Wlc_BlastReduction( pNew, pFans0, nRange0, WLC_OBJ_REDUCT_OR );
            int iLit1 = Wlc_BlastReduction( pNew, pFans1, nRange1, WLC_OBJ_REDUCT_OR );
            Vec_IntFill( vRes, 1, Gia_ManHashOr(pNew, Abc_LitNot(iLit0), iLit1) );
            for ( k = 1; k < nRange; k++ )
                Vec_IntPush( vRes, 0 );
        }
        else if ( pObj->Type == WLC_OBJ_LOGIC_AND )
        {
            int iLit0 = Wlc_BlastReduction( pNew, pFans0, nRange0, WLC_OBJ_REDUCT_OR );
            int iLit1 = Wlc_BlastReduction( pNew, pFans1, nRange1, WLC_OBJ_REDUCT_OR );
            Vec_IntFill( vRes, 1, Gia_ManHashAnd(pNew, iLit0, iLit1) );
            for ( k = 1; k < nRange; k++ )
                Vec_IntPush( vRes, 0 );
        }
        else if ( pObj->Type == WLC_OBJ_LOGIC_OR )
        {
            int iLit0 = Wlc_BlastReduction( pNew, pFans0, nRange0, WLC_OBJ_REDUCT_OR );
            int iLit1 = Wlc_BlastReduction( pNew, pFans1, nRange1, WLC_OBJ_REDUCT_OR );
            Vec_IntFill( vRes, 1, Gia_ManHashOr(pNew, iLit0, iLit1) );
            for ( k = 1; k < nRange; k++ )
                Vec_IntPush( vRes, 0 );
        }
        else if ( pObj->Type == WLC_OBJ_LOGIC_XOR )
        {
            int iLit0 = Wlc_BlastReduction( pNew, pFans0, nRange0, WLC_OBJ_REDUCT_OR );
            int iLit1 = Wlc_BlastReduction( pNew, pFans1, nRange1, WLC_OBJ_REDUCT_OR );
            Vec_IntFill( vRes, 1, Gia_ManHashXor(pNew, iLit0, iLit1) );
            for ( k = 1; k < nRange; k++ )
                Vec_IntPush( vRes, 0 );
        }
        else if ( pObj->Type == WLC_OBJ_COMP_NOTEQU && Wlc_ObjFaninNum(pObj) > 2 )
        {
            // find the max range
            int a, b, iRes = 1, nRangeMax = Abc_MaxInt( nRange0, nRange1 );
            for ( k = 2; k < Wlc_ObjFaninNum(pObj); k++ )
                nRangeMax = Abc_MaxInt( nRangeMax, Wlc_ObjRange( Wlc_NtkObj(p, Wlc_ObjFaninId(pObj, k)) ) );
            // create pairwise distinct
            for ( a = 0; a < Wlc_ObjFaninNum(pObj); a++ )
            for ( b = a+1; b < Wlc_ObjFaninNum(pObj); b++ )
            {
                int nRange0 = Wlc_ObjRange( Wlc_NtkObj(p, Wlc_ObjFaninId(pObj, a)) );
                int nRange1 = Wlc_ObjRange( Wlc_NtkObj(p, Wlc_ObjFaninId(pObj, b)) );
                int * pFans0 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId(pObj, a)) );
                int * pFans1 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId(pObj, b)) );
                int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, 0 );
                int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, 0 );
                int iLit = 0;
                for ( k = 0; k < nRangeMax; k++ )
                    iLit = Gia_ManHashOr( pNew, iLit, Gia_ManHashXor(pNew, pArg0[k], pArg1[k]) ); 
                iRes = Gia_ManHashAnd( pNew, iRes, iLit ); 
            }
            Vec_IntFill( vRes, 1, iRes );
            for ( k = 1; k < nRange; k++ )
                Vec_IntPush( vRes, 0 );
        }
        else if ( pObj->Type == WLC_OBJ_COMP_EQU || pObj->Type == WLC_OBJ_COMP_NOTEQU )
        {
            int iLit = 0, nRangeMax = Abc_MaxInt( nRange0, nRange1 );
            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
            for ( k = 0; k < nRangeMax; k++ )
                iLit = Gia_ManHashOr( pNew, iLit, Gia_ManHashXor(pNew, pArg0[k], pArg1[k]) ); 
            Vec_IntFill( vRes, 1, Abc_LitNotCond(iLit, pObj->Type == WLC_OBJ_COMP_EQU) );
            for ( k = 1; k < nRange; k++ )
                Vec_IntPush( vRes, 0 );
        }
        else if ( pObj->Type == WLC_OBJ_COMP_LESS || pObj->Type == WLC_OBJ_COMP_MOREEQU ||
                  pObj->Type == WLC_OBJ_COMP_MORE || pObj->Type == WLC_OBJ_COMP_LESSEQU )
        {
            int nRangeMax = Abc_MaxInt( nRange0, nRange1 );
            int fSigned = Wlc_ObjIsSignedFanin01(p, pObj);
            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, fSigned );
            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, fSigned );
            int fSwap  = (pObj->Type == WLC_OBJ_COMP_MORE    || pObj->Type == WLC_OBJ_COMP_LESSEQU);
            int fCompl = (pObj->Type == WLC_OBJ_COMP_MOREEQU || pObj->Type == WLC_OBJ_COMP_LESSEQU);
            if ( fSwap ) ABC_SWAP( int *, pArg0, pArg1 );
            if ( fSigned )
                iLit = pParIn->fBlastNew ? Wlc_BlastLessSigned3( pNew, pArg0, pArg1, nRangeMax ) :  Wlc_BlastLessSigned( pNew, pArg0, pArg1, nRangeMax );
            else
                iLit = pParIn->fBlastNew ? Wlc_BlastLess3( pNew, pArg0, pArg1, nRangeMax ) : Wlc_BlastLess( pNew, pArg0, pArg1, nRangeMax );
            iLit = Abc_LitNotCond( iLit, fCompl );
            Vec_IntFill( vRes, 1, iLit );
            for ( k = 1; k < nRange; k++ )
                Vec_IntPush( vRes, 0 );
        }
        else if ( pObj->Type == WLC_OBJ_REDUCT_AND  || pObj->Type == WLC_OBJ_REDUCT_OR  || pObj->Type == WLC_OBJ_REDUCT_XOR ||
                  pObj->Type == WLC_OBJ_REDUCT_NAND || pObj->Type == WLC_OBJ_REDUCT_NOR || pObj->Type == WLC_OBJ_REDUCT_NXOR )
        {
            Vec_IntPush( vRes, Wlc_BlastReduction( pNew, pFans0, nRange0, pObj->Type ) );
            for ( k = 1; k < nRange; k++ )
                Vec_IntPush( vRes, 0 );
        }
        else if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB ) 
        {
            int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
            int * pArg0 = Wlc_VecLoadFanins( vRes,   pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
            int CarryIn = Wlc_ObjFaninNum(pObj) == 3 ? pFans2[0] : 0;
            if ( pObj->Type == WLC_OBJ_ARI_ADD )
            {
                if ( pPar->fCla )
                    Wlc_BlastAdderCLA( pNew, pArg0, pArg1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj), CarryIn ); // result is in pFan0 (vRes)
                    //Wlc_BlastAdderFast( pNew, pArg0, pArg1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj), CarryIn ); // result is in pFan0 (vRes)
                else
                    Wlc_BlastAdder( pNew, pArg0, pArg1, nRangeMax, CarryIn ); // result is in pFan0 (vRes)
            }
            else 
                Wlc_BlastSubtract( pNew, pArg0, pArg1, nRange, 1 ); // result is in pFan0 (vRes)
            Vec_IntShrink( vRes, nRange );
        }
        else if ( pObj->Type == WLC_OBJ_ARI_ADDSUB ) 
        {
            int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange2, nRange3) );
            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans2, nRange2, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans2, nRange2, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
            int * pArg2 = Wlc_VecLoadFanins( vTemp2, pFans3, nRange3, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
            int ModeIn   = pFans0[0];
            int CarryIn  = pFans1[0]; int j;
            Wlc_BlastAdder   ( pNew, pArg0, pArg2, nRangeMax, CarryIn ); // result is in pArg0 (vTemp0)
            Wlc_BlastSubtract( pNew, pArg1, pArg2, nRangeMax, Abc_LitNot(CarryIn) ); // result is in pArg1 (vTemp1)
            Vec_IntClear( vRes );
            for ( j = 0; j < nRange; j++ )
                Vec_IntPush( vRes, Gia_ManHashMux(pNew, ModeIn, pArg0[j], pArg1[j]) ); 
        }
        else if ( pObj->Type == WLC_OBJ_ARI_MULTI )
        {
            if ( fUseOldMultiplierBlasting )
            {
                int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
                int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
                int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
                Wlc_BlastMultiplier2( pNew, pArg0, pArg1, nRange, vTemp2, vRes );
                Vec_IntShrink( vRes, nRange );
            }
            else
            {
                int fSigned = Wlc_ObjIsSignedFanin01(p, pObj);
                int nRangeMax = Abc_MaxInt(nRange0, nRange1);
                int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, fSigned );
                int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, fSigned );
                if ( nRange0 == nRange1 && Wlc_NtkCountConstBits(pArg0, nRangeMax) < Wlc_NtkCountConstBits(pArg1, nRangeMax) )
                    ABC_SWAP( int *, pArg0, pArg1 );
                if ( pPar->fBooth )
                    Wlc_BlastBooth( pNew, pArg0, pArg1, nRange0, nRange1, vRes, fSigned, pPar->fCla, NULL, pParIn->fVerbose );
                else if ( pPar->fCla )
                    Wlc_BlastMultiplier3( pNew, pArg0, pArg1, nRange0, nRange1, vRes, Wlc_ObjIsSignedFanin01(p, pObj), pPar->fCla, NULL, pParIn->fVerbose );
                else
                    Wlc_BlastMultiplier( pNew, pArg0, pArg1, nRangeMax, nRangeMax, vTemp2, vRes, fSigned );
                    //Wlc_BlastMultiplierC( pNew, pArg0, pArg1, nRangeMax, nRangeMax, vTemp2, vRes, fSigned );
                if ( nRange > Vec_IntSize(vRes) )
                    Vec_IntFillExtra( vRes, nRange, fSigned ? Vec_IntEntryLast(vRes) : 0 );
                else
                    Vec_IntShrink( vRes, nRange );
                assert( Vec_IntSize(vRes) == nRange );
            }
        }
        else if ( pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS )
        {
            int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
            int fSigned = Wlc_ObjIsSignedFanin01(p, pObj);
            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, fSigned );
            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, fSigned );
            if ( fSigned )
                Wlc_BlastDividerSigned( pNew, pArg0, nRangeMax, pArg1, nRangeMax, pObj->Type == WLC_OBJ_ARI_DIVIDE, vRes, pPar->fNonRest );
            else
                Wlc_BlastDividerTop( pNew, pArg0, nRangeMax, pArg1, nRangeMax, pObj->Type == WLC_OBJ_ARI_DIVIDE, vRes, pPar->fNonRest );
            Vec_IntShrink( vRes, nRange );
            if ( !pPar->fDivBy0 )
                Wlc_BlastZeroCondition( pNew, pFans1, nRange1, vRes );
        }
        else if ( pObj->Type == WLC_OBJ_ARI_MINUS )
        {
            int nRangeMax = Abc_MaxInt( nRange0, nRange );
            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin0(p, pObj) );
            Wlc_BlastMinus( pNew, pArg0, nRangeMax, vRes );
            Vec_IntShrink( vRes, nRange );
        }
        else if ( pObj->Type == WLC_OBJ_ARI_POWER )
        {
            int nRangeMax = Abc_MaxInt(nRange0, nRange);
            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin0(p, pObj) );
            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRange1, Wlc_ObjIsSignedFanin1(p, pObj) );
            Wlc_BlastPower( pNew, pArg0, nRangeMax, pArg1, nRange1, vTemp2, vRes );
            Vec_IntShrink( vRes, nRange );
        }
        else if ( pObj->Type == WLC_OBJ_ARI_SQRT )
        {
            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRange0 + (nRange0 & 1), 0 );
            nRange0 += (nRange0 & 1);
            if ( pPar->fNonRest )
                Wlc_BlastSqrtNR( pNew, pArg0, nRange0, vTemp2, vRes );
            else
                Wlc_BlastSqrt( pNew, pArg0, nRange0, vTemp2, vRes );
            if ( nRange > Vec_IntSize(vRes) )
                Vec_IntFillExtra( vRes, nRange, 0 );
            else
                Vec_IntShrink( vRes, nRange );
        }
        else if ( pObj->Type == WLC_OBJ_ARI_SQUARE )
        {
            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRange0, 0 );
            Wlc_BlastSquare( pNew, pArg0, nRange0, vTemp2, vRes );
            if ( nRange > Vec_IntSize(vRes) )
                Vec_IntFillExtra( vRes, nRange, 0 );
            else
                Vec_IntShrink( vRes, nRange );
        }
        else if ( pObj->Type == WLC_OBJ_DEC )
        {
            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRange0, 0 );
            if ( pParIn->fBlastNew )
                Wlc_BlastDecoder2( pNew, pArg0, nRange0, vTemp2, vRes );
            else
                Wlc_BlastDecoder( pNew, pArg0, nRange0, vTemp2, vRes );
            if ( nRange > Vec_IntSize(vRes) )
                Vec_IntFillExtra( vRes, nRange, 0 );
            else
                Vec_IntShrink( vRes, nRange );
        }
        else if ( pObj->Type == WLC_OBJ_TABLE )
            Wlc_BlastTable( pNew, Wlc_ObjTable(p, pObj), pFans0, nRange0, nRange, vRes );
        else if ( pObj->Type == WLC_OBJ_LUT && p->vLutTruths )
            Wlc_BlastLut( pNew, Vec_WrdEntry(p->vLutTruths, Wlc_ObjId(p, pObj)), pFans0, nRange0, nRange, vRes );
        else assert( 0 );
        assert( Vec_IntSize(vBits) == Wlc_ObjCopy(p, i) );
        Vec_IntAppend( vBits, vRes );
        if ( vAddOutputs && !Wlc_ObjIsCo(pObj) && 
            (
             (pObj->Type >= WLC_OBJ_MUX      && pObj->Type <= WLC_OBJ_ROTATE_L)     || 
             (pObj->Type >= WLC_OBJ_COMP_EQU && pObj->Type <= WLC_OBJ_COMP_MOREEQU) || 
             (pObj->Type >= WLC_OBJ_ARI_ADD  && pObj->Type <= WLC_OBJ_ARI_SQUARE)
            )
           )
        {
            Vec_IntAppend( vAddOutputs, vRes );
            Vec_IntPush( vAddObjs, Wlc_ObjId(p, pObj) );
        }
        p->nAnds[pObj->Type] += Gia_ManAndNum(pNew) - nAndPrev;
    }
    p->nAnds[0] = Gia_ManAndNum(pNew);
    assert( nBits == Vec_IntSize(vBits) );
    Vec_IntFree( vTemp0 );
    Vec_IntFree( vTemp1 );
    Vec_IntFree( vTemp2 );
    Vec_IntFree( vRes );
    // create flop boxes
    Wlc_NtkForEachFf2( p, pObj, i )
    {
        If_Box_t * pBox;
        char Buffer[100];
        float * pTable;
        Vec_Int_t * vTemp0 = Vec_IntAlloc( 100 );
        Vec_Int_t * vTemp1 = Vec_IntAlloc( 100 );
        int iLit, nRange = Wlc_ObjRange(pObj);
        int * pFans0, * pFans1, * pFans2, * pFans3;
        int iReset, iSet, iEnable;
        int nRangeIn = 2*nRange + 3; // D, reset, set, enable, Q
        int iSre = Wlc_ObjFaninId(pObj, 6);
 
        assert( pObj->Type == WLC_OBJ_FF );
 
        // create new box
        if ( vTables == NULL ) {
            Tim_ManSetDelayTables( pManTime, (vTables = Vec_PtrAlloc(100)) );
            Vec_PtrPush( vTables, NULL );
        }
        Tim_ManCreateBox( pManTime, curPo, nRangeIn, curPi, nRange, Vec_PtrSize(vTables), 0 );
        curPi += nRange;
        curPo += nRangeIn;
 
        // create delay table
        pTable = ABC_ALLOC( float, 3 + nRange * nRangeIn );
        pTable[0] = Vec_PtrSize(vTables);
        pTable[1] = nRangeIn;
        pTable[2] = nRange;
        for ( k = 0; k < nRange * nRangeIn; k++ )
            pTable[3 + k] = 1.0;
        Vec_PtrPush( vTables, pTable );
 
        // create combinational outputs in the normal manager
        pFans0  = Wlc_ObjFaninNum(pObj) > 0 ? Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId0(pObj)) ) : NULL;
        pFans1  = Wlc_ObjFaninNum(pObj) > 2 ? Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId(pObj,2)) ) : NULL; // reset
        pFans2  = Wlc_ObjFaninNum(pObj) > 3 ? Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId(pObj,3)) ) : NULL; // set
        pFans3  = Wlc_ObjFaninNum(pObj) > 4 ? Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId(pObj,4)) ) : NULL; // enable
        for ( k = 0; k < nRange; k++ )
            Gia_ManAppendCo( pNew, pFans0[k] );
        Gia_ManAppendCo( pNew, pFans1[0] );
        Gia_ManAppendCo( pNew, pFans2[0] );
        Gia_ManAppendCo( pNew, pFans3[0] );
        for ( k = 0; k < nRange; k++ )
            Gia_ManAppendCo( pNew, Gia_Obj2Lit(pNew, Gia_ManCi(pNew, Vec_IntEntry(vFf2Ci, i)+k)) );
 
        // make sure there is enough primary inputs in the manager
        for ( k = Gia_ManPiNum(pExtra); k < nRangeIn; k++ )
            Gia_ManAppendCi( pExtra );
        // create combinational inputs
        for ( k = 0; k < nRange; k++ )
            Vec_IntPush( vTemp0, Gia_Obj2Lit(pExtra, Gia_ManPi(pExtra, k)) );
        iReset  = Gia_Obj2Lit(pExtra, Gia_ManPi(pExtra, nRange+0));
        iSet    = Gia_Obj2Lit(pExtra, Gia_ManPi(pExtra, nRange+1));
        iEnable = Gia_Obj2Lit(pExtra, Gia_ManPi(pExtra, nRange+2));
        for ( k = 0; k < nRange; k++ )
            Vec_IntPush( vTemp1, Gia_Obj2Lit(pExtra, Gia_ManPi(pExtra, nRangeIn-nRange+k)) );
 
        // bit-blast in the external manager
        for ( k = 0; k < nRange; k++ )
        {
            // enable
            //iLitFlop = Gia_LitNotCond( Gia_ObjCopy(pObj), Gia_FlopIsOne(pObj) );
            //iLit = Gia_ManHashMux( Gia_ObjGia(pObj), Gia_FlopEnableCopy(pObj), iLit, iLitFlop );
            iLit = Gia_ManHashMux( pExtra, iEnable, Vec_IntEntry(vTemp0, k), Vec_IntEntry(vTemp1, k) );
            if ( iSre )
            {
                // reset
                //iLit = Gia_ManHashAnd( Gia_ObjGia(pObj), iLit, Gia_LitNot(Gia_FlopResetCopy(pObj)) );
                iLit = Gia_ManHashAnd( pExtra, iLit, Abc_LitNot(iReset) );
                // set
                //iLit = Gia_ManHashOr( Gia_ObjGia(pObj), iLit, Gia_FlopSetCopy(pObj) );
                iLit = Gia_ManHashOr( pExtra, iLit, iSet );
            }
            else
            {
                // set
                //iLit = Gia_ManHashOr( Gia_ObjGia(pObj), iLit, Gia_FlopSetCopy(pObj) );
                iLit = Gia_ManHashOr( pExtra, iLit, iSet );
                // reset
                //iLit = Gia_ManHashAnd( Gia_ObjGia(pObj), iLit, Gia_LitNot(Gia_FlopResetCopy(pObj)) );
                iLit = Gia_ManHashAnd( pExtra, iLit, Abc_LitNot(iReset) );
            }
            // create outputs in the external manager
            Gia_ManAppendCo( pExtra, iLit );
        }
 
        // add box to the library
        sprintf( Buffer, "%s%03d", "ff_comb", 1+If_LibBoxNum(pBoxLib) );
        pBox = If_BoxStart( Abc_UtilStrsav(Buffer), 1+If_LibBoxNum(pBoxLib), nRangeIn, nRange, 0, 0, 0 ); 
        If_LibBoxAdd( pBoxLib, pBox );
        for ( k = 0; k < pBox->nPis * pBox->nPos; k++ )
            pBox->pDelays[k] = 1;
        Vec_IntFree( vTemp0 );
        Vec_IntFree( vTemp1 );
    }
    Vec_IntFree( vFf2Ci );
    // create COs
    if ( pPar->fCreateMiter || pPar->fCreateWordMiter )
    {
        int nPairs = 0, nBits = 0;
        Vec_Int_t * vOuts = Vec_IntAlloc( 100 );
        assert( Wlc_NtkPoNum(p) % 2 == 0 );
        Wlc_NtkForEachCo( p, pObj, i )
        {
            if ( pObj->fIsFi )
            {
                nRange = Wlc_ObjRange( pObj );
                pFans0 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)) );
                if ( Wlc_ObjRangeIsReversed(pObj) )
                {
                    for ( k = 0; k < nRange; k++ )
                        Gia_ManAppendCo( pNew, pFans0[nRange-1-k] );
                }
                else
                {
                    for ( k = 0; k < nRange; k++ )
                        Gia_ManAppendCo( pNew, pFans0[k] );
                }
                nFFins += nRange;
                continue;
            }
            pObj2   = Wlc_NtkCo( p, ++i );
            nRange1 = Wlc_ObjRange( pObj );
            nRange2 = Wlc_ObjRange( pObj2 );
            assert( nRange1 == nRange2 );
            pFans1  = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)) );
            pFans2  = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj2)) );
            if ( pPar->fCreateWordMiter )
            {
                Vec_IntClear( vOuts );
                if ( Wlc_ObjRangeIsReversed(pObj) )
                {
                    for ( k = 0; k < nRange1; k++ )
                        Vec_IntPushTwo( vOuts, pFans1[nRange1-1-k], pFans2[nRange2-1-k] );
                }
                else
                {
                    for ( k = 0; k < nRange1; k++ )
                        Vec_IntPushTwo( vOuts, pFans1[k], pFans2[k] );
                }
                Gia_ManAppendCo( pNew, Gia_ManHashDualMiter(pNew, vOuts) );
            }
            else
            {
                if ( Wlc_ObjRangeIsReversed(pObj) )
                {
                    for ( k = 0; k < nRange1; k++ )
                    {
                        Gia_ManAppendCo( pNew, pFans1[nRange1-1-k] );
                        Gia_ManAppendCo( pNew, pFans2[nRange2-1-k] );
                    }
                }
                else
                {
                    for ( k = 0; k < nRange1; k++ )
                    {
                        Gia_ManAppendCo( pNew, pFans1[k] );
                        Gia_ManAppendCo( pNew, pFans2[k] );
                    }
                }
            }
            nPairs++;
            nBits += nRange1;
        }
        Vec_IntFree( vOuts );
        if ( pPar->fCreateWordMiter )
            printf( "Derived an ordinary miter with %d bit-level outputs, one for each pair of word-level outputs.\n", nPairs );
        else
            printf( "Derived a dual-output miter with %d pairs of bits belonging to %d pairs of word-level outputs.\n", nBits, nPairs );
    }
    else
    {
        Wlc_NtkForEachCo( p, pObj, i )
        {
            // skip all outputs except the given ones
            if ( pPar->iOutput >= 0 && (i < pPar->iOutput || i >= pPar->iOutput + pPar->nOutputRange) )
                continue;
            // create additional PO literals
            if ( vAddOutputs && pObj->fIsFi )
            {
                Vec_IntForEachEntry( vAddOutputs, iLit, k )
                    Gia_ManAppendCo( pNew, iLit );
                printf( "Created %d additional POs for %d interesting internal word-level variables.\n", Vec_IntSize(vAddOutputs), Vec_IntSize(vAddObjs) );
                Vec_IntFreeP( &vAddOutputs );
            }
            nRange = Wlc_ObjRange( pObj );
            pFans0 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)) );
            if ( fVerbose )
                printf( "%s(%d) ", Wlc_ObjName(p, Wlc_ObjId(p, pObj)), Gia_ManCoNum(pNew) );
            if ( Wlc_ObjRangeIsReversed(pObj) )
            {
                for ( k = 0; k < nRange; k++ )
                    Gia_ManAppendCo( pNew, pFans0[nRange-1-k] );
            }
            else
            {
                for ( k = 0; k < nRange; k++ )
                    Gia_ManAppendCo( pNew, pFans0[k] );
            }
            if ( pObj->fIsFi )
                nFFins += nRange;
        }
        if ( fVerbose )
            printf( "\n" );
    }
    //Vec_IntErase( vBits );
    //Vec_IntErase( &p->vCopies );
    // set the number of registers
    if ( Vec_IntSize(&p->vFfs2) > 0 )
    {
        assert( nFFins == 0 && nFFouts == 0 );
        // complement flop inputs whose init state is 1
        for ( i = 0; i < nFf2Regs; i++ )
            Gia_ManAppendCo( pNew, Gia_ManAppendCi(pNew) );
        Gia_ManSetRegNum( pNew, nFf2Regs );
    }
    else
    {
        assert( nFFins == nFFouts );
        Gia_ManSetRegNum( pNew, nFFins );
    }
    // finalize AIG
    if ( !pPar->fGiaSimple && !pPar->fNoCleanup )
    {
        pNew = Gia_ManCleanup( pTemp = pNew );
        Gia_ManDupRemapLiterals( vBits, pTemp );
        //printf( "Cutoff ID %d became %d.\n", 75, Abc_Lit2Var(Gia_ManObj(pTemp, 73)->Value) );
        Gia_ManStop( pTemp );
    }
    // transform AIG with init state
    if ( p->pInits )
    {
        if ( (int)strlen(p->pInits) != Gia_ManRegNum(pNew) )
        {
            printf( "The number of init values (%d) does not match the number of flops (%d).\n", (int)strlen(p->pInits), Gia_ManRegNum(pNew) );
            printf( "It is assumed that the AIG has constant 0 initial state.\n" );
        }
        else
        {
            pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, pPar->fSaveFfNames ? 1+Gia_ManRegNum(pNew) : 0, pPar->fGiaSimple, pPar->fVerbose );
            Gia_ManDupRemapLiterals( vBits, pTemp );
            Gia_ManStop( pTemp );
        }
    }
    // finalize AIG with boxes
    if ( Vec_IntSize(&p->vFfs2) > 0 )
    {
        curPo += nBitCos + nFf2Regs;
        assert( curPi == Tim_ManCiNum(pManTime) );
        assert( curPo == Tim_ManCoNum(pManTime) );
        // finalize the extra AIG
        pExtra = Gia_ManCleanup( pTemp = pExtra );
        Gia_ManStop( pTemp );
        assert( Gia_ManPoNum(pExtra) == Gia_ManCiNum(pNew) - nBitCis - nFf2Regs );
        // attach
        pNew->pAigExtra = pExtra;
        pNew->pManTime = pManTime;
        // normalize AIG
        pNew = Gia_ManDupNormalize( pTemp = pNew, 0 );
        Gia_ManTransferTiming( pNew, pTemp );
        Gia_ManStop( pTemp );
        //Tim_ManPrint( pManTime );
    }
    if ( pPar->vBoxIds )
    {
        curPo += nBitCos;
        assert( curPi == Tim_ManCiNum(pManTime) );
        assert( curPo == Tim_ManCoNum(pManTime) );
        // finalize the extra AIG
        pExtra = Gia_ManCleanup( pTemp = pExtra );
        Gia_ManStop( pTemp );
        assert( Gia_ManPoNum(pExtra) == Gia_ManCiNum(pNew) - nBitCis - nFf2Regs );
        // attach
        pNew->pAigExtra = pExtra;
        pNew->pManTime = pManTime;
        // normalize AIG
        pNew = Gia_ManDupNormalize( pTemp = pNew, 0 );
        Gia_ManTransferTiming( pNew, pTemp );
        Gia_ManStop( pTemp );
        //Tim_ManPrint( pManTime );
    }
    // create input names
    pNew->vNamesIn = Vec_PtrAlloc( Gia_ManCiNum(pNew) );
    Wlc_NtkForEachCi( p, pObj, i )
    if ( Wlc_ObjIsPi(pObj) )
    {
        char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
        nRange = Wlc_ObjRange( pObj );
        if ( fSkipBitRange && nRange == 1 )
            Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(pName) );
        else
            for ( k = 0; k < nRange; k++ )
            {
                char Buffer[1000];
                sprintf( Buffer, "%s[%d]", pName, pObj->Beg < pObj->End ? pObj->Beg+k : pObj->Beg-k );
                Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
                //printf( "Writing %s\n", Buffer );
            }
    }
    if ( p->pInits )
    {
        int Length = strlen(p->pInits);
        for ( i = 0; i < Length; i++ )
        if ( p->pInits[i] == 'x' || p->pInits[i] == 'X' )
        {
            char Buffer[100];
            sprintf( Buffer, "_%s_abc_%d_", "init", i );
            Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
            fAdded = 1;
        }
        if ( pPar->fSaveFfNames )
            for ( i = 0; i < 1+Length; i++ )
                Vec_PtrPush( pNew->vNamesIn, NULL );
    }
    Wlc_NtkForEachCi( p, pObj, i )
    if ( !Wlc_ObjIsPi(pObj) )
    {
        char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
        nRange = Wlc_ObjRange( pObj );
        if ( fSkipBitRange && nRange == 1 )
            Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(pName) );
        else
            for ( k = 0; k < nRange; k++ )
            {
                char Buffer[1000];
                sprintf( Buffer, "%s[%d]", pName, pObj->Beg < pObj->End ? pObj->Beg+k : pObj->Beg-k );
                Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
            }
    }
    Wlc_NtkForEachFf2( p, pObj, i )
    {
        char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
        nRange = Wlc_ObjRange( pObj );
        if ( fSkipBitRange && nRange == 1 )
        {
            char Buffer[1000];
            sprintf( Buffer, "%s_fo", pName );
            Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
        }
        else
            for ( k = 0; k < nRange; k++ )
            {
                char Buffer[1000];
                sprintf( Buffer, "%s_fo[%d]", pName, pObj->Beg < pObj->End ? pObj->Beg+k : pObj->Beg-k );
                Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
            }
    }
    Wlc_NtkForEachFf2( p, pObj, i )
    {
        char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
        nRange = Wlc_ObjRange( pObj );
        if ( fSkipBitRange && nRange == 1 )
            Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(pName) );
        else
            for ( k = 0; k < nRange; k++ )
            {
                char Buffer[1000];
                sprintf( Buffer, "%s[%d]", pName, pObj->Beg < pObj->End ? pObj->Beg+k : pObj->Beg-k );
                Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
            }
    }
    if ( p->pInits && pPar->fSaveFfNames )
    {
        char * pName;
        int Length    = (int)strlen(p->pInits);
        int NameStart = Vec_PtrSize(pNew->vNamesIn)-Length;
        int NullStart = Vec_PtrSize(pNew->vNamesIn)-2*Length;
        int SepStart  = Vec_PtrSize(pNew->vNamesIn)-2*Length-1;
        assert( Vec_PtrEntry(pNew->vNamesIn, SepStart) == NULL );
        Vec_PtrWriteEntry( pNew->vNamesIn, SepStart, Abc_UtilStrsav("_abc_190121_abc_") );
        for ( i = 0; i < Length; i++ )
        {
            char Buffer[100];
            sprintf( Buffer, "%c%s", p->pInits[i], (char *)Vec_PtrEntry(pNew->vNamesIn, NameStart+i) );
            assert( Vec_PtrEntry(pNew->vNamesIn, NullStart+i) == NULL );
            Vec_PtrWriteEntry( pNew->vNamesIn, NullStart+i, Abc_UtilStrsav(Buffer) );
        }
        Vec_PtrForEachEntry( char *, pNew->vNamesIn, pName, i )
            assert( pName != NULL );
    }
    if ( p->pInits && fAdded )
        Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav("abc_reset_flop") );
    if ( pPar->vBoxIds )
    {
        Wlc_NtkForEachObjVec( pPar->vBoxIds, p, pObj, i )
        {
            char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
            nRange = Wlc_ObjRange( pObj );
            assert( nRange > 1 );
            for ( k = 0; k < nRange; k++ )
            {
                char Buffer[1000];
                sprintf( Buffer, "%s[%d]", pName, pObj->Beg < pObj->End ? pObj->Beg+k : pObj->Beg-k );
                Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(Buffer) );
            }
        }
    }
    assert( Vec_PtrSize(pNew->vNamesIn) == Gia_ManCiNum(pNew) );
    // create output names
    pNew->vNamesOut = Vec_PtrAlloc( Gia_ManCoNum(pNew) );
    Wlc_NtkForEachFf2( p, pObj, i )
    {
        int iFanin;
        Wlc_ObjForEachFanin( pObj, iFanin, b )
        {
            char * pName = Wlc_ObjName(p, iFanin);
            nRange = Wlc_ObjRange( Wlc_NtkObj(p, iFanin) );
            if ( fSkipBitRange && nRange == 1 )
                Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) );
            else
                for ( k = 0; k < nRange; k++ )
                {
                    char Buffer[1000];
                    Wlc_Obj_t * pFanin = Wlc_NtkObj(p, iFanin);
                    sprintf( Buffer, "%s[%d]", pName, pFanin->Beg < pFanin->End ? pFanin->Beg+k : pFanin->Beg-k );
                    Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
                }
            if ( b == 3 )
                break;
        }
        {
            char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
            nRange = Wlc_ObjRange( pObj );
            if ( fSkipBitRange && nRange == 1 )
            {
                char Buffer[1000];
                sprintf( Buffer, "%s_in", pName );
                Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
            }
            else
                for ( k = 0; k < nRange; k++ )
                {
                    char Buffer[1000];
                    sprintf( Buffer, "%s_in[%d]", pName, pObj->Beg < pObj->End ? pObj->Beg+k : pObj->Beg-k );
                    Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
                }
        }
    }
    if ( pPar->vBoxIds )
    {
        Wlc_NtkForEachObjVec( pPar->vBoxIds, p, pObj, i )
        {
            int iFanin, f;
            Wlc_ObjForEachFanin( pObj, iFanin, f )
            {
                char * pName = Wlc_ObjName(p, iFanin);
                nRange = Wlc_ObjRange( Wlc_NtkObj(p, iFanin) );
                assert( nRange >= 1 );
                for ( k = 0; k < nRange; k++ )
                {
                    char Buffer[1000];
                    Wlc_Obj_t * pFanin = Wlc_NtkObj(p, iFanin);
                    sprintf( Buffer, "%s[%d]", pName, pFanin->Beg < pFanin->End ? pFanin->Beg+k : pFanin->Beg-k );
                    Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
                }
            }
        }
    }
    // add real primary outputs
    Wlc_NtkForEachCo( p, pObj, i )
    if ( Wlc_ObjIsPo(pObj) )
    {
        char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
        nRange = Wlc_ObjRange( pObj );
        if ( pPar->fCreateWordMiter )
        {
            Wlc_Obj_t * pObj2 = Wlc_NtkCo( p, ++i );
            char * pName2 = Wlc_ObjName(p, Wlc_ObjId(p, pObj2));
            char Buffer[1000];
            sprintf( Buffer, "%s_xor_%s", pName, pName2 );
            Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
            //printf( "Adding output %s\n", Buffer );
        }
        else if ( pPar->fCreateMiter && nRange > 1 )
        {
            Wlc_Obj_t * pObj2 = Wlc_NtkCo( p, ++i );
            char * pName2 = Wlc_ObjName(p, Wlc_ObjId(p, pObj2));
            int nRange1 = Wlc_ObjRange( pObj );
            assert( nRange == nRange1 );
            for ( k = 0; k < nRange; k++ )
            {
                char Buffer[1000];
                sprintf( Buffer, "%s[%d]", pName, pObj->Beg < pObj->End ? pObj->Beg+k : pObj->Beg-k );
                Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
                sprintf( Buffer, "%s[%d]", pName2, pObj->Beg < pObj->End ? pObj->Beg+k : pObj->Beg-k );
                Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
            }
        }
        else 
        {
            if ( fSkipBitRange && nRange == 1 )
                Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) );
            else
                for ( k = 0; k < nRange; k++ )
                {
                    char Buffer[1000];
                    sprintf( Buffer, "%s[%d]", pName, pObj->Beg < pObj->End ? pObj->Beg+k : pObj->Beg-k );
                    Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
                }
        }
    }
    if ( vAddObjs )
    {
        // add internal primary outputs
        Wlc_NtkForEachObjVec( vAddObjs, p, pObj, i )
        {
            char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
            nRange = Wlc_ObjRange( pObj );
            if ( fSkipBitRange && nRange == 1 )
                Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) );
            else
                for ( k = 0; k < nRange; k++ )
                {
                    char Buffer[1000];
                    sprintf( Buffer, "%s[%d]", pName, pObj->Beg < pObj->End ? pObj->Beg+k : pObj->Beg-k );
                    Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
                }
        }
        Vec_IntFreeP( &vAddObjs );
    }
    // add flop outputs
    if ( fAdded )
        Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav("abc_reset_flop_in") );
    Wlc_NtkForEachCo( p, pObj, i )
    if ( !Wlc_ObjIsPo(pObj) )
    {
        char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
        nRange = Wlc_ObjRange( pObj );
        if ( fSkipBitRange && nRange == 1 )
        {
            char Buffer[1000];
            sprintf( Buffer, "%s_fi", pName );
            Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
        }
        else
            for ( k = 0; k < nRange; k++ )
            {
                char Buffer[1000];
                sprintf( Buffer, "%s_fi[%d]", pName, pObj->Beg < pObj->End ? pObj->Beg+k : pObj->Beg-k );
                Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
            }
    }
    Wlc_NtkForEachFf2( p, pObj, i )
    {
        char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
        nRange = Wlc_ObjRange( pObj );
        if ( fSkipBitRange && nRange == 1 )
        {
            char Buffer[1000];
            sprintf( Buffer, "%s_fi", pName );
            Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
        }
        else
            for ( k = 0; k < nRange; k++ )
            {
                char Buffer[1000];
                sprintf( Buffer, "%s_fi[%d]", pName, pObj->Beg < pObj->End ? pObj->Beg+k : pObj->Beg-k );
                Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
            }
    }
    assert( Vec_PtrSize(pNew->vNamesOut) == Gia_ManCoNum(pNew) );
 
    // replace the current library
    if ( pBoxLib )
    {
        If_LibBoxFree( (If_LibBox_t *)Abc_FrameReadLibBox() );
        Abc_FrameSetLibBox( pBoxLib );
    }
 
    //pNew->pSpec = Abc_UtilStrsav( p->pSpec ? p->pSpec : p->pName );
    // dump the miter parts
    if ( 0 )
    {
        char pFileName0[1000], pFileName1[1000];
        char * pNameGeneric = Extra_FileNameGeneric( p->pSpec );
        Vec_Int_t * vOrder = Vec_IntStartNatural( Gia_ManPoNum(pNew) );
        Gia_Man_t * pGia0 = Gia_ManDupCones( pNew, Vec_IntArray(vOrder),                         Vec_IntSize(vOrder)/2, 0 );
        Gia_Man_t * pGia1 = Gia_ManDupCones( pNew, Vec_IntArray(vOrder) + Vec_IntSize(vOrder)/2, Vec_IntSize(vOrder)/2, 0 );
        assert( Gia_ManPoNum(pNew) % 2 == 0 );
        sprintf( pFileName0, "%s_lhs_.aig", pNameGeneric );
        sprintf( pFileName1, "%s_rhs_.aig", pNameGeneric );
        Gia_AigerWrite( pGia0, pFileName0, 0, 0, 0 );
        Gia_AigerWrite( pGia1, pFileName1, 0, 0, 0 );
        Gia_ManStop( pGia0 );
        Gia_ManStop( pGia1 );
        Vec_IntFree( vOrder );
        ABC_FREE( pNameGeneric );
        printf( "Dumped two parts of the miter into files \"%s\" and \"%s\".\n", pFileName0, pFileName1 );
    }
    //Wlc_NtkPrintNameArray( pNew->vNamesIn );
    //Wlc_NtkPrintNameArray( pNew->vNamesOut );
    if ( pPar->vBoxIds )
    {
        Vec_PtrFreeFree( pNew->vNamesIn );   pNew->vNamesIn  = NULL;
        Vec_PtrFreeFree( pNew->vNamesOut );  pNew->vNamesOut = NULL;
    }
    pNew->vRegClasses = vRegClasses;
    return pNew;
}

Here is the caller graph for this function:

Wlc_NtkCleanMarks()

void Wlc_NtkCleanMarks ( Wlc_Ntk_t * p )

extern

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

Synopsis [Select the cone of the given output.]

Description []

SideEffects []

SeeAlso []

Definition at line 1135 of file wlcNtk.c.

{
    Wlc_Obj_t * pObj;
    int i;
    Wlc_NtkForEachObj( p, pObj, i )
        pObj->Mark = 0;
}

Here is the caller graph for this function:

Wlc_NtkCollectAddMult()

Vec_Int_t * Wlc_NtkCollectAddMult ( Wlc_Ntk_t * p, Wlc_BstPar_t * pPar, int * pCountA, int * CountM )

extern

Definition at line 54 of file wlcUif.c.

{
    Vec_Int_t * vBoxIds;
    Wlc_Obj_t * pObj;  int i;
    *pCountA = *pCountM = 0;
    if ( pPar->nAdderLimit == 0 && pPar->nMultLimit == 0 )
        return NULL;
    vBoxIds = Vec_IntAlloc( 100 );
    Wlc_NtkForEachObj( p, pObj, i )
    {
        if ( pObj->Type == WLC_OBJ_ARI_ADD && pPar->nAdderLimit && Wlc_ObjRange(pObj) >= pPar->nAdderLimit )
            Vec_IntPush( vBoxIds, i ), (*pCountA)++;
        else if ( pObj->Type == WLC_OBJ_ARI_MULTI && pPar->nMultLimit && Wlc_ObjRange(pObj) >= pPar->nMultLimit )
            Vec_IntPush( vBoxIds, i ), (*pCountM)++;
    }
    if ( Vec_IntSize( vBoxIds ) > 0 )
    {
        Wlc_NtkCollectBoxes( p, vBoxIds );
        return vBoxIds;
    }
    Vec_IntFree( vBoxIds );
    return NULL;
}

Here is the call graph for this function:

Wlc_NtkCollectMemory()

Vec_Int_t * Wlc_NtkCollectMemory ( Wlc_Ntk_t * p, int fClean )

extern

Definition at line 216 of file wlcMem.c.

{
    Wlc_Obj_t * pObj; int i;
    Vec_Int_t * vMemSizes = Wlc_NtkCollectMemSizes( p );
    Vec_Int_t * vMemObjs = Vec_IntAlloc( 10 );
    Wlc_NtkForEachObj( p, pObj, i )
    {
        if ( Wlc_ObjType(pObj) == WLC_OBJ_WRITE || Wlc_ObjType(pObj) == WLC_OBJ_READ )
            Vec_IntPush( vMemObjs, i );
        else if ( Vec_IntFind(vMemSizes, Wlc_ObjRange(pObj)) >= 0 )
            Vec_IntPush( vMemObjs, i );
    }
    Vec_IntFree( vMemSizes );
    Vec_IntSort( vMemObjs, 0 );
    //Wlc_NtkPrintNodeArray( p, vMemObjs ); 
    if ( fClean )
    {
        Vec_Int_t * vTemp;
        vMemObjs = Wlc_NtkCleanObjects( p, vTemp = vMemObjs );
        Vec_IntFree( vTemp );
    }
    return vMemObjs;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_NtkCollectMultipliers()

Vec_Int_t * Wlc_NtkCollectMultipliers ( Wlc_Ntk_t * p )

extern

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

Synopsis [Collect IDs of the multipliers.]

Description []

SideEffects []

SeeAlso []

Definition at line 121 of file wlcUif.c.

{
    Wlc_Obj_t * pObj;  int i;
    Vec_Int_t * vBoxIds = Vec_IntAlloc( 100 );
    Wlc_NtkForEachObj( p, pObj, i )
        if ( pObj->Type == WLC_OBJ_ARI_MULTI )
            Vec_IntPush( vBoxIds, i );
    if ( Vec_IntSize( vBoxIds ) > 0 )
        return vBoxIds;
    Vec_IntFree( vBoxIds );
    return NULL;
}

Here is the caller graph for this function:

Wlc_NtkCountObjBits()

int Wlc_NtkCountObjBits ( Wlc_Ntk_t * p, Vec_Int_t * vPisNew )

extern

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

Synopsis [This procedure simply count the number of PPI bits.]

Description []

SideEffects []

SeeAlso []

Definition at line 1395 of file wlcNtk.c.

{
    Wlc_Obj_t * pObj; 
    int i, Count = 0;
    Wlc_NtkForEachObjVec( vPisNew, p, pObj, i )
        Count += Wlc_ObjRange(pObj);
    return Count;
}

Here is the caller graph for this function:

Wlc_NtkCountRealPis()

int Wlc_NtkCountRealPis ( Wlc_Ntk_t * p )

extern

Definition at line 445 of file wlcNtk.c.

{
    Wlc_Obj_t * pObj;
    int i, Count = 0;
    Wlc_NtkMarkCone( p, -1, -1, 1, 0 );
    Wlc_NtkForEachPi( p, pObj, i )
        Count += pObj->Mark;
    Wlc_NtkCleanMarks( p );
    return Count;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_NtkCreateLevels()

int Wlc_NtkCreateLevels ( Wlc_Ntk_t * p )

extern

Definition at line 372 of file wlcNtk.c.

{
    Wlc_Obj_t * pObj;  int i, LeveMax = 0;
    Vec_IntFill( &p->vLevels, Wlc_NtkObjNumMax(p), 0 );
    Wlc_NtkForEachObj( p, pObj, i )
        Wlc_NtkCreateLevels_rec( p, pObj );
    Wlc_NtkForEachObj( p, pObj, i )
        if ( !Wlc_ObjIsCi(pObj) && Wlc_ObjFaninNum(pObj) )
            Vec_IntAddToEntry( &p->vLevels, i, 1 );
    LeveMax = Vec_IntFindMax( &p->vLevels );
    Wlc_NtkForEachFf2( p, pObj, i )
        Vec_IntWriteEntry( &p->vLevels, Wlc_ObjId(p, pObj), LeveMax+1 );
    //Wlc_NtkPrintObjects( p ); 
    return LeveMax+1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_NtkCreateLevelsRev()

int Wlc_NtkCreateLevelsRev ( Wlc_Ntk_t * p )

extern

Definition at line 326 of file wlcNtk.c.

{
    Wlc_Obj_t * pObj; 
    int i, k, iFanin, Level, LevelMax = 0;
    Vec_IntFill( &p->vLevels, Wlc_NtkObjNumMax(p), 0 );
    Wlc_NtkForEachObjReverse( p, pObj, i )
    {
        if ( Wlc_ObjIsCi(pObj) )
            continue;
        Level = Wlc_ObjLevel(p, pObj) + 1;
        Wlc_ObjForEachFanin( pObj, iFanin, k )
            Vec_IntUpdateEntry( &p->vLevels, iFanin, Level );
        LevelMax = Abc_MaxInt( LevelMax, Level );
    }
    // reverse the values
    Wlc_NtkForEachObj( p, pObj, i )
        Vec_IntWriteEntry( &p->vLevels, i, LevelMax - Wlc_ObjLevelId(p, i) );
    Wlc_NtkForEachCi( p, pObj, i )
        Vec_IntWriteEntry( &p->vLevels, Wlc_ObjId(p, pObj), 0 );
    //Wlc_NtkForEachObj( p, pObj, i )
    //    printf( "%d -> %d\n", i, Wlc_ObjLevelId(p, i) );
    return LevelMax;
}

Wlc_NtkDcFlopNum()

int Wlc_NtkDcFlopNum ( Wlc_Ntk_t * p )

extern

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

Synopsis [Count the number of flops initialized to DC value.]

Description []

SideEffects []

SeeAlso []

Definition at line 1351 of file wlcNtk.c.

{
    int i, nFlops, Count = 0;
    if ( p->pInits == NULL )
        return 0;
    nFlops = strlen(p->pInits);
    for ( i = 0; i < nFlops; i++ )
        Count += (p->pInits[i] == 'x' || p->pInits[i] == 'X');
    return Count;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_NtkDeleteSim()

void Wlc_NtkDeleteSim ( Vec_Ptr_t * p )

extern

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

Synopsis [Performs simulation of a word-level network.]

Description [Returns vRes, a 2D array of simulation information for the output of each bit of each object listed in vNodes. In particular, Vec_Ptr_t * vSimObj = (Vec_Ptr_t *)Vec_PtrEntry(vRes, iObj) and Vec_Ptr_t * vSimObjBit = (Vec_Ptr_t *)Vec_PtrEntry(vSimObj, iBit) are arrays containing the simulation info for each object (vSimObj) and for each output bit of this object (vSimObjBit). Alternatively, Vec_Ptr_t * vSimObjBit = Vec_VecEntryEntry( (Vec_Vec_t *)vRes, iObj, iBit ). The output bitwidth of an object is Wlc_ObjRange( Wlc_NtkObj(pNtk, iObj) ). Simulation information is binary data constaining the given number (nWords) of 64-bit machine words for the given number (nFrames) of consecutive timeframes. The total number of timeframes is nWords * nFrames for each bit of each object.]

SideEffects []

SeeAlso []

Definition at line 120 of file wlcSim.c.

{
    word * pInfo; int i, k;
    Vec_Vec_t * vVec = (Vec_Vec_t *)p;
    Vec_VecForEachEntry( word *, vVec, pInfo, i, k )
        ABC_FREE( pInfo );
    Vec_VecFree( vVec );
}

Here is the caller graph for this function:

Wlc_NtkDupDfs()

Wlc_Ntk_t * Wlc_NtkDupDfs ( Wlc_Ntk_t * p, int fMarked, int fSeq )

extern

Definition at line 986 of file wlcNtk.c.

{
    Wlc_Ntk_t * pNew;
    Wlc_Obj_t * pObj, * pObjNew;
    Vec_Int_t * vFanins;
    int i, k, iObj, iFanin;
    vFanins = Vec_IntAlloc( 100 );
    Wlc_NtkCleanCopy( p );
    pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
    pNew->fSmtLib = p->fSmtLib;
    pNew->fAsyncRst = p->fAsyncRst;
    pNew->fMemPorts = p->fMemPorts;
    pNew->fEasyFfs = p->fEasyFfs;
    Wlc_NtkForEachCi( p, pObj, i )
        if ( !fMarked || pObj->Mark )
        {
            unsigned Type = pObj->Type;
            if ( !fSeq ) pObj->Type = WLC_OBJ_PI;
            Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
            pObj->Type = Type;
        }
    Wlc_NtkForEachFf2( p, pObj, i )
    {
        int iObjNew = Wlc_ObjAlloc( pNew, pObj->Type, Wlc_ObjIsSigned(pObj), pObj->End, pObj->Beg );
        Wlc_ObjSetCopy( p, Wlc_ObjId(p, pObj), iObjNew );
        Vec_IntPush( &pNew->vFfs2, iObjNew );
    }
    Wlc_NtkForEachCo( p, pObj, i )
        if ( !fMarked || pObj->Mark )
            Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins );
    Wlc_NtkForEachCo( p, pObj, i )
        if ( !fMarked || pObj->Mark )
            Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), fSeq ? pObj->fIsFi : 0 );
    Wlc_NtkForEachFf2( p, pObj, i )
    {
        iObj = Wlc_ObjId(p, pObj);
        Wlc_ObjForEachFanin( pObj, iFanin, k )
            Wlc_NtkDupDfs_rec( pNew, p, iFanin, vFanins );
        Wlc_ObjCollectCopyFanins( p, iObj, vFanins );
        pObjNew = Wlc_NtkObj( pNew, Wlc_ObjCopy(p, iObj) );
        Wlc_ObjAddFanins( pNew, pObjNew, vFanins );
        pObjNew->fXConst = pObj->fXConst;
    }
    Vec_IntFree( vFanins );
    if ( fSeq && p->vInits )
    {
        if ( fMarked )
        {
            if ( p->vInits )
                pNew->vInits = Wlc_ReduceMarkedInitVec( p, p->vInits );
            if ( p->pInits )
                pNew->pInits = Wlc_ReduceMarkedInitStr( p, p->pInits );
        }
        else
        {
            if ( p->vInits )
                pNew->vInits = Vec_IntDup( p->vInits );
            if ( p->pInits )
                pNew->pInits = Abc_UtilStrsav( p->pInits );
        }
    }
    if ( p->pSpec )
        pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    if ( Wlc_NtkHasNameId(p) )
        Wlc_NtkTransferNames( pNew, p );
    if ( Vec_IntSize(&p->vPoPairs) )
        Vec_IntAppend( &pNew->vPoPairs, &p->vPoPairs );
    return pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_NtkDupDfsAbs()

Wlc_Ntk_t * Wlc_NtkDupDfsAbs ( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )

extern

Definition at line 1055 of file wlcNtk.c.

{
    Wlc_Ntk_t * pNew;
    Wlc_Obj_t * pObj;
    Vec_Int_t * vFanins;
    int i;
    Wlc_NtkCleanCopy( p );
    pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
    pNew->fSmtLib = p->fSmtLib;
    pNew->fAsyncRst = p->fAsyncRst;
    pNew->fMemPorts = p->fMemPorts;
    pNew->fEasyFfs = p->fEasyFfs;
 
    // duplicate marked PIs
    vFanins = Vec_IntAlloc( 100 );
    Wlc_NtkForEachObjVec( vPisOld, p, pObj, i )
    {
        assert( Wlc_ObjIsPi(pObj) );
        Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
    }
    // duplicate additional PIs
    Wlc_NtkForEachObjVec( vPisNew, p, pObj, i )
    {
        unsigned Type = pObj->Type;
        int nFanins = Wlc_ObjFaninNum(pObj);
        assert( !Wlc_ObjIsPi(pObj) );
        pObj->Type = WLC_OBJ_PI;
        pObj->nFanins = 0;
        Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
        pObj->Type = Type;
        pObj->nFanins = (unsigned)nFanins;
    }
    // duplicate flop outputs
    Wlc_NtkForEachObjVec( vFlops, p, pObj, i )
    {
        assert( !Wlc_ObjIsPi(pObj) && Wlc_ObjIsCi(pObj) );
        Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
    }
 
    // duplicate logic cones of primary outputs
    Wlc_NtkForEachPo( p, pObj, i )
        Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins );
    // duplidate logic cone of flop inputs
    Wlc_NtkForEachObjVec( vFlops, p, pObj, i )
        Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, Wlc_ObjFo2Fi(p, pObj)), vFanins );
 
    // duplicate POs
    Wlc_NtkForEachPo( p, pObj, i )
        Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), 0 );
    // duplicate flop inputs 
    Wlc_NtkForEachObjVec( vFlops, p, pObj, i )
        Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, Wlc_ObjFo2Fi(p, pObj)), 1 );
    Vec_IntFree( vFanins );
 
    // mark flop outputs
    Wlc_NtkForEachObjVec( vFlops, p, pObj, i )
        pObj->Mark = 1;
    if ( p->vInits )
        pNew->vInits = Wlc_ReduceMarkedInitVec( p, p->vInits );
    if ( p->pInits )
        pNew->pInits = Wlc_ReduceMarkedInitStr( p, p->pInits );
    Wlc_NtkCleanMarks( p );
 
    if ( p->pSpec )
        pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    //Wlc_NtkTransferNames( pNew, p );
    return pNew;
}

Here is the call graph for this function:

Wlc_NtkDupDfsSimple()

Wlc_Ntk_t * Wlc_NtkDupDfsSimple ( Wlc_Ntk_t * p )

extern

Definition at line 957 of file wlcNtk.c.

{
    Wlc_Ntk_t * pNew;
    Wlc_Obj_t * pObj;
    Vec_Int_t * vFanins;
    int i;
    Wlc_NtkCleanCopy( p );
    vFanins = Vec_IntAlloc( 100 );
    pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
    pNew->fSmtLib = p->fSmtLib;
    pNew->fAsyncRst = p->fAsyncRst;
    pNew->fMemPorts = p->fMemPorts;
    pNew->fEasyFfs = p->fEasyFfs;
    Wlc_NtkForEachCi( p, pObj, i )
        Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
    Wlc_NtkForEachCo( p, pObj, i )
        Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins );
    Wlc_NtkForEachCo( p, pObj, i )
        Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
    if ( p->vInits )
    pNew->vInits = Vec_IntDup( p->vInits );
    if ( p->pInits )
    pNew->pInits = Abc_UtilStrsav( p->pInits );
    Vec_IntFree( vFanins );
    if ( p->pSpec )
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    return pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_NtkDupSingleNodes()

Wlc_Ntk_t * Wlc_NtkDupSingleNodes ( Wlc_Ntk_t * p )

extern

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

Synopsis [Duplicates the network by copying each node.]

Description []

SideEffects []

SeeAlso []

Definition at line 1232 of file wlcNtk.c.

{
    Wlc_Ntk_t * pNew;
    Vec_Int_t * vFanins;
    Wlc_Obj_t * pObj, * pObjNew;
    Wlc_Obj_t * pFanin, * pFaninNew;
    int i, k, iFanin, iFaninNew, iObjNew, Count = 0;
    // count objects
    Wlc_NtkForEachObj( p, pObj, i )
        if ( !Wlc_ObjIsCi(pObj) )
            Count += 1 + Wlc_ObjFaninNum(pObj);
    // copy objects
    Wlc_NtkCleanCopy( p );
    vFanins = Vec_IntAlloc( 100 );
    pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
    pNew->fSmtLib = p->fSmtLib;
    pNew->fAsyncRst = p->fAsyncRst;
    pNew->fMemPorts = p->fMemPorts;
    pNew->fEasyFfs = p->fEasyFfs;
    Wlc_NtkForEachObj( p, pObj, i )
    {
        if ( Wlc_ObjIsCi(pObj) )
            continue;
        if ( pObj->Type == WLC_OBJ_ARI_MULTI )
            continue;
        if ( pObj->Type == WLC_OBJ_MUX && Wlc_ObjFaninNum(pObj) > 3 )
            continue;
        // create CIs for the fanins
        Wlc_ObjForEachFanin( pObj, iFanin, k )
        {
            pFanin = Wlc_NtkObj(p, iFanin);
            iFaninNew = Wlc_ObjAlloc( pNew, WLC_OBJ_PI, pFanin->Signed, pFanin->End, pFanin->Beg );
            pFaninNew = Wlc_NtkObj(pNew, iFaninNew);
            Wlc_ObjSetCopy( p, iFanin, iFaninNew );
            //Wlc_ObjSetCi( pNew, pFaninNew );
        }
        // create object
        iObjNew = Wlc_ObjDup( pNew, p, i, vFanins );
        pObjNew = Wlc_NtkObj(pNew, iObjNew);
        pObjNew->fIsPo = 1;
        Vec_IntPush( &pNew->vPos, iObjNew );
    }
    Vec_IntFree( vFanins );
    Wlc_NtkTransferNames( pNew, p );
    if ( p->pSpec )
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    return pNew;
}

Here is the call graph for this function:

Wlc_NtkFindUifableMultiplierPairs()

Vec_Int_t * Wlc_NtkFindUifableMultiplierPairs ( Wlc_Ntk_t * p )

extern

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

Synopsis [Returns all pairs of uifable multipliers.]

Description []

SideEffects []

SeeAlso []

Definition at line 145 of file wlcUif.c.

{
    Vec_Int_t * vMultis = Wlc_NtkCollectMultipliers( p );
    Vec_Int_t * vPairs = Vec_IntAlloc( 2 );
    Wlc_Obj_t * pObj, * pObj2;  int i, k;
    // iterate through unique pairs
    Wlc_NtkForEachObjVec( vMultis, p, pObj, i )
        Wlc_NtkForEachObjVec( vMultis, p, pObj2, k )
        {
            if ( k == i )  
                break;
            if ( Wlc_NtkPairIsUifable( p, pObj, pObj2 ) )
            {
                Vec_IntPush( vPairs, Wlc_ObjId(p, pObj) );
                Vec_IntPush( vPairs, Wlc_ObjId(p, pObj2) );
            }
        }
    Vec_IntFree( vMultis );
    if ( Vec_IntSize( vPairs ) > 0 )
        return vPairs;
    Vec_IntFree( vPairs );
    return NULL;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_NtkFree()

void Wlc_NtkFree ( Wlc_Ntk_t * p )

extern

Definition at line 253 of file wlcNtk.c.

{
    if ( p->pManName )
        Abc_NamStop( p->pManName );
    if ( p->pMemFanin )
        Mem_FlexStop( p->pMemFanin, 0 );
    if ( p->pMemTable )
        Mem_FlexStop( p->pMemTable, 0 );
    ABC_FREE( p->vPoPairs.pArray );
    Vec_PtrFreeP( &p->vTables );
    Vec_WrdFreeP( &p->vLutTruths );
    ABC_FREE( p->vPis.pArray );
    ABC_FREE( p->vPos.pArray );
    ABC_FREE( p->vCis.pArray );
    ABC_FREE( p->vCos.pArray );
    ABC_FREE( p->vFfs.pArray );
    ABC_FREE( p->vFfs2.pArray );
    Vec_IntFreeP( &p->vInits );
    Vec_IntFreeP( &p->vArsts );
    ABC_FREE( p->vTravIds.pArray );
    ABC_FREE( p->vNameIds.pArray );
    ABC_FREE( p->vValues.pArray );
    ABC_FREE( p->vCopies.pArray );
    ABC_FREE( p->vBits.pArray );
    ABC_FREE( p->vLevels.pArray );
    ABC_FREE( p->vRefs.pArray );
    ABC_FREE( p->pInits );
    ABC_FREE( p->pObjs );
    ABC_FREE( p->pName );
    ABC_FREE( p->pSpec );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_NtkFromNdr()

Wlc_Ntk_t * Wlc_NtkFromNdr ( void * pData )

extern

Definition at line 366 of file wlcNdr.c.

{
    Ndr_Data_t * p = (Ndr_Data_t *)pData;  
    Wlc_Obj_t * pObj; Vec_Int_t * vName2Obj, * vFanins = Vec_IntAlloc( 100 );
    int Mod = 2, i, k, Obj, * pArray, fFound, NameId, NameIdMax;
    unsigned char nDigits;
    Vec_Wrd_t * vTruths = NULL; int nTruths[2] = {0};
    Wlc_Ntk_t * pTemp, * pNtk = Wlc_NtkAlloc( "top", Ndr_DataObjNum(p, Mod)+1 );
    Wlc_NtkCheckIntegrity( pData );
    Vec_IntClear( &pNtk->vFfs );
    //pNtk->pSpec = Abc_UtilStrsav( pFileName );
    // construct network and save name IDs
    Wlc_NtkCleanNameId( pNtk );
    Ndr_ModForEachPi( p, Mod, Obj )
    {
        int End, Beg, Signed = Ndr_ObjReadRange(p, Obj, &End, &Beg);
        int iObj = Wlc_ObjAlloc( pNtk, WLC_OBJ_PI, Signed, End, Beg );
        int NameId = Ndr_ObjReadBody( p, Obj, NDR_OUTPUT );
        Wlc_ObjSetNameId( pNtk, iObj, NameId );
    }
    Ndr_ModForEachNode( p, Mod, Obj )
    {
        int End, Beg, Signed = Ndr_ObjReadRange(p, Obj, &End, &Beg);
        int Type    = Ndr_ObjReadBody( p, Obj, NDR_OPERTYPE );
        int nArray  = Ndr_ObjReadArray( p, Obj, NDR_INPUT, &pArray );
        Vec_Int_t F = {nArray, nArray, pArray}, * vTemp = &F;
        int iObj    = Wlc_ObjAlloc( pNtk, Ndr_TypeNdr2Wlc(Type), Signed, End, Beg );
        int NameId  = Ndr_ObjReadBody( p, Obj, NDR_OUTPUT );
        Vec_IntClear( vFanins );
        Vec_IntAppend( vFanins, vTemp );
        if ( Type == ABC_OPER_DFF )
        {
            // save init state
            if ( pNtk->vInits == NULL )
                pNtk->vInits = Vec_IntAlloc( 100 );
            if ( Vec_IntSize(vFanins) == 2 )
                Vec_IntPush( pNtk->vInits, Vec_IntPop(vFanins) );
            else // assume const0 if init is not given
                Vec_IntPush( pNtk->vInits, -(End-Beg+1) );
            // save flop output
            pObj = Wlc_NtkObj(pNtk, iObj);
            assert( Wlc_ObjType(pObj) == WLC_OBJ_FO );
            Wlc_ObjSetNameId( pNtk, iObj, NameId );
            Vec_IntPush( &pNtk->vFfs, NameId );
            // save flop input
            assert( Vec_IntSize(vFanins) == 1 );
            Vec_IntPush( &pNtk->vFfs, Vec_IntEntry(vFanins, 0) );
            continue;
        }
        if ( Type == ABC_OPER_DFFRSE )
            Vec_IntPush( &pNtk->vFfs2, iObj );
        if ( Type == ABC_OPER_LUT )
        {
            word * pTruth;
            if ( vTruths == NULL )
                vTruths = Vec_WrdStart( 1000 );
            if ( NameId >= Vec_WrdSize(vTruths) )
                Vec_WrdFillExtra( vTruths, 2*NameId, 0 );
            pTruth = (word *)Ndr_ObjReadBodyP(p, Obj, NDR_FUNCTION);
            Vec_WrdWriteEntry( vTruths, NameId, pTruth ? *pTruth : 0 );
            nTruths[ pTruth != NULL ]++;
        }
        if ( Type == ABC_OPER_SLICE )
            Vec_IntPushTwo( vFanins, End, Beg );
        else if ( Type == ABC_OPER_CONST )
            Ndr_ObjReadConstant( vFanins, (char *)Ndr_ObjReadBodyP(p, Obj, NDR_FUNCTION) );
        else if ( Type == ABC_OPER_BIT_MUX && Vec_IntSize(vFanins) == 3 )
            ABC_SWAP( int, Vec_IntEntryP(vFanins, 1)[0], Vec_IntEntryP(vFanins, 2)[0] );
        Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins );
        Wlc_ObjSetNameId( pNtk, iObj, NameId );
        if ( Type == ABC_OPER_ARI_SMUL )
        {
            pObj = Wlc_NtkObj(pNtk, iObj);
            assert( Wlc_ObjFaninNum(pObj) == 2 );
            Wlc_ObjFanin0(pNtk, pObj)->Signed = 1;
            Wlc_ObjFanin1(pNtk, pObj)->Signed = 1;
        }
    }
    if ( nTruths[0] )
        printf( "Warning! The number of LUTs without function is %d (out of %d).\n", nTruths[0], nTruths[0]+nTruths[1] );
    // mark primary outputs
    Ndr_ModForEachPo( p, Mod, Obj )
    {
        int End, Beg, Signed = Ndr_ObjReadRange(p, Obj, &End, &Beg);
        int nArray  = Ndr_ObjReadArray( p, Obj, NDR_INPUT, &pArray );
        int iObj    = Wlc_ObjAlloc( pNtk, WLC_OBJ_BUF, Signed, End, Beg );
        int NameId  = Ndr_ObjReadBody( p, Obj, NDR_OUTPUT );
        assert( nArray == 1 && NameId == -1 );
        pObj = Wlc_NtkObj( pNtk, iObj );
        Vec_IntFill( vFanins, 1, pArray[0] );
        Wlc_ObjAddFanins( pNtk, pObj, vFanins );
        Wlc_ObjSetCo( pNtk, pObj, 0 );
    }
    Vec_IntFree( vFanins );
    // map name IDs into object IDs
    vName2Obj = Vec_IntInvert( &pNtk->vNameIds, 0 );
    Wlc_NtkForEachObj( pNtk, pObj, i )
    {
        int * pFanins = Wlc_ObjFanins(pObj);
        for ( k = 0; k < Wlc_ObjFaninNum(pObj); k++ )
            pFanins[k] = Vec_IntEntry(vName2Obj, pFanins[k]);
    }
    if ( pNtk->vInits )
    {
        Vec_IntForEachEntry( &pNtk->vFfs, NameId, i )
            Vec_IntWriteEntry( &pNtk->vFfs, i, Vec_IntEntry(vName2Obj, NameId) );
        Vec_IntForEachEntry( pNtk->vInits, NameId, i )
            if ( NameId > 0 )
                Vec_IntWriteEntry( pNtk->vInits, i, Vec_IntEntry(vName2Obj, NameId) );
        // move FO/FI to be part of CI/CO
        assert( (Vec_IntSize(&pNtk->vFfs) & 1) == 0 );
        assert( Vec_IntSize(&pNtk->vFfs) == 2 * Vec_IntSize(pNtk->vInits) );
        Wlc_NtkForEachFf( pNtk, pObj, i )
            if ( i & 1 )
                Wlc_ObjSetCo( pNtk, pObj, 1 );
            //else
            //    Wlc_ObjSetCi( pNtk, pObj );
        Vec_IntClear( &pNtk->vFfs );
        // convert init values into binary string
        //Vec_IntPrint( &p->pNtk->vInits );
        pNtk->pInits = Wlc_PrsConvertInitValues( pNtk );
        //printf( "%s", p->pNtk->pInits );
    }
    Vec_IntFree(vName2Obj);
    // create fake object names
    NameIdMax = Vec_IntFindMax(&pNtk->vNameIds);
    nDigits = (unsigned char)Abc_Base10Log( NameIdMax+1 );
    pNtk->pManName = Abc_NamStart( NameIdMax+1, 10 );
    for ( i = 1; i <= NameIdMax; i++ )
    {
        char pName[1000]; sprintf( pName, "s%0*d", nDigits, i );
        NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound );
        assert( !fFound && i == NameId );
    }
    //Ndr_NtkPrintNodes( pNtk );
    //Wlc_WriteVer( pNtk, "temp_ndr.v", 0, 0 );
    // derive topological order
    pNtk = Wlc_NtkDupDfs( pTemp = pNtk, 0, 1 );
    Wlc_NtkFree( pTemp );
    // copy truth tables
    if ( vTruths )
    {
        pNtk->vLutTruths = Vec_WrdStart( Wlc_NtkObjNumMax(pNtk) );
        Wlc_NtkForEachObj( pNtk, pObj, i )
        {
            int iObj   = Wlc_ObjId(pNtk, pObj);
            int NameId = Wlc_ObjNameId(pNtk, iObj);
            word Truth;
            if ( pObj->Type != WLC_OBJ_LUT || NameId == 0 )
                continue;
            Truth = Vec_WrdEntry(vTruths, NameId);
            assert( sizeof(void *) == 8 || Wlc_ObjFaninNum(pObj) < 6 );
            Vec_WrdWriteEntry( pNtk->vLutTruths, iObj, Truth );
        }
        Vec_WrdFreeP( &vTruths );
    }
    //Ndr_NtkPrintNodes( pNtk );
    pNtk->fMemPorts = 1;          // the network contains memory ports
    pNtk->fEasyFfs = 1;           // the network contains simple flops
    return pNtk;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_NtkMarkCone()

void Wlc_NtkMarkCone ( Wlc_Ntk_t * p, int iCoId, int Range, int fSeq, int fAllPis )

extern

Definition at line 1181 of file wlcNtk.c.

{
    Vec_Int_t * vFlops;
    Wlc_Obj_t * pObj;
    int i, CiId, CoId;
    Wlc_NtkCleanMarks( p );
    if ( fAllPis )
    Wlc_NtkForEachPi( p, pObj, i )
        pObj->Mark = 1;
    vFlops = Vec_IntAlloc( 100 );
    Wlc_NtkForEachCo( p, pObj, i )
        if ( iCoId == -1 || (i >= iCoId && i < iCoId + Range) )
            Wlc_NtkMarkCone_rec( p, pObj, vFlops );
    if ( fSeq )
    Vec_IntForEachEntry( vFlops, CiId, i )
    {
        CoId = Wlc_NtkPoNum(p) + CiId - Wlc_NtkPiNum(p);
        Wlc_NtkMarkCone_rec( p, Wlc_NtkCo(p, CoId), vFlops );
    }
    Vec_IntFree( vFlops );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_NtkMemAbstract()

int Wlc_NtkMemAbstract ( Wlc_Ntk_t * p, int nIterMax, int fDumpAbs, int fPdrVerbose, int fVerbose )

extern

Definition at line 986 of file wlcMem.c.

{
    abctime clk = Abc_Clock();
    Wlc_Ntk_t * pNewFull, * pNew; Aig_Man_t * pAig, * pTempAig;
    Gia_Man_t * pAbsFull, * pAbs;
    Abc_Cex_t * pCex = NULL;  Vec_Wrd_t * vValues = NULL; 
    Vec_Wec_t * vRefines = Vec_WecAlloc( 100 );
    Vec_Int_t * vNodeFrames = Vec_IntAlloc( 100 );
    Vec_Int_t * vMemObjs, * vMemFanins, * vFirstTotal, * vRefine; 
    int RetValue = -1, iFirstMemPi, iFirstCi, iFirstMemCi, nDcBits, nIters;
 
    vMemObjs    = Wlc_NtkCollectMemory( p, 0 );
    vMemFanins  = Wlc_NtkCollectMemFanins( p, vMemObjs );
    pNewFull    = Wlc_NtkAbstractMemory( p, vMemObjs, vMemFanins, &iFirstMemPi, &iFirstCi, &iFirstMemCi, NULL, NULL );
    nDcBits     = Wlc_CountDcs( pNewFull->pInits );
    vFirstTotal = Wlc_NtkDeriveFirstTotal( p, vMemObjs, vMemFanins, iFirstMemPi, nDcBits + iFirstMemCi, fVerbose );
 
    pAbsFull    = Wlc_NtkBitBlast( pNewFull, NULL );
    assert( Gia_ManPiNum(pAbsFull) == iFirstCi + nDcBits );
    Wlc_NtkFree( pNewFull );
 
    // perform abstraction
    for ( nIters = 0; nIters < nIterMax; nIters++ )
    {
        // set up parameters to run PDR
        Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
        Pdr_ManSetDefaultParams( pPdrPars );
        pPdrPars->fUseAbs    = 0;   // use 'pdr -t'  (on-the-fly abstraction)
        pPdrPars->fVerbose   = fVerbose;
 
        // derive specific abstraction
        pNew = Wlc_NtkAbstractMemory( p, vMemObjs, NULL, &iFirstMemPi, &iFirstCi, &iFirstMemCi, vRefines, vNodeFrames );
        pAbs = Wlc_NtkBitBlast( pNew, NULL );
        // simplify the AIG
        //pAbs = Gia_ManSeqStructSweep( pGiaTemp = pAbs, 1, 1, 0 );
        //Gia_ManStop( pGiaTemp );
 
        // roll in the constraints
        pAig = Gia_ManToAigSimple( pAbs );
        Gia_ManStop( pAbs );
        pAig->nConstrs = 1;
        pAig = Saig_ManDupFoldConstrsFunc( pTempAig = pAig, 0, 0, 1 );
        Aig_ManStop( pTempAig );
        pAbs = Gia_ManFromAigSimple( pAig );
        Aig_ManStop( pAig );
 
        // try to prove abstracted GIA by converting it to AIG and calling PDR
        pAig = Gia_ManToAigSimple( pAbs );
        RetValue = Pdr_ManSolve( pAig, pPdrPars );
        pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
        Aig_ManStop( pAig );
 
        if ( fVerbose )
            printf( "\nITERATIONS %d:\n", nIters );
        if ( fVerbose )
            Wlc_NtkPrintCex( p, pNew, pCex );
        Wlc_NtkFree( pNew );
 
        if ( fDumpAbs )
        {
            char * pFileName = "mem_abs.aig";
            Gia_AigerWrite( pAbs, pFileName, 0, 0, 0 );
            printf( "Iteration %3d: Dumped abstraction in file \"%s\" after finding CEX in frame %d.\n", nIters, pFileName, pCex ? pCex->iFrame : -1 );
        }
 
        // check if proved or undecided
        if ( pCex == NULL ) 
        {
            assert( RetValue );
            Gia_ManStop( pAbs );
            break;
        }
 
        // analyze counter-example
        vValues = Wlc_NtkConvertCex( vFirstTotal, pAbsFull, pCex, fVerbose );
        Gia_ManStop( pAbs );
        vRefine = Wlc_NtkFindConflict( p, vMemObjs, vValues, pCex->iFrame + 1 );
        Vec_WrdFree( vValues );
        if ( vRefine == NULL ) // cannot refine
            break;
        Abc_CexFreeP( &pCex );
 
        // save refinement for the future
        if ( fVerbose )
            Wlc_NtkPrintConflict( p, vRefine );
        Vec_WecPushLevel( vRefines );
        Vec_IntAppend( Vec_WecEntryLast(vRefines), vRefine );
        Wlc_NtkAbsAddToNodeFrames( vNodeFrames, vRefine );
        Vec_IntFree( vRefine );
    }
    // cleanup
    Gia_ManStop( pAbsFull );
    Vec_WecFree( vRefines );
    Vec_IntFreeP( &vMemObjs );
    Vec_IntFreeP( &vMemFanins );
    Vec_IntFreeP( &vFirstTotal );
    Vec_IntFreeP( &vNodeFrames );
 
    // report the result
    if ( fVerbose )
        printf( "\n" );
    printf( "Abstraction " );
    if ( RetValue == 0 && pCex )
        printf( "resulted in a real CEX in frame %d", pCex->iFrame );
    else if ( RetValue == 1 )
        printf( "is successfully proved" );
    else 
        printf( "timed out" );
    printf( " after %d iterations. ", nIters );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    Abc_CexFreeP( &pCex ); // return CEX in the future
    return RetValue;
}

Here is the call graph for this function:

Wlc_NtkMemAbstractTest()

Wlc_Ntk_t * Wlc_NtkMemAbstractTest ( Wlc_Ntk_t * p )

extern

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

Synopsis [Perform abstraction.]

Description []

SideEffects []

SeeAlso []

Definition at line 954 of file wlcMem.c.

{
    int iFirstMemPi, iFirstCi, iFirstMemCi, nDcBits;
    Vec_Int_t * vRefine;
    Vec_Int_t * vMemObjs    = Wlc_NtkCollectMemory( p, 0 );
    Vec_Int_t * vMemFanins  = Wlc_NtkCollectMemFanins( p, vMemObjs );
 
    Vec_Wec_t * vRefines    = Vec_WecAlloc( 100 );
    Vec_Int_t * vNodeFrames = Vec_IntAlloc( 100 );
    Wlc_Ntk_t * pNewFull;
 
    vRefine     = Vec_WecPushLevel(vRefines);
    Vec_IntPush( vRefine,  (11 << 11) | 0 );
    Vec_IntPush( vRefine,  (10 << 11) | 0 );
    Vec_IntPush( vRefine,  ( 8 << 11) | 0 );
    Vec_IntPush( vRefine,  ( 9 << 11) | 0 );
    Wlc_NtkAbsAddToNodeFrames( vNodeFrames, vRefine );
 
//    pNewFull    = Wlc_NtkAbstractMemory( p, vMemObjs, vMemFanins, &iFirstMemPi, &iFirstCi, &iFirstMemCi, NULL, NULL );
    pNewFull    = Wlc_NtkAbstractMemory( p, vMemObjs, NULL, &iFirstMemPi, &iFirstCi, &iFirstMemCi, vRefines, vNodeFrames );
 
    Vec_WecFree( vRefines );
    Vec_IntFree( vNodeFrames );
 
    nDcBits     = Wlc_CountDcs( pNewFull->pInits );
    printf( "iFirstMemPi = %d  iFirstCi = %d  iFirstMemCi = %d  nDcBits = %d\n", iFirstMemPi, iFirstCi, iFirstMemCi, nDcBits );
 
    Vec_IntFreeP( &vMemObjs );
    Vec_IntFreeP( &vMemFanins );
    return pNewFull;
}

Here is the call graph for this function:

Wlc_NtkNewName()

char * Wlc_NtkNewName ( Wlc_Ntk_t * p, int iCoId, int fSeq )

extern

Definition at line 847 of file wlcNtk.c.

{
    static char pBuffer[1000];
    sprintf( pBuffer, "%s_o%d_%s", p->pName, iCoId, fSeq ? "seq": "comb" );
    return pBuffer;
}

Here is the call graph for this function:

Wlc_NtkPairIsUifable()

int Wlc_NtkPairIsUifable ( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 )

extern

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

Synopsis [Check if two objects have the same input/output signatures.]

Description []

SideEffects []

SeeAlso []

Definition at line 89 of file wlcUif.c.

{
    Wlc_Obj_t * pFanin, * pFanin2;  int k;
    if ( Wlc_ObjRange(pObj) != Wlc_ObjRange(pObj2) )
        return 0;
    if ( Wlc_ObjIsSigned(pObj) != Wlc_ObjIsSigned(pObj2) )
        return 0;
    if ( Wlc_ObjFaninNum(pObj) != Wlc_ObjFaninNum(pObj2) )
        return 0;
    for ( k = 0; k < Wlc_ObjFaninNum(pObj); k++ )
    {
        pFanin = Wlc_ObjFanin(p, pObj, k);
        pFanin2 = Wlc_ObjFanin(p, pObj2, k);
        if ( Wlc_ObjRange(pFanin) != Wlc_ObjRange(pFanin2) )
            return 0;
        if ( Wlc_ObjIsSigned(pFanin) != Wlc_ObjIsSigned(pFanin2) )
            return 0;
    }
    return 1;
}

Here is the caller graph for this function:

Wlc_NtkPdrAbs()

int Wlc_NtkPdrAbs ( Wlc_Ntk_t * p, Wlc_Par_t * pPars )

extern

Definition at line 1755 of file wlcAbs.c.

{
    Wla_Man_t * pWla = NULL;
    
    int RetValue = -1;
 
    pWla = Wla_ManStart( p, pPars );
 
    RetValue = Wla_ManSolve( pWla, pPars );
 
    Wla_ManStop( pWla );
    
    return RetValue;
}

Here is the call graph for this function:

Wlc_NtkPrintMemory()

void Wlc_NtkPrintMemory ( Wlc_Ntk_t * p )

extern

Definition at line 239 of file wlcMem.c.

{
    Vec_Int_t * vMemory;
    vMemory = Wlc_NtkCollectMemory( p, 1 );
    printf( "Memory subsystem is composed of the following objects:\n" );
    Wlc_NtkPrintNodeArray( p, vMemory );
    Vec_IntFree( vMemory );
}

Here is the call graph for this function:

Wlc_NtkPrintNode()

void Wlc_NtkPrintNode ( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )

extern

Definition at line 703 of file wlcNtk.c.

{
    printf( "%8d  :  ", Wlc_ObjId(p, pObj) );
    if ( Vec_IntSize(&p->vLevels) )
        printf( "Lev = %2d  ", Vec_IntEntry(&p->vLevels, Wlc_ObjId(p,pObj)) );
    printf( "%6d%s = ", Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ? "s" : " " );
    if ( pObj->Type == WLC_OBJ_PI )
    {
        printf( "            PI                   :    %-12s\n", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
        return;
    }
    if ( pObj->Type == WLC_OBJ_FO )
    {
        printf( "            FO                   :    %-12s = %-12s\n", Wlc_ObjName(p, Wlc_ObjId(p, pObj)), Wlc_ObjName(p, Wlc_ObjId(p, Wlc_ObjFo2Fi(p, pObj))) );
        return;
    }
    if ( pObj->Type != WLC_OBJ_CONST && Wlc_ObjFaninNum(pObj) == 0 )
    {
        printf( "Unknown object without fanins    :    %-12s\n", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
        return;
    }
    if ( pObj->Type != WLC_OBJ_CONST )
    {
        printf( "%6d%s  %5s  ",  Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin0(p, pObj)) ? "s" : " ", Wlc_Names[(int)pObj->Type] );
        if ( Wlc_ObjFaninNum(pObj) > 1 )
            printf( "%6d%s ",       Wlc_ObjRange(Wlc_ObjFanin1(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin1(p, pObj)) ? "s" : " " );
        else
            printf( "        " );
        if ( Wlc_ObjFaninNum(pObj) > 2 )
            printf( "%6d%s ",       Wlc_ObjRange(Wlc_ObjFanin2(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin2(p, pObj)) ? "s" : " " );
        else
            printf( "        " );
    }
    else
        printf( "                                " );
    printf( " :    " );
    printf( "%-12s",   Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
    if ( pObj->Type == WLC_OBJ_CONST )
    {
        printf( " = %d\'%sh", Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ? "s":"" );
        if ( pObj->fXConst )
        {
            int k;
            for ( k = 0; k < (Wlc_ObjRange(pObj) + 3) / 4; k++ )
                printf( "x" );
        }
        else
            Abc_TtPrintHexArrayRev( stdout, (word *)Wlc_ObjConstValue(pObj), (Wlc_ObjRange(pObj) + 3) / 4 );
    }
    else
    {
        printf( " =  %-12s  %5s  ", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)), Wlc_Names[(int)pObj->Type] );
        if ( Wlc_ObjFaninNum(pObj) > 1 )
            printf( "%-12s ",       Wlc_ObjName(p, Wlc_ObjFaninId1(pObj)) );
        else
            printf( "             " );
        if ( Wlc_ObjFaninNum(pObj) > 2 )
            printf( "%-12s ",       Wlc_ObjName(p, Wlc_ObjFaninId2(pObj)) );
    }
    printf( "\n" );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_NtkPrintNodeArray()

void Wlc_NtkPrintNodeArray ( Wlc_Ntk_t * p, Vec_Int_t * vArray )

extern

Definition at line 764 of file wlcNtk.c.

{
    Wlc_Obj_t * pObj; 
    int i;
    Wlc_NtkForEachObjVec( vArray, p, pObj, i )
        Wlc_NtkPrintNode( p, pObj );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_NtkPrintNodes()

void Wlc_NtkPrintNodes ( Wlc_Ntk_t * p, int Type )

extern

Definition at line 771 of file wlcNtk.c.

{
    Wlc_Obj_t * pObj; 
    int i, Counter = 0;
    printf( "Operation %s\n", Wlc_Names[Type] );
    Wlc_NtkForEachObj( p, pObj, i )
    {
        if ( (int)pObj->Type != Type )
            continue;
        printf( "%8d  :", Counter++ );
        Wlc_NtkPrintNode( p, pObj );
    }
}

Here is the call graph for this function:

Wlc_NtkPrintObjects()

void Wlc_NtkPrintObjects ( Wlc_Ntk_t * p )

extern

Definition at line 812 of file wlcNtk.c.

{
    Wlc_Obj_t * pObj; int i;
    Wlc_NtkForEachObj( p, pObj, i )
        Wlc_NtkPrintNode( p, pObj );
}

Here is the call graph for this function:

Wlc_NtkPrintStats()

void Wlc_NtkPrintStats ( Wlc_Ntk_t * p, int fDistrib, int fTwoSides, int fVerbose )

extern

Definition at line 784 of file wlcNtk.c.

{
    int i;
    printf( "%-20s : ",        p->pName );
    printf( "PI = %4d  ",      Wlc_NtkCountRealPis(p) ); //Wlc_NtkPiNum(p) );
    printf( "PO = %4d  ",      Wlc_NtkPoNum(p) );
    printf( "FF = %4d  ",      Wlc_NtkFfNum(p) );
    printf( "Obj = %6d  ",     Wlc_NtkObjNum(p) - Wlc_NtkPiNum(p) - Wlc_NtkPoNum(p) - Wlc_NtkFfNum(p) );
    printf( "Mem = %.3f MB",   1.0*Wlc_NtkMemUsage(p)/(1<<20) );
    printf( "\n" );
    if ( fDistrib )
    {
        Wlc_NtkPrintDistrib( p, fTwoSides, fVerbose );
        return;
    }
    if ( !fVerbose )
        return;
    printf( "Node type statistics:\n" );
    for ( i = 1; i < WLC_OBJ_NUMBER; i++ )
    {
        if ( !p->nObjs[i] )
            continue;
        if ( p->nAnds[0] && p->nAnds[i] )
            printf( "%2d  :  %-8s  %6d  %7.2f %%\n", i, Wlc_Names[i], p->nObjs[i], 100.0*p->nAnds[i]/p->nAnds[0] );
        else
            printf( "%2d  :  %-8s  %6d\n", i, Wlc_Names[i], p->nObjs[i] );
    }
}

Here is the call graph for this function:

Wlc_NtkProfileCones()

void Wlc_NtkProfileCones ( Wlc_Ntk_t * p )

extern

Definition at line 1202 of file wlcNtk.c.

{
    Wlc_Obj_t * pObj; 
    int i, nPis, nFos, nNodes, nAdders, nMults;
    Wlc_NtkForEachCo( p, pObj, i )
    {
        Wlc_NtkMarkCone( p, i, 1, 0, 0 );
        nNodes = Wlc_NtkCountMarked( p, &nPis, &nFos, &nAdders, &nMults );
        printf( "Cone %5d : ", i );
        printf( "PI = %4d  ", nPis );
        printf( "FO = %4d  ", nFos );
        printf( "Node = %6d  ", nNodes );
        printf( "Add/Sub = %4d  ", nAdders );
        printf( "Mult = %4d  ", nMults );
        printf( "\n" );
    }
    Wlc_NtkCleanMarks( p );
}

Here is the call graph for this function:

Wlc_NtkRemapLevels()

int Wlc_NtkRemapLevels ( Wlc_Ntk_t * p, Vec_Int_t * vObjs, int nLevels )

extern

Definition at line 387 of file wlcNtk.c.

{
    int i, k, iFanin, iObj, Entry, Level = 0, Res = nLevels;
    Vec_Int_t * vMap  = Vec_IntStart( nLevels+1 );
    Vec_Int_t * vUsed = Vec_IntStart( nLevels+1 );
    // mark used levels
    Vec_IntWriteEntry( vUsed, nLevels, 1 );
    Vec_IntForEachEntry( vObjs, iObj, i )
    {
        Vec_IntWriteEntry( vUsed, Wlc_ObjLevelId(p, iObj), 1 );
        Wlc_ObjForEachFanin( Wlc_NtkObj(p, iObj), iFanin, k ) if ( iFanin )
            Vec_IntWriteEntry( vUsed, Wlc_ObjLevelId(p, iFanin), 1 );
    }
    // create level map
    Vec_IntForEachEntry( vUsed, Entry, i )
        if ( Entry )
            Vec_IntWriteEntry( vMap, i, Level++ );
    //printf( "Total used levels %d -> %d\n", nLevels, Level );
    // remap levels
    Vec_IntForEachEntry( &p->vLevels, Level, i )
    {
        if ( Vec_IntEntry(vUsed, Level) )
            Vec_IntWriteEntry( &p->vLevels, i, Vec_IntEntry(vMap, Level) );
        else
            Vec_IntWriteEntry( &p->vLevels, i, -1 );
    }
    Res = Vec_IntEntry( vMap, nLevels );
    Vec_IntFree( vUsed );
    Vec_IntFree( vMap );
    return Res;
}

Here is the caller graph for this function:

Wlc_NtkSetRefs()

void Wlc_NtkSetRefs ( Wlc_Ntk_t * p )

extern

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

Synopsis [Create references.]

Description []

SideEffects []

SeeAlso []

Definition at line 1373 of file wlcNtk.c.

{
    Wlc_Obj_t * pObj; int i, k, Fanin;
    Vec_IntFill( &p->vRefs, Wlc_NtkObjNumMax(p), 0 );
    Wlc_NtkForEachObj( p, pObj, i )
        Wlc_ObjForEachFanin( pObj, Fanin, k )
            Vec_IntAddToEntry( &p->vRefs, Fanin, 1 );
    Wlc_NtkForEachCo( p, pObj, i )
        Vec_IntAddToEntry( &p->vRefs, Wlc_ObjId(p, pObj), 1 );
}

Here is the caller graph for this function:

Wlc_NtkShortNames()

void Wlc_NtkShortNames ( Wlc_Ntk_t * p )

extern

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

Synopsis [Creates short names for all objects.]

Description []

SideEffects []

SeeAlso []

Definition at line 1292 of file wlcNtk.c.

{
    Wlc_Obj_t * pObj;
    char pBuffer[1000];
    int NameId, fFound, i;
    int nFlops = Wlc_NtkCoNum(p) - Wlc_NtkPoNum(p);
    unsigned char nDigits = (unsigned char)Abc_Base10Log( nFlops );
    Wlc_NtkForEachCo( p, pObj, i )
    {
        if ( Wlc_ObjIsPo(pObj) )
            continue;
        sprintf( pBuffer, "%s%0*d", "fi", nDigits, i - Wlc_NtkPoNum(p) );
        NameId = Abc_NamStrFindOrAdd( p->pManName, pBuffer, &fFound );
        Wlc_ObjSetNameId( p, Wlc_ObjId(p, pObj), NameId );
    }
    Wlc_NtkForEachCi( p, pObj, i )
    {
        if ( Wlc_ObjIsPi(pObj) )
            continue;
        sprintf( pBuffer, "%s%0*d", "fo", nDigits, i - Wlc_NtkPiNum(p) );
        NameId = Abc_NamStrFindOrAdd( p->pManName, pBuffer, &fFound );
        Wlc_ObjSetNameId( p, Wlc_ObjId(p, pObj), NameId );
    }
    nDigits = Abc_Base10Log( Wlc_NtkPoNum(p) );
    Wlc_NtkForEachPo( p, pObj, i )
    {
        sprintf( pBuffer, "%s%0*d", "po", nDigits, i );
        NameId = Abc_NamStrFindOrAdd( p->pManName, pBuffer, &fFound );
        Wlc_ObjSetNameId( p, Wlc_ObjId(p, pObj), NameId );
    }
    nDigits = Abc_Base10Log( Wlc_NtkPiNum(p) );
    Wlc_NtkForEachPi( p, pObj, i )
    {
        sprintf( pBuffer, "%s%0*d", "pi", nDigits, i );
        NameId = Abc_NamStrFindOrAdd( p->pManName, pBuffer, &fFound );
        Wlc_ObjSetNameId( p, Wlc_ObjId(p, pObj), NameId );
    }
    nDigits = Abc_Base10Log( Wlc_NtkObjNum(p) );
    Wlc_NtkForEachObj( p, pObj, i )
    {
        if ( Wlc_ObjIsCi(pObj) || Wlc_ObjIsCo(pObj) )
            continue;
        sprintf( pBuffer, "%s%0*d", "n", nDigits, i );
        NameId = Abc_NamStrFindOrAdd( p->pManName, pBuffer, &fFound );
        Wlc_ObjSetNameId( p, Wlc_ObjId(p, pObj), NameId );
    }
}

Here is the call graph for this function:

Wlc_NtkSimulate()

Vec_Ptr_t * Wlc_NtkSimulate ( Wlc_Ntk_t * p, Vec_Int_t * vNodes, int nWords, int nFrames )

extern

Definition at line 128 of file wlcSim.c.

{
    Gia_Obj_t * pObj; 
    Vec_Ptr_t * vOne, * vRes;
    Gia_Man_t * pGia = Wlc_NtkBitBlast( p, NULL );
    Wlc_Obj_t * pWlcObj;
    int f, i, k, w, nBits, Counter = 0;
    // allocate simulation info for one timeframe
    Vec_WrdFreeP( &pGia->vSims );
    pGia->vSims = Vec_WrdStart( Gia_ManObjNum(pGia) * nWords );
    pGia->nSimWords = nWords;
    // allocate resulting simulation info
    vRes = Vec_PtrAlloc( Vec_IntSize(vNodes) );
    Wlc_NtkForEachObjVec( vNodes, p, pWlcObj, i )
    {
        nBits = Wlc_ObjRange(pWlcObj);
        vOne = Vec_PtrAlloc( nBits );
        for ( k = 0; k < nBits; k++ )
            Vec_PtrPush( vOne, ABC_CALLOC(word, nWords * nFrames) );
        Vec_PtrPush( vRes, vOne ); 
    }
    // perform simulation (const0 and flop outputs are already initialized)
    Gia_ManRandomW( 1 );
    for ( f = 0; f < nFrames; f++ )
    {
        Gia_ManForEachObj1( pGia, pObj, i )
        {
            if ( Gia_ObjIsAnd(pObj) )
                Wlc_ObjSimAnd( pGia, i );
            else if ( Gia_ObjIsCo(pObj) )
                Wlc_ObjSimCo( pGia, i );
            else if ( Gia_ObjIsPi(pGia, pObj) )
                Wlc_ObjSimPi( pGia, i );
            else if ( Gia_ObjIsRo(pGia, pObj) )
                Wlc_ObjSimRo( pGia, i );
        }
        // collect simulation data
        Wlc_NtkForEachObjVec( vNodes, p, pWlcObj, i )
        {
            int nBits = Wlc_ObjRange(pWlcObj);
            int iFirst = Vec_IntEntry( &p->vCopies, Wlc_ObjId(p, pWlcObj) );
            for ( k = 0; k < nBits; k++ )
            {
                int iLit = Vec_IntEntry( &p->vBits, iFirst + k );
                word * pInfo = (word*)Vec_VecEntryEntry( (Vec_Vec_t *)vRes, i, k );
                if ( iLit == -1 )
                {
                    Counter++;
                    for ( w = 0; w < nWords; w++ )
                        pInfo[f * nWords + w] = 0;
                }
                else
                {
                    word * pInfoObj = Wlc_ObjSim( pGia, Abc_Lit2Var(iLit) );
                    for ( w = 0; w < nWords; w++ )
                        pInfo[f * nWords + w] = Abc_LitIsCompl(iLit) ? ~pInfoObj[w] : pInfoObj[w];
                }
            }
        }
        if ( f == 0 && Counter )
            printf( "Replaced %d dangling internal bits with constant 0.\n", Counter );
    }
    Vec_WrdFreeP( &pGia->vSims );
    pGia->nSimWords = 0;
    Gia_ManStop( pGia );
    return vRes;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_NtkToNdr()

void * Wlc_NtkToNdr ( Wlc_Ntk_t * pNtk )

extern

Definition at line 190 of file wlcNdr.c.

{
    Wlc_Obj_t * pObj; 
    int i, k, iFanin, iOutId, Type;
    // create a new module
    void * pDesign = Ndr_Create( 1 );
    int ModId = Ndr_AddModule( pDesign, 1 );
    // add primary inputs
    Vec_Int_t * vFanins = Vec_IntAlloc( 10 );
    Wlc_NtkForEachPi( pNtk, pObj, i ) 
    {
        iOutId = Wlc_ObjId(pNtk, pObj);
        Ndr_AddObject( pDesign, ModId, ABC_OPER_CI, 0,   
            pObj->End, pObj->Beg, pObj->Signed,   
            0, NULL,      1, &iOutId,  NULL  ); // no fanins
    }
    // add internal nodes 
    Wlc_NtkForEachObj( pNtk, pObj, iOutId ) 
    {
        char * pFunction = NULL;
        if ( Wlc_ObjIsPi(pObj) || pObj->Type == 0 )
            continue;
        Vec_IntClear( vFanins );
        Wlc_ObjForEachFanin( pObj, iFanin, k )
            Vec_IntPush( vFanins, iFanin );
        if ( pObj->Type == WLC_OBJ_CONST )
            pFunction = Ndr_ObjWriteConstant( (unsigned *)Wlc_ObjFanins(pObj), Wlc_ObjRange(pObj) );
        if ( pObj->Type == WLC_OBJ_MUX && Wlc_ObjRange(Wlc_ObjFanin0(pNtk, pObj)) > 1 )
            Type = ABC_OPER_SEL_NMUX;
        else if ( pObj->Type == WLC_OBJ_FO )
        {
            Wlc_Obj_t * pFi = Wlc_ObjFo2Fi( pNtk, pObj );
            assert( Vec_IntSize(vFanins) == 0 );
            Vec_IntPush( vFanins, Wlc_ObjId(pNtk, pFi) );
            Vec_IntFillExtra( vFanins, 7, 0 );
            Type = ABC_OPER_DFFRSE;
        }
        else
            Type = Ndr_TypeWlc2Ndr(pObj->Type);
        assert( Type > 0 );
        Ndr_AddObject( pDesign, ModId, Type, 0,   
            pObj->End, pObj->Beg, pObj->Signed,   
            Vec_IntSize(vFanins), Vec_IntArray(vFanins), 1, &iOutId,  pFunction  ); 
    }
    // add primary outputs
    Wlc_NtkForEachObj( pNtk, pObj, iOutId ) 
    {
        if ( !Wlc_ObjIsPo(pObj) )
            continue;
        Vec_IntFill( vFanins, 1, iOutId );
        Ndr_AddObject( pDesign, ModId, ABC_OPER_CO, 0,                   
            pObj->End, pObj->Beg, pObj->Signed,   
            1, Vec_IntArray(vFanins),  0, NULL,  NULL ); 
    }
    Vec_IntFree( vFanins );
    return pDesign;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_NtkTransferNames()

void Wlc_NtkTransferNames ( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 830 of file wlcNtk.c.

{
    int i;
    assert( !Wlc_NtkHasCopy(pNew)   && Wlc_NtkHasCopy(p)   );
    assert( !Wlc_NtkHasNameId(pNew) && Wlc_NtkHasNameId(p) );
    assert( pNew->pManName  == NULL && p->pManName != NULL );
    Wlc_NtkCleanNameId( pNew );
    for ( i = 0; i < p->nObjsAlloc; i++ )
        if ( Wlc_ObjCopy(p, i) > 0 && i < Vec_IntSize(&p->vNameIds) && Wlc_ObjNameId(p, i) )
            Wlc_ObjSetNameId( pNew, Wlc_ObjCopy(p, i), Wlc_ObjNameId(p, i) );
    pNew->pManName = p->pManName; 
    p->pManName = NULL;
    Vec_IntErase( &p->vNameIds );
    // transfer table
    pNew->pMemTable = p->pMemTable;  p->pMemTable = NULL;
    pNew->vTables = p->vTables;      p->vTables = NULL;
}

Here is the caller graph for this function:

Wlc_NtkUifNodePairs()

Wlc_Ntk_t * Wlc_NtkUifNodePairs ( Wlc_Ntk_t * p, Vec_Int_t * vPairsInit )

extern

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

Synopsis [Adds UIF constraints to node pairs and updates POs.]

Description []

SideEffects []

SeeAlso []

Definition at line 236 of file wlcUif.c.

{
    Vec_Int_t * vPairs = vPairsInit;
    Wlc_Ntk_t * pNew;
    Wlc_Obj_t * pObj, * pObj2;
    Vec_Int_t * vUifConstrs, * vCompares, * vFanins;
    int i, k, iObj, iObj2, iObjNew, iObjNew2;
    int iFanin, iFanin2, iFaninNew;
    // get multiplier pairs if not given
    if ( vPairs == NULL )
        vPairs = Wlc_NtkFindUifableMultiplierPairs( p );
    if ( vPairs == NULL )
        return NULL;
    // sanity checks
    assert( Vec_IntSize(vPairs) > 0 && Vec_IntSize(vPairs) % 2 == 0 );
    // iterate through node pairs
    vFanins = Vec_IntAlloc( 100 );
    vCompares = Vec_IntAlloc( 100 );
    vUifConstrs = Vec_IntAlloc( 100 );
    Vec_IntForEachEntryDouble( vPairs, iObj, iObj2, i )
    {
        // get two nodes
        pObj  = Wlc_NtkObj( p, iObj );
        pObj2 = Wlc_NtkObj( p, iObj2 );
        assert( Wlc_NtkPairIsUifable(p, pObj, pObj2) );
        // create fanin comparator nodes
        Vec_IntClear( vCompares );
        Wlc_ObjForEachFanin( pObj, iFanin, k )
        {
            iFanin2 = Wlc_ObjFaninId( pObj2, k );
            Vec_IntFillTwo( vFanins, 2, iFanin, iFanin2 );
            iFaninNew = Wlc_ObjCreate( p, WLC_OBJ_COMP_NOTEQU, 0, 0, 0, vFanins );
            Vec_IntPush( vCompares, iFaninNew );
            // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to 
            // Wlc_ObjCreate() due to a possible realloc of the internal array of objects...
            pObj = Wlc_NtkObj( p, iObj );
        }
        // concatenate fanin comparators
        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vCompares) - 1, 0, vCompares );
        // create reduction-OR node
        Vec_IntFill( vFanins, 1, iObjNew );
        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_OR, 0, 0, 0, vFanins );
        // craete output comparator node
        Vec_IntFillTwo( vFanins, 2, iObj, iObj2 );
        iObjNew2 = Wlc_ObjCreate( p, WLC_OBJ_COMP_EQU, 0, 0, 0, vFanins );
        // create implication node (iObjNew is already complemented above)
        Vec_IntFillTwo( vFanins, 2, iObjNew, iObjNew2 );
        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_OR, 0, 0, 0, vFanins );
        // save the constraint
        Vec_IntPush( vUifConstrs, iObjNew );
    }
    // derive the AND of the UIF contraints
    assert( Vec_IntSize(vUifConstrs) > 0 );
    if ( Vec_IntSize(vUifConstrs) == 1 )
        iObjNew = Vec_IntEntry( vUifConstrs, 0 );
    else
    {
        // concatenate
        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vUifConstrs) - 1, 0, vUifConstrs );
        // create reduction-AND node
        Vec_IntFill( vFanins, 1, iObjNew );
        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_AND, 0, 0, 0, vFanins );
    }
    // update each PO to point to the new node
    Wlc_NtkForEachPo( p, pObj, i )
    {
        iObj = Wlc_ObjId(p, pObj);
        Vec_IntFillTwo( vFanins, 2, iObj, iObjNew );
        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_AND, 0, 0, 0, vFanins );
        // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to 
        // Wlc_ObjCreate() due to a possible realloc of the internal array of objects...
        pObj = Wlc_NtkObj( p, iObj );
        // update PO/CO arrays
        assert( Vec_IntEntry(&p->vPos, i) == iObj );
        assert( Vec_IntEntry(&p->vCos, i) == iObj );
        Vec_IntWriteEntry( &p->vPos, i, iObjNew );
        Vec_IntWriteEntry( &p->vCos, i, iObjNew );
        // transfer the PO attribute
        Wlc_NtkObj(p, iObjNew)->fIsPo = 1;
        assert( pObj->fIsPo );
        pObj->fIsPo = 0;
    }
    // cleanup
    Vec_IntFree( vUifConstrs );
    Vec_IntFree( vCompares );
    Vec_IntFree( vFanins );
    if ( vPairs != vPairsInit )
        Vec_IntFree( vPairs );
    // reconstruct topological order
    pNew = Wlc_NtkDupDfs( p, 0, 1 );
    return pNew;
}

Here is the call graph for this function:

Wlc_ObjAddFanins()

void Wlc_ObjAddFanins ( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFanins )

extern

Definition at line 240 of file wlcNtk.c.

{
    assert( pObj->nFanins == 0 );
    pObj->nFanins = Vec_IntSize(vFanins);
    // special treatment of CONST, SELECT and TABLE
    if ( pObj->Type == WLC_OBJ_CONST )
        pObj->nFanins = 0;
    else if ( pObj->Type == WLC_OBJ_BIT_SELECT || pObj->Type == WLC_OBJ_TABLE )
        pObj->nFanins = 1;
    if ( Wlc_ObjHasArray(pObj) )
        pObj->pFanins[0] = (int *)Mem_FlexEntryFetch( p->pMemFanin, Vec_IntSize(vFanins) * sizeof(int) );
    memcpy( Wlc_ObjFanins(pObj), Vec_IntArray(vFanins), sizeof(int) * Vec_IntSize(vFanins) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_ObjAlloc()

int Wlc_ObjAlloc ( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg )

extern

Definition at line 199 of file wlcNtk.c.

{
    Wlc_Obj_t * pObj;
    assert( Type != WLC_OBJ_PO && Type != WLC_OBJ_FI );
    if ( p->iObj == p->nObjsAlloc )
    {
        p->pObjs = ABC_REALLOC( Wlc_Obj_t, p->pObjs, 2 * p->nObjsAlloc );
        memset( p->pObjs + p->nObjsAlloc, 0, sizeof(Wlc_Obj_t) * p->nObjsAlloc );
        p->nObjsAlloc *= 2;
    }
    pObj = Wlc_NtkObj( p, p->iObj );
    pObj->Type   = Type;
    pObj->Signed = Signed;
    pObj->End    = End;
    pObj->Beg    = Beg;
    if ( Wlc_ObjIsCi(pObj) )
        Wlc_ObjSetCi( p, pObj );
    p->nObjs[Type]++;
    return p->iObj++;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_ObjCreate()

int Wlc_ObjCreate ( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg, Vec_Int_t * vFanins )

extern

Definition at line 219 of file wlcNtk.c.

{
    int iFaninNew = Wlc_ObjAlloc( p, Type, Signed, End, Beg );
    Wlc_ObjAddFanins( p, Wlc_NtkObj(p, iFaninNew), vFanins );
    return iFaninNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_ObjDup()

int Wlc_ObjDup ( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec_Int_t * vFanins )

extern

Definition at line 930 of file wlcNtk.c.

{
    Wlc_Obj_t * pObj = Wlc_NtkObj( p, iObj );
    int iFaninNew = Wlc_ObjAlloc( pNew, pObj->Type, Wlc_ObjIsSigned(pObj), pObj->End, pObj->Beg );
    Wlc_Obj_t * pObjNew = Wlc_NtkObj(pNew, iFaninNew);
    Wlc_ObjCollectCopyFanins( p, iObj, vFanins );
    Wlc_ObjAddFanins( pNew, pObjNew, vFanins );
    Wlc_ObjSetCopy( p, iObj, iFaninNew );
    pObjNew->fXConst = pObj->fXConst;
    return iFaninNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_ObjName()

char * Wlc_ObjName ( Wlc_Ntk_t * p, int iObj )

extern

Definition at line 225 of file wlcNtk.c.

{
    static char Buffer[100];
    if ( Wlc_NtkHasNameId(p) && Wlc_ObjNameId(p, iObj) )
        return Abc_NamStr( p->pManName, Wlc_ObjNameId(p, iObj) );
    sprintf( Buffer, "n%d", iObj );
    return Buffer;
}                          

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_ObjSetCi()

void Wlc_ObjSetCi ( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )

extern

Definition at line 168 of file wlcNtk.c.

{
    assert( Wlc_ObjIsCi(pObj) );
    assert( Wlc_ObjFaninNum(pObj) == 0 );
    if ( Wlc_NtkPiNum(p) == Wlc_NtkCiNum(p) || pObj->Type != WLC_OBJ_PI )
    {
        pObj->Fanins[1] = Vec_IntSize(&p->vCis);
        Vec_IntPush( &p->vCis, Wlc_ObjId(p, pObj) );
    }
    else // insert in the array of CI at the end of PIs
    {
        Wlc_Obj_t * pTemp; int i;
        Vec_IntInsert( &p->vCis, Wlc_NtkPiNum(p), Wlc_ObjId(p, pObj) );
        // other CI IDs are invalidated... naive fix!
        Wlc_NtkForEachCi( p, pTemp, i )
            pTemp->Fanins[1] = i;
    }
    if ( pObj->Type == WLC_OBJ_PI )
        Vec_IntPush( &p->vPis, Wlc_ObjId(p, pObj) );
}

Here is the caller graph for this function:

Wlc_ObjSetCo()

void Wlc_ObjSetCo ( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int fFlopInput )

extern

Definition at line 188 of file wlcNtk.c.

{
//    pObj->Fanins[1] = Vec_IntSize(&p->vCos);
    Vec_IntPush( &p->vCos, Wlc_ObjId(p, pObj) );
    if ( !fFlopInput )
        Vec_IntPush( &p->vPos, Wlc_ObjId(p, pObj) );
    if ( fFlopInput )
        pObj->fIsFi = 1;
    else
        pObj->fIsPo = 1;
}

Here is the caller graph for this function:

Wlc_ObjTypeName()

char * Wlc_ObjTypeName ( Wlc_Obj_t * p )

extern

Definition at line 97 of file wlcNtk.c.

{ return p ? (p->Type < WLC_OBJ_NUMBER ? Wlc_Names[p->Type] : (char *)"out_of_bound") : (char *)"no_obj"; }

Here is the caller graph for this function:

Wlc_ObjUpdateType()

void Wlc_ObjUpdateType ( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int Type )

extern

Definition at line 233 of file wlcNtk.c.

{
    assert( pObj->Type == WLC_OBJ_NONE );
    p->nObjs[pObj->Type]--;
    pObj->Type = Type;
    p->nObjs[pObj->Type]++;
}

Here is the caller graph for this function:

Wlc_PrsConvertInitValues()

char * Wlc_PrsConvertInitValues ( Wlc_Ntk_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 440 of file wlcReadVer.c.

{
    Wlc_Obj_t * pObj; 
    int i, k, Value, * pInits;
    char * pResult;
    Vec_Str_t * vStr = Vec_StrAlloc( 1000 );
    Vec_IntForEachEntry( p->vInits, Value, i )
    {
        if ( Value < 0 )
        {
            for ( k = 0; k < -Value; k++ )
                Vec_StrPush( vStr, '0' );
            continue;
        }
        pObj = Wlc_NtkObj( p, Value );
        Value = Wlc_ObjRange(pObj);
        while ( pObj->Type == WLC_OBJ_BUF )
            pObj = Wlc_NtkObj( p, Wlc_ObjFaninId0(pObj) );
        pInits = (pObj->Type == WLC_OBJ_CONST && !pObj->fXConst) ? Wlc_ObjConstValue(pObj) : NULL;
        for ( k = 0; k < Abc_MinInt(Value, Wlc_ObjRange(pObj)); k++ )
            Vec_StrPush( vStr, (char)(pInits ? '0' + Abc_InfoHasBit((unsigned *)pInits, k) : 'x') );
        // extend values with zero, in case the init value signal has different range compared to constant used
        for ( ; k < Value; k++ )
            Vec_StrPush( vStr, '0' );
        // update vInits to contain either number of values or PI index
        Vec_IntWriteEntry( p->vInits, i, (pInits || pObj->fXConst) ? -Value : Wlc_ObjCiId(pObj) );
    }
    Vec_StrPush( vStr, '\0' );
    pResult = Vec_StrReleaseArray( vStr );
    Vec_StrFree( vStr );
    return pResult;
}

Here is the caller graph for this function:

Wlc_ReadNdr()

Wlc_Ntk_t * Wlc_ReadNdr ( char * pFileName )

extern

Definition at line 551 of file wlcNdr.c.

{
    void * pData = Ndr_Read( pFileName );
    Wlc_Ntk_t * pNtk = Wlc_NtkFromNdr( pData );
    //Ndr_DumpNdr( pData );
    //char * ppNames[10] = { NULL, "a", "b", "c", "d", "e", "f", "g", "h", "i" };
    //Ndr_WriteVerilog( NULL, pData, ppNames, 0 );
    //Ndr_Delete( pData );
    Abc_FrameInputNdr( Abc_FrameGetGlobalFrame(), pData );
    return pNtk;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_ReadSmt()

Wlc_Ntk_t * Wlc_ReadSmt ( char * pFileName, int fOldParser, int fPrintTree )

extern

Definition at line 1766 of file wlcReadSmt.c.

{
    Wlc_Ntk_t * pNtk = NULL;
    char * pBuffer, * pLimit; 
    pBuffer = Smt_PrsLoadFile( pFileName, &pLimit );
    if ( pBuffer == NULL )
        return NULL;
    pNtk = Wlc_ReadSmtBuffer( pFileName, pBuffer, pLimit, fOldParser, fPrintTree );
    ABC_FREE( pBuffer );
    return pNtk;
}

Here is the call graph for this function:

Wlc_ReadSmtBuffer()

Wlc_Ntk_t * Wlc_ReadSmtBuffer ( char * pFileName, char * pBuffer, char * pLimit, int fOldParser, int fPrintTree )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1751 of file wlcReadSmt.c.

{
    Wlc_Ntk_t * pNtk = NULL;
    int nCount = Smt_PrsRemoveComments( pBuffer, pLimit );
    Smt_Prs_t * p = Smt_PrsAlloc( pFileName, pBuffer, pLimit, nCount );
    if ( p == NULL )
        return NULL;
    Smt_PrsReadLines( p );
    if ( fPrintTree )
        Smt_PrsPrintParser( p );
    if ( Smt_PrsErrorPrint(p) )
        pNtk = fOldParser ? Smt_PrsBuild(p) : Smt_PrsBuild2(p);
    Smt_PrsFree( p );
    return pNtk;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_ReadVer()

Wlc_Ntk_t * Wlc_ReadVer ( char * pFileName, char * pStr, int fInter )

extern

Definition at line 1693 of file wlcReadVer.c.

{
    Wlc_Prs_t * p;
    Wlc_Ntk_t * pNtk = NULL;
    // either file name or string is given
    assert( (pFileName == NULL) != (pStr == NULL) );
    // start the parser 
    p = Wlc_PrsStart( pFileName, pStr );
    if ( p == NULL )
        return NULL;
    // detect lines
    if ( !Wlc_PrsPrepare( p ) )
        goto finish;
    // parse models
    if ( !Wlc_PrsDerive( p, fInter ) )
    {
        if ( fInter )
        {
            printf( "Finished deriving interface for module \"%s\".\n", p->pNtk->pName );
            pNtk = p->pNtk;  p->pNtk = NULL;
            pNtk->pSpec = Abc_UtilStrsav( pFileName );
            if ( Vec_IntSize(&pNtk->vNameIds) == 0 ) 
            {
                Vec_Int_t * vTemp = Vec_IntStartNatural( Wlc_NtkObjNumMax(pNtk) );
                pNtk->vNameIds = *vTemp, Vec_IntZero(vTemp);
                Vec_IntFree( vTemp );
            }
            return pNtk;
        }
        goto finish;
    }
    // derive topological order
    if ( p->pNtk )
    {
        Wlc_Obj_t * pObj; int i;
        Wlc_NtkForEachObj( p->pNtk, pObj, i )
            if ( pObj->Type == WLC_OBJ_FF )
                Vec_IntPush( &p->pNtk->vFfs2, Wlc_ObjId(p->pNtk, pObj) );
        pNtk = Wlc_NtkDupDfs( p->pNtk, 0, 1 );
        pNtk->pSpec = Abc_UtilStrsav( pFileName );
    }
finish:
    Wlc_PrsPrintErrorMessage( p );
    Wlc_PrsStop( p );
    return pNtk;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_SetNtk()

void Wlc_SetNtk ( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 133 of file wlcCom.c.

{
    Wlc_AbcUpdateNtk( pAbc, pNtk );
}

Here is the caller graph for this function:

Wlc_StdinProcessSmt()

int Wlc_StdinProcessSmt ( Abc_Frame_t * pAbc, char * pCmd )

extern

Definition at line 190 of file wlcStdin.c.

{
    // collect stdin until (check-sat)
    Vec_Str_t * vInput = Wlc_StdinCollectProblem( "(check-sat)" );
    // parse input
    Wlc_Ntk_t * pNtk = Wlc_ReadSmtBuffer( "top", Vec_StrArray(vInput), Vec_StrArray(vInput) + Vec_StrSize(vInput), 0, 0 );
    Vec_StrFree( vInput );
    // install current network
    Wlc_SetNtk( pAbc, pNtk );
    // execute command
    if ( Cmd_CommandExecute(pAbc, pCmd) )
    {
        Abc_Print( 1, "Something did not work out with the command \"%s\".\n", pCmd );
        return 0;
    }
    // solver finished
    if ( Abc_FrameReadProbStatus(pAbc) == -1 )
        printf( "undecided\n" );
    else if ( Abc_FrameReadProbStatus(pAbc) == 1 )
        printf( "unsat\n" );
    else if ( Abc_FrameReadProbStatus(pAbc) == 0 )
        printf( "sat\n" );
    else assert( 0 );
    fflush( stdout );
    // wait for stdin for give directions
    while ( (vInput = Wlc_StdinCollectQuery()) != NULL )
    {
        char * pName = strtok( Vec_StrArray(vInput), " \n\t\r()" );
        // check directive 
        if ( strcmp(pName, "get-value") )
        {
            Abc_Print( 1, "ABC is expecting \"get-value\" in a follow-up input of the satisfiable problem.\n" );
            Vec_StrFree( vInput );
            return 0;
        }
        // check status
        if ( Abc_FrameReadProbStatus(pAbc) != 0 )
        {
            Abc_Print( 1, "ABC received a follow-up input for a problem that is not known to be satisfiable.\n" );
            Vec_StrFree( vInput );
            return 0;
        }
        // get the variable number
        pName = strtok( NULL, "() \n\t\r" );
        // get the counter-example
        if ( Abc_FrameReadCex(pAbc) == NULL )
        {
            Abc_Print( 1, "ABC does not have a counter-example available to process a \"get-value\" request.\n" );
            Vec_StrFree( vInput );
            return 0;
        }
        // report value of this variable
        Wlc_NtkReport( (Wlc_Ntk_t *)pAbc->pAbcWlc, (Abc_Cex_t *)Abc_FrameReadCex(pAbc), pName, 16 );
        Vec_StrFree( vInput );
        fflush( stdout );
    }
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Wlc_WinProfileArith()

void Wlc_WinProfileArith ( Wlc_Ntk_t * p )

extern

Definition at line 132 of file wlcWin.c.

{
    Vec_Int_t * vLeaves = Vec_IntAlloc( 1000 );
    Vec_Int_t * vNodes  = Vec_IntAlloc( 1000 );
    Wlc_Obj_t * pObj; int i, Count = 0;
    Wlc_NtkForEachObj( p, pObj, i )
        pObj->Mark = 0;
    Wlc_NtkForEachObj( p, pObj, i )
        if ( Wlc_ObjHasArithm_rec(p, pObj) ? Wlc_ObjIsCo(pObj) : Wlc_ObjHasArithmFanins(p, pObj) )
        {
            Wlc_WinCompute( p, pObj, vLeaves, vNodes ); 
            if ( Wlc_ManCountArithmReal(p, vNodes) < 2 )
                continue;
 
            printf( "Arithmetic cone of node %d (%s):\n", Wlc_ObjId(p, pObj), Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
            Wlc_NtkPrintNode( p, pObj );
            Vec_IntReverseOrder( vNodes );
            Wlc_NtkPrintNodeArray( p, vNodes );
            printf( "\n" );
            Count++;
        }
    Wlc_NtkForEachObj( p, pObj, i )
        assert( pObj->Mark == 0 );
    printf( "Finished printing %d arithmetic cones.\n", Count );
    Vec_IntFree( vLeaves );
    Vec_IntFree( vNodes );
}

Here is the call graph for this function:

Wlc_WriteNdr()

void Wlc_WriteNdr ( Wlc_Ntk_t * pNtk, char * pFileName )

extern

Definition at line 247 of file wlcNdr.c.

{
    void * pDesign = Wlc_NtkToNdr( pNtk );
    Ndr_Write( pFileName, pDesign );
    Ndr_Delete( pDesign );
    printf( "Dumped the current design into file \"%s\".\n", pFileName );
}

Here is the call graph for this function:

Wlc_WriteVer()

void Wlc_WriteVer ( Wlc_Ntk_t * p, char * pFileName, int fAddCos, int fNoFlops )

extern

Definition at line 597 of file wlcWriteVer.c.

{
    FILE * pFile;
    pFile = fopen( pFileName, "w" );
    if ( pFile == NULL )
    {
        fprintf( stdout, "Wlc_WriteVer(): Cannot open the output file \"%s\".\n", pFileName );
        return;
    }
    fprintf( pFile, "// Benchmark \"%s\" from file \"%s\" written by ABC on %s\n", p->pName, p->pSpec ? p->pSpec : "unknown", Extra_TimeStamp() );
    fprintf( pFile, "\n" );
    Wlc_WriteTables( pFile, p );
    if ( fAddCos )
        Wlc_WriteAddPos( p );
    Wlc_WriteVerInt( pFile, p, fNoFlops );
    fprintf( pFile, "\n" );
    fclose( pFile );
}

Here is the call graph for this function:

Here is the caller graph for this function: