abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions
abcQbf.c File Reference
#include "base/abc/abc.h"
#include "sat/cnf/cnf.h"

Go to the source code of this file.

Functions

static
ABC_NAMESPACE_IMPL_START void 		Abc_NtkModelToVector (Abc_Ntk_t *pNtk, Vec_Int_t *vPiValues)
 DECLARATIONS ///. More...
 
static void Abc_NtkVectorClearPars (Vec_Int_t *vPiValues, int nPars)
 
static void Abc_NtkVectorClearVars (Abc_Ntk_t *pNtk, Vec_Int_t *vPiValues, int nPars)
 
static void Abc_NtkVectorPrintPars (Vec_Int_t *vPiValues, int nPars)
 
static void Abc_NtkVectorPrintVars (Abc_Ntk_t *pNtk, Vec_Int_t *vPiValues, int nPars)
 
int Abc_NtkDSat (Abc_Ntk_t *pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose)
 
void Abc_NtkQbf (Abc_Ntk_t *pNtk, int nPars, int nItersMax, int fDumpCnf, int fVerbose)
 FUNCTION DEFINITIONS ///. More...
 

Function Documentation

int Abc_NtkDSat ( Abc_Ntk_t *  pNtk,
ABC_INT64_T  nConfLimit,
ABC_INT64_T  nInsLimit,
int  nLearnedStart,
int  nLearnedDelta,
int  nLearnedPerce,
int  fAlignPol,
int  fAndOuts,
int  fNewSolver,
int  fVerbose 
)

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

Synopsis [Solves combinational miter using a SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 1804 of file abcDar.c.

1805 {
1806  Aig_Man_t * pMan;
1807  int RetValue;//, clk = Abc_Clock();
1808  assert( Abc_NtkIsStrash(pNtk) );
1809  assert( Abc_NtkLatchNum(pNtk) == 0 );
1810 // assert( Abc_NtkPoNum(pNtk) == 1 );
1811  pMan = Abc_NtkToDar( pNtk, 0, 0 );
1812  RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fAlignPol, fAndOuts, fNewSolver, fVerbose );
1813  pNtk->pModel = (int *)pMan->pData, pMan->pData = NULL;
1814  Aig_ManStop( pMan );
1815  return RetValue;
1816 }
Abc_NtkIsStrash
static int Abc_NtkIsStrash(Abc_Ntk_t *pNtk)
Definition: abc.h:251
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Abc_NtkLatchNum
static int Abc_NtkLatchNum(Abc_Ntk_t *pNtk)
Definition: abc.h:294
Abc_Ntk_t_::pModel
int * pModel
Definition: abc.h:198
assert
#define assert(ex)
Definition: util_old.h:213
Fra_FraigSat
int Fra_FraigSat(Aig_Man_t *pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose)
ITERATORS ///.
Definition: fraCec.c:47
Abc_NtkToDar
Aig_Man_t * Abc_NtkToDar(Abc_Ntk_t *pNtk, int fExors, int fRegisters)
DECLARATIONS ///.
Definition: abcDar.c:233
void Abc_NtkModelToVector ( Abc_Ntk_t *  pNtk,
Vec_Int_t *  vPiValues 
)
static

DECLARATIONS ///.

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

FileName [abcQbf.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Implementation of a simple QBF solver.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]

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

Synopsis [Translates model into the vector of values.]

Description []

SideEffects []

SeeAlso []

Definition at line 232 of file abcQbf.c.

233 {
234  int * pModel, i;
235  pModel = pNtk->pModel;
236  for ( i = 0; i < Abc_NtkPiNum(pNtk); i++ )
237  Vec_IntWriteEntry( vPiValues, i, pModel[i] );
238 }
Abc_Ntk_t_::pModel
int * pModel
Definition: abc.h:198
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Abc_NtkPiNum
static int Abc_NtkPiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:285
void Abc_NtkQbf ( Abc_Ntk_t *  pNtk,
int  nPars,
int  nItersMax,
int  fDumpCnf,
int  fVerbose 
)

FUNCTION DEFINITIONS ///.

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

Synopsis [Solve the QBF problem EpAx[M(p,x)].]

