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

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START
Aig_Obj_t
Ssw_BmcUnroll_rec (Ssw_Frm_t *pFrm, Aig_Obj_t *pObj, int f)
 DECLARATIONS ///. More...
 
Abc_Cex_tSsw_BmcGetCounterExample (Ssw_Frm_t *pFrm, Ssw_Sat_t *pSat, int iPo, int iFrame)
 
int Ssw_BmcDynamic (Aig_Man_t *pAig, int nFramesMax, int nConfLimit, int fVerbose, int *piFrame)
 MACRO DEFINITIONS ///. More...
 

Function Documentation

int Ssw_BmcDynamic ( Aig_Man_t pAig,
int  nFramesMax,
int  nConfLimit,
int  fVerbose,
int *  piFrame 
)

MACRO DEFINITIONS ///.

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

Synopsis [Performs BMC for the given AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 126 of file sswBmc.c.

127 {
128  Ssw_Frm_t * pFrm;
129  Ssw_Sat_t * pSat;
130  Aig_Obj_t * pObj, * pObjFrame;
131  int status, Lit, i, f, RetValue;
132  abctime clkPart;
133 
134  // start managers
135  assert( Saig_ManRegNum(pAig) > 0 );
136  Aig_ManSetCioIds( pAig );
137  pSat = Ssw_SatStart( 0 );
138  pFrm = Ssw_FrmStart( pAig );
139  pFrm->pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * 3 );
140  // report statistics
141  if ( fVerbose )
142  {
143  Abc_Print( 1, "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n",
144  Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
145  Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
146  fflush( stdout );
147  }
148  // perform dynamic unrolling
149  RetValue = -1;
150  for ( f = 0; f < nFramesMax; f++ )
151  {
152  clkPart = Abc_Clock();
153  Saig_ManForEachPo( pAig, pObj, i )
154  {
155  // unroll the circuit for this output
156  Ssw_BmcUnroll_rec( pFrm, pObj, f );
157  pObjFrame = Ssw_ObjFrame_( pFrm, pObj, f );
158  Ssw_CnfNodeAddToSolver( pSat, Aig_Regular(pObjFrame) );
159  status = sat_solver_simplify(pSat->pSat);
160  assert( status );
161  // solve
162  Lit = toLitCond( Ssw_ObjSatNum(pSat,pObjFrame), Aig_IsComplement(pObjFrame) );
163  if ( fVerbose )
164  {
165  Abc_Print( 1, "Solving output %2d of frame %3d ... \r",
166  i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
167  }
168  status = sat_solver_solve( pSat->pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
169  if ( status == l_False )
170  {
171 /*
172  Lit = lit_neg( Lit );
173  RetValue = sat_solver_addclause( pSat->pSat, &Lit, &Lit + 1 );
174  assert( RetValue );
175  if ( pSat->pSat->qtail != pSat->pSat->qhead )
176  {
177  RetValue = sat_solver_simplify(pSat->pSat);
178  assert( RetValue );
179  }
180 */
181  RetValue = 1;
182  continue;
183  }
184  else if ( status == l_True )
185  {
186  pAig->pSeqModel = Ssw_BmcGetCounterExample( pFrm, pSat, i, f );
187  if ( piFrame )
188  *piFrame = f;
189  RetValue = 0;
190  break;
191  }
192  else
193  {
194  if ( piFrame )
195  *piFrame = f;
196  RetValue = -1;
197  break;
198  }
199  }
200  if ( fVerbose )
201  {
202  Abc_Print( 1, "Solved %2d outputs of frame %3d. ", Saig_ManPoNum(pAig), f );
203  Abc_Print( 1, "Conf =%8.0f. Var =%8d. AIG=%9d. ",
204  (double)pSat->pSat->stats.conflicts,
205  pSat->nSatVars, Aig_ManNodeNum(pFrm->pFrames) );
206  ABC_PRT( "T", Abc_Clock() - clkPart );
207  clkPart = Abc_Clock();
208  fflush( stdout );
209  }
210  if ( RetValue != 1 )
211  break;
212  }
213 
214  Ssw_SatStop( pSat );
215  Ssw_FrmStop( pFrm );
216  return RetValue;
217 }
void Ssw_CnfNodeAddToSolver(Ssw_Sat_t *p, Aig_Obj_t *pObj)
Definition: sswCnf.c:351
ABC_NAMESPACE_IMPL_START Ssw_Sat_t * Ssw_SatStart(int fPolarFlip)
DECLARATIONS ///.
Definition: sswCnf.c:45
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
#define l_True
Definition: SolverTypes.h:84
ABC_NAMESPACE_IMPL_START Aig_Obj_t * Ssw_BmcUnroll_rec(Ssw_Frm_t *pFrm, Aig_Obj_t *pObj, int f)
DECLARATIONS ///.
Definition: sswBmc.c:45
static abctime Abc_Clock()
Definition: abc_global.h:279
stats_t stats
Definition: satSolver.h:156
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
sat_solver * pSat
Definition: sswInt.h:147
static lit toLitCond(int v, int c)
Definition: satVec.h:143
Aig_Man_t * pFrames
Definition: sswInt.h:161
Definition: aig.h:69
ABC_NAMESPACE_IMPL_START Ssw_Frm_t * Ssw_FrmStart(Aig_Man_t *pAig)
DECLARATIONS ///.
Definition: sswAig.c:45
void Aig_ManSetCioIds(Aig_Man_t *p)
Definition: aigUtil.c:965
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
static Aig_Obj_t * Ssw_ObjFrame_(Ssw_Frm_t *p, Aig_Obj_t *pObj, int i)
Definition: sswInt.h:188
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
int Aig_ManLevelNum(Aig_Man_t *p)
Definition: aigDfs.c:486
ABC_INT64_T conflicts
Definition: satVec.h:154
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Abc_Cex_t * Ssw_BmcGetCounterExample(Ssw_Frm_t *pFrm, Ssw_Sat_t *pSat, int iPo, int iFrame)
Definition: sswBmc.c:90
#define l_False
Definition: SolverTypes.h:85
static int Ssw_ObjSatNum(Ssw_Sat_t *p, Aig_Obj_t *pObj)
MACRO DEFINITIONS ///.
Definition: sswInt.h:169
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
#define assert(ex)
Definition: util_old.h:213
void Ssw_FrmStop(Ssw_Frm_t *p)
Definition: sswAig.c:70
void Ssw_SatStop(Ssw_Sat_t *p)
Definition: sswCnf.c:81
ABC_INT64_T abctime
Definition: abc_global.h:278
int nSatVars
Definition: sswInt.h:148
Abc_Cex_t* Ssw_BmcGetCounterExample ( Ssw_Frm_t pFrm,
Ssw_Sat_t pSat,
int  iPo,
int  iFrame 
)

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

Synopsis [Derives counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 90 of file sswBmc.c.

91 {
92  Abc_Cex_t * pCex;
93  Aig_Obj_t * pObj, * pObjFrames;
94  int f, i, nShift;
95  assert( Saig_ManRegNum(pFrm->pAig) > 0 );
96  // allocate the counter example
97  pCex = Abc_CexAlloc( Saig_ManRegNum(pFrm->pAig), Saig_ManPiNum(pFrm->pAig), iFrame + 1 );
98  pCex->iPo = iPo;
99  pCex->iFrame = iFrame;
100  // create data-bits
101  nShift = Saig_ManRegNum(pFrm->pAig);
102  for ( f = 0; f <= iFrame; f++, nShift += Saig_ManPiNum(pFrm->pAig) )
103  Saig_ManForEachPi( pFrm->pAig, pObj, i )
104  {
105  pObjFrames = Ssw_ObjFrame_(pFrm, pObj, f);
106  if ( pObjFrames == NULL )
107  continue;
108  if ( Ssw_CnfGetNodeValue( pSat, pObjFrames ) )
109  Abc_InfoSetBit( pCex->pData, nShift + i );
110  }
111  return pCex;
112 }
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
Aig_Man_t * pAig
Definition: sswInt.h:158
Definition: aig.h:69
static Aig_Obj_t * Ssw_ObjFrame_(Ssw_Frm_t *p, Aig_Obj_t *pObj, int i)
Definition: sswInt.h:188
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
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
#define assert(ex)
Definition: util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
int Ssw_CnfGetNodeValue(Ssw_Sat_t *p, Aig_Obj_t *pObj)
Definition: sswCnf.c:402
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
ABC_NAMESPACE_IMPL_START Aig_Obj_t* Ssw_BmcUnroll_rec ( Ssw_Frm_t pFrm,
Aig_Obj_t pObj,
int  f 
)

DECLARATIONS ///.

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

FileName [sswBmc.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [Bounded model checker using dynamic unrolling.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

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

Synopsis [Incrementally unroll the timeframes.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sswBmc.c.

46 {
47  Aig_Obj_t * pRes, * pRes0, * pRes1;
48  if ( (pRes = Ssw_ObjFrame_(pFrm, pObj, f)) )
49  return pRes;
50  if ( Aig_ObjIsConst1(pObj) )
51  pRes = Aig_ManConst1( pFrm->pFrames );
52  else if ( Saig_ObjIsPi(pFrm->pAig, pObj) )
53  pRes = Aig_ObjCreateCi( pFrm->pFrames );
54  else if ( Aig_ObjIsCo(pObj) )
55  {
56  Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f );
57  pRes = Ssw_ObjChild0Fra_( pFrm, pObj, f );
58  }
59  else if ( Saig_ObjIsLo(pFrm->pAig, pObj) )
60  {
61  if ( f == 0 )
62  pRes = Aig_ManConst0( pFrm->pFrames );
63  else
64  pRes = Ssw_BmcUnroll_rec( pFrm, Saig_ObjLoToLi(pFrm->pAig, pObj), f-1 );
65  }
66  else
67  {
68  assert( Aig_ObjIsNode(pObj) );
69  Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f );
70  Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin1(pObj), f );
71  pRes0 = Ssw_ObjChild0Fra_( pFrm, pObj, f );
72  pRes1 = Ssw_ObjChild1Fra_( pFrm, pObj, f );
73  pRes = Aig_And( pFrm->pFrames, pRes0, pRes1 );
74  }
75  Ssw_ObjSetFrame_( pFrm, pObj, f, pRes );
76  return pRes;
77 }
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
static Aig_Obj_t * Aig_ManConst0(Aig_Man_t *p)
Definition: aig.h:263
ABC_NAMESPACE_IMPL_START Aig_Obj_t * Ssw_BmcUnroll_rec(Ssw_Frm_t *pFrm, Aig_Obj_t *pObj, int f)
DECLARATIONS ///.
Definition: sswBmc.c:45
static void Ssw_ObjSetFrame_(Ssw_Frm_t *p, Aig_Obj_t *pObj, int i, Aig_Obj_t *pNode)
Definition: sswInt.h:189
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Aig_Man_t * pAig
Definition: sswInt.h:158
Aig_Man_t * pFrames
Definition: sswInt.h:161
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Definition: aig.h:69
static Aig_Obj_t * Ssw_ObjFrame_(Ssw_Frm_t *p, Aig_Obj_t *pObj, int i)
Definition: sswInt.h:188
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
#define assert(ex)
Definition: util_old.h:213
static Aig_Obj_t * Ssw_ObjChild1Fra_(Ssw_Frm_t *p, Aig_Obj_t *pObj, int i)
Definition: sswInt.h:192
static Aig_Obj_t * Ssw_ObjChild0Fra_(Ssw_Frm_t *p, Aig_Obj_t *pObj, int i)
Definition: sswInt.h:191
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276