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