1 /**CFile****************************************************************
2 
3   FileName    [giaFront.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Scalable AIG package.]
8 
9   Synopsis    [Frontier representation.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - June 20, 2005.]
16 
17   Revision    [$Id: giaFront.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "gia.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 ///                        DECLARATIONS                              ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 ///                     FUNCTION DEFINITIONS                         ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36   Synopsis    [Find the next place on the frontier.]
37 
38   Description []
39 
40   SideEffects []
41 
42   SeeAlso     []
43 
44 ***********************************************************************/
Gia_ManFrontFindNext(char * pFront,int nFront,int iFront)45 static inline int Gia_ManFrontFindNext( char * pFront, int nFront, int iFront )
46 {
47     assert( iFront < nFront );
48     for ( ; pFront[iFront]; iFront = (iFront + 1) % nFront );
49     assert( pFront[iFront] == 0 );
50     pFront[iFront] = 1;
51     return iFront;
52 }
53 
54 /**Function*************************************************************
55 
56   Synopsis    [Transforms the frontier manager to its initial state.]
57 
58   Description []
59 
60   SideEffects []
61 
62   SeeAlso     []
63 
64 ***********************************************************************/
Gia_ManFrontTransform(Gia_Man_t * p)65 void Gia_ManFrontTransform( Gia_Man_t * p )
66 {
67     Gia_Obj_t * pObj;
68     int i, * pFrontToId; // mapping of nodes into frontier variables
69     assert( p->nFront > 0 );
70     pFrontToId = ABC_FALLOC( int, p->nFront );
71     Gia_ManForEachObj( p, pObj, i )
72     {
73         if ( Gia_ObjIsCo(pObj) )
74         {
75             assert( pObj->Value == GIA_NONE );
76             pObj->iDiff0 = i - pFrontToId[Gia_ObjDiff0(pObj)];
77         }
78         else if ( Gia_ObjIsAnd(pObj) )
79         {
80             assert( (int)pObj->Value < p->nFront );
81             pObj->iDiff0 = i - pFrontToId[Gia_ObjDiff0(pObj)];
82             pObj->iDiff1 = i - pFrontToId[Gia_ObjDiff1(pObj)];
83             pFrontToId[pObj->Value] = i;
84         }
85         else
86         {
87             assert( (int)pObj->Value < p->nFront );
88             pFrontToId[pObj->Value] = i;
89         }
90         pObj->Value = 0;
91     }
92     ABC_FREE( pFrontToId );
93 }
94 
95 /**Function*************************************************************
96 
97   Synopsis    [Determine the frontier.]
98 
99   Description []
100 
101   SideEffects []
102 
103   SeeAlso     []
104 
105 ***********************************************************************/
Gia_ManCrossCutSimple(Gia_Man_t * p)106 int Gia_ManCrossCutSimple( Gia_Man_t * p )
107 {
108     Gia_Obj_t * pObj;
109     int i, nCutCur = 0, nCutMax = 0;
110     Gia_ManCreateValueRefs( p );
111     Gia_ManForEachObj( p, pObj, i )
112     {
113         if ( pObj->Value )
114             nCutCur++;
115         if ( nCutMax < nCutCur )
116             nCutMax = nCutCur;
117         if ( Gia_ObjIsAnd(pObj) )
118         {
119             if ( --Gia_ObjFanin0(pObj)->Value == 0 )
120                 nCutCur--;
121             if ( --Gia_ObjFanin1(pObj)->Value == 0 )
122                 nCutCur--;
123         }
124         else if ( Gia_ObjIsCo(pObj) )
125         {
126             if ( --Gia_ObjFanin0(pObj)->Value == 0 )
127                 nCutCur--;
128         }
129     }
130 //    Gia_ManForEachObj( p, pObj, i )
131 //        assert( pObj->Value == 0 );
132     return nCutMax;
133 }
134 
135 
136 /**Function*************************************************************
137 
138   Synopsis    [Determine the frontier.]
139 
140   Description []
141 
142   SideEffects []
143 
144   SeeAlso     []
145 
146 ***********************************************************************/
Gia_ManFront(Gia_Man_t * p)147 Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
148 {
149     Gia_Man_t * pNew;
150     Gia_Obj_t * pObj, * pFanin0New, * pFanin1New, * pObjNew;
151     char * pFront;    // places used for the frontier
152     int i, iLit, nCrossCut = 0, nCrossCutMax = 0;
153     int nCrossCutMaxInit = Gia_ManCrossCutSimple( p );
154     int iFront = 0;//, clk = Abc_Clock();
155     // set references for all objects
156     Gia_ManCreateValueRefs( p );
157     // start the new manager
158     pNew = Gia_ManStart( Gia_ManObjNum(p) );
159     pNew->pName = Abc_UtilStrsav( p->pName );
160     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
161     pNew->nFront = 1 + (int)((float)1.1 * nCrossCutMaxInit);
162     // start the frontier
163     pFront = ABC_CALLOC( char, pNew->nFront );
164     // add constant node
165     Gia_ManConst0(pNew)->Value = iFront = Gia_ManFrontFindNext( pFront, pNew->nFront, iFront );
166     if ( Gia_ObjValue(Gia_ManConst0(p)) == 0 )
167         pFront[iFront] = 0;
168     else
169         nCrossCut = 1;
170     // iterate through the objects
171     Gia_ManForEachObj1( p, pObj, i )
172     {
173         if ( Gia_ObjIsCi(pObj) )
174         {
175             if ( Gia_ObjValue(pObj) && nCrossCutMax < ++nCrossCut )
176                 nCrossCutMax = nCrossCut;
177             // create new node
178             iLit = Gia_ManAppendCi( pNew );
179             pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(iLit) );
180             assert( Gia_ObjId(pNew, pObjNew) == Gia_ObjId(p, pObj) );
181             pObjNew->Value = iFront = Gia_ManFrontFindNext( pFront, pNew->nFront, iFront );
182             // handle CIs without fanout
183             if ( Gia_ObjValue(pObj) == 0 )
184                 pFront[iFront] = 0;
185             continue;
186         }
187         if ( Gia_ObjIsCo(pObj) )
188         {
189             assert( Gia_ObjValue(pObj) == 0 );
190             // create new node
191             iLit = Gia_ManAppendCo( pNew, 0 );
192             pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(iLit) );
193             assert( Gia_ObjId(pNew, pObjNew) == Gia_ObjId(p, pObj) );
194             // get the fanin
195             pFanin0New = Gia_ManObj( pNew, Gia_ObjFaninId0(pObj, i) );
196             assert( pFanin0New->Value != GIA_NONE );
197             pObjNew->Value = GIA_NONE;
198             pObjNew->iDiff0 = pFanin0New->Value;
199             pObjNew->fCompl0 = Gia_ObjFaninC0(pObj);
200             // deref the fanin
201             if ( --Gia_ObjFanin0(pObj)->Value == 0 )
202             {
203                 pFront[pFanin0New->Value] = 0;
204                 nCrossCut--;
205             }
206             continue;
207         }
208         if ( Gia_ObjValue(pObj) && nCrossCutMax < ++nCrossCut )
209             nCrossCutMax = nCrossCut;
210         // create new node
211         pObjNew = Gia_ManAppendObj( pNew );
212         assert( Gia_ObjId(pNew, pObjNew) == Gia_ObjId(p, pObj) );
213         // assign the first fanin
214         pFanin0New = Gia_ManObj( pNew, Gia_ObjFaninId0(pObj, i) );
215         assert( pFanin0New->Value != GIA_NONE );
216         pObjNew->iDiff0 = pFanin0New->Value;
217         pObjNew->fCompl0 = Gia_ObjFaninC0(pObj);
218         // assign the second fanin
219         pFanin1New = Gia_ManObj( pNew, Gia_ObjFaninId1(pObj, i) );
220         assert( pFanin1New->Value != GIA_NONE );
221         pObjNew->iDiff1 = pFanin1New->Value;
222         pObjNew->fCompl1 = Gia_ObjFaninC1(pObj);
223         // assign the frontier number
224         pObjNew->Value = iFront = Gia_ManFrontFindNext( pFront, pNew->nFront, iFront );
225         // deref the fanins
226         if ( --Gia_ObjFanin0(pObj)->Value == 0 )
227         {
228             pFront[pFanin0New->Value] = 0;
229             nCrossCut--;
230         }
231         if ( --Gia_ObjFanin1(pObj)->Value == 0 )
232         {
233             pFront[pFanin1New->Value] = 0;
234             nCrossCut--;
235         }
236         // handle nodes without fanout (choice nodes)
237         if ( Gia_ObjValue(pObj) == 0 )
238             pFront[iFront] = 0;
239     }
240     assert( pNew->nObjs == p->nObjs );
241     assert( nCrossCut == 0 || nCrossCutMax == nCrossCutMaxInit );
242     for ( i = 0; i < pNew->nFront; i++ )
243         assert( pFront[i] == 0 );
244     ABC_FREE( pFront );
245 //printf( "Crosscut = %6d. Frontier = %6d. ", nCrossCutMaxInit, pNew->nFront );
246 //ABC_PRT( "Time", Abc_Clock() - clk );
247     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
248     return pNew;
249 }
250 
251 /**Function*************************************************************
252 
253   Synopsis    []
254 
255   Description []
256 
257   SideEffects []
258 
259   SeeAlso     []
260 
261 ***********************************************************************/
Gia_ManFrontTest(Gia_Man_t * p)262 void Gia_ManFrontTest( Gia_Man_t * p )
263 {
264     Gia_Man_t * pNew;
265     pNew  = Gia_ManFront( p );
266     Gia_ManFrontTransform( pNew );
267 //    Gia_ManCleanValue( p );
268 //    Gia_ManCleanValue( pNew );
269     if ( memcmp( pNew->pObjs, p->pObjs, sizeof(Gia_Obj_t) * p->nObjs ) )
270     {
271 /*
272         Gia_Obj_t * pObj, * pObjNew;
273         int i;
274         Gia_ManForEachObj( p, pObj, i )
275         {
276             pObjNew = Gia_ManObj( pNew, i );
277             printf( "%5d %5d   %5d %5d\n",
278                 pObj->iDiff0, pObjNew->iDiff0,
279                 pObj->iDiff1, pObjNew->iDiff1 );
280         }
281 */
282         printf( "Verification failed.\n" );
283     }
284     else
285         printf( "Verification successful.\n" );
286     Gia_ManStop( pNew );
287 }
288 
289 ////////////////////////////////////////////////////////////////////////
290 ///                       END OF FILE                                ///
291 ////////////////////////////////////////////////////////////////////////
292 
293 
294 ABC_NAMESPACE_IMPL_END
295 
296