ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
kitHop.c
Go to the documentation of this file.
1
20
21#include "kit.h"
22#include "aig/hop/hop.h"
23#include "aig/gia/gia.h"
24
26
27
31
35
47int Kit_GraphToGiaInternal( Gia_Man_t * pMan, Kit_Graph_t * pGraph, int fHash )
48{
49 Kit_Node_t * pNode = NULL;
50 int i, pAnd0, pAnd1;
51 // check for constant function
52 if ( Kit_GraphIsConst(pGraph) )
53 return Abc_LitNotCond( 1, Kit_GraphIsComplement(pGraph) );
54 // check for a literal
55 if ( Kit_GraphIsVar(pGraph) )
56 return Abc_LitNotCond( Kit_GraphVar(pGraph)->iFunc, Kit_GraphIsComplement(pGraph) );
57 // build the AIG nodes corresponding to the AND gates of the graph
58 Kit_GraphForEachNode( pGraph, pNode, i )
59 {
60 pAnd0 = Abc_LitNotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->iFunc, pNode->eEdge0.fCompl );
61 pAnd1 = Abc_LitNotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->iFunc, pNode->eEdge1.fCompl );
62 if ( fHash )
63 pNode->iFunc = Gia_ManHashAnd( pMan, pAnd0, pAnd1 );
64 else
65 pNode->iFunc = Gia_ManAppendAnd2( pMan, pAnd0, pAnd1 );
66 }
67 // complement the result if necessary
68 return Abc_LitNotCond( pNode->iFunc, Kit_GraphIsComplement(pGraph) );
69}
70int Kit_GraphToGia( Gia_Man_t * pMan, Kit_Graph_t * pGraph, Vec_Int_t * vLeaves, int fHash )
71{
72 Kit_Node_t * pNode = NULL;
73 int i;
74 // collect the fanins
75 Kit_GraphForEachLeaf( pGraph, pNode, i )
76 pNode->iFunc = vLeaves ? Vec_IntEntry(vLeaves, i) : Gia_Obj2Lit(pMan, Gia_ManPi(pMan, i));
77 // perform strashing
78 return Kit_GraphToGiaInternal( pMan, pGraph, fHash );
79}
80int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash )
81{
82 int iLit;
83 Kit_Graph_t * pGraph;
84 // transform truth table into the decomposition tree
85 if ( vMemory == NULL )
86 {
87 vMemory = Vec_IntAlloc( 0 );
88 pGraph = Kit_TruthToGraph( pTruth, nVars, vMemory );
89 Vec_IntFree( vMemory );
90 }
91 else
92 pGraph = Kit_TruthToGraph( pTruth, nVars, vMemory );
93 if ( pGraph == NULL )
94 {
95 printf( "Kit_TruthToGia(): Converting truth table to AIG has failed for function:\n" );
96 Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
97 }
98 // derive the AIG for the decomposition tree
99 iLit = Kit_GraphToGia( pMan, pGraph, vLeaves, fHash );
100 Kit_GraphFree( pGraph );
101 return iLit;
102}
103int Kit_TruthToGia2( Gia_Man_t * pMan, unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash )
104{
105 int iLit;
106 Kit_Graph_t * pGraph;
107 // transform truth table into the decomposition tree
108 if ( vMemory == NULL )
109 {
110 vMemory = Vec_IntAlloc( 0 );
111 pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory );
112 Vec_IntFree( vMemory );
113 }
114 else
115 pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory );
116 if ( pGraph == NULL )
117 {
118 printf( "Kit_TruthToGia2(): Converting truth table to AIG has failed for function:\n" );
119 Kit_DsdPrintFromTruth( pTruth0, nVars ); printf( "\n" );
120 Kit_DsdPrintFromTruth( pTruth1, nVars ); printf( "\n" );
121 }
122 // derive the AIG for the decomposition tree
123 iLit = Kit_GraphToGia( pMan, pGraph, vLeaves, fHash );
124 Kit_GraphFree( pGraph );
125 return iLit;
126}
127
139int Kit_IsopNodeNum( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory )
140{
141 Kit_Graph_t * pGraph;
142 int nNodes;
143 // transform truth table into the decomposition tree
144 if ( vMemory == NULL )
145 {
146 vMemory = Vec_IntAlloc( 0 );
147 pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory );
148 Vec_IntFree( vMemory );
149 }
150 else
151 pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory );
152 if ( pGraph == NULL )
153 {
154 printf( "Kit_TruthToGia2(): Converting truth table to AIG has failed for function:\n" );
155 Kit_DsdPrintFromTruth( pTruth0, nVars ); printf( "\n" );
156 Kit_DsdPrintFromTruth( pTruth1, nVars ); printf( "\n" );
157 }
158 // derive the AIG for the decomposition tree
159 nNodes = Kit_GraphNodeNum( pGraph );
160 Kit_GraphFree( pGraph );
161 return nNodes;
162}
163
175void Kit_IsopResubInt( Kit_Graph_t * pGraph, Vec_Int_t * vRes )
176{
177 int nVars = Kit_GraphLeaveNum(pGraph);
178 assert( nVars >= 0 && nVars <= pGraph->nSize );
179 if ( Kit_GraphIsConst(pGraph) )
180 Vec_IntPush( vRes, Kit_GraphIsConst1(pGraph) );
181 else if ( Kit_GraphIsVar(pGraph) )
182 Vec_IntPush( vRes, 4 + Abc_Var2Lit(Kit_GraphVarInt(pGraph), Kit_GraphIsComplement(pGraph)) );
183 else
184 {
185 Kit_Node_t * pNode = NULL; int i;
186 Kit_GraphForEachNode( pGraph, pNode, i )
187 {
188 Kit_Node_t * pFan0 = Kit_GraphNodeFanin0( pGraph, pNode );
189 Kit_Node_t * pFan1 = Kit_GraphNodeFanin1( pGraph, pNode );
190 int iLit0 = Abc_Var2Lit( Kit_GraphNodeInt(pGraph, pFan0), pNode->eEdge0.fCompl );
191 int iLit1 = Abc_Var2Lit( Kit_GraphNodeInt(pGraph, pFan1), pNode->eEdge1.fCompl );
192 if ( iLit0 > iLit1 )
193 iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
194 Vec_IntPushTwo( vRes, 4 + iLit0, 4 + iLit1 );
195 }
196 assert( pNode == Kit_GraphNode(pGraph, pGraph->eRoot.Node) );
197 Vec_IntPush( vRes, 4 + Abc_Var2Lit(Kit_GraphNodeInt(pGraph, pNode), Kit_GraphIsComplement(pGraph)) );
198 }
199}
200Vec_Int_t * Kit_IsopResub( unsigned * pTruth0, unsigned * pTruth1, int nVars, Vec_Int_t * vMemory )
201{
202 Vec_Int_t * vRes = NULL;
203 Kit_Graph_t * pGraph;
204 int nNodes;
205 // transform truth table into the decomposition tree
206 if ( vMemory == NULL )
207 {
208 vMemory = Vec_IntAlloc( 0 );
209 pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory );
210 Vec_IntFree( vMemory );
211 }
212 else
213 pGraph = Kit_TruthToGraph2( pTruth0, pTruth1, nVars, vMemory );
214 if ( pGraph == NULL )
215 {
216 printf( "Kit_TruthToGia2(): Converting truth table to AIG has failed for function:\n" );
217 Kit_DsdPrintFromTruth( pTruth0, nVars ); printf( "\n" );
218 Kit_DsdPrintFromTruth( pTruth1, nVars ); printf( "\n" );
219 }
220 // derive the AIG for the decomposition tree
221 nNodes = Kit_GraphNodeNum( pGraph );
222 vRes = Vec_IntAlloc( 2*nNodes + 1 );
223 Kit_IsopResubInt( pGraph, vRes );
224 assert( Vec_IntSize(vRes) == 2*nNodes + 1 );
225 Kit_GraphFree( pGraph );
226 return vRes;
227}
228
241{
242 Kit_Node_t * pNode = NULL;
243 Hop_Obj_t * pAnd0, * pAnd1;
244 int i;
245 // check for constant function
246 if ( Kit_GraphIsConst(pGraph) )
247 return Hop_NotCond( Hop_ManConst1(pMan), Kit_GraphIsComplement(pGraph) );
248 // check for a literal
249 if ( Kit_GraphIsVar(pGraph) )
250 return Hop_NotCond( (Hop_Obj_t *)Kit_GraphVar(pGraph)->pFunc, Kit_GraphIsComplement(pGraph) );
251 // build the AIG nodes corresponding to the AND gates of the graph
252 Kit_GraphForEachNode( pGraph, pNode, i )
253 {
254 pAnd0 = Hop_NotCond( (Hop_Obj_t *)Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
255 pAnd1 = Hop_NotCond( (Hop_Obj_t *)Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
256 pNode->pFunc = Hop_And( pMan, pAnd0, pAnd1 );
257 }
258 // complement the result if necessary
259 return Hop_NotCond( (Hop_Obj_t *)pNode->pFunc, Kit_GraphIsComplement(pGraph) );
260}
262{
263 Kit_Node_t * pNode = NULL;
264 int i;
265 // collect the fanins
266 Kit_GraphForEachLeaf( pGraph, pNode, i )
267 pNode->pFunc = Hop_IthVar( pMan, i );
268 // perform strashing
269 return Kit_GraphToHopInternal( pMan, pGraph );
270}
271Hop_Obj_t * Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory )
272{
273 Hop_Obj_t * pObj;
274 Kit_Graph_t * pGraph;
275 // transform truth table into the decomposition tree
276 if ( vMemory == NULL )
277 {
278 vMemory = Vec_IntAlloc( 0 );
279 pGraph = Kit_TruthToGraph( pTruth, nVars, vMemory );
280 Vec_IntFree( vMemory );
281 }
282 else
283 pGraph = Kit_TruthToGraph( pTruth, nVars, vMemory );
284 if ( pGraph == NULL )
285 {
286 printf( "Kit_TruthToHop(): Converting truth table to AIG has failed for function:\n" );
287 Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
288 }
289 // derive the AIG for the decomposition tree
290 pObj = Kit_GraphToHop( pMan, pGraph );
291 Kit_GraphFree( pGraph );
292 return pObj;
293}
294
306Hop_Obj_t * Kit_CoverToHop( Hop_Man_t * pMan, Vec_Int_t * vCover, int nVars, Vec_Int_t * vMemory )
307{
308 Kit_Graph_t * pGraph;
309 Hop_Obj_t * pFunc;
310 // perform factoring
311 Vec_IntClear( vMemory );
312 pGraph = Kit_SopFactor( vCover, 0, nVars, vMemory );
313 // convert graph to the AIG
314 pFunc = Kit_GraphToHop( pMan, pGraph );
315 Kit_GraphFree( pGraph );
316 return pFunc;
317}
318
322
323
325
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:576
typedefABC_NAMESPACE_HEADER_START struct Hop_Man_t_ Hop_Man_t
INCLUDES ///.
Definition hop.h:49
Hop_Obj_t * Hop_IthVar(Hop_Man_t *p, int i)
FUNCTION DEFINITIONS ///.
Definition hopOper.c:63
Hop_Obj_t * Hop_And(Hop_Man_t *p, Hop_Obj_t *p0, Hop_Obj_t *p1)
Definition hopOper.c:104
struct Hop_Obj_t_ Hop_Obj_t
Definition hop.h:50
Hop_Obj_t * Kit_GraphToHop(Hop_Man_t *pMan, Kit_Graph_t *pGraph)
Definition kitHop.c:261
int Kit_GraphToGia(Gia_Man_t *pMan, Kit_Graph_t *pGraph, Vec_Int_t *vLeaves, int fHash)
Definition kitHop.c:70
Hop_Obj_t * Kit_GraphToHopInternal(Hop_Man_t *pMan, Kit_Graph_t *pGraph)
Definition kitHop.c:240
ABC_NAMESPACE_IMPL_START int Kit_GraphToGiaInternal(Gia_Man_t *pMan, Kit_Graph_t *pGraph, int fHash)
DECLARATIONS ///.
Definition kitHop.c:47
int Kit_TruthToGia2(Gia_Man_t *pMan, unsigned *pTruth0, unsigned *pTruth1, int nVars, Vec_Int_t *vMemory, Vec_Int_t *vLeaves, int fHash)
Definition kitHop.c:103
Hop_Obj_t * Kit_TruthToHop(Hop_Man_t *pMan, unsigned *pTruth, int nVars, Vec_Int_t *vMemory)
Definition kitHop.c:271
int Kit_TruthToGia(Gia_Man_t *pMan, unsigned *pTruth, int nVars, Vec_Int_t *vMemory, Vec_Int_t *vLeaves, int fHash)
DECLARATIONS ///.
Definition kitHop.c:80
Vec_Int_t * Kit_IsopResub(unsigned *pTruth0, unsigned *pTruth1, int nVars, Vec_Int_t *vMemory)
Definition kitHop.c:200
Hop_Obj_t * Kit_CoverToHop(Hop_Man_t *pMan, Vec_Int_t *vCover, int nVars, Vec_Int_t *vMemory)
Definition kitHop.c:306
void Kit_IsopResubInt(Kit_Graph_t *pGraph, Vec_Int_t *vRes)
Definition kitHop.c:175
int Kit_IsopNodeNum(unsigned *pTruth0, unsigned *pTruth1, int nVars, Vec_Int_t *vMemory)
Definition kitHop.c:139
#define Kit_GraphForEachNode(pGraph, pAnd, i)
Definition kit.h:507
struct Kit_Graph_t_ Kit_Graph_t
Definition kit.h:88
Kit_Graph_t * Kit_SopFactor(Vec_Int_t *vCover, int fCompl, int nVars, Vec_Int_t *vMemory)
FUNCTION DEFINITIONS ///.
Definition kitFactor.c:55
Kit_Graph_t * Kit_TruthToGraph2(unsigned *pTruth0, unsigned *pTruth1, int nVars, Vec_Int_t *vMemory)
Definition kitGraph.c:384
struct Kit_Node_t_ Kit_Node_t
Definition kit.h:69
void Kit_DsdPrintFromTruth(unsigned *pTruth, int nVars)
Definition kitDsd.c:491
void Kit_GraphFree(Kit_Graph_t *pGraph)
Definition kitGraph.c:132
#define Kit_GraphForEachLeaf(pGraph, pLeaf, i)
Definition kit.h:505
Kit_Graph_t * Kit_TruthToGraph(unsigned *pTruth, int nVars, Vec_Int_t *vMemory)
Definition kitGraph.c:356
unsigned fCompl
Definition kit.h:65
unsigned Node
Definition kit.h:66
Kit_Edge_t eRoot
Definition kit.h:96
Kit_Edge_t eEdge0
Definition kit.h:72
Kit_Edge_t eEdge1
Definition kit.h:73
void * pFunc
Definition kit.h:76
int iFunc
Definition kit.h:75
#define assert(ex)
Definition util_old.h:213