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

Go to the source code of this file.

Data Structures

struct  Ssw_Sem_t_
 

Typedefs

typedef
typedefABC_NAMESPACE_IMPL_START
struct Ssw_Sem_t_ 
Ssw_Sem_t
 DECLARATIONS ///. More...
 

Functions

Ssw_Sem_tSsw_SemManStart (Ssw_Man_t *pMan, int nConfMax, int fVerbose)
 FUNCTION DEFINITIONS ///. More...
 
void Ssw_SemManStop (Ssw_Sem_t *p)
 
int Ssw_SemCheckTargets (Ssw_Sem_t *p)
 
void Ssw_ManFilterBmcSavePattern (Ssw_Sem_t *p)
 
int Ssw_ManFilterBmc (Ssw_Sem_t *pBmc, int iPat, int fCheckTargets)
 
int Ssw_FilterUsingSemi (Ssw_Man_t *pMan, int fCheckTargets, int nConfMax, int fVerbose)
 

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Ssw_Sem_t_ Ssw_Sem_t

DECLARATIONS ///.

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

FileName [sswSemi.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [Semiformal for equivalence classes.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2008.]

Revision [

Id:
sswSemi.c,v 1.00 2008/09/01 00:00:00 alanmi Exp

]

Definition at line 30 of file sswSemi.c.

Function Documentation

int Ssw_FilterUsingSemi ( Ssw_Man_t pMan,
int  fCheckTargets,
int  nConfMax,
int  fVerbose 
)

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

Synopsis [Returns 1 if one of the targets has failed.]

Description []

SideEffects []

SeeAlso []

Definition at line 261 of file sswSemi.c.

262 {
263  Ssw_Sem_t * p;
264  int RetValue, Frames, Iter;
265  abctime clk = Abc_Clock();
266  p = Ssw_SemManStart( pMan, nConfMax, fVerbose );
267  if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
268  {
269  assert( 0 );
270  Ssw_SemManStop( p );
271  return 1;
272  }
273  if ( fVerbose )
274  {
275  Abc_Print( 1, "AIG : C = %6d. Cl = %6d. Nodes = %6d. ConfMax = %6d. FramesMax = %6d.\n",
276  Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
277  Aig_ManNodeNum(p->pMan->pAig), p->nConfMax, p->nFramesSweep );
278  }
279  RetValue = 0;
280  for ( Iter = 0; Iter < p->nPatterns; Iter++ )
281  {
282 clk = Abc_Clock();
283  pMan->pMSat = Ssw_SatStart( 0 );
284  Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets );
285  if ( fVerbose )
286  {
287  Abc_Print( 1, "%3d : C = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ",
288  Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
289  Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns,
290  p->pMan->nSatFailsReal? "f" : " " );
291  ABC_PRT( "T", Abc_Clock() - clk );
292  }
293  Ssw_ManCleanup( p->pMan );
294  if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
295  {
296  Abc_Print( 1, "Target is hit!!!\n" );
297  RetValue = 1;
298  }
299  if ( p->nPatterns >= p->nPatternsAlloc )
300  break;
301  }
302  Ssw_SemManStop( p );
303 
304  pMan->nStrangers = 0;
305  pMan->nSatCalls = 0;
306  pMan->nSatProof = 0;
307  pMan->nSatFailsReal = 0;
308  pMan->nSatCallsUnsat = 0;
309  pMan->nSatCallsSat = 0;
310  pMan->timeSimSat = 0;
311  pMan->timeSat = 0;
312  pMan->timeSatSat = 0;
313  pMan->timeSatUnsat = 0;
314  pMan->timeSatUndec = 0;
315  return RetValue;
316 }
int Ssw_ClassesClassNum(Ssw_Cla_t *p)
Definition: sswClass.c:275
void Ssw_ManCleanup(Ssw_Man_t *p)
Definition: sswMan.c:158
ABC_NAMESPACE_IMPL_START Ssw_Sat_t * Ssw_SatStart(int fPolarFlip)
DECLARATIONS ///.
Definition: sswCnf.c:45
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int Ssw_ClassesCand1Num(Ssw_Cla_t *p)
Definition: sswClass.c:259
int Ssw_SemCheckTargets(Ssw_Sem_t *p)
Definition: sswSemi.c:129
static abctime Abc_Clock()
Definition: abc_global.h:279
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
typedefABC_NAMESPACE_IMPL_START struct Ssw_Sem_t_ Ssw_Sem_t
DECLARATIONS ///.
Definition: sswSemi.c:30
Ssw_Sem_t * Ssw_SemManStart(Ssw_Man_t *pMan, int nConfMax, int fVerbose)
FUNCTION DEFINITIONS ///.
Definition: sswSemi.c:64
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
#define ABC_PRT(a, t)
Definition: abc_global.h:220
void Ssw_SemManStop(Ssw_Sem_t *p)
Definition: sswSemi.c:110
#define assert(ex)
Definition: util_old.h:213
int Ssw_ManFilterBmc(Ssw_Sem_t *pBmc, int iPat, int fCheckTargets)
Definition: sswSemi.c:177
ABC_INT64_T abctime
Definition: abc_global.h:278
int Ssw_ManFilterBmc ( Ssw_Sem_t pBmc,
int  iPat,
int  fCheckTargets 
)

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

