tarski.h File Reference

#include "assert.h"
#include "util.h"
#include "stdarg.h"
#include "bdd.h"

Go to the source code of this file.

Classes
class	Fnode
	Node structure - basically a cons list. More...
class	F
	Wrapper around the node stucture, facilitates op overloading. More...
class	Fvector
class	Fv
	Dummy class encapsulating Fvector --- allows us to perform operator overloading in a natural way. More...
class	Fmatrix
	A matrix of F formulas. More...
class	Fm
	Wrapper around Fmatrix, used for op overloading. More...
struct	NetStruct
	Net structure. Used to go back and forth between nodes, vars, defns, registers/NS/init, etc. More...
class	cube
	Structure encapsulating a cube - a valuation to a subset of F nodes. More...
Defines
#define	USE   __attribute__((unused))
	Macro to make an unused variable look like it's used.
#define	nil   ( ( Fnode * ) 0 )
	Convenient to refer to nil directly.
Typedefs
typedef NetStruct	Net_t
Enumerations
enum	Operator_t {   Undef_c, List_c, Pair_c, ScalarPI_c,   BooleanPI_c, ScalarReg_c, BooleanReg_c, InternalScalarVar_c,   InternalBooleanVar_c, Assign_c, And_c, Or_c,   Not_c, Iff_c, TRUE_c, FALSE_c,   Mux_c, Equal_c, UnaryFunc_c, Func_c,   Relation_c, ScalarConst_c }
	Types of operators allowed in our logic formulas. More...
Functions
Fnode *	new_node (Operator_t type, Fnode *lchild, Fnode *rchild)
	Create a new node of a give type with left and right children as specified.
Fnode *	new_node_raw (Operator_t type, Fnode *lchild, Fnode *rchild)
	Allocate a new node with params.
char *	string_register (char *aString)
	Register a new string with the global database of string.
Fnode *	node_register (Fnode *aNode)
	Test if a node with aNode's type, left and right children exists in the global database of nodes.
int	node_cmp (Fnode *aNode, Fnode *bNode)
	Straightforward compare function for Formulas.
int	node_hash (Fnode *aNode, int modulus)
	Straightforward hash function for formulas.
Fnode *	node_dup (Net_t *net, Fnode *formula, char *suf, st_table *processedTable)
	Duplicate a node and all its TFI, with prefix pre attached to each variable name from the original formulas names.
int	node_test_is_boolean (Fnode *A)
	Test if a node is a Boolean.
int	node_test_is_scalar (Fnode *A)
	Test if a node is a scalar.
F	TRUE ()
	Returns the Boolean TRUE node.
F	FALSE ()
	Returns the Boolean FALSE node.
F	si (char *name)
	Returns a scaler PI node with given name.
F	bi (char *name)
	Returns a Boolean PI node with given name.
F	sr (char *name)
	Returns a scaler reg node with given name.
F	br (char *name)
	Returns a Boolean Reg node with given name.
F	sc (char *name)
	Returns a scalar constant with given name.
F	bc (char *name)
	Returns a boolean constant with given name.
F	uif2 (char *name, F arg1, F arg2)
	Return a UIF of given name, takes 2 args.
F	uir3 (char *name, F arg1, F arg2, F arg3)
	Return a relation of given name, takes 3 args.
F	uif3 (char *name, F arg1, F arg2, F arg3)
	Return a UIF of given name, takes 3 args.
F	uif (char *name, F arg)
	Return a UIF of given name, arg.
F	assign (char *name, F arg)
	Create an assignment node.
F	mux (F c, F D1, F D0)
	Create a mux node, first arg is cond, second is if, third is else.
int	Node_HasLeftChildNode (Fnode *node)
	Check if a node has a left node; use for avoiding valgrind warnings.
int	Node_HasRightChildNode (Fnode *node)
	Check if a node has a right node; use for avoiding valgrind warnings.
Fnode *	node_GetUnique (Fnode *node)
	Return the unique node from the unique node table.
Fnode *	cons (Fnode *a, Fnode *b)
	Lisp-style cons function.
Fnode *	car (Fnode *a)
	List-style car function.
Fnode *	cdr (Fnode *a)
	List-style cdr function.
F	list (F startNode,...)
	Create a list from the arguments.
int	listlength (F aList)
	Return the length of a list.
F	ri (char *name, F restrictedList)
	Create a new scalar input whose range is restricted to the set of scalar constants in the list provided.
F	restrict (F aNode, F restrictedList)
	Take a scalar node and restrict it to the range provided in the list given.
Fnode *	nn (Operator_t a, Fnode *b, Fnode *c)
	Creates a new node with less typing.
Fnode *	rn (Fnode *aNode)
	Create/return a new node with less typing.
char *	rs (char *aString)
	Create/return a new string with less typing.
Fnode *	Mux_ThenInput (Fnode *aNode)
	Get the then input to a mux.
Fnode *	Mux_ElseInput (Fnode *aNode)
	Get the else input.
Fnode *	Reg_InitFunc (Fnode *node)
	Get the init input for a reg.
Fnode *	Reg_NsFunc (Fnode *node)
	Get the NS input for a reg.
Fnode *	Func_FirstArg (Fnode *node)
	Get the First Argument of a Function.
Fnode *	Func_SecondArg (Fnode *node)
	Get the Second Argument of a Function.
Fnode *	Func_ThirdArg (Fnode *node)
	Get the Third Argument of a Function.
Fnode *	Func_NextArg (Fnode *node, Fnode *node)
	Iterative Function to get the Next Argument.
st_table *	nodeGetSupport (F aNode)
	Get support for a node - everything down to PIs and Regs.
void	nodeGetSupportRecur (F aNode, st_table *result, st_table *processedTable)
	Function to get support for a node, proceeds recursively.
void	reg (F aReg, F nextState, F initState)
	Shorthand for setting up the next state and initial state functions for a node.
Fnode *	Net_NameToNode (Net_t *net, char *name)
	Return the node associated with a name (which could be a PI, a register, a constant, or an internal node).
Net_t *	Net_CreateFromFormula (Fnode *aFormula)
	Create a net struct from a formula.
