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