compile.h
External header file
compileInt.h
Internal header file
compileBEval.c
compileCheck.c
Performs semantic checks on the model.
compileCheckWff.c
Checks for potential formula errors.
compileCmd.c
Shell interface for the compile package.
compileCone.c
Computes the cone of influence of the model variables.
compileFlatten.c
Flattening of the model.
compileFsmMgr.c
High level object that can contruct FSMs
compileStruct.c
Structure used to store compilation results.
compileUtil.c
Routines for model computation.
compileWriteBool.c
Creation of an SMV file containing the flattened booleanized model.
compileWriteFlat.c
Creation of an SMV file containing the flattened model.

compile.h

External header file

By: Marco Roveri, Emanuele Olivetti

()
The symbolic name of the input process selector variable.

compileInt.h

Internal header file

By: Marco Roveri, Roberto Cavada


compileBEval.c

By: Alessandro Cimatti and Marco Roveri

Conversion from scalar expressions to boolean expressions.

See Alsooptional

expr2bexpr()
Converts a scalar expression into a boolean expression.
detexpr2bexpr()
Converts a scalar expression into a boolean expression.
expr2bexpr_recur()
Converts a generic expression into a boolean expression.
scalar_atom2bexpr()
Converts an atomic expression into the corresponding (boolean) expression.
add2bexpr()
Converts a ADD into the corresponding (boolean) expression.
add2bexpr_recur()
Converts a ADD into the corresponding (boolean) expression.
mk_new_var()
Create a new (boolean) variable.

compileCheck.c

Performs semantic checks on the model.

By: Marco Roveri

The routines to perform some the semantic checks.
The performed checks are:

Compile_CheckProgram()
Semantic checks on the model.
Compile_get_expression_dependencies()
Gets list of variables in the expression
compileCheckForInputVars()
Checks expressions for illegal occurrences of input vars
init_check_program()
Initializes the data structure to perform semantic checks.
init_check_program_recur()
Recursive step of init_check_program
check_circ()
Checks for circular definitions.
check_circular_assign()
Performs circular assignment checking
check_assign()
Checks for multiple or circular assignments.
check_assign_both()
Given a variable, it checks if there are multiple assignments to it.
print_io_atom_stack_assign()
compileCheckAssignForInputVars()
Checks flattened assign statement for input variables
compileExpressionHasNextInputs()
Checks expression for input variables in next statements
compileCheckTransForInputVars()
Checks flattened trans statement for input variables
compileCheckInvarForInputVars()
Checks flattened invar statement for input variables
compileCheckInitForInputVars()
Checks flattened init statement for input variables

compileCheckWff.c

Checks for potential formula errors.

By: Andrea Morichetti and Marco Roveri

Routines to check for potential formula errors. A potential error may arise when arguments do not match the formula operator domain, e.g. a AND b, where a or b are not booleans.

Compile_CheckWff()
Checking formula potential errors and results.
check_wff()
Checking formula potential errors and results. It is a front end of Compile_CheckWff
parsecheckwffcmd()
Parses string looking for a simple/ctl/ltl/compute expression.
wff_is_boolean()
Checks if an atom is boolean or symbolic.
wff_is_numeric()
Checks if an atom is numeric or symbolic.
check_wff_recur()
Performs the recursive step of the Compile_CheckWff function.
check_definition()
Returns the definition of a symbol.
Compile_is_input_variable_formula()
Checks whether given formula contains input variables.

compileCmd.c

Shell interface for the compile package.

By: Marco Roveri

This file contains the interface of the compile package with the interactive shell.

See AlsocmdCmd.c

