abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cecSweep.c File Reference
#include "cecInt.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START
Gia_Man_t
Cec_ManFraSpecReduction (Cec_ManFra_t *p)
 DECLARATIONS ///. More...
 
int Cec_ManFraClassesUpdate_rec (Gia_Obj_t *pObj)
 
void Cec_ManFraCreateInfo (Cec_ManSim_t *p, Vec_Ptr_t *vCiInfo, Vec_Ptr_t *vInfo, int nSeries)
 
int Cec_ManFraClassesUpdate (Cec_ManFra_t *p, Cec_ManSim_t *pSim, Cec_ManPat_t *pPat, Gia_Man_t *pNew)
 

Function Documentation

int Cec_ManFraClassesUpdate ( Cec_ManFra_t p,
Cec_ManSim_t pSim,
Cec_ManPat_t pPat,
Gia_Man_t pNew 
)

Function*************************************************************

Synopsis [Updates equivalence classes using the patterns.]

Description []

SideEffects []

SeeAlso []

Definition at line 188 of file cecSweep.c.

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  {
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 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
abctime timeSim
Definition: cecInt.h:157
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition: giaUtil.c:215
int Cec_ManSimSimulateRound(Cec_ManSim_t *p, Vec_Ptr_t *vInfoCis, Vec_Ptr_t *vInfoCos)
Definition: cecClass.c:652
void Cec_ManFraCreateInfo(Cec_ManSim_t *p, Vec_Ptr_t *vCiInfo, Vec_Ptr_t *vInfo, int nSeries)
Definition: cecSweep.c:163
int nAllFailed
Definition: cecInt.h:155
Vec_Int_t * vXorNodes
Definition: cecInt.h:152
unsigned fMark1
Definition: gia.h:84
static abctime Abc_Clock()
Definition: abc_global.h:279
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Definition: gia.h:75
void Gia_ManCleanMark1(Gia_Man_t *p)
Definition: giaUtil.c:272
int nAllDisproved
Definition: cecInt.h:154
void Gia_ManCreateValueRefs(Gia_Man_t *p)
Definition: giaUtil.c:687
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
static void Gia_ObjSetProved(Gia_Man_t *p, int Id)
Definition: gia.h:897
int nWords
Definition: cecInt.h:117
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Vec_Ptr_t * vCiSimInfo
Definition: cecInt.h:127
if(last==0)
Definition: sparse_int.h:34
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
Vec_Ptr_t * Cec_ManPatCollectPatterns(Cec_ManPat_t *pMan, int nInputs, int nWords)
Definition: cecPat.c:455
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
unsigned fMark0
Definition: gia.h:79
int nDepthMax
Definition: cec.h:103
Gia_Man_t * pAig
Definition: cecInt.h:149
Vec_Ptr_t * vCoSimInfo
Definition: cecInt.h:128
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
static int Gia_ObjFailed(Gia_Man_t *p, int Id)
Definition: gia.h:900
static int Gia_ObjProved(Gia_Man_t *p, int Id)
Definition: gia.h:896
#define assert(ex)
Definition: util_old.h:213
abctime timePat
Definition: cecInt.h:158
ABC_INT64_T abctime
Definition: abc_global.h:278
int nAllProved
Definition: cecInt.h:153
static void Gia_ObjSetFailed(Gia_Man_t *p, int Id)
Definition: gia.h:901
static int Gia_ObjRepr(Gia_Man_t *p, int Id)
Definition: gia.h:887
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
Cec_ParFra_t * pPars
Definition: cecInt.h:150
int Cec_ManFraClassesUpdate_rec ( Gia_Obj_t pObj)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 140 of file cecSweep.c.

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) ) |
149  return pObj->fMark0 = Result;
150 }
static int Gia_ObjIsConst0(Gia_Obj_t *pObj)
Definition: gia.h:430
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
int Cec_ManFraClassesUpdate_rec(Gia_Obj_t *pObj)
Definition: cecSweep.c:140
unsigned fMark0
Definition: gia.h:79
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
void Cec_ManFraCreateInfo ( Cec_ManSim_t p,
Vec_Ptr_t vCiInfo,
Vec_Ptr_t vInfo,
int  nSeries 
)

Function*************************************************************

Synopsis [Creates simulation info for this round.]

Description []

SideEffects []

SeeAlso []

Definition at line 163 of file cecSweep.c.

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 }
Gia_Man_t * pAig
Definition: cecInt.h:115
int nWords
Definition: cecInt.h:117
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
ABC_NAMESPACE_IMPL_START Gia_Man_t* Cec_ManFraSpecReduction ( Cec_ManFra_t p)

DECLARATIONS ///.

CFile****************************************************************

FileName [cecSweep.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Combinational equivalence checking.]

Synopsis [SAT sweeping manager.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:
cecSweep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Performs limited speculative reduction.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file cecSweep.c.

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 }
static int Gia_ObjLevelId(Gia_Man_t *p, int Id)
Definition: gia.h:500
static int Gia_ObjPhaseReal(Gia_Obj_t *pObj)
Definition: gia.h:416
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
int Gia_ManHashXor(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:658
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Vec_Int_t * vXorNodes
Definition: cecInt.h:152
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition: giaMan.c:628
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Definition: gia.h:75
static int Gia_ObjDiffColors2(Gia_Man_t *p, int i, int j)
Definition: gia.h:909
int fDualOut
Definition: cec.h:107
char * pName
Definition: gia.h:97
int fColorDiff
Definition: cec.h:108
static int Gia_ObjDiffColors(Gia_Man_t *p, int i, int j)
Definition: gia.h:908
char * pSpec
Definition: gia.h:98
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
#define GIA_VOID
Definition: gia.h:45
#define ABC_FREE(obj)
Definition: abc_global.h:232
Definition: gia.h:95
int nDepthMax
Definition: cec.h:103
int nLevelMax
Definition: cec.h:102
Gia_Man_t * pAig
Definition: cecInt.h:149
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
static int Gia_ObjFailed(Gia_Man_t *p, int Id)
Definition: gia.h:900
static int Gia_ObjProved(Gia_Man_t *p, int Id)
Definition: gia.h:896
static int Abc_LitRegular(int Lit)
Definition: abc_global.h:268
#define assert(ex)
Definition: util_old.h:213
void Gia_ManSetPhase(Gia_Man_t *p)
Definition: giaUtil.c:379
int Gia_ManLevelNum(Gia_Man_t *p)
Definition: giaUtil.c:505
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
#define Gia_ManForEachObj1(p, pObj, i)
Definition: gia.h:986
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:461
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static int Gia_ObjRepr(Gia_Man_t *p, int Id)
Definition: gia.h:887
#define ABC_FALLOC(type, num)
Definition: abc_global.h:231
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
Cec_ParFra_t * pPars
Definition: cecInt.h:150