1 /**CFile****************************************************************
2 
3   FileName    [saigTempor.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Sequential AIG package.]
8 
9   Synopsis    [Temporal decomposition.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - June 20, 2005.]
16 
17   Revision    [$Id: saigTempor.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "saig.h"
22 #include "sat/bmc/bmc.h"
23 
24 ABC_NAMESPACE_IMPL_START
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 ///                        DECLARATIONS                              ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 ////////////////////////////////////////////////////////////////////////
32 ///                     FUNCTION DEFINITIONS                         ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 /**Function*************************************************************
36 
37   Synopsis    [Creates initialized timeframes for temporal decomposition.]
38 
39   Description []
40 
41   SideEffects []
42 
43   SeeAlso     []
44 
45 ***********************************************************************/
Saig_ManTemporFrames(Aig_Man_t * pAig,int nFrames)46 Aig_Man_t * Saig_ManTemporFrames( Aig_Man_t * pAig, int nFrames )
47 {
48     Aig_Man_t * pFrames;
49     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
50     int i, f;
51     // start the frames package
52     Aig_ManCleanData( pAig );
53     pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
54     pFrames->pName = Abc_UtilStrsav( pAig->pName );
55     // initiliaze the flops
56     Saig_ManForEachLo( pAig, pObj, i )
57         pObj->pData = Aig_ManConst0(pFrames);
58     // for each timeframe
59     for ( f = 0; f < nFrames; f++ )
60     {
61         Aig_ManConst1(pAig)->pData = Aig_ManConst1(pFrames);
62         Saig_ManForEachPi( pAig, pObj, i )
63             pObj->pData = Aig_ObjCreateCi(pFrames);
64         Aig_ManForEachNode( pAig, pObj, i )
65             pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
66         Aig_ManForEachCo( pAig, pObj, i )
67             pObj->pData = Aig_ObjChild0Copy(pObj);
68         Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
69             pObjLo->pData = pObjLi->pData;
70     }
71     // create POs for the flop inputs
72     Saig_ManForEachLi( pAig, pObj, i )
73         Aig_ObjCreateCo( pFrames, (Aig_Obj_t *)pObj->pData );
74     Aig_ManCleanup( pFrames );
75     return pFrames;
76 }
77 
78 
79 /**Function*************************************************************
80 
81   Synopsis    []
82 
83   Description []
84 
85   SideEffects []
86 
87   SeeAlso     []
88 
89 ***********************************************************************/
Saig_ManTemporDecompose(Aig_Man_t * pAig,int nFrames)90 Aig_Man_t * Saig_ManTemporDecompose( Aig_Man_t * pAig, int nFrames )
91 {
92     Aig_Man_t * pAigNew, * pFrames;
93     Aig_Obj_t * pObj, * pReset;
94     int i;
95     if ( pAig->nConstrs > 0 )
96     {
97         printf( "The AIG manager should have no constraints.\n" );
98         return NULL;
99     }
100     // create initialized timeframes
101     pFrames = Saig_ManTemporFrames( pAig, nFrames );
102     assert( Aig_ManCoNum(pFrames) == Aig_ManRegNum(pAig) );
103 
104     // start the new manager
105     Aig_ManCleanData( pAig );
106     pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
107     pAigNew->pName = Abc_UtilStrsav( pAig->pName );
108     // map the constant node and primary inputs
109     Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
110     Saig_ManForEachPi( pAig, pObj, i )
111         pObj->pData = Aig_ObjCreateCi( pAigNew );
112 
113     // insert initialization logic
114     Aig_ManConst1(pFrames)->pData = Aig_ManConst1( pAigNew );
115     Aig_ManForEachCi( pFrames, pObj, i )
116         pObj->pData = Aig_ObjCreateCi( pAigNew );
117     Aig_ManForEachNode( pFrames, pObj, i )
118         pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
119     Aig_ManForEachCo( pFrames, pObj, i )
120         pObj->pData = Aig_ObjChild0Copy(pObj);
121 
122     // create reset latch (the first one among the latches)
123     pReset = Aig_ObjCreateCi( pAigNew );
124 
125     // create flop output values
126     Saig_ManForEachLo( pAig, pObj, i )
127         pObj->pData = Aig_Mux( pAigNew, pReset, Aig_ObjCreateCi(pAigNew), (Aig_Obj_t *)Aig_ManCo(pFrames, i)->pData );
128     Aig_ManStop( pFrames );
129 
130     // add internal nodes of this frame
131     Aig_ManForEachNode( pAig, pObj, i )
132         pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
133     // create primary outputs
134     Saig_ManForEachPo( pAig, pObj, i )
135         Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
136 
137     // create reset latch (the first one among the latches)
138     Aig_ObjCreateCo( pAigNew, Aig_ManConst1(pAigNew) );
139     // create latch inputs
140     Saig_ManForEachLi( pAig, pObj, i )
141         Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
142 
143     // finalize
144     Aig_ManCleanup( pAigNew );
145     Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 ); // + reset latch (011111...)
146     return pAigNew;
147 }
148 
149 /**Function*************************************************************
150 
151   Synopsis    [Find index of first non-zero entry.]
152 
153   Description []
154 
155   SideEffects []
156 
157   SeeAlso     []
158 
159 ***********************************************************************/
Vec_IntLastNonZeroBeforeLimit(Vec_Int_t * vTemp,int Limit)160 int Vec_IntLastNonZeroBeforeLimit( Vec_Int_t * vTemp, int Limit )
161 {
162     int Entry, i;
163     if ( vTemp == NULL )
164         return -1;
165     Vec_IntForEachEntryReverse( vTemp, Entry, i )
166     {
167         if ( i >= Limit )
168             continue;
169         if ( Entry )
170             return i;
171     }
172     return -1;
173 }
174 
175 /**Function*************************************************************
176 
177   Synopsis    []
178 
179   Description []
180 
181   SideEffects []
182 
183   SeeAlso     []
184 
185 ***********************************************************************/
Saig_ManTempor(Aig_Man_t * pAig,int nFrames,int TimeOut,int nConfLimit,int fUseBmc,int fUseTransSigs,int fVerbose,int fVeryVerbose)186 Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fUseTransSigs, int fVerbose, int fVeryVerbose )
187 {
188     extern int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose, Vec_Int_t ** pvTrans );
189 
190     Vec_Int_t * vTransSigs = NULL;
191     int RetValue, nFramesFinished = -1;
192     assert( nFrames >= 0 );
193     if ( nFrames == 0 )
194     {
195         nFrames = Saig_ManPhasePrefixLength( pAig, fVerbose, fVeryVerbose, &vTransSigs );
196         if ( nFrames == 0 )
197         {
198             Vec_IntFreeP( &vTransSigs );
199             printf( "The leading sequence has length 0. Temporal decomposition is not performed.\n" );
200             return NULL;
201         }
202         if ( nFrames == 1 )
203         {
204             Vec_IntFreeP( &vTransSigs );
205             printf( "The leading sequence has length 1. Temporal decomposition is not performed.\n" );
206             return NULL;
207         }
208         if ( fUseTransSigs )
209         {
210             int Entry, i, iLast = -1;
211             Vec_IntForEachEntry( vTransSigs, Entry, i )
212                 iLast = Entry ? i :iLast;
213             if ( iLast > 0 && iLast < nFrames )
214             {
215                 Abc_Print( 1, "Reducing frame count from %d to %d to fit the last transient.\n", nFrames, iLast );
216                 nFrames = iLast;
217             }
218         }
219         Abc_Print( 1, "Using computed frame number (%d).\n", nFrames );
220     }
221     else
222         Abc_Print( 1, "Using user-given frame number (%d).\n", nFrames );
223     // run BMC2
224     if ( fUseBmc )
225     {
226         RetValue = Saig_BmcPerform( pAig, 0, nFrames, 2000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished, 0, 0 );
227         if ( RetValue == 0 )
228         {
229             Vec_IntFreeP( &vTransSigs );
230             printf( "A cex found in the first %d frames.\n", nFrames );
231             return NULL;
232         }
233         if ( nFramesFinished + 1 < nFrames )
234         {
235             int iLastBefore = Vec_IntLastNonZeroBeforeLimit( vTransSigs, nFramesFinished );
236             if ( iLastBefore < 1 || !fUseTransSigs )
237             {
238                 Vec_IntFreeP( &vTransSigs );
239                 printf( "BMC for %d frames could not be completed. A cex may exist!\n", nFrames );
240                 return NULL;
241             }
242             assert( iLastBefore < nFramesFinished );
243             printf( "BMC succeeded to frame %d. Adjusting frame count to be (%d) based on the last transient signal.\n", nFramesFinished, iLastBefore );
244             nFrames = iLastBefore;
245         }
246     }
247     Vec_IntFreeP( &vTransSigs );
248     return Saig_ManTemporDecompose( pAig, nFrames );
249 }
250 
251 ////////////////////////////////////////////////////////////////////////
252 ///                       END OF FILE                                ///
253 ////////////////////////////////////////////////////////////////////////
254 
255 ABC_NAMESPACE_IMPL_END
256 
257