1 /**CFile****************************************************************
2 
3   FileName    [cecSweep.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Combinational equivalence checking.]
8 
9   Synopsis    [SAT sweeping manager.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - June 20, 2005.]
16 
17   Revision    [$Id: cecSweep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "cecInt.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    [Performs limited speculative reduction.]
37 
38   Description []
39 
40   SideEffects []
41 
42   SeeAlso     []
43 
44 ***********************************************************************/
Cec_ManFraSpecReduction(Cec_ManFra_t * p)45 Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p )
46 {
47     Gia_Man_t * pNew, * pTemp;
48     Gia_Obj_t * pObj, * pRepr = NULL;
49     int iRes0, iRes1, iRepr, iNode, iMiter;
50     int i, fCompl, * piCopies, * pDepths;
51     Gia_ManSetPhase( p->pAig );
52     Vec_IntClear( p->vXorNodes );
53     if ( p->pPars->nLevelMax )
54         Gia_ManLevelNum( p->pAig );
55     pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) );
56     pNew->pName = Abc_UtilStrsav( p->pAig->pName );
57     pNew->pSpec = Abc_UtilStrsav( p->pAig->pName );
58     Gia_ManHashAlloc( pNew );
59     piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
60     pDepths  = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
61     piCopies[0] = 0;
62     Gia_ManForEachObj1( p->pAig, pObj, i )
63     {
64         if ( Gia_ObjIsCi(pObj) )
65         {
66             piCopies[i] = Gia_ManAppendCi( pNew );
67             continue;
68         }
69         if ( Gia_ObjIsCo(pObj) )
70             continue;
71         if ( piCopies[Gia_ObjFaninId0(pObj,i)] == -1 ||
72              piCopies[Gia_ObjFaninId1(pObj,i)] == -1 )
73              continue;
74         iRes0 = Abc_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) );
75         iRes1 = Abc_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) );
76         iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 );
77         pDepths[i] = Abc_MaxInt( pDepths[Gia_ObjFaninId0(pObj,i)], pDepths[Gia_ObjFaninId1(pObj,i)] );
78         if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID || Gia_ObjFailed(p->pAig, i) )
79             continue;
80         assert( Gia_ObjRepr(p->pAig, i) < i );
81         iRepr = piCopies[Gia_ObjRepr(p->pAig, i)];
82         if ( iRepr == -1 )
83             continue;
84         if ( Abc_LitRegular(iNode) == Abc_LitRegular(iRepr) )
85             continue;
86         if ( p->pPars->nLevelMax &&
87             (Gia_ObjLevelId(p->pAig, i)  > p->pPars->nLevelMax ||
88              Gia_ObjLevelId(p->pAig, Abc_Lit2Var(iRepr)) > p->pPars->nLevelMax) )
89             continue;
90         if ( p->pPars->fDualOut )
91         {
92 //            if ( i % 1000 == 0 && Gia_ObjRepr(p->pAig, i) )
93 //                Gia_ManEquivPrintOne( p->pAig, Gia_ObjRepr(p->pAig, i), 0 );
94             if ( p->pPars->fColorDiff )
95             {
96                 if ( !Gia_ObjDiffColors( p->pAig, Gia_ObjRepr(p->pAig, i), i ) )
97                     continue;
98             }
99             else
100             {
101                 if ( !Gia_ObjDiffColors2( p->pAig, Gia_ObjRepr(p->pAig, i), i ) )
102                     continue;
103             }
104         }
105         pRepr = Gia_ManObj( p->pAig, Gia_ObjRepr(p->pAig, i) );
106         fCompl = Gia_ObjPhaseReal(pObj) ^ Gia_ObjPhaseReal(pRepr);
107         piCopies[i] = Abc_LitNotCond( iRepr, fCompl );
108         if ( Gia_ObjProved(p->pAig, i) )
109             continue;
110         // produce speculative miter
111         iMiter = Gia_ManHashXor( pNew, iNode, piCopies[i] );
112         Gia_ManAppendCo( pNew, iMiter );
113         Vec_IntPush( p->vXorNodes, Gia_ObjRepr(p->pAig, i) );
114         Vec_IntPush( p->vXorNodes, i );
115         // add to the depth of this node
116         pDepths[i] = 1 + Abc_MaxInt( pDepths[i], pDepths[Gia_ObjRepr(p->pAig, i)] );
117         if ( p->pPars->nDepthMax && pDepths[i] >= p->pPars->nDepthMax )
118             piCopies[i] = -1;
119     }
120     ABC_FREE( piCopies );
121     ABC_FREE( pDepths );
122     Gia_ManHashStop( pNew );
123     Gia_ManSetRegNum( pNew, 0 );
124     pNew = Gia_ManCleanup( pTemp = pNew );
125     Gia_ManStop( pTemp );
126     return pNew;
127 }
128 
129 /**Function*************************************************************
130 
131   Synopsis    []
132 
133   Description []
134 
135   SideEffects []
136 
137   SeeAlso     []
138 
139 ***********************************************************************/
Cec_ManFraClassesUpdate_rec(Gia_Obj_t * pObj)140 int Cec_ManFraClassesUpdate_rec( Gia_Obj_t * pObj )
141 {
142     int Result;
143     if ( pObj->fMark0 )
144         return 1;
145     if ( Gia_ObjIsCi(pObj) || Gia_ObjIsConst0(pObj) )
146         return 0;
147     Result = (Cec_ManFraClassesUpdate_rec( Gia_ObjFanin0(pObj) ) |
148               Cec_ManFraClassesUpdate_rec( Gia_ObjFanin1(pObj) ));
149     return pObj->fMark0 = Result;
150 }
151 
152 /**Function*************************************************************
153 
154   Synopsis    [Creates simulation info for this round.]
155 
156   Description []
157 
158   SideEffects []
159 
160   SeeAlso     []
161 
162 ***********************************************************************/
Cec_ManFraCreateInfo(Cec_ManSim_t * p,Vec_Ptr_t * vCiInfo,Vec_Ptr_t * vInfo,int nSeries)163 void Cec_ManFraCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vCiInfo, Vec_Ptr_t * vInfo, int nSeries )
164 {
165     unsigned * pRes0, * pRes1;
166     int i, w;
167     for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
168     {
169         pRes0 = (unsigned *)Vec_PtrEntry( vCiInfo, i );
170         pRes1 = (unsigned *)Vec_PtrEntry( vInfo, i );
171         pRes1 += p->nWords * nSeries;
172         for ( w = 0; w < p->nWords; w++ )
173             pRes0[w] = pRes1[w];
174     }
175 }
176 
177 /**Function*************************************************************
178 
179   Synopsis    [Updates equivalence classes using the patterns.]
180 
181   Description []
182 
183   SideEffects []
184 
185   SeeAlso     []
186 
187 ***********************************************************************/
Cec_ManFraClassesUpdate(Cec_ManFra_t * p,Cec_ManSim_t * pSim,Cec_ManPat_t * pPat,Gia_Man_t * pNew)188 int Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t * pPat, Gia_Man_t * pNew )
189 {
190     Vec_Ptr_t * vInfo;
191     Gia_Obj_t * pObj, * pObjOld, * pReprOld;
192     int i, k, iRepr, iNode;
193     abctime clk;
194 clk = Abc_Clock();
195     vInfo = Cec_ManPatCollectPatterns( pPat, Gia_ManCiNum(p->pAig), pSim->nWords );
196 p->timePat += Abc_Clock() - clk;
197 clk = Abc_Clock();
198     if ( vInfo != NULL )
199     {
200         Gia_ManCreateValueRefs( p->pAig );
201         for ( i = 0; i < pPat->nSeries; i++ )
202         {
203             Cec_ManFraCreateInfo( pSim, pSim->vCiSimInfo, vInfo, i );
204             if ( Cec_ManSimSimulateRound( pSim, pSim->vCiSimInfo, pSim->vCoSimInfo ) )
205             {
206                 Vec_PtrFree( vInfo );
207                 return 1;
208             }
209         }
210         Vec_PtrFree( vInfo );
211     }
212 p->timeSim += Abc_Clock() - clk;
213     assert( Vec_IntSize(p->vXorNodes) == 2*Gia_ManCoNum(pNew) );
214     // mark the transitive fanout of failed nodes
215     if ( p->pPars->nDepthMax != 1 )
216     {
217         Gia_ManCleanMark0( p->pAig );
218         Gia_ManCleanMark1( p->pAig );
219         Gia_ManForEachCo( pNew, pObj, k )
220         {
221             iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
222             iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
223             if ( pObj->fMark0 == 0 && pObj->fMark1 == 1 ) // proved
224                 continue;
225 //            Gia_ManObj(p->pAig, iRepr)->fMark0 = 1;
226             Gia_ManObj(p->pAig, iNode)->fMark0 = 1;
227         }
228         // mark the nodes reachable through the failed nodes
229         Gia_ManForEachAnd( p->pAig, pObjOld, k )
230             pObjOld->fMark0 |= (Gia_ObjFanin0(pObjOld)->fMark0 | Gia_ObjFanin1(pObjOld)->fMark0);
231         // unmark the disproved nodes
232         Gia_ManForEachCo( pNew, pObj, k )
233         {
234             iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
235             iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
236             if ( pObj->fMark0 == 0 && pObj->fMark1 == 1 ) // proved
237                 continue;
238             pObjOld = Gia_ManObj(p->pAig, iNode);
239             assert( pObjOld->fMark0 == 1 );
240             if ( Gia_ObjFanin0(pObjOld)->fMark0 == 0 && Gia_ObjFanin1(pObjOld)->fMark0 == 0 )
241                 pObjOld->fMark1 = 1;
242         }
243         // clean marks
244         Gia_ManForEachAnd( p->pAig, pObjOld, k )
245             if ( pObjOld->fMark1 )
246             {
247                 pObjOld->fMark0 = 0;
248                 pObjOld->fMark1 = 0;
249             }
250     }
251     // set the results
252     p->nAllProved = p->nAllDisproved = p->nAllFailed = 0;
253     Gia_ManForEachCo( pNew, pObj, k )
254     {
255         iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
256         iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
257         pReprOld = Gia_ManObj(p->pAig, iRepr);
258         pObjOld = Gia_ManObj(p->pAig, iNode);
259         if ( pObj->fMark1 )
260         { // proved
261             assert( pObj->fMark0 == 0 );
262             assert( !Gia_ObjProved(p->pAig, iNode) );
263             if ( pReprOld->fMark0 == 0 && pObjOld->fMark0 == 0 )
264 //            if ( pObjOld->fMark0 == 0 )
265             {
266                 assert( iRepr == Gia_ObjRepr(p->pAig, iNode) );
267                 Gia_ObjSetProved( p->pAig, iNode );
268                 p->nAllProved++;
269             }
270         }
271         else if ( pObj->fMark0 )
272         { // disproved
273             assert( pObj->fMark1 == 0 );
274             if ( pReprOld->fMark0 == 0 && pObjOld->fMark0 == 0 )
275 //            if ( pObjOld->fMark0 == 0 )
276             {
277                 if ( iRepr == Gia_ObjRepr(p->pAig, iNode) )
278                     Abc_Print( 1, "Cec_ManFraClassesUpdate(): Error! Node is not refined!\n" );
279                 p->nAllDisproved++;
280             }
281         }
282         else
283         { // failed
284             assert( pObj->fMark0 == 0 );
285             assert( pObj->fMark1 == 0 );
286             assert( !Gia_ObjFailed(p->pAig, iNode) );
287             assert( !Gia_ObjProved(p->pAig, iNode) );
288             Gia_ObjSetFailed( p->pAig, iNode );
289             p->nAllFailed++;
290         }
291     }
292     return 0;
293 }
294 
295 ////////////////////////////////////////////////////////////////////////
296 ///                       END OF FILE                                ///
297 ////////////////////////////////////////////////////////////////////////
298 
299 
300 ABC_NAMESPACE_IMPL_END
301 
302