Description [Variables p go first, followed by variable x. The number of parameters is nPars. The miter is in pNtk. The miter expresses EQUALITY of the implementation and spec.]

SideEffects []

SeeAlso []

Definition at line 64 of file abcQbf.c.

65 {
66  Abc_Ntk_t * pNtkVer, * pNtkSyn, * pNtkSyn2, * pNtkTemp;
67  Vec_Int_t * vPiValues;
68  abctime clkTotal = Abc_Clock(), clkS, clkV;
69  int nIters, nInputs, RetValue, fFound = 0;
70 
71  assert( Abc_NtkIsStrash(pNtk) );
72  assert( Abc_NtkIsComb(pNtk) );
73  assert( Abc_NtkPoNum(pNtk) == 1 );
74  assert( nPars > 0 && nPars < Abc_NtkPiNum(pNtk) );
75 // assert( Abc_NtkPiNum(pNtk)-nPars < 32 );
76  nInputs = Abc_NtkPiNum(pNtk) - nPars;
77 
78  if ( fDumpCnf )
79  {
80  // original problem: \exists p \forall x \exists y. M(p,x,y)
81  // negated problem: \forall p \exists x \exists y. !M(p,x,y)
82  extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
83  Aig_Man_t * pMan = Abc_NtkToDar( pNtk, 0, 0 );
84  Cnf_Dat_t * pCnf = Cnf_Derive( pMan, 0 );
85  Vec_Int_t * vVarMap, * vForAlls, * vExists;
86  Aig_Obj_t * pObj;
87  char * pFileName;
88  int i, Entry;
89  // create var map
90  vVarMap = Vec_IntStart( pCnf->nVars );
91  Aig_ManForEachCi( pMan, pObj, i )
92  if ( i < nPars )
93  Vec_IntWriteEntry( vVarMap, pCnf->pVarNums[Aig_ObjId(pObj)], 1 );
94  // create various maps
95  vForAlls = Vec_IntAlloc( nPars );
96  vExists = Vec_IntAlloc( Abc_NtkPiNum(pNtk) - nPars );
97  Vec_IntForEachEntry( vVarMap, Entry, i )
98  if ( Entry )
99  Vec_IntPush( vForAlls, i );
100  else
101  Vec_IntPush( vExists, i );
102  // generate CNF
103  pFileName = Extra_FileNameGenericAppend( pNtk->pSpec, ".qdimacs" );
104  Cnf_DataWriteIntoFile( pCnf, pFileName, 0, vForAlls, vExists );
105  Aig_ManStop( pMan );
106  Cnf_DataFree( pCnf );
107  Vec_IntFree( vForAlls );
108  Vec_IntFree( vExists );
109  Vec_IntFree( vVarMap );
110  printf( "The 2QBF formula was written into file \"%s\".\n", pFileName );
111  return;
112  }
113 
114  // initialize the synthesized network with 0000-combination
115  vPiValues = Vec_IntStart( Abc_NtkPiNum(pNtk) );
116 
117  // create random init value
118  {
119  int i;
120  srand( time(NULL) );
121  for ( i = nPars; i < Abc_NtkPiNum(pNtk); i++ )
122  Vec_IntWriteEntry( vPiValues, i, rand() & 1 );
123  }
124 
125  Abc_NtkVectorClearPars( vPiValues, nPars );
126  pNtkSyn = Abc_NtkMiterCofactor( pNtk, vPiValues );
127  if ( fVerbose )
128  {
129  printf( "Iter %2d : ", 0 );
130  printf( "AIG = %6d ", Abc_NtkNodeNum(pNtkSyn) );
131  Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars );
132  printf( "\n" );
133  }
134 
135  // iteratively solve
136  for ( nIters = 0; nIters < nItersMax; nIters++ )
137  {
138  // solve the synthesis instance
139 clkS = Abc_Clock();
140 // RetValue = Abc_NtkMiterSat( pNtkSyn, 0, 0, 0, NULL, NULL );
141  RetValue = Abc_NtkDSat( pNtkSyn, (ABC_INT64_T)0, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
142 clkS = Abc_Clock() - clkS;
143  if ( RetValue == 0 )
144  Abc_NtkModelToVector( pNtkSyn, vPiValues );
145  if ( RetValue == 1 )
146  {
147  break;
148  }
149  if ( RetValue == -1 )
150  {
151  printf( "Synthesis timed out.\n" );
152  break;
153  }
154  // there is a counter-example
155 
156  // construct the verification instance
157  Abc_NtkVectorClearVars( pNtk, vPiValues, nPars );
158  pNtkVer = Abc_NtkMiterCofactor( pNtk, vPiValues );
159  // complement the output
160  Abc_ObjXorFaninC( Abc_NtkPo(pNtkVer,0), 0 );
161 
162  // solve the verification instance
163 clkV = Abc_Clock();
164  RetValue = Abc_NtkMiterSat( pNtkVer, 0, 0, 0, NULL, NULL );
165 clkV = Abc_Clock() - clkV;
166  if ( RetValue == 0 )
167  Abc_NtkModelToVector( pNtkVer, vPiValues );
168  Abc_NtkDelete( pNtkVer );
169  if ( RetValue == 1 )
170  {
171  fFound = 1;
172  break;
173  }
174  if ( RetValue == -1 )
175  {
176  printf( "Verification timed out.\n" );
177  break;
178  }
179  // there is a counter-example
180 
181  // create a new synthesis network
182  Abc_NtkVectorClearPars( vPiValues, nPars );
183  pNtkSyn2 = Abc_NtkMiterCofactor( pNtk, vPiValues );
184  // add to the synthesis instance
185  pNtkSyn = Abc_NtkMiterAnd( pNtkTemp = pNtkSyn, pNtkSyn2, 0, 0 );
186  Abc_NtkDelete( pNtkSyn2 );
187  Abc_NtkDelete( pNtkTemp );
188 
189  if ( fVerbose )
190  {
191  printf( "Iter %2d : ", nIters+1 );
192  printf( "AIG = %6d ", Abc_NtkNodeNum(pNtkSyn) );
193  Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars );
194  printf( " " );
195  ABC_PRT( "Syn", clkS );
196 // ABC_PRT( "Ver", clkV );
197  }
198  if ( nIters+1 == nItersMax )
199  break;
200  }
201  Abc_NtkDelete( pNtkSyn );
202  // report the results
203  if ( fFound )
204  {
205  printf( "Parameters: " );
206  Abc_NtkVectorPrintPars( vPiValues, nPars );
207  printf( "\n" );
208  printf( "Solved after %d interations. ", nIters );
209  }
210  else if ( nIters == nItersMax )
211  printf( "Unsolved after %d interations. ", nIters );
212  else if ( nIters == nItersMax )
213  printf( "Quit after %d interatios. ", nItersMax );
214  else
215  printf( "Implementation does not exist. " );
216  ABC_PRT( "Total runtime", Abc_Clock() - clkTotal );
217  Vec_IntFree( vPiValues );
218 }
Abc_NtkIsStrash
static int Abc_NtkIsStrash(Abc_Ntk_t *pNtk)
Definition: abc.h:251
Abc_NtkIsComb
static int Abc_NtkIsComb(Abc_Ntk_t *pNtk)
Definition: abc.h:297
Cnf_Derive
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition: cnfCore.c:165
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Cnf_DataWriteIntoFile
void Cnf_DataWriteIntoFile(Cnf_Dat_t *p, char *pFileName, int fReadable, Vec_Int_t *vForAlls, Vec_Int_t *vExists)
Definition: cnfMan.c:318
Abc_Ntk_t_
Definition: abc.h:153
Cnf_Dat_t_::nVars
int nVars
Definition: cnf.h:59
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Cnf_Dat_t_
Definition: cnf.h:56
Abc_NtkDSat
int Abc_NtkDSat(Abc_Ntk_t *pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose)
Definition: abcDar.c:1804
Abc_NtkDelete
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:1233
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Abc_NtkNodeNum
static int Abc_NtkNodeNum(Abc_Ntk_t *pNtk)
Definition: abc.h:293
Abc_NtkModelToVector
static ABC_NAMESPACE_IMPL_START void Abc_NtkModelToVector(Abc_Ntk_t *pNtk, Vec_Int_t *vPiValues)
DECLARATIONS ///.
Definition: abcQbf.c:232
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Abc_NtkVectorClearPars
static void Abc_NtkVectorClearPars(Vec_Int_t *vPiValues, int nPars)
Definition: abcQbf.c:251
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Abc_NtkToDar
Aig_Man_t * Abc_NtkToDar(Abc_Ntk_t *pNtk, int fExors, int fRegisters)
Definition: abcDar.c:233
if
if(last==0)
Definition: sparse_int.h:34
else
else
Definition: sparse_int.h:55
Abc_NtkMiterSat
ABC_DLL int Abc_NtkMiterSat(Abc_Ntk_t *pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fVerbose, ABC_INT64_T *pNumConfs, ABC_INT64_T *pNumInspects)
FUNCTION DEFINITIONS ///.
Definition: abcSat.c:53
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Abc_NtkMiterCofactor
ABC_DLL Abc_Ntk_t * Abc_NtkMiterCofactor(Abc_Ntk_t *pNtk, Vec_Int_t *vPiValues)
Definition: abcMiter.c:447
Abc_NtkVectorPrintPars
static void Abc_NtkVectorPrintPars(Vec_Int_t *vPiValues, int nPars)
Definition: abcQbf.c:287
Abc_NtkVectorPrintVars
static void Abc_NtkVectorPrintVars(Abc_Ntk_t *pNtk, Vec_Int_t *vPiValues, int nPars)
Definition: abcQbf.c:305
Abc_NtkPo
static Abc_Obj_t * Abc_NtkPo(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:316
Abc_NtkPoNum
static int Abc_NtkPoNum(Abc_Ntk_t *pNtk)
Definition: abc.h:286
Abc_NtkPiNum
static int Abc_NtkPiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:285
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Abc_NtkVectorClearVars
static void Abc_NtkVectorClearVars(Abc_Ntk_t *pNtk, Vec_Int_t *vPiValues, int nPars)
Definition: abcQbf.c:269
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
Abc_ObjXorFaninC
static void Abc_ObjXorFaninC(Abc_Obj_t *pObj, int i)
Definition: abc.h:381
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
assert
#define assert(ex)
Definition: util_old.h:213
Extra_FileNameGenericAppend
char * Extra_FileNameGenericAppend(char *pBase, char *pSuffix)
Definition: extraUtilFile.c:185
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Abc_NtkMiterAnd
ABC_DLL Abc_Ntk_t * Abc_NtkMiterAnd(Abc_Ntk_t *pNtk1, Abc_Ntk_t *pNtk2, int fOr, int fCompl2)
Definition: abcMiter.c:384
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
void Abc_NtkVectorClearPars ( Vec_Int_t *  vPiValues,
int  nPars 
)
static

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

Synopsis [Clears parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 251 of file abcQbf.c.

252 {
253  int i;
254  for ( i = 0; i < nPars; i++ )
255  Vec_IntWriteEntry( vPiValues, i, -1 );
256 }
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
void Abc_NtkVectorClearVars ( Abc_Ntk_t *  pNtk,
Vec_Int_t *  vPiValues,
int  nPars 
)
static

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

Synopsis [Clears variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 269 of file abcQbf.c.

270 {
271  int i;
272  for ( i = nPars; i < Abc_NtkPiNum(pNtk); i++ )
273  Vec_IntWriteEntry( vPiValues, i, -1 );
274 }
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Abc_NtkPiNum
static int Abc_NtkPiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:285
void Abc_NtkVectorPrintPars ( Vec_Int_t *  vPiValues,
int  nPars 
)
static

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

Synopsis [Clears variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 287 of file abcQbf.c.

288 {
289  int i;
290  for ( i = 0; i < nPars; i++ )
291  printf( "%d", Vec_IntEntry(vPiValues,i) );
292 }
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
void Abc_NtkVectorPrintVars ( Abc_Ntk_t *  pNtk,
Vec_Int_t *  vPiValues,
int  nPars 
)
static

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

Synopsis [Clears variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 305 of file abcQbf.c.

306 {
307  int i;
308  for ( i = nPars; i < Abc_NtkPiNum(pNtk); i++ )
309  printf( "%d", Vec_IntEntry(vPiValues,i) );
310 }
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Abc_NtkPiNum
static int Abc_NtkPiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:285