nanotrav/bnet.c File Reference

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

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

Defines

#define MAXLENGTH   131072

Functions

BnetNetworkBnet_ReadNetwork (FILE *fp, int pr)
 Reads boolean network from blif file.
void Bnet_PrintNetwork (BnetNetwork *net)
 Prints to stdout a boolean network created by Bnet_ReadNetwork.
void Bnet_FreeNetwork (BnetNetwork *net)
 Frees a boolean network created by Bnet_ReadNetwork.
int Bnet_BuildNodeBDD (DdManager *dd, BnetNode *nd, st_table *hash, int params, int nodrop)
 Builds the BDD for the function of a node.
int Bnet_DfsVariableOrder (DdManager *dd, BnetNetwork *net)
 Orders the BDD variables by DFS.
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.
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.
int Bnet_ReadOrder (DdManager *dd, char *ordFile, BnetNetwork *net, int locGlob, int nodrop)
 Reads the variable order from a file.
int Bnet_PrintOrder (BnetNetwork *net, DdManager *dd)
 Prints the order of the DD variables of a network.
static char * readString (FILE *fp)
 Reads a string from a file.
static char ** readList (FILE *fp, int *n)
 Reads a list of strings from a line of a file.
static void printList (char **list, int n)
 Prints a list of strings to the standard output.
static char ** bnetGenerateNewNames (st_table *hash, int n)
 Generates n names not currently in a symbol table.
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.
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.
static int * bnetFindVectorSupport (DdManager *dd, DdNode **list, int n)
 Finds the support of a list of DDs.
static int buildExorBDD (DdManager *dd, BnetNode *nd, st_table *hash, int params, int nodrop)
 Builds BDD for a XOR function.
static int buildMuxBDD (DdManager *dd, BnetNode *nd, st_table *hash, int params, int nodrop)
 Builds BDD for a multiplexer.
static int bnetSetLevel (BnetNetwork *net)
 Sets the level of each node.
static int bnetLevelDFS (BnetNetwork *net, BnetNode *node)
 Does a DFS from a node setting the level field.
static BnetNode ** bnetOrderRoots (BnetNetwork *net, int *nroots)
 Orders network roots for variable ordering.
static int bnetLevelCompare (BnetNode **x, BnetNode **y)
 Comparison function used by qsort.
static int bnetDfsOrder (DdManager *dd, BnetNetwork *net, BnetNode *node)
 Does a DFS from a node ordering the inputs.

Variables

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

Detailed Description

Functions to read in a boolean network.

Author:
Fabio Somenzi

Copyright (c) 1995-2015, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.


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:
dd DD manager
network network whose BDDs should be dumped
dfile file name
outputs BDDs to be dumped
onames names of the BDDs to be dumped
noutputs number of BDDs to be dumped
dumpFmt 0 -> 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:
dd DD manager
network network whose BDDs should be dumped
dfile file name
dumpFmt 0 -> dot
reencoded whether 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:
dd DD manager
nd node of the boolean network
hash symbol table of the boolean network
params type of DD to be built
nodrop retain 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:
net boolean 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:
fp pointer to the blif file
pr verbosity 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:
dd DD manager
mname model name
noutputs number of outputs
outputs array of network outputs
inames array of network input names
altnames array of names of reencoded inputs
onames array of network output names
fp file 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:
list list of pointers to strings
n length 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:
fp pointer to the file from which the list is read
n on 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:
fp pointer to the file from which the string is read
 All Data Structures Files Functions Variables Typedefs Enumerations Defines

Generated on 31 Dec 2015 for cudd by  doxygen 1.6.1