abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
llb2Dump.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [llb2Dump.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [BDD based reachability.]
8 
9  Synopsis [Dumps the BDD of reached states into a file.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: llb2Dump.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "llbInt.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 [Returns a dummy name.]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 char * Llb_ManGetDummyName( char * pPrefix, int Num, int nDigits )
46 {
47  static char Buffer[2000];
48  sprintf( Buffer, "%s%0*d", pPrefix, nDigits, Num );
49  return Buffer;
50 }
51 
52 /**Function*************************************************************
53 
54  Synopsis [Writes reached state BDD into a BLIF file.]
55 
56  Description []
57 
58  SideEffects []
59 
60  SeeAlso []
61 
62 ***********************************************************************/
63 void Llb_ManDumpReached( DdManager * ddG, DdNode * bReached, char * pModel, char * pFileName )
64 {
65  FILE * pFile;
66  Vec_Ptr_t * vNamesIn, * vNamesOut;
67  char * pName;
68  int i, nDigits;
69  // reorder the BDD
70  Cudd_ReduceHeap( ddG, CUDD_REORDER_SYMM_SIFT, 1 );
71 
72  // create input names
73  nDigits = Abc_Base10Log( Cudd_ReadSize(ddG) );
74  vNamesIn = Vec_PtrAlloc( Cudd_ReadSize(ddG) );
75  for ( i = 0; i < Cudd_ReadSize(ddG); i++ )
76  {
77  pName = Llb_ManGetDummyName( "ff", i, nDigits );
78  Vec_PtrPush( vNamesIn, Extra_UtilStrsav(pName) );
79  }
80  // create output names
81  vNamesOut = Vec_PtrAlloc( 1 );
82  Vec_PtrPush( vNamesOut, Extra_UtilStrsav("Reached") );
83 
84  // write the file
85  pFile = fopen( pFileName, "wb" );
86  Cudd_DumpBlif( ddG, 1, &bReached, (char **)Vec_PtrArray(vNamesIn), (char **)Vec_PtrArray(vNamesOut), pModel, pFile, 0 );
87  fclose( pFile );
88 
89  // cleanup
90  Vec_PtrForEachEntry( char *, vNamesIn, pName, i )
91  ABC_FREE( pName );
92  Vec_PtrForEachEntry( char *, vNamesOut, pName, i )
93  ABC_FREE( pName );
94  Vec_PtrFree( vNamesIn );
95  Vec_PtrFree( vNamesOut );
96 }
97 
98 ////////////////////////////////////////////////////////////////////////
99 /// END OF FILE ///
100 ////////////////////////////////////////////////////////////////////////
101 
102 
103 ABC_NAMESPACE_IMPL_END
104 
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
DdNode
Definition: cudd.h:278
Llb_ManGetDummyName
ABC_NAMESPACE_IMPL_START char * Llb_ManGetDummyName(char *pPrefix, int Num, int nDigits)
DECLARATIONS ///.
Definition: llb2Dump.c:45
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Cudd_ReadSize
int Cudd_ReadSize(DdManager *dd)
Definition: cuddAPI.c:1441
Extra_UtilStrsav
char * Extra_UtilStrsav(const char *s)
Definition: extraUtilUtil.c:169
Abc_Base10Log
static int Abc_Base10Log(unsigned n)
Definition: abc_global.h:252
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
sprintf
char * sprintf()
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Llb_ManDumpReached
void Llb_ManDumpReached(DdManager *ddG, DdNode *bReached, char *pModel, char *pFileName)
Definition: llb2Dump.c:63
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Cudd_DumpBlif
int Cudd_DumpBlif(DdManager *dd, int n, DdNode **f, char **inames, char **onames, char *mname, FILE *fp, int mv)
Definition: cuddExport.c:136
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Cudd_ReduceHeap
int Cudd_ReduceHeap(DdManager *table, Cudd_ReorderingType heuristic, int minsize)
Definition: cuddReorder.c:176
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Vec_PtrArray
static void ** Vec_PtrArray(Vec_Ptr_t *p)
Definition: vecPtr.h:279
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223