abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions
abcCas.c File Reference
#include "base/abc/abc.h"
#include "misc/extra/extraBdd.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START int Abc_CascadeExperiment (char *pFileGeneric, DdManager *dd, DdNode **pOutputs, int nInputs, int nOutputs, int nLutSize, int fCheck, int fVerbose)
 DECLARATIONS ///. More...
 
Abc_Ntk_t * Abc_NtkCascade (Abc_Ntk_t *pNtk, int nLutSize, int fCheck, int fVerbose)
 FUNCTION DEFINITIONS ///. More...
 

Function Documentation

ABC_NAMESPACE_IMPL_START int Abc_CascadeExperiment ( char *  pFileGeneric,
DdManager *  dd,
DdNode **  pOutputs,
int  nInputs,
int  nOutputs,
int  nLutSize,
int  fCheck,
int  fVerbose 
)

DECLARATIONS ///.

CFile****************************************************************

FileName [abcCas.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Decomposition of shared BDDs into LUT cascade.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:
abcCas.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

DECLARATIONS ///.

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 79 of file casCore.c.

80 {
81  int i;
82  int nVars = nInputs;
83  int nOuts = nOutputs;
84  abctime clk1;
85 
86  int nVarsEnc; // the number of additional variables to encode outputs
87  DdNode * pbVarsEnc[MAXOUTPUTS]; // the BDDs of the encoding vars
88 
89  int nNames; // the total number of all inputs
90  char * pNames[MAXINPUTS]; // the temporary storage for the input (and output encoding) names
91 
92  DdNode * aFunc; // the encoded 0-1 BDD containing all the outputs
93 
94  char FileNameIni[100];
95  char FileNameFin[100];
96  char Buffer[100];
97 
98 
99 //pTable = fopen( "stats.txt", "a+" );
100 //fprintf( pTable, "%s ", pFileGeneric );
101 //fprintf( pTable, "%d ", nVars );
102 //fprintf( pTable, "%d ", nOuts );
103 
104 
105  // assign the file names
106  strcpy( FileNameIni, pFileGeneric );
107  strcat( FileNameIni, "_ENC.blif" );
108 
109  strcpy( FileNameFin, pFileGeneric );
110  strcat( FileNameFin, "_LUT.blif" );
111 
112 
113  // create the variables to encode the outputs
114  nVarsEnc = Abc_Base2Log( nOuts );
115  for ( i = 0; i < nVarsEnc; i++ )
116  pbVarsEnc[i] = Cudd_bddNewVarAtLevel( dd, i );
117 
118 
119  // store the input names
120  nNames = nVars + nVarsEnc;
121  for ( i = 0; i < nVars; i++ )
122  {
123 // pNames[i] = Extra_UtilStrsav( pFunc->pInputNames[i] );
124  sprintf( Buffer, "pi%03d", i );
125  pNames[i] = Extra_UtilStrsav( Buffer );
126  }
127  // set the encoding variable name
128  for ( ; i < nNames; i++ )
129  {
130  sprintf( Buffer, "OutEnc_%02d", i-nVars );
131  pNames[i] = Extra_UtilStrsav( Buffer );
132  }
133 
134 
135  // print the variable order
136 // printf( "\n" );
137 // printf( "Variable order is: " );
138 // for ( i = 0; i < dd->size; i++ )
139 // printf( " %d", dd->invperm[i] );
140 // printf( "\n" );
141 
142  // derive the single-output function
143  clk1 = Abc_Clock();
144  aFunc = GetSingleOutputFunction( dd, pOutputs, nOuts, pbVarsEnc, nVarsEnc, fVerbose ); Cudd_Ref( aFunc );
145 // aFunc = GetSingleOutputFunctionRemapped( dd, pOutputs, nOuts, pbVarsEnc, nVarsEnc ); Cudd_Ref( aFunc );
146 // if ( fVerbose )
147 // printf( "Single-output function computation time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
148 
149 //fprintf( pTable, "%d ", Cudd_SharingSize( pOutputs, nOutputs ) );
150 //fprintf( pTable, "%d ", Extra_ProfileWidthSharingMax(dd, pOutputs, nOutputs) );
151 
152  // dispose of the multiple-output function
153 // Extra_Dissolve( pFunc );
154 
155  // reorder the single output function
156 // if ( fVerbose )
157 // printf( "Reordering variables...\n");
158  clk1 = Abc_Clock();
159 // if ( fVerbose )
160 // printf( "Node count before = %6d\n", Cudd_DagSize( aFunc ) );
161 // Cudd_ReduceHeap(dd, CUDD_REORDER_SIFT,1);
162  Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
163  Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
164 // Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
165 // Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
166 // Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
167 // Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
168  if ( fVerbose )
169  printf( "MTBDD reordered = %6d nodes\n", Cudd_DagSize( aFunc ) );
170  if ( fVerbose )
171  printf( "Variable reordering time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
172 // printf( "\n" );
173 // printf( "Variable order is: " );
174 // for ( i = 0; i < dd->size; i++ )
175 // printf( " %d", dd->invperm[i] );
176 // printf( "\n" );
177 //fprintf( pTable, "%d ", Cudd_DagSize( aFunc ) );
178 //fprintf( pTable, "%d ", Extra_ProfileWidthMax(dd, aFunc) );
179 
180  // write the single-output function into BLIF for verification
181  clk1 = Abc_Clock();
182  if ( fCheck )
183  WriteSingleOutputFunctionBlif( dd, aFunc, pNames, nNames, FileNameIni );
184 // if ( fVerbose )
185 // printf( "Single-output function writing time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
186 
187 /*
188  ///////////////////////////////////////////////////////////////////
189  // verification of single output function
190  clk1 = Abc_Clock();
191  {
192  BFunc g_Func;
193  DdNode * aRes;
194 
195  g_Func.dd = dd;
196  g_Func.FileInput = Extra_UtilStrsav(FileNameIni);
197 
198  if ( Extra_ReadFile( &g_Func ) == 0 )
199  {
200  printf( "\nSomething did not work out while reading the input file for verification\n");
201  Extra_Dissolve( &g_Func );
202  return;
203  }
204 
205  aRes = Cudd_BddToAdd( dd, g_Func.pOutputs[0] ); Cudd_Ref( aRes );
206 
207  if ( aRes != aFunc )
208  printf( "\nVerification FAILED!\n");
209  else
210  printf( "\nVerification okay!\n");
211 
212  Cudd_RecursiveDeref( dd, aRes );
213 
214  // delocate
215  Extra_Dissolve( &g_Func );
216  }
217  printf( "Preliminary verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
218  ///////////////////////////////////////////////////////////////////
219 */
220 
221  if ( !CreateDecomposedNetwork( dd, aFunc, pNames, nNames, FileNameFin, nLutSize, fCheck, fVerbose ) )
222  return 0;
223 
224 /*
225  ///////////////////////////////////////////////////////////////////
226  // verification of the decomposed LUT network
227  clk1 = Abc_Clock();
228  {
229  BFunc g_Func;
230  DdNode * aRes;
231 
232  g_Func.dd = dd;
233  g_Func.FileInput = Extra_UtilStrsav(FileNameFin);
234 
235  if ( Extra_ReadFile( &g_Func ) == 0 )
236  {
237  printf( "\nSomething did not work out while reading the input file for verification\n");
238  Extra_Dissolve( &g_Func );
239  return;
240  }
241 
242  aRes = Cudd_BddToAdd( dd, g_Func.pOutputs[0] ); Cudd_Ref( aRes );
243 
244  if ( aRes != aFunc )
245  printf( "\nFinal verification FAILED!\n");
246  else
247  printf( "\nFinal verification okay!\n");
248 
249  Cudd_RecursiveDeref( dd, aRes );
250 
251  // delocate
252  Extra_Dissolve( &g_Func );
253  }
254  printf( "Final verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
255  ///////////////////////////////////////////////////////////////////
256 */
257 
258  // verify the results
259  if ( fCheck )
260  {
261  char Command[200];
262  sprintf( Command, "cec %s %s", FileNameIni, FileNameFin );
263  Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
264  }
265 
266  Cudd_RecursiveDeref( dd, aFunc );
267 
268  // release the names
269  for ( i = 0; i < nNames; i++ )
270  ABC_FREE( pNames[i] );
271 
272 
273 //fprintf( pTable, "\n" );
274 //fclose( pTable );
275 
276  return 1;
277 }
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cmd_CommandExecute
int Cmd_CommandExecute(void *pAbc, char *pCommandLine)
MAXINPUTS
#define MAXINPUTS
INCLUDES ///.
Definition: cas.h:38
GetSingleOutputFunction
ABC_NAMESPACE_IMPL_START DdNode * GetSingleOutputFunction(DdManager *dd, DdNode **pbOuts, int nOuts, DdNode **pbVarsEnc, int nVarsEnc, int fVerbose)
static functions ///
Definition: casCore.c:508
WriteSingleOutputFunctionBlif
void WriteSingleOutputFunctionBlif(DdManager *dd, DdNode *aFunc, char **pNames, int nNames, char *FileName)
Definition: casCore.c:781
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Extra_UtilStrsav
char * Extra_UtilStrsav(const char *s)
Definition: extraUtilUtil.c:169
CreateDecomposedNetwork
int CreateDecomposedNetwork(DdManager *dd, DdNode *aFunc, char **pNames, int nNames, char *FileName, int nLutSize, int fCheck, int fVerbose)
EXTERNAL FUNCTIONS ///.
Definition: casDec.c:108
Cudd_bddNewVarAtLevel
DdNode * Cudd_bddNewVarAtLevel(DdManager *dd, int level)
Definition: cuddAPI.c:351
Abc_FrameGetGlobalFrame
void * Abc_FrameGetGlobalFrame()
Definition: mainFrame.c:593
sprintf
char * sprintf()
strcpy
char * strcpy()
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Abc_Base2Log
static int Abc_Base2Log(unsigned n)
Definition: abc_global.h:251
strcat
char * strcat()
Cudd_ReduceHeap
int Cudd_ReduceHeap(DdManager *table, Cudd_ReorderingType heuristic, int minsize)
Definition: cuddReorder.c:176
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
MAXOUTPUTS
#define MAXOUTPUTS
Definition: cas.h:39
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Cudd_DagSize
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
Abc_Ntk_t* Abc_NtkCascade ( Abc_Ntk_t *  pNtk,
int  nLutSize,
int  fCheck,
int  fVerbose 
)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 55 of file abcCas.c.

56 {
57  DdManager * dd;
58  DdNode ** ppOutputs;
59  Abc_Ntk_t * pNtkNew;
60  Abc_Obj_t * pNode;
61  char * pFileGeneric;
62  int fBddSizeMax = 500000;
63  int i, fReorder = 1;
64  abctime clk = Abc_Clock();
65 
66  assert( Abc_NtkIsStrash(pNtk) );
67  // compute the global BDDs
68  if ( Abc_NtkBuildGlobalBdds(pNtk, fBddSizeMax, 1, fReorder, fVerbose) == NULL )
69  return NULL;
70 
71  if ( fVerbose )
72  {
73  DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk );
74  printf( "Shared BDD size = %6d nodes. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
75  ABC_PRT( "BDD construction time", Abc_Clock() - clk );
76  }
77 
78  // collect global BDDs
79  dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk );
80  ppOutputs = ABC_ALLOC( DdNode *, Abc_NtkCoNum(pNtk) );
81  Abc_NtkForEachCo( pNtk, pNode, i )
82  ppOutputs[i] = (DdNode *)Abc_ObjGlobalBdd(pNode);
83 
84  // call the decomposition
85  pFileGeneric = Extra_FileNameGeneric( pNtk->pSpec );
86  if ( !Abc_CascadeExperiment( pFileGeneric, dd, ppOutputs, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), nLutSize, fCheck, fVerbose ) )
87  {
88  // the LUT size is too small
89  }
90 
91  // for now, duplicate the network
92  pNtkNew = Abc_NtkDup( pNtk );
93 
94  // cleanup
95  Abc_NtkFreeGlobalBdds( pNtk, 1 );
96  ABC_FREE( ppOutputs );
97  ABC_FREE( pFileGeneric );
98 
99 // if ( pNtk->pExdc )
100 // pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
101  // make sure that everything is okay
102  if ( !Abc_NtkCheck( pNtkNew ) )
103  {
104  printf( "Abc_NtkCollapse: The network check has failed.\n" );
105  Abc_NtkDelete( pNtkNew );
106  return NULL;
107  }
108  return pNtkNew;
109 }
Abc_NtkIsStrash
static int Abc_NtkIsStrash(Abc_Ntk_t *pNtk)
Definition: abc.h:251
DdNode
Definition: cudd.h:278
Abc_Ntk_t_
Definition: abc.h:153
Abc_NtkDup
ABC_DLL Abc_Ntk_t * Abc_NtkDup(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:419
Abc_NtkCiNum
static int Abc_NtkCiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:287
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Abc_NtkForEachCo
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition: abc.h:519
Abc_NtkCheck
ABC_DLL int Abc_NtkCheck(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition: abcCheck.c:61
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_NtkCoNum
static int Abc_NtkCoNum(Abc_Ntk_t *pNtk)
Definition: abc.h:288
Abc_NtkDelete
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:1233
Abc_ObjGlobalBdd
static void * Abc_ObjGlobalBdd(Abc_Obj_t *pObj)
Definition: abc.h:431
Abc_Obj_t_
Definition: abc.h:128
Abc_NtkFreeGlobalBdds
ABC_DLL void * Abc_NtkFreeGlobalBdds(Abc_Ntk_t *pNtk, int fFreeMan)
Definition: abcNtbdd.c:476
Extra_FileNameGeneric
char * Extra_FileNameGeneric(char *FileName)
Definition: extraUtilFile.c:165
if
if(last==0)
Definition: sparse_int.h:34
Abc_NtkGlobalBddMan
static void * Abc_NtkGlobalBddMan(Abc_Ntk_t *pNtk)
Definition: abc.h:429
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Cudd_ReadKeys
unsigned int Cudd_ReadKeys(DdManager *dd)
Definition: cuddAPI.c:1626
Abc_CascadeExperiment
ABC_NAMESPACE_IMPL_START int Abc_CascadeExperiment(char *pFileGeneric, DdManager *dd, DdNode **pOutputs, int nInputs, int nOutputs, int nLutSize, int fCheck, int fVerbose)
DECLARATIONS ///.
Definition: casCore.c:79
assert
#define assert(ex)
Definition: util_old.h:213
Abc_NtkBuildGlobalBdds
ABC_DLL void * Abc_NtkBuildGlobalBdds(Abc_Ntk_t *pNtk, int fBddSizeMax, int fDropInternal, int fReorder, int fVerbose)
Definition: abcNtbdd.c:251
Cudd_ReadDead
unsigned int Cudd_ReadDead(DdManager *dd)
Definition: cuddAPI.c:1646
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278