1 /**CFile****************************************************************
2
3 FileName [abcMiter.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Network and node package.]
8
9 Synopsis [Procedures to derive the miter of two circuits.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: abcMiter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "base/abc/abc.h"
22 #include "base/io/ioAbc.h"
23 #include "sat/cnf/cnf.h"
24 #include "sat/bsat/satStore.h"
25
26 ABC_NAMESPACE_IMPL_START
27
28
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32
33 static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize, int fImplic, int fMulti );
34 static void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize, int fMulti );
35 static void Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter );
36 static void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize, int fImplic, int fMulti );
37 static void Abc_NtkAddFrame( Abc_Ntk_t * pNetNew, Abc_Ntk_t * pNet, int iFrame );
38
39 // to be exported
40 typedef void (*AddFrameMapping)( Abc_Obj_t*, Abc_Obj_t*, int, void*);
41 extern Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFrameMapping addFrameMapping, void* arg );
42 static void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vNodes, AddFrameMapping addFrameMapping, void* arg );
43
44 ////////////////////////////////////////////////////////////////////////
45 /// FUNCTION DEFINITIONS ///
46 ////////////////////////////////////////////////////////////////////////
47
48 /**Function*************************************************************
49
50 Synopsis [Derives the miter of two networks.]
51
52 Description [Preprocesses the networks to make sure that they are strashed.]
53
54 SideEffects []
55
56 SeeAlso []
57
58 ***********************************************************************/
Abc_NtkMiter(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,int fComb,int nPartSize,int fImplic,int fMulti)59 Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize, int fImplic, int fMulti )
60 {
61 Abc_Ntk_t * pTemp = NULL;
62 int fRemove1, fRemove2;
63 assert( Abc_NtkHasOnlyLatchBoxes(pNtk1) );
64 assert( Abc_NtkHasOnlyLatchBoxes(pNtk2) );
65 // check that the networks have the same PIs/POs/latches
66 if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, fImplic, fComb ) )
67 return NULL;
68 // make sure the circuits are strashed
69 fRemove1 = (!Abc_NtkIsStrash(pNtk1) || Abc_NtkGetChoiceNum(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0, 0));
70 fRemove2 = (!Abc_NtkIsStrash(pNtk2) || Abc_NtkGetChoiceNum(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0, 0));
71 if ( pNtk1 && pNtk2 )
72 pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb, nPartSize, fImplic, fMulti );
73 if ( fRemove1 ) Abc_NtkDelete( pNtk1 );
74 if ( fRemove2 ) Abc_NtkDelete( pNtk2 );
75 return pTemp;
76 }
77
78 /**Function*************************************************************
79
80 Synopsis [Derives the miter of two sequential networks.]
81
82 Description [Assumes that the networks are strashed.]
83
84 SideEffects []
85
86 SeeAlso []
87
88 ***********************************************************************/
Abc_NtkMiterInt(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,int fComb,int nPartSize,int fImplic,int fMulti)89 Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize, int fImplic, int fMulti )
90 {
91 char Buffer[1000];
92 Abc_Ntk_t * pNtkMiter;
93
94 assert( Abc_NtkIsStrash(pNtk1) );
95 assert( Abc_NtkIsStrash(pNtk2) );
96
97 // start the new network
98 pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
99 sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
100 pNtkMiter->pName = Extra_UtilStrsav(Buffer);
101
102 // perform strashing
103 Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize, fMulti );
104 Abc_NtkMiterAddOne( pNtk1, pNtkMiter );
105 Abc_NtkMiterAddOne( pNtk2, pNtkMiter );
106 Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize, fImplic, fMulti );
107 Abc_AigCleanup((Abc_Aig_t *)pNtkMiter->pManFunc);
108
109 // make sure that everything is okay
110 if ( !Abc_NtkCheck( pNtkMiter ) )
111 {
112 printf( "Abc_NtkMiter: The network check has failed.\n" );
113 Abc_NtkDelete( pNtkMiter );
114 return NULL;
115 }
116 return pNtkMiter;
117 }
118
119 /**Function*************************************************************
120
121 Synopsis [Prepares the network for mitering.]
122
123 Description []
124
125 SideEffects []
126
127 SeeAlso []
128
129 ***********************************************************************/
Abc_NtkMiterPrepare(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,Abc_Ntk_t * pNtkMiter,int fComb,int nPartSize,int fMulti)130 void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize, int fMulti )
131 {
132 Abc_Obj_t * pObj, * pObjNew;
133 int i;
134 // clean the copy field in all objects
135 // Abc_NtkCleanCopy( pNtk1 );
136 // Abc_NtkCleanCopy( pNtk2 );
137 Abc_AigConst1(pNtk1)->pCopy = Abc_AigConst1(pNtkMiter);
138 Abc_AigConst1(pNtk2)->pCopy = Abc_AigConst1(pNtkMiter);
139
140 if ( fComb )
141 {
142 // create new PIs and remember them in the old PIs
143 Abc_NtkForEachCi( pNtk1, pObj, i )
144 {
145 pObjNew = Abc_NtkCreatePi( pNtkMiter );
146 // remember this PI in the old PIs
147 pObj->pCopy = pObjNew;
148 pObj = Abc_NtkCi(pNtk2, i);
149 pObj->pCopy = pObjNew;
150 // add name
151 Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), NULL );
152 }
153 if ( nPartSize <= 0 )
154 {
155 // create POs
156 if ( fMulti )
157 {
158 Abc_NtkForEachCo( pNtk1, pObj, i )
159 {
160 pObjNew = Abc_NtkCreatePo( pNtkMiter );
161 Abc_ObjAssignName( pObjNew, "miter", Abc_ObjName(pObjNew) );
162 }
163
164 }
165 else
166 {
167 pObjNew = Abc_NtkCreatePo( pNtkMiter );
168 Abc_ObjAssignName( pObjNew, "miter", NULL );
169 }
170 }
171 }
172 else
173 {
174 // create new PIs and remember them in the old PIs
175 Abc_NtkForEachPi( pNtk1, pObj, i )
176 {
177 pObjNew = Abc_NtkCreatePi( pNtkMiter );
178 // remember this PI in the old PIs
179 pObj->pCopy = pObjNew;
180 pObj = Abc_NtkPi(pNtk2, i);
181 pObj->pCopy = pObjNew;
182 // add name
183 Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), NULL );
184 }
185 if ( nPartSize <= 0 )
186 {
187 // create POs
188 if ( fMulti )
189 {
190 Abc_NtkForEachPo( pNtk1, pObj, i )
191 {
192 pObjNew = Abc_NtkCreatePo( pNtkMiter );
193 Abc_ObjAssignName( pObjNew, "miter", Abc_ObjName(pObjNew) );
194 }
195
196 }
197 else
198 {
199 pObjNew = Abc_NtkCreatePo( pNtkMiter );
200 Abc_ObjAssignName( pObjNew, "miter", NULL );
201 }
202 }
203 // create the latches
204 Abc_NtkForEachLatch( pNtk1, pObj, i )
205 {
206 pObjNew = Abc_NtkDupBox( pNtkMiter, pObj, 0 );
207 // add names
208 Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), "_1" );
209 Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjName(Abc_ObjFanin0(pObj)), "_1" );
210 Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pObj)), "_1" );
211 }
212 Abc_NtkForEachLatch( pNtk2, pObj, i )
213 {
214 pObjNew = Abc_NtkDupBox( pNtkMiter, pObj, 0 );
215 // add name
216 Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), "_2" );
217 Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjName(Abc_ObjFanin0(pObj)), "_2" );
218 Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pObj)), "_2" );
219 }
220 }
221 }
222
223 /**Function*************************************************************
224
225 Synopsis [Performs mitering for one network.]
226
227 Description []
228
229 SideEffects []
230
231 SeeAlso []
232
233 ***********************************************************************/
Abc_NtkMiterAddOne(Abc_Ntk_t * pNtk,Abc_Ntk_t * pNtkMiter)234 void Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter )
235 {
236 Abc_Obj_t * pNode;
237 int i;
238 assert( Abc_NtkIsDfsOrdered(pNtk) );
239 Abc_AigForEachAnd( pNtk, pNode, i )
240 pNode->pCopy = Abc_AigAnd( (Abc_Aig_t *)pNtkMiter->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
241 }
242
243 /**Function*************************************************************
244
245 Synopsis [Performs mitering for one network.]
246
247 Description []
248
249 SideEffects []
250
251 SeeAlso []
252
253 ***********************************************************************/
Abc_NtkMiterAddCone(Abc_Ntk_t * pNtk,Abc_Ntk_t * pNtkMiter,Abc_Obj_t * pRoot)254 void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pRoot )
255 {
256 Vec_Ptr_t * vNodes;
257 Abc_Obj_t * pNode;
258 int i;
259 // map the constant nodes
260 Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkMiter);
261 // perform strashing
262 vNodes = Abc_NtkDfsNodes( pNtk, &pRoot, 1 );
263 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
264 if ( Abc_AigNodeIsAnd(pNode) )
265 pNode->pCopy = Abc_AigAnd( (Abc_Aig_t *)pNtkMiter->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
266 Vec_PtrFree( vNodes );
267 }
268
269
270 /**Function*************************************************************
271
272 Synopsis [Finalizes the miter by adding the output part.]
273
274 Description []
275
276 SideEffects []
277
278 SeeAlso []
279
280 ***********************************************************************/
Abc_NtkMiterFinalize(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,Abc_Ntk_t * pNtkMiter,int fComb,int nPartSize,int fImplic,int fMulti)281 void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize, int fImplic, int fMulti )
282 {
283 Vec_Ptr_t * vPairs;
284 Abc_Obj_t * pMiter, * pNode;
285 int i;
286 assert( nPartSize == 0 || fMulti == 0 );
287 // collect the PO pairs from both networks
288 vPairs = Vec_PtrAlloc( 100 );
289 if ( fComb )
290 {
291 // collect the CO nodes for the miter
292 Abc_NtkForEachCo( pNtk1, pNode, i )
293 {
294 if ( fMulti )
295 {
296 pMiter = Abc_AigXor( (Abc_Aig_t *)pNtkMiter->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild0Copy(Abc_NtkCo(pNtk2, i)) );
297 Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,i), pMiter );
298 }
299 else
300 {
301 Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pNode) );
302 pNode = Abc_NtkCo( pNtk2, i );
303 Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pNode) );
304 }
305 }
306 }
307 else
308 {
309 // collect the PO nodes for the miter
310 Abc_NtkForEachPo( pNtk1, pNode, i )
311 {
312 if ( fMulti )
313 {
314 pMiter = Abc_AigXor( (Abc_Aig_t *)pNtkMiter->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild0Copy(Abc_NtkCo(pNtk2, i)) );
315 Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,i), pMiter );
316 }
317 else
318 {
319 Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pNode) );
320 pNode = Abc_NtkPo( pNtk2, i );
321 Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pNode) );
322 }
323 }
324 // connect new latches
325 Abc_NtkForEachLatch( pNtk1, pNode, i )
326 Abc_ObjAddFanin( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjChild0Copy(Abc_ObjFanin0(pNode)) );
327 Abc_NtkForEachLatch( pNtk2, pNode, i )
328 Abc_ObjAddFanin( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjChild0Copy(Abc_ObjFanin0(pNode)) );
329 }
330 // add the miter
331 if ( nPartSize <= 0 )
332 {
333 if ( !fMulti )
334 {
335 pMiter = Abc_AigMiter( (Abc_Aig_t *)pNtkMiter->pManFunc, vPairs, fImplic );
336 Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
337 }
338 }
339 else
340 {
341 char Buffer[1024];
342 Vec_Ptr_t * vPairsPart;
343 int nParts, i, k, iCur;
344 assert( Vec_PtrSize(vPairs) == 2 * Abc_NtkCoNum(pNtk1) );
345 // create partitions
346 nParts = Abc_NtkCoNum(pNtk1) / nPartSize + (int)((Abc_NtkCoNum(pNtk1) % nPartSize) > 0);
347 vPairsPart = Vec_PtrAlloc( nPartSize );
348 for ( i = 0; i < nParts; i++ )
349 {
350 Vec_PtrClear( vPairsPart );
351 for ( k = 0; k < nPartSize; k++ )
352 {
353 iCur = i * nPartSize + k;
354 if ( iCur >= Abc_NtkCoNum(pNtk1) )
355 break;
356 Vec_PtrPush( vPairsPart, Vec_PtrEntry(vPairs, 2*iCur ) );
357 Vec_PtrPush( vPairsPart, Vec_PtrEntry(vPairs, 2*iCur+1) );
358 }
359 pMiter = Abc_AigMiter( (Abc_Aig_t *)pNtkMiter->pManFunc, vPairsPart, fImplic );
360 pNode = Abc_NtkCreatePo( pNtkMiter );
361 Abc_ObjAddFanin( pNode, pMiter );
362 // assign the name to the node
363 if ( nPartSize == 1 )
364 sprintf( Buffer, "%s", Abc_ObjName(Abc_NtkCo(pNtk1,i)) );
365 else
366 sprintf( Buffer, "%d", i );
367 Abc_ObjAssignName( pNode, "miter_", Buffer );
368 }
369 Vec_PtrFree( vPairsPart );
370 }
371 Vec_PtrFree( vPairs );
372 }
373
374
375
376 /**Function*************************************************************
377
378 Synopsis [Derives the AND of two miters.]
379
380 Description [The network should have the same names of PIs.]
381
382 SideEffects []
383
384 SeeAlso []
385
386 ***********************************************************************/
Abc_NtkMiterAnd(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,int fOr,int fCompl2)387 Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOr, int fCompl2 )
388 {
389 char Buffer[1000];
390 Abc_Ntk_t * pNtkMiter;
391 Abc_Obj_t * pOutput1, * pOutput2;
392 Abc_Obj_t * pRoot1, * pRoot2, * pMiter;
393
394 assert( Abc_NtkIsStrash(pNtk1) );
395 assert( Abc_NtkIsStrash(pNtk2) );
396 assert( 1 == Abc_NtkCoNum(pNtk1) );
397 assert( 1 == Abc_NtkCoNum(pNtk2) );
398 assert( 0 == Abc_NtkLatchNum(pNtk1) );
399 assert( 0 == Abc_NtkLatchNum(pNtk2) );
400 assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) );
401 assert( Abc_NtkHasOnlyLatchBoxes(pNtk1) );
402 assert( Abc_NtkHasOnlyLatchBoxes(pNtk2) );
403
404 // start the new network
405 pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
406 // sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
407 sprintf( Buffer, "product" );
408 pNtkMiter->pName = Extra_UtilStrsav(Buffer);
409
410 // perform strashing
411 Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, 1, -1, 0 );
412 Abc_NtkMiterAddOne( pNtk1, pNtkMiter );
413 Abc_NtkMiterAddOne( pNtk2, pNtkMiter );
414 // Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, 1 );
415 pRoot1 = Abc_NtkPo(pNtk1,0);
416 pRoot2 = Abc_NtkPo(pNtk2,0);
417 pOutput1 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot1)->pCopy, Abc_ObjFaninC0(pRoot1) );
418 pOutput2 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot2)->pCopy, (int)Abc_ObjFaninC0(pRoot2) ^ fCompl2 );
419
420 // create the miter of the two outputs
421 if ( fOr )
422 pMiter = Abc_AigOr( (Abc_Aig_t *)pNtkMiter->pManFunc, pOutput1, pOutput2 );
423 else
424 pMiter = Abc_AigAnd( (Abc_Aig_t *)pNtkMiter->pManFunc, pOutput1, pOutput2 );
425 Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
426
427 // make sure that everything is okay
428 if ( !Abc_NtkCheck( pNtkMiter ) )
429 {
430 printf( "Abc_NtkMiterAnd: The network check has failed.\n" );
431 Abc_NtkDelete( pNtkMiter );
432 return NULL;
433 }
434 return pNtkMiter;
435 }
436
437
438 /**Function*************************************************************
439
440 Synopsis [Derives the cofactor of the miter w.r.t. the set of vars.]
441
442 Description [The array of variable values contains -1/0/1 for each PI.
443 -1 means this PI remains, 0/1 means this PI is set to 0/1.]
444
445 SideEffects []
446
447 SeeAlso []
448
449 ***********************************************************************/
Abc_NtkMiterCofactor(Abc_Ntk_t * pNtk,Vec_Int_t * vPiValues)450 Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues )
451 {
452 char Buffer[1000];
453 Abc_Ntk_t * pNtkMiter;
454 Abc_Obj_t * pRoot, * pOutput1;
455 int Value, i;
456
457 assert( Abc_NtkIsStrash(pNtk) );
458 assert( 1 == Abc_NtkCoNum(pNtk) );
459 assert( Abc_NtkHasOnlyLatchBoxes(pNtk) );
460
461 // start the new network
462 pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
463 sprintf( Buffer, "%s_miter", pNtk->pName );
464 pNtkMiter->pName = Extra_UtilStrsav(Buffer);
465
466 // get the root output
467 pRoot = Abc_NtkCo( pNtk, 0 );
468
469 // perform strashing
470 Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1, -1, 0 );
471 // set the first cofactor
472 Vec_IntForEachEntry( vPiValues, Value, i )
473 {
474 if ( Value == -1 )
475 continue;
476 if ( Value == 0 )
477 {
478 Abc_NtkCi(pNtk, i)->pCopy = Abc_ObjNot( Abc_AigConst1(pNtkMiter) );
479 continue;
480 }
481 if ( Value == 1 )
482 {
483 Abc_NtkCi(pNtk, i)->pCopy = Abc_AigConst1(pNtkMiter);
484 continue;
485 }
486 assert( 0 );
487 }
488 // add the first cofactor
489 Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot );
490
491 // save the output
492 pOutput1 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot)->pCopy, Abc_ObjFaninC0(pRoot) );
493
494 // create the miter of the two outputs
495 Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pOutput1 );
496
497 // make sure that everything is okay
498 if ( !Abc_NtkCheck( pNtkMiter ) )
499 {
500 printf( "Abc_NtkMiterCofactor: The network check has failed.\n" );
501 Abc_NtkDelete( pNtkMiter );
502 return NULL;
503 }
504 return pNtkMiter;
505 }
506 /**Function*************************************************************
507
508 Synopsis [Derives the miter of two cofactors of one output.]
509
510 Description []
511
512 SideEffects []
513
514 SeeAlso []
515
516 ***********************************************************************/
Abc_NtkMiterForCofactors(Abc_Ntk_t * pNtk,int Out,int In1,int In2)517 Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 )
518 {
519 char Buffer[1000];
520 Abc_Ntk_t * pNtkMiter;
521 Abc_Obj_t * pRoot, * pOutput1, * pOutput2, * pMiter;
522
523 assert( Abc_NtkIsStrash(pNtk) );
524 assert( Out < Abc_NtkCoNum(pNtk) );
525 assert( In1 < Abc_NtkCiNum(pNtk) );
526 assert( In2 < Abc_NtkCiNum(pNtk) );
527 assert( Abc_NtkHasOnlyLatchBoxes(pNtk) );
528
529 // start the new network
530 pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
531 sprintf( Buffer, "%s_miter", Abc_ObjName(Abc_NtkCo(pNtk, Out)) );
532 pNtkMiter->pName = Extra_UtilStrsav(Buffer);
533
534 // get the root output
535 pRoot = Abc_NtkCo( pNtk, Out );
536
537 // perform strashing
538 Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1, -1, 0 );
539 // set the first cofactor
540 Abc_NtkCi(pNtk, In1)->pCopy = Abc_ObjNot( Abc_AigConst1(pNtkMiter) );
541 if ( In2 >= 0 )
542 Abc_NtkCi(pNtk, In2)->pCopy = Abc_AigConst1(pNtkMiter);
543 // add the first cofactor
544 Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot );
545
546 // save the output
547 pOutput1 = Abc_ObjFanin0(pRoot)->pCopy;
548
549 // set the second cofactor
550 Abc_NtkCi(pNtk, In1)->pCopy = Abc_AigConst1(pNtkMiter);
551 if ( In2 >= 0 )
552 Abc_NtkCi(pNtk, In2)->pCopy = Abc_ObjNot( Abc_AigConst1(pNtkMiter) );
553 // add the second cofactor
554 Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot );
555
556 // save the output
557 pOutput2 = Abc_ObjFanin0(pRoot)->pCopy;
558
559 // create the miter of the two outputs
560 pMiter = Abc_AigXor( (Abc_Aig_t *)pNtkMiter->pManFunc, pOutput1, pOutput2 );
561 Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
562
563 // make sure that everything is okay
564 if ( !Abc_NtkCheck( pNtkMiter ) )
565 {
566 printf( "Abc_NtkMiter: The network check has failed.\n" );
567 Abc_NtkDelete( pNtkMiter );
568 return NULL;
569 }
570 return pNtkMiter;
571 }
572
573
574 /**Function*************************************************************
575
576 Synopsis [Derives the miter of two cofactors of one output.]
577
578 Description []
579
580 SideEffects []
581
582 SeeAlso []
583
584 ***********************************************************************/
Abc_NtkMiterQuantify(Abc_Ntk_t * pNtk,int In,int fExist)585 Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist )
586 {
587 Abc_Ntk_t * pNtkMiter;
588 Abc_Obj_t * pRoot, * pOutput1, * pOutput2, * pMiter;
589
590 assert( Abc_NtkIsStrash(pNtk) );
591 assert( 1 == Abc_NtkCoNum(pNtk) );
592 assert( In < Abc_NtkCiNum(pNtk) );
593 assert( Abc_NtkHasOnlyLatchBoxes(pNtk) );
594
595 // start the new network
596 pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
597 pNtkMiter->pName = Extra_UtilStrsav( Abc_ObjName(Abc_NtkCo(pNtk, 0)) );
598
599 // get the root output
600 pRoot = Abc_NtkCo( pNtk, 0 );
601
602 // perform strashing
603 Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1, -1, 0 );
604 // set the first cofactor
605 Abc_NtkCi(pNtk, In)->pCopy = Abc_ObjNot( Abc_AigConst1(pNtkMiter) );
606 // add the first cofactor
607 Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot );
608 // save the output
609 // pOutput1 = Abc_ObjFanin0(pRoot)->pCopy;
610 pOutput1 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot)->pCopy, Abc_ObjFaninC0(pRoot) );
611
612 // set the second cofactor
613 Abc_NtkCi(pNtk, In)->pCopy = Abc_AigConst1(pNtkMiter);
614 // add the second cofactor
615 Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot );
616 // save the output
617 // pOutput2 = Abc_ObjFanin0(pRoot)->pCopy;
618 pOutput2 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot)->pCopy, Abc_ObjFaninC0(pRoot) );
619
620 // create the miter of the two outputs
621 if ( fExist )
622 pMiter = Abc_AigOr( (Abc_Aig_t *)pNtkMiter->pManFunc, pOutput1, pOutput2 );
623 else
624 pMiter = Abc_AigAnd( (Abc_Aig_t *)pNtkMiter->pManFunc, pOutput1, pOutput2 );
625 Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
626
627 // make sure that everything is okay
628 if ( !Abc_NtkCheck( pNtkMiter ) )
629 {
630 printf( "Abc_NtkMiter: The network check has failed.\n" );
631 Abc_NtkDelete( pNtkMiter );
632 return NULL;
633 }
634 return pNtkMiter;
635 }
636
637 /**Function*************************************************************
638
639 Synopsis [Quantifies all the PIs existentially from the only PO of the network.]
640
641 Description []
642
643 SideEffects []
644
645 SeeAlso []
646
647 ***********************************************************************/
Abc_NtkMiterQuantifyPis(Abc_Ntk_t * pNtk)648 Abc_Ntk_t * Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk )
649 {
650 Abc_Ntk_t * pNtkTemp;
651 Abc_Obj_t * pObj;
652 int i;
653 assert( Abc_NtkHasOnlyLatchBoxes(pNtk) );
654
655 Abc_NtkForEachPi( pNtk, pObj, i )
656 {
657 if ( Abc_ObjFanoutNum(pObj) == 0 )
658 continue;
659 pNtk = Abc_NtkMiterQuantify( pNtkTemp = pNtk, i, 1 );
660 Abc_NtkDelete( pNtkTemp );
661 }
662
663 return pNtk;
664 }
665
666
667
668
669 /**Function*************************************************************
670
671 Synopsis [Checks the status of the miter.]
672
673 Description [Return 0 if the miter is sat for at least one output.
674 Return 1 if the miter is unsat for all its outputs. Returns -1 if the
675 miter is undecided for some outputs.]
676
677 SideEffects []
678
679 SeeAlso []
680
681 ***********************************************************************/
Abc_NtkMiterIsConstant(Abc_Ntk_t * pMiter)682 int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter )
683 {
684 Abc_Obj_t * pNodePo, * pChild;
685 int i;
686 assert( Abc_NtkIsStrash(pMiter) );
687 Abc_NtkForEachPo( pMiter, pNodePo, i )
688 {
689 pChild = Abc_ObjChild0( pNodePo );
690 // check if the output is constant 1
691 if ( Abc_AigNodeIsConst(pChild) )
692 {
693 assert( Abc_ObjRegular(pChild) == Abc_AigConst1(pMiter) );
694 if ( !Abc_ObjIsComplement(pChild) )
695 {
696 // if the miter is constant 1, return immediately
697 // printf( "MITER IS CONSTANT 1!\n" );
698 return 0;
699 }
700 }
701 /*
702 // check if the output is not constant 0
703 else if ( Abc_ObjRegular(pChild)->fPhase != (unsigned)Abc_ObjIsComplement(pChild) )
704 {
705 return 0;
706 }
707 */
708 // if the miter is undecided (or satisfiable), return immediately
709 else
710 return -1;
711 }
712 // return 1, meaning all outputs are constant zero
713 return 1;
714 }
715
716 /**Function*************************************************************
717
718 Synopsis [Reports the status of the miter.]
719
720 Description []
721
722 SideEffects []
723
724 SeeAlso []
725
726 ***********************************************************************/
Abc_NtkMiterReport(Abc_Ntk_t * pMiter)727 void Abc_NtkMiterReport( Abc_Ntk_t * pMiter )
728 {
729 Abc_Obj_t * pChild, * pNode;
730 int i;
731 if ( Abc_NtkPoNum(pMiter) == 1 )
732 {
733 pChild = Abc_ObjChild0( Abc_NtkPo(pMiter,0) );
734 if ( Abc_AigNodeIsConst(pChild) )
735 {
736 if ( Abc_ObjIsComplement(pChild) )
737 printf( "Unsatisfiable.\n" );
738 else
739 printf( "Satisfiable. (Constant 1).\n" );
740 }
741 else
742 printf( "Satisfiable.\n" );
743 }
744 else
745 {
746 Abc_NtkForEachPo( pMiter, pNode, i )
747 {
748 pChild = Abc_ObjChild0( Abc_NtkPo(pMiter,i) );
749 printf( "Output #%2d : ", i );
750 if ( Abc_AigNodeIsConst(pChild) )
751 {
752 if ( Abc_ObjIsComplement(pChild) )
753 printf( "Unsatisfiable.\n" );
754 else
755 printf( "Satisfiable. (Constant 1).\n" );
756 }
757 else
758 printf( "Satisfiable.\n" );
759 }
760 }
761 }
762
763
764 /**Function*************************************************************
765
766 Synopsis [Derives the timeframes of the network.]
767
768 Description []
769
770 SideEffects []
771
772 SeeAlso []
773
774 ***********************************************************************/
Abc_NtkFrames(Abc_Ntk_t * pNtk,int nFrames,int fInitial,int fVerbose)775 Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial, int fVerbose )
776 {
777 char Buffer[1000];
778 ProgressBar * pProgress;
779 Abc_Ntk_t * pNtkFrames;
780 Abc_Obj_t * pLatch, * pLatchOut;
781 int i, Counter;
782 assert( nFrames > 0 );
783 assert( Abc_NtkIsStrash(pNtk) );
784 assert( Abc_NtkIsDfsOrdered(pNtk) );
785 assert( Abc_NtkHasOnlyLatchBoxes(pNtk) );
786 // start the new network
787 pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
788 sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames );
789 pNtkFrames->pName = Extra_UtilStrsav(Buffer);
790 // map the constant nodes
791 Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkFrames);
792 // create new latches (or their initial values) and remember them in the new latches
793 if ( !fInitial )
794 {
795 Abc_NtkForEachLatch( pNtk, pLatch, i )
796 Abc_NtkDupBox( pNtkFrames, pLatch, 1 );
797 }
798 else
799 {
800 Counter = 0;
801 Abc_NtkForEachLatch( pNtk, pLatch, i )
802 {
803 pLatchOut = Abc_ObjFanout0(pLatch);
804 if ( Abc_LatchIsInitNone(pLatch) || Abc_LatchIsInitDc(pLatch) ) // don't-care initial value - create a new PI
805 {
806 pLatchOut->pCopy = Abc_NtkCreatePi(pNtkFrames);
807 Abc_ObjAssignName( pLatchOut->pCopy, Abc_ObjName(pLatchOut), NULL );
808 Counter++;
809 }
810 else
811 pLatchOut->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames), Abc_LatchIsInit0(pLatch) );
812 }
813 if ( Counter )
814 printf( "Warning: %d uninitialized latches are replaced by free PI variables.\n", Counter );
815 }
816
817 // create the timeframes
818 pProgress = Extra_ProgressBarStart( stdout, nFrames );
819 for ( i = 0; i < nFrames; i++ )
820 {
821 Extra_ProgressBarUpdate( pProgress, i, NULL );
822 Abc_NtkAddFrame( pNtkFrames, pNtk, i );
823 }
824 Extra_ProgressBarStop( pProgress );
825
826 // connect the new latches to the outputs of the last frame
827 if ( !fInitial )
828 {
829 // we cannot use pLatch->pCopy here because pLatch->pCopy is used for temporary storage of strashed values
830 Abc_NtkForEachLatch( pNtk, pLatch, i )
831 Abc_ObjAddFanin( Abc_ObjFanin0(pLatch)->pCopy, Abc_ObjFanout0(pLatch)->pCopy );
832 }
833
834 // remove dangling nodes
835 Abc_AigCleanup( (Abc_Aig_t *)pNtkFrames->pManFunc );
836 // reorder the latches
837 Abc_NtkOrderCisCos( pNtkFrames );
838 // make sure that everything is okay
839 if ( !Abc_NtkCheck( pNtkFrames ) )
840 {
841 printf( "Abc_NtkFrames: The network check has failed.\n" );
842 Abc_NtkDelete( pNtkFrames );
843 return NULL;
844 }
845 return pNtkFrames;
846 }
847
848 /**Function*************************************************************
849
850 Synopsis [Adds one time frame to the new network.]
851
852 Description [Assumes that the latches of the old network point
853 to the outputs of the previous frame of the new network (pLatch->pCopy).
854 In the end, updates the latches of the old network to point to the
855 outputs of the current frame of the new network.]
856
857 SideEffects []
858
859 SeeAlso []
860
861 ***********************************************************************/
Abc_NtkAddFrame(Abc_Ntk_t * pNtkFrames,Abc_Ntk_t * pNtk,int iFrame)862 void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame )
863 {
864 int fVerbose = 0;
865 int NodeBef = Abc_NtkNodeNum(pNtkFrames);
866 char Buffer[10];
867 Abc_Obj_t * pNode, * pLatch;
868 int i;
869 // create the prefix to be added to the node names
870 sprintf( Buffer, "_%02d", iFrame );
871 // add the new PI nodes
872 Abc_NtkForEachPi( pNtk, pNode, i )
873 Abc_ObjAssignName( Abc_NtkDupObj(pNtkFrames, pNode, 0), Abc_ObjName(pNode), Buffer );
874 // add the internal nodes
875 Abc_AigForEachAnd( pNtk, pNode, i )
876 pNode->pCopy = Abc_AigAnd( (Abc_Aig_t *)pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
877 // add the new POs
878 Abc_NtkForEachPo( pNtk, pNode, i )
879 {
880 Abc_ObjAssignName( Abc_NtkDupObj(pNtkFrames, pNode, 0), Abc_ObjName(pNode), Buffer );
881 Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) );
882 }
883 // transfer the implementation of the latch inputs to the latch outputs
884 Abc_NtkForEachLatch( pNtk, pLatch, i )
885 pLatch->pCopy = Abc_ObjChild0Copy(Abc_ObjFanin0(pLatch));
886 Abc_NtkForEachLatch( pNtk, pLatch, i )
887 Abc_ObjFanout0(pLatch)->pCopy = pLatch->pCopy;
888 // nodes after
889 if ( fVerbose )
890 printf( "F = %4d : Total = %6d. Nodes = %6d. Prop = %s.\n",
891 iFrame, Abc_NtkNodeNum(pNtk), Abc_NtkNodeNum(pNtkFrames)-NodeBef,
892 Abc_AigNodeIsConst( Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->pCopy ) ? "proof" : "unknown" );
893 }
894
895
896
897 /**Function*************************************************************
898
899 Synopsis [Derives the timeframes of the network.]
900
901 Description []
902
903 SideEffects []
904
905 SeeAlso []
906
907 ***********************************************************************/
Abc_NtkFrames2(Abc_Ntk_t * pNtk,int nFrames,int fInitial,AddFrameMapping addFrameMapping,void * arg)908 Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFrameMapping addFrameMapping, void* arg )
909 {
910 /*
911 char Buffer[1000];
912 ProgressBar * pProgress;
913 Abc_Ntk_t * pNtkFrames;
914 Vec_Ptr_t * vNodes;
915 Abc_Obj_t * pLatch, * pLatchNew;
916 int i, Counter;
917 assert( nFrames > 0 );
918 assert( Abc_NtkIsStrash(pNtk) );
919 // start the new network
920 pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
921 sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames );
922 pNtkFrames->pName = Extra_UtilStrsav(Buffer);
923 // create new latches (or their initial values) and remember them in the new latches
924 if ( !fInitial )
925 {
926 Abc_NtkForEachLatch( pNtk, pLatch, i ) {
927 Abc_NtkDupObj( pNtkFrames, pLatch );
928 if (addFrameMapping) addFrameMapping(pLatch->pCopy, pLatch, 0, arg);
929 }
930 }
931 else
932 {
933 Counter = 0;
934 Abc_NtkForEachLatch( pNtk, pLatch, i )
935 {
936 if ( Abc_LatchIsInitDc(pLatch) ) // don't-care initial value - create a new PI
937 {
938 pLatch->pCopy = Abc_NtkCreatePi(pNtkFrames);
939 Abc_ObjAssignName( pLatch->pCopy, Abc_ObjName(pLatch), NULL );
940 Counter++;
941 }
942 else {
943 pLatch->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames), Abc_LatchIsInit0(pLatch) );
944 }
945
946 if (addFrameMapping) addFrameMapping(pLatch->pCopy, pLatch, 0, arg);
947 }
948 if ( Counter )
949 printf( "Warning: %d uninitialized latches are replaced by free PI variables.\n", Counter );
950 }
951
952 // create the timeframes
953 vNodes = Abc_NtkDfs( pNtk, 0 );
954 pProgress = Extra_ProgressBarStart( stdout, nFrames );
955 for ( i = 0; i < nFrames; i++ )
956 {
957 Extra_ProgressBarUpdate( pProgress, i, NULL );
958 Abc_NtkAddFrame2( pNtkFrames, pNtk, i, vNodes, addFrameMapping, arg );
959 }
960 Extra_ProgressBarStop( pProgress );
961 Vec_PtrFree( vNodes );
962
963 // connect the new latches to the outputs of the last frame
964 if ( !fInitial )
965 {
966 Abc_NtkForEachLatch( pNtk, pLatch, i )
967 {
968 pLatchNew = Abc_NtkBox(pNtkFrames, i);
969 Abc_ObjAddFanin( pLatchNew, pLatch->pCopy );
970 Abc_ObjAssignName( pLatchNew, Abc_ObjName(pLatch), NULL );
971 }
972 }
973 Abc_NtkForEachLatch( pNtk, pLatch, i )
974 pLatch->pNext = NULL;
975
976 // remove dangling nodes
977 Abc_AigCleanup( pNtkFrames->pManFunc );
978
979 // reorder the latches
980 Abc_NtkOrderCisCos( pNtkFrames );
981
982 // make sure that everything is okay
983 if ( !Abc_NtkCheck( pNtkFrames ) )
984 {
985 printf( "Abc_NtkFrames: The network check has failed.\n" );
986 Abc_NtkDelete( pNtkFrames );
987 return NULL;
988 }
989 return pNtkFrames;
990 */
991 return NULL;
992 }
993
994 /**Function*************************************************************
995
996 Synopsis [Adds one time frame to the new network.]
997
998 Description [Assumes that the latches of the old network point
999 to the outputs of the previous frame of the new network (pLatch->pCopy).
1000 In the end, updates the latches of the old network to point to the
1001 outputs of the current frame of the new network.]
1002
1003 SideEffects []
1004
1005 SeeAlso []
1006
1007 ***********************************************************************/
Abc_NtkAddFrame2(Abc_Ntk_t * pNtkFrames,Abc_Ntk_t * pNtk,int iFrame,Vec_Ptr_t * vNodes,AddFrameMapping addFrameMapping,void * arg)1008 void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vNodes, AddFrameMapping addFrameMapping, void* arg )
1009 {
1010 /*
1011 char Buffer[10];
1012 Abc_Obj_t * pNode, * pNodeNew, * pLatch;
1013 Abc_Obj_t * pConst1, * pConst1New;
1014 int i;
1015 // get the constant nodes
1016 pConst1 = Abc_AigConst1(pNtk);
1017 pConst1New = Abc_AigConst1(pNtkFrames);
1018 // create the prefix to be added to the node names
1019 sprintf( Buffer, "_%02d", iFrame );
1020 // add the new PI nodes
1021 Abc_NtkForEachPi( pNtk, pNode, i )
1022 {
1023 pNodeNew = Abc_NtkDupObj( pNtkFrames, pNode );
1024 Abc_ObjAssignName( pNodeNew, Abc_ObjName(pNode), Buffer );
1025 if (addFrameMapping) addFrameMapping(pNodeNew, pNode, iFrame, arg);
1026 }
1027 // add the internal nodes
1028 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
1029 {
1030 if ( pNode == pConst1 )
1031 pNodeNew = pConst1New;
1032 else
1033 pNodeNew = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
1034 pNode->pCopy = pNodeNew;
1035 if (addFrameMapping) addFrameMapping(pNodeNew, pNode, iFrame, arg);
1036 }
1037 // add the new POs
1038 Abc_NtkForEachPo( pNtk, pNode, i )
1039 {
1040 pNodeNew = Abc_NtkDupObj( pNtkFrames, pNode );
1041 Abc_ObjAddFanin( pNodeNew, Abc_ObjChild0Copy(pNode) );
1042 Abc_ObjAssignName( pNodeNew, Abc_ObjName(pNode), Buffer );
1043 if (addFrameMapping) addFrameMapping(pNodeNew, pNode, iFrame, arg);
1044 }
1045 // transfer the implementation of the latch drivers to the latches
1046
1047 // it is important that these two steps are performed it two loops
1048 // and not in the same loop
1049 Abc_NtkForEachLatch( pNtk, pLatch, i )
1050 pLatch->pNext = Abc_ObjChild0Copy(pLatch);
1051 Abc_NtkForEachLatch( pNtk, pLatch, i )
1052 pLatch->pCopy = pLatch->pNext;
1053
1054 Abc_NtkForEachLatch( pNtk, pLatch, i )
1055 {
1056 if (addFrameMapping) {
1057 // don't give Mike complemented pointers because he doesn't like it
1058 if (Abc_ObjIsComplement(pLatch->pCopy)) {
1059 pNodeNew = Abc_NtkCreateNode( pNtkFrames );
1060 Abc_ObjAddFanin( pNodeNew, pLatch->pCopy );
1061 assert(Abc_ObjFaninNum(pNodeNew) == 1);
1062 pNodeNew->Level = 1 + Abc_ObjRegular(pLatch->pCopy)->Level;
1063
1064 pLatch->pNext = pNodeNew;
1065 pLatch->pCopy = pNodeNew;
1066 }
1067 addFrameMapping(pLatch->pCopy, pLatch, iFrame+1, arg);
1068 }
1069 }
1070 */
1071 }
1072
1073
1074
1075 /**Function*************************************************************
1076
1077 Synopsis [Splits the miter into two logic cones combined by an EXOR]
1078
1079 Description []
1080
1081 SideEffects []
1082
1083 SeeAlso []
1084
1085 ***********************************************************************/
Abc_NtkDemiter(Abc_Ntk_t * pNtk)1086 int Abc_NtkDemiter( Abc_Ntk_t * pNtk )
1087 {
1088 Abc_Obj_t * pNodeC, * pNodeA, * pNodeB, * pNode;
1089 Abc_Obj_t * pPoNew;
1090 Vec_Ptr_t * vNodes1, * vNodes2;
1091 int nCommon, i;
1092
1093 assert( Abc_NtkIsStrash(pNtk) );
1094 assert( Abc_NtkPoNum(pNtk) == 1 );
1095 if ( !Abc_NodeIsExorType(Abc_ObjFanin0(Abc_NtkPo(pNtk,0))) )
1096 {
1097 printf( "The root of the miter is not an EXOR gate.\n" );
1098 return 0;
1099 }
1100 pNodeC = Abc_NodeRecognizeMux( Abc_ObjFanin0(Abc_NtkPo(pNtk,0)), &pNodeA, &pNodeB );
1101 assert( Abc_ObjRegular(pNodeA) == Abc_ObjRegular(pNodeB) );
1102 if ( Abc_ObjFaninC0(Abc_NtkPo(pNtk,0)) )
1103 {
1104 pNodeA = Abc_ObjNot(pNodeA);
1105 pNodeB = Abc_ObjNot(pNodeB);
1106 }
1107
1108 // add the PO corresponding to control input
1109 pPoNew = Abc_NtkCreatePo( pNtk );
1110 Abc_ObjAddFanin( pPoNew, pNodeC );
1111 Abc_ObjAssignName( pPoNew, "addOut1", NULL );
1112
1113 // add the PO corresponding to other input
1114 pPoNew = Abc_NtkCreatePo( pNtk );
1115 Abc_ObjAddFanin( pPoNew, pNodeB );
1116 Abc_ObjAssignName( pPoNew, "addOut2", NULL );
1117
1118 // mark the nodes in the first cone
1119 pNodeB = Abc_ObjRegular(pNodeB);
1120 vNodes1 = Abc_NtkDfsNodes( pNtk, &pNodeC, 1 );
1121 vNodes2 = Abc_NtkDfsNodes( pNtk, &pNodeB, 1 );
1122
1123 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes1, pNode, i )
1124 pNode->fMarkA = 1;
1125 nCommon = 0;
1126 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes2, pNode, i )
1127 nCommon += pNode->fMarkA;
1128 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes1, pNode, i )
1129 pNode->fMarkA = 0;
1130
1131 printf( "First cone = %6d. Second cone = %6d. Common = %6d.\n", vNodes1->nSize, vNodes2->nSize, nCommon );
1132 Vec_PtrFree( vNodes1 );
1133 Vec_PtrFree( vNodes2 );
1134
1135 // reorder the latches
1136 Abc_NtkOrderCisCos( pNtk );
1137 // make sure that everything is okay
1138 if ( !Abc_NtkCheck( pNtk ) )
1139 printf( "Abc_NtkDemiter: The network check has failed.\n" );
1140 return 1;
1141 }
1142
1143 /**Function*************************************************************
1144
1145 Synopsis [Computes OR or AND of the POs.]
1146
1147 Description []
1148
1149 SideEffects []
1150
1151 SeeAlso []
1152
1153 ***********************************************************************/
Abc_NtkCombinePos(Abc_Ntk_t * pNtk,int fAnd,int fXor)1154 int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd, int fXor )
1155 {
1156 Abc_Obj_t * pNode, * pMiter;
1157 int i;
1158 assert( Abc_NtkIsStrash(pNtk) );
1159 // assert( Abc_NtkLatchNum(pNtk) == 0 );
1160 if ( Abc_NtkPoNum(pNtk) == 1 )
1161 return 1;
1162 // start the result
1163 if ( fAnd )
1164 pMiter = Abc_AigConst1(pNtk);
1165 else
1166 pMiter = Abc_ObjNot( Abc_AigConst1(pNtk) );
1167 // perform operations on the POs
1168 Abc_NtkForEachPo( pNtk, pNode, i )
1169 if ( fAnd )
1170 pMiter = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) );
1171 else if ( fXor )
1172 pMiter = Abc_AigXor( (Abc_Aig_t *)pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) );
1173 else
1174 pMiter = Abc_AigOr( (Abc_Aig_t *)pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) );
1175 // remove the POs and their names
1176 for ( i = Abc_NtkPoNum(pNtk) - 1; i >= 0; i-- )
1177 Abc_NtkDeleteObj( Abc_NtkPo(pNtk, i) );
1178 assert( Abc_NtkPoNum(pNtk) == 0 );
1179 // create the new PO
1180 pNode = Abc_NtkCreatePo( pNtk );
1181 Abc_ObjAddFanin( pNode, pMiter );
1182 Abc_ObjAssignName( pNode, "miter", NULL );
1183 Abc_NtkOrderCisCos( pNtk );
1184 // make sure that everything is okay
1185 if ( !Abc_NtkCheck( pNtk ) )
1186 {
1187 printf( "Abc_NtkOrPos: The network check has failed.\n" );
1188 return 0;
1189 }
1190 return 1;
1191 }
1192
1193 /**Function*************************************************************
1194
1195 Synopsis [Miter construction for two networks.]
1196
1197 Description []
1198
1199 SideEffects []
1200
1201 SeeAlso []
1202
1203 ***********************************************************************/
Abc_NtkTryNewMiter(char * pFileName0,char * pFileName1)1204 Vec_Ptr_t * Abc_NtkTryNewMiter( char * pFileName0, char * pFileName1 )
1205 {
1206 extern void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit );
1207 int i, nVars, * pVars, iCiVarBeg, iCoVarBeg = 1, nBTLimit = 100000;
1208 sat_solver * pSat = NULL;
1209 Cnf_Dat_t * pCnf = NULL;
1210 Vec_Ptr_t * vCexes = NULL;
1211 Abc_Ntk_t * pNtk1 = Io_Read( pFileName0, IO_FILE_VERILOG, 1, 0 );
1212 Abc_Ntk_t * pNtk2 = Io_Read( pFileName1, IO_FILE_VERILOG, 1, 0 );
1213 Abc_Ntk_t * pNtk1_ = Abc_NtkStrash( pNtk1, 1, 1, 0 );
1214 Abc_Ntk_t * pNtk2_ = Abc_NtkStrash( pNtk2, 1, 1, 0 );
1215 Abc_Ntk_t * pMiter = Abc_NtkMiter( pNtk1_, pNtk2_, 1, 0, 0, 1 );
1216 Gia_Man_t * pGia = Abc_NtkClpGia( pMiter );
1217 assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) );
1218 assert( Abc_NtkCoNum(pNtk1) == Abc_NtkCoNum(pNtk2) );
1219 Abc_NtkDelete( pNtk1 );
1220 Abc_NtkDelete( pNtk2 );
1221 Abc_NtkDelete( pNtk1_ );
1222 Abc_NtkDelete( pNtk2_ );
1223 Abc_NtkDelete( pMiter );
1224 vCexes = Vec_PtrStart( Gia_ManPoNum(pGia) );
1225 pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGia, 8, 0, 0, 0, 0 );
1226 nVars = Gia_ManPiNum(pGia);
1227 iCiVarBeg = pCnf->nVars - nVars;
1228 pVars = ABC_ALLOC( int, nVars );
1229 for ( i = 0; i < nVars; i++ )
1230 pVars[i] = iCiVarBeg + i;
1231 pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
1232 Cnf_DataFree( pCnf );
1233 for ( i = 0; i < Gia_ManPoNum(pGia); i++ )
1234 {
1235 int Lit = Abc_Var2Lit( iCoVarBeg + i, 0 );
1236 int status = sat_solver_solve( pSat, &Lit, &Lit + 1, nBTLimit, 0, 0, 0 );
1237 assert( status != l_Undef );
1238 if ( status == l_False )
1239 continue;
1240 Vec_PtrWriteEntry( vCexes, i, Sat_SolverGetModel(pSat, pVars, nVars) );
1241 printf( "Output %3d (out of %3d) is SAT.\n", i, Gia_ManPoNum(pGia) );
1242 }
1243 Gia_ManStop( pGia );
1244 sat_solver_delete( pSat );
1245 ABC_FREE( pVars );
1246 return vCexes;
1247 }
1248
1249 /**Function*************************************************************
1250
1251 Synopsis [Read node names.]
1252
1253 Description []
1254
1255 SideEffects []
1256
1257 SeeAlso []
1258
1259 ***********************************************************************/
Abc_NtkReadNodeNames(Abc_Ntk_t * pNtk,char * pFileName)1260 Vec_Ptr_t * Abc_NtkReadNodeNames( Abc_Ntk_t * pNtk, char * pFileName )
1261 {
1262 char Buffer[1000];
1263 Vec_Ptr_t * vNodes = NULL;
1264 FILE * pFile = fopen( pFileName, "rb" );
1265 if ( pFile == NULL )
1266 {
1267 printf( "Cannot open node list \"%s\".\n", pFileName );
1268 return NULL;
1269 }
1270 vNodes = Vec_PtrAlloc( 100 );
1271 while ( fgets(Buffer, 1000, pFile) != NULL )
1272 {
1273 char * pToken = strtok( Buffer, " \n\r\t" );
1274 while ( pToken )
1275 {
1276 Abc_Obj_t * pObj = Abc_NtkFindNode( pNtk, pToken );
1277 if ( pObj == NULL )
1278 {
1279 printf( "Cannot find node \"%s\".\n", pToken );
1280 Vec_PtrFree( vNodes );
1281 fclose( pFile );
1282 return NULL;
1283 }
1284 Vec_PtrPush( vNodes, pObj );
1285 pToken = strtok( NULL, " \n\r\t" );
1286 }
1287 }
1288 fclose( pFile );
1289 return vNodes;
1290 }
1291
1292 /**Function*************************************************************
1293
1294 Synopsis [Deriving specialized miter.]
1295
1296 Description []
1297
1298 SideEffects []
1299
1300 SeeAlso []
1301
1302 ***********************************************************************/
Abc_NtkSpecialMuxTree_rec(Abc_Ntk_t * pNew,Abc_Obj_t ** pCtrl,int nCtrl,Abc_Obj_t ** pData,int Shift)1303 Abc_Obj_t * Abc_NtkSpecialMuxTree_rec( Abc_Ntk_t * pNew, Abc_Obj_t ** pCtrl, int nCtrl, Abc_Obj_t ** pData, int Shift )
1304 {
1305 Abc_Obj_t * pLit0, * pLit1;
1306 if ( nCtrl == 0 )
1307 return pData[Shift];
1308 pLit0 = Abc_NtkSpecialMuxTree_rec( pNew, pCtrl, nCtrl-1, pData, Shift );
1309 pLit1 = Abc_NtkSpecialMuxTree_rec( pNew, pCtrl, nCtrl-1, pData, Shift + (1<<(nCtrl-1)) );
1310 return Abc_NtkCreateNodeMux( pNew, pCtrl[nCtrl-1], pLit1, pLit0 );
1311 }
Abc_NtkSpecialMiter(Abc_Ntk_t * pNtk,Vec_Ptr_t * vNodes)1312 Abc_Ntk_t * Abc_NtkSpecialMiter( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes )
1313 {
1314 Abc_Ntk_t * pNtkNew;
1315 Abc_Obj_t * pObj, * pFanin, * pObjNew, * pPoNew; char * pName;
1316 Vec_Int_t * vFirsts = Vec_IntAlloc( Vec_PtrSize(vNodes) );
1317 Vec_Ptr_t * vNames = Vec_PtrAlloc( 100 );
1318 Vec_Ptr_t * vFanins = Vec_PtrAlloc( 100 );
1319 Vec_Ptr_t * vDatas = Vec_PtrAlloc( 100 );
1320 Vec_Ptr_t * vDfs = Abc_NtkDfs( pNtk, 1 );
1321 Vec_Ptr_t * vCopies = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
1322 int i, k, Index, First, nNewPis = 0;
1323 // count the number of additional inputs
1324 Abc_NtkCleanCopy( pNtk );
1325 Abc_NtkCleanMarkA( pNtk );
1326 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
1327 {
1328 char Buffer[1000];
1329 assert( Abc_ObjIsNode(pObj) );
1330 pObj->fMarkA = 1;
1331 Vec_IntPush( vFirsts, nNewPis );
1332 nNewPis += 1 << Abc_ObjFaninNum(pObj);
1333 for ( k = 0; k < (1 << Abc_ObjFaninNum(pObj)); k++ )
1334 {
1335 sprintf( Buffer, "pi_%s_%d", Abc_ObjName(pObj), k );
1336 Vec_PtrPush( vNames, Abc_UtilStrsav(Buffer) );
1337 }
1338 }
1339 // create new network with the additional PIs
1340 pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
1341 pNtkNew->pName = Extra_UtilStrsav( "miter" );
1342 Vec_PtrForEachEntry( char *, vNames, pName, i )
1343 Abc_ObjAssignName( Abc_NtkCreatePi(pNtkNew), pName, NULL );
1344 // duplicate PIs
1345 Abc_NtkForEachCi( pNtk, pObj, i )
1346 pObj->pCopy = Abc_NtkDupObj( pNtkNew, pObj, 1 );
1347 // copy nodes
1348 Vec_PtrForEachEntry( Abc_Obj_t *, vDfs, pObj, i )
1349 {
1350 if ( !pObj->fMarkA )
1351 {
1352 Abc_NtkDupObj( pNtkNew, pObj, 1 );
1353 Abc_ObjForEachFanin( pObj, pFanin, k )
1354 Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
1355 Vec_PtrWriteEntry( vCopies, pObj->Id, pObj->pCopy );
1356 continue;
1357 }
1358 Vec_PtrClear( vFanins );
1359 Abc_ObjForEachFanin( pObj, pFanin, k )
1360 Vec_PtrPush( vFanins, pFanin->pCopy );
1361 Index = Vec_PtrFind( vNodes, pObj );
1362 assert( Index >= 0 );
1363 First = Vec_IntEntry( vFirsts, Index );
1364 Vec_PtrClear( vDatas );
1365 for ( k = 0; k < (1 << Abc_ObjFaninNum(pObj)); k++ )
1366 Vec_PtrPush( vDatas, Abc_NtkCi(pNtkNew, First + k) );
1367 pObj->pCopy = Abc_NtkSpecialMuxTree_rec( pNtkNew,
1368 (Abc_Obj_t **)Vec_PtrArray(vFanins), Vec_PtrSize(vFanins),
1369 (Abc_Obj_t **)Vec_PtrArray(vDatas), 0 );
1370 Vec_PtrWriteEntry( vCopies, pObj->Id, pObj->pCopy );
1371 }
1372 Vec_PtrForEachEntry( Abc_Obj_t *, vDfs, pObj, i )
1373 {
1374 pObj->fMarkA = 0;
1375 Abc_NtkDupObj( pNtkNew, pObj, 0 );
1376 Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), "_copy" );
1377 Abc_ObjForEachFanin( pObj, pFanin, k )
1378 Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
1379 }
1380 // create miter
1381 Vec_PtrClear( vDatas );
1382 Abc_NtkForEachCo( pNtk, pObj, i )
1383 {
1384 Vec_PtrClear( vFanins );
1385 Vec_PtrPush( vFanins, Abc_ObjFanin0(pObj)->pCopy );
1386 Vec_PtrPush( vFanins, (Abc_Obj_t *)Vec_PtrEntry(vCopies, Abc_ObjId(Abc_ObjFanin0(pObj))) );
1387 Vec_PtrPush( vDatas, Abc_NtkCreateNodeExor(pNtkNew, vFanins) );
1388 }
1389 if ( Vec_PtrSize(vDatas) > 1 )
1390 pObjNew = Abc_NtkCreateNodeOr( pNtkNew, vDatas );
1391 else
1392 pObjNew = (Abc_Obj_t *)Vec_PtrEntry(vDatas, 0);
1393 Abc_ObjAddFanin( (pPoNew = Abc_NtkCreatePo(pNtkNew)), pObjNew );
1394 Abc_ObjAssignName( pPoNew, "miter_output", NULL );
1395 // cleanup
1396 Vec_IntFree( vFirsts );
1397 Vec_PtrFreeFree( vNames );
1398 Vec_PtrFree( vFanins );
1399 Vec_PtrFree( vDatas );
1400 Vec_PtrFree( vDfs );
1401 Vec_PtrFree( vCopies );
1402 return pNtkNew;
1403 }
1404
1405 ////////////////////////////////////////////////////////////////////////
1406 /// END OF FILE ///
1407 ////////////////////////////////////////////////////////////////////////
1408
1409
1410 ABC_NAMESPACE_IMPL_END
1411
1412