Net_t *	Net_CreateFromFormulaArray (array_t *aFormulas)
	Create a net struct from an array of formulas.
int	Net_FreeNet (Net_t *net)
	Deallocate the net object.
int	Net_PopulateFields (Net_t *net, Fnode *aFormula, Fnode *parentFormula, st_table *processedNodes)
	Take a formula and its parent, and add it and its subformula information to the Net_t structure being created for it.
int	Net_DoBryantReduction (Net_t *net)
	Take a net structure and replace all UIFs with new PIs. Use the Bryant reduction.
int	Net_PrintFormula (Net_t *net, Fnode *formula, char *filename)
	PrintFormula Wrapper.
int	Node_PrintVHDL (Net_t *net, Fnode *formula, FILE *fptr, st_table *nodeToNameHash, st_table *processedNodes, st_table *uifInstantiateHash, st_table *uifToNumInputs, int vector_width)
	Print VHDL for a Node.
int	Net_NodeGetId (Net_t *net, Fnode *formula)
	Get id for node.
int	Net_ConstrainInput (Net_t *net, char *input, Fnode *const_formula)
	Constrain an input.
int	Net_UnConstrainInput (Net_t *net, char *input, Fnode *const_formula)
	UnConstrain an input.
array_t *	node_array_tfe (array_t *input_array, int N)
	Perform time frame expansion on an array of formulas.
Fnode *	node_tfe (Fnode *formula, int N)
	Perform time frame expansion on formula.
int	ReplaceWritewithRead (Net_t *net, char *writeUifName, char *readUifName)
	Replaces WRITEs by READs.
int	AddReadatEnd (Net_t *net, Fnode *readAddress, char *readUifName, int formula_index)
	Add Read at the end to enable replacing writes with reads.
int	Net_TopologicalSort (Fnode *aFormula, st_table *sortedTable, st_table *processedNodes)
	Topological Sorting of a Netlist.
int	Net_ConstantPropagation (st_table *sortedTable, st_table *equivalentNodeHash, int max_depth)
	Constant Propagation in a Netlist.
Fnode *	Net_SimplifyUsingConstantPropagation (Fnode *aFormula)
	Simplify a formula using constant propagation.
Fv	ivec (char *name, int N, int boolean)
Fvector *	ivecraw (char *name, int N, int boolean)
Fv	sivec (char *name, int N)
Fv	bivec (char *name, int N)
Fmatrix *	imatrixraw (char *name, int N, int M, int boolean)
Fm	imatrix (char *name, int N, int M, int boolean)
Fm	simatrix (char *name, int N, int M)
Fm	bimatrix (char *name, int N, int M)
Fmatrix *	bcm (int N, int M, int value)
Fmatrix *	raw_matrix (int N, int M)
Fvector *	raw_vector (int M)
F	matrix_lone_cols (Fm A)
F	matrix_lone_rows (Fm A)
F	vector_lone (Fv x)
Fv	operator * (Fv x, Fm M)
F	mexists (Fm A)
F	mforall (Fm A)
F	vexists (Fv A)
F	vforall (Fv A)
F	build_dlx ()
array_t *	build_dlx_impl ()
array_t *	build_dlx_impl2 ()
F	build_dlx_spec ()
array_t *	build_dlx_spec2 ()
array_t *	build_dlx_spec3 ()
F	build_fs ()
F	build_dlxuclidmain ()
F	build_dlxuclidmain_nosimplify ()
F	build_dlxuclid_seq ()
bdd_t *	nodeComputeBdd (F aNode)
int	test_bdd ()
int	bdd_print_dot (bdd_t *aBdd)
int	bdd_print_recur (bdd_t *aBdd, st_table *processedTable)
int	bdd_cmp (char *aBdd, char *bBdd)
int	bdd_hash (char *aBdd, int modulus)
st_table *	Net_ReadNodeVals (char *)
int	Net_CheckBurchFeasibility (Fnode *aFormula, Fnode *ctrl_child)
void	Net_CollectMuxes (Fnode *aFormula, st_table *mux_hash)
F	build_dlx_uclid_wholemodel ()
array_t *	build_double_instr ()
F	build_microarch_wrapper ()
array_t *	build_single_instr ()
F	build_dlx_uclid_compare ()
array_t *	build_dlx_uclid_spec ()
array_t *	build_dlx_uclid_impl ()
F	build_dlx_uclid_superscalar ()
F	build_dlx_uclid_superscalar_seq ()
F	build_fold_unfold_check ()
void	NodeAssignRegister (F reg, F init_state, F next_state)
	Sets up the initial and next state functions of a register.
Net_t *	Net_ReplaceWritewithRead (Net_t *net, char *writeUifName, char *readUifName, int output_index)
	ReplaceWritewithRead Wrapper.
Fnode *	Net_AccessOutput (Net_t *net, int output_index)
	Access the Outputs of Netlist.
int	Net_PrintVHDL (Net_t *net, int scalarWidth, char *fileName, char *entityName="example")
	Wrapper function for Net_PrintVHDL Calls Net_PrintVHDLInt.
int	Net_SetMemSize (Net_t *net, char *memName, int memSize)
	Set the size of registerfile/mem.
int	Net_AnalyzeScalarBitWidth (Net_t *net)
	Use finite domain property to come up with a bit width for scalar variables.
Variables
F	Fnil

---

Define Documentation

#define nil   ( ( Fnode * ) 0 )

Convenient to refer to nil directly. Definition at line 301 of file tarski.h. Referenced by AddReadatEnd(), bi(), br(), build_dlx_uclid_impl(), build_dlx_uclid_spec(), build_dlx_uclid_superscalar(), FALSE(), Func_NextArg(), Net_ConstantPropagation(), Net_ConstrainInput(), Net_CreateFromFormula(), Net_CreateFromFormulaArray(), Net_DoBryantReduction(), Net_UnConstrainInput(), Fnode::operator!(), ReplaceWritewithRead(), sc(), si(), sr(), and TRUE().

#define USE   __attribute__((unused))