Synopsis [Performs fraiging for the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 177 of file sswSemi.c.

178 {
179  Ssw_Man_t * p = pBmc->pMan;
180  Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
181  unsigned * pInfo;
182  int i, f, RetValue, fFirst = 0;
183  abctime clk;
184 clk = Abc_Clock();
185 
186  // start initialized timeframes
187  p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * 3 );
188  Saig_ManForEachLo( p->pAig, pObj, i )
189  {
190  pInfo = (unsigned *)Vec_PtrEntry( pBmc->vPatterns, i );
191  pObjNew = Aig_NotCond( Aig_ManConst1(p->pFrames), !Abc_InfoHasBit(pInfo, iPat) );
192  Ssw_ObjSetFrame( p, pObj, 0, pObjNew );
193  }
194 
195  // sweep internal nodes
196  RetValue = pBmc->nFramesSweep;
197  for ( f = 0; f < pBmc->nFramesSweep; f++ )
198  {
199  // map constants and PIs
200  Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
201  Saig_ManForEachPi( p->pAig, pObj, i )
202  Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
203  // sweep internal nodes
204  Aig_ManForEachNode( p->pAig, pObj, i )
205  {
206  pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
207  Ssw_ObjSetFrame( p, pObj, f, pObjNew );
208  if ( Ssw_ManSweepNode( p, pObj, f, 1, NULL ) )
209  {
211  if ( fFirst == 0 )
212  {
213  fFirst = 1;
214  pBmc->nConfMax *= 10;
215  }
216  }
217  if ( f > 0 && p->pMSat->pSat->stats.conflicts >= pBmc->nConfMax )
218  {
219  RetValue = -1;
220  break;
221  }
222  }
223  // quit if this is the last timeframe
224  if ( p->pMSat->pSat->stats.conflicts >= pBmc->nConfMax )
225  {
226  RetValue += f + 1;
227  break;
228  }
229  if ( fCheckTargets && Ssw_SemCheckTargets( pBmc ) )
230  break;
231  // transfer latch input to the latch outputs
232  // build logic cones for register outputs
233  Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
234  {
235  pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f);
236  Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
237  Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );
238  }
239 //Abc_Print( 1, "Frame %2d : Conflicts = %6d. \n", f, p->pSat->stats.conflicts );
240  }
241  if ( fFirst )
242  pBmc->nConfMax /= 10;
243 
244  // cleanup
245  Ssw_ClassesCheck( p->ppClasses );
246 p->timeBmc += Abc_Clock() - clk;
247  return RetValue;
248 }
void Ssw_CnfNodeAddToSolver(Ssw_Sat_t *p, Aig_Obj_t *pObj)
Definition: sswCnf.c:351
static Aig_Obj_t * Ssw_ObjChild0Fra(Ssw_Man_t *p, Aig_Obj_t *pObj, int i)
Definition: sswInt.h:185
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
void Ssw_ManFilterBmcSavePattern(Ssw_Sem_t *p)
Definition: sswSemi.c:150
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
int Ssw_SemCheckTargets(Ssw_Sem_t *p)
Definition: sswSemi.c:129
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
typedefABC_NAMESPACE_HEADER_START struct Ssw_Man_t_ Ssw_Man_t
INCLUDES ///.
Definition: sswInt.h:47
static abctime Abc_Clock()
Definition: abc_global.h:279
static Aig_Obj_t * Ssw_ObjChild1Fra(Ssw_Man_t *p, Aig_Obj_t *pObj, int i)
Definition: sswInt.h:186
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
void Ssw_ClassesCheck(Ssw_Cla_t *p)
Definition: sswClass.c:350
int Ssw_ManSweepNode(Ssw_Man_t *p, Aig_Obj_t *pObj, int f, int fBmc, Vec_Int_t *vPairs)
Definition: sswSweep.c:187
Definition: aig.h:69
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static void Ssw_ObjSetFrame(Ssw_Man_t *p, Aig_Obj_t *pObj, int i, Aig_Obj_t *pNode)
Definition: sswInt.h:183
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
ABC_INT64_T abctime
Definition: abc_global.h:278
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
void Ssw_ManFilterBmcSavePattern ( Ssw_Sem_t p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 150 of file sswSemi.c.

151 {
152  unsigned * pInfo;
153  Aig_Obj_t * pObj;
154  int i;
155  if ( p->nPatterns >= p->nPatternsAlloc )
156  return;
157  Saig_ManForEachLo( p->pMan->pAig, pObj, i )
158  {
159  pInfo = (unsigned *)Vec_PtrEntry( p->vPatterns, i );
160  if ( Abc_InfoHasBit( p->pMan->pPatWords, Saig_ManPiNum(p->pMan->pAig) + i ) )
161  Abc_InfoSetBit( pInfo, p->nPatterns );
162  }
163  p->nPatterns++;
164 }
Aig_Man_t * pAig
Definition: llb3Image.c:49
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Definition: aig.h:69
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
int Ssw_SemCheckTargets ( Ssw_Sem_t p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 129 of file sswSemi.c.

130 {
131  Aig_Obj_t * pObj;
132  int i;
133  Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
134  if ( !Ssw_ObjIsConst1Cand(p->pMan->pAig, pObj) )
135  return 1;
136  return 0;
137 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
if(last==0)
Definition: sparse_int.h:34
Definition: aig.h:69
static int Ssw_ObjIsConst1Cand(Aig_Man_t *pAig, Aig_Obj_t *pObj)
Definition: sswInt.h:172
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Ssw_Sem_t* Ssw_SemManStart ( Ssw_Man_t pMan,
int  nConfMax,
int  fVerbose 
)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 64 of file sswSemi.c.

65 {
66  Ssw_Sem_t * p;
67  Aig_Obj_t * pObj;
68  int i;
69  // create interpolation manager
70  p = ABC_ALLOC( Ssw_Sem_t, 1 );
71  memset( p, 0, sizeof(Ssw_Sem_t) );
72  p->nConfMaxStart = nConfMax;
73  p->nConfMax = nConfMax;
74  p->nFramesSweep = Abc_MaxInt( (1<<21)/Aig_ManNodeNum(pMan->pAig), pMan->nFrames );
75  p->fVerbose = fVerbose;
76  // equivalences considered
77  p->pMan = pMan;
78  p->vTargets = Vec_PtrAlloc( Saig_ManPoNum(p->pMan->pAig) );
79  Saig_ManForEachPo( p->pMan->pAig, pObj, i )
80  Vec_PtrPush( p->vTargets, Aig_ObjFanin0(pObj) );
81  // storage for patterns
82  p->nPatternsAlloc = 512;
83  p->nPatterns = 1;
84  p->vPatterns = Vec_PtrAllocSimInfo( Aig_ManRegNum(p->pMan->pAig), Abc_BitWordNum(p->nPatternsAlloc) );
85  Vec_PtrCleanSimInfo( p->vPatterns, 0, Abc_BitWordNum(p->nPatternsAlloc) );
86  p->vHistory = Vec_IntAlloc( 100 );
87  Vec_IntPush( p->vHistory, 0 );
88  // update arrays of the manager
89  assert( 0 );
90 /*
91  ABC_FREE( p->pMan->pNodeToFrames );
92  Vec_IntFree( p->pMan->vSatVars );
93  p->pMan->pNodeToFrames = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pMan->pAig) * p->nFramesSweep );
94  p->pMan->vSatVars = Vec_IntStart( Aig_ManObjNumMax(p->pMan->pAig) * (p->nFramesSweep+1) );
95 */
96  return p;
97 }
char * memset()
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
static void Vec_PtrCleanSimInfo(Vec_Ptr_t *vInfo, int iWord, int nWords)
Definition: vecPtr.h:968
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
typedefABC_NAMESPACE_IMPL_START struct Ssw_Sem_t_ Ssw_Sem_t
DECLARATIONS ///.
Definition: sswSemi.c:30
Definition: aig.h:69
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
#define assert(ex)
Definition: util_old.h:213
static Vec_Ptr_t * Vec_PtrAllocSimInfo(int nEntries, int nWords)
Definition: vecPtr.h:929
void Ssw_SemManStop ( Ssw_Sem_t p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 110 of file sswSemi.c.

111 {
112  Vec_PtrFree( p->vTargets );
113  Vec_PtrFree( p->vPatterns );
114  Vec_IntFree( p->vHistory );
115  ABC_FREE( p );
116 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define ABC_FREE(obj)
Definition: abc_global.h:232
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223