1 /**CFile****************************************************************
2
3 FileName [arenaViolation.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Liveness property checking.]
8
9 Synopsis [module for addition of arena violator detector
10 induced by stabilizing constraints]
11
12 Author [Sayak Ray]
13
14 Affiliation [UC Berkeley]
15
16 Date [Ver. 1.0. Started - October 31, 2012.]
17
18 ***********************************************************************/
19
20 #include <stdio.h>
21 #include "base/main/main.h"
22 #include "aig/aig/aig.h"
23 #include "aig/saig/saig.h"
24 #include <string.h>
25 #include "base/main/mainInt.h"
26 #include "proof/pdr/pdr.h"
27
28 //#define DISJUNCTIVE_CONSTRAINT_ENABLE_MODE
29 #define BARRIER_MONOTONE_TEST
30
31 ABC_NAMESPACE_IMPL_START
32
createArenaLO(Aig_Man_t * pAigNew,Vec_Ptr_t * vBarriers)33 Vec_Ptr_t * createArenaLO( Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers )
34 {
35 Vec_Ptr_t *vArenaLO;
36 int barrierCount;
37 Aig_Obj_t *pObj;
38 int i;
39
40 if( vBarriers == NULL )
41 return NULL;
42
43 barrierCount = Vec_PtrSize(vBarriers);
44 if( barrierCount <= 0 )
45 return NULL;
46
47 vArenaLO = Vec_PtrAlloc(barrierCount);
48 for( i=0; i<barrierCount; i++ )
49 {
50 pObj = Aig_ObjCreateCi( pAigNew );
51 Vec_PtrPush( vArenaLO, pObj );
52 }
53
54 return vArenaLO;
55 }
56
createArenaLi(Aig_Man_t * pAigNew,Vec_Ptr_t * vBarriers,Vec_Ptr_t * vArenaSignal)57 Vec_Ptr_t * createArenaLi( Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers, Vec_Ptr_t *vArenaSignal )
58 {
59 Vec_Ptr_t *vArenaLi;
60 int barrierCount;
61 int i;
62 Aig_Obj_t *pObj, *pObjDriver;
63
64 if( vBarriers == NULL )
65 return NULL;
66
67 barrierCount = Vec_PtrSize(vBarriers);
68 if( barrierCount <= 0 )
69 return NULL;
70
71 vArenaLi = Vec_PtrAlloc(barrierCount);
72 for( i=0; i<barrierCount; i++ )
73 {
74 pObjDriver = (Aig_Obj_t *)Vec_PtrEntry( vArenaSignal, i );
75 pObj = Aig_ObjCreateCo( pAigNew, pObjDriver );
76 Vec_PtrPush( vArenaLi, pObj );
77 }
78
79 return vArenaLi;
80 }
81
createMonotoneBarrierLO(Aig_Man_t * pAigNew,Vec_Ptr_t * vBarriers)82 Vec_Ptr_t *createMonotoneBarrierLO( Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers )
83 {
84 Vec_Ptr_t *vMonotoneLO;
85 int barrierCount;
86 Aig_Obj_t *pObj;
87 int i;
88
89 if( vBarriers == NULL )
90 return NULL;
91
92 barrierCount = Vec_PtrSize(vBarriers);
93 if( barrierCount <= 0 )
94 return NULL;
95
96 vMonotoneLO = Vec_PtrAlloc(barrierCount);
97 for( i=0; i<barrierCount; i++ )
98 {
99 pObj = Aig_ObjCreateCi( pAigNew );
100 Vec_PtrPush( vMonotoneLO, pObj );
101 }
102
103 return vMonotoneLO;
104 }
105
driverToPoNew(Aig_Man_t * pAig,Aig_Obj_t * pObjPo)106 Aig_Obj_t *driverToPoNew( Aig_Man_t *pAig, Aig_Obj_t *pObjPo )
107 {
108 Aig_Obj_t *poDriverOld;
109 Aig_Obj_t *poDriverNew;
110
111 //Aig_ObjPrint( pAig, pObjPo );
112 //printf("\n");
113
114 assert( Aig_ObjIsCo(pObjPo) );
115 poDriverOld = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObjPo), Aig_ObjFaninC0(pObjPo));
116 assert( !Aig_ObjIsCo(poDriverOld) );
117 poDriverNew = !Aig_IsComplement(poDriverOld)?
118 (Aig_Obj_t *)(Aig_Regular(poDriverOld)->pData) :
119 Aig_Not((Aig_Obj_t *)(Aig_Regular(poDriverOld)->pData));
120 //assert( !Aig_ObjIsCo(poDriverNew) );
121 return poDriverNew;
122 }
123
collectBarrierDisjunctions(Aig_Man_t * pAigOld,Aig_Man_t * pAigNew,Vec_Ptr_t * vBarriers)124 Vec_Ptr_t *collectBarrierDisjunctions(Aig_Man_t *pAigOld, Aig_Man_t *pAigNew, Vec_Ptr_t *vBarriers)
125 {
126 int barrierCount, i, j, jElem;
127 Vec_Int_t *vIthBarrier;
128 Aig_Obj_t *pObjBarrier, *pObjCurr, *pObjTargetPoOld;
129 Vec_Ptr_t *vNewBarrierSignals;
130
131 if( vBarriers == NULL )
132 return NULL;
133 barrierCount = Vec_PtrSize( vBarriers );
134 if( barrierCount <= 0 )
135 return NULL;
136
137 vNewBarrierSignals = Vec_PtrAlloc( barrierCount );
138
139 for( i=0; i<barrierCount; i++ )
140 {
141 vIthBarrier = (Vec_Int_t *)Vec_PtrEntry( vBarriers, i );
142 assert( Vec_IntSize( vIthBarrier ) >= 1 );
143 pObjBarrier = Aig_Not(Aig_ManConst1(pAigNew));
144 Vec_IntForEachEntry( vIthBarrier, jElem, j )
145 {
146 pObjTargetPoOld = Aig_ManCo( pAigOld, jElem );
147 //Aig_ObjPrint( pAigOld, pObjTargetPoOld );
148 //printf("\n");
149 pObjCurr = driverToPoNew( pAigOld, pObjTargetPoOld );
150 pObjBarrier = Aig_Or( pAigNew, pObjCurr, pObjBarrier );
151 }
152 assert( pObjBarrier );
153 Vec_PtrPush(vNewBarrierSignals, pObjBarrier);
154 }
155 assert( Vec_PtrSize( vNewBarrierSignals ) == barrierCount );
156
157 return vNewBarrierSignals;
158 }
159
Aig_Xor(Aig_Man_t * pAig,Aig_Obj_t * pObj1,Aig_Obj_t * pObj2)160 Aig_Obj_t *Aig_Xor( Aig_Man_t *pAig, Aig_Obj_t *pObj1, Aig_Obj_t *pObj2 )
161 {
162 return Aig_Or( pAig, Aig_And( pAig, pObj1, Aig_Not(pObj2) ), Aig_And( pAig, Aig_Not(pObj1), pObj2 ) );
163 }
164
createArenaViolation(Aig_Man_t * pAigOld,Aig_Man_t * pAigNew,Aig_Obj_t * pWindowBegins,Aig_Obj_t * pWithinWindow,Vec_Ptr_t * vMasterBarriers,Vec_Ptr_t * vBarrierLo,Vec_Ptr_t * vBarrierLiDriver,Vec_Ptr_t * vMonotoneDisjunctionNodes)165 Aig_Obj_t *createArenaViolation(
166 Aig_Man_t *pAigOld,
167 Aig_Man_t *pAigNew,
168 Aig_Obj_t *pWindowBegins,
169 Aig_Obj_t *pWithinWindow,
170 Vec_Ptr_t *vMasterBarriers,
171 Vec_Ptr_t *vBarrierLo,
172 Vec_Ptr_t *vBarrierLiDriver,
173 Vec_Ptr_t *vMonotoneDisjunctionNodes
174 )
175 {
176 Aig_Obj_t *pWindowBeginsLocal = pWindowBegins;
177 Aig_Obj_t *pWithinWindowLocal = pWithinWindow;
178 int i;
179 Aig_Obj_t *pObj, *pObjAnd1, *pObjOr1, *pObjAnd2, *pObjBarrierLo, *pObjBarrierSwitch, *pObjArenaViolation;
180 Vec_Ptr_t *vBarrierSignals;
181
182 assert( vBarrierLiDriver != NULL );
183 assert( vMonotoneDisjunctionNodes != NULL );
184
185 pObjArenaViolation = Aig_Not(Aig_ManConst1( pAigNew ));
186
187 vBarrierSignals = collectBarrierDisjunctions(pAigOld, pAigNew, vMasterBarriers);
188 assert( vBarrierSignals != NULL );
189
190 assert( Vec_PtrSize( vMonotoneDisjunctionNodes ) == 0 );
191 Vec_PtrForEachEntry( Aig_Obj_t *, vBarrierSignals, pObj, i )
192 Vec_PtrPush( vMonotoneDisjunctionNodes, pObj );
193 assert( Vec_PtrSize( vMonotoneDisjunctionNodes ) == Vec_PtrSize( vMasterBarriers ) );
194
195 Vec_PtrForEachEntry( Aig_Obj_t *, vBarrierSignals, pObj, i )
196 {
197 //pObjNew = driverToPoNew( pAigOld, pObj );
198 pObjAnd1 = Aig_And(pAigNew, pObj, pWindowBeginsLocal);
199 pObjBarrierLo = (Aig_Obj_t *)Vec_PtrEntry( vBarrierLo, i );
200 pObjOr1 = Aig_Or(pAigNew, pObjAnd1, pObjBarrierLo);
201 Vec_PtrPush( vBarrierLiDriver, pObjOr1 );
202
203 pObjBarrierSwitch = Aig_Xor( pAigNew, pObj, pObjBarrierLo );
204 pObjAnd2 = Aig_And( pAigNew, pObjBarrierSwitch, pWithinWindowLocal );
205 pObjArenaViolation = Aig_Or( pAigNew, pObjAnd2, pObjArenaViolation );
206 }
207
208 Vec_PtrFree(vBarrierSignals);
209 return pObjArenaViolation;
210 }
211
createConstrained0LiveConeWithDSC(Aig_Man_t * pNewAig,Vec_Ptr_t * signalList)212 Aig_Obj_t *createConstrained0LiveConeWithDSC( Aig_Man_t *pNewAig, Vec_Ptr_t *signalList )
213 {
214 Aig_Obj_t *pConsequent, *pConsequentCopy, *pAntecedent, *p0LiveCone, *pObj;
215 int i, numSigAntecedent;
216
217 numSigAntecedent = Vec_PtrSize( signalList ) - 1;
218
219 pAntecedent = Aig_ManConst1( pNewAig );
220 pConsequent = (Aig_Obj_t *)Vec_PtrEntry( signalList, numSigAntecedent );
221 pConsequentCopy = Aig_NotCond( (Aig_Obj_t *)(Aig_Regular(pConsequent)->pData), Aig_IsComplement( pConsequent ) );
222
223 for(i=0; i<numSigAntecedent; i++ )
224 {
225 pObj = (Aig_Obj_t *)Vec_PtrEntry( signalList, i );
226 assert( Aig_Regular(pObj)->pData );
227 pAntecedent = Aig_And( pNewAig, pAntecedent, Aig_NotCond((Aig_Obj_t *)(Aig_Regular(pObj)->pData), Aig_IsComplement(pObj)) );
228 }
229
230 p0LiveCone = Aig_Or( pNewAig, Aig_Not(pAntecedent), pConsequentCopy );
231
232 return p0LiveCone;
233 }
234
collectCSSignalsWithDSC(Abc_Ntk_t * pNtk,Aig_Man_t * pAig)235 Vec_Ptr_t *collectCSSignalsWithDSC( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
236 {
237 int i;
238 Aig_Obj_t *pObj, *pConsequent = NULL;
239 Vec_Ptr_t *vNodeArray;
240
241 vNodeArray = Vec_PtrAlloc(1);
242
243 Saig_ManForEachPo( pAig, pObj, i )
244 {
245 if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "csLiveConst_" ) != NULL )
246 Vec_PtrPush( vNodeArray, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj)) );
247 else if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "csLiveTarget_" ) != NULL )
248 pConsequent = Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj));
249 }
250 assert( pConsequent );
251 Vec_PtrPush( vNodeArray, pConsequent );
252 return vNodeArray;
253 }
254
collectWindowBeginSignalWithDSC(Abc_Ntk_t * pNtk,Aig_Man_t * pAig)255 int collectWindowBeginSignalWithDSC( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
256 {
257 int i;
258 Aig_Obj_t *pObj;
259
260 Saig_ManForEachPo( pAig, pObj, i )
261 {
262 if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "windowBegins_" ) != NULL )
263 {
264 return i;
265 }
266 }
267
268 return -1;
269 }
270
collectWithinWindowSignalWithDSC(Abc_Ntk_t * pNtk,Aig_Man_t * pAig)271 int collectWithinWindowSignalWithDSC( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
272 {
273 int i;
274 Aig_Obj_t *pObj;
275
276 Saig_ManForEachPo( pAig, pObj, i )
277 {
278 if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "withinWindow_" ) != NULL )
279 return i;
280 }
281
282 return -1;
283 }
284
collectPendingSignalWithDSC(Abc_Ntk_t * pNtk,Aig_Man_t * pAig)285 int collectPendingSignalWithDSC( Abc_Ntk_t *pNtk, Aig_Man_t *pAig )
286 {
287 int i;
288 Aig_Obj_t *pObj;
289
290 Saig_ManForEachPo( pAig, pObj, i )
291 {
292 if( strstr( Abc_ObjName(Abc_NtkPo( pNtk, i )), "pendingSignal" ) != NULL )
293 return i;
294 }
295
296 return -1;
297 }
298
createAndGateForMonotonicityVerification(Aig_Man_t * pNewAig,Vec_Ptr_t * vDisjunctionSignals,Vec_Ptr_t * vDisjunctionLo,Aig_Obj_t * pendingLo,Aig_Obj_t * pendingSignal)299 Aig_Obj_t *createAndGateForMonotonicityVerification(
300 Aig_Man_t *pNewAig,
301 Vec_Ptr_t *vDisjunctionSignals,
302 Vec_Ptr_t *vDisjunctionLo,
303 Aig_Obj_t *pendingLo,
304 Aig_Obj_t *pendingSignal
305 )
306 {
307 Aig_Obj_t *pObjBigAnd, *pObj, *pObjLo, *pObjImply;
308 Aig_Obj_t *pObjPendingAndPendingLo;
309 int i;
310
311 pObjBigAnd = Aig_ManConst1( pNewAig );
312 pObjPendingAndPendingLo = Aig_And( pNewAig, pendingLo, pendingSignal );
313 Vec_PtrForEachEntry( Aig_Obj_t *, vDisjunctionSignals, pObj, i )
314 {
315 pObjLo = (Aig_Obj_t *)Vec_PtrEntry( vDisjunctionLo, i );
316 pObjImply = Aig_Or( pNewAig, Aig_Not(Aig_And( pNewAig, pObjPendingAndPendingLo, pObjLo)),
317 pObj );
318 pObjBigAnd = Aig_And( pNewAig, pObjBigAnd, pObjImply );
319 }
320 return pObjBigAnd;
321 }
322
createNewAigWith0LivePoWithDSC(Aig_Man_t * pAig,Vec_Ptr_t * signalList,int * index0Live,int windowBeginIndex,int withinWindowIndex,int pendingSignalIndex,Vec_Ptr_t * vBarriers)323 Aig_Man_t *createNewAigWith0LivePoWithDSC( Aig_Man_t *pAig, Vec_Ptr_t *signalList, int *index0Live, int windowBeginIndex, int withinWindowIndex, int pendingSignalIndex, Vec_Ptr_t *vBarriers )
324 {
325 Aig_Man_t *pNewAig;
326 Aig_Obj_t *pObj, *pObjNewPoDriver;
327 int i;
328 int loCopied = 0, loCreated = 0, liCopied = 0, liCreated = 0;
329 Aig_Obj_t *pObjWindowBeginsNew, *pObjWithinWindowNew, *pObjArenaViolation, *pObjTarget, *pObjArenaViolationLiDriver;
330 Aig_Obj_t *pObjNewPoDriverArenaViolated, *pObjArenaViolationLo;
331 Vec_Ptr_t *vBarrierLo, *vBarrierLiDriver, *vBarrierLi;
332 Vec_Ptr_t *vMonotoneNodes;
333
334 #ifdef BARRIER_MONOTONE_TEST
335 Aig_Obj_t *pObjPendingSignal;
336 Aig_Obj_t *pObjPendingFlopLo;
337 Vec_Ptr_t *vMonotoneBarrierLo;
338 Aig_Obj_t *pObjPendingAndPendingSignal, *pObjMonotoneAnd, *pObjCurrMonotoneLo;
339 #endif
340
341 //assert( Vec_PtrSize( signalList ) > 1 );
342
343 //****************************************************************
344 // Step1: create the new manager
345 // Note: The new manager is created with "2 * Aig_ManObjNumMax(p)"
346 // nodes, but this selection is arbitrary - need to be justified
347 //****************************************************************
348 pNewAig = Aig_ManStart( Aig_ManObjNumMax(pAig) );
349 pNewAig->pName = (char *)malloc( strlen( pAig->pName ) + strlen("_0Live") + 1 );
350 sprintf(pNewAig->pName, "%s_%s", pAig->pName, "0Live");
351 pNewAig->pSpec = NULL;
352
353 //****************************************************************
354 // Step 2: map constant nodes
355 //****************************************************************
356 pObj = Aig_ManConst1( pAig );
357 pObj->pData = Aig_ManConst1( pNewAig );
358
359 //****************************************************************
360 // Step 3: create true PIs
361 //****************************************************************
362 Saig_ManForEachPi( pAig, pObj, i )
363 {
364 pObj->pData = Aig_ObjCreateCi( pNewAig );
365 }
366
367 //****************************************************************
368 // Step 4: create register outputs
369 //****************************************************************
370 Saig_ManForEachLo( pAig, pObj, i )
371 {
372 loCopied++;
373 pObj->pData = Aig_ObjCreateCi( pNewAig );
374 }
375
376 //****************************************************************
377 // Step 4.a: create register outputs for the barrier flops
378 //****************************************************************
379 vBarrierLo = createArenaLO( pNewAig, vBarriers );
380 loCreated = Vec_PtrSize(vBarrierLo);
381
382 //****************************************************************
383 // Step 4.b: create register output for arenaViolationFlop
384 //****************************************************************
385 pObjArenaViolationLo = Aig_ObjCreateCi( pNewAig );
386 loCreated++;
387
388 #ifdef BARRIER_MONOTONE_TEST
389 //****************************************************************
390 // Step 4.c: create register output for pendingFlop
391 //****************************************************************
392 pObjPendingFlopLo = Aig_ObjCreateCi( pNewAig );
393 loCreated++;
394
395 //****************************************************************
396 // Step 4.d: create register outputs for the barrier flops
397 // for asserting monotonicity
398 //****************************************************************
399 vMonotoneBarrierLo = createMonotoneBarrierLO( pNewAig, vBarriers );
400 loCreated = loCreated + Vec_PtrSize(vMonotoneBarrierLo);
401 #endif
402
403 //********************************************************************
404 // Step 5: create internal nodes
405 //********************************************************************
406 Aig_ManForEachNode( pAig, pObj, i )
407 {
408 pObj->pData = Aig_And( pNewAig, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
409 }
410
411 //********************************************************************
412 // Step 5.a: create internal nodes corresponding to arenaViolation
413 //********************************************************************
414 pObjTarget = Aig_ManCo( pAig, windowBeginIndex );
415 pObjWindowBeginsNew = driverToPoNew( pAig, pObjTarget );
416
417 pObjTarget = Aig_ManCo( pAig, withinWindowIndex );
418 pObjWithinWindowNew = driverToPoNew( pAig, pObjTarget );
419
420 vBarrierLiDriver = Vec_PtrAlloc( Vec_PtrSize(vBarriers) );
421 vMonotoneNodes = Vec_PtrAlloc( Vec_PtrSize(vBarriers) );
422
423 pObjArenaViolation = createArenaViolation( pAig, pNewAig,
424 pObjWindowBeginsNew, pObjWithinWindowNew,
425 vBarriers, vBarrierLo, vBarrierLiDriver, vMonotoneNodes );
426 assert( Vec_PtrSize(vMonotoneNodes) == Vec_PtrSize(vBarriers) );
427
428 #ifdef ARENA_VIOLATION_CONSTRAINT
429
430 #endif
431
432 pObjArenaViolationLiDriver = Aig_Or( pNewAig, pObjArenaViolation, pObjArenaViolationLo );
433
434 #ifdef BARRIER_MONOTONE_TEST
435 //********************************************************************
436 // Step 5.b: Create internal nodes for monotone testing
437 //********************************************************************
438
439 pObjTarget = Aig_ManCo( pAig, pendingSignalIndex );
440 pObjPendingSignal = driverToPoNew( pAig, pObjTarget );
441
442 pObjPendingAndPendingSignal = Aig_And( pNewAig, pObjPendingSignal, pObjPendingFlopLo );
443 pObjMonotoneAnd = Aig_ManConst1( pNewAig );
444 Vec_PtrForEachEntry( Aig_Obj_t *, vMonotoneNodes, pObj, i )
445 {
446 pObjCurrMonotoneLo = (Aig_Obj_t *)Vec_PtrEntry(vMonotoneBarrierLo, i);
447 pObjMonotoneAnd = Aig_And( pNewAig, pObjMonotoneAnd,
448 Aig_Or( pNewAig,
449 Aig_Not(Aig_And(pNewAig, pObjPendingAndPendingSignal, pObjCurrMonotoneLo)),
450 pObj ) );
451 }
452 #endif
453
454 //********************************************************************
455 // Step 6: create primary outputs
456 //********************************************************************
457
458 Saig_ManForEachPo( pAig, pObj, i )
459 {
460 pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
461 }
462
463 pObjNewPoDriver = createConstrained0LiveConeWithDSC( pNewAig, signalList );
464 pObjNewPoDriverArenaViolated = Aig_Or( pNewAig, pObjNewPoDriver, pObjArenaViolationLo );
465 #ifdef BARRIER_MONOTONE_TEST
466 pObjNewPoDriverArenaViolated = Aig_And( pNewAig, pObjNewPoDriverArenaViolated, pObjMonotoneAnd );
467 #endif
468 Aig_ObjCreateCo( pNewAig, pObjNewPoDriverArenaViolated );
469
470 *index0Live = i;
471
472 //********************************************************************
473 // Step 7: create register inputs
474 //********************************************************************
475
476 Saig_ManForEachLi( pAig, pObj, i )
477 {
478 liCopied++;
479 pObj->pData = Aig_ObjCreateCo( pNewAig, Aig_ObjChild0Copy(pObj) );
480 }
481
482 //********************************************************************
483 // Step 7.a: create register inputs for barrier flops
484 //********************************************************************
485 assert( Vec_PtrSize(vBarrierLiDriver) == Vec_PtrSize(vBarriers) );
486 vBarrierLi = createArenaLi( pNewAig, vBarriers, vBarrierLiDriver );
487 liCreated = Vec_PtrSize( vBarrierLi );
488
489 //********************************************************************
490 // Step 7.b: create register inputs for arenaViolation flop
491 //********************************************************************
492 Aig_ObjCreateCo( pNewAig, pObjArenaViolationLiDriver );
493 liCreated++;
494
495 #ifdef BARRIER_MONOTONE_TEST
496 //****************************************************************
497 // Step 7.c: create register input for pendingFlop
498 //****************************************************************
499 Aig_ObjCreateCo( pNewAig, pObjPendingSignal);
500 liCreated++;
501
502 //********************************************************************
503 // Step 7.d: create register inputs for the barrier flops
504 // for asserting monotonicity
505 //********************************************************************
506 Vec_PtrForEachEntry( Aig_Obj_t *, vMonotoneNodes, pObj, i )
507 {
508 Aig_ObjCreateCo( pNewAig, pObj );
509 liCreated++;
510 }
511 #endif
512
513 assert(loCopied + loCreated == liCopied + liCreated);
514 //next step should be changed
515 Aig_ManSetRegNum( pNewAig, loCopied + loCreated );
516 Aig_ManCleanup( pNewAig );
517
518 assert( Aig_ManCheck( pNewAig ) );
519
520 Vec_PtrFree(vBarrierLo);
521 Vec_PtrFree(vMonotoneBarrierLo);
522 Vec_PtrFree(vBarrierLiDriver);
523 Vec_PtrFree(vBarrierLi);
524 Vec_PtrFree(vMonotoneNodes);
525
526 return pNewAig;
527 }
528
generateWorkingAigWithDSC(Aig_Man_t * pAig,Abc_Ntk_t * pNtk,int * pIndex0Live,Vec_Ptr_t * vMasterBarriers)529 Aig_Man_t *generateWorkingAigWithDSC( Aig_Man_t *pAig, Abc_Ntk_t *pNtk, int *pIndex0Live, Vec_Ptr_t *vMasterBarriers )
530 {
531 Vec_Ptr_t *vSignalVector;
532 Aig_Man_t *pAigNew;
533 int pObjWithinWindow;
534 int pObjWindowBegin;
535 int pObjPendingSignal;
536
537 vSignalVector = collectCSSignalsWithDSC( pNtk, pAig );
538
539 pObjWindowBegin = collectWindowBeginSignalWithDSC( pNtk, pAig );
540 pObjWithinWindow = collectWithinWindowSignalWithDSC( pNtk, pAig );
541 pObjPendingSignal = collectPendingSignalWithDSC( pNtk, pAig );
542
543 pAigNew = createNewAigWith0LivePoWithDSC( pAig, vSignalVector, pIndex0Live, pObjWindowBegin, pObjWithinWindow, pObjPendingSignal, vMasterBarriers );
544 Vec_PtrFree(vSignalVector);
545
546 return pAigNew;
547 }
548
549 ABC_NAMESPACE_IMPL_END
550