Compile_Init()
Initializes the compile package.
Compile_End()
Shut down the compile package
CommandProcessModel()
Performs the batch steps and then returns control to the interactive shell.
CommandFlattenHierarchy()
Flattens the hierarchy of modules
CommandShowVars()
Shows model's symbolic variables and their values
CommandEncodeVariables()
Builds the BDD variables necessary to compile the model into BDD.
CommandBuildModel()
Compiles the flattened hierarchy into BDD
CommandBuildFlatModel()
Compiles the flattened hierarchy into SEXP
CommandBuildBooleanModel()
Compiles the flattened hierarchy into boolean SEXP
CommandWriteOrder()
Writes variable order to file.
CommandCPPrintClusterInfo()
Prints out the information of the clustering.
CommandIwls95PrintOption()
Prints the Iwls95 Options.
CommandGo()
Implements the go command
CommandGoBmc()
Implements the go_bmc command
CommandGetInternalStatus()
Implements the get_internal_status command
CommandCheckWff()
Checks formulas potential errors.
CommandWriteModelFlat()
Writes the currently loaded SMV model in the specified file, after having flattened it
CommandWriteModelFlatBool()
Writes a flat and boolean model of a given SMV file
compile_create_flat_model()
Initializes the fsm builder if needed, and creates the master scalar fsm

compileCone.c

Computes the cone of influence of the model variables.

By: Marco Roveri and Marco Pistore

