Biddy  2.0.1
An academic Binary Decision Diagrams package
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 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
 
#define oAND   1
 
#define oOR   2
 
#define oEXOR   3
 

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 a Boolean function. 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: 621 $]
Date        [$Date: 2020-03-29 10:25:11 +0200 (ned, 29 mar 2020) $]
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, 2020 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 166 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.

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 220 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 276 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 440 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 604 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 547 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 494 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 name will be used for the resulting BDD. If (name == NULL) then the resulting BDD will have name given in the file. Resulting BDD will not be 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", "var", and "label" are used.

More info

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

Definition at line 332 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 387 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 716 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 660 of file biddyInOut.c.

Variable Documentation

◆ VerilogFileGateName

const char* VerilogFileGateName[]
Initial value:
= {
"buf",
"and",
"nand",
"or",
"nor",
"xor",
"xnor",
"not", "inv"
}

Definition at line 65 of file biddyInOut.c.