1 /**CFile****************************************************************
2
3 FileName [pdrTsim3.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Property driven reachability.]
8
9 Synopsis [Improved ternary simulation.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - November 20, 2010.]
16
17 Revision [$Id: pdrTsim3.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "pdrInt.h"
22 #include "aig/gia/giaAig.h"
23
24 ABC_NAMESPACE_IMPL_START
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 struct Txs3_Man_t_
31 {
32 Gia_Man_t * pGia; // user's AIG
33 Vec_Int_t * vPrio; // priority of each flop
34 Vec_Int_t * vCiObjs; // cone leaves (CI obj IDs)
35 Vec_Int_t * vFosPre; // cone leaves (CI obj IDs)
36 Vec_Int_t * vFosAbs; // cone leaves (CI obj IDs)
37 Vec_Int_t * vCoObjs; // cone roots (CO obj IDs)
38 Vec_Int_t * vCiVals; // cone leaf values (0/1 CI values)
39 Vec_Int_t * vCoVals; // cone root values (0/1 CO values)
40 Vec_Int_t * vNodes; // cone nodes (node obj IDs)
41 Vec_Int_t * vTemp; // cone nodes (node obj IDs)
42 Vec_Int_t * vPiLits; // resulting array of PI literals
43 Vec_Int_t * vFfLits; // resulting array of flop literals
44 Pdr_Man_t * pMan; // calling manager
45 int nPiLits; // the number of PI literals
46 };
47
48 ////////////////////////////////////////////////////////////////////////
49 /// FUNCTION DEFINITIONS ///
50 ////////////////////////////////////////////////////////////////////////
51
52 /**Function*************************************************************
53
54 Synopsis [Start and stop the ternary simulation engine.]
55
56 Description []
57
58 SideEffects []
59
60 SeeAlso []
61
62 ***********************************************************************/
Txs3_ManStart(Pdr_Man_t * pMan,Aig_Man_t * pAig,Vec_Int_t * vPrio)63 Txs3_Man_t * Txs3_ManStart( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio )
64 {
65 Txs3_Man_t * p;
66 // Aig_Obj_t * pObj;
67 // int i;
68 assert( Vec_IntSize(vPrio) == Aig_ManRegNum(pAig) );
69 p = ABC_CALLOC( Txs3_Man_t, 1 );
70 p->pGia = Gia_ManFromAigSimple(pAig); // user's AIG
71 // Aig_ManForEachObj( pAig, pObj, i )
72 // assert( i == 0 || pObj->iData == Abc_Var2Lit(i, 0) );
73 p->vPrio = vPrio; // priority of each flop
74 p->vCiObjs = Vec_IntAlloc( 100 ); // cone leaves (CI obj IDs)
75 p->vFosPre = Vec_IntAlloc( 100 ); // present flop outputs
76 p->vFosAbs = Vec_IntAlloc( 100 ); // absracted flop outputs
77 p->vCoObjs = Vec_IntAlloc( 100 ); // cone roots (CO obj IDs)
78 p->vCiVals = Vec_IntAlloc( 100 ); // cone leaf values (0/1 CI values)
79 p->vCoVals = Vec_IntAlloc( 100 ); // cone root values (0/1 CO values)
80 p->vNodes = Vec_IntAlloc( 100 ); // cone nodes (node obj IDs)
81 p->vTemp = Vec_IntAlloc( 100 ); // cone nodes (node obj IDs)
82 p->vPiLits = Vec_IntAlloc( 100 ); // resulting array of PI literals
83 p->vFfLits = Vec_IntAlloc( 100 ); // resulting array of flop literals
84 p->pMan = pMan; // calling manager
85 return p;
86 }
Txs3_ManStop(Txs3_Man_t * p)87 void Txs3_ManStop( Txs3_Man_t * p )
88 {
89 Gia_ManStop( p->pGia );
90 Vec_IntFree( p->vCiObjs );
91 Vec_IntFree( p->vFosPre );
92 Vec_IntFree( p->vFosAbs );
93 Vec_IntFree( p->vCoObjs );
94 Vec_IntFree( p->vCiVals );
95 Vec_IntFree( p->vCoVals );
96 Vec_IntFree( p->vNodes );
97 Vec_IntFree( p->vTemp );
98 Vec_IntFree( p->vPiLits );
99 Vec_IntFree( p->vFfLits );
100 ABC_FREE( p );
101 }
102
103 /**Function*************************************************************
104
105 Synopsis [Marks the TFI cone and collects CIs and nodes.]
106
107 Description [For this procedure to work Value should not be ~0
108 at the beginning.]
109
110 SideEffects []
111
112 SeeAlso []
113
114 ***********************************************************************/
Txs3_ManCollectCone_rec(Txs3_Man_t * p,Gia_Obj_t * pObj)115 void Txs3_ManCollectCone_rec( Txs3_Man_t * p, Gia_Obj_t * pObj )
116 {
117 if ( !~pObj->Value )
118 return;
119 pObj->Value = ~0;
120 if ( Gia_ObjIsCi(pObj) )
121 {
122 int Entry;
123 if ( Gia_ObjIsPi(p->pGia, pObj) )
124 {
125 Vec_IntPush( p->vCiObjs, Gia_ObjId(p->pGia, pObj) );
126 return;
127 }
128 Entry = Gia_ObjCioId(pObj) - Gia_ManPiNum(p->pGia);
129 if ( Vec_IntEntry(p->vPrio, Entry) ) // present flop
130 Vec_IntPush( p->vFosPre, Gia_ObjId(p->pGia, pObj) );
131 else // asbstracted flop
132 Vec_IntPush( p->vFosAbs, Gia_ObjId(p->pGia, pObj) );
133 return;
134 }
135 assert( Gia_ObjIsAnd(pObj) );
136 Txs3_ManCollectCone_rec( p, Gia_ObjFanin0(pObj) );
137 Txs3_ManCollectCone_rec( p, Gia_ObjFanin1(pObj) );
138 Vec_IntPush( p->vNodes, Gia_ObjId(p->pGia, pObj) );
139 }
Txs3_ManCollectCone(Txs3_Man_t * p,int fVerbose)140 void Txs3_ManCollectCone( Txs3_Man_t * p, int fVerbose )
141 {
142 Gia_Obj_t * pObj; int i, Entry;
143 // printf( "Collecting cones for clause with %d literals.\n", Vec_IntSize(vCoObjs) );
144 Vec_IntClear( p->vCiObjs );
145 Vec_IntClear( p->vFosPre );
146 Vec_IntClear( p->vFosAbs );
147 Vec_IntClear( p->vNodes );
148 Gia_ManConst0(p->pGia)->Value = ~0;
149 Gia_ManForEachObjVec( p->vCoObjs, p->pGia, pObj, i )
150 Txs3_ManCollectCone_rec( p, Gia_ObjFanin0(pObj) );
151 if ( fVerbose )
152 printf( "%d %d %d \n", Vec_IntSize(p->vCiObjs), Vec_IntSize(p->vFosPre), Vec_IntSize(p->vFosAbs) );
153 p->nPiLits = Vec_IntSize(p->vCiObjs);
154 // sort primary inputs
155 Vec_IntSelectSort( Vec_IntArray(p->vCiObjs), Vec_IntSize(p->vCiObjs) );
156 // sort and add present flop variables
157 Vec_IntSelectSortReverse( Vec_IntArray(p->vFosPre), Vec_IntSize(p->vFosPre) );
158 Vec_IntForEachEntry( p->vFosPre, Entry, i )
159 Vec_IntPush( p->vCiObjs, Entry );
160 // sort and add absent flop variables
161 Vec_IntSelectSortReverse( Vec_IntArray(p->vFosAbs), Vec_IntSize(p->vFosAbs) );
162 Vec_IntForEachEntry( p->vFosAbs, Entry, i )
163 Vec_IntPush( p->vCiObjs, Entry );
164 // cleanup
165 Gia_ManForEachObjVec( p->vCiObjs, p->pGia, pObj, i )
166 pObj->Value = 0;
167 Gia_ManForEachObjVec( p->vNodes, p->pGia, pObj, i )
168 pObj->Value = 0;
169 }
170
171 /**Function*************************************************************
172
173 Synopsis [Shrinks values using ternary simulation.]
174
175 Description [The cube contains the set of flop index literals which,
176 when converted into a clause and applied to the combinational outputs,
177 led to a satisfiable SAT run in frame k (values stored in the SAT solver).
178 If the cube is NULL, it is assumed that the first property output was
179 asserted and failed.
180 The resulting array is a set of flop index literals that asserts the COs.
181 Priority contains 0 for i-th entry if the i-th FF is desirable to remove.]
182
183 SideEffects []
184
185 SeeAlso []
186
187 ***********************************************************************/
Txs3_ManTernarySim(Txs3_Man_t * p,int k,Pdr_Set_t * pCube)188 Pdr_Set_t * Txs3_ManTernarySim( Txs3_Man_t * p, int k, Pdr_Set_t * pCube )
189 {
190 // int fTryNew = 1;
191 // int fUseLit = 1;
192 int fVerbose = 0;
193 sat_solver * pSat;
194 Pdr_Set_t * pRes;
195 Gia_Obj_t * pObj;
196 Vec_Int_t * vVar2Ids, * vLits;
197 int i, Lit, LitAux, Var, Value, RetValue, nCoreLits, * pCoreLits;//, nLits;
198 // if ( k == 0 )
199 // fVerbose = 1;
200 // collect CO objects
201 Vec_IntClear( p->vCoObjs );
202 if ( pCube == NULL ) // the target is the property output
203 {
204 pObj = Gia_ManCo(p->pGia, p->pMan->iOutCur);
205 Vec_IntPush( p->vCoObjs, Gia_ObjId(p->pGia, pObj) );
206 }
207 else // the target is the cube
208 {
209 int i;
210 for ( i = 0; i < pCube->nLits; i++ )
211 {
212 if ( pCube->Lits[i] == -1 )
213 continue;
214 pObj = Gia_ManCo(p->pGia, Gia_ManPoNum(p->pGia) + Abc_Lit2Var(pCube->Lits[i]));
215 Vec_IntPush( p->vCoObjs, Gia_ObjId(p->pGia, pObj) );
216 }
217 }
218 if ( 0 )
219 {
220 Abc_Print( 1, "Trying to justify cube " );
221 if ( pCube )
222 Pdr_SetPrint( stdout, pCube, Gia_ManRegNum(p->pGia), NULL );
223 else
224 Abc_Print( 1, "<prop=fail>" );
225 Abc_Print( 1, " in frame %d.\n", k );
226 }
227
228 // collect CI objects
229 Txs3_ManCollectCone( p, fVerbose );
230 // collect values
231 Pdr_ManCollectValues( p->pMan, k, p->vCiObjs, p->vCiVals );
232 Pdr_ManCollectValues( p->pMan, k, p->vCoObjs, p->vCoVals );
233
234 // read solver
235 pSat = Pdr_ManFetchSolver( p->pMan, k );
236 LitAux = Abc_Var2Lit( Pdr_ManFreeVar(p->pMan, k), 0 );
237 // add the clause (complemented cube) in terms of next state variables
238 if ( pCube == NULL ) // the target is the property output
239 {
240 vLits = p->pMan->vLits;
241 Lit = Abc_Var2Lit( Pdr_ObjSatVar(p->pMan, k, 2, Aig_ManCo(p->pMan->pAig, p->pMan->iOutCur)), 1 ); // neg literal (property holds)
242 Vec_IntFill( vLits, 1, Lit );
243 }
244 else
245 vLits = Pdr_ManCubeToLits( p->pMan, k, pCube, 1, 1 );
246 // add activation literal
247 Vec_IntPush( vLits, LitAux );
248 RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
249 assert( RetValue == 1 );
250 sat_solver_compress( pSat );
251
252 // collect assumptions
253 Vec_IntClear( p->vTemp );
254 Vec_IntPush( p->vTemp, Abc_LitNot(LitAux) );
255 // iterate through the values of the CI variables
256 Vec_IntForEachEntryTwo( p->vCiObjs, p->vCiVals, Var, Value, i )
257 {
258 Aig_Obj_t * pObj = Aig_ManObj( p->pMan->pAig, Var );
259 // iVar = Pdr_ObjSatVar( p->pMan, k, fNext ? 2 - lit_sign(pCube->Lits[i]) : 3, pObj ); assert( iVar >= 0 );
260 int iVar = Pdr_ObjSatVar( p->pMan, k, 3, pObj ); assert( iVar >= 0 );
261 assert( Aig_ObjIsCi(pObj) );
262 Vec_IntPush( p->vTemp, Abc_Var2Lit(iVar, !Value) );
263 }
264 if ( fVerbose )
265 {
266 printf( "Clause with %d lits on lev %d\n", pCube ? pCube->nLits : 0, k );
267 Vec_IntPrint( p->vTemp );
268 }
269
270 /*
271 // solve with assumptions
272 //printf( "%d -> ", Vec_IntSize(p->vTemp) );
273 {
274 abctime clk = Abc_Clock();
275 // assume all except flops
276 Vec_IntForEachEntryStop( p->vTemp, Lit, i, p->nPiLits + 1 )
277 if ( !sat_solver_push(pSat, Lit) )
278 {
279 assert( 0 );
280 }
281 nLits = sat_solver_minimize_assumptions( pSat, Vec_IntArray(p->vTemp) + p->nPiLits + 1, Vec_IntSize(p->vTemp) - p->nPiLits - 1, p->pMan->pPars->nConfLimit );
282 Vec_IntShrink( p->vTemp, p->nPiLits + 1 + nLits );
283
284 p->pMan->tAbs += Abc_Clock() - clk;
285 for ( i = 0; i <= p->nPiLits; i++ )
286 sat_solver_pop(pSat);
287 }
288 //printf( "%d ", nLits );
289 */
290
291
292 //check one last time
293 RetValue = sat_solver_solve( pSat, Vec_IntArray(p->vTemp), Vec_IntLimit(p->vTemp), 0, 0, 0, 0 );
294 assert( RetValue == l_False );
295
296 // use analyze final
297 nCoreLits = sat_solver_final(pSat, &pCoreLits);
298 //assert( Vec_IntSize(p->vTemp) <= nCoreLits );
299
300 Vec_IntClear( p->vTemp );
301 for ( i = 0; i < nCoreLits; i++ )
302 Vec_IntPush( p->vTemp, Abc_LitNot(pCoreLits[i]) );
303 Vec_IntSelectSort( Vec_IntArray(p->vTemp), Vec_IntSize(p->vTemp) );
304
305 if ( fVerbose )
306 Vec_IntPrint( p->vTemp );
307
308 // collect the resulting sets
309 Vec_IntClear( p->vPiLits );
310 Vec_IntClear( p->vFfLits );
311 vVar2Ids = (Vec_Int_t *)Vec_PtrGetEntry( &p->pMan->vVar2Ids, k );
312 Vec_IntForEachEntry( p->vTemp, Lit, i )
313 {
314 if ( Lit != Abc_LitNot(LitAux) )
315 {
316 int Id = Vec_IntEntry( vVar2Ids, Abc_Lit2Var(Lit) );
317 Aig_Obj_t * pObj = Aig_ManObj( p->pMan->pAig, Id );
318 assert( Aig_ObjIsCi(pObj) );
319 if ( Saig_ObjIsPi(p->pMan->pAig, pObj) )
320 Vec_IntPush( p->vPiLits, Abc_Var2Lit(Aig_ObjCioId(pObj), Abc_LitIsCompl(Lit)) );
321 else
322 Vec_IntPush( p->vFfLits, Abc_Var2Lit(Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pMan->pAig), Abc_LitIsCompl(Lit)) );
323 }
324 }
325 assert( Vec_IntSize(p->vTemp) == Vec_IntSize(p->vPiLits) + Vec_IntSize(p->vFfLits) + 1 );
326
327 // move abstracted literals from flops to inputs
328 if ( p->pMan->pPars->fUseAbs && p->pMan->vAbsFlops )
329 {
330 int i, iLit, k = 0;
331 Vec_IntForEachEntry( p->vFfLits, iLit, i )
332 {
333 if ( Vec_IntEntry(p->pMan->vAbsFlops, Abc_Lit2Var(iLit)) ) // used flop
334 Vec_IntWriteEntry( p->vFfLits, k++, iLit );
335 else
336 Vec_IntPush( p->vPiLits, 2*Saig_ManPiNum(p->pMan->pAig) + iLit );
337 }
338 Vec_IntShrink( p->vFfLits, k );
339 }
340
341 if ( fVerbose )
342 Vec_IntPrint( p->vPiLits );
343 if ( fVerbose )
344 Vec_IntPrint( p->vFfLits );
345 if ( fVerbose )
346 printf( "\n" );
347
348 // derive the final set
349 pRes = Pdr_SetCreate( p->vFfLits, p->vPiLits );
350 //ZH: Disabled assertion because this invariant doesn't hold with down
351 //because of the join operation which can bring in initial states
352 assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
353 return pRes;
354 }
355
356 ////////////////////////////////////////////////////////////////////////
357 /// END OF FILE ///
358 ////////////////////////////////////////////////////////////////////////
359
360
361 ABC_NAMESPACE_IMPL_END
362