Macro to make an unused variable look like it's used. Program checkers issue warnings about variables that are declared but never used. Most of the time, such variables should be removed to simplify the code. However, on occasion we want to keep such variables, but we don't want program checkers to complain about them. Using this macro will make an unused variable look like it's being used. This macro is straight out of the gcc documentation, Chapter 5 GCC 3.4.1. Usage: put USE immediately after the variable gcc -Wall complains about Example: int foo USE; Definition at line 281 of file tarski.h.

---

Typedef Documentation

typedef struct NetStruct Net_t

Definition at line 242 of file tarski.h. Referenced by AddReadatEnd(), build_dlx_uclid_compare(), build_dlx_uclid_superscalar_seq(), build_fold_unfold_check(), build_microarch_wrapper(), Net_AccessOutput(), Net_AnalyzeScalarBitWidth(), Net_ConstrainInput(), Net_CreateFromFormula(), Net_CreateFromFormulaArray(), Net_DoBryantReduction(), Net_FreeNet(), Net_NameToNode(), Net_NodeGetId(), Net_PopulateFields(), Net_PrintFormula(), Net_PrintVHDL(), Net_ReplaceWritewithRead(), Net_SetMemSize(), Net_UnConstrainInput(), node_array_tfe(), node_dup(), Node_PrintVHDL(), node_tfe(), and ReplaceWritewithRead().

---

Enumeration Type Documentation

enum Operator_t

Types of operators allowed in our logic formulas. Enumeration values: Undef_c  List_c  Pair_c  ScalarPI_c  BooleanPI_c  ScalarReg_c  BooleanReg_c  InternalScalarVar_c  InternalBooleanVar_c  Assign_c  And_c  Or_c  Not_c  Iff_c  TRUE_c  FALSE_c  Mux_c  Equal_c  UnaryFunc_c  Func_c  Relation_c  ScalarConst_c  Definition at line 34 of file tarski.h. Referenced by Node_PrintVHDL(), nodeGetSupportRecur(), and F::type().

---

Function Documentation

int AddReadatEnd (  Net_t *  net, Fnode *  readAddress, char *  readUifName, int  formula_index )

Add Read at the end to enable replacing writes with reads. Definition at line 4028 of file net.c. References Equal_c, NetStruct::formulas, Func_c, Fnode::lchild, List_c, Net_t, new_node_raw(), nil, node_cmp(), node_hash(), Not_c, and Fnode::rchild. Referenced by build_dlx_uclid_compare(), and Net_ReplaceWritewithRead().

F assign (  char *  name, F  arg )

Create an assignment node. Prob not ever needed, since the need for assigns seems to be an artefact of uclid. Definition at line 863 of file node.c. References Assign_c, new_node(), F::raw, and rs().

F bc (  char *  name  )

Returns a boolean constant with given name. Tricky - need this to be a node that holds its value, but its value can be arbitrary. Implemented via some logic. Different from sc which creates a single node with that constant explicitly defined by the name field. Definition at line 757 of file node.c. References bi(), br(), and reg().

Fmatrix* bcm (  int  N, int  M, int  value )

int bdd_cmp (  char *  aBdd, char *  bBdd )

Function******************************************************************** Synopsis [Compare function for bdd_t] Description [Compare function for bdd_t] SideEffects [] SeeAlso [] Definition at line 267 of file bdd.c. Referenced by bdd_print_dot().

int bdd_hash (  char *  aBdd, int  modulus )

Function******************************************************************** Synopsis [Hash function for bdd_t] Description [Hash function for bdd_t] SideEffects [] SeeAlso [] Definition at line 302 of file bdd.c. Referenced by bdd_print_dot().

int bdd_print_dot (  bdd_t *  aBdd  )

Function******************************************************************** Synopsis [Print a bdd in dot format] Description [Print a bdd in dot format] SideEffects [] SeeAlso [] Definition at line 169 of file bdd.c. References bdd_cmp(), bdd_hash(), and bdd_print_recur().

int bdd_print_recur (  bdd_t *  aBdd, st_table *  processedTable )

