biddyInOut.c File Reference

File biddyInOut.c contains various parsers and generators. More...

#include "biddyInt.h"

Include dependency graph for biddyInOut.c:

Go to the source code of this file.

Macros
#define	EVAL_SIZE   4096
#define	oNOT   0
#define	oAND   1
#define	oBUTNOT   2
#define	oNOTBUT   4
#define	oXOR   6
#define	oOR   7
#define	oNOR   8
#define	oXNOR   9
#define	oIMPLEFT   11
#define	oIMPRIGHT   13
#define	oNAND   14
#define	LINESIZE   999 /* maximum length of each input line read */
#define	BUFSIZE   99999 /* maximum length of a buffer */
#define	INOUTNUM   999 /* maximum number of inputs and outputs */
#define	REGNUM   9999 /* maximum number of registers */
#define	TOKENNUM   9999 /* maximum number of tokens */
#define	GATENUM   9999 /* maximum number of gates */
#define	LINENUM   99999 /* maximum number of lines */
#define	WIRENUM   99999 /* maximum number of wires */
#define	GATESNUM   9

Functions
Biddy_String	Biddy_Managed_Eval0 (Biddy_Manager MNG, Biddy_String s)
	Function Biddy_Managed_Eval0 evaluates raw format. More...
Biddy_Edge	Biddy_Managed_Eval1x (Biddy_Manager MNG, Biddy_String s, Biddy_LookupFunction lf)
	Function Biddy_Managed_Eval1x evaluates prefix AND-OR-EXOR-NOT format. More...
Biddy_Edge	Biddy_Managed_Eval2 (Biddy_Manager MNG, Biddy_String boolFunc)
	Function Biddy_Managed_Eval2 evaluates infix format. More...
Biddy_String	Biddy_Managed_ReadBddview (Biddy_Manager MNG, const char filename[], Biddy_String name)
	Function Biddy_Managed_ReadBddview reads bddview file and creates all Boolean functions specified by labels. More...
void	Biddy_Managed_ReadVerilogFile (Biddy_Manager MNG, const char filename[], Biddy_String prefix)
	Function Biddy_Managed_ReadVerilogFile reads Verilog file and creates variables for all primary inputs and Boolean functions for all primary outputs. More...
void	Biddy_Managed_PrintBDD (Biddy_Manager MNG, Biddy_String *var, const char filename[], Biddy_Edge f, Biddy_String label)
	Function Biddy_Managed_PrintBDD writes raw format. More...
void	Biddy_Managed_PrintTable (Biddy_Manager MNG, Biddy_String *var, const char filename[], Biddy_Edge f)
	Function Biddy_Managed_PrintTable writes truth table. More...
void	Biddy_Managed_PrintSOP (Biddy_Manager MNG, Biddy_String *var, const char filename[], Biddy_Edge f)
	Function Biddy_Managed_PrintSOP writes (non-minimal) SOP. More...
void	Biddy_Managed_PrintMinterms (Biddy_Manager MNG, Biddy_String *var, const char filename[], Biddy_Edge f, Biddy_Boolean negative)
	Function Biddy_Managed_PrintMinterms writes minterms. More...
unsigned int	Biddy_Managed_WriteDot (Biddy_Manager MNG, const char filename[], Biddy_Edge f, const char label[], int id, Biddy_Boolean cudd)
	Function Biddy_Managed_WriteDot writes dot/graphviz format using fprintf. More...
unsigned int	Biddy_Managed_WriteBddview (Biddy_Manager MNG, const char filename[], Biddy_Edge f, const char label[], void *xytable)
	Function Biddy_Managed_WriteBDDView writes bddview format using fprintf. More...

Variables
const char *	VerilogFileGateName []

Detailed Description

Description

PackageName [Biddy]
Synopsis    [Biddy provides data structures and algorithms for the
             representation and manipulation of Boolean functions with
             ROBDDs, 0-sup-BDDs, and TZBDDs. A hash table is used for quick
             search of nodes. Complement edges decreases the number of
             nodes. An automatic garbage collection with a system age is
             implemented. Variable swapping and sifting are implemented.]

FileName    [biddyInOut.c]
Revision    [$Revision: 652 $]
Date        [$Date: 2021-08-28 09:52:46 +0200 (sob, 28 avg 2021) $]
Authors     [Robert Meolic (robert@meolic.com),
             Ales Casar (ales@homemade.net),
             Volodymyr Mihav (mihaw.wolodymyr@gmail.com),
             David Kebo Houngninou (dhoungninou@smu.edu)]

