1 /**CFile****************************************************************
2
3 FileName [dchCnf.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Choice computation for tech-mapping.]
8
9 Synopsis [Computation of CNF.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 29, 2008.]
16
17 Revision [$Id: dchCnf.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "dchInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 /**Function*************************************************************
35
36 Synopsis [Addes clauses to the solver.]
37
38 Description []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
Dch_AddClausesMux(Dch_Man_t * p,Aig_Obj_t * pNode)45 void Dch_AddClausesMux( Dch_Man_t * p, Aig_Obj_t * pNode )
46 {
47 Aig_Obj_t * pNodeI, * pNodeT, * pNodeE;
48 int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
49
50 assert( !Aig_IsComplement( pNode ) );
51 assert( Aig_ObjIsMuxType( pNode ) );
52 // get nodes (I = if, T = then, E = else)
53 pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
54 // get the variable numbers
55 VarF = Dch_ObjSatNum(p,pNode);
56 VarI = Dch_ObjSatNum(p,pNodeI);
57 VarT = Dch_ObjSatNum(p,Aig_Regular(pNodeT));
58 VarE = Dch_ObjSatNum(p,Aig_Regular(pNodeE));
59 // get the complementation flags
60 fCompT = Aig_IsComplement(pNodeT);
61 fCompE = Aig_IsComplement(pNodeE);
62
63 // f = ITE(i, t, e)
64
65 // i' + t' + f
66 // i' + t + f'
67 // i + e' + f
68 // i + e + f'
69
70 // create four clauses
71 pLits[0] = toLitCond(VarI, 1);
72 pLits[1] = toLitCond(VarT, 1^fCompT);
73 pLits[2] = toLitCond(VarF, 0);
74 if ( p->pPars->fPolarFlip )
75 {
76 if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
77 if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
78 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
79 }
80 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
81 assert( RetValue );
82 pLits[0] = toLitCond(VarI, 1);
83 pLits[1] = toLitCond(VarT, 0^fCompT);
84 pLits[2] = toLitCond(VarF, 1);
85 if ( p->pPars->fPolarFlip )
86 {
87 if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
88 if ( Aig_Regular(pNodeT)->fPhase ) pLits[1] = lit_neg( pLits[1] );
89 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
90 }
91 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
92 assert( RetValue );
93 pLits[0] = toLitCond(VarI, 0);
94 pLits[1] = toLitCond(VarE, 1^fCompE);
95 pLits[2] = toLitCond(VarF, 0);
96 if ( p->pPars->fPolarFlip )
97 {
98 if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
99 if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
100 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
101 }
102 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
103 assert( RetValue );
104 pLits[0] = toLitCond(VarI, 0);
105 pLits[1] = toLitCond(VarE, 0^fCompE);
106 pLits[2] = toLitCond(VarF, 1);
107 if ( p->pPars->fPolarFlip )
108 {
109 if ( pNodeI->fPhase ) pLits[0] = lit_neg( pLits[0] );
110 if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
111 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
112 }
113 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
114 assert( RetValue );
115
116 // two additional clauses
117 // t' & e' -> f'
118 // t & e -> f
119
120 // t + e + f'
121 // t' + e' + f
122
123 if ( VarT == VarE )
124 {
125 // assert( fCompT == !fCompE );
126 return;
127 }
128
129 pLits[0] = toLitCond(VarT, 0^fCompT);
130 pLits[1] = toLitCond(VarE, 0^fCompE);
131 pLits[2] = toLitCond(VarF, 1);
132 if ( p->pPars->fPolarFlip )
133 {
134 if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
135 if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
136 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
137 }
138 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
139 assert( RetValue );
140 pLits[0] = toLitCond(VarT, 1^fCompT);
141 pLits[1] = toLitCond(VarE, 1^fCompE);
142 pLits[2] = toLitCond(VarF, 0);
143 if ( p->pPars->fPolarFlip )
144 {
145 if ( Aig_Regular(pNodeT)->fPhase ) pLits[0] = lit_neg( pLits[0] );
146 if ( Aig_Regular(pNodeE)->fPhase ) pLits[1] = lit_neg( pLits[1] );
147 if ( pNode->fPhase ) pLits[2] = lit_neg( pLits[2] );
148 }
149 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
150 assert( RetValue );
151 }
152
153 /**Function*************************************************************
154
155 Synopsis [Addes clauses to the solver.]
156
157 Description []
158
159 SideEffects []
160
161 SeeAlso []
162
163 ***********************************************************************/
Dch_AddClausesSuper(Dch_Man_t * p,Aig_Obj_t * pNode,Vec_Ptr_t * vSuper)164 void Dch_AddClausesSuper( Dch_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
165 {
166 Aig_Obj_t * pFanin;
167 int * pLits, nLits, RetValue, i;
168 assert( !Aig_IsComplement(pNode) );
169 assert( Aig_ObjIsNode( pNode ) );
170 // create storage for literals
171 nLits = Vec_PtrSize(vSuper) + 1;
172 pLits = ABC_ALLOC( int, nLits );
173 // suppose AND-gate is A & B = C
174 // add !A => !C or A + !C
175 Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
176 {
177 pLits[0] = toLitCond(Dch_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
178 pLits[1] = toLitCond(Dch_ObjSatNum(p,pNode), 1);
179 if ( p->pPars->fPolarFlip )
180 {
181 if ( Aig_Regular(pFanin)->fPhase ) pLits[0] = lit_neg( pLits[0] );
182 if ( pNode->fPhase ) pLits[1] = lit_neg( pLits[1] );
183 }
184 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
185 assert( RetValue );
186 }
187 // add A & B => C or !A + !B + C
188 Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
189 {
190 pLits[i] = toLitCond(Dch_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
191 if ( p->pPars->fPolarFlip )
192 {
193 if ( Aig_Regular(pFanin)->fPhase ) pLits[i] = lit_neg( pLits[i] );
194 }
195 }
196 pLits[nLits-1] = toLitCond(Dch_ObjSatNum(p,pNode), 0);
197 if ( p->pPars->fPolarFlip )
198 {
199 if ( pNode->fPhase ) pLits[nLits-1] = lit_neg( pLits[nLits-1] );
200 }
201 RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
202 assert( RetValue );
203 ABC_FREE( pLits );
204 }
205
206 /**Function*************************************************************
207
208 Synopsis [Collects the supergate.]
209
210 Description []
211
212 SideEffects []
213
214 SeeAlso []
215
216 ***********************************************************************/
Dch_CollectSuper_rec(Aig_Obj_t * pObj,Vec_Ptr_t * vSuper,int fFirst,int fUseMuxes)217 void Dch_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
218 {
219 // if the new node is complemented or a PI, another gate begins
220 if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) ||
221 (!fFirst && Aig_ObjRefs(pObj) > 1) ||
222 (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
223 {
224 Vec_PtrPushUnique( vSuper, pObj );
225 return;
226 }
227 // go through the branches
228 Dch_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
229 Dch_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
230 }
231
232 /**Function*************************************************************
233
234 Synopsis [Collects the supergate.]
235
236 Description []
237
238 SideEffects []
239
240 SeeAlso []
241
242 ***********************************************************************/
Dch_CollectSuper(Aig_Obj_t * pObj,int fUseMuxes,Vec_Ptr_t * vSuper)243 void Dch_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
244 {
245 assert( !Aig_IsComplement(pObj) );
246 assert( !Aig_ObjIsCi(pObj) );
247 Vec_PtrClear( vSuper );
248 Dch_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
249 }
250
251 /**Function*************************************************************
252
253 Synopsis [Updates the solver clause database.]
254
255 Description []
256
257 SideEffects []
258
259 SeeAlso []
260
261 ***********************************************************************/
Dch_ObjAddToFrontier(Dch_Man_t * p,Aig_Obj_t * pObj,Vec_Ptr_t * vFrontier)262 void Dch_ObjAddToFrontier( Dch_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier )
263 {
264 assert( !Aig_IsComplement(pObj) );
265 if ( Dch_ObjSatNum(p,pObj) )
266 return;
267 assert( Dch_ObjSatNum(p,pObj) == 0 );
268 if ( Aig_ObjIsConst1(pObj) )
269 return;
270 Vec_PtrPush( p->vUsedNodes, pObj );
271 Dch_ObjSetSatNum( p, pObj, p->nSatVars++ );
272 if ( Aig_ObjIsNode(pObj) )
273 Vec_PtrPush( vFrontier, pObj );
274 }
275
276 /**Function*************************************************************
277
278 Synopsis [Updates the solver clause database.]
279
280 Description []
281
282 SideEffects []
283
284 SeeAlso []
285
286 ***********************************************************************/
Dch_CnfNodeAddToSolver(Dch_Man_t * p,Aig_Obj_t * pObj)287 void Dch_CnfNodeAddToSolver( Dch_Man_t * p, Aig_Obj_t * pObj )
288 {
289 Vec_Ptr_t * vFrontier;
290 Aig_Obj_t * pNode, * pFanin;
291 int i, k, fUseMuxes = 1;
292 // quit if CNF is ready
293 if ( Dch_ObjSatNum(p,pObj) )
294 return;
295 // start the frontier
296 vFrontier = Vec_PtrAlloc( 100 );
297 Dch_ObjAddToFrontier( p, pObj, vFrontier );
298 // explore nodes in the frontier
299 Vec_PtrForEachEntry( Aig_Obj_t *, vFrontier, pNode, i )
300 {
301 // create the supergate
302 assert( Dch_ObjSatNum(p,pNode) );
303 if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
304 {
305 Vec_PtrClear( p->vFanins );
306 Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
307 Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
308 Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
309 Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
310 Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k )
311 Dch_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
312 Dch_AddClausesMux( p, pNode );
313 }
314 else
315 {
316 Dch_CollectSuper( pNode, fUseMuxes, p->vFanins );
317 Vec_PtrForEachEntry( Aig_Obj_t *, p->vFanins, pFanin, k )
318 Dch_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
319 Dch_AddClausesSuper( p, pNode, p->vFanins );
320 }
321 assert( Vec_PtrSize(p->vFanins) > 1 );
322 }
323 Vec_PtrFree( vFrontier );
324 }
325
326
327
328 ////////////////////////////////////////////////////////////////////////
329 /// END OF FILE ///
330 ////////////////////////////////////////////////////////////////////////
331
332
333 ABC_NAMESPACE_IMPL_END
334
335