1 /**CFile****************************************************************
2
3 FileName [llb1Core.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [BDD based reachability.]
8
9 Synopsis [Top-level procedure.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: llb1Core.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "llbInt.h"
22 #include "aig/gia/gia.h"
23 #include "aig/gia/giaAig.h"
24
25 ABC_NAMESPACE_IMPL_START
26
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30
31 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34
35 /**Function*************************************************************
36
37 Synopsis []
38
39 Description []
40
41 SideEffects []
42
43 SeeAlso []
44
45 ***********************************************************************/
Llb_ManSetDefaultParams(Gia_ParLlb_t * p)46 void Llb_ManSetDefaultParams( Gia_ParLlb_t * p )
47 {
48 memset( p, 0, sizeof(Gia_ParLlb_t) );
49 p->nBddMax = 10000000;
50 p->nIterMax = 10000000;
51 p->nClusterMax = 20;
52 p->nHintDepth = 0;
53 p->HintFirst = 0;
54 p->fUseFlow = 0; // use flow
55 p->nVolumeMax = 100; // max volume
56 p->nVolumeMin = 30; // min volume
57 p->nPartValue = 5; // partitioning value
58 p->fBackward = 0; // forward by default
59 p->fReorder = 1;
60 p->fIndConstr = 0;
61 p->fUsePivots = 0;
62 p->fCluster = 0;
63 p->fSchedule = 0;
64 p->fDumpReached = 0;
65 p->fVerbose = 0;
66 p->fVeryVerbose = 0;
67 p->fSilent = 0;
68 p->TimeLimit = 0;
69 // p->TimeLimit = 0;
70 p->TimeLimitGlo = 0;
71 p->TimeTarget = 0;
72 p->iFrame = -1;
73 }
74
75
76 /**Function*************************************************************
77
78 Synopsis [Prints statistics about MFFCs.]
79
80 Description []
81
82 SideEffects []
83
84 SeeAlso []
85
86 ***********************************************************************/
Llb_ManPrintAig(Llb_Man_t * p)87 void Llb_ManPrintAig( Llb_Man_t * p )
88 {
89 Abc_Print( 1, "pi =%3d ", Saig_ManPiNum(p->pAig) );
90 Abc_Print( 1, "po =%3d ", Saig_ManPoNum(p->pAig) );
91 Abc_Print( 1, "ff =%3d ", Saig_ManRegNum(p->pAig) );
92 Abc_Print( 1, "int =%5d ", Vec_IntSize(p->vVar2Obj)-Aig_ManCiNum(p->pAig)-Saig_ManRegNum(p->pAig) );
93 Abc_Print( 1, "var =%5d ", Vec_IntSize(p->vVar2Obj) );
94 Abc_Print( 1, "part =%5d ", Vec_PtrSize(p->vGroups)-2 );
95 Abc_Print( 1, "and =%5d ", Aig_ManNodeNum(p->pAig) );
96 Abc_Print( 1, "lev =%4d ", Aig_ManLevelNum(p->pAig) );
97 // Abc_Print( 1, "cut =%4d ", Llb_ManCrossCut(p->pAig) );
98 Abc_Print( 1, "\n" );
99 }
100
101 /**Function*************************************************************
102
103 Synopsis []
104
105 Description []
106
107 SideEffects []
108
109 SeeAlso []
110
111 ***********************************************************************/
Llb_ManModelCheckAig(Aig_Man_t * pAigGlo,Gia_ParLlb_t * pPars,Vec_Int_t * vHints,DdManager ** pddGlo)112 int Llb_ManModelCheckAig( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars, Vec_Int_t * vHints, DdManager ** pddGlo )
113 {
114 Llb_Man_t * p = NULL;
115 Aig_Man_t * pAig;
116 int RetValue = -1;
117 abctime clk = Abc_Clock();
118
119 if ( pPars->fIndConstr )
120 {
121 assert( vHints == NULL );
122 vHints = Llb_ManDeriveConstraints( pAigGlo );
123 }
124
125 // derive AIG for hints
126 if ( vHints == NULL )
127 pAig = Aig_ManDupSimple( pAigGlo );
128 else
129 {
130 if ( pPars->fVerbose )
131 Llb_ManPrintEntries( pAigGlo, vHints );
132 pAig = Aig_ManDupSimpleWithHints( pAigGlo, vHints );
133 }
134
135
136 if ( pPars->fUseFlow )
137 {
138 // p = Llb_ManStartFlow( pAigGlo, pAig, pPars );
139 }
140 else
141 {
142 p = Llb_ManStart( pAigGlo, pAig, pPars );
143 if ( pPars->fVerbose )
144 {
145 Llb_ManPrintAig( p );
146 printf( "Original matrix: " );
147 Llb_MtrPrintMatrixStats( p->pMatrix );
148 if ( pPars->fVeryVerbose )
149 Llb_MtrPrint( p->pMatrix, 1 );
150 }
151 if ( pPars->fCluster )
152 {
153 Llb_ManCluster( p->pMatrix );
154 if ( pPars->fVerbose )
155 {
156 printf( "Matrix after clustering: " );
157 Llb_MtrPrintMatrixStats( p->pMatrix );
158 if ( pPars->fVeryVerbose )
159 Llb_MtrPrint( p->pMatrix, 1 );
160 }
161 }
162 if ( pPars->fSchedule )
163 {
164 Llb_MtrSchedule( p->pMatrix );
165 if ( pPars->fVerbose )
166 {
167 printf( "Matrix after scheduling: " );
168 Llb_MtrPrintMatrixStats( p->pMatrix );
169 if ( pPars->fVeryVerbose )
170 Llb_MtrPrint( p->pMatrix, 1 );
171 }
172 }
173 }
174
175 if ( !p->pPars->fSkipReach )
176 RetValue = Llb_ManReachability( p, vHints, pddGlo );
177 Llb_ManStop( p );
178
179 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
180
181 if ( pPars->fIndConstr )
182 Vec_IntFreeP( &vHints );
183 return RetValue;
184 }
185
186 /**Function*************************************************************
187
188 Synopsis []
189
190 Description []
191
192 SideEffects []
193
194 SeeAlso []
195
196 ***********************************************************************/
Llb_ManModelCheckGia(Gia_Man_t * pGia,Gia_ParLlb_t * pPars)197 int Llb_ManModelCheckGia( Gia_Man_t * pGia, Gia_ParLlb_t * pPars )
198 {
199 Gia_Man_t * pGia2;
200 Aig_Man_t * pAig;
201 int RetValue = -1;
202 pGia2 = Gia_ManDupDfs( pGia );
203 pAig = Gia_ManToAigSimple( pGia2 );
204 Gia_ManStop( pGia2 );
205 //Aig_ManShow( pAig, 0, NULL );
206
207 if ( pPars->nHintDepth == 0 )
208 RetValue = Llb_ManModelCheckAig( pAig, pPars, NULL, NULL );
209 else
210 RetValue = Llb_ManModelCheckAigWithHints( pAig, pPars );
211 pGia->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
212 Aig_ManStop( pAig );
213 return RetValue;
214 }
215
216 ////////////////////////////////////////////////////////////////////////
217 /// END OF FILE ///
218 ////////////////////////////////////////////////////////////////////////
219
220
221 ABC_NAMESPACE_IMPL_END
222
223