ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
cswInt.h
Go to the documentation of this file.
1
20
21#ifndef ABC__aig__csw__cswInt_h
22#define ABC__aig__csw__cswInt_h
23
24
28
29#include <stdio.h>
30#include <stdlib.h>
31#include <string.h>
32#include <assert.h>
33
34#include "aig/aig/aig.h"
35#include "opt/dar/dar.h"
36#include "bool/kit/kit.h"
37#include "csw.h"
38
42
43
44
46
47
51
52typedef struct Csw_Man_t_ Csw_Man_t;
53typedef struct Csw_Cut_t_ Csw_Cut_t;
54
55// the cut used to represent node in the AIG
57{
58 Csw_Cut_t * pNext; // the next cut in the table
59 int Cost; // the cost of the cut
60// float Cost; // the cost of the cut
61 unsigned uSign; // cut signature
62 int iNode; // the node, for which it is the cut
63 short nCutSize; // the number of bytes in the cut
64 char nLeafMax; // the maximum number of fanins
65 char nFanins; // the current number of fanins
66 int pFanins[0]; // the fanins (followed by the truth table)
67};
68
69// the CNF computation manager
71{
72 // AIG manager
73 Aig_Man_t * pManAig; // the input AIG manager
74 Aig_Man_t * pManRes; // the output AIG manager
75 Aig_Obj_t ** pEquiv; // the equivalent nodes in the resulting manager
76 Csw_Cut_t ** pCuts; // the cuts for each node in the output manager
77 int * pnRefs; // the number of references of each new node
78 // hash table for cuts
79 Csw_Cut_t ** pTable; // the table composed of cuts
80 int nTableSize; // the size of hash table
81 // parameters
82 int nCutsMax; // the max number of cuts at the node
83 int nLeafMax; // the max number of leaves of a cut
84 int fVerbose; // enables verbose output
85 // internal variables
86 int nCutSize; // the number of bytes needed to store one cut
87 int nTruthWords; // the number of truth table words
88 Aig_MmFixed_t * pMemCuts; // memory manager for cuts
89 unsigned * puTemp[4]; // used for the truth table computation
90 // statistics
91 int nNodesTriv0; // the number of trivial nodes
92 int nNodesTriv1; // the number of trivial nodes
93 int nNodesTriv2; // the number of trivial nodes
94 int nNodesCuts; // the number of rewritten nodes
95 int nNodesTried; // the number of nodes tried
96 abctime timeCuts; // time to compute the cut and its truth table
97 abctime timeHash; // time for hashing cuts
98 abctime timeOther; // other time
99 abctime timeTotal; // total time
100};
101
102static inline int Csw_CutLeaveNum( Csw_Cut_t * pCut ) { return pCut->nFanins; }
103static inline int * Csw_CutLeaves( Csw_Cut_t * pCut ) { return pCut->pFanins; }
104static inline unsigned * Csw_CutTruth( Csw_Cut_t * pCut ) { return (unsigned *)(pCut->pFanins + pCut->nLeafMax); }
105static inline Csw_Cut_t * Csw_CutNext( Csw_Cut_t * pCut ) { return (Csw_Cut_t *)(((char *)pCut) + pCut->nCutSize); }
106
107static inline int Csw_ObjRefs( Csw_Man_t * p, Aig_Obj_t * pObj ) { return p->pnRefs[pObj->Id]; }
108static inline void Csw_ObjAddRefs( Csw_Man_t * p, Aig_Obj_t * pObj, int nRefs ) { p->pnRefs[pObj->Id] += nRefs; }
109
110static inline Csw_Cut_t * Csw_ObjCuts( Csw_Man_t * p, Aig_Obj_t * pObj ) { return p->pCuts[pObj->Id]; }
111static inline void Csw_ObjSetCuts( Csw_Man_t * p, Aig_Obj_t * pObj, Csw_Cut_t * pCuts ) { p->pCuts[pObj->Id] = pCuts; }
112
113static inline Aig_Obj_t * Csw_ObjEquiv( Csw_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquiv[pObj->Id]; }
114static inline void Csw_ObjSetEquiv( Csw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pEquiv ) { p->pEquiv[pObj->Id] = pEquiv; }
115
116static inline Aig_Obj_t * Csw_ObjChild0Equiv( Csw_Man_t * p, Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Csw_ObjEquiv(p, Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL; }
117static inline Aig_Obj_t * Csw_ObjChild1Equiv( Csw_Man_t * p, Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Csw_ObjEquiv(p, Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL; }
118
122
126
127// iterator over cuts of the node
128#define Csw_ObjForEachCut( p, pObj, pCut, i ) \
129 for ( i = 0, pCut = Csw_ObjCuts(p, pObj); i < p->nCutsMax; i++, pCut = Csw_CutNext(pCut) )
130// iterator over leaves of the cut
131#define Csw_CutForEachLeaf( p, pCut, pLeaf, i ) \
132 for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )
133
137
138/*=== cnfCut.c ========================================================*/
139extern Csw_Cut_t * Csw_ObjPrepareCuts( Csw_Man_t * p, Aig_Obj_t * pObj, int fTriv );
140extern Aig_Obj_t * Csw_ObjSweep( Csw_Man_t * p, Aig_Obj_t * pObj, int fTriv );
141/*=== cnfMan.c ========================================================*/
142extern Csw_Man_t * Csw_ManStart( Aig_Man_t * pMan, int nCutsMax, int nLeafMax, int fVerbose );
143extern void Csw_ManStop( Csw_Man_t * p );
144/*=== cnfTable.c ========================================================*/
145extern int Csw_TableCountCuts( Csw_Man_t * p );
146extern void Csw_TableCutInsert( Csw_Man_t * p, Csw_Cut_t * pCut );
147extern Aig_Obj_t * Csw_TableCutLookup( Csw_Man_t * p, Csw_Cut_t * pCut );
148
149
150
152
153
154
155#endif
156
160
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
struct Aig_MmFixed_t_ Aig_MmFixed_t
Definition aig.h:52
Csw_Man_t * Csw_ManStart(Aig_Man_t *pMan, int nCutsMax, int nLeafMax, int fVerbose)
DECLARATIONS ///.
Definition cswMan.c:45
Csw_Cut_t * Csw_ObjPrepareCuts(Csw_Man_t *p, Aig_Obj_t *pObj, int fTriv)
FUNCTION DECLARATIONS ///.
Definition cswCut.c:453
void Csw_TableCutInsert(Csw_Man_t *p, Csw_Cut_t *pCut)
Definition cswTable.c:103
int Csw_TableCountCuts(Csw_Man_t *p)
Definition cswTable.c:82
struct Csw_Cut_t_ Csw_Cut_t
Definition cswInt.h:53
Aig_Obj_t * Csw_ObjSweep(Csw_Man_t *p, Aig_Obj_t *pObj, int fTriv)
Definition cswCut.c:492
Aig_Obj_t * Csw_TableCutLookup(Csw_Man_t *p, Csw_Cut_t *pCut)
Definition cswTable.c:121
typedefABC_NAMESPACE_HEADER_START struct Csw_Man_t_ Csw_Man_t
INCLUDES ///.
Definition cswInt.h:52
void Csw_ManStop(Csw_Man_t *p)
Definition cswMan.c:99
Cube * p
Definition exorList.c:222
int Id
Definition aig.h:85
unsigned uSign
Definition cswInt.h:61
int pFanins[0]
Definition cswInt.h:66
short nCutSize
Definition cswInt.h:63
char nLeafMax
Definition cswInt.h:64
char nFanins
Definition cswInt.h:65
int iNode
Definition cswInt.h:62
int Cost
Definition cswInt.h:59
Csw_Cut_t * pNext
Definition cswInt.h:58
int nNodesTriv0
Definition cswInt.h:91
int * pnRefs
Definition cswInt.h:77
abctime timeHash
Definition cswInt.h:97
int nLeafMax
Definition cswInt.h:83
Aig_MmFixed_t * pMemCuts
Definition cswInt.h:88
int nTruthWords
Definition cswInt.h:87
int nNodesTriv2
Definition cswInt.h:93
abctime timeOther
Definition cswInt.h:98
int nNodesTried
Definition cswInt.h:95
int nNodesCuts
Definition cswInt.h:94
Csw_Cut_t ** pCuts
Definition cswInt.h:76
int nTableSize
Definition cswInt.h:80
Aig_Obj_t ** pEquiv
Definition cswInt.h:75
abctime timeCuts
Definition cswInt.h:96
Aig_Man_t * pManRes
Definition cswInt.h:74
abctime timeTotal
Definition cswInt.h:99
int nCutSize
Definition cswInt.h:86
int nCutsMax
Definition cswInt.h:82
unsigned * puTemp[4]
Definition cswInt.h:89
int fVerbose
Definition cswInt.h:84
Aig_Man_t * pManAig
Definition cswInt.h:73
Csw_Cut_t ** pTable
Definition cswInt.h:79
int nNodesTriv1
Definition cswInt.h:92
#define assert(ex)
Definition util_old.h:213