ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
deco.h
Go to the documentation of this file.
1
20
21#ifndef ABC__aig__deco__deco_h
22#define ABC__aig__deco__deco_h
23
24
28
32
33
34
36
37
41
42typedef struct Dec_Edge_t_ Dec_Edge_t;
43struct Dec_Edge_t_
44{
45 unsigned fCompl : 1; // the complemented bit
46 unsigned Node : 30; // the decomposition node pointed by the edge
47};
48
49typedef struct Dec_Node_t_ Dec_Node_t;
50struct Dec_Node_t_
51{
52 Dec_Edge_t eEdge0; // the left child of the node
53 Dec_Edge_t eEdge1; // the right child of the node
54 // other info
55 union { int iFunc; // the literal of the node (AIG)
56 void * pFunc; }; // the function of the node (BDD or AIG)
57 unsigned Level : 14; // the level of this node in the global AIG
58 // printing info
59 unsigned fNodeOr : 1; // marks the original OR node
60 unsigned fCompl0 : 1; // marks the original complemented edge
61 unsigned fCompl1 : 1; // marks the original complemented edge
62 // latch info
63 unsigned nLat0 : 5; // the number of latches on the first edge
64 unsigned nLat1 : 5; // the number of latches on the second edge
65 unsigned nLat2 : 5; // the number of latches on the output edge
66};
67
68typedef struct Dec_Graph_t_ Dec_Graph_t;
69struct Dec_Graph_t_
70{
71 int fConst; // marks the constant 1 graph
72 int nLeaves; // the number of leaves
73 int nSize; // the number of nodes (including the leaves)
74 int nCap; // the number of allocated nodes
75 Dec_Node_t * pNodes; // the array of leaves and internal nodes
76 Dec_Edge_t eRoot; // the pointer to the topmost node
77};
78
79typedef struct Dec_Man_t_ Dec_Man_t;
80struct Dec_Man_t_
81{
82 void * pMvcMem; // memory manager for MVC cover (used for factoring)
83 Vec_Int_t * vCubes; // storage for cubes
84 Vec_Int_t * vLits; // storage for literals
85 // precomputation information about 4-variable functions
86 unsigned short * puCanons; // canonical forms
87 char * pPhases; // canonical phases
88 char * pPerms; // canonical permutations
89 unsigned char * pMap; // mapping of functions into class numbers
90};
91
92
96
97// iterator through the leaves
98#define Dec_GraphForEachLeaf( pGraph, pLeaf, i ) \
99 for ( i = 0; (i < (pGraph)->nLeaves) && (((pLeaf) = Dec_GraphNode(pGraph, i)), 1); i++ )
100// iterator through the internal nodes
101#define Dec_GraphForEachNode( pGraph, pAnd, i ) \
102 for ( i = (pGraph)->nLeaves; (i < (pGraph)->nSize) && (((pAnd) = Dec_GraphNode(pGraph, i)), 1); i++ )
103
107
111
123static inline Dec_Edge_t Dec_EdgeCreate( int Node, int fCompl )
124{
125 Dec_Edge_t eEdge = { (unsigned)fCompl, (unsigned)Node };
126 return eEdge;
127}
128
140static inline unsigned Dec_EdgeToInt( Dec_Edge_t eEdge )
141{
142 return (eEdge.Node << 1) | eEdge.fCompl;
143}
144
156static inline Dec_Edge_t Dec_IntToEdge( unsigned Edge )
157{
158 return Dec_EdgeCreate( Edge >> 1, Edge & 1 );
159}
160
172static inline unsigned Dec_EdgeToInt_( Dec_Edge_t m ) { union { Dec_Edge_t x; unsigned y; } v; v.x = m; return v.y; }
173/*
174static inline unsigned Dec_EdgeToInt_( Dec_Edge_t eEdge )
175{
176 return *(unsigned *)&eEdge;
177}
178*/
179
191static inline Dec_Edge_t Dec_IntToEdge_( unsigned m ) { union { Dec_Edge_t x; unsigned y; } v; v.y = m; return v.x; }
192/*
193static inline Dec_Edge_t Dec_IntToEdge_( unsigned Edge )
194{
195 return *(Dec_Edge_t *)&Edge;
196}
197*/
198
210static inline Dec_Graph_t * Dec_GraphCreate( int nLeaves )
211{
212 Dec_Graph_t * pGraph;
213 pGraph = ABC_ALLOC( Dec_Graph_t, 1 );
214 memset( pGraph, 0, sizeof(Dec_Graph_t) );
215 pGraph->nLeaves = nLeaves;
216 pGraph->nSize = nLeaves;
217 pGraph->nCap = 2 * nLeaves + 50;
218 pGraph->pNodes = ABC_ALLOC( Dec_Node_t, pGraph->nCap );
219 memset( pGraph->pNodes, 0, sizeof(Dec_Node_t) * pGraph->nSize );
220 return pGraph;
221}
222
234static inline Dec_Graph_t * Dec_GraphCreateConst0()
235{
236 Dec_Graph_t * pGraph;
237 pGraph = ABC_ALLOC( Dec_Graph_t, 1 );
238 memset( pGraph, 0, sizeof(Dec_Graph_t) );
239 pGraph->fConst = 1;
240 pGraph->eRoot.fCompl = 1;
241 return pGraph;
242}
243
255static inline Dec_Graph_t * Dec_GraphCreateConst1()
256{
257 Dec_Graph_t * pGraph;
258 pGraph = ABC_ALLOC( Dec_Graph_t, 1 );
259 memset( pGraph, 0, sizeof(Dec_Graph_t) );
260 pGraph->fConst = 1;
261 return pGraph;
262}
263
275static inline Dec_Graph_t * Dec_GraphCreateLeaf( int iLeaf, int nLeaves, int fCompl )
276{
277 Dec_Graph_t * pGraph;
278 assert( 0 <= iLeaf && iLeaf < nLeaves );
279 pGraph = Dec_GraphCreate( nLeaves );
280 pGraph->eRoot.Node = iLeaf;
281 pGraph->eRoot.fCompl = fCompl;
282 return pGraph;
283}
284
296static inline void Dec_GraphFree( Dec_Graph_t * pGraph )
297{
298 ABC_FREE( pGraph->pNodes );
299 ABC_FREE( pGraph );
300}
301
313static inline int Dec_GraphIsConst( Dec_Graph_t * pGraph )
314{
315 return pGraph->fConst;
316}
317
329static inline int Dec_GraphIsConst0( Dec_Graph_t * pGraph )
330{
331 return pGraph->fConst && pGraph->eRoot.fCompl;
332}
333
345static inline int Dec_GraphIsConst1( Dec_Graph_t * pGraph )
346{
347 return pGraph->fConst && !pGraph->eRoot.fCompl;
348}
349
361static inline int Dec_GraphIsComplement( Dec_Graph_t * pGraph )
362{
363 return pGraph->eRoot.fCompl;
364}
365
377static inline void Dec_GraphComplement( Dec_Graph_t * pGraph )
378{
379 pGraph->eRoot.fCompl ^= 1;
380}
381
382
394static inline int Dec_GraphLeaveNum( Dec_Graph_t * pGraph )
395{
396 return pGraph->nLeaves;
397}
398
410static inline int Dec_GraphNodeNum( Dec_Graph_t * pGraph )
411{
412 return pGraph->nSize - pGraph->nLeaves;
413}
414
426static inline Dec_Node_t * Dec_GraphNode( Dec_Graph_t * pGraph, int i )
427{
428 return pGraph->pNodes + i;
429}
430
442static inline Dec_Node_t * Dec_GraphNodeLast( Dec_Graph_t * pGraph )
443{
444 return pGraph->pNodes + pGraph->nSize - 1;
445}
446
458static inline int Dec_GraphNodeInt( Dec_Graph_t * pGraph, Dec_Node_t * pNode )
459{
460 return pNode - pGraph->pNodes;
461}
462
474static inline int Dec_GraphIsVar( Dec_Graph_t * pGraph )
475{
476 return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves;
477}
478
490static inline int Dec_GraphNodeIsVar( Dec_Graph_t * pGraph, Dec_Node_t * pNode )
491{
492 return Dec_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves;
493}
494
506static inline Dec_Node_t * Dec_GraphVar( Dec_Graph_t * pGraph )
507{
508 assert( Dec_GraphIsVar( pGraph ) );
509 return Dec_GraphNode( pGraph, pGraph->eRoot.Node );
510}
511
523static inline int Dec_GraphVarInt( Dec_Graph_t * pGraph )
524{
525 assert( Dec_GraphIsVar( pGraph ) );
526 return Dec_GraphNodeInt( pGraph, Dec_GraphVar(pGraph) );
527}
528
540static inline void Dec_GraphSetRoot( Dec_Graph_t * pGraph, Dec_Edge_t eRoot )
541{
542 pGraph->eRoot = eRoot;
543}
544
556static inline Dec_Node_t * Dec_GraphAppendNode( Dec_Graph_t * pGraph )
557{
558 Dec_Node_t * pNode;
559 if ( pGraph->nSize == pGraph->nCap )
560 {
561 pGraph->pNodes = ABC_REALLOC( Dec_Node_t, pGraph->pNodes, 2 * pGraph->nCap );
562 pGraph->nCap = 2 * pGraph->nCap;
563 }
564 pNode = pGraph->pNodes + pGraph->nSize++;
565 memset( pNode, 0, sizeof(Dec_Node_t) );
566 return pNode;
567}
568
580static inline Dec_Edge_t Dec_GraphAddNodeAnd( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1 )
581{
582 Dec_Node_t * pNode;
583 // get the new node
584 pNode = Dec_GraphAppendNode( pGraph );
585 // set the inputs and other info
586 pNode->eEdge0 = eEdge0;
587 pNode->eEdge1 = eEdge1;
588 pNode->fCompl0 = eEdge0.fCompl;
589 pNode->fCompl1 = eEdge1.fCompl;
590 return Dec_EdgeCreate( pGraph->nSize - 1, 0 );
591}
592
604static inline Dec_Edge_t Dec_GraphAddNodeOr( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1 )
605{
606 Dec_Node_t * pNode;
607 // get the new node
608 pNode = Dec_GraphAppendNode( pGraph );
609 // set the inputs and other info
610 pNode->eEdge0 = eEdge0;
611 pNode->eEdge1 = eEdge1;
612 pNode->fCompl0 = eEdge0.fCompl;
613 pNode->fCompl1 = eEdge1.fCompl;
614 // make adjustments for the OR gate
615 pNode->fNodeOr = 1;
616 pNode->eEdge0.fCompl = !pNode->eEdge0.fCompl;
617 pNode->eEdge1.fCompl = !pNode->eEdge1.fCompl;
618 return Dec_EdgeCreate( pGraph->nSize - 1, 1 );
619}
620
632static inline Dec_Edge_t Dec_GraphAddNodeXor( Dec_Graph_t * pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1, int Type )
633{
634 Dec_Edge_t eNode0, eNode1, eNode;
635 if ( Type == 0 )
636 {
637 // derive the first AND
638 eEdge0.fCompl ^= 1;
639 eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
640 eEdge0.fCompl ^= 1;
641 // derive the second AND
642 eEdge1.fCompl ^= 1;
643 eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
644 // derive the final OR
645 eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
646 }
647 else
648 {
649 // derive the first AND
650 eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
651 // derive the second AND
652 eEdge0.fCompl ^= 1;
653 eEdge1.fCompl ^= 1;
654 eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdge0, eEdge1 );
655 // derive the final OR
656 eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
657 eNode.fCompl ^= 1;
658 }
659 return eNode;
660}
661
673static inline Dec_Edge_t Dec_GraphAddNodeMux( Dec_Graph_t * pGraph, Dec_Edge_t eEdgeC, Dec_Edge_t eEdgeT, Dec_Edge_t eEdgeE, int Type )
674{
675 Dec_Edge_t eNode0, eNode1, eNode;
676 if ( Type == 0 )
677 {
678 // derive the first AND
679 eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
680 // derive the second AND
681 eEdgeC.fCompl ^= 1;
682 eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
683 // derive the final OR
684 eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
685 }
686 else
687 {
688 // complement the arguments
689 eEdgeT.fCompl ^= 1;
690 eEdgeE.fCompl ^= 1;
691 // derive the first AND
692 eNode0 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeT );
693 // derive the second AND
694 eEdgeC.fCompl ^= 1;
695 eNode1 = Dec_GraphAddNodeAnd( pGraph, eEdgeC, eEdgeE );
696 // derive the final OR
697 eNode = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
698 eNode.fCompl ^= 1;
699 }
700 return eNode;
701}
702
703
704
706
707
708
709#endif
710
714
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_REALLOC(type, obj, num)
Definition abc_global.h:268
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
struct Dec_Man_t_ Dec_Man_t
Definition dec.h:79
struct Dec_Node_t_ Dec_Node_t
Definition dec.h:49
typedefABC_NAMESPACE_HEADER_START struct Dec_Edge_t_ Dec_Edge_t
INCLUDES ///.
Definition dec.h:42
struct Dec_Graph_t_ Dec_Graph_t
Definition dec.h:68
unsigned fCompl
Definition dec.h:45
unsigned Node
Definition dec.h:46
Dec_Node_t * pNodes
Definition dec.h:75
int nCap
Definition dec.h:74
int fConst
Definition dec.h:71
int nLeaves
Definition dec.h:72
int nSize
Definition dec.h:73
Dec_Edge_t eRoot
Definition dec.h:76
Vec_Int_t * vCubes
Definition dec.h:83
char * pPerms
Definition dec.h:88
char * pPhases
Definition dec.h:87
void * pMvcMem
Definition dec.h:82
unsigned char * pMap
Definition dec.h:89
Vec_Int_t * vLits
Definition dec.h:84
unsigned short * puCanons
Definition dec.h:86
unsigned fCompl1
Definition dec.h:61
Dec_Edge_t eEdge1
Definition dec.h:53
void * pFunc
Definition dec.h:56
unsigned nLat0
Definition dec.h:63
unsigned fNodeOr
Definition dec.h:59
int iFunc
Definition dec.h:55
unsigned nLat1
Definition dec.h:64
unsigned Level
Definition dec.h:57
Dec_Edge_t eEdge0
Definition dec.h:52
unsigned fCompl0
Definition dec.h:60
unsigned nLat2
Definition dec.h:65
#define assert(ex)
Definition util_old.h:213
char * memset()