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