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
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
|
/**CFile****************************************************************
FileName [pdrTsim3.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Property driven reachability.]
Synopsis [Improved ternary simulation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - November 20, 2010.]
Revision [$Id: pdrTsim3.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "pdrInt.h"
#include "aig/gia/giaAig.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
struct Txs3_Man_t_
{
Gia_Man_t * pGia; // user's AIG
Vec_Int_t * vPrio; // priority of each flop
Vec_Int_t * vCiObjs; // cone leaves (CI obj IDs)
Vec_Int_t * vFosPre; // cone leaves (CI obj IDs)
Vec_Int_t * vFosAbs; // cone leaves (CI obj IDs)
Vec_Int_t * vCoObjs; // cone roots (CO obj IDs)
Vec_Int_t * vCiVals; // cone leaf values (0/1 CI values)
Vec_Int_t * vCoVals; // cone root values (0/1 CO values)
Vec_Int_t * vNodes; // cone nodes (node obj IDs)
Vec_Int_t * vTemp; // cone nodes (node obj IDs)
Vec_Int_t * vPiLits; // resulting array of PI literals
Vec_Int_t * vFfLits; // resulting array of flop literals
Pdr_Man_t * pMan; // calling manager
int nPiLits; // the number of PI literals
};
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Start and stop the ternary simulation engine.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Txs3_Man_t * Txs3_ManStart( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio )
{
Txs3_Man_t * p;
// Aig_Obj_t * pObj;
// int i;
assert( Vec_IntSize(vPrio) == Aig_ManRegNum(pAig) );
p = ABC_CALLOC( Txs3_Man_t, 1 );
p->pGia = Gia_ManFromAigSimple(pAig); // user's AIG
// Aig_ManForEachObj( pAig, pObj, i )
// assert( i == 0 || pObj->iData == Abc_Var2Lit(i, 0) );
p->vPrio = vPrio; // priority of each flop
p->vCiObjs = Vec_IntAlloc( 100 ); // cone leaves (CI obj IDs)
p->vFosPre = Vec_IntAlloc( 100 ); // present flop outputs
p->vFosAbs = Vec_IntAlloc( 100 ); // absracted flop outputs
p->vCoObjs = Vec_IntAlloc( 100 ); // cone roots (CO obj IDs)
p->vCiVals = Vec_IntAlloc( 100 ); // cone leaf values (0/1 CI values)
p->vCoVals = Vec_IntAlloc( 100 ); // cone root values (0/1 CO values)
p->vNodes = Vec_IntAlloc( 100 ); // cone nodes (node obj IDs)
p->vTemp = Vec_IntAlloc( 100 ); // cone nodes (node obj IDs)
p->vPiLits = Vec_IntAlloc( 100 ); // resulting array of PI literals
p->vFfLits = Vec_IntAlloc( 100 ); // resulting array of flop literals
p->pMan = pMan; // calling manager
return p;
}
void Txs3_ManStop( Txs3_Man_t * p )
{
Gia_ManStop( p->pGia );
Vec_IntFree( p->vCiObjs );
Vec_IntFree( p->vFosPre );
Vec_IntFree( p->vFosAbs );
Vec_IntFree( p->vCoObjs );
Vec_IntFree( p->vCiVals );
Vec_IntFree( p->vCoVals );
Vec_IntFree( p->vNodes );
Vec_IntFree( p->vTemp );
Vec_IntFree( p->vPiLits );
Vec_IntFree( p->vFfLits );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Marks the TFI cone and collects CIs and nodes.]
Description [For this procedure to work Value should not be ~0
at the beginning.]
SideEffects []
SeeAlso []
***********************************************************************/
void Txs3_ManCollectCone_rec( Txs3_Man_t * p, Gia_Obj_t * pObj )
{
if ( !~pObj->Value )
return;
pObj->Value = ~0;
if ( Gia_ObjIsCi(pObj) )
{
int Entry;
if ( Gia_ObjIsPi(p->pGia, pObj) )
{
Vec_IntPush( p->vCiObjs, Gia_ObjId(p->pGia, pObj) );
return;
}
Entry = Gia_ObjCioId(pObj) - Gia_ManPiNum(p->pGia);
if ( Vec_IntEntry(p->vPrio, Entry) ) // present flop
Vec_IntPush( p->vFosPre, Gia_ObjId(p->pGia, pObj) );
else // asbstracted flop
Vec_IntPush( p->vFosAbs, Gia_ObjId(p->pGia, pObj) );
return;
}
assert( Gia_ObjIsAnd(pObj) );
Txs3_ManCollectCone_rec( p, Gia_ObjFanin0(pObj) );
Txs3_ManCollectCone_rec( p, Gia_ObjFanin1(pObj) );
Vec_IntPush( p->vNodes, Gia_ObjId(p->pGia, pObj) );
}
void Txs3_ManCollectCone( Txs3_Man_t * p, int fVerbose )
{
Gia_Obj_t * pObj; int i, Entry;
// printf( "Collecting cones for clause with %d literals.\n", Vec_IntSize(vCoObjs) );
Vec_IntClear( p->vCiObjs );
Vec_IntClear( p->vFosPre );
Vec_IntClear( p->vFosAbs );
Vec_IntClear( p->vNodes );
Gia_ManConst0(p->pGia)->Value = ~0;
Gia_ManForEachObjVec( p->vCoObjs, p->pGia, pObj, i )
Txs3_ManCollectCone_rec( p, Gia_ObjFanin0(pObj) );
if ( fVerbose )
printf( "%d %d %d \n", Vec_IntSize(p->vCiObjs), Vec_IntSize(p->vFosPre), Vec_IntSize(p->vFosAbs) );
p->nPiLits = Vec_IntSize(p->vCiObjs);
// sort primary inputs
Vec_IntSelectSort( Vec_IntArray(p->vCiObjs), Vec_IntSize(p->vCiObjs) );
// sort and add present flop variables
Vec_IntSelectSortReverse( Vec_IntArray(p->vFosPre), Vec_IntSize(p->vFosPre) );
Vec_IntForEachEntry( p->vFosPre, Entry, i )
Vec_IntPush( p->vCiObjs, Entry );
// sort and add absent flop variables
Vec_IntSelectSortReverse( Vec_IntArray(p->vFosAbs), Vec_IntSize(p->vFosAbs) );
Vec_IntForEachEntry( p->vFosAbs, Entry, i )
Vec_IntPush( p->vCiObjs, Entry );
// cleanup
Gia_ManForEachObjVec( p->vCiObjs, p->pGia, pObj, i )
pObj->Value = 0;
Gia_ManForEachObjVec( p->vNodes, p->pGia, pObj, i )
pObj->Value = 0;
}
/**Function*************************************************************
Synopsis [Shrinks values using ternary simulation.]
Description [The cube contains the set of flop index literals which,
when converted into a clause and applied to the combinational outputs,
led to a satisfiable SAT run in frame k (values stored in the SAT solver).
If the cube is NULL, it is assumed that the first property output was
asserted and failed.
The resulting array is a set of flop index literals that asserts the COs.
Priority contains 0 for i-th entry if the i-th FF is desirable to remove.]
SideEffects []
SeeAlso []
***********************************************************************/
Pdr_Set_t * Txs3_ManTernarySim( Txs3_Man_t * p, int k, Pdr_Set_t * pCube )
{
// int fTryNew = 1;
// int fUseLit = 1;
int fVerbose = 0;
sat_solver * pSat;
Pdr_Set_t * pRes;
Gia_Obj_t * pObj;
Vec_Int_t * vVar2Ids, * vLits;
int i, Lit, LitAux, Var, Value, RetValue, nCoreLits, * pCoreLits;//, nLits;
// if ( k == 0 )
// fVerbose = 1;
// collect CO objects
Vec_IntClear( p->vCoObjs );
if ( pCube == NULL ) // the target is the property output
{
pObj = Gia_ManCo(p->pGia, p->pMan->iOutCur);
Vec_IntPush( p->vCoObjs, Gia_ObjId(p->pGia, pObj) );
}
else // the target is the cube
{
int i;
for ( i = 0; i < pCube->nLits; i++ )
{
if ( pCube->Lits[i] == -1 )
continue;
pObj = Gia_ManCo(p->pGia, Gia_ManPoNum(p->pGia) + Abc_Lit2Var(pCube->Lits[i]));
Vec_IntPush( p->vCoObjs, Gia_ObjId(p->pGia, pObj) );
}
}
if ( 0 )
{
Abc_Print( 1, "Trying to justify cube " );
if ( pCube )
Pdr_SetPrint( stdout, pCube, Gia_ManRegNum(p->pGia), NULL );
else
Abc_Print( 1, "<prop=fail>" );
Abc_Print( 1, " in frame %d.\n", k );
}
// collect CI objects
Txs3_ManCollectCone( p, fVerbose );
// collect values
Pdr_ManCollectValues( p->pMan, k, p->vCiObjs, p->vCiVals );
Pdr_ManCollectValues( p->pMan, k, p->vCoObjs, p->vCoVals );
// read solver
pSat = Pdr_ManFetchSolver( p->pMan, k );
LitAux = Abc_Var2Lit( Pdr_ManFreeVar(p->pMan, k), 0 );
// add the clause (complemented cube) in terms of next state variables
if ( pCube == NULL ) // the target is the property output
{
vLits = p->pMan->vLits;
Lit = Abc_Var2Lit( Pdr_ObjSatVar(p->pMan, k, 2, Aig_ManCo(p->pMan->pAig, p->pMan->iOutCur)), 1 ); // neg literal (property holds)
Vec_IntFill( vLits, 1, Lit );
}
else
vLits = Pdr_ManCubeToLits( p->pMan, k, pCube, 1, 1 );
// add activation literal
Vec_IntPush( vLits, LitAux );
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
assert( RetValue == 1 );
sat_solver_compress( pSat );
// collect assumptions
Vec_IntClear( p->vTemp );
Vec_IntPush( p->vTemp, Abc_LitNot(LitAux) );
// iterate through the values of the CI variables
Vec_IntForEachEntryTwo( p->vCiObjs, p->vCiVals, Var, Value, i )
{
Aig_Obj_t * pObj = Aig_ManObj( p->pMan->pAig, Var );
// iVar = Pdr_ObjSatVar( p->pMan, k, fNext ? 2 - lit_sign(pCube->Lits[i]) : 3, pObj ); assert( iVar >= 0 );
int iVar = Pdr_ObjSatVar( p->pMan, k, 3, pObj ); assert( iVar >= 0 );
assert( Aig_ObjIsCi(pObj) );
Vec_IntPush( p->vTemp, Abc_Var2Lit(iVar, !Value) );
}
if ( fVerbose )
{
printf( "Clause with %d lits on lev %d\n", pCube ? pCube->nLits : 0, k );
Vec_IntPrint( p->vTemp );
}
/*
// solve with assumptions
//printf( "%d -> ", Vec_IntSize(p->vTemp) );
{
abctime clk = Abc_Clock();
// assume all except flops
Vec_IntForEachEntryStop( p->vTemp, Lit, i, p->nPiLits + 1 )
if ( !sat_solver_push(pSat, Lit) )
{
assert( 0 );
}
nLits = sat_solver_minimize_assumptions( pSat, Vec_IntArray(p->vTemp) + p->nPiLits + 1, Vec_IntSize(p->vTemp) - p->nPiLits - 1, p->pMan->pPars->nConfLimit );
Vec_IntShrink( p->vTemp, p->nPiLits + 1 + nLits );
p->pMan->tAbs += Abc_Clock() - clk;
for ( i = 0; i <= p->nPiLits; i++ )
sat_solver_pop(pSat);
}
//printf( "%d ", nLits );
*/
//check one last time
RetValue = sat_solver_solve( pSat, Vec_IntArray(p->vTemp), Vec_IntLimit(p->vTemp), 0, 0, 0, 0 );
assert( RetValue == l_False );
// use analyze final
nCoreLits = sat_solver_final(pSat, &pCoreLits);
//assert( Vec_IntSize(p->vTemp) <= nCoreLits );
Vec_IntClear( p->vTemp );
for ( i = 0; i < nCoreLits; i++ )
Vec_IntPush( p->vTemp, Abc_LitNot(pCoreLits[i]) );
Vec_IntSelectSort( Vec_IntArray(p->vTemp), Vec_IntSize(p->vTemp) );
if ( fVerbose )
Vec_IntPrint( p->vTemp );
// collect the resulting sets
Vec_IntClear( p->vPiLits );
Vec_IntClear( p->vFfLits );
vVar2Ids = (Vec_Int_t *)Vec_PtrGetEntry( &p->pMan->vVar2Ids, k );
Vec_IntForEachEntry( p->vTemp, Lit, i )
{
if ( Lit != Abc_LitNot(LitAux) )
{
int Id = Vec_IntEntry( vVar2Ids, Abc_Lit2Var(Lit) );
Aig_Obj_t * pObj = Aig_ManObj( p->pMan->pAig, Id );
assert( Aig_ObjIsCi(pObj) );
if ( Saig_ObjIsPi(p->pMan->pAig, pObj) )
Vec_IntPush( p->vPiLits, Abc_Var2Lit(Aig_ObjCioId(pObj), Abc_LitIsCompl(Lit)) );
else
Vec_IntPush( p->vFfLits, Abc_Var2Lit(Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pMan->pAig), Abc_LitIsCompl(Lit)) );
}
}
assert( Vec_IntSize(p->vTemp) == Vec_IntSize(p->vPiLits) + Vec_IntSize(p->vFfLits) + 1 );
// move abstracted literals from flops to inputs
if ( p->pMan->pPars->fUseAbs && p->pMan->vAbsFlops )
{
int i, iLit, k = 0;
Vec_IntForEachEntry( p->vFfLits, iLit, i )
{
if ( Vec_IntEntry(p->pMan->vAbsFlops, Abc_Lit2Var(iLit)) ) // used flop
Vec_IntWriteEntry( p->vFfLits, k++, iLit );
else
Vec_IntPush( p->vPiLits, 2*Saig_ManPiNum(p->pMan->pAig) + iLit );
}
Vec_IntShrink( p->vFfLits, k );
}
if ( fVerbose )
Vec_IntPrint( p->vPiLits );
if ( fVerbose )
Vec_IntPrint( p->vFfLits );
if ( fVerbose )
printf( "\n" );
// derive the final set
pRes = Pdr_SetCreate( p->vFfLits, p->vPiLits );
//ZH: Disabled assertion because this invariant doesn't hold with down
//because of the join operation which can bring in initial states
assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
return pRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
|
