1 /**CFile****************************************************************
2 Copyright (c) The Regents of the University of California. All rights reserved.
3
4 Permission is hereby granted, without written agreement and without license or
5 royalty fees, to use, copy, modify, and distribute this software and its
6 documentation for any purpose, provided that the above copyright notice and
7 the following two paragraphs appear in all copies of this software.
8
9 IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
10 DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF
11 THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
12 CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
13
14 THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING,
15 BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
16 A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS,
17 AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE,
18 SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
19
20
21 FileName [kit.h]
22
23 SystemName [ABC: Logic synthesis and verification system.]
24
25 PackageName [Computation kit.]
26
27 Synopsis [External declarations.]
28
29 Author [Alan Mishchenko]
30
31 Affiliation [UC Berkeley]
32
33 Date [Ver. 1.0. Started - Dec 6, 2006.]
34
35 Revision [$Id: kit.h,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
36
37 ***********************************************************************/
38
39 #ifndef __KIT_H__
40 #define __KIT_H__
41
42 #ifdef __cplusplus
43 extern "C" {
44 #endif
45
46 ////////////////////////////////////////////////////////////////////////
47 /// INCLUDES ///
48 ////////////////////////////////////////////////////////////////////////
49
50 #include <stdio.h>
51 #include <stdlib.h>
52 #include <string.h>
53 #include <assert.h>
54 #include <time.h>
55 #include "vec.h"
56 //#include "extra.h"
57 //#include "cloud.h"
58
59 ////////////////////////////////////////////////////////////////////////
60 /// PARAMETERS ///
61 ////////////////////////////////////////////////////////////////////////
62
63 ////////////////////////////////////////////////////////////////////////
64 /// BASIC TYPES ///
65 ////////////////////////////////////////////////////////////////////////
66
67 typedef struct Kit_Sop_t_ Kit_Sop_t;
68 struct Kit_Sop_t_
69 {
70 int nCubes; // the number of cubes
71 unsigned * pCubes; // the storage for cubes
72 };
73
74 typedef union Kit_Edge_t_ Kit_Edge_t;
75 union Kit_Edge_t_
76 {
77 struct {
78 unsigned fCompl : 1; // the complemented bit
79 unsigned Node : 30; // the decomposition node pointed by the edge
80 } bits;
81 unsigned edgeInt;
82 };
83
84 typedef struct Kit_Node_t_ Kit_Node_t;
85 struct Kit_Node_t_
86 {
87 Kit_Edge_t eEdge0; // the left child of the node
88 Kit_Edge_t eEdge1; // the right child of the node
89 // other info
90 void * pFunc; // the function of the node (BDD or AIG)
91 unsigned Level : 14; // the level of this node in the global AIG
92 // printing info
93 unsigned fNodeOr : 1; // marks the original OR node
94 unsigned fCompl0 : 1; // marks the original complemented edge
95 unsigned fCompl1 : 1; // marks the original complemented edge
96 // latch info
97 unsigned nLat0 : 5; // the number of latches on the first edge
98 unsigned nLat1 : 5; // the number of latches on the second edge
99 unsigned nLat2 : 5; // the number of latches on the output edge
100 };
101
102 typedef struct Kit_Graph_t_ Kit_Graph_t;
103 struct Kit_Graph_t_
104 {
105 int fConst; // marks the constant 1 graph
106 int nLeaves; // the number of leaves
107 int nSize; // the number of nodes (including the leaves)
108 int nCap; // the number of allocated nodes
109 Kit_Node_t * pNodes; // the array of leaves and internal nodes
110 Kit_Edge_t eRoot; // the pointer to the topmost node
111 };
112
113
114 // DSD node types
115 typedef enum {
116 KIT_DSD_NONE = 0, // 0: unknown
117 KIT_DSD_CONST1, // 1: constant 1
118 KIT_DSD_VAR, // 2: elementary variable
119 KIT_DSD_AND, // 3: multi-input AND
120 KIT_DSD_XOR, // 4: multi-input XOR
121 KIT_DSD_PRIME // 5: arbitrary function of 3+ variables
122 } Kit_Dsd_t;
123
124 // DSD node
125 typedef struct Kit_DsdObj_t_ Kit_DsdObj_t;
126 struct Kit_DsdObj_t_
127 {
128 unsigned Id : 6; // the number of this node
129 unsigned Type : 3; // none, const, var, AND, XOR, MUX, PRIME
130 unsigned fMark : 1; // finished checking output
131 unsigned Offset : 8; // offset to the truth table
132 unsigned nRefs : 8; // offset to the truth table
133 unsigned nFans : 6; // the number of fanins of this node
134 unsigned char pFans[0]; // the fanin literals
135 };
136
137 // DSD network
138 typedef struct Kit_DsdNtk_t_ Kit_DsdNtk_t;
139 struct Kit_DsdNtk_t_
140 {
141 unsigned char nVars; // at most 16 (perhaps 18?)
142 unsigned char nNodesAlloc; // the number of allocated nodes (at most nVars)
143 unsigned char nNodes; // the number of nodes
144 unsigned char Root; // the root of the tree
145 unsigned * pMem; // memory for the truth tables (memory manager?)
146 unsigned * pSupps; // supports of the nodes
147 Kit_DsdObj_t** pNodes; // the nodes
148 };
149
150 #if 0
151 // DSD manager
152 typedef struct Kit_DsdMan_t_ Kit_DsdMan_t;
153 struct Kit_DsdMan_t_
154 {
155 int nVars; // the maximum number of variables
156 int nWords; // the number of words in TTs
157 Vec_Ptr_t * vTtElems; // elementary truth tables
158 Vec_Ptr_t * vTtNodes; // the node truth tables
159 // BDD representation
160 CloudManager * dd; // BDD package
161 Vec_Ptr_t * vTtBdds; // the node truth tables
162 Vec_Int_t * vNodes; // temporary array for BDD nodes
163 };
164 #endif
165
Kit_DsdVar2Lit(int Var,int fCompl)166 static inline int Kit_DsdVar2Lit( int Var, int fCompl ) { return Var + Var + fCompl; }
Kit_DsdLit2Var(int Lit)167 static inline int Kit_DsdLit2Var( int Lit ) { return Lit >> 1; }
Kit_DsdLitIsCompl(int Lit)168 static inline int Kit_DsdLitIsCompl( int Lit ) { return Lit & 1; }
Kit_DsdLitNot(int Lit)169 static inline int Kit_DsdLitNot( int Lit ) { return Lit ^ 1; }
Kit_DsdLitNotCond(int Lit,int c)170 static inline int Kit_DsdLitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); }
Kit_DsdLitRegular(int Lit)171 static inline int Kit_DsdLitRegular( int Lit ) { return Lit & 0xfe; }
172
Kit_DsdObjOffset(int nFans)173 static inline unsigned Kit_DsdObjOffset( int nFans ) { return (nFans >> 2) + ((nFans & 3) > 0); }
Kit_DsdObjTruth(Kit_DsdObj_t * pObj)174 static inline unsigned * Kit_DsdObjTruth( Kit_DsdObj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; }
Kit_DsdNtkObjNum(Kit_DsdNtk_t * pNtk)175 static inline int Kit_DsdNtkObjNum( Kit_DsdNtk_t * pNtk ){ return pNtk->nVars + pNtk->nNodes; }
Kit_DsdNtkObj(Kit_DsdNtk_t * pNtk,int Id)176 static inline Kit_DsdObj_t * Kit_DsdNtkObj( Kit_DsdNtk_t * pNtk, int Id ) { assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; }
Kit_DsdNtkRoot(Kit_DsdNtk_t * pNtk)177 static inline Kit_DsdObj_t * Kit_DsdNtkRoot( Kit_DsdNtk_t * pNtk ) { return Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(pNtk->Root) ); }
Kit_DsdLitIsLeaf(Kit_DsdNtk_t * pNtk,int Lit)178 static inline int Kit_DsdLitIsLeaf( Kit_DsdNtk_t * pNtk, int Lit ) { int Id = Kit_DsdLit2Var(Lit); assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars; }
Kit_DsdLitSupport(Kit_DsdNtk_t * pNtk,int Lit)179 static inline unsigned Kit_DsdLitSupport( Kit_DsdNtk_t * pNtk, int Lit ) { int Id = Kit_DsdLit2Var(Lit); assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return pNtk->pSupps? (Id < pNtk->nVars? (1 << Id) : pNtk->pSupps[Id - pNtk->nVars]) : 0; }
180
181 #define Kit_DsdNtkForEachObj( pNtk, pObj, i ) \
182 for ( i = 0; (i < (pNtk)->nNodes) && ((pObj) = (pNtk)->pNodes[i]); i++ )
183 #define Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) \
184 for ( i = 0; (i < (pObj)->nFans) && ((iLit) = (pObj)->pFans[i], 1); i++ )
185
186 ////////////////////////////////////////////////////////////////////////
187 /// MACRO DEFINITIONS ///
188 ////////////////////////////////////////////////////////////////////////
189
190 #define KIT_MIN(a,b) (((a) < (b))? (a) : (b))
191 #define KIT_MAX(a,b) (((a) > (b))? (a) : (b))
192 #define KIT_INFINITY (100000000)
193
194 #ifndef ALLOC
195 #define ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
196 #endif
197
198 #ifndef FREE
199 #define FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
200 #endif
201
202 #ifndef REALLOC
203 #define REALLOC(type, obj, num) \
204 ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
205 ((type *) malloc(sizeof(type) * (num))))
206 #endif
207
Kit_CubeHasLit(unsigned uCube,int i)208 static inline int Kit_CubeHasLit( unsigned uCube, int i ) { return(uCube & (unsigned)(1<<i)) > 0; }
Kit_CubeSetLit(unsigned uCube,int i)209 static inline unsigned Kit_CubeSetLit( unsigned uCube, int i ) { return uCube | (unsigned)(1<<i); }
Kit_CubeXorLit(unsigned uCube,int i)210 static inline unsigned Kit_CubeXorLit( unsigned uCube, int i ) { return uCube ^ (unsigned)(1<<i); }
Kit_CubeRemLit(unsigned uCube,int i)211 static inline unsigned Kit_CubeRemLit( unsigned uCube, int i ) { return uCube & ~(unsigned)(1<<i); }
212
Kit_CubeContains(unsigned uLarge,unsigned uSmall)213 static inline int Kit_CubeContains( unsigned uLarge, unsigned uSmall ) { return (uLarge & uSmall) == uSmall; }
Kit_CubeSharp(unsigned uCube,unsigned uMask)214 static inline unsigned Kit_CubeSharp( unsigned uCube, unsigned uMask ) { return uCube & ~uMask; }
Kit_CubeMask(int nVar)215 static inline unsigned Kit_CubeMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); }
216
Kit_CubeIsMarked(unsigned uCube)217 static inline int Kit_CubeIsMarked( unsigned uCube ) { return Kit_CubeHasLit( uCube, 31 ); }
Kit_CubeMark(unsigned uCube)218 static inline unsigned Kit_CubeMark( unsigned uCube ) { return Kit_CubeSetLit( uCube, 31 ); }
Kit_CubeUnmark(unsigned uCube)219 static inline unsigned Kit_CubeUnmark( unsigned uCube ) { return Kit_CubeRemLit( uCube, 31 ); }
220
Kit_SopCubeNum(Kit_Sop_t * cSop)221 static inline int Kit_SopCubeNum( Kit_Sop_t * cSop ) { return cSop->nCubes; }
Kit_SopCube(Kit_Sop_t * cSop,int i)222 static inline unsigned Kit_SopCube( Kit_Sop_t * cSop, int i ) { return cSop->pCubes[i]; }
Kit_SopShrink(Kit_Sop_t * cSop,int nCubesNew)223 static inline void Kit_SopShrink( Kit_Sop_t * cSop, int nCubesNew ) { cSop->nCubes = nCubesNew; }
Kit_SopPushCube(Kit_Sop_t * cSop,unsigned uCube)224 static inline void Kit_SopPushCube( Kit_Sop_t * cSop, unsigned uCube ) { cSop->pCubes[cSop->nCubes++] = uCube; }
Kit_SopWriteCube(Kit_Sop_t * cSop,unsigned uCube,int i)225 static inline void Kit_SopWriteCube( Kit_Sop_t * cSop, unsigned uCube, int i ) { cSop->pCubes[i] = uCube; }
226
Kit_EdgeCreate(int Node,int fCompl)227 static inline Kit_Edge_t Kit_EdgeCreate( int Node, int fCompl ) { Kit_Edge_t eEdge = { { fCompl, Node } }; return eEdge; }
Kit_EdgeToInt(Kit_Edge_t eEdge)228 static inline unsigned Kit_EdgeToInt( Kit_Edge_t eEdge ) { return (eEdge.bits.Node << 1) | eEdge.bits.fCompl; }
Kit_IntToEdge(unsigned Edge)229 static inline Kit_Edge_t Kit_IntToEdge( unsigned Edge ) { return Kit_EdgeCreate( Edge >> 1, Edge & 1 ); }
Kit_EdgeToInt_(Kit_Edge_t eEdge)230 static inline unsigned Kit_EdgeToInt_( Kit_Edge_t eEdge ) { return eEdge.edgeInt; }
Kit_IntToEdge_(unsigned Edge)231 static inline Kit_Edge_t Kit_IntToEdge_( unsigned Edge ) { Kit_Edge_t eEdge; eEdge.edgeInt = Edge; return eEdge; }
232
Kit_GraphIsConst(Kit_Graph_t * pGraph)233 static inline int Kit_GraphIsConst( Kit_Graph_t * pGraph ) { return pGraph->fConst; }
Kit_GraphIsConst0(Kit_Graph_t * pGraph)234 static inline int Kit_GraphIsConst0( Kit_Graph_t * pGraph ) { return pGraph->fConst && pGraph->eRoot.bits.fCompl; }
Kit_GraphIsConst1(Kit_Graph_t * pGraph)235 static inline int Kit_GraphIsConst1( Kit_Graph_t * pGraph ) { return pGraph->fConst && !pGraph->eRoot.bits.fCompl; }
Kit_GraphIsComplement(Kit_Graph_t * pGraph)236 static inline int Kit_GraphIsComplement( Kit_Graph_t * pGraph ) { return pGraph->eRoot.bits.fCompl; }
Kit_GraphIsVar(Kit_Graph_t * pGraph)237 static inline int Kit_GraphIsVar( Kit_Graph_t * pGraph ) { return pGraph->eRoot.bits.Node < (unsigned)pGraph->nLeaves; }
Kit_GraphComplement(Kit_Graph_t * pGraph)238 static inline void Kit_GraphComplement( Kit_Graph_t * pGraph ) { pGraph->eRoot.bits.fCompl ^= 1; }
Kit_GraphSetRoot(Kit_Graph_t * pGraph,Kit_Edge_t eRoot)239 static inline void Kit_GraphSetRoot( Kit_Graph_t * pGraph, Kit_Edge_t eRoot ) { pGraph->eRoot = eRoot; }
Kit_GraphLeaveNum(Kit_Graph_t * pGraph)240 static inline int Kit_GraphLeaveNum( Kit_Graph_t * pGraph ) { return pGraph->nLeaves; }
Kit_GraphNodeNum(Kit_Graph_t * pGraph)241 static inline int Kit_GraphNodeNum( Kit_Graph_t * pGraph ) { return pGraph->nSize - pGraph->nLeaves; }
Kit_GraphNode(Kit_Graph_t * pGraph,int i)242 static inline Kit_Node_t * Kit_GraphNode( Kit_Graph_t * pGraph, int i ) { return pGraph->pNodes + i; }
Kit_GraphNodeLast(Kit_Graph_t * pGraph)243 static inline Kit_Node_t * Kit_GraphNodeLast( Kit_Graph_t * pGraph ) { return pGraph->pNodes + pGraph->nSize - 1; }
Kit_GraphNodeInt(Kit_Graph_t * pGraph,Kit_Node_t * pNode)244 static inline int Kit_GraphNodeInt( Kit_Graph_t * pGraph, Kit_Node_t * pNode ) { return pNode - pGraph->pNodes; }
Kit_GraphNodeIsVar(Kit_Graph_t * pGraph,Kit_Node_t * pNode)245 static inline int Kit_GraphNodeIsVar( Kit_Graph_t * pGraph, Kit_Node_t * pNode ) { return Kit_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves; }
Kit_GraphVar(Kit_Graph_t * pGraph)246 static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNode( pGraph, pGraph->eRoot.bits.Node ); }
Kit_GraphVarInt(Kit_Graph_t * pGraph)247 static inline int Kit_GraphVarInt( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNodeInt( pGraph, Kit_GraphVar(pGraph) ); }
Kit_GraphNodeFanin0(Kit_Graph_t * pGraph,Kit_Node_t * pNode)248 static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.bits.Node); }
Kit_GraphNodeFanin1(Kit_Graph_t * pGraph,Kit_Node_t * pNode)249 static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.bits.Node); }
Kit_GraphRootLevel(Kit_Graph_t * pGraph)250 static inline int Kit_GraphRootLevel( Kit_Graph_t * pGraph ) { return Kit_GraphNode(pGraph, pGraph->eRoot.bits.Node)->Level; }
251
Kit_BitWordNum(int nBits)252 static inline int Kit_BitWordNum( int nBits ) { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0); }
Kit_TruthWordNum(int nVars)253 static inline int Kit_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
Kit_BitMask(int nBits)254 static inline unsigned Kit_BitMask( int nBits ) { assert( nBits <= 32 ); return ~((~(unsigned)0) << nBits); }
255
Kit_TruthSetBit(unsigned * p,int Bit)256 static inline void Kit_TruthSetBit( unsigned * p, int Bit ) { p[Bit>>5] |= (1<<(Bit & 31)); }
Kit_TruthXorBit(unsigned * p,int Bit)257 static inline void Kit_TruthXorBit( unsigned * p, int Bit ) { p[Bit>>5] ^= (1<<(Bit & 31)); }
Kit_TruthHasBit(unsigned * p,int Bit)258 static inline int Kit_TruthHasBit( unsigned * p, int Bit ) { return (p[Bit>>5] & (1<<(Bit & 31))) > 0; }
259
Kit_WordFindFirstBit(unsigned uWord)260 static inline int Kit_WordFindFirstBit( unsigned uWord )
261 {
262 int i;
263 for ( i = 0; i < 32; i++ )
264 if ( uWord & (1 << i) )
265 return i;
266 return -1;
267 }
Kit_WordHasOneBit(unsigned uWord)268 static inline int Kit_WordHasOneBit( unsigned uWord )
269 {
270 return (uWord & (uWord - 1)) == 0;
271 }
Kit_WordCountOnes(unsigned uWord)272 static inline int Kit_WordCountOnes( unsigned uWord )
273 {
274 uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
275 uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
276 uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
277 uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
278 return (uWord & 0x0000FFFF) + (uWord>>16);
279 }
Kit_TruthCountOnes(unsigned * pIn,int nVars)280 static inline int Kit_TruthCountOnes( unsigned * pIn, int nVars )
281 {
282 int w, Counter = 0;
283 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
284 Counter += Kit_WordCountOnes(pIn[w]);
285 return Counter;
286 }
Kit_TruthFindFirstBit(unsigned * pIn,int nVars)287 static inline int Kit_TruthFindFirstBit( unsigned * pIn, int nVars )
288 {
289 int w;
290 for ( w = 0; w < Kit_TruthWordNum(nVars); w++ )
291 if ( pIn[w] )
292 return 32*w + Kit_WordFindFirstBit(pIn[w]);
293 return -1;
294 }
Kit_TruthFindFirstZero(unsigned * pIn,int nVars)295 static inline int Kit_TruthFindFirstZero( unsigned * pIn, int nVars )
296 {
297 int w;
298 for ( w = 0; w < Kit_TruthWordNum(nVars); w++ )
299 if ( ~pIn[w] )
300 return 32*w + Kit_WordFindFirstBit(~pIn[w]);
301 return -1;
302 }
Kit_TruthIsEqual(unsigned * pIn0,unsigned * pIn1,int nVars)303 static inline int Kit_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVars )
304 {
305 int w;
306 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
307 if ( pIn0[w] != pIn1[w] )
308 return 0;
309 return 1;
310 }
Kit_TruthIsOpposite(unsigned * pIn0,unsigned * pIn1,int nVars)311 static inline int Kit_TruthIsOpposite( unsigned * pIn0, unsigned * pIn1, int nVars )
312 {
313 int w;
314 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
315 if ( pIn0[w] != ~pIn1[w] )
316 return 0;
317 return 1;
318 }
Kit_TruthIsEqualWithPhase(unsigned * pIn0,unsigned * pIn1,int nVars)319 static inline int Kit_TruthIsEqualWithPhase( unsigned * pIn0, unsigned * pIn1, int nVars )
320 {
321 int w;
322 if ( (pIn0[0] & 1) == (pIn1[0] & 1) )
323 {
324 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
325 if ( pIn0[w] != pIn1[w] )
326 return 0;
327 }
328 else
329 {
330 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
331 if ( pIn0[w] != ~pIn1[w] )
332 return 0;
333 }
334 return 1;
335 }
Kit_TruthIsConst0(unsigned * pIn,int nVars)336 static inline int Kit_TruthIsConst0( unsigned * pIn, int nVars )
337 {
338 int w;
339 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
340 if ( pIn[w] )
341 return 0;
342 return 1;
343 }
Kit_TruthIsConst1(unsigned * pIn,int nVars)344 static inline int Kit_TruthIsConst1( unsigned * pIn, int nVars )
345 {
346 int w;
347 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
348 if ( pIn[w] != ~(unsigned)0 )
349 return 0;
350 return 1;
351 }
Kit_TruthIsImply(unsigned * pIn1,unsigned * pIn2,int nVars)352 static inline int Kit_TruthIsImply( unsigned * pIn1, unsigned * pIn2, int nVars )
353 {
354 int w;
355 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
356 if ( pIn1[w] & ~pIn2[w] )
357 return 0;
358 return 1;
359 }
Kit_TruthIsDisjoint(unsigned * pIn1,unsigned * pIn2,int nVars)360 static inline int Kit_TruthIsDisjoint( unsigned * pIn1, unsigned * pIn2, int nVars )
361 {
362 int w;
363 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
364 if ( pIn1[w] & pIn2[w] )
365 return 0;
366 return 1;
367 }
Kit_TruthIsDisjoint3(unsigned * pIn1,unsigned * pIn2,unsigned * pIn3,int nVars)368 static inline int Kit_TruthIsDisjoint3( unsigned * pIn1, unsigned * pIn2, unsigned * pIn3, int nVars )
369 {
370 int w;
371 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
372 if ( pIn1[w] & pIn2[w] & pIn3[w] )
373 return 0;
374 return 1;
375 }
Kit_TruthCopy(unsigned * pOut,unsigned * pIn,int nVars)376 static inline void Kit_TruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
377 {
378 int w;
379 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
380 pOut[w] = pIn[w];
381 }
Kit_TruthClear(unsigned * pOut,int nVars)382 static inline void Kit_TruthClear( unsigned * pOut, int nVars )
383 {
384 int w;
385 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
386 pOut[w] = 0;
387 }
Kit_TruthFill(unsigned * pOut,int nVars)388 static inline void Kit_TruthFill( unsigned * pOut, int nVars )
389 {
390 int w;
391 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
392 pOut[w] = ~(unsigned)0;
393 }
Kit_TruthNot(unsigned * pOut,unsigned * pIn,int nVars)394 static inline void Kit_TruthNot( unsigned * pOut, unsigned * pIn, int nVars )
395 {
396 int w;
397 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
398 pOut[w] = ~pIn[w];
399 }
Kit_TruthAnd(unsigned * pOut,unsigned * pIn0,unsigned * pIn1,int nVars)400 static inline void Kit_TruthAnd( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
401 {
402 int w;
403 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
404 pOut[w] = pIn0[w] & pIn1[w];
405 }
Kit_TruthOr(unsigned * pOut,unsigned * pIn0,unsigned * pIn1,int nVars)406 static inline void Kit_TruthOr( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
407 {
408 int w;
409 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
410 pOut[w] = pIn0[w] | pIn1[w];
411 }
Kit_TruthXor(unsigned * pOut,unsigned * pIn0,unsigned * pIn1,int nVars)412 static inline void Kit_TruthXor( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
413 {
414 int w;
415 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
416 pOut[w] = pIn0[w] ^ pIn1[w];
417 }
Kit_TruthSharp(unsigned * pOut,unsigned * pIn0,unsigned * pIn1,int nVars)418 static inline void Kit_TruthSharp( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
419 {
420 int w;
421 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
422 pOut[w] = pIn0[w] & ~pIn1[w];
423 }
Kit_TruthNand(unsigned * pOut,unsigned * pIn0,unsigned * pIn1,int nVars)424 static inline void Kit_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
425 {
426 int w;
427 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
428 pOut[w] = ~(pIn0[w] & pIn1[w]);
429 }
Kit_TruthAndPhase(unsigned * pOut,unsigned * pIn0,unsigned * pIn1,int nVars,int fCompl0,int fCompl1)430 static inline void Kit_TruthAndPhase( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars, int fCompl0, int fCompl1 )
431 {
432 int w;
433 if ( fCompl0 && fCompl1 )
434 {
435 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
436 pOut[w] = ~(pIn0[w] | pIn1[w]);
437 }
438 else if ( fCompl0 && !fCompl1 )
439 {
440 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
441 pOut[w] = ~pIn0[w] & pIn1[w];
442 }
443 else if ( !fCompl0 && fCompl1 )
444 {
445 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
446 pOut[w] = pIn0[w] & ~pIn1[w];
447 }
448 else // if ( !fCompl0 && !fCompl1 )
449 {
450 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
451 pOut[w] = pIn0[w] & pIn1[w];
452 }
453 }
Kit_TruthMux(unsigned * pOut,unsigned * pIn0,unsigned * pIn1,unsigned * pCtrl,int nVars)454 static inline void Kit_TruthMux( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, unsigned * pCtrl, int nVars )
455 {
456 int w;
457 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
458 pOut[w] = (pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
459 }
Kit_TruthMuxPhase(unsigned * pOut,unsigned * pIn0,unsigned * pIn1,unsigned * pCtrl,int nVars,int fComp0)460 static inline void Kit_TruthMuxPhase( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, unsigned * pCtrl, int nVars, int fComp0 )
461 {
462 int w;
463 if ( fComp0 )
464 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
465 pOut[w] = (~pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
466 else
467 for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
468 pOut[w] = (pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
469 }
Kit_TruthIthVar(unsigned * pTruth,int nVars,int iVar)470 static inline void Kit_TruthIthVar( unsigned * pTruth, int nVars, int iVar )
471 {
472 unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
473 int k, nWords = (nVars <= 5 ? 1 : (1 << (nVars - 5)));
474 if ( iVar < 5 )
475 {
476 for ( k = 0; k < nWords; k++ )
477 pTruth[k] = Masks[iVar];
478 }
479 else
480 {
481 for ( k = 0; k < nWords; k++ )
482 if ( k & (1 << (iVar-5)) )
483 pTruth[k] = ~(unsigned)0;
484 else
485 pTruth[k] = 0;
486 }
487 }
488
489
490 ////////////////////////////////////////////////////////////////////////
491 /// ITERATORS ///
492 ////////////////////////////////////////////////////////////////////////
493
494 #define Kit_SopForEachCube( cSop, uCube, i ) \
495 for ( i = 0; (i < Kit_SopCubeNum(cSop)) && ((uCube) = Kit_SopCube(cSop, i)); i++ )
496 #define Kit_CubeForEachLiteral( uCube, Lit, nLits, i ) \
497 for ( i = 0; (i < (nLits)) && ((Lit) = Kit_CubeHasLit(uCube, i)); i++ )
498
499 #define Kit_GraphForEachLeaf( pGraph, pLeaf, i ) \
500 for ( i = 0; (i < (pGraph)->nLeaves) && (((pLeaf) = Kit_GraphNode(pGraph, i)), 1); i++ )
501 #define Kit_GraphForEachNode( pGraph, pAnd, i ) \
502 for ( i = (pGraph)->nLeaves; (i < (pGraph)->nSize) && (((pAnd) = Kit_GraphNode(pGraph, i)), 1); i++ )
503
504
505 ////////////////////////////////////////////////////////////////////////
506 /// FUNCTION DECLARATIONS ///
507 ////////////////////////////////////////////////////////////////////////
508
509 /*=== kitTruth.c ==========================================================*/
510 extern void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar );
511 extern void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar );
512 extern void Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn );
513 extern void Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn );
514 extern int Kit_TruthVarInSupport( unsigned * pTruth, int nVars, int iVar );
515
516 /*=== kitIsop.c ==========================================================*/
517 extern int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth );
518
519
520 ////////////////////////////////////////////////////////////////////////
521 /// UNUSED FUNCTION DECLARATIONS ///
522 ////////////////////////////////////////////////////////////////////////
523
524 #if 0
525
526 /*=== kitBdd.c ==========================================================*/
527 extern DdNode * Kit_SopToBdd( DdManager * dd, Kit_Sop_t * cSop, int nVars );
528 extern DdNode * Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph );
529 extern DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars, int fMSBonTop );
530 /*=== kitCloud.c ==========================================================*/
531 extern CloudNode * Kit_TruthToCloud( CloudManager * dd, unsigned * pTruth, int nVars );
532 extern unsigned * Kit_CloudToTruth( Vec_Int_t * vNodes, int nVars, Vec_Ptr_t * vStore, int fInv );
533 extern int Kit_CreateCloud( CloudManager * dd, CloudNode * pFunc, Vec_Int_t * vNodes );
534 extern int Kit_CreateCloudFromTruth( CloudManager * dd, unsigned * pTruth, int nVars, Vec_Int_t * vNodes );
535 extern unsigned * Kit_TruthCompose( CloudManager * dd, unsigned * pTruth, int nVars, unsigned ** pInputs, int nVarsAll, Vec_Ptr_t * vStore, Vec_Int_t * vNodes );
536 extern void Kit_TruthCofSupports( Vec_Int_t * vBddDir, Vec_Int_t * vBddInv, int nVars, Vec_Int_t * vMemory, unsigned * puSupps );
537 /*=== kitDsd.c ==========================================================*/
538 extern Kit_DsdMan_t * Kit_DsdManAlloc( int nVars, int nNodes );
539 extern void Kit_DsdManFree( Kit_DsdMan_t * p );
540 extern Kit_DsdNtk_t * Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize );
541 extern unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk );
542 extern void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes );
543 extern void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp );
544 extern void Kit_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthCo, unsigned * pTruthDec );
545 extern void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk );
546 extern void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk );
547 extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
548 extern Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars );
549 extern Kit_DsdNtk_t * Kit_DsdDecomposeExpand( unsigned * pTruth, int nVars );
550 extern Kit_DsdNtk_t * Kit_DsdDecomposeMux( unsigned * pTruth, int nVars, int nDecMux );
551 extern void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars );
552 extern void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
553 extern int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk );
554 extern unsigned Kit_DsdNonDsdSupports( Kit_DsdNtk_t * pNtk );
555 extern unsigned Kit_DsdGetSupports( Kit_DsdNtk_t * p );
556 extern Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p );
557 extern Kit_DsdNtk_t * Kit_DsdShrink( Kit_DsdNtk_t * p, int pPrios[] );
558 extern void Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] );
559 extern int Kit_DsdCofactoring( unsigned * pTruth, int nVars, int * pCofVars, int nLimit, int fVerbose );
560 /*=== kitFactor.c ==========================================================*/
561 extern Kit_Graph_t * Kit_SopFactor( Vec_Int_t * vCover, int fCompl, int nVars, Vec_Int_t * vMemory );
562 /*=== kitGraph.c ==========================================================*/
563 extern Kit_Graph_t * Kit_GraphCreate( int nLeaves );
564 extern Kit_Graph_t * Kit_GraphCreateConst0();
565 extern Kit_Graph_t * Kit_GraphCreateConst1();
566 extern Kit_Graph_t * Kit_GraphCreateLeaf( int iLeaf, int nLeaves, int fCompl );
567 extern void Kit_GraphFree( Kit_Graph_t * pGraph );
568 extern Kit_Node_t * Kit_GraphAppendNode( Kit_Graph_t * pGraph );
569 extern Kit_Edge_t Kit_GraphAddNodeAnd( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edge_t eEdge1 );
570 extern Kit_Edge_t Kit_GraphAddNodeOr( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edge_t eEdge1 );
571 extern Kit_Edge_t Kit_GraphAddNodeXor( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edge_t eEdge1, int Type );
572 extern Kit_Edge_t Kit_GraphAddNodeMux( Kit_Graph_t * pGraph, Kit_Edge_t eEdgeC, Kit_Edge_t eEdgeT, Kit_Edge_t eEdgeE, int Type );
573 extern unsigned Kit_GraphToTruth( Kit_Graph_t * pGraph );
574 extern Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
575 extern int Kit_GraphLeafDepth_rec( Kit_Graph_t * pGraph, Kit_Node_t * pNode, Kit_Node_t * pLeaf );
576 /*=== kitHop.c ==========================================================*/
577 //extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
578 //extern Hop_Obj_t * Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
579 //extern Hop_Obj_t * Kit_CoverToHop( Hop_Man_t * pMan, Vec_Int_t * vCover, int nVars, Vec_Int_t * vMemory );
580 /*=== kitSop.c ==========================================================*/
581 extern void Kit_SopCreate( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nVars, Vec_Int_t * vMemory );
582 extern void Kit_SopCreateInverse( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nVars, Vec_Int_t * vMemory );
583 extern void Kit_SopDup( Kit_Sop_t * cResult, Kit_Sop_t * cSop, Vec_Int_t * vMemory );
584 extern void Kit_SopDivideByLiteralQuo( Kit_Sop_t * cSop, int iLit );
585 extern void Kit_SopDivideByCube( Kit_Sop_t * cSop, Kit_Sop_t * cDiv, Kit_Sop_t * vQuo, Kit_Sop_t * vRem, Vec_Int_t * vMemory );
586 extern void Kit_SopDivideInternal( Kit_Sop_t * cSop, Kit_Sop_t * cDiv, Kit_Sop_t * vQuo, Kit_Sop_t * vRem, Vec_Int_t * vMemory );
587 extern void Kit_SopMakeCubeFree( Kit_Sop_t * cSop );
588 extern int Kit_SopIsCubeFree( Kit_Sop_t * cSop );
589 extern void Kit_SopCommonCubeCover( Kit_Sop_t * cResult, Kit_Sop_t * cSop, Vec_Int_t * vMemory );
590 extern int Kit_SopAnyLiteral( Kit_Sop_t * cSop, int nLits );
591 extern int Kit_SopDivisor( Kit_Sop_t * cResult, Kit_Sop_t * cSop, int nLits, Vec_Int_t * vMemory );
592 extern void Kit_SopBestLiteralCover( Kit_Sop_t * cResult, Kit_Sop_t * cSop, unsigned uCube, int nLits, Vec_Int_t * vMemory );
593 /*=== kitTruth.c ==========================================================*/
594 extern void Kit_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int Start );
595 extern int Kit_TruthSupportSize( unsigned * pTruth, int nVars );
596 extern unsigned Kit_TruthSupport( unsigned * pTruth, int nVars );
597 extern void Kit_TruthCofactor0New( unsigned * pOut, unsigned * pIn, int nVars, int iVar );
598 extern void Kit_TruthCofactor1New( unsigned * pOut, unsigned * pIn, int nVars, int iVar );
599 extern void Kit_TruthExist( unsigned * pTruth, int nVars, int iVar );
600 extern void Kit_TruthExistNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
601 extern void Kit_TruthExistSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
602 extern void Kit_TruthForall( unsigned * pTruth, int nVars, int iVar );
603 extern void Kit_TruthForallNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
604 extern void Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
605 extern void Kit_TruthUniqueNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
606 extern void Kit_TruthMuxVar( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
607 extern void Kit_TruthMuxVarPhase( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar, int fCompl0 );
608 extern void Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
609 extern int Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
610 extern int Kit_TruthBestCofVar( unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 );
611 extern void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore );
612 extern void Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVars, short * pStore, unsigned * pAux );
613 extern unsigned Kit_TruthHash( unsigned * pIn, int nWords );
614 extern unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore );
615 extern char * Kit_TruthDumpToFile( unsigned * pTruth, int nVars, int nFile );
616
617 #ifdef __cplusplus
618 }
619 #endif
620
621 #endif
622 #endif
623
624 ////////////////////////////////////////////////////////////////////////
625 /// END OF FILE ///
626 ////////////////////////////////////////////////////////////////////////
627
628