cudd  3.0.0
The University of Colorado Decision Diagram Package
Macros | Functions | Variables
bnet.c File Reference

Functions to read in a boolean network. More...

#include "cuddInt.h"
#include "bnet.h"
Include dependency graph for bnet.c:

Macros

#define MAXLENGTH   131072
 

Functions

BnetNetworkBnet_ReadNetwork (FILE *fp, int pr)
 Reads boolean network from blif file. More...
 
void Bnet_PrintNetwork (BnetNetwork *net)
 Prints to stdout a boolean network created by Bnet_ReadNetwork. More...
 
void Bnet_FreeNetwork (BnetNetwork *net)
 Frees a boolean network created by Bnet_ReadNetwork. More...
 
int Bnet_BuildNodeBDD (DdManager *dd, BnetNode *nd, st_table *hash, int params, int nodrop)
 Builds the BDD for the function of a node. More...
 
int Bnet_DfsVariableOrder (DdManager *dd, BnetNetwork *net)
 Orders the BDD variables by DFS. More...
 
int Bnet_bddDump (DdManager *dd, BnetNetwork *network, char *dfile, int dumpFmt, int reencoded)
 Writes the network BDDs to a file in dot, blif, or daVinci format. More...
 
int Bnet_bddArrayDump (DdManager *dd, BnetNetwork *network, char *dfile, DdNode **outputs, char **onames, int noutputs, int dumpFmt)
 Writes an array of BDDs to a file in dot, blif, DDcal, factored-form, daVinci, or blif-MV format. More...
 
int Bnet_ReadOrder (DdManager *dd, char *ordFile, BnetNetwork *net, int locGlob, int nodrop)
 Reads the variable order from a file. More...
 
int Bnet_PrintOrder (BnetNetwork *net, DdManager *dd)
 Prints the order of the DD variables of a network. More...
 
static char * readString (FILE *fp)
 Reads a string from a file. More...
 
static char ** readList (FILE *fp, int *n)
 Reads a list of strings from a line of a file. More...
 
static void printList (char **list, int n)
 Prints a list of strings to the standard output. More...
 
static char ** bnetGenerateNewNames (st_table *hash, int n)
 Generates n names not currently in a symbol table. More...
 
static int bnetDumpReencodingLogic (DdManager *dd, char *mname, int noutputs, DdNode **outputs, char **inames, char **altnames, char **onames, FILE *fp)
 Writes blif for the reencoding logic. More...
 
static int bnetBlifWriteReencode (DdManager *dd, char *mname, char **inames, char **altnames, int *support, FILE *fp)
 Writes blif for the truth table of an n-input xnor. More...
 
static int * bnetFindVectorSupport (DdManager *dd, DdNode **list, int n)
 Finds the support of a list of DDs. More...
 
static int buildExorBDD (DdManager *dd, BnetNode *nd, st_table *hash, int params, int nodrop)
 Builds BDD for a XOR function. More...
 
static int buildMuxBDD (DdManager *dd, BnetNode *nd, st_table *hash, int params, int nodrop)
 Builds BDD for a multiplexer. More...
 
static int bnetSetLevel (BnetNetwork *net)
 Sets the level of each node. More...
 
static int bnetLevelDFS (BnetNetwork *net, BnetNode *node)
 Does a DFS from a node setting the level field. More...
 
static BnetNode ** bnetOrderRoots (BnetNetwork *net, int *nroots)
 Orders network roots for variable ordering. More...
 
static int bnetLevelCompare (BnetNode **x, BnetNode **y)
 Comparison function used by qsort. More...
 
static int bnetDfsOrder (DdManager *dd, BnetNetwork *net, BnetNode *node)
 Does a DFS from a node ordering the inputs. More...
 

Variables

static char BuffLine [131072]
 
static char * CurPos
 
static int newNameNumber = 0
 

Detailed Description

Functions to read in a boolean network.

Author
Fabio Somenzi

Function Documentation

int Bnet_bddArrayDump ( DdManager dd,
BnetNetwork network,
char *  dfile,
DdNode **  outputs,
char **  onames,
int  noutputs,
int  dumpFmt 
)

Writes an array of BDDs to a file in dot, blif, DDcal, factored-form, daVinci, or blif-MV format.

The BDDs and their names are passed as arguments. The inputs and their names are taken from the network. If "-" is passed as file name, the BDDs are dumped to the standard output. The encoding of the format is:

  • 0: dot
  • 1: blif
  • 2: da Vinci
  • 3: ddcal
  • 4: factored form
  • 5: blif-MV
