1 /**CFile****************************************************************
2 
3   FileName    [intCheck.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Interpolation engine.]
8 
9   Synopsis    [Procedures to perform incremental inductive check.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - June 24, 2008.]
16 
17   Revision    [$Id: intCheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "intInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 ///                        DECLARATIONS                              ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 // checking manager
31 struct Inter_Check_t_
32 {
33     int           nFramesK;     // the number of timeframes (K=1 for simple induction)
34     int           nVars;        // the current number of variables in the solver
35     Aig_Man_t *   pFrames;      // unrolled timeframes
36     Cnf_Dat_t *   pCnf;         // CNF of unrolled timeframes
37     sat_solver *  pSat;         // SAT solver
38     Vec_Int_t *   vOrLits;      // OR vars in each time frame (total number is the number nFrames)
39     Vec_Int_t *   vAndLits;     // AND vars in the last timeframe (total number is the number of interpolants)
40     Vec_Int_t *   vAssLits;     // assumptions (the union of the two)
41 };
42 
43 ////////////////////////////////////////////////////////////////////////
44 ///                     FUNCTION DEFINITIONS                         ///
45 ////////////////////////////////////////////////////////////////////////
46 
47 /**Function*************************************************************
48 
49   Synopsis    [Create timeframes of the manager for interpolation.]
50 
51   Description [The resulting manager is combinational. The primary inputs
52   corresponding to register outputs are ordered first.]
53 
54   SideEffects []
55 
56   SeeAlso     []
57 
58 ***********************************************************************/
Inter_ManUnrollFrames(Aig_Man_t * pAig,int nFrames)59 Aig_Man_t * Inter_ManUnrollFrames( Aig_Man_t * pAig, int nFrames )
60 {
61     Aig_Man_t * pFrames;
62     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
63     int i, f;
64     assert( Saig_ManRegNum(pAig) > 0 );
65     pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
66     // map the constant node
67     Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
68     // create variables for register outputs
69     Saig_ManForEachLo( pAig, pObj, i )
70         pObj->pData = Aig_ObjCreateCi( pFrames );
71     // add timeframes
72     for ( f = 0; f < nFrames; f++ )
73     {
74         // create PI nodes for this frame
75         Saig_ManForEachPi( pAig, pObj, i )
76             pObj->pData = Aig_ObjCreateCi( pFrames );
77         // add internal nodes of this frame
78         Aig_ManForEachNode( pAig, pObj, i )
79             pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
80         // save register inputs
81         Saig_ManForEachLi( pAig, pObj, i )
82             pObj->pData = Aig_ObjChild0Copy(pObj);
83         // transfer to register outputs
84         Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
85         {
86             pObjLo->pData = pObjLi->pData;
87             Aig_ObjCreateCo( pFrames, (Aig_Obj_t *)pObjLo->pData );
88         }
89     }
90     Aig_ManCleanup( pFrames );
91     return pFrames;
92 }
93 
94 /**Function*************************************************************
95 
96   Synopsis    [This procedure sets default values of interpolation parameters.]
97 
98   Description []
99 
100   SideEffects []
101 
102   SeeAlso     []
103 
104 ***********************************************************************/
Inter_CheckStart(Aig_Man_t * pTrans,int nFramesK)105 Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK )
106 {
107     Inter_Check_t * p;
108     // create solver
109     p = ABC_CALLOC( Inter_Check_t, 1 );
110     p->vOrLits  = Vec_IntAlloc( 100 );
111     p->vAndLits = Vec_IntAlloc( 100 );
112     p->vAssLits = Vec_IntAlloc( 100 );
113     // generate the timeframes
114     p->pFrames = Inter_ManUnrollFrames( pTrans, nFramesK );
115     assert( Aig_ManCiNum(p->pFrames) == nFramesK * Saig_ManPiNum(pTrans) + Saig_ManRegNum(pTrans) );
116     assert( Aig_ManCoNum(p->pFrames) == nFramesK * Saig_ManRegNum(pTrans) );
117     // convert to CNF
118     p->pCnf = Cnf_Derive( p->pFrames, Aig_ManCoNum(p->pFrames) );
119     p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
120     // assign parameters
121     p->nFramesK = nFramesK;
122     p->nVars    = p->pCnf->nVars;
123     return p;
124 }
125 
126 /**Function*************************************************************
127 
128   Synopsis    [This procedure sets default values of interpolation parameters.]
129 
130   Description []
131 
132   SideEffects []
133 
134   SeeAlso     []
135 
136 ***********************************************************************/
Inter_CheckStop(Inter_Check_t * p)137 void Inter_CheckStop( Inter_Check_t * p )
138 {
139     if ( p == NULL )
140         return;
141     Vec_IntFree( p->vOrLits );
142     Vec_IntFree( p->vAndLits );
143     Vec_IntFree( p->vAssLits );
144     Cnf_DataFree( p->pCnf );
145     Aig_ManStop( p->pFrames );
146     sat_solver_delete( p->pSat );
147     ABC_FREE( p );
148 }
149 
150 
151 /**Function*************************************************************
152 
153   Synopsis    [Creates one OR-gate: A + B = C.]
154 
155   Description []
156 
157   SideEffects []
158 
159   SeeAlso     []
160 
161 ***********************************************************************/
Inter_CheckAddOrGate(Inter_Check_t * p,int iVarA,int iVarB,int iVarC)162 void Inter_CheckAddOrGate( Inter_Check_t * p, int iVarA, int iVarB, int iVarC )
163 {
164     int RetValue, pLits[3];
165     // add A => C   or   !A + C
166     pLits[0] = toLitCond(iVarA, 1);
167     pLits[1] = toLitCond(iVarC, 0);
168     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
169     assert( RetValue );
170     // add B => C   or   !B + C
171     pLits[0] = toLitCond(iVarB, 1);
172     pLits[1] = toLitCond(iVarC, 0);
173     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
174     assert( RetValue );
175     // add !A & !B => !C  or A + B + !C
176     pLits[0] = toLitCond(iVarA, 0);
177     pLits[1] = toLitCond(iVarB, 0);
178     pLits[2] = toLitCond(iVarC, 1);
179     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
180     assert( RetValue );
181 }
182 
183 /**Function*************************************************************
184 
185   Synopsis    [Creates equality: A = B.]
186 
187   Description []
188 
189   SideEffects []
190 
191   SeeAlso     []
192 
193 ***********************************************************************/
Inter_CheckAddEqual(Inter_Check_t * p,int iVarA,int iVarB)194 void Inter_CheckAddEqual( Inter_Check_t * p, int iVarA, int iVarB )
195 {
196     int RetValue, pLits[3];
197     // add A => B   or   !A + B
198     pLits[0] = toLitCond(iVarA, 1);
199     pLits[1] = toLitCond(iVarB, 0);
200     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
201     assert( RetValue );
202     // add B => A   or   !B + A
203     pLits[0] = toLitCond(iVarB, 1);
204     pLits[1] = toLitCond(iVarA, 0);
205     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
206     assert( RetValue );
207 }
208 
209 /**Function*************************************************************
210 
211   Synopsis    [Perform the checking.]
212 
213   Description [Returns 1 if the check has passed.]
214 
215   SideEffects []
216 
217   SeeAlso     []
218 
219 ***********************************************************************/
Inter_CheckPerform(Inter_Check_t * p,Cnf_Dat_t * pCnfInt,abctime nTimeNewOut)220 int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, abctime nTimeNewOut )
221 {
222     Aig_Obj_t * pObj, * pObj2;
223     int i, f, VarA, VarB, RetValue, Entry, status;
224     int nRegs = Aig_ManCiNum(pCnfInt->pMan);
225     assert( Aig_ManCoNum(p->pCnf->pMan) == p->nFramesK * nRegs );
226     assert( Aig_ManCoNum(pCnfInt->pMan) == 1 );
227 
228     // set runtime limit
229     if ( nTimeNewOut )
230         sat_solver_set_runtime_limit( p->pSat, nTimeNewOut );
231 
232     // add clauses to the SAT solver
233     Cnf_DataLift( pCnfInt, p->nVars );
234     for ( f = 0; f <= p->nFramesK; f++ )
235     {
236         // add clauses to the solver
237         for ( i = 0; i < pCnfInt->nClauses; i++ )
238         {
239             RetValue = sat_solver_addclause( p->pSat, pCnfInt->pClauses[i], pCnfInt->pClauses[i+1] );
240             assert( RetValue );
241         }
242         // add equality clauses for the flop variables
243         Aig_ManForEachCi( pCnfInt->pMan, pObj, i )
244         {
245             pObj2 = f ? Aig_ManCo(p->pFrames, i + (f-1) * nRegs) : Aig_ManCi(p->pFrames, i);
246             Inter_CheckAddEqual( p, pCnfInt->pVarNums[pObj->Id], p->pCnf->pVarNums[pObj2->Id] );
247         }
248         // add final clauses
249         if ( f < p->nFramesK )
250         {
251             if ( f == Vec_IntSize(p->vOrLits) ) // find time here
252             {
253                 // add literal to this frame
254                 VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ];
255                 Vec_IntPush( p->vOrLits, VarB );
256             }
257             else
258             {
259                 // add OR gate for this frame
260                 VarA = Vec_IntEntry( p->vOrLits, f );
261                 VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ];
262                 Inter_CheckAddOrGate( p, VarA, VarB, p->nVars + pCnfInt->nVars );
263                 Vec_IntWriteEntry( p->vOrLits, f, p->nVars + pCnfInt->nVars ); // using var ID!
264             }
265         }
266         else
267         {
268             // add AND gate for this frame
269             VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ];
270             Vec_IntPush( p->vAndLits, VarB );
271         }
272         // update variable IDs
273         Cnf_DataLift( pCnfInt, pCnfInt->nVars + 1 );
274         p->nVars += pCnfInt->nVars + 1;
275     }
276     Cnf_DataLift( pCnfInt, -p->nVars );
277     assert( Vec_IntSize(p->vOrLits) == p->nFramesK );
278 
279     // collect the assumption literals
280     Vec_IntClear( p->vAssLits );
281     Vec_IntForEachEntry( p->vOrLits, Entry, i )
282         Vec_IntPush( p->vAssLits, toLitCond(Entry, 0) );
283     Vec_IntForEachEntry( p->vAndLits, Entry, i )
284         Vec_IntPush( p->vAssLits, toLitCond(Entry, 1) );
285 /*
286     if ( pCnfInt->nLiterals == 3635 )
287     {
288         int s = 0;
289     }
290 */
291     // call the SAT solver
292     status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssLits),
293         Vec_IntArray(p->vAssLits) + Vec_IntSize(p->vAssLits),
294         (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
295 
296     return status == l_False;
297 }
298 
299 
300 ////////////////////////////////////////////////////////////////////////
301 ///                       END OF FILE                                ///
302 ////////////////////////////////////////////////////////////////////////
303 
304 ABC_NAMESPACE_IMPL_END
305 
306