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
BnetNetwork *	Bnet_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

Copyright

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

◆ Bnet_bddArrayDump()

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

◆ Bnet_bddDump()

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

◆ Bnet_BuildNodeBDD()

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

◆ Bnet_DfsVariableOrder()

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.

◆ Bnet_FreeNetwork()

void Bnet_FreeNetwork ( BnetNetwork * net )

Frees a boolean network created by Bnet_ReadNetwork.

Side effects None

See also: Bnet_ReadNetwork

◆ Bnet_PrintNetwork()

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

◆ Bnet_PrintOrder()

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

◆ Bnet_ReadNetwork()

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

◆ Bnet_ReadOrder()

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.

◆ bnetBlifWriteReencode()

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

◆ bnetDfsOrder()

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

◆ bnetDumpReencodingLogic()

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

◆ bnetFindVectorSupport()

static int* bnetFindVectorSupport	(	DdManager *	dd,
		DdNode **	list,
		int	n
	)

static

Finds the support of a list of DDs.

Side effects None

◆ bnetGenerateNewNames()

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

◆ bnetLevelCompare()

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

◆ bnetLevelDFS()

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

◆ bnetOrderRoots()

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

◆ bnetSetLevel()

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

◆ buildExorBDD()

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

◆ buildMuxBDD()

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

◆ printList()

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

◆ readList()

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

◆ readString()

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

Macros

Functions

Variables

Detailed Description

Function Documentation

◆ Bnet_bddArrayDump()

◆ Bnet_bddDump()

◆ Bnet_BuildNodeBDD()

◆ Bnet_DfsVariableOrder()

◆ Bnet_FreeNetwork()

◆ Bnet_PrintNetwork()

◆ Bnet_PrintOrder()

◆ Bnet_ReadNetwork()

◆ Bnet_ReadOrder()

◆ bnetBlifWriteReencode()

◆ bnetDfsOrder()

◆ bnetDumpReencodingLogic()

◆ bnetFindVectorSupport()

◆ bnetGenerateNewNames()

◆ bnetLevelCompare()

◆ bnetLevelDFS()

◆ bnetOrderRoots()

◆ bnetSetLevel()

◆ buildExorBDD()

◆ buildMuxBDD()

◆ printList()

◆ readList()

◆ readString()