aboutsummaryrefslogtreecommitdiffstats
path: root/kernel/utils.h
blob: 8942905fe3584af5ff0fa39c6d2e3a63c3eac035 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
/*
 *  yosys -- Yosys Open SYnthesis Suite
 *
 *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
 *
 *  Permission to use, copy, modify, and/or distribute this software for any
 *  purpose with or without fee is hereby granted, provided that the above
 *  copyright notice and this permission notice appear in all copies.
 *
 *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
 *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
 *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *
 */

// This file contains various c++ utility routines and helper classes that
// do not depend on any other components of yosys (except stuff like log_*).

#include "kernel/yosys.h"

#ifndef UTILS_H
#define UTILS_H

YOSYS_NAMESPACE_BEGIN

// ------------------------------------------------
// A map-like container, but you can save and restore the state
// ------------------------------------------------

template<typename Key, typename T, typename OPS = hash_ops<Key>>
struct stackmap
{
private:
	std::vector<dict<Key, T*, OPS>> backup_state;
	dict<Key, T, OPS> current_state;
	static T empty_tuple;

public:
	stackmap() { }
	stackmap(const dict<Key, T, OPS> &other) : current_state(other) { }

	template<typename Other>
	void operator=(const Other &other)
	{
		for (auto &it : current_state)
			if (!backup_state.empty() && backup_state.back().count(it.first) == 0)
				backup_state.back()[it.first] = new T(it.second);
		current_state.clear();

		for (auto &it : other)
			set(it.first, it.second);
	}

	bool has(const Key &k)
	{
		return current_state.count(k) != 0;
	}

	void set(const Key &k, const T &v)
	{
		if (!backup_state.empty() && backup_state.back().count(k) == 0)
			backup_state.back()[k] = current_state.count(k) ? new T(current_state.at(k)) : nullptr;
		current_state[k] = v;
	}

	void unset(const Key &k)
	{
		if (!backup_state.empty() && backup_state.back().count(k) == 0)
			backup_state.back()[k] = current_state.count(k) ? new T(current_state.at(k)) : nullptr;
		current_state.erase(k);
	}

	const T &get(const Key &k)
	{
		if (current_state.count(k) == 0)
			return empty_tuple;
		return current_state.at(k);
	}

	void reset(const Key &k)
	{
		for (int i = GetSize(backup_state)-1; i >= 0; i--)
			if (backup_state[i].count(k) != 0) {
				if (backup_state[i].at(k) == nullptr)
					current_state.erase(k);
				else
					current_state[k] = *backup_state[i].at(k);
				return;
			}
		current_state.erase(k);
	}

	const dict<Key, T, OPS> &stdmap()
	{
		return current_state;
	}

	void save()
	{
		backup_state.resize(backup_state.size()+1);
	}

	void restore()
	{
		log_assert(!backup_state.empty());
		for (auto &it : backup_state.back())
			if (it.second != nullptr) {
				current_state[it.first] = *it.second;
				delete it.second;
			} else
				current_state.erase(it.first);
		backup_state.pop_back();
	}

	~stackmap()
	{
		while (!backup_state.empty())
			restore();
	}
};


// ------------------------------------------------
// A simple class for topological sorting
// ------------------------------------------------

template<typename T, typename C = std::less<T>>
struct TopoSort
{
	bool analyze_loops, found_loops;
	std::map<T, std::set<T, C>, C> database;
	std::set<std::set<T, C>> loops;
	std::vector<T> sorted;

	TopoSort()
	{
		analyze_loops = true;
		found_loops = false;
	}

	void node(T n)
	{
		if (database.count(n) == 0)
			database[n] = std::set<T, C>();
	}

	void edge(T left, T right)
	{
		node(left);
		database[right].insert(left);
	}

	void sort_worker(const T &n, std::set<T, C> &marked_cells, std::set<T, C> &active_cells, std::vector<T> &active_stack)
	{
		if (active_cells.count(n)) {
			found_loops = true;
			if (analyze_loops) {
				std::set<T, C> loop;
				for (int i = GetSize(active_stack)-1; i >= 0; i--) {
					loop.insert(active_stack[i]);
					if (active_stack[i] == n)
						break;
				}
				loops.insert(loop);
			}
			return;
		}

		if (marked_cells.count(n))
			return;

		if (!database.at(n).empty())
		{
			if (analyze_loops)
				active_stack.push_back(n);
			active_cells.insert(n);

			for (auto &left_n : database.at(n))
				sort_worker(left_n, marked_cells, active_cells, active_stack);

			if (analyze_loops)
				active_stack.pop_back();
			active_cells.erase(n);
		}

		marked_cells.insert(n);
		sorted.push_back(n);
	}

	bool sort()
	{
		loops.clear();
		sorted.clear();
		found_loops = false;

		std::set<T, C> marked_cells;
		std::set<T, C> active_cells;
		std::vector<T> active_stack;

		for (auto &it : database)
			sort_worker(it.first, marked_cells, active_cells, active_stack);

		log_assert(GetSize(sorted) == GetSize(database));
		return !found_loops;
	}
};

YOSYS_NAMESPACE_END

