1 /**CFile****************************************************************
2
3 FileName [saigConstr.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Sequential AIG package.]
8
9 Synopsis [Structural constraint detection.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: saigConstr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "saig.h"
22 #include "sat/cnf/cnf.h"
23 #include "sat/bsat/satSolver.h"
24 #include "bool/kit/kit.h"
25 #include "aig/ioa/ioa.h"
26
27 ABC_NAMESPACE_IMPL_START
28
29 /*
30 Property holds iff it is const 0.
31 Constraint holds iff it is const 0.
32
33 The following structure is used for folding constraints:
34 - the output of OR gate is 0 as long as all constraints hold
35 - as soon as one constraint fail, the property output becomes 0 forever
36 because the flop becomes 1 and it stays 1 forever
37
38
39 property output
40
41 |
42 |-----|
43 | and |
44 |-----|
45 | |
46 | / \
47 | /inv\
48 | -----
49 ____| |_________________________
50 | | |
51 / \ ----------- |
52 / \ | or | |
53 / \ ----------- |
54 / logic \ | | | |
55 / cone \ | | | |
56 /___________\ | | | |
57 | | ------ |
58 | | |flop| (init=0) |
59 | | ------ |
60 | | | |
61 | | |______________|
62 | |
63 c1 c2
64 */
65
66 ////////////////////////////////////////////////////////////////////////
67 /// DECLARATIONS ///
68 ////////////////////////////////////////////////////////////////////////
69
70 ////////////////////////////////////////////////////////////////////////
71 /// FUNCTION DEFINITIONS ///
72 ////////////////////////////////////////////////////////////////////////
73
74 /**Function*************************************************************
75
76 Synopsis [Collects the supergate.]
77
78 Description []
79
80 SideEffects []
81
82 SeeAlso []
83
84 ***********************************************************************/
Saig_DetectConstrCollectSuper_rec(Aig_Obj_t * pObj,Vec_Ptr_t * vSuper)85 void Saig_DetectConstrCollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
86 {
87 // if the new node is complemented or a PI, another gate begins
88 if ( Aig_IsComplement(pObj) || !Aig_ObjIsNode(pObj) )//|| (Aig_ObjRefs(pObj) > 1) )
89 {
90 Vec_PtrPushUnique( vSuper, Aig_Not(pObj) );
91 return;
92 }
93 // go through the branches
94 Saig_DetectConstrCollectSuper_rec( Aig_ObjChild0(pObj), vSuper );
95 Saig_DetectConstrCollectSuper_rec( Aig_ObjChild1(pObj), vSuper );
96 }
97
98 /**Function*************************************************************
99
100 Synopsis [Collects the supergate.]
101
102 Description []
103
104 SideEffects []
105
106 SeeAlso []
107
108 ***********************************************************************/
Saig_DetectConstrCollectSuper(Aig_Obj_t * pObj)109 Vec_Ptr_t * Saig_DetectConstrCollectSuper( Aig_Obj_t * pObj )
110 {
111 Vec_Ptr_t * vSuper;
112 assert( !Aig_IsComplement(pObj) );
113 assert( Aig_ObjIsAnd(pObj) );
114 vSuper = Vec_PtrAlloc( 4 );
115 Saig_DetectConstrCollectSuper_rec( Aig_ObjChild0(pObj), vSuper );
116 Saig_DetectConstrCollectSuper_rec( Aig_ObjChild1(pObj), vSuper );
117 return vSuper;
118 }
119
120 /**Function*************************************************************
121
122 Synopsis [Returns NULL if not contained, or array with unique entries.]
123
124 Description [Returns NULL if vSuper2 is not contained in vSuper. Otherwise
125 returns the array of entries in vSuper that are not found in vSuper2.]
126
127 SideEffects []
128
129 SeeAlso []
130
131 ***********************************************************************/
Saig_ManDetectConstrCheckCont(Vec_Ptr_t * vSuper,Vec_Ptr_t * vSuper2)132 Vec_Ptr_t * Saig_ManDetectConstrCheckCont( Vec_Ptr_t * vSuper, Vec_Ptr_t * vSuper2 )
133 {
134 Vec_Ptr_t * vUnique;
135 Aig_Obj_t * pObj, * pObj2;
136 int i;
137 Vec_PtrForEachEntry( Aig_Obj_t *, vSuper2, pObj2, i )
138 if ( Vec_PtrFind( vSuper, pObj2 ) == -1 )
139 return 0;
140 vUnique = Vec_PtrAlloc( 100 );
141 Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pObj, i )
142 if ( Vec_PtrFind( vSuper2, pObj ) == -1 )
143 Vec_PtrPush( vUnique, pObj );
144 return vUnique;
145 }
146
147 /**Function*************************************************************
148
149 Synopsis [Detects constraints using structural methods.]
150
151 Description []
152
153 SideEffects []
154
155 SeeAlso []
156
157 ***********************************************************************/
Saig_ManDetectConstr(Aig_Man_t * p,int iOut,Vec_Ptr_t ** pvOuts,Vec_Ptr_t ** pvCons)158 int Saig_ManDetectConstr( Aig_Man_t * p, int iOut, Vec_Ptr_t ** pvOuts, Vec_Ptr_t ** pvCons )
159 {
160 Vec_Ptr_t * vSuper, * vSuper2 = NULL, * vUnique;
161 Aig_Obj_t * pObj, * pObj2, * pFlop;
162 int i, nFlops, RetValue;
163 assert( iOut >= 0 && iOut < Saig_ManPoNum(p) );
164 *pvOuts = NULL;
165 *pvCons = NULL;
166 pObj = Aig_ObjChild0( Aig_ManCo(p, iOut) );
167 if ( pObj == Aig_ManConst0(p) )
168 {
169 vUnique = Vec_PtrStart( 1 );
170 Vec_PtrWriteEntry( vUnique, 0, Aig_ManConst1(p) );
171 *pvOuts = vUnique;
172 *pvCons = Vec_PtrAlloc( 0 );
173 return -1;
174 }
175 if ( Aig_IsComplement(pObj) || !Aig_ObjIsNode(pObj) )
176 {
177 printf( "The output is not an AND.\n" );
178 return 0;
179 }
180 vSuper = Saig_DetectConstrCollectSuper( pObj );
181 assert( Vec_PtrSize(vSuper) >= 2 );
182 nFlops = 0;
183 Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pObj, i )
184 nFlops += Saig_ObjIsLo( p, Aig_Regular(pObj) );
185 if ( nFlops == 0 )
186 {
187 printf( "There is no flop outputs.\n" );
188 Vec_PtrFree( vSuper );
189 return 0;
190 }
191 // try flops
192 vUnique = NULL;
193 Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pObj, i )
194 {
195 pFlop = Aig_Regular( pObj );
196 if ( !Saig_ObjIsLo(p, pFlop) )
197 continue;
198 pFlop = Saig_ObjLoToLi( p, pFlop );
199 pObj2 = Aig_ObjChild0( pFlop );
200 if ( !Aig_IsComplement(pObj2) || !Aig_ObjIsNode(Aig_Regular(pObj2)) )
201 continue;
202 vSuper2 = Saig_DetectConstrCollectSuper( Aig_Regular(pObj2) );
203 // every node in vSuper2 should appear in vSuper
204 vUnique = Saig_ManDetectConstrCheckCont( vSuper, vSuper2 );
205 if ( vUnique != NULL )
206 {
207 /// assert( !Aig_IsComplement(pObj) );
208 // assert( Vec_PtrFind( vSuper2, pObj ) >= 0 );
209 if ( Aig_IsComplement(pObj) )
210 {
211 printf( "Special flop input is complemented.\n" );
212 Vec_PtrFreeP( &vUnique );
213 Vec_PtrFree( vSuper2 );
214 break;
215 }
216 if ( Vec_PtrFind( vSuper2, pObj ) == -1 )
217 {
218 printf( "Cannot find special flop about the inputs of OR gate.\n" );
219 Vec_PtrFreeP( &vUnique );
220 Vec_PtrFree( vSuper2 );
221 break;
222 }
223 // remove the flop output
224 Vec_PtrRemove( vSuper2, pObj );
225 break;
226 }
227 Vec_PtrFree( vSuper2 );
228 }
229 Vec_PtrFree( vSuper );
230 if ( vUnique == NULL )
231 {
232 printf( "There is no structural constraints.\n" );
233 return 0;
234 }
235 // vUnique contains unique entries
236 // vSuper2 contains the supergate
237 printf( "Output %d : Structural analysis found %d original properties and %d constraints.\n",
238 iOut, Vec_PtrSize(vUnique), Vec_PtrSize(vSuper2) );
239 // remember the number of constraints
240 RetValue = Vec_PtrSize(vSuper2);
241 // make the AND of properties
242 // Vec_PtrFree( vUnique );
243 // Vec_PtrFree( vSuper2 );
244 *pvOuts = vUnique;
245 *pvCons = vSuper2;
246 return RetValue;
247 }
248
249
250 /**Function*************************************************************
251
252 Synopsis [Procedure used for sorting nodes by ID.]
253
254 Description []
255
256 SideEffects []
257
258 SeeAlso []
259
260 ***********************************************************************/
Saig_ManDupCompare(Aig_Obj_t ** pp1,Aig_Obj_t ** pp2)261 int Saig_ManDupCompare( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
262 {
263 int Diff = Aig_ObjToLit(*pp1) - Aig_ObjToLit(*pp2);
264 if ( Diff < 0 )
265 return -1;
266 if ( Diff > 0 )
267 return 1;
268 return 0;
269 }
270
271 /**Function*************************************************************
272
273 Synopsis [Duplicates the AIG while unfolding constraints.]
274
275 Description []
276
277 SideEffects []
278
279 SeeAlso []
280
281 ***********************************************************************/
Saig_ManDupUnfoldConstrs(Aig_Man_t * pAig)282 Aig_Man_t * Saig_ManDupUnfoldConstrs( Aig_Man_t * pAig )
283 {
284 Vec_Ptr_t * vOutsAll, * vConsAll;
285 Vec_Ptr_t * vOuts, * vCons, * vCons0;
286 Aig_Man_t * pAigNew;
287 Aig_Obj_t * pMiter, * pObj;
288 int i, k, RetValue;
289 // detect constraints for each output
290 vOutsAll = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
291 vConsAll = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
292 Saig_ManForEachPo( pAig, pObj, i )
293 {
294 RetValue = Saig_ManDetectConstr( pAig, i, &vOuts, &vCons );
295 if ( RetValue == 0 )
296 {
297 Vec_PtrFreeP( &vOuts );
298 Vec_PtrFreeP( &vCons );
299 Vec_VecFree( (Vec_Vec_t *)vOutsAll );
300 Vec_VecFree( (Vec_Vec_t *)vConsAll );
301 return Aig_ManDupDfs( pAig );
302 }
303 Vec_PtrSort( vOuts, (int (*)(void))Saig_ManDupCompare );
304 Vec_PtrSort( vCons, (int (*)(void))Saig_ManDupCompare );
305 Vec_PtrPush( vOutsAll, vOuts );
306 Vec_PtrPush( vConsAll, vCons );
307 }
308 // check if constraints are compatible
309 vCons0 = (Vec_Ptr_t *)Vec_PtrEntry( vConsAll, 0 );
310 Vec_PtrForEachEntry( Vec_Ptr_t *, vConsAll, vCons, i )
311 if ( Vec_PtrSize(vCons) )
312 vCons0 = vCons;
313 Vec_PtrForEachEntry( Vec_Ptr_t *, vConsAll, vCons, i )
314 {
315 // Constant 0 outputs are always compatible (vOuts stores the negation)
316 vOuts = (Vec_Ptr_t *)Vec_PtrEntry( vOutsAll, i );
317 if ( Vec_PtrSize(vOuts) == 1 && (Aig_Obj_t *)Vec_PtrEntry( vOuts, 0 ) == Aig_ManConst1(pAig) )
318 continue;
319 if ( !Vec_PtrEqual(vCons0, vCons) )
320 break;
321 }
322 if ( i < Vec_PtrSize(vConsAll) )
323 {
324 printf( "Collected constraints are not compatible.\n" );
325 Vec_VecFree( (Vec_Vec_t *)vOutsAll );
326 Vec_VecFree( (Vec_Vec_t *)vConsAll );
327 return Aig_ManDupDfs( pAig );
328 }
329
330 // start the new manager
331 pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
332 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
333 // map the constant node
334 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
335 // create variables for PIs
336 Aig_ManForEachCi( pAig, pObj, i )
337 pObj->pData = Aig_ObjCreateCi( pAigNew );
338 // add internal nodes of this frame
339 Aig_ManForEachNode( pAig, pObj, i )
340 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
341 // transform each output
342 Vec_PtrForEachEntry( Vec_Ptr_t *, vOutsAll, vOuts, i )
343 {
344 // AND the outputs
345 pMiter = Aig_ManConst1( pAigNew );
346 Vec_PtrForEachEntry( Aig_Obj_t *, vOuts, pObj, k )
347 pMiter = Aig_And( pAigNew, pMiter, Aig_Not(Aig_ObjRealCopy(pObj)) );
348 Aig_ObjCreateCo( pAigNew, pMiter );
349 }
350 // add constraints
351 pAigNew->nConstrs = Vec_PtrSize(vCons0);
352 Vec_PtrForEachEntry( Aig_Obj_t *, vCons0, pObj, i )
353 Aig_ObjCreateCo( pAigNew, Aig_ObjRealCopy(pObj) );
354 // transfer to register outputs
355 Saig_ManForEachLi( pAig, pObj, i )
356 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
357 // Vec_PtrFreeP( &vOuts );
358 // Vec_PtrFreeP( &vCons );
359 Vec_VecFree( (Vec_Vec_t *)vOutsAll );
360 Vec_VecFree( (Vec_Vec_t *)vConsAll );
361
362 Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
363 Aig_ManCleanup( pAigNew );
364 Aig_ManSeqCleanup( pAigNew );
365 return pAigNew;
366 }
367
368 /**Function*************************************************************
369
370 Synopsis [Duplicates the AIG while folding in the constraints.]
371
372 Description []
373
374 SideEffects []
375
376 SeeAlso []
377
378 ***********************************************************************/
Saig_ManDupFoldConstrs(Aig_Man_t * pAig,Vec_Int_t * vConstrs)379 Aig_Man_t * Saig_ManDupFoldConstrs( Aig_Man_t * pAig, Vec_Int_t * vConstrs )
380 {
381 Aig_Man_t * pAigNew;
382 Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
383 int Entry, i;
384 assert( Saig_ManRegNum(pAig) > 0 );
385 // start the new manager
386 pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
387 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
388 // map the constant node
389 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
390 // create variables for PIs
391 Aig_ManForEachCi( pAig, pObj, i )
392 pObj->pData = Aig_ObjCreateCi( pAigNew );
393 // add internal nodes of this frame
394 Aig_ManForEachNode( pAig, pObj, i )
395 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
396
397 // OR the constraint outputs
398 pMiter = Aig_ManConst0( pAigNew );
399 Vec_IntForEachEntry( vConstrs, Entry, i )
400 {
401 assert( Entry > 0 && Entry < Saig_ManPoNum(pAig) );
402 pObj = Aig_ManCo( pAig, Entry );
403 pMiter = Aig_Or( pAigNew, pMiter, Aig_ObjChild0Copy(pObj) );
404 }
405 // create additional flop
406 pFlopOut = Aig_ObjCreateCi( pAigNew );
407 pFlopIn = Aig_Or( pAigNew, pMiter, pFlopOut );
408
409 // create primary output
410 Saig_ManForEachPo( pAig, pObj, i )
411 {
412 pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) );
413 Aig_ObjCreateCo( pAigNew, pMiter );
414 }
415
416 // transfer to register outputs
417 Saig_ManForEachLi( pAig, pObj, i )
418 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
419 // create additional flop
420 Aig_ObjCreateCo( pAigNew, pFlopIn );
421
422 Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 );
423 Aig_ManCleanup( pAigNew );
424 Aig_ManSeqCleanup( pAigNew );
425 return pAigNew;
426 }
427
428
429 /**Function*************************************************************
430
431 Synopsis [Tests the above two procedures.]
432
433 Description []
434
435 SideEffects []
436
437 SeeAlso []
438
439 ***********************************************************************/
Saig_ManFoldConstrTest(Aig_Man_t * pAig)440 void Saig_ManFoldConstrTest( Aig_Man_t * pAig )
441 {
442 Aig_Man_t * pAig1, * pAig2;
443 Vec_Int_t * vConstrs;
444 // unfold constraints
445 pAig1 = Saig_ManDupUnfoldConstrs( pAig );
446 // create the constraint list
447 vConstrs = Vec_IntStartNatural( Saig_ManPoNum(pAig1) );
448 Vec_IntRemove( vConstrs, 0 );
449 // fold constraints back
450 pAig2 = Saig_ManDupFoldConstrs( pAig1, vConstrs );
451 Vec_IntFree( vConstrs );
452 // compare the two AIGs
453 Ioa_WriteAiger( pAig2, "test.aig", 0, 0 );
454 Aig_ManStop( pAig1 );
455 Aig_ManStop( pAig2 );
456 }
457
458 /**Function*************************************************************
459
460 Synopsis [Experiment with the above procedure.]
461
462 Description []
463
464 SideEffects []
465
466 SeeAlso []
467
468 ***********************************************************************/
Saig_ManDetectConstrTest(Aig_Man_t * p)469 int Saig_ManDetectConstrTest( Aig_Man_t * p )
470 {
471 Vec_Ptr_t * vOuts, * vCons;
472 int RetValue = Saig_ManDetectConstr( p, 0, &vOuts, &vCons );
473 Vec_PtrFreeP( &vOuts );
474 Vec_PtrFreeP( &vCons );
475 return RetValue;
476 }
477
478 ////////////////////////////////////////////////////////////////////////
479 /// END OF FILE ///
480 ////////////////////////////////////////////////////////////////////////
481
482
483 ABC_NAMESPACE_IMPL_END
484
485