Copyright

Copyright (C) 2006, 2019 UM FERI, Koroska cesta 46, SI-2000 Maribor, Slovenia. Copyright (C) 2019, 2021 Robert Meolic, SI-2000 Maribor, Slovenia.

Biddy is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.

Biddy is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.

More info

See also: biddy.h, biddyInt.h

Definition in file biddyInOut.c.

Function Documentation

Biddy_Managed_Eval0()

Biddy_String Biddy_Managed_Eval0	(	Biddy_Manager	MNG,
		Biddy_String	s
	)

Description

First word is a name. It is followed by raw format. Function return name of the formula.

Side effects

All variables should already exists in the correct ordering! Not reentrant.

More info

Macro Biddy_Eval0(s) is defined for use with anonymous manager.

Definition at line 240 of file biddyInOut.c.

Biddy_Managed_Eval1x()

Biddy_Edge Biddy_Managed_Eval1x	(	Biddy_Manager	MNG,
		Biddy_String	s,
		Biddy_LookupFunction	lf
	)

Description

Parameter lf is a lookup function in the user-defined cache table.

Side effects

Not reentrant. For ZBDDs and TZBDDs, all used variables must already exist! For ZBDDs and TZBDDs, user-defined cache is not supported!

More info

Macro Biddy_Eval1x(s,lf) is defined for use with anonymous manager. Macros Biddy_Managed_Eval1(s) and Biddy_Eval1(s) are defined for use without searching in the user-defined cache.

Definition at line 296 of file biddyInOut.c.

Biddy_Managed_Eval2()

Biddy_Edge Biddy_Managed_Eval2	(	Biddy_Manager	MNG,
		Biddy_String	boolFunc
	)

Description

Parenthesis are implemented. Operators' priority is implemented. Formula Tree is suported (global table, only). Boolean constants are '0' and '1'. Boolean operators are NOT (~!), AND (&*), OR (|+), XOR (^%), XNOR (-), IMPLIES (><), NAND (@), NOR (#), BUTNOT (), NOTBUT (/).

Side effects

More info

Original author: Volodymyr Mihav (mihaw.nosp@m..wol.nosp@m.odymy.nosp@m.r@gm.nosp@m.ail.c.nosp@m.om) Original implementation of this function is on https://github.com/sungmaster/liBDD. Macro Biddy_Eval2(boolFunc) is defined for use with anonymous manager.

Definition at line 352 of file biddyInOut.c.

Biddy_Managed_PrintBDD()

void Biddy_Managed_PrintBDD	(	Biddy_Manager	MNG,
		Biddy_String *	var,
		const char	filename[],
		Biddy_Edge	f,
		Biddy_String	label
	)

Description

This function can write to a variable, to an output channel via printf calls, and into the file via fprintf calls.

Side effects

More info

Macro Biddy_PrintBDD(f) is defined for use with anonymous manager. Macros Biddy_Managed_PrintfBDD, Biddy_PrintfBDD, Biddy_Managed_SprintfBDD, Biddy_SprintfBDD, Biddy_Managed_WriteBDD, and Biddy_WriteBDD are defined for usage in typical usecases.

Definition at line 516 of file biddyInOut.c.

Biddy_Managed_PrintMinterms()

void Biddy_Managed_PrintMinterms	(	Biddy_Manager	MNG,
		Biddy_String *	var,
		const char	filename[],
		Biddy_Edge	f,
		Biddy_Boolean	negative
	)

Description

This function can write to a variable, to an output channel via printf calls, and into the file via fprintf calls. If (negative == true) then writes complete minterms (for Boolean functions), otherwise writes only positive literals (for combination sets).

Side effects

The used algorithm is imitating writing SOP.

More info

Macro Biddy_PrintMinterms(f) is defined for use with anonymous manager. Macros Biddy_Managed_PrintfMinterms, Biddy_PrintfMinterms, Biddy_Managed_SprintfMinterms, Biddy_SprintfMinterms, Biddy_Managed_WriteMinterms, and Biddy_WriteMinterms are defined for usage in typical usecases.

Definition at line 680 of file biddyInOut.c.

Biddy_Managed_PrintSOP()

