1 /**CFile****************************************************************
2
3 FileName [abcDar.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Network and node package.]
8
9 Synopsis [DAG-aware rewriting.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: abcDar.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "base/abc/abc.h"
22 #include "base/main/main.h"
23 #include "aig/gia/giaAig.h"
24 #include "opt/dar/dar.h"
25 #include "sat/cnf/cnf.h"
26 #include "proof/fra/fra.h"
27 #include "proof/fraig/fraig.h"
28 #include "proof/int/int.h"
29 #include "proof/dch/dch.h"
30 #include "proof/ssw/ssw.h"
31 #include "opt/cgt/cgt.h"
32 #include "bdd/bbr/bbr.h"
33 #include "aig/gia/gia.h"
34 #include "proof/cec/cec.h"
35 #include "opt/csw/csw.h"
36 #include "proof/pdr/pdr.h"
37 #include "sat/bmc/bmc.h"
38 #include "map/mio/mio.h"
39
40 ABC_NAMESPACE_IMPL_START
41
42 ////////////////////////////////////////////////////////////////////////
43 /// DECLARATIONS ///
44 ////////////////////////////////////////////////////////////////////////
45
46 ////////////////////////////////////////////////////////////////////////
47 /// FUNCTION DEFINITIONS ///
48 ////////////////////////////////////////////////////////////////////////
49
50 /**Function*************************************************************
51
52 Synopsis []
53
54 Description []
55
56 SideEffects []
57
58 SeeAlso []
59
60 ***********************************************************************/
Abc_ObjCompareById(Abc_Obj_t ** pp1,Abc_Obj_t ** pp2)61 int Abc_ObjCompareById( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 )
62 {
63 return Abc_ObjId(Abc_ObjRegular(*pp1)) - Abc_ObjId(Abc_ObjRegular(*pp2));
64 }
65
66 /**Function*************************************************************
67
68 Synopsis [Collects the supergate.]
69
70 Description []
71
72 SideEffects []
73
74 SeeAlso []
75
76 ***********************************************************************/
Abc_CollectTopOr_rec(Abc_Obj_t * pObj,Vec_Ptr_t * vSuper)77 void Abc_CollectTopOr_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vSuper )
78 {
79 if ( Abc_ObjIsComplement(pObj) || !Abc_ObjIsNode(pObj) )
80 {
81 Vec_PtrPush( vSuper, pObj );
82 return;
83 }
84 // go through the branches
85 Abc_CollectTopOr_rec( Abc_ObjChild0(pObj), vSuper );
86 Abc_CollectTopOr_rec( Abc_ObjChild1(pObj), vSuper );
87 }
Abc_CollectTopOr(Abc_Obj_t * pObj,Vec_Ptr_t * vSuper)88 void Abc_CollectTopOr( Abc_Obj_t * pObj, Vec_Ptr_t * vSuper )
89 {
90 Vec_PtrClear( vSuper );
91 if ( Abc_ObjIsComplement(pObj) )
92 {
93 Abc_CollectTopOr_rec( Abc_ObjNot(pObj), vSuper );
94 Vec_PtrUniqify( vSuper, (int (*)())Abc_ObjCompareById );
95 }
96 else
97 Vec_PtrPush( vSuper, Abc_ObjNot(pObj) );
98 }
99
100 /**Function*************************************************************
101
102 Synopsis [Converts the network from the AIG manager into ABC.]
103
104 Description [The returned map maps new PO IDs into old ones.]
105
106 SideEffects []
107
108 SeeAlso []
109
110 ***********************************************************************/
Abc_NtkToDarBmc(Abc_Ntk_t * pNtk,Vec_Int_t ** pvMap)111 Aig_Man_t * Abc_NtkToDarBmc( Abc_Ntk_t * pNtk, Vec_Int_t ** pvMap )
112 {
113 Aig_Man_t * pMan;
114 Abc_Obj_t * pObj, * pTemp;
115 Vec_Ptr_t * vDrivers;
116 Vec_Ptr_t * vSuper;
117 int i, k, nDontCares;
118
119 // print warning about initial values
120 nDontCares = 0;
121 Abc_NtkForEachLatch( pNtk, pObj, i )
122 if ( Abc_LatchIsInitDc(pObj) )
123 {
124 Abc_LatchSetInit0(pObj);
125 nDontCares++;
126 }
127 if ( nDontCares )
128 {
129 Abc_Print( 1, "Warning: %d registers in this network have don't-care init values.\n", nDontCares );
130 Abc_Print( 1, "The don't-care are assumed to be 0. The result may not verify.\n" );
131 Abc_Print( 1, "Use command \"print_latch\" to see the init values of registers.\n" );
132 Abc_Print( 1, "Use command \"zero\" to convert or \"init\" to change the values.\n" );
133 }
134
135 // collect the drivers
136 vSuper = Vec_PtrAlloc( 100 );
137 vDrivers = Vec_PtrAlloc( 100 );
138 if ( pvMap )
139 *pvMap = Vec_IntAlloc( 100 );
140 Abc_NtkForEachPo( pNtk, pObj, i )
141 {
142 if ( pNtk->nConstrs && i >= pNtk->nConstrs )
143 {
144 Vec_PtrPush( vDrivers, Abc_ObjNot(Abc_ObjChild0(pObj)) );
145 if ( pvMap )
146 Vec_IntPush( *pvMap, i );
147 continue;
148 }
149 Abc_CollectTopOr( Abc_ObjChild0(pObj), vSuper );
150 Vec_PtrForEachEntry( Abc_Obj_t *, vSuper, pTemp, k )
151 {
152 Vec_PtrPush( vDrivers, pTemp );
153 if ( pvMap )
154 Vec_IntPush( *pvMap, i );
155 }
156 }
157 Vec_PtrFree( vSuper );
158
159 // create network
160 pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
161 pMan->nConstrs = pNtk->nConstrs;
162 pMan->nBarBufs = pNtk->nBarBufs;
163 pMan->pName = Extra_UtilStrsav( pNtk->pName );
164 pMan->pSpec = Extra_UtilStrsav( pNtk->pSpec );
165 // transfer the pointers to the basic nodes
166 Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
167 Abc_NtkForEachCi( pNtk, pObj, i )
168 pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreateCi(pMan);
169 // create flops
170 Abc_NtkForEachLatch( pNtk, pObj, i )
171 Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNotCond( Abc_ObjFanout0(pObj)->pCopy, Abc_LatchIsInit1(pObj) );
172 // copy internal nodes
173 Abc_NtkForEachNode( pNtk, pObj, i )
174 pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
175 // create the POs
176 Vec_PtrForEachEntry( Abc_Obj_t *, vDrivers, pTemp, k )
177 Aig_ObjCreateCo( pMan, (Aig_Obj_t *)Abc_ObjNotCond(Abc_ObjRegular(pTemp)->pCopy, !Abc_ObjIsComplement(pTemp)) );
178 Vec_PtrFree( vDrivers );
179 // create flops
180 Abc_NtkForEachLatchInput( pNtk, pObj, i )
181 Aig_ObjCreateCo( pMan, (Aig_Obj_t *)Abc_ObjNotCond(Abc_ObjChild0Copy(pObj), Abc_LatchIsInit1(Abc_ObjFanout0(pObj))) );
182
183 // remove dangling nodes
184 Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
185 Aig_ManCleanup( pMan );
186 if ( !Aig_ManCheck( pMan ) )
187 {
188 Abc_Print( 1, "Abc_NtkToDarBmc: AIG check has failed.\n" );
189 Aig_ManStop( pMan );
190 return NULL;
191 }
192 return pMan;
193 }
194
195
196 /**Function*************************************************************
197
198 Synopsis [Collects information about what flops have unknown values.]
199
200 Description []
201
202 SideEffects []
203
204 SeeAlso []
205
206 ***********************************************************************/
Abc_NtkFindDcLatches(Abc_Ntk_t * pNtk)207 Vec_Int_t * Abc_NtkFindDcLatches( Abc_Ntk_t * pNtk )
208 {
209 Vec_Int_t * vUnknown;
210 Abc_Obj_t * pObj;
211 int i;
212 vUnknown = Vec_IntStart( Abc_NtkLatchNum(pNtk) );
213 Abc_NtkForEachLatch( pNtk, pObj, i )
214 if ( Abc_LatchIsInitDc(pObj) )
215 {
216 Vec_IntWriteEntry( vUnknown, i, 1 );
217 Abc_LatchSetInit0(pObj);
218 }
219 return vUnknown;
220 }
221
222 /**Function*************************************************************
223
224 Synopsis [Converts the network from the AIG manager into ABC.]
225
226 Description [Assumes that registers are ordered after PIs/POs.]
227
228 SideEffects []
229
230 SeeAlso []
231
232 ***********************************************************************/
Abc_NtkToDar(Abc_Ntk_t * pNtk,int fExors,int fRegisters)233 Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters )
234 {
235 Vec_Ptr_t * vNodes;
236 Aig_Man_t * pMan;
237 Aig_Obj_t * pObjNew;
238 Abc_Obj_t * pObj;
239 int i, nNodes, nDontCares;
240 // make sure the latches follow PIs/POs
241 if ( fRegisters )
242 {
243 assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
244 Abc_NtkForEachCi( pNtk, pObj, i )
245 if ( i < Abc_NtkPiNum(pNtk) )
246 {
247 assert( Abc_ObjIsPi(pObj) );
248 if ( !Abc_ObjIsPi(pObj) )
249 Abc_Print( 1, "Abc_NtkToDar(): Temporary bug: The PI ordering is wrong!\n" );
250 }
251 else
252 assert( Abc_ObjIsBo(pObj) );
253 Abc_NtkForEachCo( pNtk, pObj, i )
254 if ( i < Abc_NtkPoNum(pNtk) )
255 {
256 assert( Abc_ObjIsPo(pObj) );
257 if ( !Abc_ObjIsPo(pObj) )
258 Abc_Print( 1, "Abc_NtkToDar(): Temporary bug: The PO ordering is wrong!\n" );
259 }
260 else
261 assert( Abc_ObjIsBi(pObj) );
262 // print warning about initial values
263 nDontCares = 0;
264 Abc_NtkForEachLatch( pNtk, pObj, i )
265 if ( Abc_LatchIsInitDc(pObj) )
266 {
267 Abc_LatchSetInit0(pObj);
268 nDontCares++;
269 }
270 if ( nDontCares )
271 {
272 Abc_Print( 1, "Warning: %d registers in this network have don't-care init values.\n", nDontCares );
273 Abc_Print( 1, "The don't-care are assumed to be 0. The result may not verify.\n" );
274 Abc_Print( 1, "Use command \"print_latch\" to see the init values of registers.\n" );
275 Abc_Print( 1, "Use command \"zero\" to convert or \"init\" to change the values.\n" );
276 }
277 }
278 // create the manager
279 pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
280 pMan->fCatchExor = fExors;
281 pMan->nConstrs = pNtk->nConstrs;
282 pMan->nBarBufs = pNtk->nBarBufs;
283 pMan->pName = Extra_UtilStrsav( pNtk->pName );
284 pMan->pSpec = Extra_UtilStrsav( pNtk->pSpec );
285 // transfer the pointers to the basic nodes
286 Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
287 Abc_NtkForEachCi( pNtk, pObj, i )
288 {
289 pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreateCi(pMan);
290 // initialize logic level of the CIs
291 ((Aig_Obj_t *)pObj->pCopy)->Level = pObj->Level;
292 }
293
294 // complement the 1-values registers
295 if ( fRegisters ) {
296 Abc_NtkForEachLatch( pNtk, pObj, i )
297 if ( Abc_LatchIsInit1(pObj) )
298 Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy);
299 }
300 // perform the conversion of the internal nodes (assumes DFS ordering)
301 // pMan->fAddStrash = 1;
302 vNodes = Abc_NtkDfs( pNtk, 0 );
303 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
304 // Abc_NtkForEachNode( pNtk, pObj, i )
305 {
306 pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
307 // Abc_Print( 1, "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id );
308 }
309 Vec_PtrFree( vNodes );
310 pMan->fAddStrash = 0;
311 // create the POs
312 Abc_NtkForEachCo( pNtk, pObj, i )
313 Aig_ObjCreateCo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) );
314 // complement the 1-valued registers
315 Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
316 if ( fRegisters )
317 Aig_ManForEachLiSeq( pMan, pObjNew, i )
318 if ( Abc_LatchIsInit1(Abc_ObjFanout0(Abc_NtkCo(pNtk,i))) )
319 pObjNew->pFanin0 = Aig_Not(pObjNew->pFanin0);
320 // remove dangling nodes
321 nNodes = (Abc_NtkGetChoiceNum(pNtk) == 0)? Aig_ManCleanup( pMan ) : 0;
322 if ( !fExors && nNodes )
323 Abc_Print( 1, "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes );
324 //Aig_ManDumpVerilog( pMan, "test.v" );
325 // save the number of registers
326 if ( fRegisters )
327 {
328 Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
329 pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
330 // pMan->vFlopNums = NULL;
331 // pMan->vOnehots = Abc_NtkConverLatchNamesIntoNumbers( pNtk );
332 if ( pNtk->vOnehots )
333 pMan->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots );
334 }
335 if ( !Aig_ManCheck( pMan ) )
336 {
337 Abc_Print( 1, "Abc_NtkToDar: AIG check has failed.\n" );
338 Aig_ManStop( pMan );
339 return NULL;
340 }
341 return pMan;
342 }
343
344 /**Function*************************************************************
345
346 Synopsis [Converts the network from the AIG manager into ABC.]
347
348 Description [Assumes that registers are ordered after PIs/POs.]
349
350 SideEffects []
351
352 SeeAlso []
353
354 ***********************************************************************/
Abc_NtkToDarChoices(Abc_Ntk_t * pNtk)355 Aig_Man_t * Abc_NtkToDarChoices( Abc_Ntk_t * pNtk )
356 {
357 Aig_Man_t * pMan;
358 Abc_Obj_t * pObj, * pPrev, * pFanin;
359 Vec_Ptr_t * vNodes;
360 int i;
361 vNodes = Abc_AigDfs( pNtk, 0, 0 );
362 // create the manager
363 pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
364 pMan->nConstrs = pNtk->nConstrs;
365 pMan->nBarBufs = pNtk->nBarBufs;
366 pMan->pName = Extra_UtilStrsav( pNtk->pName );
367 pMan->pSpec = Extra_UtilStrsav( pNtk->pSpec );
368 if ( Abc_NtkGetChoiceNum(pNtk) )
369 {
370 pMan->pEquivs = ABC_ALLOC( Aig_Obj_t *, Abc_NtkObjNum(pNtk) );
371 memset( pMan->pEquivs, 0, sizeof(Aig_Obj_t *) * Abc_NtkObjNum(pNtk) );
372 }
373 // transfer the pointers to the basic nodes
374 Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
375 Abc_NtkForEachCi( pNtk, pObj, i )
376 pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreateCi(pMan);
377 // perform the conversion of the internal nodes (assumes DFS ordering)
378 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
379 {
380 pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
381 // Abc_Print( 1, "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id );
382 if ( Abc_AigNodeIsChoice( pObj ) )
383 {
384 for ( pPrev = pObj, pFanin = (Abc_Obj_t *)pObj->pData; pFanin; pPrev = pFanin, pFanin = (Abc_Obj_t *)pFanin->pData )
385 Aig_ObjSetEquiv( pMan, (Aig_Obj_t *)pPrev->pCopy, (Aig_Obj_t *)pFanin->pCopy );
386 // Aig_ManCreateChoice( pIfMan, (Aig_Obj_t *)pNode->pCopy );
387 }
388 }
389 Vec_PtrFree( vNodes );
390 // create the POs
391 Abc_NtkForEachCo( pNtk, pObj, i )
392 Aig_ObjCreateCo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) );
393 // complement the 1-valued registers
394 Aig_ManSetRegNum( pMan, 0 );
395 if ( !Aig_ManCheck( pMan ) )
396 {
397 Abc_Print( 1, "Abc_NtkToDar: AIG check has failed.\n" );
398 Aig_ManStop( pMan );
399 return NULL;
400 }
401 return pMan;
402 }
403
404 /**Function*************************************************************
405
406 Synopsis [Converts the network from the AIG manager into ABC.]
407
408 Description []
409
410 SideEffects []
411
412 SeeAlso []
413
414 ***********************************************************************/
Abc_NtkFromDar(Abc_Ntk_t * pNtkOld,Aig_Man_t * pMan)415 Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
416 {
417 Vec_Ptr_t * vNodes;
418 Abc_Ntk_t * pNtkNew;
419 Aig_Obj_t * pObj;
420 int i;
421 assert( pMan->nAsserts == 0 );
422 // assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) );
423 // perform strashing
424 pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
425 pNtkNew->nConstrs = pMan->nConstrs;
426 pNtkNew->nBarBufs = pNtkOld->nBarBufs;
427 // transfer the pointers to the basic nodes
428 Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
429 Aig_ManForEachCi( pMan, pObj, i )
430 {
431 pObj->pData = Abc_NtkCi(pNtkNew, i);
432 // initialize logic level of the CIs
433 ((Abc_Obj_t *)pObj->pData)->Level = pObj->Level;
434 }
435 // rebuild the AIG
436 vNodes = Aig_ManDfs( pMan, 1 );
437 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
438 if ( Aig_ObjIsBuf(pObj) )
439 pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
440 else
441 pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
442 Vec_PtrFree( vNodes );
443 // connect the PO nodes
444 Aig_ManForEachCo( pMan, pObj, i )
445 {
446 if ( pMan->nAsserts && i == Aig_ManCoNum(pMan) - pMan->nAsserts )
447 break;
448 Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
449 }
450 // if there are assertions, add them
451 if ( !Abc_NtkCheck( pNtkNew ) )
452 Abc_Print( 1, "Abc_NtkFromDar(): Network check has failed.\n" );
453 //Abc_NtkPrintCiLevels( pNtkNew );
454 return pNtkNew;
455 }
456
457 /**Function*************************************************************
458
459 Synopsis [Converts the network from the AIG manager into ABC.]
460
461 Description [This procedure should be called after seq sweeping,
462 which changes the number of registers.]
463
464 SideEffects []
465
466 SeeAlso []
467
468 ***********************************************************************/
Abc_NtkFromDarSeqSweep(Abc_Ntk_t * pNtkOld,Aig_Man_t * pMan)469 Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
470 {
471 Vec_Ptr_t * vNodes;
472 Abc_Ntk_t * pNtkNew;
473 Abc_Obj_t * pObjNew, * pLatch;
474 Aig_Obj_t * pObj, * pObjLo, * pObjLi;
475 int i, iNodeId, nDigits;
476 assert( pMan->nAsserts == 0 );
477 assert( pNtkOld->nBarBufs == 0 );
478 // assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) );
479 // perform strashing
480 pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
481 pNtkNew->nConstrs = pMan->nConstrs;
482 pNtkNew->nBarBufs = pMan->nBarBufs;
483 // consider the case of target enlargement
484 if ( Abc_NtkCiNum(pNtkNew) < Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) )
485 {
486 for ( i = Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) - Abc_NtkCiNum(pNtkNew); i > 0; i-- )
487 {
488 pObjNew = Abc_NtkCreatePi( pNtkNew );
489 Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
490 }
491 Abc_NtkOrderCisCos( pNtkNew );
492 }
493 assert( Abc_NtkCiNum(pNtkNew) == Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) );
494 assert( Abc_NtkCoNum(pNtkNew) == Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) );
495 // transfer the pointers to the basic nodes
496 Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
497 Aig_ManForEachPiSeq( pMan, pObj, i )
498 pObj->pData = Abc_NtkCi(pNtkNew, i);
499 // create as many latches as there are registers in the manager
500 Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
501 {
502 pObjNew = Abc_NtkCreateLatch( pNtkNew );
503 pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
504 pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
505 Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)pObjLi->pData );
506 Abc_ObjAddFanin( (Abc_Obj_t *)pObjLo->pData, pObjNew );
507 Abc_LatchSetInit0( pObjNew );
508 }
509 // rebuild the AIG
510 vNodes = Aig_ManDfs( pMan, 1 );
511 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
512 if ( Aig_ObjIsBuf(pObj) )
513 pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
514 else
515 pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
516 Vec_PtrFree( vNodes );
517 // connect the PO nodes
518 Aig_ManForEachCo( pMan, pObj, i )
519 {
520 // if ( pMan->nAsserts && i == Aig_ManCoNum(pMan) - pMan->nAsserts )
521 // break;
522 iNodeId = Nm_ManFindIdByNameTwoTypes( pNtkNew->pManName, Abc_ObjName(Abc_NtkCo(pNtkNew, i)), ABC_OBJ_PI, ABC_OBJ_BO );
523 if ( iNodeId >= 0 )
524 pObjNew = Abc_NtkObj( pNtkNew, iNodeId );
525 else
526 pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
527 Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
528 }
529 if ( pMan->vFlopNums == NULL )
530 Abc_NtkAddDummyBoxNames( pNtkNew );
531 else
532 {
533 /*
534 {
535 int i, k, iFlop, Counter = 0;
536 FILE * pFile;
537 pFile = fopen( "out.txt", "w" );
538 fAbc_Print( 1, pFile, "The total of %d registers were removed (out of %d):\n",
539 Abc_NtkLatchNum(pNtkOld)-Vec_IntSize(pMan->vFlopNums), Abc_NtkLatchNum(pNtkOld) );
540 for ( i = 0; i < Abc_NtkLatchNum(pNtkOld); i++ )
541 {
542 Vec_IntForEachEntry( pMan->vFlopNums, iFlop, k )
543 {
544 if ( i == iFlop )
545 break;
546 }
547 if ( k == Vec_IntSize(pMan->vFlopNums) )
548 fAbc_Print( 1, pFile, "%6d (%6d) : %s\n", ++Counter, i, Abc_ObjName( Abc_ObjFanout0(Abc_NtkBox(pNtkOld, i)) ) );
549 }
550 fclose( pFile );
551 //Abc_Print( 1, "\n" );
552 }
553 */
554 assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) );
555 nDigits = Abc_Base10Log( Abc_NtkLatchNum(pNtkNew) );
556 Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
557 {
558 pLatch = Abc_NtkBox( pNtkOld, Vec_IntEntry( pMan->vFlopNums, i ) );
559 iNodeId = Nm_ManFindIdByName( pNtkNew->pManName, Abc_ObjName(Abc_ObjFanout0(pLatch)), ABC_OBJ_PO );
560 if ( iNodeId >= 0 )
561 {
562 Abc_ObjAssignName( pObjNew, Abc_ObjNameDummy("l", i, nDigits), NULL );
563 Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjNameDummy("li", i, nDigits), NULL );
564 Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjNameDummy("lo", i, nDigits), NULL );
565 //Abc_Print( 1, "happening %s -> %s\n", Abc_ObjName(Abc_ObjFanin0(pObjNew)), Abc_ObjName(Abc_ObjFanout0(pObjNew)) );
566 continue;
567 }
568 Abc_ObjAssignName( pObjNew, Abc_ObjName(pLatch), NULL );
569 Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjName(Abc_ObjFanin0(pLatch)), NULL );
570 Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pLatch)), NULL );
571 }
572 }
573 // if there are assertions, add them
574 if ( !Abc_NtkCheck( pNtkNew ) )
575 Abc_Print( 1, "Abc_NtkFromDar(): Network check has failed.\n" );
576 return pNtkNew;
577 }
578
579 /**Function*************************************************************
580
581 Synopsis [Converts the network from the AIG manager into ABC.]
582
583 Description [This procedure should be called after seq sweeping,
584 which changes the number of registers.]
585
586 SideEffects []
587
588 SeeAlso []
589
590 ***********************************************************************/
Abc_NtkFromAigPhase(Aig_Man_t * pMan)591 Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan )
592 {
593 Vec_Ptr_t * vNodes;
594 Abc_Ntk_t * pNtkNew;
595 Abc_Obj_t * pObjNew;
596 Aig_Obj_t * pObj, * pObjLo, * pObjLi;
597 int i;
598 assert( pMan->nAsserts == 0 );
599 // perform strashing
600 pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
601 pNtkNew->nConstrs = pMan->nConstrs;
602 pNtkNew->nBarBufs = pMan->nBarBufs;
603 // duplicate the name and the spec
604 // pNtkNew->pName = Extra_UtilStrsav(pMan->pName);
605 // pNtkNew->pSpec = Extra_UtilStrsav(pMan->pSpec);
606 Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
607 // create PIs
608 Aig_ManForEachPiSeq( pMan, pObj, i )
609 {
610 pObjNew = Abc_NtkCreatePi( pNtkNew );
611 // Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
612 pObj->pData = pObjNew;
613 }
614 // create POs
615 Aig_ManForEachPoSeq( pMan, pObj, i )
616 {
617 pObjNew = Abc_NtkCreatePo( pNtkNew );
618 // Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
619 pObj->pData = pObjNew;
620 }
621 assert( Abc_NtkCiNum(pNtkNew) == Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) );
622 assert( Abc_NtkCoNum(pNtkNew) == Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) );
623 // create as many latches as there are registers in the manager
624 Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
625 {
626 pObjNew = Abc_NtkCreateLatch( pNtkNew );
627 pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
628 pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
629 Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)pObjLi->pData );
630 Abc_ObjAddFanin( (Abc_Obj_t *)pObjLo->pData, pObjNew );
631 Abc_LatchSetInit0( pObjNew );
632 // Abc_ObjAssignName( (Abc_Obj_t *)pObjLi->pData, Abc_ObjName((Abc_Obj_t *)pObjLi->pData), NULL );
633 // Abc_ObjAssignName( (Abc_Obj_t *)pObjLo->pData, Abc_ObjName((Abc_Obj_t *)pObjLo->pData), NULL );
634 }
635 // rebuild the AIG
636 vNodes = Aig_ManDfs( pMan, 1 );
637 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
638 if ( Aig_ObjIsBuf(pObj) )
639 pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
640 else
641 pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
642 Vec_PtrFree( vNodes );
643 // connect the PO nodes
644 Aig_ManForEachCo( pMan, pObj, i )
645 {
646 pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
647 Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
648 }
649
650 Abc_NtkAddDummyPiNames( pNtkNew );
651 Abc_NtkAddDummyPoNames( pNtkNew );
652 Abc_NtkAddDummyBoxNames( pNtkNew );
653
654 // check the resulting AIG
655 if ( !Abc_NtkCheck( pNtkNew ) )
656 Abc_Print( 1, "Abc_NtkFromAigPhase(): Network check has failed.\n" );
657 return pNtkNew;
658 }
659
660
661
662 /**Function*************************************************************
663
664 Synopsis [Creates local function of the node.]
665
666 Description []
667
668 SideEffects []
669
670 SeeAlso []
671
672 ***********************************************************************/
Abc_ObjHopFromGia_rec(Hop_Man_t * pHopMan,Gia_Man_t * p,int Id,Vec_Ptr_t * vCopies)673 Hop_Obj_t * Abc_ObjHopFromGia_rec( Hop_Man_t * pHopMan, Gia_Man_t * p, int Id, Vec_Ptr_t * vCopies )
674 {
675 Gia_Obj_t * pObj;
676 Hop_Obj_t * gFunc, * gFunc0, * gFunc1;
677 if ( Gia_ObjIsTravIdCurrentId(p, Id) )
678 return (Hop_Obj_t *)Vec_PtrEntry( vCopies, Id );
679 Gia_ObjSetTravIdCurrentId(p, Id);
680 pObj = Gia_ManObj(p, Id);
681 assert( Gia_ObjIsAnd(pObj) );
682 // compute the functions of the children
683 gFunc0 = Abc_ObjHopFromGia_rec( pHopMan, p, Gia_ObjFaninId0(pObj, Id), vCopies );
684 gFunc1 = Abc_ObjHopFromGia_rec( pHopMan, p, Gia_ObjFaninId1(pObj, Id), vCopies );
685 // get the function of the cut
686 gFunc = Hop_And( pHopMan, Hop_NotCond(gFunc0, Gia_ObjFaninC0(pObj)), Hop_NotCond(gFunc1, Gia_ObjFaninC1(pObj)) );
687 Vec_PtrWriteEntry( vCopies, Id, gFunc );
688 return gFunc;
689 }
Abc_ObjHopFromGia(Hop_Man_t * pHopMan,Gia_Man_t * p,int GiaId,Vec_Ptr_t * vCopies)690 Hop_Obj_t * Abc_ObjHopFromGia( Hop_Man_t * pHopMan, Gia_Man_t * p, int GiaId, Vec_Ptr_t * vCopies )
691 {
692 int k, iFan;
693 assert( Gia_ObjIsLut(p, GiaId) );
694 assert( Gia_ObjLutSize(p, GiaId) > 0 );
695 Gia_ManIncrementTravId( p );
696 Gia_LutForEachFanin( p, GiaId, iFan, k )
697 {
698 Gia_ObjSetTravIdCurrentId(p, iFan);
699 Vec_PtrWriteEntry( vCopies, iFan, Hop_IthVar(pHopMan, k) );
700 }
701 return Abc_ObjHopFromGia_rec( pHopMan, p, GiaId, vCopies );
702 }
703
704 /**Function*************************************************************
705
706 Synopsis [Converts the network from the mapped GIA manager.]
707
708 Description []
709
710 SideEffects []
711
712 SeeAlso []
713
714 ***********************************************************************/
Abc_NtkFromMappedGia_rec(Abc_Ntk_t * pNtkNew,Gia_Man_t * p,int iObj,int fAddInv)715 Abc_Obj_t * Abc_NtkFromMappedGia_rec( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, int iObj, int fAddInv )
716 {
717 Abc_Obj_t * pObjNew;
718 Gia_Obj_t * pObj = Gia_ManObj(p, iObj);
719 if ( Gia_ObjValue(pObj) >= 0 )
720 pObjNew = Abc_NtkObj( pNtkNew, Gia_ObjValue(pObj) );
721 else
722 {
723 Abc_NtkFromMappedGia_rec( pNtkNew, p, Gia_ObjFaninId0(pObj, iObj), 0 );
724 Abc_NtkFromMappedGia_rec( pNtkNew, p, Gia_ObjFaninId1(pObj, iObj), 0 );
725 pObjNew = Abc_NtkCreateNode( pNtkNew );
726 Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ObjFanin0(pObj))) );
727 Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ObjFanin1(pObj))) );
728 pObjNew->pData = Abc_SopCreateAnd( (Mem_Flex_t *)pNtkNew->pManFunc, 2, NULL );
729 if ( Gia_ObjFaninC0(pObj) ) Abc_SopComplementVar( (char *)pObjNew->pData, 0 );
730 if ( Gia_ObjFaninC1(pObj) ) Abc_SopComplementVar( (char *)pObjNew->pData, 1 );
731 pObj->Value = Abc_ObjId( pObjNew );
732 }
733 if ( fAddInv )
734 pObjNew = Abc_NtkCreateNodeInv(pNtkNew, pObjNew);
735 return pObjNew;
736 }
Abc_NtkFromMappedGia(Gia_Man_t * p,int fFindEnables,int fUseBuffs)737 Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p, int fFindEnables, int fUseBuffs )
738 {
739 int fVerbose = 0;
740 int fDuplicate = 0;
741 Abc_Ntk_t * pNtkNew;
742 Abc_Obj_t * pObjNew, * pObjNewLi, * pObjNewLo, * pConst0 = NULL;
743 Gia_Obj_t * pObj, * pObjLi, * pObjLo;
744 Vec_Ptr_t * vReflect;
745 int i, k, iFan, nDupGates, nCountMux = 0;
746 assert( Gia_ManHasMapping(p) || p->pMuxes || fFindEnables );
747 assert( !fFindEnables || !p->pMuxes );
748 pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, Gia_ManHasMapping(p) ? ABC_FUNC_AIG : ABC_FUNC_SOP, 1 );
749 // duplicate the name and the spec
750 pNtkNew->pName = Extra_UtilStrsav(p->pName);
751 pNtkNew->pSpec = Extra_UtilStrsav(p->pSpec);
752 Gia_ManFillValue( p );
753 // create constant
754 pConst0 = Abc_NtkCreateNodeConst0( pNtkNew );
755 Gia_ManConst0(p)->Value = Abc_ObjId(pConst0);
756 // create PIs
757 Gia_ManForEachPi( p, pObj, i )
758 pObj->Value = Abc_ObjId( Abc_NtkCreatePi( pNtkNew ) );
759 // create POs
760 Gia_ManForEachPo( p, pObj, i )
761 pObj->Value = Abc_ObjId( Abc_NtkCreatePo( pNtkNew ) );
762 // create as many latches as there are registers in the manager
763 Gia_ManForEachRiRo( p, pObjLi, pObjLo, i )
764 {
765 pObjNew = Abc_NtkCreateLatch( pNtkNew );
766 pObjNewLi = Abc_NtkCreateBi( pNtkNew );
767 pObjNewLo = Abc_NtkCreateBo( pNtkNew );
768 Abc_ObjAddFanin( pObjNew, pObjNewLi );
769 Abc_ObjAddFanin( pObjNewLo, pObjNew );
770 pObjLi->Value = Abc_ObjId( pObjNewLi );
771 pObjLo->Value = Abc_ObjId( pObjNewLo );
772 Abc_LatchSetInit0( pObjNew );
773 }
774 // rebuild the AIG
775 if ( fFindEnables )
776 {
777 Gia_ManForEachCo( p, pObj, i )
778 {
779 pObjNew = NULL;
780 if ( Gia_ObjIsRi(p, pObj) && Gia_ObjIsMuxType(Gia_ObjFanin0(pObj)) )
781 {
782 int iObjRo = Gia_ObjRiToRoId( p, Gia_ObjId(p, pObj) );
783 int iLitE, iLitT, iCtrl = Gia_ObjRecognizeMuxLits( p, Gia_ObjFanin0(pObj), &iLitT, &iLitE );
784 iLitE = Abc_LitNotCond( iLitE, Gia_ObjFaninC0(pObj) );
785 iLitT = Abc_LitNotCond( iLitT, Gia_ObjFaninC0(pObj) );
786 if ( Abc_Lit2Var(iLitT) == iObjRo )
787 {
788 int iTemp = iLitE;
789 iLitE = iLitT;
790 iLitT = iTemp;
791 iCtrl = Abc_LitNot( iCtrl );
792 }
793 if ( Abc_Lit2Var(iLitE) == iObjRo )
794 {
795 Abc_Obj_t * pObjCtrl = Abc_NtkFromMappedGia_rec( pNtkNew, p, Abc_Lit2Var(iCtrl), Abc_LitIsCompl(iCtrl) );
796 Abc_Obj_t * pObjNodeT = Abc_NtkFromMappedGia_rec( pNtkNew, p, Abc_Lit2Var(iLitT), Abc_LitIsCompl(iLitT) );
797 Abc_Obj_t * pObjNodeE = Abc_NtkFromMappedGia_rec( pNtkNew, p, Abc_Lit2Var(iLitE), Abc_LitIsCompl(iLitE) );
798 pObjNew = Abc_NtkCreateNode( pNtkNew );
799 Abc_ObjAddFanin( pObjNew, pObjCtrl );
800 Abc_ObjAddFanin( pObjNew, pObjNodeT );
801 Abc_ObjAddFanin( pObjNew, pObjNodeE );
802 pObjNew->pData = Abc_SopCreateMux( (Mem_Flex_t *)pNtkNew->pManFunc );
803 nCountMux++;
804 }
805 }
806 if ( pObjNew == NULL )
807 pObjNew = Abc_NtkFromMappedGia_rec( pNtkNew, p, Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninC0(pObj) );
808 Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
809 }
810 }
811 else if ( p->pMuxes )
812 {
813 Gia_ManForEachAnd( p, pObj, i )
814 {
815 pObjNew = Abc_NtkCreateNode( pNtkNew );
816 if ( Gia_ObjIsMuxId(p, i) )
817 {
818 Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ObjFanin2(p, pObj))) );
819 Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ObjFanin1(pObj))) );
820 Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ObjFanin0(pObj))) );
821 pObjNew->pData = Abc_SopCreateMux( (Mem_Flex_t *)pNtkNew->pManFunc );
822 if ( Gia_ObjFaninC2(p, pObj) ) Abc_SopComplementVar( (char *)pObjNew->pData, 0 );
823 if ( Gia_ObjFaninC1(pObj) ) Abc_SopComplementVar( (char *)pObjNew->pData, 1 );
824 if ( Gia_ObjFaninC0(pObj) ) Abc_SopComplementVar( (char *)pObjNew->pData, 2 );
825 }
826 else if ( Gia_ObjIsXor(pObj) )
827 {
828 Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ObjFanin0(pObj))) );
829 Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ObjFanin1(pObj))) );
830 pObjNew->pData = Abc_SopCreateXor( (Mem_Flex_t *)pNtkNew->pManFunc, 2 );
831 if ( Gia_ObjFaninC0(pObj) ) Abc_SopComplementVar( (char *)pObjNew->pData, 0 );
832 if ( Gia_ObjFaninC1(pObj) ) Abc_SopComplementVar( (char *)pObjNew->pData, 1 );
833 }
834 else
835 {
836 Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ObjFanin0(pObj))) );
837 Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ObjFanin1(pObj))) );
838 pObjNew->pData = Abc_SopCreateAnd( (Mem_Flex_t *)pNtkNew->pManFunc, 2, NULL );
839 if ( Gia_ObjFaninC0(pObj) ) Abc_SopComplementVar( (char *)pObjNew->pData, 0 );
840 if ( Gia_ObjFaninC1(pObj) ) Abc_SopComplementVar( (char *)pObjNew->pData, 1 );
841 }
842 pObj->Value = Abc_ObjId( pObjNew );
843 }
844 }
845 else
846 {
847 vReflect = Vec_PtrStart( Gia_ManObjNum(p) );
848 Gia_ManForEachLut( p, i )
849 {
850 pObj = Gia_ManObj(p, i);
851 assert( pObj->Value == ~0 );
852 if ( Gia_ObjLutSize(p, i) == 0 )
853 {
854 pObj->Value = Abc_ObjId(pConst0);
855 continue;
856 }
857 pObjNew = Abc_NtkCreateNode( pNtkNew );
858 Gia_LutForEachFanin( p, i, iFan, k )
859 Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ManObj(p, iFan))) );
860 pObjNew->pData = Abc_ObjHopFromGia( (Hop_Man_t *)pNtkNew->pManFunc, p, i, vReflect );
861 pObj->Value = Abc_ObjId( pObjNew );
862 }
863 Vec_PtrFree( vReflect );
864 }
865 //if ( fFindEnables )
866 // printf( "Extracted %d flop enable signals.\n", nCountMux );
867 // connect the PO nodes
868 if ( !fFindEnables )
869 Gia_ManForEachCo( p, pObj, i )
870 {
871 pObjNew = Abc_NtkObj( pNtkNew, Gia_ObjValue(Gia_ObjFanin0(pObj)) );
872 Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), Abc_ObjNotCond( pObjNew, Gia_ObjFaninC0(pObj) ) );
873 }
874 // create names
875 Abc_NtkAddDummyPiNames( pNtkNew );
876 Abc_NtkAddDummyPoNames( pNtkNew );
877 Abc_NtkAddDummyBoxNames( pNtkNew );
878
879 // decouple the PO driver nodes to reduce the number of levels
880 nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, !fUseBuffs );
881 if ( fVerbose && nDupGates && !Abc_FrameReadFlag("silentmode") )
882 {
883 if ( !fDuplicate )
884 printf( "Added %d buffers/inverters to decouple the CO drivers.\n", nDupGates );
885 else
886 printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
887 }
888 // remove const node if it is not used
889 if ( !Abc_ObjIsNone(pConst0) && Abc_ObjFanoutNum(pConst0) == 0 )
890 Abc_NtkDeleteObj( pConst0 );
891
892 assert( Gia_ManPiNum(p) == Abc_NtkPiNum(pNtkNew) );
893 assert( Gia_ManPoNum(p) == Abc_NtkPoNum(pNtkNew) );
894 assert( Gia_ManRegNum(p) == Abc_NtkLatchNum(pNtkNew) );
895
896 // check the resulting AIG
897 if ( !Abc_NtkCheck( pNtkNew ) )
898 Abc_Print( 1, "Abc_NtkFromMappedGia(): Network check has failed.\n" );
899 return pNtkNew;
900 }
901
902 /**Function*************************************************************
903
904 Synopsis [Converts the network from the mapped GIA manager.]
905
906 Description []
907
908 SideEffects []
909
910 SeeAlso []
911
912 ***********************************************************************/
Abc_NtkFromCellWrite(Vec_Int_t * vCopyLits,int i,int c,int Id)913 static inline void Abc_NtkFromCellWrite( Vec_Int_t * vCopyLits, int i, int c, int Id )
914 {
915 Vec_IntWriteEntry( vCopyLits, Abc_Var2Lit(i, c), Id );
916 }
Abc_NtkFromCellRead(Abc_Ntk_t * p,Vec_Int_t * vCopyLits,int i,int c)917 static inline Abc_Obj_t * Abc_NtkFromCellRead( Abc_Ntk_t * p, Vec_Int_t * vCopyLits, int i, int c )
918 {
919 Abc_Obj_t * pObjNew;
920 int iObjNew = Vec_IntEntry( vCopyLits, Abc_Var2Lit(i, c) );
921 if ( iObjNew >= 0 )
922 return Abc_NtkObj(p, iObjNew);
923 // opposite phase should be already constructed
924 assert( 0 );
925 if ( i == 0 )
926 pObjNew = c ? Abc_NtkCreateNodeConst1(p) : Abc_NtkCreateNodeConst0(p);
927 else
928 {
929 iObjNew = Vec_IntEntry( vCopyLits, Abc_Var2Lit(i, !c) ); assert( iObjNew >= 0 );
930 pObjNew = Abc_NtkCreateNodeInv( p, Abc_NtkObj(p, iObjNew) );
931 }
932 Abc_NtkFromCellWrite( vCopyLits, i, c, Abc_ObjId(pObjNew) );
933 return pObjNew;
934 }
Abc_NtkFromCellMappedGia(Gia_Man_t * p,int fUseBuffs)935 Abc_Ntk_t * Abc_NtkFromCellMappedGia( Gia_Man_t * p, int fUseBuffs )
936 {
937 int fFixDrivers = 1;
938 int fVerbose = 0;
939 Abc_Ntk_t * pNtkNew;
940 Vec_Int_t * vCopyLits;
941 Abc_Obj_t * pObjNew, * pObjNewLi, * pObjNewLo;
942 Gia_Obj_t * pObj, * pObjLi, * pObjLo;
943 int i, k, iLit, iFanLit, nCells, fNeedConst[2] = {0};
944 Mio_Cell2_t * pCells = Mio_CollectRootsNewDefault2( 6, &nCells, 0 );
945 assert( Gia_ManHasCellMapping(p) );
946 // start network
947 pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_MAP, 1 );
948 pNtkNew->pName = Extra_UtilStrsav(p->pName);
949 pNtkNew->pSpec = Extra_UtilStrsav(p->pSpec);
950 assert( pNtkNew->pManFunc == Abc_FrameReadLibGen() );
951 vCopyLits = Vec_IntStartFull( 2*Gia_ManObjNum(p) );
952 // create PIs
953 Gia_ManForEachPi( p, pObj, i )
954 Abc_NtkFromCellWrite( vCopyLits, Gia_ObjId(p, pObj), 0, Abc_ObjId( Abc_NtkCreatePi( pNtkNew ) ) );
955 // create POs
956 Gia_ManForEachPo( p, pObj, i )
957 Abc_NtkFromCellWrite( vCopyLits, Gia_ObjId(p, pObj), 0, Abc_ObjId( Abc_NtkCreatePo( pNtkNew ) ) );
958 // create as many latches as there are registers in the manager
959 Gia_ManForEachRiRo( p, pObjLi, pObjLo, i )
960 {
961 pObjNew = Abc_NtkCreateLatch( pNtkNew );
962 pObjNewLi = Abc_NtkCreateBi( pNtkNew );
963 pObjNewLo = Abc_NtkCreateBo( pNtkNew );
964 Abc_ObjAddFanin( pObjNew, pObjNewLi );
965 Abc_ObjAddFanin( pObjNewLo, pObjNew );
966 // pObjLi->Value = Abc_ObjId( pObjNewLi );
967 // pObjLo->Value = Abc_ObjId( pObjNewLo );
968 Abc_NtkFromCellWrite( vCopyLits, Gia_ObjId(p, pObjLi), 0, Abc_ObjId( pObjNewLi ) );
969 Abc_NtkFromCellWrite( vCopyLits, Gia_ObjId(p, pObjLo), 0, Abc_ObjId( pObjNewLo ) );
970 Abc_LatchSetInit0( pObjNew );
971 }
972
973 // create constants
974 Gia_ManForEachCo( p, pObj, i )
975 if ( Gia_ObjFaninId0p(p, pObj) == 0 )
976 fNeedConst[Gia_ObjFaninC0(pObj)] = 1;
977 Gia_ManForEachBuf( p, pObj, i )
978 if ( Gia_ObjFaninId0p(p, pObj) == 0 )
979 fNeedConst[Gia_ObjFaninC0(pObj)] = 1;
980 if ( fNeedConst[0] )
981 Abc_NtkFromCellWrite( vCopyLits, 0, 0, Abc_ObjId(Abc_NtkCreateNodeConst0(pNtkNew)) );
982 if ( fNeedConst[1] )
983 Abc_NtkFromCellWrite( vCopyLits, 0, 1, Abc_ObjId(Abc_NtkCreateNodeConst1(pNtkNew)) );
984
985 // rebuild the AIG
986 Gia_ManForEachCell( p, iLit )
987 {
988 int fSkip = 0;
989 if ( Gia_ObjIsCellBuf(p, iLit) )
990 {
991 assert( !Abc_LitIsCompl(iLit) );
992 // build buffer
993 pObjNew = Abc_NtkCreateNode( pNtkNew );
994 iFanLit = Gia_ObjFaninLit0p( p, Gia_ManObj(p, Abc_Lit2Var(iLit)) );
995 Abc_ObjAddFanin( pObjNew, Abc_NtkFromCellRead(pNtkNew, vCopyLits, Abc_Lit2Var(iFanLit), Abc_LitIsCompl(iFanLit)) );
996 pObjNew->pData = NULL; // barrier buffer
997 assert( Abc_ObjIsBarBuf(pObjNew) );
998 pNtkNew->nBarBufs2++;
999 }
1000 else if ( Gia_ObjIsCellInv(p, iLit) )
1001 {
1002 int iLitNot = Abc_LitNot(iLit);
1003 if ( !Abc_LitIsCompl(iLit) ) // positive phase
1004 {
1005 // build negative phase
1006 assert( Vec_IntEntry(vCopyLits, iLitNot) == -1 );
1007 assert( Gia_ObjCellId(p, iLitNot) > 0 );
1008 pObjNew = Abc_NtkCreateNode( pNtkNew );
1009 Gia_CellForEachFanin( p, iLitNot, iFanLit, k )
1010 Abc_ObjAddFanin( pObjNew, Abc_NtkFromCellRead(pNtkNew, vCopyLits, Abc_Lit2Var(iFanLit), Abc_LitIsCompl(iFanLit)) );
1011 pObjNew->pData = Mio_LibraryReadGateByName( (Mio_Library_t *)pNtkNew->pManFunc, pCells[Gia_ObjCellId(p, iLitNot)].pName, NULL );
1012 Abc_NtkFromCellWrite( vCopyLits, Abc_Lit2Var(iLitNot), Abc_LitIsCompl(iLitNot), Abc_ObjId(pObjNew) );
1013 fSkip = 1;
1014 }
1015 else // negative phase
1016 {
1017 // positive phase is available
1018 assert( Vec_IntEntry(vCopyLits, iLitNot) != -1 );
1019 }
1020 // build inverter
1021 pObjNew = Abc_NtkCreateNode( pNtkNew );
1022 Abc_ObjAddFanin( pObjNew, Abc_NtkFromCellRead(pNtkNew, vCopyLits, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLitNot)) );
1023 pObjNew->pData = Mio_LibraryReadGateByName( (Mio_Library_t *)pNtkNew->pManFunc, pCells[3].pName, NULL );
1024 }
1025 else
1026 {
1027 assert( Gia_ObjCellId(p, iLit) >= 0 );
1028 pObjNew = Abc_NtkCreateNode( pNtkNew );
1029 Gia_CellForEachFanin( p, iLit, iFanLit, k )
1030 Abc_ObjAddFanin( pObjNew, Abc_NtkFromCellRead(pNtkNew, vCopyLits, Abc_Lit2Var(iFanLit), Abc_LitIsCompl(iFanLit)) );
1031 pObjNew->pData = Mio_LibraryReadGateByName( (Mio_Library_t *)pNtkNew->pManFunc, pCells[Gia_ObjCellId(p, iLit)].pName, NULL );
1032 }
1033 assert( Vec_IntEntry(vCopyLits, iLit) == -1 );
1034 Abc_NtkFromCellWrite( vCopyLits, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLit), Abc_ObjId(pObjNew) );
1035 // skip next
1036 iLit += fSkip;
1037 }
1038
1039 // connect the PO nodes
1040 Gia_ManForEachCo( p, pObj, i )
1041 {
1042 pObjNew = Abc_NtkFromCellRead( pNtkNew, vCopyLits, Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninC0(pObj) );
1043 Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
1044 }
1045 // create names
1046 Abc_NtkAddDummyPiNames( pNtkNew );
1047 Abc_NtkAddDummyPoNames( pNtkNew );
1048 Abc_NtkAddDummyBoxNames( pNtkNew );
1049
1050 // decouple the PO driver nodes to reduce the number of levels
1051 if ( fFixDrivers )
1052 {
1053 int nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, !fUseBuffs );
1054 if ( fVerbose && nDupGates && !Abc_FrameReadFlag("silentmode") )
1055 {
1056 if ( fUseBuffs )
1057 printf( "Added %d buffers/inverters to decouple the CO drivers.\n", nDupGates );
1058 else
1059 printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
1060 }
1061 }
1062
1063 assert( Gia_ManPiNum(p) == Abc_NtkPiNum(pNtkNew) );
1064 assert( Gia_ManPoNum(p) == Abc_NtkPoNum(pNtkNew) );
1065 assert( Gia_ManRegNum(p) == Abc_NtkLatchNum(pNtkNew) );
1066 Vec_IntFree( vCopyLits );
1067 ABC_FREE( pCells );
1068
1069 // check the resulting AIG
1070 if ( !Abc_NtkCheck( pNtkNew ) )
1071 Abc_Print( 1, "Abc_NtkFromMappedGia(): Network check has failed.\n" );
1072 return pNtkNew;
1073 }
1074
1075
1076 /**Function*************************************************************
1077
1078 Synopsis [Converts the network from the AIG manager into ABC.]
1079
1080 Description [This procedure should be called after seq sweeping,
1081 which changes the number of registers.]
1082
1083 SideEffects []
1084
1085 SeeAlso []
1086
1087 ***********************************************************************/
Abc_NtkAfterTrim(Aig_Man_t * pMan,Abc_Ntk_t * pNtkOld)1088 Abc_Ntk_t * Abc_NtkAfterTrim( Aig_Man_t * pMan, Abc_Ntk_t * pNtkOld )
1089 {
1090 Vec_Ptr_t * vNodes;
1091 Abc_Ntk_t * pNtkNew;
1092 Abc_Obj_t * pObjNew, * pObjOld;
1093 Aig_Obj_t * pObj, * pObjLo, * pObjLi;
1094 int i;
1095 assert( pMan->nAsserts == 0 );
1096 assert( pNtkOld->nBarBufs == 0 );
1097 assert( Aig_ManRegNum(pMan) <= Abc_NtkLatchNum(pNtkOld) );
1098 assert( Saig_ManPiNum(pMan) <= Abc_NtkCiNum(pNtkOld) );
1099 assert( Saig_ManPoNum(pMan) == Abc_NtkPoNum(pNtkOld) );
1100 assert( pMan->vCiNumsOrig != NULL );
1101 // perform strashing
1102 pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
1103 pNtkNew->nConstrs = pMan->nConstrs;
1104 pNtkNew->nBarBufs = pMan->nBarBufs;
1105 // duplicate the name and the spec
1106 // pNtkNew->pName = Extra_UtilStrsav(pMan->pName);
1107 // pNtkNew->pSpec = Extra_UtilStrsav(pMan->pSpec);
1108 Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
1109 // create PIs
1110 Aig_ManForEachPiSeq( pMan, pObj, i )
1111 {
1112 pObjNew = Abc_NtkCreatePi( pNtkNew );
1113 pObj->pData = pObjNew;
1114 // find the name
1115 pObjOld = Abc_NtkCi( pNtkOld, Vec_IntEntry(pMan->vCiNumsOrig, i) );
1116 Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjOld), NULL );
1117 }
1118 // create POs
1119 Aig_ManForEachPoSeq( pMan, pObj, i )
1120 {
1121 pObjNew = Abc_NtkCreatePo( pNtkNew );
1122 pObj->pData = pObjNew;
1123 // find the name
1124 pObjOld = Abc_NtkCo( pNtkOld, i );
1125 Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjOld), NULL );
1126 }
1127 assert( Abc_NtkCiNum(pNtkNew) == Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) );
1128 assert( Abc_NtkCoNum(pNtkNew) == Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) );
1129 // create as many latches as there are registers in the manager
1130 Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
1131 {
1132 pObjNew = Abc_NtkCreateLatch( pNtkNew );
1133 pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
1134 pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
1135 Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)pObjLi->pData );
1136 Abc_ObjAddFanin( (Abc_Obj_t *)pObjLo->pData, pObjNew );
1137 Abc_LatchSetInit0( pObjNew );
1138 // find the name
1139 pObjOld = Abc_NtkCi( pNtkOld, Vec_IntEntry(pMan->vCiNumsOrig, Saig_ManPiNum(pMan)+i) );
1140 Abc_ObjAssignName( (Abc_Obj_t *)pObjLo->pData, Abc_ObjName(pObjOld), NULL );
1141 // find the name
1142 pObjOld = Abc_NtkCo( pNtkOld, Saig_ManPoNum(pMan)+i );
1143 Abc_ObjAssignName( (Abc_Obj_t *)pObjLi->pData, Abc_ObjName(pObjOld), NULL );
1144 }
1145 // rebuild the AIG
1146 vNodes = Aig_ManDfs( pMan, 1 );
1147 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
1148 if ( Aig_ObjIsBuf(pObj) )
1149 pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
1150 else
1151 pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
1152 Vec_PtrFree( vNodes );
1153 // connect the PO nodes
1154 Aig_ManForEachCo( pMan, pObj, i )
1155 {
1156 pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
1157 Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
1158 }
1159 // check the resulting AIG
1160 if ( !Abc_NtkCheck( pNtkNew ) )
1161 Abc_Print( 1, "Abc_NtkAfterTrim(): Network check has failed.\n" );
1162 return pNtkNew;
1163 }
1164
1165 /**Function*************************************************************
1166
1167 Synopsis [Converts the network from the AIG manager into ABC.]
1168
1169 Description []
1170
1171 SideEffects []
1172
1173 SeeAlso []
1174
1175 ***********************************************************************/
Abc_NtkFromDarChoices(Abc_Ntk_t * pNtkOld,Aig_Man_t * pMan)1176 Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
1177 {
1178 Abc_Ntk_t * pNtkNew;
1179 Aig_Obj_t * pObj, * pTemp;
1180 int i;
1181 assert( pMan->pEquivs != NULL );
1182 assert( Aig_ManBufNum(pMan) == 0 );
1183 // perform strashing
1184 pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
1185 pNtkNew->nConstrs = pMan->nConstrs;
1186 pNtkNew->nBarBufs = pNtkOld->nBarBufs;
1187 // transfer the pointers to the basic nodes
1188 Aig_ManCleanData( pMan );
1189 Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
1190 Aig_ManForEachCi( pMan, pObj, i )
1191 pObj->pData = Abc_NtkCi(pNtkNew, i);
1192 // rebuild the AIG
1193 Aig_ManForEachNode( pMan, pObj, i )
1194 {
1195 pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
1196 if ( (pTemp = Aig_ObjEquiv(pMan, pObj)) )
1197 {
1198 assert( pTemp->pData != NULL );
1199 ((Abc_Obj_t *)pObj->pData)->pData = ((Abc_Obj_t *)pTemp->pData);
1200 }
1201 }
1202 // connect the PO nodes
1203 Aig_ManForEachCo( pMan, pObj, i )
1204 Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
1205 if ( !Abc_NtkCheck( pNtkNew ) )
1206 Abc_Print( 1, "Abc_NtkFromDar(): Network check has failed.\n" );
1207
1208 // verify topological order
1209 if ( 0 )
1210 {
1211 Abc_Obj_t * pNode;
1212 Abc_NtkForEachNode( pNtkNew, pNode, i )
1213 if ( Abc_AigNodeIsChoice( pNode ) )
1214 {
1215 int Counter = 0;
1216 for ( pNode = Abc_ObjEquiv(pNode); pNode; pNode = Abc_ObjEquiv(pNode) )
1217 Counter++;
1218 printf( "%d ", Counter );
1219 }
1220 printf( "\n" );
1221 }
1222 return pNtkNew;
1223 }
1224
1225 /**Function*************************************************************
1226
1227 Synopsis [Converts the network from the AIG manager into ABC.]
1228
1229 Description []
1230
1231 SideEffects []
1232
1233 SeeAlso []
1234
1235 ***********************************************************************/
Abc_NtkFromDarSeq(Abc_Ntk_t * pNtkOld,Aig_Man_t * pMan)1236 Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
1237 {
1238 Vec_Ptr_t * vNodes;
1239 Abc_Ntk_t * pNtkNew;
1240 Abc_Obj_t * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
1241 Aig_Obj_t * pObj;
1242 int i;
1243 // assert( Aig_ManLatchNum(pMan) > 0 );
1244 assert( pNtkOld->nBarBufs == 0 );
1245 // perform strashing
1246 pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
1247 pNtkNew->nConstrs = pMan->nConstrs;
1248 pNtkNew->nBarBufs = pMan->nBarBufs;
1249 // transfer the pointers to the basic nodes
1250 Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
1251 Aig_ManForEachCi( pMan, pObj, i )
1252 pObj->pData = Abc_NtkPi(pNtkNew, i);
1253 // create latches of the new network
1254 Aig_ManForEachObj( pMan, pObj, i )
1255 {
1256 pObjNew = Abc_NtkCreateLatch( pNtkNew );
1257 pFaninNew0 = Abc_NtkCreateBi( pNtkNew );
1258 pFaninNew1 = Abc_NtkCreateBo( pNtkNew );
1259 Abc_ObjAddFanin( pObjNew, pFaninNew0 );
1260 Abc_ObjAddFanin( pFaninNew1, pObjNew );
1261 Abc_LatchSetInit0( pObjNew );
1262 pObj->pData = Abc_ObjFanout0( pObjNew );
1263 }
1264 Abc_NtkAddDummyBoxNames( pNtkNew );
1265 // rebuild the AIG
1266 vNodes = Aig_ManDfs( pMan, 1 );
1267 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
1268 {
1269 // add the first fanin
1270 pObj->pData = pFaninNew0 = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
1271 if ( Aig_ObjIsBuf(pObj) )
1272 continue;
1273 // add the second fanin
1274 pFaninNew1 = (Abc_Obj_t *)Aig_ObjChild1Copy(pObj);
1275 // create the new node
1276 if ( Aig_ObjIsExor(pObj) )
1277 pObj->pData = pObjNew = Abc_AigXor( (Abc_Aig_t *)pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
1278 else
1279 pObj->pData = pObjNew = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, pFaninNew0, pFaninNew1 );
1280 }
1281 Vec_PtrFree( vNodes );
1282 // connect the PO nodes
1283 Aig_ManForEachCo( pMan, pObj, i )
1284 {
1285 pFaninNew = (Abc_Obj_t *)Aig_ObjChild0Copy( pObj );
1286 Abc_ObjAddFanin( Abc_NtkPo(pNtkNew, i), pFaninNew );
1287 }
1288 // connect the latches
1289 Aig_ManForEachObj( pMan, pObj, i )
1290 {
1291 pFaninNew = (Abc_Obj_t *)Aig_ObjChild0Copy( pObj );
1292 Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0((Abc_Obj_t *)pObj->pData)), pFaninNew );
1293 }
1294 if ( !Abc_NtkCheck( pNtkNew ) )
1295 Abc_Print( 1, "Abc_NtkFromIvySeq(): Network check has failed.\n" );
1296 return pNtkNew;
1297 }
1298
1299 /**Function*************************************************************
1300
1301 Synopsis [Collects CI of the network.]
1302
1303 Description []
1304
1305 SideEffects []
1306
1307 SeeAlso []
1308
1309 ***********************************************************************/
Abc_NtkCollectCiNames(Abc_Ntk_t * pNtk)1310 Vec_Ptr_t * Abc_NtkCollectCiNames( Abc_Ntk_t * pNtk )
1311 {
1312 Abc_Obj_t * pObj;
1313 int i;
1314 Vec_Ptr_t * vNames;
1315 vNames = Vec_PtrAlloc( 100 );
1316 Abc_NtkForEachCi( pNtk, pObj, i )
1317 Vec_PtrPush( vNames, Extra_UtilStrsav(Abc_ObjName(pObj)) );
1318 return vNames;
1319 }
1320
1321 /**Function*************************************************************
1322
1323 Synopsis [Collects CO of the network.]
1324
1325 Description []
1326
1327 SideEffects []
1328
1329 SeeAlso []
1330
1331 ***********************************************************************/
Abc_NtkCollectCoNames(Abc_Ntk_t * pNtk)1332 Vec_Ptr_t * Abc_NtkCollectCoNames( Abc_Ntk_t * pNtk )
1333 {
1334 Abc_Obj_t * pObj;
1335 int i;
1336 Vec_Ptr_t * vNames;
1337 vNames = Vec_PtrAlloc( 100 );
1338 Abc_NtkForEachCo( pNtk, pObj, i )
1339 Vec_PtrPush( vNames, Extra_UtilStrsav(Abc_ObjName(pObj)) );
1340 return vNames;
1341 }
1342
1343 /**Function*************************************************************
1344
1345 Synopsis [Collect latch values.]
1346
1347 Description []
1348
1349 SideEffects []
1350
1351 SeeAlso []
1352
1353 ***********************************************************************/
Abc_NtkGetLatchValues(Abc_Ntk_t * pNtk)1354 Vec_Int_t * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk )
1355 {
1356 Vec_Int_t * vInits;
1357 Abc_Obj_t * pLatch;
1358 int i;
1359 vInits = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
1360 Abc_NtkForEachLatch( pNtk, pLatch, i )
1361 {
1362 if ( Abc_LatchIsInit0(pLatch) )
1363 Vec_IntPush( vInits, 0 );
1364 else if ( Abc_LatchIsInit1(pLatch) )
1365 Vec_IntPush( vInits, 1 );
1366 else if ( Abc_LatchIsInitDc(pLatch) )
1367 Vec_IntPush( vInits, 2 );
1368 else
1369 assert( 0 );
1370 }
1371 return vInits;
1372 }
1373
1374 /**Function*************************************************************
1375
1376 Synopsis [Gives the current ABC network to AIG manager for processing.]
1377
1378 Description []
1379
1380 SideEffects []
1381
1382 SeeAlso []
1383
1384 ***********************************************************************/
Abc_NtkDar(Abc_Ntk_t * pNtk)1385 Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
1386 {
1387 Abc_Ntk_t * pNtkAig = NULL;
1388 Aig_Man_t * pMan;
1389 extern void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim );
1390
1391 assert( Abc_NtkIsStrash(pNtk) );
1392 // convert to the AIG manager
1393 pMan = Abc_NtkToDar( pNtk, 0, 0 );
1394 if ( pMan == NULL )
1395 return NULL;
1396
1397 // perform computation
1398 // Fra_ManPartitionTest( pMan, 4 );
1399 pNtkAig = Abc_NtkFromDar( pNtk, pMan );
1400 Aig_ManStop( pMan );
1401
1402 // make sure everything is okay
1403 if ( pNtkAig && !Abc_NtkCheck( pNtkAig ) )
1404 {
1405 Abc_Print( 1, "Abc_NtkDar: The network check has failed.\n" );
1406 Abc_NtkDelete( pNtkAig );
1407 return NULL;
1408 }
1409 return pNtkAig;
1410 }
1411
1412
1413 /**Function*************************************************************
1414
1415 Synopsis [Gives the current ABC network to AIG manager for processing.]
1416
1417 Description []
1418
1419 SideEffects []
1420
1421 SeeAlso []
1422
1423 ***********************************************************************/
Abc_NtkDarFraig(Abc_Ntk_t * pNtk,int nConfLimit,int fDoSparse,int fProve,int fTransfer,int fSpeculate,int fChoicing,int fVerbose)1424 Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fChoicing, int fVerbose )
1425 {
1426 Fra_Par_t Pars, * pPars = &Pars;
1427 Abc_Ntk_t * pNtkAig;
1428 Aig_Man_t * pMan, * pTemp;
1429 pMan = Abc_NtkToDar( pNtk, 0, 0 );
1430 if ( pMan == NULL )
1431 return NULL;
1432 Fra_ParamsDefault( pPars );
1433 pPars->nBTLimitNode = nConfLimit;
1434 pPars->fChoicing = fChoicing;
1435 pPars->fDoSparse = fDoSparse;
1436 pPars->fSpeculate = fSpeculate;
1437 pPars->fProve = fProve;
1438 pPars->fVerbose = fVerbose;
1439 pMan = Fra_FraigPerform( pTemp = pMan, pPars );
1440 if ( fChoicing )
1441 pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
1442 else
1443 pNtkAig = Abc_NtkFromDar( pNtk, pMan );
1444 Aig_ManStop( pTemp );
1445 Aig_ManStop( pMan );
1446 return pNtkAig;
1447 }
1448
1449 /**Function*************************************************************
1450
1451 Synopsis [Gives the current ABC network to AIG manager for processing.]
1452
1453 Description []
1454
1455 SideEffects []
1456
1457 SeeAlso []
1458
1459 ***********************************************************************/
Abc_NtkDarFraigPart(Abc_Ntk_t * pNtk,int nPartSize,int nConfLimit,int nLevelMax,int fVerbose)1460 Abc_Ntk_t * Abc_NtkDarFraigPart( Abc_Ntk_t * pNtk, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose )
1461 {
1462 Abc_Ntk_t * pNtkAig;
1463 Aig_Man_t * pMan, * pTemp;
1464 pMan = Abc_NtkToDar( pNtk, 0, 0 );
1465 if ( pMan == NULL )
1466 return NULL;
1467 pMan = Aig_ManFraigPartitioned( pTemp = pMan, nPartSize, nConfLimit, nLevelMax, fVerbose );
1468 Aig_ManStop( pTemp );
1469 pNtkAig = Abc_NtkFromDar( pNtk, pMan );
1470 Aig_ManStop( pMan );
1471 return pNtkAig;
1472 }
1473
1474 /**Function*************************************************************
1475
1476 Synopsis [Gives the current ABC network to AIG manager for processing.]
1477
1478 Description []
1479
1480 SideEffects []
1481
1482 SeeAlso []
1483
1484 ***********************************************************************/
Abc_NtkCSweep(Abc_Ntk_t * pNtk,int nCutsMax,int nLeafMax,int fVerbose)1485 Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVerbose )
1486 {
1487 // extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );
1488 Abc_Ntk_t * pNtkAig;
1489 Aig_Man_t * pMan, * pTemp;
1490 pMan = Abc_NtkToDar( pNtk, 0, 0 );
1491 if ( pMan == NULL )
1492 return NULL;
1493 pMan = Csw_Sweep( pTemp = pMan, nCutsMax, nLeafMax, fVerbose );
1494 pNtkAig = Abc_NtkFromDar( pNtk, pMan );
1495 Aig_ManStop( pTemp );
1496 Aig_ManStop( pMan );
1497 return pNtkAig;
1498 }
1499
1500 /**Function*************************************************************
1501
1502 Synopsis [Gives the current ABC network to AIG manager for processing.]
1503
1504 Description []
1505
1506 SideEffects []
1507
1508 SeeAlso []
1509
1510 ***********************************************************************/
Abc_NtkDRewrite(Abc_Ntk_t * pNtk,Dar_RwrPar_t * pPars)1511 Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars )
1512 {
1513 Aig_Man_t * pMan, * pTemp;
1514 Abc_Ntk_t * pNtkAig;
1515 abctime clk;
1516 assert( Abc_NtkIsStrash(pNtk) );
1517 pMan = Abc_NtkToDar( pNtk, 0, 0 );
1518 if ( pMan == NULL )
1519 return NULL;
1520 // Aig_ManPrintStats( pMan );
1521 /*
1522 // Aig_ManSupports( pMan );
1523 {
1524 Vec_Vec_t * vParts;
1525 vParts = Aig_ManPartitionSmart( pMan, 50, 1, NULL );
1526 Vec_VecFree( vParts );
1527 }
1528 */
1529 Dar_ManRewrite( pMan, pPars );
1530 // pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
1531 // Aig_ManStop( pTemp );
1532
1533 clk = Abc_Clock();
1534 pMan = Aig_ManDupDfs( pTemp = pMan );
1535 Aig_ManStop( pTemp );
1536 //ABC_PRT( "time", Abc_Clock() - clk );
1537
1538 // Aig_ManPrintStats( pMan );
1539 pNtkAig = Abc_NtkFromDar( pNtk, pMan );
1540 Aig_ManStop( pMan );
1541 return pNtkAig;
1542 }
1543
1544 /**Function*************************************************************
1545
1546 Synopsis [Gives the current ABC network to AIG manager for processing.]
1547
1548 Description []
1549
1550 SideEffects []
1551
1552 SeeAlso []
1553
1554 ***********************************************************************/
Abc_NtkDRefactor(Abc_Ntk_t * pNtk,Dar_RefPar_t * pPars)1555 Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars )
1556 {
1557 Aig_Man_t * pMan, * pTemp;
1558 Abc_Ntk_t * pNtkAig;
1559 abctime clk;
1560 assert( Abc_NtkIsStrash(pNtk) );
1561 pMan = Abc_NtkToDar( pNtk, 0, 0 );
1562 if ( pMan == NULL )
1563 return NULL;
1564 // Aig_ManPrintStats( pMan );
1565
1566 Dar_ManRefactor( pMan, pPars );
1567 // pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
1568 // Aig_ManStop( pTemp );
1569
1570 clk = Abc_Clock();
1571 pMan = Aig_ManDupDfs( pTemp = pMan );
1572 Aig_ManStop( pTemp );
1573 //ABC_PRT( "time", Abc_Clock() - clk );
1574
1575 // Aig_ManPrintStats( pMan );
1576 pNtkAig = Abc_NtkFromDar( pNtk, pMan );
1577 Aig_ManStop( pMan );
1578 return pNtkAig;
1579 }
1580
1581 /**Function*************************************************************
1582
1583 Synopsis [Gives the current ABC network to AIG manager for processing.]
1584
1585 Description []
1586
1587 SideEffects []
1588
1589 SeeAlso []
1590
1591 ***********************************************************************/
Abc_NtkDC2(Abc_Ntk_t * pNtk,int fBalance,int fUpdateLevel,int fFanout,int fPower,int fVerbose)1592 Abc_Ntk_t * Abc_NtkDC2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose )
1593 {
1594 Aig_Man_t * pMan, * pTemp;
1595 Abc_Ntk_t * pNtkAig;
1596 abctime clk;
1597 assert( Abc_NtkIsStrash(pNtk) );
1598 pMan = Abc_NtkToDar( pNtk, 0, 0 );
1599 if ( pMan == NULL )
1600 return NULL;
1601 // Aig_ManPrintStats( pMan );
1602
1603 clk = Abc_Clock();
1604 pMan = Dar_ManCompress2( pTemp = pMan, fBalance, fUpdateLevel, fFanout, fPower, fVerbose );
1605 Aig_ManStop( pTemp );
1606 //ABC_PRT( "time", Abc_Clock() - clk );
1607
1608 // Aig_ManPrintStats( pMan );
1609 pNtkAig = Abc_NtkFromDar( pNtk, pMan );
1610 Aig_ManStop( pMan );
1611 return pNtkAig;
1612 }
1613
1614 /**Function*************************************************************
1615
1616 Synopsis [Gives the current ABC network to AIG manager for processing.]
1617
1618 Description []
1619
1620 SideEffects []
1621
1622 SeeAlso []
1623
1624 ***********************************************************************/
Abc_NtkDChoice(Abc_Ntk_t * pNtk,int fBalance,int fUpdateLevel,int fConstruct,int nConfMax,int nLevelMax,int fVerbose)1625 Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose )
1626 {
1627 Aig_Man_t * pMan, * pTemp;
1628 Abc_Ntk_t * pNtkAig;
1629 assert( Abc_NtkIsStrash(pNtk) );
1630 pMan = Abc_NtkToDar( pNtk, 0, 0 );
1631 if ( pMan == NULL )
1632 return NULL;
1633 pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose );
1634 Aig_ManStop( pTemp );
1635 pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
1636 Aig_ManStop( pMan );
1637 return pNtkAig;
1638 }
1639
1640 /**Function*************************************************************
1641
1642 Synopsis [Gives the current ABC network to AIG manager for processing.]
1643
1644 Description []
1645
1646 SideEffects []
1647
1648 SeeAlso []
1649
1650 ***********************************************************************/
Abc_NtkDch(Abc_Ntk_t * pNtk,Dch_Pars_t * pPars)1651 Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
1652 {
1653 extern Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fLightSynth, int fVerbose );
1654 extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
1655
1656 Aig_Man_t * pMan, * pTemp;
1657 Abc_Ntk_t * pNtkAig;
1658 Gia_Man_t * pGia;
1659 abctime clk;
1660 assert( Abc_NtkIsStrash(pNtk) );
1661 pMan = Abc_NtkToDar( pNtk, 0, 0 );
1662 if ( pMan == NULL )
1663 return NULL;
1664 clk = Abc_Clock();
1665 if ( pPars->fSynthesis )
1666 pGia = Dar_NewChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
1667 else
1668 {
1669 pGia = Gia_ManFromAig( pMan );
1670 Aig_ManStop( pMan );
1671 }
1672 pPars->timeSynth = Abc_Clock() - clk;
1673 if ( pPars->fUseGia )
1674 pMan = Cec_ComputeChoices( pGia, pPars );
1675 else
1676 {
1677 pMan = Gia_ManToAigSkip( pGia, 3 );
1678 Gia_ManStop( pGia );
1679 pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
1680 Aig_ManStop( pTemp );
1681 }
1682 pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
1683 Aig_ManStop( pMan );
1684 return pNtkAig;
1685 }
1686
1687 /**Function*************************************************************
1688
1689 Synopsis [Gives the current ABC network to AIG manager for processing.]
1690
1691 Description []
1692
1693 SideEffects []
1694
1695 SeeAlso []
1696
1697 ***********************************************************************/
Abc_NtkDrwsat(Abc_Ntk_t * pNtk,int fBalance,int fVerbose)1698 Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose )
1699 {
1700 Aig_Man_t * pMan, * pTemp;
1701 Abc_Ntk_t * pNtkAig;
1702 abctime clk;
1703 assert( Abc_NtkIsStrash(pNtk) );
1704 pMan = Abc_NtkToDar( pNtk, 0, 0 );
1705 if ( pMan == NULL )
1706 return NULL;
1707 // Aig_ManPrintStats( pMan );
1708
1709 clk = Abc_Clock();
1710 pMan = Dar_ManRwsat( pTemp = pMan, fBalance, fVerbose );
1711 Aig_ManStop( pTemp );
1712 //ABC_PRT( "time", Abc_Clock() - clk );
1713
1714 // Aig_ManPrintStats( pMan );
1715 pNtkAig = Abc_NtkFromDar( pNtk, pMan );
1716 Aig_ManStop( pMan );
1717 return pNtkAig;
1718 }
1719
1720 /**Function*************************************************************
1721
1722 Synopsis [Gives the current ABC network to AIG manager for processing.]
1723
1724 Description []
1725
1726 SideEffects []
1727
1728 SeeAlso []
1729
1730 ***********************************************************************/
Abc_NtkConstructFromCnf(Abc_Ntk_t * pNtk,Cnf_Man_t * p,Vec_Ptr_t * vMapped)1731 Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t * vMapped )
1732 {
1733 Abc_Ntk_t * pNtkNew;
1734 Abc_Obj_t * pNode, * pNodeNew;
1735 Aig_Obj_t * pObj, * pLeaf;
1736 Cnf_Cut_t * pCut;
1737 Vec_Int_t * vCover;
1738 unsigned uTruth;
1739 int i, k, nDupGates;
1740 // create the new network
1741 pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
1742 // make the mapper point to the new network
1743 Aig_ManConst1(p->pManAig)->pData = Abc_NtkCreateNodeConst1(pNtkNew);
1744 Abc_NtkForEachCi( pNtk, pNode, i )
1745 Aig_ManCi(p->pManAig, i)->pData = pNode->pCopy;
1746 // process the nodes in topological order
1747 vCover = Vec_IntAlloc( 1 << 16 );
1748 Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
1749 {
1750 // create new node
1751 pNodeNew = Abc_NtkCreateNode( pNtkNew );
1752 // add fanins according to the cut
1753 pCut = (Cnf_Cut_t *)pObj->pData;
1754 Cnf_CutForEachLeaf( p->pManAig, pCut, pLeaf, k )
1755 Abc_ObjAddFanin( pNodeNew, (Abc_Obj_t *)pLeaf->pData );
1756 // add logic function
1757 if ( pCut->nFanins < 5 )
1758 {
1759 uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
1760 Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vCover );
1761 pNodeNew->pData = Abc_SopCreateFromIsop( (Mem_Flex_t *)pNtkNew->pManFunc, pCut->nFanins, vCover );
1762 }
1763 else
1764 pNodeNew->pData = Abc_SopCreateFromIsop( (Mem_Flex_t *)pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] );
1765 // save the node
1766 pObj->pData = pNodeNew;
1767 }
1768 Vec_IntFree( vCover );
1769 // add the CO drivers
1770 Abc_NtkForEachCo( pNtk, pNode, i )
1771 {
1772 pObj = Aig_ManCo(p->pManAig, i);
1773 pNodeNew = Abc_ObjNotCond( (Abc_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
1774 Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
1775 }
1776
1777 // remove the constant node if not used
1778 pNodeNew = (Abc_Obj_t *)Aig_ManConst1(p->pManAig)->pData;
1779 if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
1780 Abc_NtkDeleteObj( pNodeNew );
1781 // minimize the node
1782 // Abc_NtkSweep( pNtkNew, 0 );
1783 // decouple the PO driver nodes to reduce the number of levels
1784 nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
1785 // if ( nDupGates && If_ManReadVerbose(pIfMan) )
1786 // Abc_Print( 1, "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
1787 if ( !Abc_NtkCheck( pNtkNew ) )
1788 Abc_Print( 1, "Abc_NtkConstructFromCnf(): Network check has failed.\n" );
1789 return pNtkNew;
1790 }
1791
1792 /**Function*************************************************************
1793
1794 Synopsis [Gives the current ABC network to AIG manager for processing.]
1795
1796 Description []
1797
1798 SideEffects []
1799
1800 SeeAlso []
1801
1802 ***********************************************************************/
Abc_NtkDarToCnf(Abc_Ntk_t * pNtk,char * pFileName,int fFastAlgo,int fChangePol,int fVerbose)1803 Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo, int fChangePol, int fVerbose )
1804 {
1805 // Vec_Ptr_t * vMapped = NULL;
1806 Aig_Man_t * pMan;
1807 // Cnf_Man_t * pManCnf = NULL;
1808 Cnf_Dat_t * pCnf;
1809 Abc_Ntk_t * pNtkNew = NULL;
1810 abctime clk = Abc_Clock();
1811 assert( Abc_NtkIsStrash(pNtk) );
1812
1813 // convert to the AIG manager
1814 pMan = Abc_NtkToDar( pNtk, 0, 0 );
1815 if ( pMan == NULL )
1816 return NULL;
1817 if ( !Aig_ManCheck( pMan ) )
1818 {
1819 Abc_Print( 1, "Abc_NtkDarToCnf: AIG check has failed.\n" );
1820 Aig_ManStop( pMan );
1821 return NULL;
1822 }
1823 // perform balance
1824 if ( fVerbose )
1825 Aig_ManPrintStats( pMan );
1826
1827 // derive CNF
1828 if ( fFastAlgo )
1829 pCnf = Cnf_DeriveFast( pMan, 0 );
1830 else
1831 pCnf = Cnf_Derive( pMan, 0 );
1832
1833 // adjust polarity
1834 if ( fChangePol )
1835 Cnf_DataTranformPolarity( pCnf, 0 );
1836
1837 // print stats
1838 // if ( fVerbose )
1839 {
1840 Abc_Print( 1, "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
1841 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1842 }
1843
1844 /*
1845 // write the network for verification
1846 pManCnf = Cnf_ManRead();
1847 vMapped = Cnf_ManScanMapping( pManCnf, 1, 0 );
1848 pNtkNew = Abc_NtkConstructFromCnf( pNtk, pManCnf, vMapped );
1849 Vec_PtrFree( vMapped );
1850 */
1851 // write CNF into a file
1852 Cnf_DataWriteIntoFile( pCnf, pFileName, 0, NULL, NULL );
1853 Cnf_DataFree( pCnf );
1854 Cnf_ManFree();
1855 Aig_ManStop( pMan );
1856 return pNtkNew;
1857 }
1858
1859
1860 /**Function*************************************************************
1861
1862 Synopsis [Solves combinational miter using a SAT solver.]
1863
1864 Description []
1865
1866 SideEffects []
1867
1868 SeeAlso []
1869
1870 ***********************************************************************/
Abc_NtkDSat(Abc_Ntk_t * pNtk,ABC_INT64_T nConfLimit,ABC_INT64_T nInsLimit,int nLearnedStart,int nLearnedDelta,int nLearnedPerce,int fAlignPol,int fAndOuts,int fNewSolver,int fVerbose)1871 int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose )
1872 {
1873 Aig_Man_t * pMan;
1874 int RetValue;//, clk = Abc_Clock();
1875 assert( Abc_NtkIsStrash(pNtk) );
1876 assert( Abc_NtkLatchNum(pNtk) == 0 );
1877 // assert( Abc_NtkPoNum(pNtk) == 1 );
1878 pMan = Abc_NtkToDar( pNtk, 0, 0 );
1879 RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fAlignPol, fAndOuts, fNewSolver, fVerbose );
1880 pNtk->pModel = (int *)pMan->pData, pMan->pData = NULL;
1881 Aig_ManStop( pMan );
1882 return RetValue;
1883 }
1884
1885 /**Function*************************************************************
1886
1887 Synopsis [Solves combinational miter using a SAT solver.]
1888
1889 Description []
1890
1891 SideEffects []
1892
1893 SeeAlso []
1894
1895 ***********************************************************************/
Abc_NtkPartitionedSat(Abc_Ntk_t * pNtk,int nAlgo,int nPartSize,int nConfPart,int nConfTotal,int fAlignPol,int fSynthesize,int fVerbose)1896 int Abc_NtkPartitionedSat( Abc_Ntk_t * pNtk, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose )
1897 {
1898 extern int Aig_ManPartitionedSat( Aig_Man_t * pNtk, int nAlgo, int nPartSize, int nConfPart, int nConfTotal, int fAlignPol, int fSynthesize, int fVerbose );
1899 Aig_Man_t * pMan;
1900 int RetValue;//, clk = Abc_Clock();
1901 assert( Abc_NtkIsStrash(pNtk) );
1902 assert( Abc_NtkLatchNum(pNtk) == 0 );
1903 pMan = Abc_NtkToDar( pNtk, 0, 0 );
1904 RetValue = Aig_ManPartitionedSat( pMan, nAlgo, nPartSize, nConfPart, nConfTotal, fAlignPol, fSynthesize, fVerbose );
1905 pNtk->pModel = (int *)pMan->pData, pMan->pData = NULL;
1906 Aig_ManStop( pMan );
1907 return RetValue;
1908 }
1909
1910 /**Function*************************************************************
1911
1912 Synopsis [Gives the current ABC network to AIG manager for processing.]
1913
1914 Description []
1915
1916 SideEffects []
1917
1918 SeeAlso []
1919
1920 ***********************************************************************/
Abc_NtkDarCec(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,int nConfLimit,int fPartition,int fVerbose)1921 int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPartition, int fVerbose )
1922 {
1923 Aig_Man_t * pMan, * pMan1, * pMan2;
1924 Abc_Ntk_t * pMiter;
1925 int RetValue;
1926 abctime clkTotal = Abc_Clock();
1927 /*
1928 {
1929 extern void Cec_ManVerifyTwoAigs( Aig_Man_t * pAig0, Aig_Man_t * pAig1, int fVerbose );
1930 Aig_Man_t * pAig0 = Abc_NtkToDar( pNtk1, 0, 0 );
1931 Aig_Man_t * pAig1 = Abc_NtkToDar( pNtk2, 0, 0 );
1932 Cec_ManVerifyTwoAigs( pAig0, pAig1, 1 );
1933 Aig_ManStop( pAig0 );
1934 Aig_ManStop( pAig1 );
1935 return 1;
1936 }
1937 */
1938 // cannot partition if it is already a miter
1939 if ( pNtk2 == NULL && fPartition == 1 )
1940 {
1941 Abc_Print( 1, "Abc_NtkDarCec(): Switching to non-partitioned CEC for the miter.\n" );
1942 fPartition = 0;
1943 }
1944
1945 // if partitioning is selected, call partitioned CEC
1946 if ( fPartition )
1947 {
1948 pMan1 = Abc_NtkToDar( pNtk1, 0, 0 );
1949 pMan2 = Abc_NtkToDar( pNtk2, 0, 0 );
1950 RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, 100, 1, fVerbose );
1951 Aig_ManStop( pMan1 );
1952 Aig_ManStop( pMan2 );
1953 goto finish;
1954 }
1955
1956 if ( pNtk2 != NULL )
1957 {
1958 // get the miter of the two networks
1959 pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0, 0 );
1960 if ( pMiter == NULL )
1961 {
1962 Abc_Print( 1, "Miter computation has failed.\n" );
1963 return 0;
1964 }
1965 }
1966 else
1967 {
1968 pMiter = Abc_NtkDup( pNtk1 );
1969 }
1970 RetValue = Abc_NtkMiterIsConstant( pMiter );
1971 if ( RetValue == 0 )
1972 {
1973 // extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
1974 Abc_Print( 1, "Networks are NOT EQUIVALENT after structural hashing.\n" );
1975 // report the error
1976 if ( pNtk2 == NULL )
1977 pNtk1->pModel = Abc_NtkVerifyGetCleanModel( pNtk1, 1 );
1978 // pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
1979 // Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
1980 // ABC_FREE( pMiter->pModel );
1981 Abc_NtkDelete( pMiter );
1982 return 0;
1983 }
1984 if ( RetValue == 1 )
1985 {
1986 Abc_NtkDelete( pMiter );
1987 Abc_Print( 1, "Networks are equivalent after structural hashing.\n" );
1988 return 1;
1989 }
1990
1991 // derive the AIG manager
1992 pMan = Abc_NtkToDar( pMiter, 0, 0 );
1993 Abc_NtkDelete( pMiter );
1994 if ( pMan == NULL )
1995 {
1996 Abc_Print( 1, "Converting miter into AIG has failed.\n" );
1997 return -1;
1998 }
1999 // perform verification
2000 RetValue = Fra_FraigCec( &pMan, 100000, fVerbose );
2001 // transfer model if given
2002 if ( pNtk2 == NULL )
2003 pNtk1->pModel = (int *)pMan->pData, pMan->pData = NULL;
2004 Aig_ManStop( pMan );
2005
2006 finish:
2007 // report the miter
2008 if ( RetValue == 1 )
2009 {
2010 Abc_Print( 1, "Networks are equivalent. " );
2011 ABC_PRT( "Time", Abc_Clock() - clkTotal );
2012 }
2013 else if ( RetValue == 0 )
2014 {
2015 Abc_Print( 1, "Networks are NOT EQUIVALENT. " );
2016 ABC_PRT( "Time", Abc_Clock() - clkTotal );
2017 }
2018 else
2019 {
2020 Abc_Print( 1, "Networks are UNDECIDED. " );
2021 ABC_PRT( "Time", Abc_Clock() - clkTotal );
2022 }
2023 fflush( stdout );
2024 return RetValue;
2025 }
2026
2027 /**Function*************************************************************
2028
2029 Synopsis [Gives the current ABC network to AIG manager for processing.]
2030
2031 Description []
2032
2033 SideEffects []
2034
2035 SeeAlso []
2036
2037 ***********************************************************************/
Abc_NtkDarSeqSweep(Abc_Ntk_t * pNtk,Fra_Ssw_t * pPars)2038 Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, Fra_Ssw_t * pPars )
2039 {
2040 Fraig_Params_t Params;
2041 Abc_Ntk_t * pNtkAig = NULL, * pNtkFraig;
2042 Aig_Man_t * pMan, * pTemp;
2043 abctime clk = Abc_Clock();
2044
2045 // preprocess the miter by fraiging it
2046 // (note that for each functional class, fraiging leaves one representative;
2047 // so fraiging does not reduce the number of functions represented by nodes
2048 Fraig_ParamsSetDefault( &Params );
2049 Params.nBTLimit = 100000;
2050 if ( pPars->fFraiging && pPars->nPartSize == 0 )
2051 {
2052 pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 );
2053 if ( pPars->fVerbose )
2054 {
2055 ABC_PRT( "Initial fraiging time", Abc_Clock() - clk );
2056 }
2057 }
2058 else
2059 pNtkFraig = Abc_NtkDup( pNtk );
2060
2061 pMan = Abc_NtkToDar( pNtkFraig, 0, 1 );
2062 Abc_NtkDelete( pNtkFraig );
2063 if ( pMan == NULL )
2064 return NULL;
2065
2066 // pPars->TimeLimit = 5.0;
2067 pMan = Fra_FraigInduction( pTemp = pMan, pPars );
2068 Aig_ManStop( pTemp );
2069 if ( pMan )
2070 {
2071 if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
2072 pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
2073 else
2074 {
2075 Abc_Obj_t * pObj;
2076 int i;
2077 pNtkAig = Abc_NtkFromDar( pNtk, pMan );
2078 Abc_NtkForEachLatch( pNtkAig, pObj, i )
2079 Abc_LatchSetInit0( pObj );
2080 }
2081 Aig_ManStop( pMan );
2082 }
2083 return pNtkAig;
2084 }
2085
2086 /**Function*************************************************************
2087
2088 Synopsis [Print Latch Equivalence Classes.]
2089
2090 Description []
2091
2092 SideEffects []
2093
2094 SeeAlso []
2095
2096 ***********************************************************************/
Abc_NtkPrintLatchEquivClasses(Abc_Ntk_t * pNtk,Aig_Man_t * pAig)2097 void Abc_NtkPrintLatchEquivClasses( Abc_Ntk_t * pNtk, Aig_Man_t * pAig )
2098 {
2099 int header_dumped = 0;
2100 int num_orig_latches = Abc_NtkLatchNum(pNtk);
2101 char **pNames = ABC_ALLOC( char *, num_orig_latches );
2102 int *p_irrelevant = ABC_ALLOC( int, num_orig_latches );
2103 char * pFlopName, * pReprName;
2104 Aig_Obj_t * pFlop, * pRepr;
2105 Abc_Obj_t * pNtkFlop;
2106 int repr_idx;
2107 int i;
2108
2109 Abc_NtkForEachLatch( pNtk, pNtkFlop, i )
2110 {
2111 char *temp_name = Abc_ObjName( Abc_ObjFanout0(pNtkFlop) );
2112 pNames[i] = ABC_ALLOC( char , strlen(temp_name)+1);
2113 strcpy(pNames[i], temp_name);
2114 }
2115 i = 0;
2116
2117 Aig_ManSetCioIds( pAig );
2118 Saig_ManForEachLo( pAig, pFlop, i )
2119 {
2120 p_irrelevant[i] = false;
2121
2122 pFlopName = pNames[i];
2123
2124 pRepr = Aig_ObjRepr(pAig, pFlop);
2125
2126 if ( pRepr == NULL )
2127 {
2128 // Abc_Print( 1, "Nothing equivalent to flop %s\n", pFlopName);
2129 // p_irrelevant[i] = true;
2130 continue;
2131 }
2132
2133 if (!header_dumped)
2134 {
2135 Abc_Print( 1, "Here are the flop equivalences:\n");
2136 header_dumped = true;
2137 }
2138
2139 // pRepr is representative of the equivalence class, to which pFlop belongs
2140 if ( Aig_ObjIsConst1(pRepr) )
2141 {
2142 Abc_Print( 1, "Original flop %s is proved equivalent to constant.\n", pFlopName );
2143 // Abc_Print( 1, "Original flop # %d is proved equivalent to constant.\n", i );
2144 continue;
2145 }
2146
2147 assert( Saig_ObjIsLo( pAig, pRepr ) );
2148 repr_idx = Aig_ObjCioId(pRepr) - Saig_ManPiNum(pAig);
2149 pReprName = pNames[repr_idx];
2150 Abc_Print( 1, "Original flop %s is proved equivalent to flop %s.\n", pFlopName, pReprName );
2151 // Abc_Print( 1, "Original flop # %d is proved equivalent to flop # %d.\n", i, repr_idx );
2152 }
2153
2154 header_dumped = false;
2155 for (i=0; i<num_orig_latches; ++i)
2156 {
2157 if (p_irrelevant[i])
2158 {
2159 if (!header_dumped)
2160 {
2161 Abc_Print( 1, "The following flops have been deemed irrelevant:\n");
2162 header_dumped = true;
2163 }
2164 Abc_Print( 1, "%s ", pNames[i]);
2165 }
2166
2167 ABC_FREE(pNames[i]);
2168 }
2169 if (header_dumped)
2170 Abc_Print( 1, "\n");
2171
2172 ABC_FREE(pNames);
2173 ABC_FREE(p_irrelevant);
2174 }
2175
2176 /**Function*************************************************************
2177
2178 Synopsis [Gives the current ABC network to AIG manager for processing.]
2179
2180 Description []
2181
2182 SideEffects []
2183
2184 SeeAlso []
2185
2186 ***********************************************************************/
Abc_NtkDarSeqSweep2(Abc_Ntk_t * pNtk,Ssw_Pars_t * pPars)2187 Abc_Ntk_t * Abc_NtkDarSeqSweep2( Abc_Ntk_t * pNtk, Ssw_Pars_t * pPars )
2188 {
2189 Abc_Ntk_t * pNtkAig;
2190 Aig_Man_t * pMan, * pTemp;
2191
2192 pMan = Abc_NtkToDar( pNtk, 0, 1 );
2193 if ( pMan == NULL )
2194 return NULL;
2195
2196 pMan = Ssw_SignalCorrespondence( pTemp = pMan, pPars );
2197
2198 if ( pPars->fFlopVerbose )
2199 Abc_NtkPrintLatchEquivClasses(pNtk, pTemp);
2200
2201 Aig_ManStop( pTemp );
2202 if ( pMan == NULL )
2203 return NULL;
2204
2205 if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
2206 pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
2207 else
2208 {
2209 Abc_Obj_t * pObj;
2210 int i;
2211 pNtkAig = Abc_NtkFromDar( pNtk, pMan );
2212 Abc_NtkForEachLatch( pNtkAig, pObj, i )
2213 Abc_LatchSetInit0( pObj );
2214 }
2215 Aig_ManStop( pMan );
2216 return pNtkAig;
2217 }
2218
2219 /**Function*************************************************************
2220
2221 Synopsis [Computes latch correspondence.]
2222
2223 Description []
2224
2225 SideEffects []
2226
2227 SeeAlso []
2228
2229 ***********************************************************************/
Abc_NtkDarLcorr(Abc_Ntk_t * pNtk,int nFramesP,int nConfMax,int fVerbose)2230 Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int fVerbose )
2231 {
2232 Aig_Man_t * pMan, * pTemp;
2233 Abc_Ntk_t * pNtkAig = NULL;
2234 pMan = Abc_NtkToDar( pNtk, 0, 1 );
2235 if ( pMan == NULL )
2236 return NULL;
2237 pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, 0, fVerbose, NULL, 0.0 );
2238 Aig_ManStop( pTemp );
2239 if ( pMan )
2240 {
2241 if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
2242 pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
2243 else
2244 {
2245 Abc_Obj_t * pObj;
2246 int i;
2247 pNtkAig = Abc_NtkFromDar( pNtk, pMan );
2248 Abc_NtkForEachLatch( pNtkAig, pObj, i )
2249 Abc_LatchSetInit0( pObj );
2250 }
2251 Aig_ManStop( pMan );
2252 }
2253 return pNtkAig;
2254 }
2255
2256 /**Function*************************************************************
2257
2258 Synopsis [Computes latch correspondence.]
2259
2260 Description []
2261
2262 SideEffects []
2263
2264 SeeAlso []
2265
2266 ***********************************************************************/
Abc_NtkDarLcorrNew(Abc_Ntk_t * pNtk,int nVarsMax,int nConfMax,int fVerbose)2267 Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, int fVerbose )
2268 {
2269 Ssw_Pars_t Pars, * pPars = &Pars;
2270 Aig_Man_t * pMan, * pTemp;
2271 Abc_Ntk_t * pNtkAig = NULL;
2272 pMan = Abc_NtkToDar( pNtk, 0, 1 );
2273 if ( pMan == NULL )
2274 return NULL;
2275 Ssw_ManSetDefaultParams( pPars );
2276 pPars->fLatchCorrOpt = 1;
2277 pPars->nBTLimit = nConfMax;
2278 pPars->nSatVarMax = nVarsMax;
2279 pPars->fVerbose = fVerbose;
2280 pMan = Ssw_SignalCorrespondence( pTemp = pMan, pPars );
2281 Aig_ManStop( pTemp );
2282 if ( pMan )
2283 {
2284 if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
2285 pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
2286 else
2287 {
2288 Abc_Obj_t * pObj;
2289 int i;
2290 pNtkAig = Abc_NtkFromDar( pNtk, pMan );
2291 Abc_NtkForEachLatch( pNtkAig, pObj, i )
2292 Abc_LatchSetInit0( pObj );
2293 }
2294 Aig_ManStop( pMan );
2295 }
2296 return pNtkAig;
2297 }
2298
2299 /*
2300 #include <signal.h>
2301 #include "misc/util/utilMem.h"
2302 static void sigfunc( int signo )
2303 {
2304 if (signo == SIGINT) {
2305 Abc_Print( 1, "SIGINT received!\n");
2306 s_fInterrupt = 1;
2307 }
2308 }
2309 */
2310
2311 /**Function*************************************************************
2312
2313 Synopsis [Gives the current ABC network to AIG manager for processing.]
2314
2315 Description []
2316
2317 SideEffects []
2318
2319 SeeAlso []
2320
2321 ***********************************************************************/
Abc_NtkDarBmc(Abc_Ntk_t * pNtk,int nStart,int nFrames,int nSizeMax,int nNodeDelta,int nTimeOut,int nBTLimit,int nBTLimitAll,int fRewrite,int fNewAlgo,int fOrDecomp,int nCofFanLit,int fVerbose,int * piFrames,int fUseSatoko)2322 int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int nNodeDelta, int nTimeOut, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fOrDecomp, int nCofFanLit, int fVerbose, int * piFrames, int fUseSatoko )
2323 {
2324 Aig_Man_t * pMan;
2325 Vec_Int_t * vMap = NULL;
2326 int status, RetValue = -1;
2327 abctime clk = Abc_Clock();
2328 abctime nTimeLimit = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
2329 // derive the AIG manager
2330 if ( fOrDecomp )
2331 pMan = Abc_NtkToDarBmc( pNtk, &vMap );
2332 else
2333 pMan = Abc_NtkToDar( pNtk, 0, 1 );
2334 if ( pMan == NULL )
2335 {
2336 Abc_Print( 1, "Converting miter into AIG has failed.\n" );
2337 return RetValue;
2338 }
2339 assert( pMan->nRegs > 0 );
2340 assert( vMap == NULL || Vec_IntSize(vMap) == Saig_ManPoNum(pMan) );
2341 if ( fVerbose && vMap && Abc_NtkPoNum(pNtk) != Saig_ManPoNum(pMan) )
2342 Abc_Print( 1, "Expanded %d outputs into %d outputs using OR decomposition.\n", Abc_NtkPoNum(pNtk), Saig_ManPoNum(pMan) );
2343
2344 // perform verification
2345 if ( fNewAlgo ) // command 'bmc'
2346 {
2347 int iFrame;
2348 RetValue = Saig_ManBmcSimple( pMan, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &iFrame, nCofFanLit, fUseSatoko );
2349 if ( piFrames )
2350 *piFrames = iFrame;
2351 ABC_FREE( pNtk->pModel );
2352 ABC_FREE( pNtk->pSeqModel );
2353 pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
2354 if ( RetValue == 1 )
2355 Abc_Print( 1, "Incorrect return value. " );
2356 else if ( RetValue == -1 )
2357 {
2358 Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(iFrame+1,0) );
2359 if ( nTimeLimit && Abc_Clock() > nTimeLimit )
2360 Abc_Print( 1, "(timeout %d sec). ", nTimeLimit );
2361 else
2362 Abc_Print( 1, "(conf limit %d). ", nBTLimit );
2363 }
2364 else // if ( RetValue == 0 )
2365 {
2366 Abc_Cex_t * pCex = pNtk->pSeqModel;
2367 Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame );
2368 }
2369 ABC_PRT( "Time", Abc_Clock() - clk );
2370 }
2371 else
2372 {
2373 RetValue = Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, piFrames, 0, fUseSatoko );
2374 ABC_FREE( pNtk->pModel );
2375 ABC_FREE( pNtk->pSeqModel );
2376 pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
2377 }
2378 // verify counter-example
2379 if ( pNtk->pSeqModel )
2380 {
2381 status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel );
2382 if ( status == 0 )
2383 Abc_Print( 1, "Abc_NtkDarBmc(): Counter-example verification has FAILED.\n" );
2384 }
2385 Aig_ManStop( pMan );
2386 // update the counter-example
2387 if ( pNtk->pSeqModel && vMap )
2388 pNtk->pSeqModel->iPo = Vec_IntEntry( vMap, pNtk->pSeqModel->iPo );
2389 Vec_IntFreeP( &vMap );
2390 return RetValue;
2391 }
2392
2393 /**Function*************************************************************
2394
2395 Synopsis []
2396
2397 Description []
2398
2399 SideEffects []
2400
2401 SeeAlso []
2402
2403 ***********************************************************************/
Abc_NtkDarBmc3(Abc_Ntk_t * pNtk,Saig_ParBmc_t * pPars,int fOrDecomp)2404 int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
2405 {
2406 Aig_Man_t * pMan;
2407 Vec_Int_t * vMap = NULL;
2408 int status, RetValue = -1;
2409 abctime clk = Abc_Clock();
2410 abctime nTimeOut = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
2411 if ( fOrDecomp && !pPars->fSolveAll )
2412 pMan = Abc_NtkToDarBmc( pNtk, &vMap );
2413 else
2414 pMan = Abc_NtkToDar( pNtk, 0, 1 );
2415 if ( pMan == NULL )
2416 {
2417 Abc_Print( 1, "Converting miter into AIG has failed.\n" );
2418 return RetValue;
2419 }
2420 assert( pMan->nRegs > 0 );
2421 if ( pPars->fVerbose && vMap && Abc_NtkPoNum(pNtk) != Saig_ManPoNum(pMan) )
2422 Abc_Print( 1, "Expanded %d outputs into %d outputs using OR decomposition.\n", Abc_NtkPoNum(pNtk), Saig_ManPoNum(pMan) );
2423
2424 RetValue = Saig_ManBmcScalable( pMan, pPars );
2425 ABC_FREE( pNtk->pModel );
2426 ABC_FREE( pNtk->pSeqModel );
2427 pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
2428 if ( !pPars->fSilent )
2429 {
2430 if ( RetValue == 1 )
2431 {
2432 Abc_Print( 1, "Explored all reachable states after completing %d frames. ", 1<<Aig_ManRegNum(pMan) );
2433 }
2434 else if ( RetValue == -1 )
2435 {
2436 if ( pPars->nFailOuts == 0 )
2437 {
2438 Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(pPars->iFrame+1,0) );
2439 if ( nTimeOut && Abc_Clock() > nTimeOut )
2440 Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
2441 else
2442 Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
2443 }
2444 else
2445 {
2446 Abc_Print( 1, "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame );
2447 if ( Abc_Clock() > nTimeOut )
2448 Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
2449 else
2450 Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
2451 }
2452 }
2453 else // if ( RetValue == 0 )
2454 {
2455 if ( !pPars->fSolveAll )
2456 {
2457 Abc_Cex_t * pCex = pNtk->pSeqModel;
2458 Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame );
2459 }
2460 else
2461 {
2462 int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan);
2463 if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
2464 Abc_Print( 1, "None of the %d outputs is found to be SAT", nOutputs );
2465 else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
2466 Abc_Print( 1, "All %d outputs are found to be SAT", nOutputs );
2467 else
2468 {
2469 Abc_Print( 1, "Some outputs are SAT (%d out of %d)", nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
2470 if ( pPars->nDropOuts )
2471 Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs );
2472 }
2473 Abc_Print( 1, " after %d frames", pPars->iFrame+2 );
2474 Abc_Print( 1, ". " );
2475 }
2476 }
2477 ABC_PRT( "Time", Abc_Clock() - clk );
2478 }
2479 if ( RetValue == 0 && pPars->fSolveAll )
2480 {
2481 if ( pNtk->vSeqModelVec )
2482 Vec_PtrFreeFree( pNtk->vSeqModelVec );
2483 pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
2484 }
2485 if ( pNtk->pSeqModel )
2486 {
2487 status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel );
2488 if ( status == 0 )
2489 Abc_Print( 1, "Abc_NtkDarBmc3(): Counter-example verification has FAILED.\n" );
2490 }
2491 Aig_ManStop( pMan );
2492 // update the counter-example
2493 if ( pNtk->pSeqModel && vMap )
2494 pNtk->pSeqModel->iPo = Vec_IntEntry( vMap, pNtk->pSeqModel->iPo );
2495 Vec_IntFreeP( &vMap );
2496 return RetValue;
2497 }
2498
2499 /**Function*************************************************************
2500
2501 Synopsis [Gives the current ABC network to AIG manager for processing.]
2502
2503 Description []
2504
2505 SideEffects []
2506
2507 SeeAlso []
2508
2509 ***********************************************************************/
Abc_NtkDarBmcInter_int(Aig_Man_t * pMan,Inter_ManParams_t * pPars,Aig_Man_t ** ppNtkRes)2510 int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars, Aig_Man_t ** ppNtkRes )
2511 {
2512 int RetValue = -1, iFrame;
2513 abctime clk = Abc_Clock();
2514 int nTotalProvedSat = 0;
2515 assert( pMan->nRegs > 0 );
2516 if ( ppNtkRes )
2517 *ppNtkRes = NULL;
2518 if ( pPars->fUseSeparate )
2519 {
2520 Aig_Man_t * pTemp, * pAux;
2521 Aig_Obj_t * pObjPo;
2522 int i, Counter = 0;
2523 Saig_ManForEachPo( pMan, pObjPo, i )
2524 {
2525 if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pMan) )
2526 continue;
2527 if ( pPars->fVerbose )
2528 Abc_Print( 1, "Solving output %2d (out of %2d):\n", i, Saig_ManPoNum(pMan) );
2529 pTemp = Aig_ManDupOneOutput( pMan, i, 1 );
2530 pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0, -1, -1, 0, 0 );
2531 Aig_ManStop( pAux );
2532 if ( Aig_ManRegNum(pTemp) == 0 )
2533 {
2534 pTemp->pSeqModel = NULL;
2535 RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0, 0, 0, 0, 0 );
2536 if ( pTemp->pData )
2537 pTemp->pSeqModel = Abc_CexCreate( Aig_ManRegNum(pMan), Saig_ManPiNum(pMan), (int *)pTemp->pData, 0, i, 1 );
2538 // pNtk->pModel = pTemp->pData, pTemp->pData = NULL;
2539 }
2540 else
2541 RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &iFrame );
2542 if ( pTemp->pSeqModel )
2543 {
2544 if ( pPars->fDropSatOuts )
2545 {
2546 Abc_Print( 1, "Output %d proved SAT in frame %d (replacing by const 0 and continuing...)\n", i, pTemp->pSeqModel->iFrame );
2547 Aig_ObjPatchFanin0( pMan, pObjPo, Aig_ManConst0(pMan) );
2548 Aig_ManStop( pTemp );
2549 nTotalProvedSat++;
2550 continue;
2551 }
2552 else
2553 {
2554 Abc_Cex_t * pCex;
2555 pCex = pMan->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
2556 pCex->iPo = i;
2557 Aig_ManStop( pTemp );
2558 break;
2559 }
2560 }
2561 // if solved, remove the output
2562 if ( RetValue == 1 )
2563 {
2564 Aig_ObjPatchFanin0( pMan, pObjPo, Aig_ManConst0(pMan) );
2565 // Abc_Print( 1, "Output %3d : Solved ", i );
2566 }
2567 else
2568 {
2569 Counter++;
2570 // Abc_Print( 1, "Output %3d : Undec ", i );
2571 }
2572 // Aig_ManPrintStats( pTemp );
2573 Aig_ManStop( pTemp );
2574 Abc_Print( 1, "Solving output %3d (out of %3d) using interpolation.\r", i, Saig_ManPoNum(pMan) );
2575 }
2576 Aig_ManCleanup( pMan );
2577 if ( pMan->pSeqModel == NULL )
2578 {
2579 Abc_Print( 1, "Interpolation left %d (out of %d) outputs unsolved \n", Counter, Saig_ManPoNum(pMan) );
2580 if ( Counter )
2581 RetValue = -1;
2582 }
2583 if ( ppNtkRes )
2584 {
2585 pTemp = Aig_ManDupUnsolvedOutputs( pMan, 1 );
2586 *ppNtkRes = Aig_ManScl( pTemp, 1, 1, 0, -1, -1, 0, 0 );
2587 Aig_ManStop( pTemp );
2588 }
2589 }
2590 else
2591 {
2592 RetValue = Inter_ManPerformInterpolation( pMan, pPars, &iFrame );
2593 }
2594 if ( nTotalProvedSat )
2595 Abc_Print( 1, "The total of %d outputs proved SAT and replaced by const 0 in this run.\n", nTotalProvedSat );
2596 if ( RetValue == 1 )
2597 Abc_Print( 1, "Property proved. " );
2598 else if ( RetValue == 0 )
2599 Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pMan->pSeqModel ? pMan->pSeqModel->iPo : -1, pMan->pName, iFrame );
2600 else if ( RetValue == -1 )
2601 Abc_Print( 1, "Property UNDECIDED. " );
2602 else
2603 assert( 0 );
2604 ABC_PRT( "Time", Abc_Clock() - clk );
2605 return RetValue;
2606 }
2607
2608 /**Function*************************************************************
2609
2610 Synopsis [Gives the current ABC network to AIG manager for processing.]
2611
2612 Description []
2613
2614 SideEffects []
2615
2616 SeeAlso []
2617
2618 ***********************************************************************/
Abc_NtkDarBmcInter(Abc_Ntk_t * pNtk,Inter_ManParams_t * pPars,Abc_Ntk_t ** ppNtkRes)2619 int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars, Abc_Ntk_t ** ppNtkRes )
2620 {
2621 Aig_Man_t * pMan;
2622 int RetValue;
2623 if ( ppNtkRes )
2624 *ppNtkRes = NULL;
2625 pMan = Abc_NtkToDar( pNtk, 0, 1 );
2626 if ( pMan == NULL )
2627 {
2628 Abc_Print( 1, "Converting miter into AIG has failed.\n" );
2629 return -1;
2630 }
2631 if ( pPars->fUseSeparate && ppNtkRes )
2632 {
2633 Aig_Man_t * pManNew;
2634 RetValue = Abc_NtkDarBmcInter_int( pMan, pPars, &pManNew );
2635 *ppNtkRes = Abc_NtkFromAigPhase( pManNew );
2636 Aig_ManStop( pManNew );
2637 }
2638 else
2639 {
2640 RetValue = Abc_NtkDarBmcInter_int( pMan, pPars, NULL );
2641 }
2642 ABC_FREE( pNtk->pModel );
2643 ABC_FREE( pNtk->pSeqModel );
2644 pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
2645 Aig_ManStop( pMan );
2646 return RetValue;
2647 }
2648
2649 /**Function*************************************************************
2650
2651 Synopsis [Gives the current ABC network to AIG manager for processing.]
2652
2653 Description []
2654
2655 SideEffects []
2656
2657 SeeAlso []
2658
2659 ***********************************************************************/
Abc_NtkDarDemiter(Abc_Ntk_t * pNtk)2660 int Abc_NtkDarDemiter( Abc_Ntk_t * pNtk )
2661 {
2662 char * pFileNameGeneric, pFileName0[1000], pFileName1[1000];
2663 Aig_Man_t * pMan, * pPart0, * pPart1;//, * pMiter;
2664 // derive the AIG manager
2665 pMan = Abc_NtkToDar( pNtk, 0, 1 );
2666 if ( pMan == NULL )
2667 {
2668 Abc_Print( 1, "Converting network into AIG has failed.\n" );
2669 return 0;
2670 }
2671 // if ( !Saig_ManDemiterSimple( pMan, &pPart0, &pPart1 ) )
2672 if ( !Saig_ManDemiterSimpleDiff( pMan, &pPart0, &pPart1 ) )
2673 {
2674 Aig_ManStop( pMan );
2675 Abc_Print( 1, "Demitering has failed.\n" );
2676 return 0;
2677 }
2678 // create file names
2679 pFileNameGeneric = Extra_FileNameGeneric( pNtk->pSpec ? pNtk->pSpec : pNtk->pName );
2680 // sprintf( pFileName0, "%s%s", pFileNameGeneric, "_part0.aig" );
2681 // sprintf( pFileName1, "%s%s", pFileNameGeneric, "_part1.aig" );
2682 sprintf( pFileName0, "%s", "part0.aig" );
2683 sprintf( pFileName1, "%s", "part1.aig" );
2684 ABC_FREE( pFileNameGeneric );
2685 // dump files
2686 Ioa_WriteAiger( pPart0, pFileName0, 0, 0 );
2687 Ioa_WriteAiger( pPart1, pFileName1, 0, 0 );
2688 Abc_Print( 1, "Demitering produced two files \"%s\" and \"%s\".\n", pFileName0, pFileName1 );
2689 // create two-level miter
2690 // pMiter = Saig_ManCreateMiterTwo( pPart0, pPart1, 2 );
2691 // Aig_ManDumpBlif( pMiter, "miter01.blif", NULL, NULL );
2692 // Aig_ManStop( pMiter );
2693 // Abc_Print( 1, "The new miter is written into file \"%s\".\n", "miter01.blif" );
2694 Aig_ManStop( pPart0 );
2695 Aig_ManStop( pPart1 );
2696 Aig_ManStop( pMan );
2697 return 1;
2698 }
2699
2700 /**Function*************************************************************
2701
2702 Synopsis [Gives the current ABC network to AIG manager for processing.]
2703
2704 Description []
2705
2706 SideEffects []
2707
2708 SeeAlso []
2709
2710 ***********************************************************************/
Abc_NtkDarDemiterNew(Abc_Ntk_t * pNtk)2711 int Abc_NtkDarDemiterNew( Abc_Ntk_t * pNtk )
2712 {
2713 char * pFileNameGeneric, pFileName0[1000], pFileName1[1000];
2714 Aig_Man_t * pMan, * pPart0, * pPart1;//, * pMiter;
2715 // derive the AIG manager
2716 pMan = Abc_NtkToDar( pNtk, 0, 1 );
2717 if ( pMan == NULL )
2718 {
2719 Abc_Print( 1, "Converting network into AIG has failed.\n" );
2720 return 0;
2721 }
2722
2723 Saig_ManDemiterNew( pMan );
2724 Aig_ManStop( pMan );
2725 return 1;
2726
2727 // if ( !Saig_ManDemiterSimple( pMan, &pPart0, &pPart1 ) )
2728 if ( !Saig_ManDemiterSimpleDiff( pMan, &pPart0, &pPart1 ) )
2729 {
2730 Abc_Print( 1, "Demitering has failed.\n" );
2731 return 0;
2732 }
2733 // create file names
2734 pFileNameGeneric = Extra_FileNameGeneric( pNtk->pSpec );
2735 sprintf( pFileName0, "%s%s", pFileNameGeneric, "_part0.aig" );
2736 sprintf( pFileName1, "%s%s", pFileNameGeneric, "_part1.aig" );
2737 ABC_FREE( pFileNameGeneric );
2738 // dump files
2739 Ioa_WriteAiger( pPart0, pFileName0, 0, 0 );
2740 Ioa_WriteAiger( pPart1, pFileName1, 0, 0 );
2741 Abc_Print( 1, "Demitering produced two files \"%s\" and \"%s\".\n", pFileName0, pFileName1 );
2742 // create two-level miter
2743 // pMiter = Saig_ManCreateMiterTwo( pPart0, pPart1, 2 );
2744 // Aig_ManDumpBlif( pMiter, "miter01.blif", NULL, NULL );
2745 // Aig_ManStop( pMiter );
2746 // Abc_Print( 1, "The new miter is written into file \"%s\".\n", "miter01.blif" );
2747 Aig_ManStop( pPart0 );
2748 Aig_ManStop( pPart1 );
2749 Aig_ManStop( pMan );
2750 return 1;
2751 }
2752
2753 /**Function*************************************************************
2754
2755 Synopsis [Gives the current ABC network to AIG manager for processing.]
2756
2757 Description []
2758
2759 SideEffects []
2760
2761 SeeAlso []
2762
2763 ***********************************************************************/
Abc_NtkDarDemiterDual(Abc_Ntk_t * pNtk,int fVerbose)2764 int Abc_NtkDarDemiterDual( Abc_Ntk_t * pNtk, int fVerbose )
2765 {
2766 char * pFileNameGeneric, pFileName0[1000], pFileName1[1000];
2767 Aig_Man_t * pMan, * pPart0, * pPart1;//, * pMiter;
2768 if ( (Abc_NtkPoNum(pNtk) & 1) )
2769 {
2770 Abc_Print( 1, "The number of POs should be even.\n" );
2771 return 0;
2772 }
2773 // derive the AIG manager
2774 pMan = Abc_NtkToDar( pNtk, 0, 1 );
2775 if ( pMan == NULL )
2776 {
2777 Abc_Print( 1, "Converting network into AIG has failed.\n" );
2778 return 0;
2779 }
2780 // if ( !Saig_ManDemiterSimple( pMan, &pPart0, &pPart1 ) )
2781 if ( !Saig_ManDemiterDual( pMan, &pPart0, &pPart1 ) )
2782 {
2783 Abc_Print( 1, "Demitering has failed.\n" );
2784 return 0;
2785 }
2786 // create new AIG
2787 ABC_FREE( pPart0->pName );
2788 pPart0->pName = Abc_UtilStrsav( "part0" );
2789 // create new AIGs
2790 ABC_FREE( pPart1->pName );
2791 pPart1->pName = Abc_UtilStrsav( "part1" );
2792 // create file names
2793 pFileNameGeneric = Extra_FileNameGeneric( pNtk->pSpec );
2794 // sprintf( pFileName0, "%s%s", pFileNameGeneric, "_part0.aig" );
2795 // sprintf( pFileName1, "%s%s", pFileNameGeneric, "_part1.aig" );
2796 sprintf( pFileName0, "%s", "part0.aig" );
2797 sprintf( pFileName1, "%s", "part1.aig" );
2798 ABC_FREE( pFileNameGeneric );
2799 Ioa_WriteAiger( pPart0, pFileName0, 0, 0 );
2800 Ioa_WriteAiger( pPart1, pFileName1, 0, 0 );
2801 Abc_Print( 1, "Demitering produced two files \"%s\" and \"%s\".\n", pFileName0, pFileName1 );
2802 // dump files
2803 if ( fVerbose )
2804 {
2805 // Abc_Print( 1, "Init: " );
2806 Aig_ManPrintStats( pMan );
2807 // Abc_Print( 1, "Part1: " );
2808 Aig_ManPrintStats( pPart0 );
2809 // Abc_Print( 1, "Part2: " );
2810 Aig_ManPrintStats( pPart1 );
2811 }
2812 // create two-level miter
2813 // pMiter = Saig_ManCreateMiterTwo( pPart0, pPart1, 2 );
2814 // Aig_ManDumpBlif( pMiter, "miter01.blif", NULL, NULL );
2815 // Aig_ManStop( pMiter );
2816 // Abc_Print( 1, "The new miter is written into file \"%s\".\n", "miter01.blif" );
2817 Aig_ManStop( pPart0 );
2818 Aig_ManStop( pPart1 );
2819 Aig_ManStop( pMan );
2820 return 1;
2821 }
2822
2823 /**Function*************************************************************
2824
2825 Synopsis [Gives the current ABC network to AIG manager for processing.]
2826
2827 Description []
2828
2829 SideEffects []
2830
2831 SeeAlso []
2832
2833 ***********************************************************************/
Abc_NtkDarProve(Abc_Ntk_t * pNtk,Fra_Sec_t * pSecPar,int nBmcFramesMax,int nBmcConfMax)2834 int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar, int nBmcFramesMax, int nBmcConfMax )
2835 {
2836 Aig_Man_t * pMan;
2837 int iFrame = -1, RetValue = -1;
2838 abctime clkTotal = Abc_Clock();
2839 if ( pSecPar->fTryComb || Abc_NtkLatchNum(pNtk) == 0 )
2840 {
2841 Prove_Params_t Params, * pParams = &Params;
2842 Abc_Ntk_t * pNtkComb;
2843 int RetValue;
2844 if ( Abc_NtkLatchNum(pNtk) == 0 )
2845 Abc_Print( 1, "The network has no latches. Running CEC.\n" );
2846 // create combinational network
2847 pNtkComb = Abc_NtkDup( pNtk );
2848 Abc_NtkMakeComb( pNtkComb, 1 );
2849 // solve it using combinational equivalence checking
2850 Prove_ParamsSetDefault( pParams );
2851 pParams->fVerbose = 1;
2852 RetValue = Abc_NtkIvyProve( &pNtkComb, pParams );
2853 // transfer model if given
2854 // pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
2855 if ( RetValue == 0 && (Abc_NtkLatchNum(pNtk) == 0) )
2856 {
2857 pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
2858 if ( pSecPar->fReportSolution )
2859 Abc_Print( 1, "SOLUTION: FAIL " );
2860 else
2861 Abc_Print( 1, "SATISFIABLE " );
2862 ABC_PRT( "Time", Abc_Clock() - clkTotal );
2863 return RetValue;
2864 }
2865 Abc_NtkDelete( pNtkComb );
2866 // return the result, if solved
2867 if ( RetValue == 1 )
2868 {
2869 if ( pSecPar->fReportSolution )
2870 Abc_Print( 1, "SOLUTION: PASS " );
2871 else
2872 Abc_Print( 1, "UNSATISFIABLE " );
2873 ABC_PRT( "Time", Abc_Clock() - clkTotal );
2874 return RetValue;
2875 }
2876 // return undecided, if the miter is combinational
2877 if ( Abc_NtkLatchNum(pNtk) == 0 )
2878 {
2879 Abc_Print( 1, "UNDECIDED " );
2880 ABC_PRT( "Time", Abc_Clock() - clkTotal );
2881 return RetValue;
2882 }
2883 }
2884 // derive the AIG manager
2885 pMan = Abc_NtkToDar( pNtk, 0, 1 );
2886 if ( pMan == NULL )
2887 {
2888 Abc_Print( 1, "Converting miter into AIG has failed.\n" );
2889 return -1;
2890 }
2891 assert( pMan->nRegs > 0 );
2892
2893 if ( pSecPar->fTryBmc )
2894 {
2895 RetValue = Saig_BmcPerform( pMan, 0, nBmcFramesMax, 2000, 0, nBmcConfMax, 0, pSecPar->fVerbose, 0, &iFrame, 0, 0 );
2896 if ( RetValue == 0 )
2897 {
2898 Abc_Print( 1, "Networks are not equivalent.\n" );
2899 if ( pSecPar->fReportSolution )
2900 {
2901 Abc_Print( 1, "SOLUTION: FAIL " );
2902 ABC_PRT( "Time", Abc_Clock() - clkTotal );
2903 }
2904 // return the counter-example generated
2905 ABC_FREE( pNtk->pModel );
2906 ABC_FREE( pNtk->pSeqModel );
2907 pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
2908 Aig_ManStop( pMan );
2909 return RetValue;
2910 }
2911 }
2912 // perform verification
2913 if ( pSecPar->fUseNewProver )
2914 {
2915 RetValue = Ssw_SecGeneralMiter( pMan, NULL );
2916 }
2917 else
2918 {
2919 RetValue = Fra_FraigSec( pMan, pSecPar, NULL );
2920 ABC_FREE( pNtk->pModel );
2921 ABC_FREE( pNtk->pSeqModel );
2922 pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
2923 if ( pNtk->pSeqModel )
2924 {
2925 Abc_Cex_t * pCex = pNtk->pSeqModel;
2926 Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.\n", pCex->iPo, pNtk->pName, pCex->iFrame );
2927 if ( !Saig_ManVerifyCex( pMan, pNtk->pSeqModel ) )
2928 Abc_Print( 1, "Abc_NtkDarProve(): Counter-example verification has FAILED.\n" );
2929 }
2930 }
2931 Aig_ManStop( pMan );
2932 return RetValue;
2933 }
2934
2935 /**Function*************************************************************
2936
2937 Synopsis [Gives the current ABC network to AIG manager for processing.]
2938
2939 Description []
2940
2941 SideEffects []
2942
2943 SeeAlso []
2944
2945 ***********************************************************************/
Abc_NtkDarSec(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,Fra_Sec_t * pSecPar)2946 int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar )
2947 {
2948 // Fraig_Params_t Params;
2949 Aig_Man_t * pMan;
2950 Abc_Ntk_t * pMiter;//, * pTemp;
2951 int RetValue;
2952
2953 // get the miter of the two networks
2954 pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0, 0 );
2955 if ( pMiter == NULL )
2956 {
2957 Abc_Print( 1, "Miter computation has failed.\n" );
2958 return -1;
2959 }
2960 RetValue = Abc_NtkMiterIsConstant( pMiter );
2961 if ( RetValue == 0 )
2962 {
2963 extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
2964 Abc_Print( 1, "Networks are NOT EQUIVALENT after structural hashing.\n" );
2965 // report the error
2966 pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, pSecPar->nFramesMax );
2967 // Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, pSecPar->nFramesMax );
2968 ABC_FREE( pMiter->pModel );
2969 Abc_NtkDelete( pMiter );
2970 return 0;
2971 }
2972 if ( RetValue == 1 )
2973 {
2974 Abc_NtkDelete( pMiter );
2975 Abc_Print( 1, "Networks are equivalent after structural hashing.\n" );
2976 return 1;
2977 }
2978
2979 // commented out because sometimes the problem became non-inductive
2980 /*
2981 // preprocess the miter by fraiging it
2982 // (note that for each functional class, fraiging leaves one representative;
2983 // so fraiging does not reduce the number of functions represented by nodes
2984 Fraig_ParamsSetDefault( &Params );
2985 Params.nBTLimit = 100000;
2986 pMiter = Abc_NtkFraig( pTemp = pMiter, &Params, 0, 0 );
2987 Abc_NtkDelete( pTemp );
2988 RetValue = Abc_NtkMiterIsConstant( pMiter );
2989 if ( RetValue == 0 )
2990 {
2991 extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
2992 Abc_Print( 1, "Networks are NOT EQUIVALENT after structural hashing.\n" );
2993 // report the error
2994 pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
2995 Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
2996 ABC_FREE( pMiter->pModel );
2997 Abc_NtkDelete( pMiter );
2998 return 0;
2999 }
3000 if ( RetValue == 1 )
3001 {
3002 Abc_NtkDelete( pMiter );
3003 Abc_Print( 1, "Networks are equivalent after structural hashing.\n" );
3004 return 1;
3005 }
3006 */
3007 // derive the AIG manager
3008 pMan = Abc_NtkToDar( pMiter, 0, 1 );
3009 Abc_NtkDelete( pMiter );
3010 if ( pMan == NULL )
3011 {
3012 Abc_Print( 1, "Converting miter into AIG has failed.\n" );
3013 return -1;
3014 }
3015 assert( pMan->nRegs > 0 );
3016
3017 // perform verification
3018 RetValue = Fra_FraigSec( pMan, pSecPar, NULL );
3019 Aig_ManStop( pMan );
3020 return RetValue;
3021 }
3022
3023 /**Function*************************************************************
3024
3025 Synopsis [Gives the current ABC network to AIG manager for processing.]
3026
3027 Description []
3028
3029 SideEffects []
3030
3031 SeeAlso []
3032
3033 ***********************************************************************/
Abc_NtkDarPdr(Abc_Ntk_t * pNtk,Pdr_Par_t * pPars)3034 int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
3035 {
3036 int RetValue = -1;
3037 abctime clk = Abc_Clock();
3038 Aig_Man_t * pMan;
3039 pMan = Abc_NtkToDar( pNtk, 0, 1 );
3040 if ( pMan == NULL )
3041 {
3042 Abc_Print( 1, "Converting network into AIG has failed.\n" );
3043 return -1;
3044 }
3045 RetValue = Pdr_ManSolve( pMan, pPars );
3046 pPars->nDropOuts = Saig_ManPoNum(pMan) - pPars->nProveOuts - pPars->nFailOuts;
3047 if ( !pPars->fSilent )
3048 {
3049 if ( pPars->fSolveAll )
3050 Abc_Print( 1, "Properties: All = %d. Proved = %d. Disproved = %d. Undecided = %d. ",
3051 Saig_ManPoNum(pMan), pPars->nProveOuts, pPars->nFailOuts, pPars->nDropOuts );
3052 else if ( RetValue == 1 )
3053 Abc_Print( 1, "Property proved. " );
3054 else
3055 {
3056 if ( RetValue == 0 )
3057 {
3058 if ( pMan->pSeqModel == NULL )
3059 Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example is not available.\n" );
3060 else
3061 {
3062 Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pMan->pSeqModel->iPo, pNtk->pName, pMan->pSeqModel->iFrame );
3063 if ( !Saig_ManVerifyCex( pMan, pMan->pSeqModel ) )
3064 Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" );
3065 }
3066 }
3067 else if ( RetValue == -1 )
3068 Abc_Print( 1, "Property UNDECIDED. " );
3069 else
3070 assert( 0 );
3071 }
3072 ABC_PRT( "Time", Abc_Clock() - clk );
3073 /*
3074 Abc_Print( 1, "Status: " );
3075 if ( pPars->pOutMap )
3076 {
3077 int i;
3078 for ( i = 0; i < Saig_ManPoNum(pMan); i++ )
3079 if ( pPars->pOutMap[i] == 1 )
3080 Abc_Print( 1, "%d=%s ", i, "unsat" );
3081 else if ( pPars->pOutMap[i] == 0 )
3082 Abc_Print( 1, "%d=%s ", i, "sat" );
3083 else if ( pPars->pOutMap[i] < 0 )
3084 Abc_Print( 1, "%d=%s ", i, "undec" );
3085 else assert( 0 );
3086 }
3087 Abc_Print( 1, "\n" );
3088 */
3089 }
3090 ABC_FREE( pNtk->pSeqModel );
3091 pNtk->pSeqModel = pMan->pSeqModel;
3092 pMan->pSeqModel = NULL;
3093 if ( pNtk->vSeqModelVec )
3094 Vec_PtrFreeFree( pNtk->vSeqModelVec );
3095 pNtk->vSeqModelVec = pMan->vSeqModelVec;
3096 pMan->vSeqModelVec = NULL;
3097 Aig_ManStop( pMan );
3098 return RetValue;
3099 }
3100
3101 /**Function*************************************************************
3102
3103 Synopsis [Performs BDD-based reachability analysis.]
3104
3105 Description []
3106
3107 SideEffects []
3108
3109 SeeAlso []
3110
3111 ***********************************************************************/
Abc_NtkDarAbSec(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,int nFrames,int fVerbose)3112 int Abc_NtkDarAbSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose )
3113 {
3114 Aig_Man_t * pMan1, * pMan2 = NULL;
3115 int RetValue;
3116 // derive AIG manager
3117 pMan1 = Abc_NtkToDar( pNtk1, 0, 1 );
3118 if ( pMan1 == NULL )
3119 {
3120 Abc_Print( 1, "Converting miter into AIG has failed.\n" );
3121 return -1;
3122 }
3123 assert( Aig_ManRegNum(pMan1) > 0 );
3124 // derive AIG manager
3125 if ( pNtk2 )
3126 {
3127 pMan2 = Abc_NtkToDar( pNtk2, 0, 1 );
3128 if ( pMan2 == NULL )
3129 {
3130 Aig_ManStop( pMan1 );
3131 Abc_Print( 1, "Converting miter into AIG has failed.\n" );
3132 return -1;
3133 }
3134 assert( Aig_ManRegNum(pMan2) > 0 );
3135 if ( Saig_ManPiNum(pMan1) != Saig_ManPiNum(pMan2) )
3136 {
3137 Aig_ManStop( pMan1 );
3138 Aig_ManStop( pMan2 );
3139 Abc_Print( 1, "The networks have different number of PIs.\n" );
3140 return -1;
3141 }
3142 if ( Saig_ManPoNum(pMan1) != Saig_ManPoNum(pMan2) )
3143 {
3144 Aig_ManStop( pMan1 );
3145 Aig_ManStop( pMan2 );
3146 Abc_Print( 1, "The networks have different number of POs.\n" );
3147 return -1;
3148 }
3149 if ( Aig_ManRegNum(pMan1) != Aig_ManRegNum(pMan2) )
3150 {
3151 Aig_ManStop( pMan1 );
3152 Aig_ManStop( pMan2 );
3153 Abc_Print( 1, "The networks have different number of flops.\n" );
3154 return -1;
3155 }
3156 }
3157 // perform verification
3158 RetValue = Ssw_SecSpecialMiter( pMan1, pMan2, nFrames, fVerbose );
3159 Aig_ManStop( pMan1 );
3160 if ( pMan2 )
3161 Aig_ManStop( pMan2 );
3162 return RetValue;
3163 }
3164
3165
3166 /**Function*************************************************************
3167
3168 Synopsis [Gives the current ABC network to AIG manager for processing.]
3169
3170 Description []
3171
3172 SideEffects []
3173
3174 SeeAlso []
3175
3176 ***********************************************************************/
Abc_NtkDarSimSec(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,Ssw_Pars_t * pPars)3177 int Abc_NtkDarSimSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Ssw_Pars_t * pPars )
3178 {
3179 Aig_Man_t * pMan1, * pMan2 = NULL;
3180 int RetValue;
3181 // derive AIG manager
3182 pMan1 = Abc_NtkToDar( pNtk1, 0, 1 );
3183 if ( pMan1 == NULL )
3184 {
3185 Abc_Print( 1, "Converting miter into AIG has failed.\n" );
3186 return -1;
3187 }
3188 assert( Aig_ManRegNum(pMan1) > 0 );
3189 // derive AIG manager
3190 if ( pNtk2 )
3191 {
3192 pMan2 = Abc_NtkToDar( pNtk2, 0, 1 );
3193 if ( pMan2 == NULL )
3194 {
3195 Abc_Print( 1, "Converting miter into AIG has failed.\n" );
3196 return -1;
3197 }
3198 assert( Aig_ManRegNum(pMan2) > 0 );
3199 }
3200
3201 // perform verification
3202 RetValue = Ssw_SecWithSimilarity( pMan1, pMan2, pPars );
3203 Aig_ManStop( pMan1 );
3204 if ( pMan2 )
3205 Aig_ManStop( pMan2 );
3206 return RetValue;
3207 }
3208
3209 /**Function*************************************************************
3210
3211 Synopsis []
3212
3213 Description []
3214
3215 SideEffects []
3216
3217 SeeAlso []
3218
3219 ***********************************************************************/
Abc_NtkDarMatch(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,int nDist,int fVerbose)3220 Abc_Ntk_t * Abc_NtkDarMatch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nDist, int fVerbose )
3221 {
3222 extern Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose, Aig_Man_t ** ppMiter );
3223 Abc_Ntk_t * pNtkAig;
3224 Aig_Man_t * pMan1, * pMan2 = NULL, * pManRes;
3225 Vec_Int_t * vPairs;
3226 assert( Abc_NtkIsStrash(pNtk1) );
3227 // derive AIG manager
3228 pMan1 = Abc_NtkToDar( pNtk1, 0, 1 );
3229 if ( pMan1 == NULL )
3230 {
3231 Abc_Print( 1, "Converting miter into AIG has failed.\n" );
3232 return NULL;
3233 }
3234 assert( Aig_ManRegNum(pMan1) > 0 );
3235 // derive AIG manager
3236 if ( pNtk2 )
3237 {
3238 pMan2 = Abc_NtkToDar( pNtk2, 0, 1 );
3239 if ( pMan2 == NULL )
3240 {
3241 Abc_Print( 1, "Converting miter into AIG has failed.\n" );
3242 return NULL;
3243 }
3244 assert( Aig_ManRegNum(pMan2) > 0 );
3245 }
3246
3247 // perform verification
3248 vPairs = Saig_StrSimPerformMatching( pMan1, pMan2, nDist, 1, &pManRes );
3249 pNtkAig = Abc_NtkFromAigPhase( pManRes );
3250 if ( vPairs )
3251 Vec_IntFree( vPairs );
3252 if ( pManRes )
3253 Aig_ManStop( pManRes );
3254 Aig_ManStop( pMan1 );
3255 if ( pMan2 )
3256 Aig_ManStop( pMan2 );
3257 return pNtkAig;
3258 }
3259
3260
3261 /**Function*************************************************************
3262
3263 Synopsis [Gives the current ABC network to AIG manager for processing.]
3264
3265 Description []
3266
3267 SideEffects []
3268
3269 SeeAlso []
3270
3271 ***********************************************************************/
Abc_NtkDarLatchSweep(Abc_Ntk_t * pNtk,int fLatchConst,int fLatchEqual,int fSaveNames,int fUseMvSweep,int nFramesSymb,int nFramesSatur,int fVerbose,int fVeryVerbose)3272 Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fSaveNames, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose )
3273 {
3274 extern void Aig_ManPrintControlFanouts( Aig_Man_t * p );
3275 Abc_Ntk_t * pNtkAig;
3276 Aig_Man_t * pMan, * pTemp;
3277 pMan = Abc_NtkToDar( pNtk, 0, 1 );
3278 if ( pMan == NULL )
3279 return NULL;
3280 if ( fSaveNames )
3281 {
3282 Aig_ManSeqCleanup( pMan );
3283 if ( fLatchConst && pMan->nRegs )
3284 pMan = Aig_ManConstReduce( pMan, fUseMvSweep, nFramesSymb, nFramesSatur, fVerbose, fVeryVerbose );
3285 if ( fLatchEqual && pMan->nRegs )
3286 pMan = Aig_ManReduceLaches( pMan, fVerbose );
3287 }
3288 else
3289 {
3290 if ( pMan->vFlopNums )
3291 Vec_IntFree( pMan->vFlopNums );
3292 pMan->vFlopNums = NULL;
3293 pMan = Aig_ManScl( pTemp = pMan, fLatchConst, fLatchEqual, fUseMvSweep, nFramesSymb, nFramesSatur, fVerbose, fVeryVerbose );
3294 Aig_ManStop( pTemp );
3295 }
3296
3297 pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
3298 //Aig_ManPrintControlFanouts( pMan );
3299 Aig_ManStop( pMan );
3300 return pNtkAig;
3301 }
3302
3303 /**Function*************************************************************
3304
3305 Synopsis [Gives the current ABC network to AIG manager for processing.]
3306
3307 Description []
3308
3309 SideEffects []
3310
3311 SeeAlso []
3312
3313 ***********************************************************************/
Abc_NtkDarRetime(Abc_Ntk_t * pNtk,int nStepsMax,int fVerbose)3314 Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
3315 {
3316 Abc_Ntk_t * pNtkAig;
3317 Aig_Man_t * pMan, * pTemp;
3318 pMan = Abc_NtkToDar( pNtk, 0, 1 );
3319 if ( pMan == NULL )
3320 return NULL;
3321 // Aig_ManReduceLachesCount( pMan );
3322 if ( pMan->vFlopNums )
3323 Vec_IntFree( pMan->vFlopNums );
3324 pMan->vFlopNums = NULL;
3325
3326 pMan = Rtm_ManRetime( pTemp = pMan, 1, nStepsMax, fVerbose );
3327 Aig_ManStop( pTemp );
3328
3329 // pMan = Aig_ManReduceLaches( pMan, 1 );
3330 // pMan = Aig_ManConstReduce( pMan, 1, 0 );
3331
3332 pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
3333 Aig_ManStop( pMan );
3334 return pNtkAig;
3335 }
3336
3337 /**Function*************************************************************
3338
3339 Synopsis [Gives the current ABC network to AIG manager for processing.]
3340
3341 Description []
3342
3343 SideEffects []
3344
3345 SeeAlso []
3346
3347 ***********************************************************************/
Abc_NtkDarRetimeF(Abc_Ntk_t * pNtk,int nStepsMax,int fVerbose)3348 Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
3349 {
3350 Abc_Ntk_t * pNtkAig;
3351 Aig_Man_t * pMan, * pTemp;
3352 pMan = Abc_NtkToDar( pNtk, 0, 1 );
3353 if ( pMan == NULL )
3354 return NULL;
3355 // Aig_ManReduceLachesCount( pMan );
3356 if ( pMan->vFlopNums )
3357 Vec_IntFree( pMan->vFlopNums );
3358 pMan->vFlopNums = NULL;
3359
3360 pMan = Aig_ManRetimeFrontier( pTemp = pMan, nStepsMax );
3361 Aig_ManStop( pTemp );
3362
3363 // pMan = Aig_ManReduceLaches( pMan, 1 );
3364 // pMan = Aig_ManConstReduce( pMan, 1, 0 );
3365
3366 pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
3367 Aig_ManStop( pMan );
3368 return pNtkAig;
3369 }
3370
3371 /**Function*************************************************************
3372
3373 Synopsis [Gives the current ABC network to AIG manager for processing.]
3374
3375 Description []
3376
3377 SideEffects []
3378
3379 SeeAlso []
3380
3381 ***********************************************************************/
Abc_NtkDarRetimeMostFwd(Abc_Ntk_t * pNtk,int nMaxIters,int fVerbose)3382 Abc_Ntk_t * Abc_NtkDarRetimeMostFwd( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose )
3383 {
3384 extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nIters, int fVerbose );
3385
3386 Abc_Ntk_t * pNtkAig;
3387 Aig_Man_t * pMan, * pTemp;
3388 pMan = Abc_NtkToDar( pNtk, 0, 1 );
3389 if ( pMan == NULL )
3390 return NULL;
3391 // Aig_ManReduceLachesCount( pMan );
3392 if ( pMan->vFlopNums )
3393 Vec_IntFree( pMan->vFlopNums );
3394 pMan->vFlopNums = NULL;
3395
3396 pMan = Saig_ManRetimeForward( pTemp = pMan, nMaxIters, fVerbose );
3397 Aig_ManStop( pTemp );
3398
3399 // pMan = Aig_ManReduceLaches( pMan, 1 );
3400 // pMan = Aig_ManConstReduce( pMan, 1, 0 );
3401
3402 pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
3403 Aig_ManStop( pMan );
3404 return pNtkAig;
3405 }
3406
3407 /**Function*************************************************************
3408
3409 Synopsis [Gives the current ABC network to AIG manager for processing.]
3410
3411 Description []
3412
3413 SideEffects []
3414
3415 SeeAlso []
3416
3417 ***********************************************************************/
Abc_NtkDarRetimeMinArea(Abc_Ntk_t * pNtk,int nMaxIters,int fForwardOnly,int fBackwardOnly,int fInitial,int fVerbose)3418 Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
3419 {
3420 extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
3421 Abc_Ntk_t * pNtkAig;
3422 Aig_Man_t * pMan, * pTemp;
3423 pMan = Abc_NtkToDar( pNtk, 0, 1 );
3424 if ( pMan == NULL )
3425 return NULL;
3426 if ( pMan->vFlopNums )
3427 Vec_IntFree( pMan->vFlopNums );
3428 pMan->vFlopNums = NULL;
3429
3430 pMan = Saig_ManRetimeMinArea( pTemp = pMan, nMaxIters, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
3431 Aig_ManStop( pTemp );
3432
3433 pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
3434 Aig_ManStop( pMan );
3435 return pNtkAig;
3436 }
3437
3438 /**Function*************************************************************
3439
3440 Synopsis [Gives the current ABC network to AIG manager for processing.]
3441
3442 Description []
3443
3444 SideEffects []
3445
3446 SeeAlso []
3447
3448 ***********************************************************************/
Abc_NtkDarRetimeStep(Abc_Ntk_t * pNtk,int fVerbose)3449 Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose )
3450 {
3451 Abc_Ntk_t * pNtkAig;
3452 Aig_Man_t * pMan;
3453 assert( Abc_NtkIsStrash(pNtk) );
3454 pMan = Abc_NtkToDar( pNtk, 0, 1 );
3455 if ( pMan == NULL )
3456 return NULL;
3457 if ( pMan->vFlopNums )
3458 Vec_IntFree( pMan->vFlopNums );
3459 pMan->vFlopNums = NULL;
3460
3461 Aig_ManPrintStats(pMan);
3462 Saig_ManRetimeSteps( pMan, 1000, 1, 0 );
3463 Aig_ManPrintStats(pMan);
3464
3465 pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
3466 Aig_ManStop( pMan );
3467 return pNtkAig;
3468 }
3469
3470 /**Function*************************************************************
3471
3472 Synopsis [Gives the current ABC network to AIG manager for processing.]
3473
3474 Description []
3475
3476 SideEffects []
3477
3478 SeeAlso []
3479
3480 ***********************************************************************/
3481 /*
3482 Abc_Ntk_t * Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose )
3483 {
3484 Abc_Ntk_t * pNtkAig;
3485 Aig_Man_t * pMan, * pTemp;
3486 pMan = Abc_NtkToDar( pNtk, 0, 1 );
3487 if ( pMan == NULL )
3488 return NULL;
3489 if ( pMan->vFlopNums )
3490 Vec_IntFree( pMan->vFlopNums );
3491 pMan->vFlopNums = NULL;
3492
3493 pMan = Saig_ManHaigRecord( pTemp = pMan, nIters, nSteps, fRetimingOnly, fAddBugs, fUseCnf, fVerbose );
3494 Aig_ManStop( pTemp );
3495
3496 pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
3497 Aig_ManStop( pMan );
3498 return pNtkAig;
3499 }
3500 */
3501
3502 /**Function*************************************************************
3503
3504 Synopsis [Performs random simulation.]
3505
3506 Description []
3507
3508 SideEffects []
3509
3510 SeeAlso []
3511
3512 ***********************************************************************/
Abc_NtkDarSeqSim(Abc_Ntk_t * pNtk,int nFrames,int nWords,int TimeOut,int fNew,int fMiter,int fVerbose,char * pFileSim)3513 int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, int fNew, int fMiter, int fVerbose, char * pFileSim )
3514 {
3515 Aig_Man_t * pMan;
3516 Abc_Cex_t * pCex;
3517 int status, RetValue = -1;
3518 abctime clk = Abc_Clock();
3519 if ( Abc_NtkGetChoiceNum(pNtk) )
3520 {
3521 Abc_Print( 1, "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pNtk) );
3522 Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
3523 }
3524 pMan = Abc_NtkToDar( pNtk, 0, 1 );
3525 if ( fNew )
3526 {
3527 Gia_Man_t * pGia;
3528 Gia_ParSim_t Pars, * pPars = &Pars;
3529 Gia_ManSimSetDefaultParams( pPars );
3530 pPars->nWords = nWords;
3531 pPars->nIters = nFrames;
3532 pPars->TimeLimit = TimeOut;
3533 pPars->fCheckMiter = fMiter;
3534 pPars->fVerbose = fVerbose;
3535 pGia = Gia_ManFromAig( pMan );
3536 if ( Gia_ManSimSimulate( pGia, pPars ) )
3537 {
3538 if ( pGia->pCexSeq )
3539 {
3540 Abc_Print( 1, "Simulation of %d frames with %d words asserted output %d in frame %d. ",
3541 nFrames, nWords, pGia->pCexSeq->iPo, pGia->pCexSeq->iFrame );
3542 status = Saig_ManVerifyCex( pMan, pGia->pCexSeq );
3543 if ( status == 0 )
3544 Abc_Print( 1, "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
3545 }
3546 ABC_FREE( pNtk->pModel );
3547 ABC_FREE( pNtk->pSeqModel );
3548 pNtk->pSeqModel = pGia->pCexSeq; pGia->pCexSeq = NULL;
3549 RetValue = 0;
3550 }
3551 else
3552 {
3553 Abc_Print( 1, "Simulation of %d frames with %d words did not assert the outputs. ",
3554 nFrames, nWords );
3555 }
3556 Gia_ManStop( pGia );
3557 }
3558 else // comb/seq simulator
3559 {
3560 Fra_Sml_t * pSml;
3561 if ( pFileSim != NULL )
3562 {
3563 assert( Abc_NtkLatchNum(pNtk) == 0 );
3564 pSml = Fra_SmlSimulateCombGiven( pMan, pFileSim, fMiter, fVerbose );
3565 }
3566 else if ( Abc_NtkLatchNum(pNtk) == 0 )
3567 pSml = Fra_SmlSimulateComb( pMan, nWords, fMiter );
3568 else
3569 pSml = Fra_SmlSimulateSeq( pMan, 0, nFrames, nWords, fMiter );
3570 if ( pSml->fNonConstOut )
3571 {
3572 pCex = Fra_SmlGetCounterExample( pSml );
3573 if ( pCex )
3574 {
3575 Abc_Print( 1, "Simulation of %d frame%s with %d word%s asserted output %d in frame %d. ",
3576 pSml->nFrames, pSml->nFrames == 1 ? "": "s",
3577 pSml->nWordsFrame, pSml->nWordsFrame == 1 ? "": "s",
3578 pCex->iPo, pCex->iFrame );
3579 status = Saig_ManVerifyCex( pMan, pCex );
3580 if ( status == 0 )
3581 Abc_Print( 1, "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
3582 }
3583 ABC_FREE( pNtk->pModel );
3584 ABC_FREE( pNtk->pSeqModel );
3585 pNtk->pSeqModel = pCex;
3586 RetValue = 0;
3587 }
3588 else
3589 {
3590 Abc_Print( 1, "Simulation of %d frames with %d words did not assert the outputs. ",
3591 nFrames, nWords );
3592 }
3593 Fra_SmlStop( pSml );
3594 }
3595 ABC_PRT( "Time", Abc_Clock() - clk );
3596 Aig_ManStop( pMan );
3597 return RetValue;
3598 }
3599
3600 /**Function*************************************************************
3601
3602 Synopsis [Performs random simulation.]
3603
3604 Description []
3605
3606 SideEffects []
3607
3608 SeeAlso []
3609
3610 ***********************************************************************/
Abc_NtkDarSeqSim3(Abc_Ntk_t * pNtk,Ssw_RarPars_t * pPars)3611 int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, Ssw_RarPars_t * pPars )
3612 {
3613 Aig_Man_t * pMan;
3614 int status, RetValue = -1;
3615 // abctime clk = Abc_Clock();
3616 if ( Abc_NtkGetChoiceNum(pNtk) )
3617 {
3618 Abc_Print( 1, "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pNtk) );
3619 Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
3620 }
3621 pMan = Abc_NtkToDar( pNtk, 0, 1 );
3622 if ( Ssw_RarSimulate( pMan, pPars ) == 0 )
3623 {
3624 if ( pMan->pSeqModel )
3625 {
3626 // Abc_Print( 1, "Simulation of %d frames with %d words asserted output %d in frame %d. ",
3627 // nFrames, nWords, pMan->pSeqModel->iPo, pMan->pSeqModel->iFrame );
3628 status = Saig_ManVerifyCex( pMan, pMan->pSeqModel );
3629 if ( status == 0 )
3630 Abc_Print( 1, "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
3631 }
3632 ABC_FREE( pNtk->pModel );
3633 ABC_FREE( pNtk->pSeqModel );
3634 pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
3635 RetValue = 0;
3636 }
3637 else
3638 {
3639 // Abc_Print( 1, "Simulation of %d frames with %d words did not assert the outputs. ",
3640 // nFrames, nWords );
3641 }
3642 if ( pNtk->vSeqModelVec )
3643 Vec_PtrFreeFree( pNtk->vSeqModelVec );
3644 pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
3645 // ABC_PRT( "Time", Abc_Clock() - clk );
3646 pNtk->pData = pMan->pData; pMan->pData = NULL;
3647 Aig_ManStop( pMan );
3648 return RetValue;
3649 }
3650
3651 /**Function*************************************************************
3652
3653 Synopsis [Gives the current ABC network to AIG manager for processing.]
3654
3655 Description []
3656
3657 SideEffects []
3658
3659 SeeAlso []
3660
3661 ***********************************************************************/
Abc_NtkDarClau(Abc_Ntk_t * pNtk,int nFrames,int nPref,int nClauses,int nLutSize,int nLevels,int nCutsMax,int nBatches,int fStepUp,int fBmc,int fRefs,int fTarget,int fVerbose,int fVeryVerbose)3662 int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nPref, int nClauses, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose )
3663 {
3664 extern int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose );
3665 extern int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClauses, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose );
3666 Aig_Man_t * pMan;
3667 if ( fTarget && Abc_NtkPoNum(pNtk) != 1 )
3668 {
3669 Abc_Print( 1, "The number of outputs should be 1.\n" );
3670 return 1;
3671 }
3672 pMan = Abc_NtkToDar( pNtk, 0, 1 );
3673 if ( pMan == NULL )
3674 return 1;
3675 // Aig_ManReduceLachesCount( pMan );
3676 if ( pMan->vFlopNums )
3677 Vec_IntFree( pMan->vFlopNums );
3678 pMan->vFlopNums = NULL;
3679
3680 // Fra_Clau( pMan, nStepsMax, fVerbose, fVeryVerbose );
3681 Fra_Claus( pMan, nFrames, nPref, nClauses, nLutSize, nLevels, nCutsMax, nBatches, fStepUp, fBmc, fRefs, fTarget, fVerbose, fVeryVerbose );
3682 Aig_ManStop( pMan );
3683 return 1;
3684 }
3685
3686 /**Function*************************************************************
3687
3688 Synopsis [Performs targe enlargement.]
3689
3690 Description []
3691
3692 SideEffects []
3693
3694 SeeAlso []
3695
3696 ***********************************************************************/
Abc_NtkDarEnlarge(Abc_Ntk_t * pNtk,int nFrames,int fVerbose)3697 Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
3698 {
3699 Abc_Ntk_t * pNtkAig;
3700 Aig_Man_t * pMan, * pTemp;
3701 pMan = Abc_NtkToDar( pNtk, 0, 1 );
3702 if ( pMan == NULL )
3703 return NULL;
3704 pMan = Aig_ManFrames( pTemp = pMan, nFrames, 0, 1, 1, 1, NULL );
3705 Aig_ManStop( pTemp );
3706 pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
3707 Aig_ManStop( pMan );
3708 return pNtkAig;
3709 }
3710
3711 /**Function*************************************************************
3712
3713 Synopsis [Performs targe enlargement.]
3714
3715 Description []
3716
3717 SideEffects []
3718
3719 SeeAlso []
3720
3721 ***********************************************************************/
Abc_NtkDarTempor(Abc_Ntk_t * pNtk,int nFrames,int TimeOut,int nConfLimit,int fUseBmc,int fUseTransSigs,int fVerbose,int fVeryVerbose)3722 Abc_Ntk_t * Abc_NtkDarTempor( Abc_Ntk_t * pNtk, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fUseTransSigs, int fVerbose, int fVeryVerbose )
3723 {
3724 extern Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fUseTransSigs, int fVerbose, int fVeryVerbose );
3725 Abc_Ntk_t * pNtkAig;
3726 Aig_Man_t * pMan, * pTemp;
3727 pMan = Abc_NtkToDar( pNtk, 0, 1 );
3728 if ( pMan == NULL )
3729 return NULL;
3730 pTemp = Saig_ManTempor( pMan, nFrames, TimeOut, nConfLimit, fUseBmc, fUseTransSigs, fVerbose, fVeryVerbose );
3731 Aig_ManStop( pMan );
3732 if ( pTemp == NULL )
3733 return Abc_NtkDup( pNtk );
3734 pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pTemp );
3735 Aig_ManStop( pTemp );
3736 return pNtkAig;
3737 }
3738
3739 /**Function*************************************************************
3740
3741 Synopsis [Performs induction for property only.]
3742
3743 Description []
3744
3745 SideEffects []
3746
3747 SeeAlso []
3748
3749 ***********************************************************************/
Abc_NtkDarInduction(Abc_Ntk_t * pNtk,int nTimeOut,int nFramesMax,int nConfMax,int fUnique,int fUniqueAll,int fGetCex,int fVerbose,int fVeryVerbose)3750 int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nTimeOut, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose )
3751 {
3752 Aig_Man_t * pMan;
3753 abctime clkTotal = Abc_Clock();
3754 int RetValue;
3755 pMan = Abc_NtkToDar( pNtk, 0, 1 );
3756 if ( pMan == NULL )
3757 return -1;
3758 RetValue = Saig_ManInduction( pMan, nTimeOut, nFramesMax, nConfMax, fUnique, fUniqueAll, fGetCex, fVerbose, fVeryVerbose );
3759 if ( RetValue == 1 )
3760 {
3761 Abc_Print( 1, "Networks are equivalent. " );
3762 ABC_PRT( "Time", Abc_Clock() - clkTotal );
3763 }
3764 else if ( RetValue == 0 )
3765 {
3766 Abc_Print( 1, "Networks are NOT EQUIVALENT. " );
3767 ABC_PRT( "Time", Abc_Clock() - clkTotal );
3768 }
3769 else
3770 {
3771 Abc_Print( 1, "Networks are UNDECIDED. " );
3772 ABC_PRT( "Time", Abc_Clock() - clkTotal );
3773 }
3774 if ( fGetCex )
3775 {
3776 ABC_FREE( pNtk->pModel );
3777 ABC_FREE( pNtk->pSeqModel );
3778 pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
3779 }
3780 Aig_ManStop( pMan );
3781 return RetValue;
3782 }
3783
3784
3785 /**Function*************************************************************
3786
3787 Synopsis [Interplates two networks.]
3788
3789 Description []
3790
3791 SideEffects []
3792
3793 SeeAlso []
3794
3795 ***********************************************************************/
Abc_NtkInterOne(Abc_Ntk_t * pNtkOn,Abc_Ntk_t * pNtkOff,int fRelation,int fVerbose)3796 Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation, int fVerbose )
3797 {
3798 extern Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fRelation, int fVerbose );
3799 Abc_Ntk_t * pNtkAig;
3800 Aig_Man_t * pManOn, * pManOff, * pManAig;
3801 if ( Abc_NtkCoNum(pNtkOn) != 1 || Abc_NtkCoNum(pNtkOff) != 1 )
3802 {
3803 Abc_Print( 1, "Currently works only for single-output networks.\n" );
3804 return NULL;
3805 }
3806 if ( Abc_NtkCiNum(pNtkOn) != Abc_NtkCiNum(pNtkOff) )
3807 {
3808 Abc_Print( 1, "The number of PIs should be the same.\n" );
3809 return NULL;
3810 }
3811 // create internal AIGs
3812 pManOn = Abc_NtkToDar( pNtkOn, 0, 0 );
3813 if ( pManOn == NULL )
3814 return NULL;
3815 pManOff = Abc_NtkToDar( pNtkOff, 0, 0 );
3816 if ( pManOff == NULL )
3817 return NULL;
3818 // derive the interpolant
3819 pManAig = Aig_ManInter( pManOn, pManOff, fRelation, fVerbose );
3820 if ( pManAig == NULL )
3821 {
3822 Abc_Print( 1, "Interpolant computation failed.\n" );
3823 return NULL;
3824 }
3825 Aig_ManStop( pManOn );
3826 Aig_ManStop( pManOff );
3827 // for the relation, add an extra input
3828 if ( fRelation )
3829 {
3830 Abc_Obj_t * pObj;
3831 pObj = Abc_NtkCreatePi( pNtkOff );
3832 Abc_ObjAssignName( pObj, "New", NULL );
3833 }
3834 // create logic network
3835 pNtkAig = Abc_NtkFromDar( pNtkOff, pManAig );
3836 Aig_ManStop( pManAig );
3837 return pNtkAig;
3838 }
Gia_ManInterOne(Gia_Man_t * pNtkOn,Gia_Man_t * pNtkOff,int fVerbose)3839 Gia_Man_t * Gia_ManInterOne( Gia_Man_t * pNtkOn, Gia_Man_t * pNtkOff, int fVerbose )
3840 {
3841 extern Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fRelation, int fVerbose );
3842 Gia_Man_t * pNtkAig;
3843 Aig_Man_t * pManOn, * pManOff, * pManAig;
3844 assert( Gia_ManCiNum(pNtkOn) == Gia_ManCiNum(pNtkOff) );
3845 assert( Gia_ManCoNum(pNtkOn) == 1 );
3846 assert( Gia_ManCoNum(pNtkOff) == 1 );
3847 // create internal AIGs
3848 pManOn = Gia_ManToAigSimple( pNtkOn );
3849 if ( pManOn == NULL )
3850 return NULL;
3851 pManOff = Gia_ManToAigSimple( pNtkOff );
3852 if ( pManOff == NULL )
3853 return NULL;
3854 // derive the interpolant
3855 pManAig = Aig_ManInter( pManOn, pManOff, 0, fVerbose );
3856 if ( pManAig == NULL )
3857 {
3858 Abc_Print( 1, "Interpolant computation failed.\n" );
3859 return NULL;
3860 }
3861 Aig_ManStop( pManOn );
3862 Aig_ManStop( pManOff );
3863 // create logic network
3864 pNtkAig = Gia_ManFromAigSimple( pManAig );
3865 Aig_ManStop( pManAig );
3866 return pNtkAig;
3867 }
3868
3869 /**Function*************************************************************
3870
3871 Synopsis [Fast interpolation.]
3872
3873 Description []
3874
3875 SideEffects []
3876
3877 SeeAlso []
3878
3879 ***********************************************************************/
Abc_NtkInterFast(Abc_Ntk_t * pNtkOn,Abc_Ntk_t * pNtkOff,int fVerbose)3880 void Abc_NtkInterFast( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
3881 {
3882 extern void Aig_ManInterFast( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose );
3883 Aig_Man_t * pManOn, * pManOff;
3884 // create internal AIGs
3885 pManOn = Abc_NtkToDar( pNtkOn, 0, 0 );
3886 if ( pManOn == NULL )
3887 return;
3888 pManOff = Abc_NtkToDar( pNtkOff, 0, 0 );
3889 if ( pManOff == NULL )
3890 return;
3891 Aig_ManInterFast( pManOn, pManOff, fVerbose );
3892 Aig_ManStop( pManOn );
3893 Aig_ManStop( pManOff );
3894 }
3895
3896 abctime timeCnf;
3897 abctime timeSat;
3898 abctime timeInt;
3899
3900 /**Function*************************************************************
3901
3902 Synopsis [Interplates two networks.]
3903
3904 Description []
3905
3906 SideEffects []
3907
3908 SeeAlso []
3909
3910 ***********************************************************************/
Abc_NtkInter(Abc_Ntk_t * pNtkOn,Abc_Ntk_t * pNtkOff,int fRelation,int fVerbose)3911 Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation, int fVerbose )
3912 {
3913 Abc_Ntk_t * pNtkOn1, * pNtkOff1, * pNtkInter1, * pNtkInter;
3914 Abc_Obj_t * pObj;
3915 int i; //, clk = Abc_Clock();
3916 if ( Abc_NtkCoNum(pNtkOn) != Abc_NtkCoNum(pNtkOff) )
3917 {
3918 Abc_Print( 1, "Currently works only for networks with equal number of POs.\n" );
3919 return NULL;
3920 }
3921 // compute the fast interpolation time
3922 // Abc_NtkInterFast( pNtkOn, pNtkOff, fVerbose );
3923 // consider the case of one output
3924 if ( Abc_NtkCoNum(pNtkOn) == 1 )
3925 return Abc_NtkInterOne( pNtkOn, pNtkOff, fRelation, fVerbose );
3926 // start the new network
3927 pNtkInter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
3928 pNtkInter->pName = Extra_UtilStrsav(pNtkOn->pName);
3929 Abc_NtkForEachPi( pNtkOn, pObj, i )
3930 Abc_NtkDupObj( pNtkInter, pObj, 1 );
3931 // process each POs separately
3932 timeCnf = 0;
3933 timeSat = 0;
3934 timeInt = 0;
3935 Abc_NtkForEachCo( pNtkOn, pObj, i )
3936 {
3937 pNtkOn1 = Abc_NtkCreateCone( pNtkOn, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 1 );
3938 if ( Abc_ObjFaninC0(pObj) )
3939 Abc_ObjXorFaninC( Abc_NtkPo(pNtkOn1, 0), 0 );
3940
3941 pObj = Abc_NtkCo(pNtkOff, i);
3942 pNtkOff1 = Abc_NtkCreateCone( pNtkOff, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 1 );
3943 if ( Abc_ObjFaninC0(pObj) )
3944 Abc_ObjXorFaninC( Abc_NtkPo(pNtkOff1, 0), 0 );
3945
3946 if ( Abc_NtkNodeNum(pNtkOn1) == 0 )
3947 pNtkInter1 = Abc_NtkDup( pNtkOn1 );
3948 else if ( Abc_NtkNodeNum(pNtkOff1) == 0 )
3949 {
3950 pNtkInter1 = Abc_NtkDup( pNtkOff1 );
3951 Abc_ObjXorFaninC( Abc_NtkPo(pNtkInter1, 0), 0 );
3952 }
3953 else
3954 pNtkInter1 = Abc_NtkInterOne( pNtkOn1, pNtkOff1, 0, fVerbose );
3955 if ( pNtkInter1 )
3956 {
3957 Abc_NtkAppend( pNtkInter, pNtkInter1, 1 );
3958 Abc_NtkDelete( pNtkInter1 );
3959 }
3960
3961 Abc_NtkDelete( pNtkOn1 );
3962 Abc_NtkDelete( pNtkOff1 );
3963 }
3964 // ABC_PRT( "CNF", timeCnf );
3965 // ABC_PRT( "SAT", timeSat );
3966 // ABC_PRT( "Int", timeInt );
3967 // ABC_PRT( "Slow interpolation time", Abc_Clock() - clk );
3968
3969 // return the network
3970 if ( !Abc_NtkCheck( pNtkInter ) )
3971 Abc_Print( 1, "Abc_NtkAttachBottom(): Network check has failed.\n" );
3972 return pNtkInter;
3973 }
3974
3975 /**Function*************************************************************
3976
3977 Synopsis []
3978
3979 Description []
3980
3981 SideEffects []
3982
3983 SeeAlso []
3984
3985 ***********************************************************************/
Abc_NtkPrintSccs(Abc_Ntk_t * pNtk,int fVerbose)3986 void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose )
3987 {
3988 // extern Vec_Ptr_t * Aig_ManRegPartitionLinear( Aig_Man_t * pAig, int nPartSize );
3989 Aig_Man_t * pMan;
3990 pMan = Abc_NtkToDar( pNtk, 0, 1 );
3991 if ( pMan == NULL )
3992 return;
3993 Aig_ManComputeSccs( pMan );
3994 // Aig_ManRegPartitionLinear( pMan, 1000 );
3995 Aig_ManStop( pMan );
3996 }
3997
3998 /**Function*************************************************************
3999
4000 Synopsis []
4001
4002 Description []
4003
4004 SideEffects []
4005
4006 SeeAlso []
4007
4008 ***********************************************************************/
Abc_NtkDarPrintCone(Abc_Ntk_t * pNtk)4009 int Abc_NtkDarPrintCone( Abc_Ntk_t * pNtk )
4010 {
4011 extern void Saig_ManPrintCones( Aig_Man_t * pAig );
4012 Aig_Man_t * pMan;
4013 pMan = Abc_NtkToDar( pNtk, 0, 1 );
4014 if ( pMan == NULL )
4015 return 0;
4016 assert( Aig_ManRegNum(pMan) > 0 );
4017 Saig_ManPrintCones( pMan );
4018 Aig_ManStop( pMan );
4019 return 1;
4020 }
4021
4022 /**Function*************************************************************
4023
4024 Synopsis []
4025
4026 Description []
4027
4028 SideEffects []
4029
4030 SeeAlso []
4031
4032 ***********************************************************************/
Abc_NtkBalanceExor(Abc_Ntk_t * pNtk,int fUpdateLevel,int fVerbose)4033 Abc_Ntk_t * Abc_NtkBalanceExor( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose )
4034 {
4035 extern void Dar_BalancePrintStats( Aig_Man_t * p );
4036 Abc_Ntk_t * pNtkAig;
4037 Aig_Man_t * pMan, * pTemp;//, * pTemp2;
4038 assert( Abc_NtkIsStrash(pNtk) );
4039 // derive AIG with EXORs
4040 pMan = Abc_NtkToDar( pNtk, 1, 0 );
4041 if ( pMan == NULL )
4042 return NULL;
4043 // Aig_ManPrintStats( pMan );
4044 if ( fVerbose )
4045 Dar_BalancePrintStats( pMan );
4046 // perform balancing
4047 pTemp = Dar_ManBalance( pMan, fUpdateLevel );
4048 // Aig_ManPrintStats( pTemp );
4049 // create logic network
4050 pNtkAig = Abc_NtkFromDar( pNtk, pTemp );
4051 Aig_ManStop( pTemp );
4052 Aig_ManStop( pMan );
4053 return pNtkAig;
4054 }
4055
4056 /**Function*************************************************************
4057
4058 Synopsis [Performs phase abstraction.]
4059
4060 Description []
4061
4062 SideEffects []
4063
4064 SeeAlso []
4065
4066 ***********************************************************************/
Abc_NtkPhaseAbstract(Abc_Ntk_t * pNtk,int nFrames,int nPref,int fIgnore,int fPrint,int fVerbose)4067 Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose )
4068 {
4069 extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose );
4070 Vec_Int_t * vInits;
4071 Abc_Ntk_t * pNtkAig;
4072 Aig_Man_t * pMan, * pTemp;
4073 pMan = Abc_NtkToDar( pNtk, 0, 1 );
4074 if ( pMan == NULL )
4075 return NULL;
4076 vInits = Abc_NtkGetLatchValues(pNtk);
4077 pMan = Saig_ManPhaseAbstract( pTemp = pMan, vInits, nFrames, nPref, fIgnore, fPrint, fVerbose );
4078 Vec_IntFree( vInits );
4079 Aig_ManStop( pTemp );
4080 if ( pMan == NULL )
4081 return NULL;
4082 pNtkAig = Abc_NtkFromAigPhase( pMan );
4083 // pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
4084 // pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
4085 Aig_ManStop( pMan );
4086 return pNtkAig;
4087 }
4088
4089 /**Function*************************************************************
4090
4091 Synopsis [Performs phase abstraction.]
4092
4093 Description []
4094
4095 SideEffects []
4096
4097 SeeAlso []
4098
4099 ***********************************************************************/
Abc_NtkPhaseFrameNum(Abc_Ntk_t * pNtk)4100 int Abc_NtkPhaseFrameNum( Abc_Ntk_t * pNtk )
4101 {
4102 extern int Saig_ManPhaseFrameNum( Aig_Man_t * p, Vec_Int_t * vInits );
4103 Vec_Int_t * vInits;
4104 Aig_Man_t * pMan;
4105 int nFrames;
4106 pMan = Abc_NtkToDar( pNtk, 0, 1 );
4107 if ( pMan == NULL )
4108 return 1;
4109 vInits = Abc_NtkGetLatchValues(pNtk);
4110 nFrames = Saig_ManPhaseFrameNum( pMan, vInits );
4111 Vec_IntFree( vInits );
4112 Aig_ManStop( pMan );
4113 return nFrames;
4114 }
4115
4116 /**Function*************************************************************
4117
4118 Synopsis [Performs phase abstraction.]
4119
4120 Description []
4121
4122 SideEffects []
4123
4124 SeeAlso []
4125
4126 ***********************************************************************/
Abc_NtkDarSynchOne(Abc_Ntk_t * pNtk,int nWords,int fVerbose)4127 Abc_Ntk_t * Abc_NtkDarSynchOne( Abc_Ntk_t * pNtk, int nWords, int fVerbose )
4128 {
4129 extern Aig_Man_t * Saig_SynchSequenceApply( Aig_Man_t * pAig, int nWords, int fVerbose );
4130 Abc_Ntk_t * pNtkAig;
4131 Aig_Man_t * pMan, * pTemp;
4132 pMan = Abc_NtkToDar( pNtk, 0, 1 );
4133 if ( pMan == NULL )
4134 return NULL;
4135 pMan = Saig_SynchSequenceApply( pTemp = pMan, nWords, fVerbose );
4136 Aig_ManStop( pTemp );
4137 if ( pMan == NULL )
4138 return NULL;
4139 pNtkAig = Abc_NtkFromDar( pNtk, pMan );
4140 Aig_ManStop( pMan );
4141 return pNtkAig;
4142 }
4143
4144 /**Function*************************************************************
4145
4146 Synopsis [Performs phase abstraction.]
4147
4148 Description []
4149
4150 SideEffects []
4151
4152 SeeAlso []
4153
4154 ***********************************************************************/
Abc_NtkDarSynch(Abc_Ntk_t * pNtk1,Abc_Ntk_t * pNtk2,int nWords,int fVerbose)4155 Abc_Ntk_t * Abc_NtkDarSynch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nWords, int fVerbose )
4156 {
4157 extern Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords, int fVerbose );
4158 Abc_Ntk_t * pNtkAig;
4159 Aig_Man_t * pMan1, * pMan2, * pMan;
4160 pMan1 = Abc_NtkToDar( pNtk1, 0, 1 );
4161 if ( pMan1 == NULL )
4162 return NULL;
4163 pMan2 = Abc_NtkToDar( pNtk2, 0, 1 );
4164 if ( pMan2 == NULL )
4165 {
4166 Aig_ManStop( pMan1 );
4167 return NULL;
4168 }
4169 pMan = Saig_Synchronize( pMan1, pMan2, nWords, fVerbose );
4170 Aig_ManStop( pMan1 );
4171 Aig_ManStop( pMan2 );
4172 if ( pMan == NULL )
4173 return NULL;
4174 pNtkAig = Abc_NtkFromAigPhase( pMan );
4175 // pNtkAig->pName = Extra_UtilStrsav("miter");
4176 // pNtkAig->pSpec = NULL;
4177 Aig_ManStop( pMan );
4178 return pNtkAig;
4179 }
4180
4181 /**Function*************************************************************
4182
4183 Synopsis [Performs phase abstraction.]
4184
4185 Description []
4186
4187 SideEffects []
4188
4189 SeeAlso []
4190
4191 ***********************************************************************/
Abc_NtkDarClockGate(Abc_Ntk_t * pNtk,Abc_Ntk_t * pCare,Cgt_Par_t * pPars)4192 Abc_Ntk_t * Abc_NtkDarClockGate( Abc_Ntk_t * pNtk, Abc_Ntk_t * pCare, Cgt_Par_t * pPars )
4193 {
4194 Abc_Ntk_t * pNtkAig;
4195 Aig_Man_t * pMan1, * pMan2 = NULL, * pMan;
4196 pMan1 = Abc_NtkToDar( pNtk, 0, 1 );
4197 if ( pMan1 == NULL )
4198 return NULL;
4199 if ( pCare )
4200 {
4201 pMan2 = Abc_NtkToDar( pCare, 0, 0 );
4202 if ( pMan2 == NULL )
4203 {
4204 Aig_ManStop( pMan1 );
4205 return NULL;
4206 }
4207 }
4208 pMan = Cgt_ClockGating( pMan1, pMan2, pPars );
4209 Aig_ManStop( pMan1 );
4210 if ( pMan2 )
4211 Aig_ManStop( pMan2 );
4212 if ( pMan == NULL )
4213 return NULL;
4214 pNtkAig = Abc_NtkFromDar( pNtk, pMan );
4215 Aig_ManStop( pMan );
4216 return pNtkAig;
4217 }
4218
4219 /**Function*************************************************************
4220
4221 Synopsis [Performs phase abstraction.]
4222
4223 Description []
4224
4225 SideEffects []
4226
4227 SeeAlso []
4228
4229 ***********************************************************************/
Abc_NtkDarExtWin(Abc_Ntk_t * pNtk,int nObjId,int nDist,int fVerbose)4230 Abc_Ntk_t * Abc_NtkDarExtWin( Abc_Ntk_t * pNtk, int nObjId, int nDist, int fVerbose )
4231 {
4232 Abc_Ntk_t * pNtkAig;
4233 Aig_Man_t * pMan1, * pMan;
4234 Aig_Obj_t * pObj;
4235 pMan1 = Abc_NtkToDar( pNtk, 0, 1 );
4236 if ( pMan1 == NULL )
4237 return NULL;
4238 if ( nObjId == -1 )
4239 {
4240 pObj = Saig_ManFindPivot( pMan1 );
4241 Abc_Print( 1, "Selected object %d as a window pivot.\n", pObj->Id );
4242 }
4243 else
4244 {
4245 if ( nObjId >= Aig_ManObjNumMax(pMan1) )
4246 {
4247 Aig_ManStop( pMan1 );
4248 Abc_Print( 1, "The ID is too large.\n" );
4249 return NULL;
4250 }
4251 pObj = Aig_ManObj( pMan1, nObjId );
4252 if ( pObj == NULL )
4253 {
4254 Aig_ManStop( pMan1 );
4255 Abc_Print( 1, "Object with ID %d does not exist.\n", nObjId );
4256 return NULL;
4257 }
4258 if ( !Saig_ObjIsLo(pMan1, pObj) && !Aig_ObjIsNode(pObj) )
4259 {
4260 Aig_ManStop( pMan1 );
4261 Abc_Print( 1, "Object with ID %d is not a node or reg output.\n", nObjId );
4262 return NULL;
4263 }
4264 }
4265 pMan = Saig_ManWindowExtract( pMan1, pObj, nDist );
4266 Aig_ManStop( pMan1 );
4267 if ( pMan == NULL )
4268 return NULL;
4269 pNtkAig = Abc_NtkFromAigPhase( pMan );
4270 pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
4271 pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
4272 Aig_ManStop( pMan );
4273 return pNtkAig;
4274 }
4275
4276 /**Function*************************************************************
4277
4278 Synopsis [Performs phase abstraction.]
4279
4280 Description []
4281
4282 SideEffects []
4283
4284 SeeAlso []
4285
4286 ***********************************************************************/
Abc_NtkDarInsWin(Abc_Ntk_t * pNtk,Abc_Ntk_t * pCare,int nObjId,int nDist,int fVerbose)4287 Abc_Ntk_t * Abc_NtkDarInsWin( Abc_Ntk_t * pNtk, Abc_Ntk_t * pCare, int nObjId, int nDist, int fVerbose )
4288 {
4289 Abc_Ntk_t * pNtkAig;
4290 Aig_Man_t * pMan1, * pMan2 = NULL, * pMan;
4291 Aig_Obj_t * pObj;
4292 pMan1 = Abc_NtkToDar( pNtk, 0, 1 );
4293 if ( pMan1 == NULL )
4294 return NULL;
4295 if ( nObjId == -1 )
4296 {
4297 pObj = Saig_ManFindPivot( pMan1 );
4298 Abc_Print( 1, "Selected object %d as a window pivot.\n", pObj->Id );
4299 }
4300 else
4301 {
4302 if ( nObjId >= Aig_ManObjNumMax(pMan1) )
4303 {
4304 Aig_ManStop( pMan1 );
4305 Abc_Print( 1, "The ID is too large.\n" );
4306 return NULL;
4307 }
4308 pObj = Aig_ManObj( pMan1, nObjId );
4309 if ( pObj == NULL )
4310 {
4311 Aig_ManStop( pMan1 );
4312 Abc_Print( 1, "Object with ID %d does not exist.\n", nObjId );
4313 return NULL;
4314 }
4315 if ( !Saig_ObjIsLo(pMan1, pObj) && !Aig_ObjIsNode(pObj) )
4316 {
4317 Aig_ManStop( pMan1 );
4318 Abc_Print( 1, "Object with ID %d is not a node or reg output.\n", nObjId );
4319 return NULL;
4320 }
4321 }
4322 if ( pCare )
4323 {
4324 pMan2 = Abc_NtkToDar( pCare, 0, 0 );
4325 if ( pMan2 == NULL )
4326 {
4327 Aig_ManStop( pMan1 );
4328 return NULL;
4329 }
4330 }
4331 pMan = Saig_ManWindowInsert( pMan1, pObj, nDist, pMan2 );
4332 Aig_ManStop( pMan1 );
4333 if ( pMan2 )
4334 Aig_ManStop( pMan2 );
4335 if ( pMan == NULL )
4336 return NULL;
4337 pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
4338 Aig_ManStop( pMan );
4339 return pNtkAig;
4340 }
4341
4342 /**Function*************************************************************
4343
4344 Synopsis [Performs phase abstraction.]
4345
4346 Description []
4347
4348 SideEffects []
4349
4350 SeeAlso []
4351
4352 ***********************************************************************/
Abc_NtkDarFrames(Abc_Ntk_t * pNtk,int nPrefix,int nFrames,int fInit,int fVerbose)4353 Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fInit, int fVerbose )
4354 {
4355 Abc_Ntk_t * pNtkAig;
4356 Aig_Man_t * pMan, * pTemp;
4357 pMan = Abc_NtkToDar( pNtk, 0, 1 );
4358 if ( pMan == NULL )
4359 return NULL;
4360 pMan = Saig_ManTimeframeSimplify( pTemp = pMan, nPrefix, nFrames, fInit, fVerbose );
4361 Aig_ManStop( pTemp );
4362 if ( pMan == NULL )
4363 return NULL;
4364 pNtkAig = Abc_NtkFromAigPhase( pMan );
4365 pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
4366 pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
4367 Aig_ManStop( pMan );
4368 return pNtkAig;
4369 }
4370
4371 /**Function*************************************************************
4372
4373 Synopsis [Performs phase abstraction.]
4374
4375 Description []
4376
4377 SideEffects []
4378
4379 SeeAlso []
4380
4381 ***********************************************************************/
Abc_NtkDarCleanupAig(Abc_Ntk_t * pNtk,int fCleanupPis,int fCleanupPos,int fVerbose)4382 Abc_Ntk_t * Abc_NtkDarCleanupAig( Abc_Ntk_t * pNtk, int fCleanupPis, int fCleanupPos, int fVerbose )
4383 {
4384 Abc_Ntk_t * pNtkAig;
4385 Aig_Man_t * pMan;
4386 pMan = Abc_NtkToDar( pNtk, 0, 1 );
4387 if ( pMan == NULL )
4388 return NULL;
4389 if ( fCleanupPis )
4390 {
4391 int Temp = Aig_ManCiCleanup( pMan );
4392 if ( fVerbose )
4393 Abc_Print( 1, "Cleanup removed %d primary inputs without fanout.\n", Temp );
4394 }
4395 if ( fCleanupPos )
4396 {
4397 int Temp = Aig_ManCoCleanup( pMan );
4398 if ( fVerbose )
4399 Abc_Print( 1, "Cleanup removed %d primary outputs driven by const-0.\n", Temp );
4400 }
4401 pNtkAig = Abc_NtkFromAigPhase( pMan );
4402 pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
4403 pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
4404 Aig_ManStop( pMan );
4405 return pNtkAig;
4406 }
4407
4408 /**Function*************************************************************
4409
4410 Synopsis [Performs BDD-based reachability analysis.]
4411
4412 Description []
4413
4414 SideEffects []
4415
4416 SeeAlso []
4417
4418 ***********************************************************************/
Abc_NtkDarReach(Abc_Ntk_t * pNtk,Saig_ParBbr_t * pPars)4419 int Abc_NtkDarReach( Abc_Ntk_t * pNtk, Saig_ParBbr_t * pPars )
4420 {
4421 Aig_Man_t * pMan;
4422 int RetValue;
4423 pMan = Abc_NtkToDar( pNtk, 0, 1 );
4424 if ( pMan == NULL )
4425 return -1;
4426 RetValue = Aig_ManVerifyUsingBdds( pMan, pPars );
4427 ABC_FREE( pNtk->pModel );
4428 ABC_FREE( pNtk->pSeqModel );
4429 pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
4430 Aig_ManStop( pMan );
4431 return RetValue;
4432 }
4433
4434 ABC_NAMESPACE_IMPL_END
4435
4436 #include "map/amap/amap.h"
4437 #include "map/mio/mio.h"
4438
4439 ABC_NAMESPACE_IMPL_START
4440
4441
4442 /**Function*************************************************************
4443
4444 Synopsis []
4445
4446 Description []
4447
4448 SideEffects []
4449
4450 SeeAlso []
4451
4452 ***********************************************************************/
Amap_ManProduceNetwork(Abc_Ntk_t * pNtk,Vec_Ptr_t * vMapping)4453 Abc_Ntk_t * Amap_ManProduceNetwork( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapping )
4454 {
4455 // extern void * Abc_FrameReadLibGen();
4456 Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen();
4457 Amap_Out_t * pRes;
4458 Vec_Ptr_t * vNodesNew;
4459 Abc_Ntk_t * pNtkNew;
4460 Abc_Obj_t * pNodeNew, * pFaninNew;
4461 int i, k, iPis, iPos, nDupGates;
4462 // make sure gates exist in the current library
4463 Vec_PtrForEachEntry( Amap_Out_t *, vMapping, pRes, i )
4464 if ( pRes->pName && Mio_LibraryReadGateByName( pLib, pRes->pName, NULL ) == NULL )
4465 {
4466 Abc_Print( 1, "Current library does not contain gate \"%s\".\n", pRes->pName );
4467 return NULL;
4468 }
4469 // create the network
4470 pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_MAP );
4471 pNtkNew->pManFunc = pLib;
4472 iPis = iPos = 0;
4473 vNodesNew = Vec_PtrAlloc( Vec_PtrSize(vMapping) );
4474 Vec_PtrForEachEntry( Amap_Out_t *, vMapping, pRes, i )
4475 {
4476 if ( pRes->Type == -1 )
4477 pNodeNew = Abc_NtkCi( pNtkNew, iPis++ );
4478 else if ( pRes->Type == 1 )
4479 pNodeNew = Abc_NtkCo( pNtkNew, iPos++ );
4480 else
4481 {
4482 pNodeNew = Abc_NtkCreateNode( pNtkNew );
4483 pNodeNew->pData = Mio_LibraryReadGateByName( pLib, pRes->pName, NULL );
4484 }
4485 for ( k = 0; k < pRes->nFans; k++ )
4486 {
4487 pFaninNew = (Abc_Obj_t *)Vec_PtrEntry( vNodesNew, pRes->pFans[k] );
4488 Abc_ObjAddFanin( pNodeNew, pFaninNew );
4489 }
4490 Vec_PtrPush( vNodesNew, pNodeNew );
4491 }
4492 Vec_PtrFree( vNodesNew );
4493 assert( iPis == Abc_NtkCiNum(pNtkNew) );
4494 assert( iPos == Abc_NtkCoNum(pNtkNew) );
4495 // decouple the PO driver nodes to reduce the number of levels
4496 nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
4497 // if ( nDupGates && Map_ManReadVerbose(pMan) )
4498 // Abc_Print( 1, "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
4499 return pNtkNew;
4500 }
4501
4502 /**Function*************************************************************
4503
4504 Synopsis [Gives the current ABC network to AIG manager for processing.]
4505
4506 Description []
4507
4508 SideEffects []
4509
4510 SeeAlso []
4511
4512 ***********************************************************************/
Abc_NtkDarAmap(Abc_Ntk_t * pNtk,Amap_Par_t * pPars)4513 Abc_Ntk_t * Abc_NtkDarAmap( Abc_Ntk_t * pNtk, Amap_Par_t * pPars )
4514 {
4515 extern Vec_Ptr_t * Amap_ManTest( Aig_Man_t * pAig, Amap_Par_t * pPars );
4516 Vec_Ptr_t * vMapping;
4517 Abc_Ntk_t * pNtkAig = NULL;
4518 Aig_Man_t * pMan;
4519 Aig_MmFlex_t * pMem;
4520
4521 assert( Abc_NtkIsStrash(pNtk) );
4522 // convert to the AIG manager
4523 pMan = Abc_NtkToDarChoices( pNtk );
4524 if ( pMan == NULL )
4525 return NULL;
4526
4527 // perform computation
4528 vMapping = Amap_ManTest( pMan, pPars );
4529 Aig_ManStop( pMan );
4530 if ( vMapping == NULL )
4531 return NULL;
4532 pMem = (Aig_MmFlex_t *)Vec_PtrPop( vMapping );
4533 pNtkAig = Amap_ManProduceNetwork( pNtk, vMapping );
4534 Aig_MmFlexStop( pMem, 0 );
4535 Vec_PtrFree( vMapping );
4536
4537 // make sure everything is okay
4538 if ( pNtkAig && !Abc_NtkCheck( pNtkAig ) )
4539 {
4540 Abc_Print( 1, "Abc_NtkDar: The network check has failed.\n" );
4541 Abc_NtkDelete( pNtkAig );
4542 return NULL;
4543 }
4544 return pNtkAig;
4545 }
4546
4547 /**Function*************************************************************
4548
4549 Synopsis [Performs BDD-based reachability analysis.]
4550
4551 Description []
4552
4553 SideEffects []
4554
4555 SeeAlso []
4556
4557 ***********************************************************************/
Abc_NtkDarConstr(Abc_Ntk_t * pNtk,int nFrames,int nConfs,int nProps,int fStruct,int fOldAlgo,int fVerbose)4558 void Abc_NtkDarConstr( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose )
4559 {
4560 Aig_Man_t * pMan;//, * pMan2;//, * pTemp;
4561 assert( Abc_NtkIsStrash(pNtk) );
4562 pMan = Abc_NtkToDar( pNtk, 0, 1 );
4563 if ( pMan == NULL )
4564 return;
4565 if ( fStruct )
4566 Saig_ManDetectConstrTest( pMan );
4567 else
4568 Saig_ManDetectConstrFuncTest( pMan, nFrames, nConfs, nProps, fOldAlgo, fVerbose );
4569 Aig_ManStop( pMan );
4570 }
4571
4572 /**Function*************************************************************
4573
4574 Synopsis [Performs BDD-based reachability analysis.]
4575
4576 Description []
4577
4578 SideEffects []
4579
4580 SeeAlso []
4581
4582 ***********************************************************************/
Abc_NtkDarOutdec(Abc_Ntk_t * pNtk,int nLits,int fVerbose)4583 Abc_Ntk_t * Abc_NtkDarOutdec( Abc_Ntk_t * pNtk, int nLits, int fVerbose )
4584 {
4585 Abc_Ntk_t * pNtkAig;
4586 Aig_Man_t * pMan, * pTemp;
4587 assert( Abc_NtkIsStrash(pNtk) );
4588 pMan = Abc_NtkToDar( pNtk, 0, 1 );
4589 if ( pMan == NULL )
4590 return NULL;
4591 pMan = Saig_ManDecPropertyOutput( pTemp = pMan, nLits, fVerbose );
4592 Aig_ManStop( pTemp );
4593 if ( pMan == NULL )
4594 return NULL;
4595 pNtkAig = Abc_NtkFromAigPhase( pMan );
4596 pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
4597 pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
4598 Aig_ManStop( pMan );
4599 return pNtkAig;
4600 }
4601
4602 /**Function*************************************************************
4603
4604 Synopsis [Performs BDD-based reachability analysis.]
4605
4606 Description []
4607
4608 SideEffects []
4609
4610 SeeAlso []
4611
4612 ***********************************************************************/
Abc_NtkDarUnfold(Abc_Ntk_t * pNtk,int nFrames,int nConfs,int nProps,int fStruct,int fOldAlgo,int fVerbose)4613 Abc_Ntk_t * Abc_NtkDarUnfold( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose )
4614 {
4615 Abc_Ntk_t * pNtkAig;
4616 Aig_Man_t * pMan, * pTemp;
4617 assert( Abc_NtkIsStrash(pNtk) );
4618 pMan = Abc_NtkToDar( pNtk, 0, 1 );
4619 if ( pMan == NULL )
4620 return NULL;
4621 if ( fStruct )
4622 pMan = Saig_ManDupUnfoldConstrs( pTemp = pMan );
4623 else
4624 pMan = Saig_ManDupUnfoldConstrsFunc( pTemp = pMan, nFrames, nConfs, nProps, fOldAlgo, fVerbose );
4625 Aig_ManStop( pTemp );
4626 if ( pMan == NULL )
4627 return NULL;
4628 pNtkAig = Abc_NtkFromAigPhase( pMan );
4629 pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
4630 pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
4631 Aig_ManStop( pMan );
4632 return pNtkAig;
4633 }
4634
4635 /**Function*************************************************************
4636
4637 Synopsis [Performs BDD-based reachability analysis.]
4638
4639 Description []
4640
4641 SideEffects []
4642
4643 SeeAlso []
4644
4645 ***********************************************************************/
Abc_NtkDarFold(Abc_Ntk_t * pNtk,int fCompl,int fVerbose)4646 Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose )
4647 {
4648 Abc_Ntk_t * pNtkAig;
4649 Aig_Man_t * pMan, * pTemp;
4650 assert( Abc_NtkIsStrash(pNtk) );
4651 pMan = Abc_NtkToDar( pNtk, 0, 1 );
4652 if ( pMan == NULL )
4653 return NULL;
4654 pMan = Saig_ManDupFoldConstrsFunc( pTemp = pMan, fCompl, fVerbose );
4655 Aig_ManStop( pTemp );
4656 pNtkAig = Abc_NtkFromAigPhase( pMan );
4657 pNtkAig->pName = Extra_UtilStrsav(pMan->pName);
4658 pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec);
4659 Aig_ManStop( pMan );
4660 return pNtkAig;
4661 }
4662
4663 /**Function*************************************************************
4664
4665 Synopsis [Performs BDD-based reachability analysis.]
4666
4667 Description []
4668
4669 SideEffects []
4670
4671 SeeAlso []
4672
4673 ***********************************************************************/
Abc_NtkDarConstrProfile(Abc_Ntk_t * pNtk,int fVerbose)4674 void Abc_NtkDarConstrProfile( Abc_Ntk_t * pNtk, int fVerbose )
4675 {
4676 extern int Ssw_ManProfileConstraints( Aig_Man_t * p, int nWords, int nFrames, int fVerbose );
4677 extern Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, int fProbOne );
4678 Aig_Man_t * pMan;
4679 // Vec_Int_t * vProbOne;
4680 // Aig_Obj_t * pObj;
4681 // int i, Entry;
4682 assert( Abc_NtkIsStrash(pNtk) );
4683 assert( Abc_NtkConstrNum(pNtk) );
4684 pMan = Abc_NtkToDar( pNtk, 0, 1 );
4685 if ( pMan == NULL )
4686 return;
4687 // value in the init state
4688 // Abc_AigSetNodePhases( pNtk );
4689 /*
4690 // derive probabilities
4691 vProbOne = Saig_ManComputeSwitchProbs( pMan, 48, 16, 1 );
4692 // iterate over the constraint outputs
4693 Saig_ManForEachPo( pMan, pObj, i )
4694 {
4695 Entry = Vec_IntEntry( vProbOne, Aig_ObjId(pObj) );
4696 if ( i < Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan) )
4697 Abc_Print( 1, "Primary output : ", i );
4698 else
4699 Abc_Print( 1, "Constraint %3d : ", i-(Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan)) );
4700 Abc_Print( 1, "ProbOne = %f ", Abc_Int2Float(Entry) );
4701 Abc_Print( 1, "AllZeroValue = %d ", Aig_ObjPhase(pObj) );
4702 Abc_Print( 1, "\n" );
4703 }
4704 */
4705 // double-check
4706 Ssw_ManProfileConstraints( pMan, 16, 64, 1 );
4707 Abc_Print( 1, "TwoFrameSatValue = %d.\n", Ssw_ManSetConstrPhases(pMan, 2, NULL) );
4708 // clean up
4709 // Vec_IntFree( vProbOne );
4710 Aig_ManStop( pMan );
4711 }
4712
4713 /**Function*************************************************************
4714
4715 Synopsis [Performs BDD-based reachability analysis.]
4716
4717 Description []
4718
4719 SideEffects []
4720
4721 SeeAlso []
4722
4723 ***********************************************************************/
Abc_NtkDarTest(Abc_Ntk_t * pNtk,int Num)4724 void Abc_NtkDarTest( Abc_Ntk_t * pNtk, int Num )
4725 {
4726 // extern void Saig_ManDetectConstr( Aig_Man_t * p );
4727 // extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p );
4728 // extern void Saig_ManFoldConstrTest( Aig_Man_t * pAig );
4729 extern void Llb_ManComputeDomsTest( Aig_Man_t * pAig, int Num );
4730
4731
4732
4733 // extern void Fsim_ManTest( Aig_Man_t * pAig );
4734 extern Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose, Aig_Man_t ** ppMiter );
4735 // Vec_Int_t * vPairs;
4736 Aig_Man_t * pMan;//, * pMan2;//, * pTemp;
4737 assert( Abc_NtkIsStrash(pNtk) );
4738 pMan = Abc_NtkToDar( pNtk, 0, 1 );
4739 if ( pMan == NULL )
4740 return;
4741 /*
4742 Aig_ManSetRegNum( pMan, pMan->nRegs );
4743 Aig_ManPrintStats( pMan );
4744 Saig_ManDumpBlif( pMan, "_temp_.blif" );
4745 Aig_ManStop( pMan );
4746 pMan = Saig_ManReadBlif( "_temp_.blif" );
4747 Aig_ManPrintStats( pMan );
4748 */
4749 /*
4750 Aig_ManSetRegNum( pMan, pMan->nRegs );
4751 pTemp = Ssw_SignalCorrespondeceTestPairs( pMan );
4752 Aig_ManStop( pTemp );
4753 */
4754
4755 /*
4756 // Ssw_SecSpecialMiter( pMan, NULL, 2, 1 );
4757 pMan2 = Aig_ManDupSimple(pMan);
4758 vPairs = Saig_StrSimPerformMatching( pMan, pMan2, 0, 1, NULL );
4759 Vec_IntFree( vPairs );
4760 Aig_ManStop( pMan );
4761 Aig_ManStop( pMan2 );
4762 */
4763 // Ioa_WriteAigerBufferTest( pMan, "test.aig", 0, 0 );
4764 // Saig_ManFoldConstrTest( pMan );
4765 {
4766 extern void Saig_ManBmcSectionsTest( Aig_Man_t * p );
4767 extern void Saig_ManBmcTerSimTest( Aig_Man_t * p );
4768 extern void Saig_ManBmcSupergateTest( Aig_Man_t * p );
4769 extern void Saig_ManBmcMappingTest( Aig_Man_t * p );
4770 // Saig_ManBmcSectionsTest( pMan );
4771 // Saig_ManBmcTerSimTest( pMan );
4772 // Saig_ManBmcSupergateTest( pMan );
4773 // Saig_ManBmcMappingTest( pMan );
4774 }
4775
4776 {
4777 // void Pdr_ManEquivClasses( Aig_Man_t * pMan );
4778 // Pdr_ManEquivClasses( pMan );
4779 }
4780
4781 // Llb_ManComputeDomsTest( pMan, Num );
4782 {
4783 extern void Llb_ManMinCutTest( Aig_Man_t * pMan, int Num );
4784 extern void Llb_BddStructAnalysis( Aig_Man_t * pMan );
4785 extern void Llb_NonlinExperiment( Aig_Man_t * pAig, int Num );
4786 // Llb_BddStructAnalysis( pMan );
4787 // Llb_ManMinCutTest( pMan, Num );
4788 // Llb_NonlinExperiment( pMan, Num );
4789 }
4790
4791 // Saig_MvManSimulate( pMan, 1 );
4792 // Saig_ManDetectConstr( pMan );
4793 // Saig_ManDetectConstrFuncTest( pMan );
4794
4795 // Fsim_ManTest( pMan );
4796 Aig_ManStop( pMan );
4797
4798 }
4799
4800 /**Function*************************************************************
4801
4802 Synopsis [Performs BDD-based reachability analysis.]
4803
4804 Description []
4805
4806 SideEffects []
4807
4808 SeeAlso []
4809
4810 ***********************************************************************/
Abc_NtkDarTestNtk(Abc_Ntk_t * pNtk)4811 Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
4812 {
4813 // extern Aig_Man_t * Saig_ManDualRail( Aig_Man_t * p, int fMiter );
4814
4815 /*
4816 extern Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig );
4817
4818 Abc_Ntk_t * pNtkAig;
4819 Aig_Man_t * pMan, * pTemp;
4820 assert( Abc_NtkIsStrash(pNtk) );
4821 pMan = Abc_NtkToDar( pNtk, 0, 1 );
4822 if ( pMan == NULL )
4823 return NULL;
4824
4825 Aig_ManSetRegNum( pMan, pMan->nRegs );
4826 pMan = Ssw_SignalCorrespondeceTestPairs( pTemp = pMan );
4827 Aig_ManStop( pTemp );
4828 if ( pMan == NULL )
4829 return NULL;
4830
4831 pNtkAig = Abc_NtkFromAigPhase( pMan );
4832 pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
4833 pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
4834 Aig_ManStop( pMan );
4835 return pNtkAig;
4836 */
4837 Abc_Ntk_t * pNtkAig;
4838 Aig_Man_t * pMan;//, * pTemp;
4839 assert( Abc_NtkIsStrash(pNtk) );
4840 pMan = Abc_NtkToDar( pNtk, 0, 1 );
4841 if ( pMan == NULL )
4842 return NULL;
4843
4844 /*
4845 Aig_ManSetRegNum( pMan, pMan->nRegs );
4846 pMan = Saig_ManDualRail( pTemp = pMan, 1 );
4847 Aig_ManStop( pTemp );
4848 if ( pMan == NULL )
4849 return NULL;
4850
4851 pNtkAig = Abc_NtkFromAigPhase( pMan );
4852 pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
4853 pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
4854 Aig_ManStop( pMan );
4855 */
4856
4857 pNtkAig = Abc_NtkFromDar( pNtk, pMan );
4858 Aig_ManStop( pMan );
4859
4860 return pNtkAig;
4861
4862 }
4863
4864 ////////////////////////////////////////////////////////////////////////
4865 /// END OF FILE ///
4866 ////////////////////////////////////////////////////////////////////////
4867
4868 #include "abcDarUnfold2.c"
4869 ABC_NAMESPACE_IMPL_END
4870
4871