#endif
> 1; // terminal node (CI/CO) unsigned iDiff1 : 29; // the diff of the second fanin unsigned fCompl1: 1; // the complemented attribute unsigned fMark1 : 1; // second user-controlled mark unsigned fPhase : 1; // value under 000 pattern unsigned Value; // application-specific value }; // Value is currently used to store several types of information // - pointer to the next node in the hash table during structural hashing // - pointer to the node copy during duplication // - traversal ID of the node during traversal // - reference counter of the node (will not be used in the future) // new AIG manager typedef struct Gia_Man_t_ Gia_Man_t; struct Gia_Man_t_ { char * pName; // name of the AIG int nRegs; // number of registers int nRegsAlloc; // number of allocated registers int nObjs; // number of objects int nObjsAlloc; // number of allocated objects Gia_Obj_t * pObjs; // the array of objects Vec_Int_t * vCis; // the vector of CIs (PIs + LOs) Vec_Int_t * vCos; // the vector of COs (POs + LIs) int * pHTable; // hash table int nHTable; // hash table size int fAddStrash; // performs additional structural hashing int * pRefs; // the reference count int * pNodeRefs; // node references Vec_Int_t * vLevels; // levels of the nodes int nLevels; // the mamixum level int nConstrs; // the number of constraints int nTravIds; // the current traversal ID int nFront; // frontier size int * pReprsOld; // representatives (for CIs and ANDs) Gia_Rpr_t * pReprs; // representatives (for CIs and ANDs) int * pNexts; // next nodes in the equivalence classes int * pIso; // pairs of structurally isomorphic nodes int nTerLoop; // the state where loop begins int nTerStates; // the total number of ternary states int * pFanData; // the database to store fanout information int nFansAlloc; // the size of fanout representation int * pMapping; // mapping for each node Vec_Int_t * vLutConfigs; // LUT configurations Abc_Cex_t * pCexComb; // combinational counter-example Abc_Cex_t * pCexSeq; // sequential counter-example int * pCopies; // intermediate copies Vec_Int_t * vTruths; // used for truth table computation Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc unsigned char* pSwitching; // switching activity for each object Gia_Plc_t * pPlacement; // placement of the objects int * pTravIds; // separate traversal ID representation int nTravIdsAlloc; // the number of trav IDs allocated Vec_Ptr_t * vNamesIn; // the input names Vec_Ptr_t * vNamesOut; // the output names Vec_Int_t * vUserPiIds; // numbers assigned to PIs by the user Vec_Int_t * vUserPoIds; // numbers assigned to POs by the user Vec_Int_t * vUserFfIds; // numbers assigned to FFs by the user Vec_Int_t * vCiNumsOrig; // original CI names Vec_Int_t * vCoNumsOrig; // original CO names Vec_Vec_t * vClockDoms; // clock domains Vec_Flt_t * vTiming; // arrival/required/slack void * pManTime; // the timing manager void * pLutLib; // LUT library }; typedef struct Emb_Par_t_ Emb_Par_t; struct Emb_Par_t_ { int nDims; // the number of dimension int nSols; // the number of solutions (typically, 2) int nIters; // the number of iterations of FORCE int fRefine; // use refinement by FORCE int fCluster; // use clustered representation int fDump; // dump Gnuplot file int fDumpLarge; // dump Gnuplot file for large benchmarks int fShowImage; // shows image if Gnuplot is installed int fVerbose; // verbose flag }; // frames parameters typedef struct Gia_ParFra_t_ Gia_ParFra_t; struct Gia_ParFra_t_ { int nFrames; // the number of frames to unroll int fInit; // initialize the timeframes int fVerbose; // enables verbose output }; // simulation parameters typedef struct Gia_ParSim_t_ Gia_ParSim_t; struct Gia_ParSim_t_ { // user-controlled parameters int nWords; // the number of machine words int nIters; // the number of timeframes int RandSeed; // seed to generate random numbers int TimeLimit; // time limit in seconds int fCheckMiter; // check if miter outputs are non-zero int fVerbose; // enables verbose output int iOutFail; // index of the failed output }; extern void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p ); extern int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars ); static inline int Gia_IntAbs( int n ) { return (n < 0)? -n : n; } static inline int Gia_Float2Int( float Val ) { union { int x; float y; } v; v.y = Val; return v.x; } static inline float Gia_Int2Float( int Num ) { union { int x; float y; } v; v.x = Num; return v.y; } static inline int Gia_Base2Log( unsigned n ) { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; } static inline int Gia_Base10Log( unsigned n ) { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; } static inline int Gia_Base16Log( unsigned n ) { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 16, r++ ); return r; } static inline char * Gia_UtilStrsav( char * s ) { return s ? strcpy(ABC_ALLOC(char, strlen(s)+1), s) : NULL; } static inline int Gia_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); } static inline int Gia_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); } static inline int Gia_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; } static inline void Gia_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); } static inline void Gia_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); } static inline unsigned Gia_InfoMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); } static inline unsigned Gia_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); } static inline int Gia_WordHasOneBit( unsigned uWord ) { return (uWord & (uWord-1)) == 0; } static inline int Gia_WordHasOnePair( unsigned uWord ) { return Gia_WordHasOneBit(uWord & (uWord>>1) & 0x55555555); } static inline int Gia_WordCountOnes( unsigned uWord ) { uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555); uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333); uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F); uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF); return (uWord & 0x0000FFFF) + (uWord>>16); } static inline int Gia_WordFindFirstBit( unsigned uWord ) { int i; for ( i = 0; i < 32; i++ ) if ( uWord & (1 << i) ) return i; return -1; } static inline int Gia_ManTruthIsConst0( unsigned * pIn, int nVars ) { int w; for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- ) if ( pIn[w] ) return 0; return 1; } static inline int Gia_ManTruthIsConst1( unsigned * pIn, int nVars ) { int w; for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- ) if ( pIn[w] != ~(unsigned)0 ) return 0; return 1; } static inline void Gia_ManTruthCopy( unsigned * pOut, unsigned * pIn, int nVars ) { int w; for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- ) pOut[w] = pIn[w]; } static inline void Gia_ManTruthClear( unsigned * pOut, int nVars ) { int w; for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- ) pOut[w] = 0; } static inline void Gia_ManTruthFill( unsigned * pOut, int nVars ) { int w; for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- ) pOut[w] = ~(unsigned)0; } static inline void Gia_ManTruthNot( unsigned * pOut, unsigned * pIn, int nVars ) { int w; for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- ) pOut[w] = ~pIn[w]; } static inline int Gia_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; } static inline int Gia_Lit2Var( int Lit ) { return Lit >> 1; } static inline int Gia_LitIsCompl( int Lit ) { return Lit & 1; } static inline int Gia_LitNot( int Lit ) { return Lit ^ 1; } static inline int Gia_LitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); } static inline int Gia_LitRegular( int Lit ) { return Lit & ~01; } static inline Gia_Obj_t * Gia_Regular( Gia_Obj_t * p ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); } static inline Gia_Obj_t * Gia_Not( Gia_Obj_t * p ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ 01); } static inline Gia_Obj_t * Gia_NotCond( Gia_Obj_t * p, int c ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); } static inline int Gia_IsComplement( Gia_Obj_t * p ) { return (int)((ABC_PTRUINT_T)(p) & 01); } static inline int Gia_ManCiNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCis); } static inline int Gia_ManCoNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCos); } static inline int Gia_ManPiNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCis) - p->nRegs; } static inline int Gia_ManPoNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCos) - p->nRegs; } static inline int Gia_ManRegNum( Gia_Man_t * p ) { return p->nRegs; } static inline int Gia_ManObjNum( Gia_Man_t * p ) { return p->nObjs; } static inline int Gia_ManAndNum( Gia_Man_t * p ) { return p->nObjs - Vec_IntSize(p->vCis) - Vec_IntSize(p->vCos) - 1; } static inline int Gia_ManCandNum( Gia_Man_t * p ) { return Gia_ManCiNum(p) + Gia_ManAndNum(p); } static inline int Gia_ManConstrNum( Gia_Man_t * p ) { return p->nConstrs; } static inline Gia_Obj_t * Gia_ManConst0( Gia_Man_t * p ) { return p->pObjs; } static inline Gia_Obj_t * Gia_ManConst1( Gia_Man_t * p ) { return Gia_Not(Gia_ManConst0(p)); } static inline Gia_Obj_t * Gia_ManObj( Gia_Man_t * p, int v ) { assert( v < p->nObjs ); return p->pObjs + v; } static inline Gia_Obj_t * Gia_ManCi( Gia_Man_t * p, int v ) { return Gia_ManObj( p, Vec_IntEntry(p->vCis,v) ); } static inline Gia_Obj_t * Gia_ManCo( Gia_Man_t * p, int v ) { return Gia_ManObj( p, Vec_IntEntry(p->vCos,v) ); } static inline Gia_Obj_t * Gia_ManPi( Gia_Man_t * p, int v ) { assert( v < Gia_ManPiNum(p) ); return Gia_ManCi( p, v ); } static inline Gia_Obj_t * Gia_ManPo( Gia_Man_t * p, int v ) { assert( v < Gia_ManPoNum(p) ); return Gia_ManCo( p, v ); } static inline Gia_Obj_t * Gia_ManRo( Gia_Man_t * p, int v ) { assert( v < Gia_ManRegNum(p) ); return Gia_ManCi( p, Gia_ManPiNum(p)+v ); } static inline Gia_Obj_t * Gia_ManRi( Gia_Man_t * p, int v ) { assert( v < Gia_ManRegNum(p) ); return Gia_ManCo( p, Gia_ManPoNum(p)+v ); } static inline int Gia_ObjIsTerm( Gia_Obj_t * pObj ) { return pObj->fTerm; } static inline int Gia_ObjIsAndOrConst0( Gia_Obj_t * pObj ) { return!pObj->fTerm; } static inline int Gia_ObjIsCi( Gia_Obj_t * pObj ) { return pObj->fTerm && pObj->iDiff0 == GIA_NONE; } static inline int Gia_ObjIsCo( Gia_Obj_t * pObj ) { return pObj->fTerm && pObj->iDiff0 != GIA_NONE; } static inline int Gia_ObjIsAnd( Gia_Obj_t * pObj ) { return!pObj->fTerm && pObj->iDiff0 != GIA_NONE; } static inline int Gia_ObjIsCand( Gia_Obj_t * pObj ) { return Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj); } static inline int Gia_ObjIsConst0( Gia_Obj_t * pObj ) { return pObj->iDiff0 == GIA_NONE && pObj->iDiff1 == GIA_NONE; } static inline int Gia_ManObjIsConst0( Gia_Man_t * p, Gia_Obj_t * pObj){ return pObj == p->pObjs; } static inline int Gia_ObjId( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pObjs <= pObj && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; } static inline int Gia_ObjCioId( Gia_Obj_t * pObj ) { assert( Gia_ObjIsTerm(pObj) ); return pObj->iDiff1; } static inline void Gia_ObjSetCioId( Gia_Obj_t * pObj, int v ) { assert( Gia_ObjIsTerm(pObj) ); pObj->iDiff1 = v; } static inline int Gia_ObjValue( Gia_Obj_t * pObj ) { return pObj->Value; } static inline void Gia_ObjSetValue( Gia_Obj_t * pObj, int i ) { pObj->Value = i; } static inline int Gia_ObjPhase( Gia_Obj_t * pObj ) { return pObj->fPhase; } static inline int Gia_ObjPhaseReal( Gia_Obj_t * pObj ) { return Gia_Regular(pObj)->fPhase ^ Gia_IsComplement(pObj); } static inline int Gia_ManIdToCioId( Gia_Man_t * p, int Id ) { return Gia_ObjCioId( Gia_ManObj(p, Id) ); } static inline int Gia_ManCiIdToId( Gia_Man_t * p, int CiId ) { return Gia_ObjId( p, Gia_ManCi(p, CiId) ); } static inline int Gia_ManCoIdToId( Gia_Man_t * p, int CoId ) { return Gia_ObjId( p, Gia_ManCo(p, CoId) ); } static inline int Gia_ObjIsPi( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjIsCi(pObj) && Gia_ObjCioId(pObj) < Gia_ManPiNum(p); } static inline int Gia_ObjIsPo( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjIsCo(pObj) && Gia_ObjCioId(pObj) < Gia_ManPoNum(p); } static inline int Gia_ObjIsRo( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjIsCi(pObj) && Gia_ObjCioId(pObj) >= Gia_ManPiNum(p); } static inline int Gia_ObjIsRi( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjIsCo(pObj) && Gia_ObjCioId(pObj) >= Gia_ManPoNum(p); } static inline Gia_Obj_t * Gia_ObjRoToRi( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsRo(p, pObj) ); return Gia_ManCo(p, Gia_ManCoNum(p) - Gia_ManCiNum(p) + Gia_ObjCioId(pObj)); } static inline Gia_Obj_t * Gia_ObjRiToRo( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsRi(p, pObj) ); return Gia_ManCi(p, Gia_ManCiNum(p) - Gia_ManCoNum(p) + Gia_ObjCioId(pObj)); } static inline int Gia_ObjDiff0( Gia_Obj_t * pObj ) { return pObj->iDiff0; } static inline int Gia_ObjDiff1( Gia_Obj_t * pObj ) { return pObj->iDiff1; } static inline int Gia_ObjFaninC0( Gia_Obj_t * pObj ) { return pObj->fCompl0; } static inline int Gia_ObjFaninC1( Gia_Obj_t * pObj ) { return pObj->fCompl1; } static inline Gia_Obj_t * Gia_ObjFanin0( Gia_Obj_t * pObj ) { return pObj - pObj->iDiff0; } static inline Gia_Obj_t * Gia_ObjFanin1( Gia_Obj_t * pObj ) { return pObj - pObj->iDiff1; } static inline Gia_Obj_t * Gia_ObjChild0( Gia_Obj_t * pObj ) { return Gia_NotCond( Gia_ObjFanin0(pObj), Gia_ObjFaninC0(pObj) ); } static inline Gia_Obj_t * Gia_ObjChild1( Gia_Obj_t * pObj ) { return Gia_NotCond( Gia_ObjFanin1(pObj), Gia_ObjFaninC1(pObj) ); } static inline int Gia_ObjFaninId0( Gia_Obj_t * pObj, int ObjId ) { return ObjId - pObj->iDiff0; } static inline int Gia_ObjFaninId1( Gia_Obj_t * pObj, int ObjId ) { return ObjId - pObj->iDiff1; } static inline int Gia_ObjFaninId0p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFaninId0( pObj, Gia_ObjId(p, pObj) ); } static inline int Gia_ObjFaninId1p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFaninId1( pObj, Gia_ObjId(p, pObj) ); } static inline int Gia_ObjFaninLit0( Gia_Obj_t * pObj, int ObjId ) { return Gia_Var2Lit( Gia_ObjFaninId0(pObj, ObjId), Gia_ObjFaninC0(pObj) ); } static inline int Gia_ObjFaninLit1( Gia_Obj_t * pObj, int ObjId ) { return Gia_Var2Lit( Gia_ObjFaninId1(pObj, ObjId), Gia_ObjFaninC1(pObj) ); } static inline int Gia_ObjFaninLit0p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Gia_Var2Lit( Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninC0(pObj) ); } static inline int Gia_ObjFaninLit1p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Gia_Var2Lit( Gia_ObjFaninId1p(p, pObj), Gia_ObjFaninC1(pObj) ); } static inline void Gia_ObjFlipFaninC0( Gia_Obj_t * pObj ) { assert( Gia_ObjIsCo(pObj) ); pObj->fCompl0 ^= 1; } static inline int Gia_ObjWhatFanin( Gia_Obj_t * pObj, Gia_Obj_t * pFanin ) { return Gia_ObjFanin0(pObj) == pFanin ? 0 : (Gia_ObjFanin1(pObj) == pFanin ? 1 : -1); } static inline int Gia_ObjFanin0Copy( Gia_Obj_t * pObj ) { return Gia_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); } static inline int Gia_ObjFanin1Copy( Gia_Obj_t * pObj ) { return Gia_LitNotCond( Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) ); } static inline int Gia_ObjCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)]; } static inline void Gia_ObjSetCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit ) { p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)] = iLit; } static inline int Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Gia_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj)); } static inline int Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Gia_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj)); } static inline Gia_Obj_t * Gia_ObjFromLit( Gia_Man_t * p, int iLit ) { return Gia_NotCond( Gia_ManObj(p, Gia_Lit2Var(iLit)), Gia_LitIsCompl(iLit) ); } static inline int Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); } static inline int Gia_ObjPhaseRealLit( Gia_Man_t * p, int iLit ) { return Gia_ObjPhaseReal( Gia_ObjFromLit(p, iLit) ); } static inline int Gia_ObjLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntGetEntry(p->vLevels, Gia_ObjId(p,pObj)); } static inline int Gia_ObjLevelId( Gia_Man_t * p, int Id ) { return Vec_IntGetEntry(p->vLevels, Id); } static inline void Gia_ObjSetLevel( Gia_Man_t * p, Gia_Obj_t * pObj, int l ) { Vec_IntSetEntry(p->vLevels, Gia_ObjId(p,pObj), l); } static inline void Gia_ObjSetCoLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsCo(pObj) ); Gia_ObjSetLevel( p, pObj, Gia_ObjLevel(p,Gia_ObjFanin0(pObj)) ); } static inline void Gia_ObjSetAndLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsAnd(pObj) ); Gia_ObjSetLevel( p, pObj, 1+ABC_MAX(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))) ); } static inline int Gia_ObjRefs( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)]; } static inline int Gia_ObjRefsId( Gia_Man_t * p, int Id ) { assert( p->pRefs); return p->pRefs[Id]; } static inline int Gia_ObjRefInc( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)]++; } static inline int Gia_ObjRefDec( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return --p->pRefs[Gia_ObjId(p, pObj)]; } static inline void Gia_ObjRefFanin0Inc(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefInc(p, Gia_ObjFanin0(pObj)); } static inline void Gia_ObjRefFanin1Inc(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefInc(p, Gia_ObjFanin1(pObj)); } static inline void Gia_ObjRefFanin0Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin0(pObj)); } static inline void Gia_ObjRefFanin1Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin1(pObj)); } static inline int Gia_ObjNodeRefs( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pNodeRefs); return p->pNodeRefs[Gia_ObjId(p, pObj)]; } static inline int Gia_ObjNodeRefsId( Gia_Man_t * p, int Id ) { assert( p->pNodeRefs); return p->pNodeRefs[Id]; } static inline int Gia_ObjNodeRefIncId( Gia_Man_t * p, int Id ) { assert( p->pNodeRefs); return p->pNodeRefs[Id]++; } static inline int Gia_ObjNodeRefDecId( Gia_Man_t * p, int Id ) { assert( p->pNodeRefs); return --p->pNodeRefs[Id]; } static inline int Gia_ObjNodeRefInc( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pNodeRefs); return p->pNodeRefs[Gia_ObjId(p, pObj)]++; } static inline int Gia_ObjNodeRefDec( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pNodeRefs); return --p->pNodeRefs[Gia_ObjId(p, pObj)]; } static inline void Gia_ObjSetTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds; } static inline void Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds - 1; } static inline int Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds); } static inline int Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds - 1); } static inline void Gia_ObjSetTravIdCurrentId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); p->pTravIds[Id] = p->nTravIds; } static inline int Gia_ObjIsTravIdCurrentId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); return (p->pTravIds[Id] == p->nTravIds); } static inline void Gia_ManTimeClean( Gia_Man_t * p ) { int i; assert( p->vTiming != NULL ); Vec_FltFill(p->vTiming, 3*Gia_ManObjNum(p), 0); for ( i = 0; i < Gia_ManObjNum(p); i++ ) Vec_FltWriteEntry( p->vTiming, 3*i+1, (float)(ABC_INFINITY) ); } static inline void Gia_ManTimeStart( Gia_Man_t * p ) { assert( p->vTiming == NULL ); p->vTiming = Vec_FltAlloc(0); Gia_ManTimeClean( p ); } static inline void Gia_ManTimeStop( Gia_Man_t * p ) { assert( p->vTiming != NULL ); Vec_FltFreeP(&p->vTiming); } static inline float Gia_ObjTimeArrival( Gia_Man_t * p, int Id ) { return Vec_FltEntry(p->vTiming, 3*Id+0); } static inline float Gia_ObjTimeRequired( Gia_Man_t * p, int Id ) { return Vec_FltEntry(p->vTiming, 3*Id+1); } static inline float Gia_ObjTimeSlack( Gia_Man_t * p, int Id ) { return Vec_FltEntry(p->vTiming, 3*Id+2); } static inline float Gia_ObjTimeArrivalObj( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjTimeArrival( p, Gia_ObjId(p, pObj) ); } static inline float Gia_ObjTimeRequiredObj( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjTimeRequired( p, Gia_ObjId(p, pObj) ); } static inline float Gia_ObjTimeSlackObj( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjTimeSlack( p, Gia_ObjId(p, pObj) ); } static inline void Gia_ObjSetTimeArrival( Gia_Man_t * p, int Id, float t ) { Vec_FltWriteEntry( p->vTiming, 3*Id+0, t ); } static inline void Gia_ObjSetTimeRequired( Gia_Man_t * p, int Id, float t ) { Vec_FltWriteEntry( p->vTiming, 3*Id+1, t ); } static inline void Gia_ObjSetTimeSlack( Gia_Man_t * p, int Id, float t ) { Vec_FltWriteEntry( p->vTiming, 3*Id+2, t ); } static inline void Gia_ObjSetTimeArrivalObj( Gia_Man_t * p, Gia_Obj_t * pObj, float t ) { Gia_ObjSetTimeArrival( p, Gia_ObjId(p, pObj), t ); } static inline void Gia_ObjSetTimeRequiredObj( Gia_Man_t * p, Gia_Obj_t * pObj, float t ) { Gia_ObjSetTimeRequired( p, Gia_ObjId(p, pObj), t ); } static inline void Gia_ObjSetTimeSlackObj( Gia_Man_t * p, Gia_Obj_t * pObj, float t ) { Gia_ObjSetTimeSlack( p, Gia_ObjId(p, pObj), t ); } // AIG construction extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout ); static inline Gia_Obj_t * Gia_ManAppendObj( Gia_Man_t * p ) { if ( p->nObjs == p->nObjsAlloc ) { // printf("Reallocing %d.\n", 2 * p->nObjsAlloc ); assert( p->nObjsAlloc > 0 ); p->pObjs = ABC_REALLOC( Gia_Obj_t, p->pObjs, 2 * p->nObjsAlloc ); memset( p->pObjs + p->nObjsAlloc, 0, sizeof(Gia_Obj_t) * p->nObjsAlloc ); p->nObjsAlloc *= 2; } return Gia_ManObj( p, p->nObjs++ ); } static inline int Gia_ManAppendCi( Gia_Man_t * p ) { Gia_Obj_t * pObj = Gia_ManAppendObj( p ); pObj->fTerm = 1; pObj->iDiff0 = GIA_NONE; pObj->iDiff1 = Vec_IntSize( p->vCis ); Vec_IntPush( p->vCis, Gia_ObjId(p, pObj) ); return Gia_ObjId( p, pObj ) << 1; } static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 ) { Gia_Obj_t * pObj = Gia_ManAppendObj( p ); assert( iLit0 != iLit1 ); if ( iLit0 < iLit1 ) { pObj->iDiff0 = Gia_ObjId(p, pObj) - Gia_Lit2Var(iLit0); pObj->fCompl0 = Gia_LitIsCompl(iLit0); pObj->iDiff1 = Gia_ObjId(p, pObj) - Gia_Lit2Var(iLit1); pObj->fCompl1 = Gia_LitIsCompl(iLit1); } else { pObj->iDiff1 = Gia_ObjId(p, pObj) - Gia_Lit2Var(iLit0); pObj->fCompl1 = Gia_LitIsCompl(iLit0); pObj->iDiff0 = Gia_ObjId(p, pObj) - Gia_Lit2Var(iLit1); pObj->fCompl0 = Gia_LitIsCompl(iLit1); } if ( p->pFanData ) { Gia_ObjAddFanout( p, Gia_ObjFanin0(pObj), pObj ); Gia_ObjAddFanout( p, Gia_ObjFanin1(pObj), pObj ); } return Gia_ObjId( p, pObj ) << 1; } static inline int Gia_ManAppendCo( Gia_Man_t * p, int iLit0 ) { Gia_Obj_t * pObj = Gia_ManAppendObj( p ); pObj->fTerm = 1; pObj->iDiff0 = Gia_ObjId(p, pObj) - Gia_Lit2Var(iLit0); pObj->fCompl0 = Gia_LitIsCompl(iLit0); pObj->iDiff1 = Vec_IntSize( p->vCos ); Vec_IntPush( p->vCos, Gia_ObjId(p, pObj) ); if ( p->pFanData ) Gia_ObjAddFanout( p, Gia_ObjFanin0(pObj), pObj ); return Gia_ObjId( p, pObj ) << 1; } static inline int Gia_ManAppendMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 ) { int iTemp0 = Gia_ManAppendAnd( p, Gia_LitNot(iCtrl), iData0 ); int iTemp1 = Gia_ManAppendAnd( p, iCtrl, iData1 ); return Gia_LitNotCond( Gia_ManAppendAnd( p, Gia_LitNot(iTemp0), Gia_LitNot(iTemp1) ), 1 ); } #define GIA_ZER 1 #define GIA_ONE 2 #define GIA_UND 3 static inline int Gia_XsimNotCond( int Value, int fCompl ) { if ( Value == GIA_UND ) return GIA_UND; if ( Value == GIA_ZER + fCompl ) return GIA_ZER; return GIA_ONE; } static inline int Gia_XsimAndCond( int Value0, int fCompl0, int Value1, int fCompl1 ) { if ( Value0 == GIA_ZER + fCompl0 || Value1 == GIA_ZER + fCompl1 ) return GIA_ZER; if ( Value0 == GIA_UND || Value1 == GIA_UND ) return GIA_UND; return GIA_ONE; } static inline Gia_Obj_t * Gia_ObjReprObj( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr == GIA_VOID ? NULL : Gia_ManObj( p, p->pReprs[Id].iRepr ); } static inline int Gia_ObjRepr( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr; } static inline void Gia_ObjSetRepr( Gia_Man_t * p, int Id, int Num ) { assert( Num == GIA_VOID || Num < Id ); p->pReprs[Id].iRepr = Num; } static inline void Gia_ObjUnsetRepr( Gia_Man_t * p, int Id ) { p->pReprs[Id].iRepr = GIA_VOID; } static inline int Gia_ObjHasRepr( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr != GIA_VOID; } static inline int Gia_ObjProved( Gia_Man_t * p, int Id ) { return p->pReprs[Id].fProved; } static inline void Gia_ObjSetProved( Gia_Man_t * p, int Id ) { p->pReprs[Id].fProved = 1; } static inline void Gia_ObjUnsetProved( Gia_Man_t * p, int Id ) { p->pReprs[Id].fProved = 0; } static inline int Gia_ObjFailed( Gia_Man_t * p, int Id ) { return p->pReprs[Id].fFailed; } static inline void Gia_ObjSetFailed( Gia_Man_t * p, int Id ) { p->pReprs[Id].fFailed = 1; } static inline int Gia_ObjColor( Gia_Man_t * p, int Id, int c ) { return c? p->pReprs[Id].fColorB : p->pReprs[Id].fColorA; } static inline int Gia_ObjColors( Gia_Man_t * p, int Id ) { return p->pReprs[Id].fColorB * 2 + p->pReprs[Id].fColorA; } static inline void Gia_ObjSetColor( Gia_Man_t * p, int Id, int c ) { if (c) p->pReprs[Id].fColorB = 1; else p->pReprs[Id].fColorA = 1; } static inline void Gia_ObjSetColors( Gia_Man_t * p, int Id ) { p->pReprs[Id].fColorB = p->pReprs[Id].fColorA = 1; } static inline int Gia_ObjVisitColor( Gia_Man_t * p, int Id, int c ) { int x; if (c) { x = p->pReprs[Id].fColorB; p->pReprs[Id].fColorB = 1; } else { x = p->pReprs[Id].fColorA; p->pReprs[Id].fColorA = 1; } return x; } static inline int Gia_ObjDiffColors( Gia_Man_t * p, int i, int j ) { return (p->pReprs[i].fColorA ^ p->pReprs[j].fColorA) && (p->pReprs[i].fColorB ^ p->pReprs[j].fColorB); } static inline int Gia_ObjDiffColors2( Gia_Man_t * p, int i, int j ) { return (p->pReprs[i].fColorA ^ p->pReprs[j].fColorA) || (p->pReprs[i].fColorB ^ p->pReprs[j].fColorB); } static inline Gia_Obj_t * Gia_ObjNextObj( Gia_Man_t * p, int Id ) { return p->pNexts[Id] == 0 ? NULL : Gia_ManObj( p, p->pNexts[Id] );} static inline int Gia_ObjNext( Gia_Man_t * p, int Id ) { return p->pNexts[Id]; } static inline void Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num ) { p->pNexts[Id] = Num; } static inline int Gia_ObjIsConst( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == 0; } static inline int Gia_ObjIsUsed( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) != GIA_VOID && Gia_ObjNext(p, Id) > 0; } static inline int Gia_ObjIsHead( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) > 0; } static inline int Gia_ObjIsNone( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) == 0; } static inline int Gia_ObjIsTail( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) == 0; } static inline int Gia_ObjIsClass( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) || Gia_ObjNext(p, Id) > 0; } static inline int Gia_ObjHasSameRepr( Gia_Man_t * p, int i, int k ) { assert( k ); return i? (Gia_ObjRepr(p, i) == Gia_ObjRepr(p, k) && Gia_ObjRepr(p, i) != GIA_VOID) : Gia_ObjRepr(p, k) == 0; } static inline int Gia_ObjIsFailedPair( Gia_Man_t * p, int i, int k ) { assert( k ); return i? (Gia_ObjFailed(p, i) || Gia_ObjFailed(p, k)) : Gia_ObjFailed(p, k); } static inline int Gia_ClassIsPair( Gia_Man_t * p, int i ) { assert( Gia_ObjIsHead(p, i) ); assert( Gia_ObjNext(p, i) ); return Gia_ObjNext(p, Gia_ObjNext(p, i)) == 0; } static inline void Gia_ClassUndoPair( Gia_Man_t * p, int i ) { assert( Gia_ClassIsPair(p,i) ); Gia_ObjSetRepr(p, Gia_ObjNext(p, i), GIA_VOID); Gia_ObjSetNext(p, i, 0); } #define Gia_ManForEachConst( p, i ) \ for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsConst(p, i) ) {} else #define Gia_ManForEachClass( p, i ) \ for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsHead(p, i) ) {} else #define Gia_ManForEachClassReverse( p, i ) \ for ( i = Gia_ManObjNum(p) - 1; i > 0; i-- ) if ( !Gia_ObjIsHead(p, i) ) {} else #define Gia_ClassForEachObj( p, i, iObj ) \ for ( assert(Gia_ObjIsHead(p, i)), iObj = i; iObj; iObj = Gia_ObjNext(p, iObj) ) #define Gia_ClassForEachObj1( p, i, iObj ) \ for ( assert(Gia_ObjIsHead(p, i)), iObj = Gia_ObjNext(p, i); iObj; iObj = Gia_ObjNext(p, iObj) ) static inline int Gia_ObjIsLut( Gia_Man_t * p, int Id ) { return p->pMapping[Id] != 0; } static inline int Gia_ObjLutSize( Gia_Man_t * p, int Id ) { return p->pMapping[p->pMapping[Id]]; } static inline int * Gia_ObjLutFanins( Gia_Man_t * p, int Id ) { return p->pMapping + p->pMapping[Id] + 1; } static inline int Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i ) { return Gia_ObjLutFanins(p, Id)[i]; } #define Gia_ManForEachLut( p, i ) \ for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsLut(p, i) ) {} else #define Gia_LutForEachFanin( p, i, iFan, k ) \ for ( k = 0; k < Gia_ObjLutSize(p,i) && ((iFan = Gia_ObjLutFanins(p,i)[k]),1); k++ ) #define Gia_LutForEachFaninObj( p, i, pFanin, k ) \ for ( k = 0; k < Gia_ObjLutSize(p,i) && ((pFanin = Gia_ManObj(p, Gia_ObjLutFanins(p,i)[k])),1); k++ ) //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// #define Gia_ManForEachObj( p, pObj, i ) \ for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) #define Gia_ManForEachObj1( p, pObj, i ) \ for ( i = 1; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) #define Gia_ManForEachObjVec( vVec, p, pObj, i ) \ for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Vec_IntEntry(vVec,i))); i++ ) #define Gia_ManForEachObjVecLit( vVec, p, pObj, fCompl, i ) \ for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Gia_Lit2Var(Vec_IntEntry(vVec,i)))) && (((fCompl) = Gia_LitIsCompl(Vec_IntEntry(vVec,i))),1); i++ ) #define Gia_ManForEachObjReverse( p, pObj, i ) \ for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- ) #define Gia_ManForEachAnd( p, pObj, i ) \ for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsAnd(pObj) ) {} else #define Gia_ManForEachAndReverse( p, pObj, i ) \ for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- ) if ( !Gia_ObjIsAnd(pObj) ) {} else #define Gia_ManForEachCi( p, pObj, i ) \ for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((pObj) = Gia_ManCi(p, i)); i++ ) #define Gia_ManForEachCo( p, pObj, i ) \ for ( i = 0; (i < Vec_IntSize(p->vCos)) && ((pObj) = Gia_ManCo(p, i)); i++ ) #define Gia_ManForEachCoReverse( p, pObj, i ) \ for ( i = Vec_IntSize(p->vCos) - 1; (i >= 0) && ((pObj) = Gia_ManCo(p, i)); i-- ) #define Gia_ManForEachCoDriver( p, pObj, i ) \ for ( i = 0; (i < Vec_IntSize(p->vCos)) && ((pObj) = Gia_ObjFanin0(Gia_ManCo(p, i))); i++ ) #define Gia_ManForEachPi( p, pObj, i ) \ for ( i = 0; (i < Gia_ManPiNum(p)) && ((pObj) = Gia_ManCi(p, i)); i++ ) #define Gia_ManForEachPo( p, pObj, i ) \ for ( i = 0; (i < Gia_ManPoNum(p)) && ((pObj) = Gia_ManCo(p, i)); i++ ) #define Gia_ManForEachRo( p, pObj, i ) \ for ( i = 0; (i < Gia_ManRegNum(p)) && ((pObj) = Gia_ManCi(p, Gia_ManPiNum(p)+i)); i++ ) #define Gia_ManForEachRi( p, pObj, i ) \ for ( i = 0; (i < Gia_ManRegNum(p)) && ((pObj) = Gia_ManCo(p, Gia_ManPoNum(p)+i)); i++ ) #define Gia_ManForEachRiRo( p, pObjRi, pObjRo, i ) \ for ( i = 0; (i < Gia_ManRegNum(p)) && ((pObjRi) = Gia_ManCo(p, Gia_ManPoNum(p)+i)) && ((pObjRo) = Gia_ManCi(p, Gia_ManPiNum(p)+i)); i++ ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// /*=== giaAbs.c ===========================================================*/ extern void Gia_ManCexAbstractionStart( Gia_Man_t * p, Gia_ParAbs_t * pPars ); Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia ); int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose ); extern int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int fVerbose, int * piFrame ); extern int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars ); /*=== giaAiger.c ===========================================================*/ extern int Gia_FileSize( char * pFileName ); extern Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck ); extern Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck ); extern void Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact ); extern void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits ); /*=== giaBidec.c ===========================================================*/ extern unsigned * Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vTruth, Vec_Int_t * vVisited ); extern Gia_Man_t * Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose ); /*=== giaCsatOld.c ============================================================*/ extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); /*=== giaCsat.c ============================================================*/ extern Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); /*=== giaCTas.c ============================================================*/ extern Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); /*=== giaCof.c =============================================================*/ extern void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes ); extern Gia_Man_t * Gia_ManDupCof( Gia_Man_t * p, int iVar ); extern Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose ); extern Gia_Man_t * Gia_ManDupCofAll( Gia_Man_t * p, int nFanLim, int fVerbose ); /*=== giaDfs.c ============================================================*/ extern void Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vSupp ); extern void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes ); extern Vec_Int_t * Gia_ManCollectNodesCis( Gia_Man_t * p, int * pNodes, int nNodes ); extern int Gia_ManSuppSize( Gia_Man_t * p, int * pNodes, int nNodes ); extern int Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes ); extern Vec_Vec_t * Gia_ManLevelize( Gia_Man_t * p ); extern Vec_Int_t * Gia_ManOrderReverse( Gia_Man_t * p ); /*=== giaDup.c ============================================================*/ extern Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupOrderDfsChoices( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupOutputGroup( Gia_Man_t * p, int iOutStart, int iOutStop ); extern Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState ); extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass ); extern Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes ); extern Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupDfsSkip( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pObj ); extern Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits ); extern Gia_Man_t * Gia_ManDupNormalized( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos ); extern Gia_Man_t * Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 ); extern Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits ); extern Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose ); extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int fDualOut, int fSeq, int fVerbose ); extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias ); extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes ); extern Gia_Man_t * Gia_ManDupAbstraction( Gia_Man_t * p, Vec_Int_t * vFlopClasses ); /*=== giaEnable.c ==========================================================*/ extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose ); extern Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose ); extern Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p ); /*=== giaEquiv.c ==========================================================*/ extern void Gia_ManEquivFixOutputPairs( Gia_Man_t * p ); extern int Gia_ManCheckTopoOrder( Gia_Man_t * p ); extern int * Gia_ManDeriveNexts( Gia_Man_t * p ); extern void Gia_ManDeriveReprs( Gia_Man_t * p ); extern int Gia_ManEquivCountLits( Gia_Man_t * p ); extern int Gia_ManEquivCountLitsAll( Gia_Man_t * p ); extern int Gia_ManEquivCountClasses( Gia_Man_t * p ); extern void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter ); extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ); extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose ); extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs ); extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ); extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fReduce, int fSkipSome, int fVerbose ); extern Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames, int fDualOut ); extern Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Abc_Cex_t * pInit, int nFramesMax, int * pnFrames, int fDualOut, int nMinOutputs ); extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose ); extern void Gia_ManEquivImprove( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots ); extern int Gia_ManCountChoiceNodes( Gia_Man_t * p ); extern int Gia_ManCountChoices( Gia_Man_t * p ); extern int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * pName2, int fLatchA, int fLatchB ); extern int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName2 ); extern void Gia_ManFilterEquivsUsingLatches( Gia_Man_t * pGia, int fFlopsOnly, int fFlopsWith ); /*=== giaFanout.c =========================================================*/ extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout ); extern void Gia_ObjRemoveFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout ); extern void Gia_ManFanoutStart( Gia_Man_t * p ); extern void Gia_ManFanoutStop( Gia_Man_t * p ); /*=== giaForce.c =========================================================*/ extern void For_ManExperiment( Gia_Man_t * pGia, int nIters, int fClustered, int fVerbose ); /*=== giaFrames.c =========================================================*/ extern void Gia_ManFraSetDefaultParams( Gia_ParFra_t * p ); extern Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars ); /*=== giaFront.c ==========================================================*/ extern Gia_Man_t * Gia_ManFront( Gia_Man_t * p ); extern void Gia_ManFrontTest( Gia_Man_t * p ); /*=== giaHash.c ===========================================================*/ extern void Gia_ManHashAlloc( Gia_Man_t * p ); extern void Gia_ManHashStart( Gia_Man_t * p ); extern void Gia_ManHashStop( Gia_Man_t * p ); extern int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 ); extern int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 ); extern int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 ); extern int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 ); extern Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash ); extern void Gia_ManHashProfile( Gia_Man_t * p ); extern int Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 ); /*=== giaIf.c ===========================================================*/ extern void Gia_ManPrintNpnClasses( Gia_Man_t * p ); /*=== giaLogic.c ===========================================================*/ extern void Gia_ManTestDistance( Gia_Man_t * p ); extern void Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pPars ); /*=== giaMan.c ===========================================================*/ extern Gia_Man_t * Gia_ManStart( int nObjsMax ); extern void Gia_ManStop( Gia_Man_t * p ); extern void Gia_ManStopP( Gia_Man_t ** p ); extern void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch ); extern void Gia_ManPrintStatsShort( Gia_Man_t * p ); extern void Gia_ManPrintMiterStatus( Gia_Man_t * p ); extern void Gia_ManSetRegNum( Gia_Man_t * p, int nRegs ); extern void Gia_ManReportImprovement( Gia_Man_t * p, Gia_Man_t * pNew ); /*=== giaMap.c ===========================================================*/ extern void Gia_ManPrintMappingStats( Gia_Man_t * p ); extern int Gia_ManLutFaninCount( Gia_Man_t * p ); extern int Gia_ManLutSizeMax( Gia_Man_t * p ); extern int Gia_ManLutNum( Gia_Man_t * p ); extern int Gia_ManLutLevel( Gia_Man_t * p ); /*=== giaMem.c ===========================================================*/ extern Gia_MmFixed_t * Gia_MmFixedStart( int nEntrySize, int nEntriesMax ); extern void Gia_MmFixedStop( Gia_MmFixed_t * p, int fVerbose ); extern char * Gia_MmFixedEntryFetch( Gia_MmFixed_t * p ); extern void Gia_MmFixedEntryRecycle( Gia_MmFixed_t * p, char * pEntry ); extern void Gia_MmFixedRestart( Gia_MmFixed_t * p ); extern int Gia_MmFixedReadMemUsage( Gia_MmFixed_t * p ); extern int Gia_MmFixedReadMaxEntriesUsed( Gia_MmFixed_t * p ); extern Gia_MmFlex_t * Gia_MmFlexStart(); extern void Gia_MmFlexStop( Gia_MmFlex_t * p, int fVerbose ); extern char * Gia_MmFlexEntryFetch( Gia_MmFlex_t * p, int nBytes ); extern void Gia_MmFlexRestart( Gia_MmFlex_t * p ); extern int Gia_MmFlexReadMemUsage( Gia_MmFlex_t * p ); extern Gia_MmStep_t * Gia_MmStepStart( int nSteps ); extern void Gia_MmStepStop( Gia_MmStep_t * p, int fVerbose ); extern char * Gia_MmStepEntryFetch( Gia_MmStep_t * p, int nBytes ); extern void Gia_MmStepEntryRecycle( Gia_MmStep_t * p, char * pEntry, int nBytes ); extern int Gia_MmStepReadMemUsage( Gia_MmStep_t * p ); /*=== giaPat.c ===========================================================*/ extern void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit ); /*=== giaReparam.c ===========================================================*/ extern Gia_Man_t * Gia_ManReparm( Gia_Man_t * p, int fVerbose ); /*=== giaRetime.c ===========================================================*/ extern Gia_Man_t * Gia_ManRetimeForward( Gia_Man_t * p, int nMaxIters, int fVerbose ); /*=== giaSat.c ============================================================*/ extern int Sat_ManTest( Gia_Man_t * pGia, Gia_Obj_t * pObj, int nConfsMax ); /*=== giaScl.c ============================================================*/ extern int Gia_ManSeqMarkUsed( Gia_Man_t * p ); extern int Gia_ManCombMarkUsed( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManCleanup( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManSeqCleanup( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManSeqStructSweep( Gia_Man_t * p, int fConst, int fEquiv, int fVerbose ); /*=== giaShrink.c ===========================================================*/ extern Gia_Man_t * Gia_ManPerformMapShrink( Gia_Man_t * p, int fKeepLevel, int fVerbose ); /*=== giaSort.c ============================================================*/ extern int * Gia_SortFloats( float * pArray, int * pPerm, int nSize ); /*=== giaSim.c ============================================================*/ extern int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars ); /*=== giaSpeedup.c ============================================================*/ extern float Gia_ManDelayTraceLut( Gia_Man_t * p ); extern float Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose ); extern Gia_Man_t * Gia_ManSpeedup( Gia_Man_t * p, int Percentage, int Degree, int fVerbose, int fVeryVerbose ); /*=== giaSwitch.c ============================================================*/ extern float Gia_ManEvaluateSwitching( Gia_Man_t * p ); extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne ); /*=== giaTsim.c ============================================================*/ extern Gia_Man_t * Gia_ManReduceConst( Gia_Man_t * pAig, int fVerbose ); /*=== giaUtil.c ===========================================================*/ extern unsigned Gia_ManRandom( int fReset ); extern void Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop ); extern unsigned int Gia_PrimeCudd( unsigned int p ); extern char * Gia_TimeStamp(); extern char * Gia_FileNameGenericAppend( char * pBase, char * pSuffix ); extern void Gia_ManIncrementTravId( Gia_Man_t * p ); extern void Gia_ManSetMark0( Gia_Man_t * p ); extern void Gia_ManCleanMark0( Gia_Man_t * p ); extern void Gia_ManCheckMark0( Gia_Man_t * p ); extern void Gia_ManSetMark1( Gia_Man_t * p ); extern void Gia_ManCleanMark1( Gia_Man_t * p ); extern void Gia_ManCheckMark1( Gia_Man_t * p ); extern void Gia_ManCleanValue( Gia_Man_t * p ); extern void Gia_ManCleanLevels( Gia_Man_t * p, int Size ); extern void Gia_ManCleanTruth( Gia_Man_t * p ); extern void Gia_ManFillValue( Gia_Man_t * p ); extern void Gia_ObjSetPhase( Gia_Obj_t * pObj ); extern void Gia_ManSetPhase( Gia_Man_t * p ); extern void Gia_ManSetPhase1( Gia_Man_t * p ); extern void Gia_ManCleanPhase( Gia_Man_t * p ); extern int Gia_ManLevelNum( Gia_Man_t * p ); extern void Gia_ManSetRefs( Gia_Man_t * p ); extern int * Gia_ManCreateMuxRefs( Gia_Man_t * p ); extern void Gia_ManCreateRefs( Gia_Man_t * p ); extern int Gia_ManCrossCut( Gia_Man_t * p ); extern int Gia_ManIsNormalized( Gia_Man_t * p ); extern Vec_Int_t * Gia_ManCollectPoIds( Gia_Man_t * p ); extern int Gia_ObjIsMuxType( Gia_Obj_t * pNode ); extern int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ppFan0, Gia_Obj_t ** ppFan1 ); extern Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE ); extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode ); extern int Gia_ManHasChoices( Gia_Man_t * p ); extern int Gia_ManHasDangling( Gia_Man_t * p ); extern Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p ); extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj ); extern int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ); extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs ); /*=== giaCTas.c ===========================================================*/ typedef struct Tas_Man_t_ Tas_Man_t; extern Tas_Man_t * Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit ); extern void Tas_ManStop( Tas_Man_t * p ); extern Vec_Int_t * Tas_ReadModel( Tas_Man_t * p ); extern void Tas_ManSatPrintStats( Tas_Man_t * p ); extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ); extern int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs ); ABC_NAMESPACE_HEADER_END #endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////