Returns
1 in case of success; 0 otherwise.
Side effects
None
Parameters
ddDD manager
networknetwork whose BDDs should be dumped
dfilefile name
outputsBDDs to be dumped
onamesnames of the BDDs to be dumped
noutputsnumber of BDDs to be dumped
dumpFmt0 -> dot
int Bnet_bddDump ( DdManager dd,
BnetNetwork network,
char *  dfile,
int  dumpFmt,
int  reencoded 
)

Writes the network BDDs to a file in dot, blif, or daVinci format.

If "-" is passed as file name, the BDDs are dumped to the standard output.

Returns
1 in case of success; 0 otherwise.
Side effects
None
Parameters
ddDD manager
networknetwork whose BDDs should be dumped
dfilefile name
dumpFmt0 -> dot
reencodedwhether variables have been reencoded
int Bnet_BuildNodeBDD ( DdManager dd,
BnetNode nd,
st_table hash,
int  params,
int  nodrop 
)

Builds the BDD for the function of a node.

Builds the BDD for the function of a node and stores a pointer to it in the dd field of the node itself. The reference count of the BDD is incremented. If params is BNET_LOCAL_DD, then the BDD is built in terms of the local inputs to the node; otherwise, if params is BNET_GLOBAL_DD, the BDD is built in terms of the network primary inputs. To build the global BDD of a node, the BDDs for its local inputs must exist. If that is not the case, Bnet_BuildNodeBDD recursively builds them. Likewise, to create the local BDD for a node, the local inputs must have variables assigned to them. If that is not the case, Bnet_BuildNodeBDD recursively assigns variables to nodes.

Returns
1 in case of success; 0 otherwise.
Side effects
Sets the dd field of the node.
Parameters
ddDD manager
ndnode of the boolean network
hashsymbol table of the boolean network
paramstype of DD to be built
nodropretain the intermediate node DDs until the end
int Bnet_DfsVariableOrder ( DdManager dd,
BnetNetwork net 
)

Orders the BDD variables by DFS.

Returns
1 in case of success; 0 otherwise.
Side effects
Uses the visited flags of the nodes.
void Bnet_FreeNetwork ( BnetNetwork net)

Frees a boolean network created by Bnet_ReadNetwork.

Side effects
None
See also
Bnet_ReadNetwork
void Bnet_PrintNetwork ( BnetNetwork net)

Prints to stdout a boolean network created by Bnet_ReadNetwork.

Uses the blif format; this way, one can verify the equivalence of the input and the output with, say, sis.

Side effects
None
See also
Bnet_ReadNetwork
Parameters
netboolean network
int Bnet_PrintOrder ( BnetNetwork net,
DdManager dd 
)

Prints the order of the DD variables of a network.

Only primary inputs and present states are printed.

Returns
1 if successful; 0 otherwise.
Side effects
None
BnetNetwork* Bnet_ReadNetwork ( FILE *  fp,
int  pr 
)

Reads boolean network from blif file.

A very restricted subset of blif is supported. Specifically:

  • The only directives recognized are:
    • .model
    • .inputs
    • .outputs
    • .latch
    • .names
    • .exdc
    • .wire_load_slope
    • .end
  • Latches must have an initial values and no other parameters specified.
  • Lines must not exceed MAXLENGTH-1 characters, and individual names must not exceed 1023 characters.

Caveat emptor: There may be other limitations as well. One should check the syntax of the blif file with some other tool before relying on this parser.

Returns
a pointer to the network if successful; NULL otherwise.
Side effects
None
See also
Bnet_PrintNetwork Bnet_FreeNetwork
Parameters
fppointer to the blif file
prverbosity level
int Bnet_ReadOrder ( DdManager dd,
char *  ordFile,
BnetNetwork net,
int  locGlob,
int  nodrop 
)

Reads the variable order from a file.

Returns
1 if successful; 0 otherwise.
Side effects
The BDDs for the primary inputs and present state variables are built.
static int bnetBlifWriteReencode ( DdManager dd,
char *  mname,
char **  inames,
char **  altnames,
int *  support,
FILE *  fp 
)
static

Writes blif for the truth table of an n-input xnor.

Returns
1 if successful; 0 otherwise.
Side effects
None Writes blif for the reencoding logic.