This file contains the functions needed for computing the cone of influence (COI) of a given formula. The COI of all the variables in the model is pre-computed ancd cached the first time a cone of influence is required (function initCoi. Functions are also provided that compute the dependency variables for a formula, namely those variables that appear in the formula or in one of the definitions the formula depends on.

()
Indicates that the dependency computation is ongoing.
()
Indicates that the COI computation should be verbose.
Formula_GetDependencies()
Computes dependencies of a given SMV expression
Formulae_GetDependencies()
Compute the dependencies of two set of formulae
ComputeCOI()
Compute the COI of a given set of variables
formulaGetDefinitionDependencies()
Compute the dependencies of an atom
formulaGetDependenciesRecur()
Recursive call to Formula_GetDependencies.
coiInit()
Pre-compute the COI of the variables

compileFlatten.c

Flattening of the model.

By: Marco Roveri

Performs the flattening of the model. We start from the module main and we recursively instantiate all the modules or processes declared in it.
Consider the following example:

MODULE main
...
VAR
a : boolean;
b : foo;
...

MODULE foo
VAR
z : boolean;
ASSIGN
z := 1;
The flattening instantiate the module foo in the main module. You can refer to the variables "z" declared in the module foo after the flattening by using the dot notation b.z.

()
Body of define in evaluation
Compile_FlattenHierarchy()
Traverse the module hierarchy, extracts the informations and flatten the hierarchy.
Compile_FlattenTableau()
Traverse the module tableau, extracts the informations and flatten the tableau.
compileFlattenProcess()
Flatten a hierarchy of SMV processes.
Compile_FlattenSexp()
Builds the flattened version of an expression.
Compile_FlattenSexpExpandDefine()
Flattens an expression and expands defined symbols.
compileFlattenSexpModel()
required
CompileFlatten_expand_range()
Returns a range going from a to b
CompileFlatten_resolve_name()
Takes an expression representing an identifier and recursively evaluates it.
CompileFlatten_quit_flattener()
Quits the flattener module
instantiate_var()
Instantiates the given variable.
instantiate_vars()
Recursively applies instantiate_var.
Flatten_GetDefinition()
Gets the flattened version of an atom.
put_in_context()
Put a variable in the current "context"
make_params()
Builds the parameters of a module from the list of formal parameters of the module itself.
instantiate()
Instantiates all in the body of a module.
instantiate_by_name()
Starts the flattening from a given point in the module hierarchy.
compileFlattenHierarchy()
Traverses the module hierarchy and extracts the information needed to compile the automaton.
Flatten_FlattenSexpRecur()
Recursive function for flattenig a sexp.
compileFlattenProcessRecur()
Recursive definition of Compute_FlattenProcess
make_atom_set()
Builds the atom set of the given range
compileFlattenSexpModelAux()
required
compileFlattenSexpModelRecur()
required
compileFlattenConstantSexpCheck()
Called when a constant has been found in INVAR, INIT or TRANS
create_process_symbolic_variables()
Creates the internal process selector variable.
mk_and()
required
mk_true()
required
mk_false()
required
type_to_string()
required
compile_flatten_resolve_name_recur()
Performs the recursive step of CompileFlatten_resolve_name.

compileFsmMgr.c

High level object that can contruct FSMs

By: Roberto Cavada

Defines an high-level object that lives at top-level, that is used to help contruction of FSMs. It can control information that are not shared between lower levels, so it can handle with objects that have not the full knowledge of the whole system

FsmBuilder_create()
The constructor creates a BddEnc and self handles it
FsmBuilder_destroy()
Class FsmBuilder destructor
FsmBuilder_create_sexp_fsm()
Creates a new sexp fsm
FsmBuilder_create_bdd_fsm()
Creates a BddFsm instance from a given SexpFsm
fsm_builder_init()
fsm_builder_deinit()
fsm_builder_clusterize_expr()
Converts an expression into a list of clusters. This list can be used to create a BddFsm
fsm_builder_clusterize_expr_aux()
Auxiliary function to recursively traverse the given expression, clusterizing each node as bdd. If called from outside, parameter is_inside_and is false.
fsm_builder_justice_sexp_to_bdd()
Converts a list of expressions into a list of bdds, wrapped inside a justice list object
fsm_builder_compassion_sexp_to_bdd()
Converts a list of couple of expressions into a list of couple of bdds, wrapped inside a compassion list object

compileStruct.c

Structure used to store compilation results.

By: Marco Roveri

Structure used to store compilation results.


compileUtil.c

Routines for model computation.

By: Marco Roveri

This file contains the code for the compilation of the flattened hierarchy into BDD:

[1] R. K. Ranjan and A. Aziz and B. Plessier and C. Pixley and R. K. Brayton, "Efficient BDD Algorithms for FSM Synthesis and Verification, IEEE/ACM Proceedings International Workshop on Logic Synthesis, Lake Tahoe (NV), May 1995.

sym_intern()
Builds an internal representation for a given string.
Compile_InitializeBuildModel()
Initializes the build model.

compileWriteBool.c

Creation of an SMV file containing the flattened booleanized model.

By: Marco Roveri

Creation of an SMV file containing the booleanized and flattened model, processes will be removed by explicitly introducing a process variable and modifying assignments to take care of inertia.

Compile_WriteFlattenBool()
Prints the flatten version of an SMV model.
write_flatten_vars()
Writes VAR declarations in SMV format on a file.
write_flatten_expr()
Writes flattened expression in SMV format on a file.
write_flatten_expr_pair()
Writes flattened expression pairs in SMV format on a file.
write_flatten_bfexpr()
Writes flattened expression in SMV format on a file.
compile_write_flatten_psl()
Writes PSL properties as they are.

compileWriteFlat.c

Creation of an SMV file containing the flattened model.

By: Marco Roveri

Creation of an SMV file containing the flattened model, processes will be removed by explicitly introducing a process variable and modifying assignments to take care of inertia.

Compile_WriteFlatten()
Prints the flatten version of an SMV model.
write_flatten_vars()
Writes VAR declarations in SMV format on a file.
write_process_selector_define()
Writes DEFINE declarations in SMV format on a file.
write_flatten_define()
Writes DEFINE declarations in SMV format on a file.
write_flatten_expr()
Writes flattened expression in SMV format on a file.
write_flatten_expr_pair()
Writes flattened expression pairs in SMV format on a file.
write_flatten_assign()
Writes flattened ASSIGN declarations in SMV format on a file.
print_assign()
Prints an assignement statement
compile_write_flatten_psl()
Writes PSL properties as they are.

Last updated on 2005/07/18 15h:57