Function******************************************************************** Synopsis [Print each bdd node one at a time] Description [Print each bdd node one at a time. There's no chance a GC will take place in this routine, so we can key off of the bdd_node field.] SideEffects [] SeeAlso [] Definition at line 199 of file bdd.c. References indexToName. Referenced by bdd_print_dot().

F bi (  char *  name  )

Returns a Boolean PI node with given name. Definition at line 643 of file node.c. References BooleanPI_c, nil, nn(), F::raw, and rs(). Referenced by bc(), build_dlx_uclid_impl(), and build_dlx_uclid_superscalar().

Fm bimatrix (  char *  name, int  N, int  M )

Fv bivec (  char *  name, int  N )

F br (  char *  name  )

Returns a Boolean Reg node with given name. Need to tack on the init-ns list (e.g., with <<) Definition at line 716 of file node.c. References BooleanReg_c, nil, nn(), F::raw, and rs(). Referenced by bc(), build_dlx_uclid_compare(), build_dlx_uclid_impl(), build_dlx_uclid_spec(), build_dlx_uclid_superscalar(), build_double_instr(), build_fold_unfold_wrapper(), and build_single_instr().

F build_dlx (   )

array_t* build_dlx_impl (   )

array_t* build_dlx_impl2 (   )

F build_dlx_spec (   )

array_t* build_dlx_spec2 (   )

array_t* build_dlx_spec3 (   )

F build_dlx_uclid_compare (   )

Definition at line 6 of file dlx_deep_pipeline_uclid.c. References AddReadatEnd(), br(), build_dlx_uclid_impl(), build_dlx_uclid_spec(), FALSE(), NetStruct::formulas, Net_ConstantPropagation(), Net_ConstrainInput(), Net_CreateFromFormulaArray(), Net_DoBryantReduction(), Net_FreeNet(), Net_PrintFormula(), Net_t, Net_TopologicalSort(), Net_UnConstrainInput(), node_tfe(), F::raw, ReplaceWritewithRead(), si(), TRUE(), and NetStruct::UIFs.

array_t* build_dlx_uclid_impl (   )

Definition at line 616 of file dlx_deep_pipeline_uclid.c. References bi(), br(), FALSE(), list(), mux(), nil, F::raw, restrict(), ri(), sc(), si(), sr(), TRUE(), uif(), uif2(), uif3(), and uir3(). Referenced by build_dlx_uclid_compare().

array_t* build_dlx_uclid_spec (   )

Definition at line 818 of file dlx_deep_pipeline_uclid.c. References br(), FALSE(), list(), mux(), nil, F::raw, restrict(), sc(), si(), sr(), TRUE(), uif(), uif2(), uif3(), and uir3(). Referenced by build_dlx_uclid_compare().

F build_dlx_uclid_superscalar (   )

Definition at line 927 of file dlx_deep_pipeline_uclid.c. References bi(), br(), FALSE(), list(), mux(), nil, restrict(), ri(), sc(), si(), sr(), TRUE(), uif(), uif2(), uif3(), and uir3(). Referenced by build_dlx_uclid_superscalar_seq().

F build_dlx_uclid_superscalar_seq (   )

Definition at line 1432 of file dlx_deep_pipeline_uclid.c. References build_dlx_uclid_superscalar(), Net_ConstantPropagation(), Net_CreateFromFormula(), Net_PrintVHDL(), Net_t, Net_TopologicalSort(), and F::raw.

F build_dlx_uclid_wholemodel (   )

F build_dlxuclid_seq (   )

F build_dlxuclidmain (   )

F build_dlxuclidmain_nosimplify (   )

array_t* build_double_instr (   )

Definition at line 7 of file micro_arch.c. References br(), FALSE(), mux(), F::raw, sc(), si(), sr(), TRUE(), uif(), uif2(), and uif3(). Referenced by build_microarch_wrapper().

F build_fold_unfold_check (   )

Definition at line 9 of file fold_unfold.c. References build_fold_unfold_wrapper(), NetStruct::formulas, Net_CreateFromFormula(), Net_DoBryantReduction(), Net_PrintVHDL(), Net_t, node_tfe(), and F::raw.

F build_fs (   )

Referenced by test_bdd().

F build_microarch_wrapper (   )

Definition at line 162 of file micro_arch.c. References build_double_instr(), build_single_instr(), Net_CreateFromFormula(), Net_CreateFromFormulaArray(), Net_PrintVHDL(), Net_t, and F::raw.

array_t* build_single_instr (   )

Definition at line 214 of file micro_arch.c. References br(), FALSE(), mux(), F::raw, sc(), si(), sr(), TRUE(), uif(), uif2(), and uif3(). Referenced by build_microarch_wrapper().

Fnode* car (  Fnode *  a  )

List-style car function. Definition at line 981 of file node.c. References Fnode::lchild.

Fnode* cdr (  Fnode *  a  )

List-style cdr function. Definition at line 994 of file node.c. References Fnode::rchild.

Fnode* cons (  Fnode *  a, Fnode *  b )

Lisp-style cons function. Definition at line 962 of file node.c. References Fnode::lchild, Fnode::rchild, and Fnode::type.

F FALSE (   )

Returns the Boolean FALSE node. Definition at line 609 of file node.c. References FALSE_c, nil, nn(), and F::raw. Referenced by build_dlx_uclid_compare(), build_dlx_uclid_impl(), build_dlx_uclid_spec(), build_dlx_uclid_superscalar(), build_double_instr(), build_fold_unfold_wrapper(), and build_single_instr().

Fnode* Func_FirstArg (  Fnode *  node  )

Get the First Argument of a Function. Definition at line 1260 of file node.c. References Func_c, Fnode::rchild, Fnode::type, and UnaryFunc_c. Referenced by Node_PrintVHDL(), and ReplaceWritewithRead().

Fnode* Func_NextArg (  Fnode *  node, Fnode *  node )

Iterative Function to get the Next Argument. Definition at line 1317 of file node.c. References Func_c, Fnode::lchild, nil, Fnode::type, and UnaryFunc_c.

Fnode* Func_SecondArg (  Fnode *  node  )

Get the Second Argument of a Function. Definition at line 1275 of file node.c. References Func_c, Fnode::rchild, and Fnode::type. Referenced by ReplaceWritewithRead().

Fnode* Func_ThirdArg (  Fnode *  node  )

Get the Third Argument of a Function. Definition at line 1296 of file node.c. References Func_c, Fnode::rchild, and Fnode::type.

Fm imatrix (  char *  name, int  N, int  M, int  boolean )

Fmatrix* imatrixraw (  char *  name, int  N, int  M, int  boolean )

Fv ivec (  char *  name, int  N, int  boolean )

Fvector* ivecraw (  char *  name, int  N, int  boolean )

F list (  F  startNode,   ... )

Create a list from the arguments. Currently checks to make sure all arguments are scalars; this may be overly conservative for some applications. Definition at line 1011 of file node.c. References Fnil, List_c, new_node(), and F::raw. Referenced by build_dlx_uclid_impl(), build_dlx_uclid_spec(), build_dlx_uclid_superscalar(), uif(), uif2(), and uif3().

int listlength (  F  aList  )

Return the length of a list. Definition at line 1047 of file node.c. References F::raw, F::rchild(), and F::type().

F matrix_lone_cols (  Fm  A  )

F matrix_lone_rows (  Fm  A  )

F mexists (  Fm  A  )

F mforall (  Fm  A  )

F mux (  F  c, F  D1, F  D0 )

Create a mux node, first arg is cond, second is if, third is else. Definition at line 883 of file node.c. References Mux_c, new_node(), and F::raw. Referenced by build_dlx_uclid_impl(), build_dlx_uclid_spec(), build_dlx_uclid_superscalar(), build_double_instr(), build_fold_unfold_wrapper(), build_single_instr(), restrict(), and ri().

Fnode* Mux_ElseInput (  Fnode *  aNode  )

Get the else input. Definition at line 1215 of file node.c. References Mux_c, Fnode::rchild, and Fnode::type. Referenced by Net_CheckBurchFeasibility(), Net_ConstantPropagation(), and Node_PrintVHDL().

Fnode* Mux_ThenInput (  Fnode *  aNode  )

Get the then input to a mux. Definition at line 1200 of file node.c. References Fnode::lchild, Mux_c, Fnode::rchild, and Fnode::type. Referenced by Net_CheckBurchFeasibility(), Net_ConstantPropagation(), and Node_PrintVHDL().

Fnode* Net_AccessOutput (  Net_t *  net, int  output_index )

Access the Outputs of Netlist. Definition at line 950 of file net.c. References NetStruct::formulas, and Net_t.

int Net_AnalyzeScalarBitWidth (  Net_t *  net  )

Use finite domain property to come up with a bit width for scalar variables. Definition at line 998 of file net.c. References Net_t, NetStruct::PIs, and Fnode::type.

int Net_CheckBurchFeasibility (  Fnode *  aFormula, Fnode *  ctrl_child )

Definition at line 4548 of file net.c. References And_c, BooleanPI_c, BooleanReg_c, Equal_c, FALSE_c, Func_c, Iff_c, InternalBooleanVar_c, InternalScalarVar_c, List_c, Mux_c, Mux_ElseInput(), Mux_ThenInput(), Not_c, Or_c, Pair_c, Reg_InitFunc(), Reg_NsFunc(), ScalarConst_c, ScalarPI_c, ScalarReg_c, TRUE_c, Fnode::type, UnaryFunc_c, and Undef_c.

void Net_CollectMuxes (  Fnode *  aFormula, st_table *  mux_hash )

Definition at line 4634 of file net.c. References And_c, BooleanPI_c, BooleanReg_c, Equal_c, FALSE_c, Func_c, Iff_c, InternalBooleanVar_c, InternalScalarVar_c, List_c, Mux_c, Not_c, Or_c, Pair_c, Reg_InitFunc(), Reg_NsFunc(), ScalarConst_c, ScalarPI_c, ScalarReg_c, TRUE_c, Fnode::type, UnaryFunc_c, and Undef_c.

int Net_ConstantPropagation (  st_table *  sortedTable, st_table *  equivalentNodeHash, int  max_depth )

Constant Propagation in a Netlist. Definition at line 4181 of file net.c. References And_c, BooleanPI_c, BooleanReg_c, Equal_c, FALSE_c, Func_c, Iff_c, InternalBooleanVar_c, InternalScalarVar_c, Fnode::lchild, List_c, Mux_c, Mux_ElseInput(), Mux_ThenInput(), new_node_raw(), nil, node_GetUnique(), Not_c, Or_c, Pair_c, Fnode::rchild, ScalarConst_c, ScalarPI_c, ScalarReg_c, TRUE_c, Fnode::type, UnaryFunc_c, and Undef_c. Referenced by build_dlx_uclid_compare(), build_dlx_uclid_superscalar_seq(), and Net_SimplifyUsingConstantPropagation().

int Net_ConstrainInput (  Net_t *  net, char *  input, Fnode *  const_formula )

Constrain an input. Definition at line 865 of file net.c. References Net_NameToNode(), Net_t, nil, node_cmp(), and node_hash(). Referenced by build_dlx_uclid_compare().

Net_t* Net_CreateFromFormula (  Fnode *  aFormula  )

Create a net struct from a formula. Definition at line 106 of file net.c. References NetStruct::allNodes, NetStruct::constants, NetStruct::formulas, NetStruct::memToSizeHash, NetStruct::nameToNodeHash, Net_PopulateFields(), Net_t, nil, node_cmp(), node_hash(), NetStruct::nodeToFanoutArray, NetStruct::nodeToId, NetStruct::numNodes, NetStruct::PIs, and NetStruct::UIFs. Referenced by build_dlx_uclid_superscalar_seq(), build_fold_unfold_check(), build_microarch_wrapper(), Net_ReplaceWritewithRead(), and node_tfe().

Net_t* Net_CreateFromFormulaArray (  array_t *  aFormulas  )

Create a net struct from an array of formulas. Definition at line 150 of file net.c. References NetStruct::allNodes, NetStruct::constants, NetStruct::formulas, NetStruct::memToSizeHash, NetStruct::nameToNodeHash, Net_PopulateFields(), Net_t, nil, node_cmp(), node_hash(), NetStruct::nodeToFanoutArray, NetStruct::nodeToId, NetStruct::numNodes, NetStruct::PIs, and NetStruct::UIFs. Referenced by build_dlx_uclid_compare(), build_microarch_wrapper(), and node_array_tfe().

int Net_DoBryantReduction (  Net_t *  net  )

Take a net structure and replace all UIFs with new PIs. Use the Bryant reduction. Given * F u_0, F u_1, F u_2,... F u_{n-1} * replace these with * v_0 * (u_1 = u_0 ) ? v_0 : * v_1 * (u_2 = u_0 ) ? v_0 : * (u_2 = u_1 ) ? v_1 : * v_2 * (u_{n-1} = u_0 ) ? v_0 : * (u_{n-1} = u_1 ) ? v_1 : * (u_{n-1} = u_{n-2}) ? v_{n-2} : * v_{n-1} * This is quadratic in complexity, but avoids the comparisons between v_i's, which is the case for the Ackerman reduction, wherein for each i, j<i there's a constraint u_i = u_j v_i = v_j. The Ackermann style also add a lot of logic flowing to the output node. As implemented, the Net_t structure passed in is corrupted, since we change fanouts, remove/add nodes, etc. Rather than try to repair the structure on the fly, it's better to recreate it from the new formula. Definition at line 383 of file net.c. References Fnode::lchild, Net_t, new_node(), nil, node_cmp(), node_hash(), Fnode::rchild, ScalarPI_c, and NetStruct::UIFs. Referenced by build_dlx_uclid_compare(), and build_fold_unfold_check().

int Net_FreeNet (  Net_t *  net  )

Deallocate the net object. Definition at line 192 of file net.c. References NetStruct::allNodes, NetStruct::constants, NetStruct::memToSizeHash, NetStruct::nameToNodeHash, Net_t, NetStruct::nodeToFanoutArray, NetStruct::nodeToId, NetStruct::PIs, and NetStruct::UIFs. Referenced by build_dlx_uclid_compare(), and Net_ReplaceWritewithRead().

Fnode* Net_NameToNode (  Net_t *  net, char *  name )

Return the node associated with a name (which could be a PI, a register, a constant, or an internal node). Definition at line 84 of file net.c. References NetStruct::nameToNodeHash, and Net_t. Referenced by Net_ConstrainInput(), and Net_UnConstrainInput().

int Net_NodeGetId (  Net_t *  net, Fnode *  formula )

Get id for node. Definition at line 845 of file net.c. References Net_t, and NetStruct::nodeToId.

int Net_PopulateFields (  Net_t *  net, Fnode *  aFormula, Fnode *  parentFormula, st_table *  processedNodes )

Take a formula and its parent, and add it and its subformula information to the Net_t structure being created for it. We need the parent to fill in the fanout information. Definition at line 226 of file net.c. References NetStruct::allNodes, NetStruct::constants, Fnode::lchild, NetStruct::nameToNodeHash, Net_t, Node_HasLeftChildNode(), Node_HasRightChildNode(), NetStruct::nodeToFanoutArray, NetStruct::nodeToId, NetStruct::numNodes, NetStruct::PIs, Fnode::rchild, ScalarConst_c, Fnode::type, and NetStruct::UIFs. Referenced by Net_CreateFromFormula(), and Net_CreateFromFormulaArray().

int Net_PrintFormula (  Net_t *  net, Fnode *  formula, char *  filename )

PrintFormula Wrapper. Definition at line 1105 of file net.c. References Net_t. Referenced by build_dlx_uclid_compare().

int Net_PrintVHDL (  Net_t *  net, int  scalarWidth, char *  fileName, char *  entityName = "example" )

Wrapper function for Net_PrintVHDL Calls Net_PrintVHDLInt. Definition at line 964 of file net.c. References Net_t. Referenced by build_dlx_uclid_superscalar_seq(), build_fold_unfold_check(), and build_microarch_wrapper().

st_table* Net_ReadNodeVals (  char *   )

Definition at line 4520 of file net.c.

Net_t* Net_ReplaceWritewithRead (  Net_t *  net, char *  writeUifName, char *  readUifName, int  output_index )

ReplaceWritewithRead Wrapper. This function will first add a generic Read (with random read_address) at the specific output and then call the ReplaceWritewithRead function to perform the actual transformation Definition at line 917 of file net.c. References AddReadatEnd(), NetStruct::formulas, Net_CreateFromFormula(), Net_FreeNet(), Net_t, F::raw, ReplaceWritewithRead(), si(), and NetStruct::UIFs.

int Net_SetMemSize (  Net_t *  net, char *  memName, int  memSize )

Set the size of registerfile/mem. Definition at line 978 of file net.c. References NetStruct::memToSizeHash, and Net_t.

Fnode* Net_SimplifyUsingConstantPropagation (  Fnode *  aFormula  )

Simplify a formula using constant propagation. Definition at line 4695 of file net.c. References Net_ConstantPropagation(), and Net_TopologicalSort().

int Net_TopologicalSort (  Fnode *  aFormula, st_table *  sortedTable, st_table *  processedNodes )

Topological Sorting of a Netlist. Definition at line 4080 of file net.c. References And_c, BooleanPI_c, BooleanReg_c, Equal_c, FALSE_c, Func_c, Iff_c, InternalBooleanVar_c, InternalScalarVar_c, List_c, Mux_c, Not_c, Or_c, Pair_c, ScalarConst_c, ScalarPI_c, ScalarReg_c, TRUE_c, UnaryFunc_c, and Undef_c. Referenced by build_dlx_uclid_compare(), build_dlx_uclid_superscalar_seq(), and Net_SimplifyUsingConstantPropagation().

int Net_UnConstrainInput (  Net_t *  net, char *  input, Fnode *  const_formula )

UnConstrain an input. Definition at line 893 of file net.c. References Net_NameToNode(), Net_t, and nil. Referenced by build_dlx_uclid_compare().

Fnode* new_node (  Operator_t  type, Fnode *  lchild, Fnode *  rchild )

Create a new node of a give type with left and right children as specified. Need to take care that we don't created different nodes for single variable formulas repeatedly. This is what the call to node_register is for. lchild and rchild must be legal nodes, or a string (for lchild) or nil. Definition at line 78 of file node.c. References new_node_raw(), and node_register(). Referenced by assign(), list(), mux(), Net_DoBryantReduction(), nn(), uif(), uif2(), and uif3().

Fnode* new_node_raw (  Operator_t  type, Fnode *  lchild, Fnode *  rchild )

Allocate a new node with params. Definition at line 99 of file node.c. References Fnode::lchild, Fnode::rchild, and Fnode::type. Referenced by AddReadatEnd(), Net_ConstantPropagation(), new_node(), Fnode::operator &(), Fnode::operator!(), Fnode::operator%(), Fnode::operator==(), and Fnode::operator|().

Fnode* nn (  Operator_t  a, Fnode *  b, Fnode *  c )

Creates a new node with less typing. See also: new_node() Definition at line 1156 of file node.c. References new_node(). Referenced by bi(), br(), FALSE(), sc(), si(), sr(), and TRUE().

array_t* node_array_tfe (  array_t *  input_array, int  N )

Perform time frame expansion on an array of formulas. Definition at line 1026 of file net.c. References Net_CreateFromFormulaArray(), Net_t, and node_dup().

int node_cmp (  Fnode *  aNode, Fnode *  bNode )

Straightforward compare function for Formulas. Not complete, but assuming children are reasonably canonical, the check is reasonable, and covers the impt case, namely PIs. Note that st expects -1, 0, +1, based on whether one node is less, equal or greater. Definition at line 229 of file node.c. References Fnode::lchild, Fnode::rchild, and Fnode::type. Referenced by AddReadatEnd(), cube::cube(), Net_ConstrainInput(), Net_CreateFromFormula(), Net_CreateFromFormulaArray(), Net_DoBryantReduction(), node_register(), nodeComputeBdd(), nodeGetSupport(), and ReplaceWritewithRead().

Fnode* node_dup (  Net_t *  net, Fnode *  formula, char *  suf, st_table *  processedTable )

Duplicate a node and all its TFI, with prefix pre attached to each variable name from the original formulas names. Definition at line 284 of file node.c. References Net_t. Referenced by node_array_tfe().

Fnode* node_GetUnique (  Fnode *  node  )

Return the unique node from the unique node table. Definition at line 1424 of file node.c. References nodeHash. Referenced by Net_ConstantPropagation().

int node_hash (  Fnode *  aNode, int  modulus )

Straightforward hash function for formulas. Could be heavily optimized, but formula manipulation is unlikely to be on the critical path. Definition at line 264 of file node.c. References Fnode::lchild, Fnode::rchild, and Fnode::type. Referenced by AddReadatEnd(), cube::cube(), Net_ConstrainInput(), Net_CreateFromFormula(), Net_CreateFromFormulaArray(), Net_DoBryantReduction(), node_register(), nodeComputeBdd(), nodeGetSupport(), and ReplaceWritewithRead().

int Node_HasLeftChildNode (  Fnode *  node  )

Check if a node has a left node; use for avoiding valgrind warnings. Definition at line 904 of file node.c. References Fnode::type. Referenced by Net_PopulateFields().

int Node_HasRightChildNode (  Fnode *  node  )

Check if a node has a right node; use for avoiding valgrind warnings. Definition at line 931 of file node.c. References Fnode::type. Referenced by Net_PopulateFields().

int Node_PrintVHDL (  Net_t *  net, Fnode *  formula, FILE *  fptr, st_table *  nodeToNameHash, st_table *  processedNodes, st_table *  uifInstantiateHash, st_table *  uifToNumInputs, int  vector_width )

Print VHDL for a Node. Definition at line 607 of file net.c. References And_c, Assign_c, BooleanPI_c, BooleanReg_c, Equal_c, FALSE_c, Func_c, Func_FirstArg(), Iff_c, InternalBooleanVar_c, InternalScalarVar_c, List_c, Mux_c, Mux_ElseInput(), Mux_ThenInput(), Net_t, NetStruct::nodeToId, Not_c, Operator_t, Or_c, Pair_c, Reg_InitFunc(), Reg_NsFunc(), ScalarConst_c, ScalarPI_c, ScalarReg_c, TRUE_c, Fnode::type, UnaryFunc_c, and Undef_c.

Fnode* node_register (  Fnode *  aNode  )

Test if a node with aNode's type, left and right children exists in the global database of nodes. If so, free node, and return representative. Otherwise, dup the node, insert it. aNode is always freed! Definition at line 155 of file node.c. References Fnode::lchild, node_cmp(), node_hash(), nodeHash, Fnode::rchild, and Fnode::type. Referenced by new_node(), and rn().

int node_test_is_boolean (  Fnode *  A  )

Test if a node is a Boolean. Definition at line 544 of file node.c. References Fnode::type. Referenced by nodeComputeBdd(), nodeGetSupportRecur(), Fnode::operator &(), Fnode::operator!(), Fnode::operator%(), F::operator()(), Fnode::operator==(), Fnode::operator^(), and Fnode::operator|().

int node_test_is_scalar (  Fnode *  A  )

Test if a node is a scalar. Definition at line 571 of file node.c. References Fnode::type. Referenced by Fnode::operator%(), and Fnode::operator==().

Fnode* node_tfe (  Fnode *  formula, int  N )

Perform time frame expansion on formula. Definition at line 1069 of file net.c. References Net_CreateFromFormula(), and Net_t. Referenced by build_dlx_uclid_compare(), and build_fold_unfold_check().

void NodeAssignRegister (  F  reg, F  init_state, F  next_state )

Sets up the initial and next state functions of a register. Definition at line 1441 of file node.c. References reg().

bdd_t* nodeComputeBdd (  F  aNode  )

Function******************************************************************** Synopsis [Create a Bdd for the given formula node. Tree rooted at node is assumed to consist solely of Boolean nodes. Returns a freshly allocated bdd_t, caller is responsible for freeing.] Description [Create a Bdd for the given formula node. Tree rooted at node is assumed to consist solely of Boolean nodes. Returns a freshly allocated bdd_t, caller is responsible for freeing. Proceeds recursively - recursion stops at PIs and registers, with which we associate bdd variables. Right now, we don't do any ordering, just tack new variables on at the end, let the reordering figure out orders. We associate F nodes with bdd_t's and therefore even in the presence of garbage collection and reordering, wherein the bdd_node field changes for the bdd_t's we are safe, since the manager will automatically update these fields.] Definition at line 62 of file bdd.c. References And_c, bddMgr, FALSE_c, Iff_c, indexToName, F::lchild(), node_cmp(), node_hash(), node_test_is_boolean(), nodeToBdd, Not_c, Or_c, F::raw, F::rchild(), TRUE_c, and F::type().

st_table* nodeGetSupport (  F  aNode  )

Get support for a node - everything down to PIs and Regs. Definition at line 1338 of file node.c. References node_cmp(), node_hash(), and nodeGetSupportRecur(). Referenced by test_bdd().

void nodeGetSupportRecur (  F  aNode, st_table *  result, st_table *  processedTable )

Function to get support for a node, proceeds recursively. Needs more thought on how to handle scalar ops, but for now focus just on boolean case. See also: nodeGetSupport() Definition at line 1362 of file node.c. References F::lchild(), node_test_is_boolean(), Operator_t, F::raw, F::rchild(), and F::type(). Referenced by nodeGetSupport().

Fv operator * (  Fv  x, Fm  M )

Fmatrix* raw_matrix (  int  N, int  M )

Fvector* raw_vector (  int  M  )

void reg (  F  aReg, F  nextState, F  initState )

Shorthand for setting up the next state and initial state functions for a node. Definition at line 1407 of file node.c. Referenced by bc(), and NodeAssignRegister().

Fnode* Reg_InitFunc (  Fnode *  node  )

Get the init input for a reg. Definition at line 1230 of file node.c. References BooleanReg_c, Fnode::rchild, ScalarReg_c, and Fnode::type. Referenced by Net_CheckBurchFeasibility(), Net_CollectMuxes(), and Node_PrintVHDL().

Fnode* Reg_NsFunc (  Fnode *  node  )

Get the NS input for a reg. Definition at line 1245 of file node.c. References BooleanReg_c, Fnode::rchild, ScalarReg_c, and Fnode::type. Referenced by Net_CheckBurchFeasibility(), Net_CollectMuxes(), and Node_PrintVHDL().

int ReplaceWritewithRead (  Net_t *  net, char *  writeUifName, char *  readUifName )

Replaces WRITEs by READs. Definition at line 3845 of file net.c. References Func_FirstArg(), Func_SecondArg(), Net_t, nil, node_cmp(), node_hash(), and NetStruct::UIFs. Referenced by build_dlx_uclid_compare(), and Net_ReplaceWritewithRead().

F restrict (  F  aNode, F  restrictedList )

Take a scalar node and restrict it to the range provided in the list given. We see the need for this e.g. in the dlx example from uclid, where next\fdType\ := itype(next\[fdInstr\]); and fdInstr is given by ( Fetch Stage *) init\fdInstr\ := fdi0; ( initially arbitrary *) next\fdInstr\ := case stall: fdInstr; ( Stalling *) default: imem(pPC); ( Read from instruction memory *) esac; Definition at line 1121 of file node.c. References F::lchild(), mux(), F::raw, F::rchild(), and F::type(). Referenced by build_dlx_uclid_impl(), build_dlx_uclid_spec(), and build_dlx_uclid_superscalar().

F ri (  char *  name, F  restrictedList )

Create a new scalar input whose range is restricted to the set of scalar constants in the list provided. Definition at line 1070 of file node.c. References F::lchild(), mux(), F::raw, F::rchild(), si(), and F::type(). Referenced by build_dlx_uclid_impl(), and build_dlx_uclid_superscalar().

Fnode* rn (  Fnode *  aNode  )

Create/return a new node with less typing. See also: register_node() Definition at line 1172 of file node.c. References node_register(). Referenced by Fnode::operator &(), Fnode::operator!(), Fnode::operator%(), Fnode::operator==(), and Fnode::operator|().

char* rs (  char *  aString  )

Create/return a new string with less typing. See also: register_string() Definition at line 1186 of file node.c. References string_register(). Referenced by assign(), bi(), br(), sc(), si(), sr(), uif(), uif2(), and uif3().

F sc (  char *  name  )

Returns a scalar constant with given name. Definition at line 735 of file node.c. References nil, nn(), F::raw, rs(), and ScalarConst_c. Referenced by build_dlx_uclid_impl(), build_dlx_uclid_spec(), build_dlx_uclid_superscalar(), build_double_instr(), build_single_instr(), and uir3().

F si (  char *  name  )

Returns a scaler PI node with given name. Definition at line 624 of file node.c. References nil, nn(), F::raw, rs(), and ScalarPI_c. Referenced by build_dlx_uclid_compare(), build_dlx_uclid_impl(), build_dlx_uclid_spec(), build_dlx_uclid_superscalar(), build_double_instr(), build_fold_unfold_wrapper(), build_single_instr(), Net_ReplaceWritewithRead(), and ri().

Fm simatrix (  char *  name, int  N, int  M )

Fv sivec (  char *  name, int  N )

F sr (  char *  name  )

Returns a scaler reg node with given name. Need to add the init-NS node list later (e.g., using <<) Definition at line 696 of file node.c. References nil, nn(), F::raw, rs(), and ScalarReg_c. Referenced by build_dlx_uclid_impl(), build_dlx_uclid_spec(), build_dlx_uclid_superscalar(), build_double_instr(), build_fold_unfold_wrapper(), and build_single_instr().

char* string_register (  char *  aString  )

Register a new string with the global database of string. Takes a char , returns a pointer to that string in the global database (stringHash). Does not free the string passed in. Create a duplicate the first time a string is added. Definition at line 123 of file node.c. References stringHash. Referenced by rs().

int test_bdd (   )

Function******************************************************************** Synopsis [Test the bdd routines] Description [Test the bdd routines] Definition at line 129 of file bdd.c. References build_fs(), nodeGetSupport(), and cube::nodeToValue.

F TRUE (   )

Returns the Boolean TRUE node. Definition at line 594 of file node.c. References nil, nn(), F::raw, and TRUE_c. Referenced by build_dlx_uclid_compare(), build_dlx_uclid_impl(), build_dlx_uclid_spec(), build_dlx_uclid_superscalar(), build_double_instr(), and build_single_instr().

F uif (  char *  name, F  arg )

Return a UIF of given name, arg. Definition at line 842 of file node.c. References Fnil, Func_c, list(), new_node(), F::raw, and rs(). Referenced by build_dlx_uclid_impl(), build_dlx_uclid_spec(), build_dlx_uclid_superscalar(), build_double_instr(), and build_single_instr().

F uif2 (  char *  name, F  arg1, F  arg2 )

Return a UIF of given name, takes 2 args. Definition at line 779 of file node.c. References Fnil, Func_c, list(), new_node(), F::raw, and rs(). Referenced by build_dlx_uclid_impl(), build_dlx_uclid_spec(), build_dlx_uclid_superscalar(), build_double_instr(), build_fold_unfold_wrapper(), and build_single_instr().

F uif3 (  char *  name, F  arg1, F  arg2, F  arg3 )

Return a UIF of given name, takes 3 args. Definition at line 820 of file node.c. References Fnil, Func_c, list(), new_node(), F::raw, and rs(). Referenced by build_dlx_uclid_impl(), build_dlx_uclid_spec(), build_dlx_uclid_superscalar(), build_double_instr(), build_single_instr(), and uir3().

F uir3 (  char *  name, F  arg1, F  arg2, F  arg3 )

Return a relation of given name, takes 3 args. Definition at line 799 of file node.c. References sc(), and uif3(). Referenced by build_dlx_uclid_impl(), build_dlx_uclid_spec(), and build_dlx_uclid_superscalar().

F vector_lone (  Fv  x  )

F vexists (  Fv  A  )

F vforall (  Fv  A  )

---

Variable Documentation

F Fnil

AutomaticEnd************************************************************** Definition at line 30 of file node.c. Referenced by list(), uif(), uif2(), and uif3().

---