Exclusive NORs with more than two inputs are decomposed into cascaded two-input gates.

Returns
1 if successful; 0 otherwise.
Side effects
None
static int bnetDfsOrder ( DdManager dd,
BnetNetwork net,
BnetNode node 
)
static

Does a DFS from a node ordering the inputs.

Returns
1 if successful; 0 otherwise.
Side effects
Changes visited fields of the nodes it visits.
See also
Bnet_DfsVariableOrder
static int bnetDumpReencodingLogic ( DdManager dd,
char *  mname,
int  noutputs,
DdNode **  outputs,
char **  inames,
char **  altnames,
char **  onames,
FILE *  fp 
)
static

Writes blif for the reencoding logic.

Side effects
None
Parameters
ddDD manager
mnamemodel name
noutputsnumber of outputs
outputsarray of network outputs
inamesarray of network input names
altnamesarray of names of reencoded inputs
onamesarray of network output names
fpfile pointer
static int* bnetFindVectorSupport ( DdManager dd,
DdNode **  list,
int  n 
)
static

Finds the support of a list of DDs.

Side effects
None
static char** bnetGenerateNewNames ( st_table hash,
int  n 
)
static

Generates n names not currently in a symbol table.

The pointer to the symbol table may be NULL, in which case no test is made. The names generated by the procedure are unique. So, if there is no possibility of conflict with pre-existing names, NULL can be passed for the hash table.

Returns
an array of names if succesful; NULL otherwise.
Side effects
None
See also
static int bnetLevelCompare ( BnetNode **  x,
BnetNode **  y 
)
static

Comparison function used by qsort.

Used to order the variables according to the number of keys in the subtables.

Returns
the difference in number of keys between the two variables being compared.
Side effects
None
static int bnetLevelDFS ( BnetNetwork net,
BnetNode node 
)
static

Does a DFS from a node setting the level field.

Returns
1 if successful; 0 otherwise.
Side effects
Changes the level and visited fields of the nodes it visits.
See also
bnetSetLevel
static BnetNode** bnetOrderRoots ( BnetNetwork net,
int *  nroots 
)
static

Orders network roots for variable ordering.

Returns
an array with the ordered outputs and next state variables if successful; NULL otherwise.
Side effects
None
static int bnetSetLevel ( BnetNetwork net)
static

Sets the level of each node.

Returns
1 if successful; 0 otherwise.
Side effects
Changes the level and visited fields of the nodes it visits.
See also
bnetLevelDFS
static int buildExorBDD ( DdManager dd,
BnetNode nd,
st_table hash,
int  params,
int  nodrop 
)
static

Builds BDD for a XOR function.

Checks whether a function is a XOR with 2 or 3 inputs. If so, it builds the BDD.

Returns
1 if the BDD has been built; 0 otherwise.
Side effects
None
static int buildMuxBDD ( DdManager dd,
BnetNode nd,
st_table hash,
int  params,
int  nodrop 
)
static

Builds BDD for a multiplexer.

Checks whether a function is a 2-to-1 multiplexer. If so, it builds the BDD.

Returns
1 if the BDD has been built; 0 otherwise.
Side effects
None
static void printList ( char **  list,
int  n 
)
static

Prints a list of strings to the standard output.

The list is in the format created by readList.

Side effects
None
See also
readList Bnet_PrintNetwork
Parameters
listlist of pointers to strings
nlength of the list
static char** readList ( FILE *  fp,
int *  n 
)
static

Reads a list of strings from a line of a file.

The strings are sequences of characters separated by spaces or tabs. The total length of the list, white space included, must not exceed MAXLENGTH-1 characters. readList allocates memory for the strings and creates an array of pointers to the individual lists. Only two pieces of memory are allocated by readList: One to hold all the strings, and one to hold the pointers to them. Therefore, when freeing the memory allocated by readList, only the pointer to the list of pointers, and the pointer to the beginning of the first string should be freed.

Returns
the pointer to the list of pointers if successful; NULL otherwise.
Side effects
n is set to the number of strings in the list.
See also
readString printList
Parameters
fppointer to the file from which the list is read
non return, number of strings in the list
static char* readString ( FILE *  fp)
static

Reads a string from a file.

The string can be MAXLENGTH-1 characters at most. readString allocates memory to hold the string.

Returns
a pointer to the result string if successful. It returns NULL otherwise.
Side effects
None
See also
readList
Parameters
fppointer to the file from which the string is read