void Biddy_Managed_PrintSOP	(	Biddy_Manager	MNG,
		Biddy_String *	var,
		const char	filename[],
		Biddy_Edge	f
	)

Description

This function can write to a variable, to an output channel via printf calls, and into the file via fprintf calls.

Side effects

More info

Macro Biddy_PrintSOP(f) is defined for use with anonymous manager. Macros Biddy_Managed_PrintfSOP, Biddy_PrintfSOP, Biddy_Managed_SprintfSOP, Biddy_SprintfSOP, Biddy_Managed_WriteSOP, and Biddy_WriteSOP are defined for usage in typical usecases.

Definition at line 623 of file biddyInOut.c.

Biddy_Managed_PrintTable()

void Biddy_Managed_PrintTable	(	Biddy_Manager	MNG,
		Biddy_String *	var,
		const char	filename[],
		Biddy_Edge	f
	)

Description

This function can write to a variable, to an output channel via printf calls, and into the file via fprintf calls.

Side effects

More info

Thanks to Jan Kraner and Ziga Kobale for prototype implementation. Macro Biddy_PrintTable(f) is defined for use with anonymous manager. Macros Biddy_Managed_PrintfTable, Biddy_PrintfTable, Biddy_Managed_SprintfTable, Biddy_SprintfTable, Biddy_Managed_WriteTable, and Biddy_WriteTable are defined for usage in typical usecases.

Definition at line 570 of file biddyInOut.c.

Biddy_Managed_ReadBddview()

Biddy_String Biddy_Managed_ReadBddview	(	Biddy_Manager	MNG,
		const char	filename[],
		Biddy_String	name
	)

Description

If (name != NULL) then root formula (id = 0) is stored also with this name. Returns the list of all labels (plus the given name if it exists). Resulting BDDs are not preserved.

Side effects

BiddyManagedConstructBDD is used and thus, if variable ordering in the file is not compatible with the active ordering then the result will be wrong! To improve efficiency, only the first "type" is used. Multiples "var" and "label" are supported.

More info

Macro Biddy_ReadBddview(filename) is defined for use with anonymous manager.

Definition at line 408 of file biddyInOut.c.

Biddy_Managed_ReadVerilogFile()

void Biddy_Managed_ReadVerilogFile	(	Biddy_Manager	MNG,
		const char	filename[],
		Biddy_String	prefix
	)

Description

If (prefix != NULL) then the created BDD variables and formulae will get it.

Side effects

More info

Original author: David Kebo Houngninou, Southern Methodist University Original implementation of this function is on https://github.com/davidkebo/verilog-parser Macro Biddy_ReadVerilogFile(filename,prefix) is defined for use with anonymous manager.

Definition at line 463 of file biddyInOut.c.

Biddy_Managed_WriteBddview()

unsigned int Biddy_Managed_WriteBddview	(	Biddy_Manager	MNG,
		const char	filename[],
		Biddy_Edge	f,
		const char	label[],
		void *	xytable
	)

Description

Output bddview format. Parameter table is optional, if not NULL then it must contain node names and coordinates. If (filename == NULL) then output is to stdout.

Side effects

A conservative approach to list all the existing variables in the manager (and not only the dependent ones) is used. Variable names containing # are adpated. To support EST, also variable names containing <> are adapted. The optional table is type-casted to BiddyXYTable.

More info

Macro Biddy_WriteBddview(filename,f,label) is defined for use with anonymous manager.

Definition at line 792 of file biddyInOut.c.

Biddy_Managed_WriteDot()

unsigned int Biddy_Managed_WriteDot	(	Biddy_Manager	MNG,
		const char	filename[],
		Biddy_Edge	f,
		const char	label[],
		int	id,
		Biddy_Boolean	cudd
	)

Description

Output dot format. Two approaches are implemented. The CUDD-like implementation is copyied from CUDD 3.0.

Side effects

If (id != -1) then id is used instead of <...> for variable names. If (filename == NULL) then output is to stdout. Function resets all variables value. Variable names containing # are adpated.

More info

Macro Biddy_WriteDot(filename,f,label,id,cudd) is defined for use with anonymous manager.

Definition at line 736 of file biddyInOut.c.

Variable Documentation

VerilogFileGateName

const char* VerilogFileGateName[]

Initial value:

= {
  "buf",
  "and",
  "nand",
  "or",
  "nor",
  "xor",
  "xnor",
  "not", "inv"
}

Definition at line 80 of file biddyInOut.c.