1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
|
/**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 $]
***********************************************************************/
#include "base/abc/abc.h"
#include "sat/cnf/cnf.h"
ABC_NAMESPACE_IMPL_START
/*
Implementation of a simple QBF solver along the lines of
A. Solar-Lezama, L. Tancau, R. Bodik, V. Saraswat, and S. Seshia,
"Combinatorial sketching for finite programs", 12th International
Conference on Architectural Support for Programming Languages and
Operating Systems (ASPLOS 2006), San Jose, CA, October 2006.
*/
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Abc_NtkModelToVector( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues );
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 );
extern 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 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 []
***********************************************************************/
void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nItersMax, int fDumpCnf, int fVerbose )
{
Abc_Ntk_t * pNtkVer, * pNtkSyn, * pNtkSyn2, * pNtkTemp;
Vec_Int_t * vPiValues;
abctime clkTotal = Abc_Clock(), clkS, clkV;
int nIters, nInputs, RetValue, fFound = 0;
assert( Abc_NtkIsStrash(pNtk) );
assert( Abc_NtkIsComb(pNtk) );
assert( Abc_NtkPoNum(pNtk) == 1 );
assert( nPars > 0 && nPars < Abc_NtkPiNum(pNtk) );
// assert( Abc_NtkPiNum(pNtk)-nPars < 32 );
nInputs = Abc_NtkPiNum(pNtk) - nPars;
if ( fDumpCnf )
{
// original problem: \exists p \forall x \exists y. M(p,x,y)
// negated problem: \forall p \exists x \exists y. !M(p,x,y)
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pMan = Abc_NtkToDar( pNtk, 0, 0 );
Cnf_Dat_t * pCnf = Cnf_Derive( pMan, 0 );
Vec_Int_t * vVarMap, * vForAlls, * vExists;
Aig_Obj_t * pObj;
char * pFileName;
int i, Entry;
// create var map
vVarMap = Vec_IntStart( pCnf->nVars );
Aig_ManForEachCi( pMan, pObj, i )
if ( i < nPars )
Vec_IntWriteEntry( vVarMap, pCnf->pVarNums[Aig_ObjId(pObj)], 1 );
// create various maps
vForAlls = Vec_IntAlloc( nPars );
vExists = Vec_IntAlloc( Abc_NtkPiNum(pNtk) - nPars );
Vec_IntForEachEntry( vVarMap, Entry, i )
if ( Entry )
Vec_IntPush( vForAlls, i );
else
Vec_IntPush( vExists, i );
// generate CNF
pFileName = Extra_FileNameGenericAppend( pNtk->pSpec, ".qdimacs" );
Cnf_DataWriteIntoFile( pCnf, pFileName, 0, vForAlls, vExists );
Aig_ManStop( pMan );
Cnf_DataFree( pCnf );
Vec_IntFree( vForAlls );
Vec_IntFree( vExists );
Vec_IntFree( vVarMap );
printf( "The 2QBF formula was written into file \"%s\".\n", pFileName );
return;
}
// initialize the synthesized network with 0000-combination
vPiValues = Vec_IntStart( Abc_NtkPiNum(pNtk) );
// create random init value
{
int i;
srand( time(NULL) );
for ( i = nPars; i < Abc_NtkPiNum(pNtk); i++ )
Vec_IntWriteEntry( vPiValues, i, rand() & 1 );
}
Abc_NtkVectorClearPars( vPiValues, nPars );
pNtkSyn = Abc_NtkMiterCofactor( pNtk, vPiValues );
if ( fVerbose )
{
printf( "Iter %2d : ", 0 );
printf( "AIG = %6d ", Abc_NtkNodeNum(pNtkSyn) );
Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars );
printf( "\n" );
}
// iteratively solve
for ( nIters = 0; nIters < nItersMax; nIters++ )
{
// solve the synthesis instance
clkS = Abc_Clock();
// RetValue = Abc_NtkMiterSat( pNtkSyn, 0, 0, 0, NULL, NULL );
RetValue = Abc_NtkDSat( pNtkSyn, (ABC_INT64_T)0, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
clkS = Abc_Clock() - clkS;
if ( RetValue == 0 )
Abc_NtkModelToVector( pNtkSyn, vPiValues );
if ( RetValue == 1 )
{
break;
}
if ( RetValue == -1 )
{
printf( "Synthesis timed out.\n" );
break;
}
// there is a counter-example
// construct the verification instance
Abc_NtkVectorClearVars( pNtk, vPiValues, nPars );
pNtkVer = Abc_NtkMiterCofactor( pNtk, vPiValues );
// complement the output
Abc_ObjXorFaninC( Abc_NtkPo(pNtkVer,0), 0 );
// solve the verification instance
clkV = Abc_Clock();
RetValue = Abc_NtkMiterSat( pNtkVer, 0, 0, 0, NULL, NULL );
clkV = Abc_Clock() - clkV;
if ( RetValue == 0 )
Abc_NtkModelToVector( pNtkVer, vPiValues );
Abc_NtkDelete( pNtkVer );
if ( RetValue == 1 )
{
fFound = 1;
break;
}
if ( RetValue == -1 )
{
printf( "Verification timed out.\n" );
break;
}
// there is a counter-example
// create a new synthesis network
Abc_NtkVectorClearPars( vPiValues, nPars );
pNtkSyn2 = Abc_NtkMiterCofactor( pNtk, vPiValues );
// add to the synthesis instance
pNtkSyn = Abc_NtkMiterAnd( pNtkTemp = pNtkSyn, pNtkSyn2, 0, 0 );
Abc_NtkDelete( pNtkSyn2 );
Abc_NtkDelete( pNtkTemp );
if ( fVerbose )
{
printf( "Iter %2d : ", nIters+1 );
printf( "AIG = %6d ", Abc_NtkNodeNum(pNtkSyn) );
Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars );
printf( " " );
ABC_PRT( "Syn", clkS );
// ABC_PRT( "Ver", clkV );
}
}
Abc_NtkDelete( pNtkSyn );
// report the results
if ( fFound )
{
int nZeros = Vec_IntCountZero( vPiValues );
printf( "Parameters: " );
Abc_NtkVectorPrintPars( vPiValues, nPars );
printf( " Statistics: 0=%d 1=%d\n", nZeros, Vec_IntSize(vPiValues) - nZeros );
printf( "Solved after %d iterations. ", nIters );
}
else if ( nIters == nItersMax )
printf( "Quit after %d iterations. ", nItersMax );
else
printf( "Implementation does not exist. " );
ABC_PRT( "Total runtime", Abc_Clock() - clkTotal );
Vec_IntFree( vPiValues );
}
/**Function*************************************************************
Synopsis [Translates model into the vector of values.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkModelToVector( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues )
{
int * pModel, i;
pModel = pNtk->pModel;
for ( i = 0; i < Abc_NtkPiNum(pNtk); i++ )
Vec_IntWriteEntry( vPiValues, i, pModel[i] );
}
/**Function*************************************************************
Synopsis [Clears parameters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkVectorClearPars( Vec_Int_t * vPiValues, int nPars )
{
int i;
for ( i = 0; i < nPars; i++ )
Vec_IntWriteEntry( vPiValues, i, -1 );
}
/**Function*************************************************************
Synopsis [Clears variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkVectorClearVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars )
{
int i;
for ( i = nPars; i < Abc_NtkPiNum(pNtk); i++ )
Vec_IntWriteEntry( vPiValues, i, -1 );
}
/**Function*************************************************************
Synopsis [Clears variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkVectorPrintPars( Vec_Int_t * vPiValues, int nPars )
{
int i;
for ( i = 0; i < nPars; i++ )
printf( "%d", Vec_IntEntry(vPiValues,i) );
}
/**Function*************************************************************
Synopsis [Clears variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkVectorPrintVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars )
{
int i;
for ( i = nPars; i < Abc_NtkPiNum(pNtk); i++ )
printf( "%d", Vec_IntEntry(vPiValues,i) );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
|
