compile.h
External header file
compileInt.h
Internal header file
compileBEval.c
compileCheck.c
Performs semantic checks on the model.
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.
compileStruct.c
Structure used to store compilation results.
compileUtil.c
Routines for model computation.
compileWrite.c
Creation of an SMV file containing the flattened or booleanized model.

compile.h

External header file

By: Marco Roveri, Emanuele Olivetti

()
The name of the standard layer dedicated to model symbols

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

Compile_expr2bexpr()
Converts a scalar expression into a boolean expression.
Compile_detexpr2bexpr()
Converts a scalar expression into a boolean expression.
Compile_cleanup_booleanizer_cache_about()
Cleans those hashed entries that are about a symbol that is being removed
expr2bexpr_shift_left()
Creates the encoding of the left-shifting circuit for words
expr2bexpr_shift_right()
Creates the encoding of the right-shifting circuit for words
expr2bexpr_get_shift_def_value()
Private service for shifting operations
expr2bexpr_shift()
High-level function for shifting operations
expr2bexpr_rotate()
High-level function for rotating words
expr2bexpr_recur_unary()
Applied unary operand to booleanize depending on the operand type. Operation is passed through 'op'. Operation can be a closure W->W
expr2bexpr_recur_binary()
Applied to binary operands to booleanize depending on the operands types. Operation is passed through 'op'. Operation can be a closure WxW->W or a predicate over words WxW->Bool
expr2bexpr_ite()
Creates an encoding for CASE node. If CASE evaluates to a word, a WORD encoding is created.
expr2bexpr_word_ite_aux()
Service of expr2bexpr_word_ite, that creates the word encoding
expr2bexpr_recur()
Converts a generic expression into a boolean expression.
scalar_atom2bexpr()
Converts an atomic expression into the corresponding (boolean) expression.

compileCheck.c

Performs semantic checks on the model.

By: Marco Roveri

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

Compile_CheckAssigns()
Semantic checks on assignments of the modele.
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.
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.
compile_check_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

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_init_cmd()
Initializes the commands provided by this package
Compile_quit()
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 information about the clustering. ** DEPRECATED in 2.4 **
CommandPrintFsmStats()
Prints out information about the fsm and clustering.
CommandIwls95PrintOption()
Prints the Iwls95 Options.
CommandGo()
Implements the go command
CommandGoBmc()
Implements the go_bmc command
CommandGetInternalStatus()
Implements the get_internal_status command
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()
creates the master scalar fsm if needed
compile_create_boolean_model()
Creates the master boolean fsm if needed. A new layer called DETERM_LAYER_NAME will be added if the bool fsm is created.

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.
()
Clears and frees (with entries) given hash
Formula_GetDependencies()
Computes dependencies of a given SMV expression
Formula_GetDependenciesByType()
Computes the dependencies of an SMV expression by type
Formulae_GetDependencies()
Compute the dependencies of two set of formulae
ComputeCOI()
Computes the COI of a given set of variables, defined within the given symb_table
formulaGetDefinitionDependencies()
Compute the dependencies of an atom
formulaGetDependenciesRecur()
Recursive call to Formula_GetDependenciesByType
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
()
Cleans and frees the hash
Compile_FlattenHierarchy()
Traverse the module hierarchy, collect all required the informations and flatten the hierarchy.
Compile_ConstructHierarchy()
Traverses the module hierarchy and extracts the information needed to compile the automaton.
Compile_ProcessHierarchy()
This function processes a hierarchy after collecting all its subparts.
Compile_FlattenSexp()
Builds the flattened version of an expression.
Compile_FlattenSexpExpandDefine()
Flattens an expression and expands defined symbols.
Flatten_GetDefinition()
Gets the flattened version of an atom.
Flatten_remove_symbol_info()
Resets the hashed information about the given symbol
error_bit_selection_assignment_not_supported()
Error message for unsupported feature
compileFlattenProcess()
Flatten a hierarchy of SMV processes.
compileFlattenSexpModel()
Creates association between variables and all the expressions the variables occur in.
CompileFlatten_expand_range()
Returns a range going from a to b
CompileFlatten_normalise_value_list()
Takes a list of values and returns the same list being normalised
CompileFlatten_resolve_name()
Takes an expression representing an identifier and recursively evaluates it.
CompileFlatten_resolve_number()
Resolves the given symbol to be a number
CompileFlatten_init_flattener()
Inits the flattener module
CompileFlatten_quit_flattener()
Quits the flattener module
compile_instantiate_var()
Instantiates the given variable.
compile_instantiate_vars()
Recursively applies compile_instantiate_var.
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.
compile_instantiate()
Instantiates all in the body of a module.
compile_instantiate_by_name()
Starts the flattening from a given point in the module hierarchy.
compileFlattenSexpRecur()
Recursive function for flattenig a sexp.
compileFlattenProcessRecur()
Recursive definition of compileFlattenProcess
compileFlattenSexpModelAux()
compileFlattenSexpModelRecur()
compileFlattenConstantSexpCheck()
Called when a constant has been found in INVAR, INIT or TRANS
create_process_symbolic_variables()
Creates the internal process selector variable, within the given layer
type_to_string()
required
compile_flatten_resolve_name_recur()
Performs the recursive step of CompileFlatten_resolve_name. Returns TYPE_ERROR if not resolvable name
compile_flatten_eval_number()
Simple evaluator for positive and negative constant numbers
flatten_declare_constants_within_list()
Traverses the list of values, and declare all constants (leaves) it finds

compileStruct.c

Structure used to store compilation results.

By: Marco Roveri

Structure used to store compilation results.

Compile_get_global_predicate_normaliser()
Returns a global predicate normaliser
Compile_get_global_fsm_builder()
Returns the global fsm builder
cmp_struct_init()
Initializes the cmp structure

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.
()
Private macros for the sake of readability of the function Compile_pop_global
Compile_pop_distrib_ops()
Simplifies the given property by exploiting the distributivity of G, AG and H over AND, and distributivity of F, AF and O over OR
Compile_make_sorted_vars_list_from_order()
This function creates a new list of variables that will contain the same symbols into 'vars', but ordered wrt to 'vars_order' content
Compile_check_if_model_was_built()
Checks if bdd model has been constructed
Compile_check_if_bool_model_was_built()
Checks if boolean model has been constructed
Compile_check_if_flat_model_was_built()
Checks if flat model has been constructed
Compile_check_if_encoding_was_built()
Checks if the variables enconding has been constructed
Compile_check_if_flattening_was_built()
Checks if the flattening has been carried out

compileWrite.c

Creation of an SMV file containing the flattened or booleanized model.

By: Marco Roveri, Roberto Cavada

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

Compile_WriteFlattenFsm()
Prints the flatten version of FSM of an SMV model.
Compile_WriteFlattenSpecs()
Prints the flatten specifications.
Compile_WriteBoolFsm()
Prints the boolean FSM of an SMV model.
Compile_WriteBoolSpecs()
Prints the boolean specifications of an SMV model.
write_flatten_define()
Writes DEFINE declarations 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_vars()
Writes VAR and IVAR declarations in SMV format on a file.
compile_write_flatten_bool_vars()
Writes boolean VAR and IVAR declarations in SMV format on a file. Non boolean vars are dumped as defines for the sake of readability of conterexamples.
compile_write_flatten_expr_split()
Writes flattened expression in SMV format on a file.
compile_write_flatten_expr()
Writes flattened expression in SMV format on a file.
compile_write_flatten_psl()
Writes PSL properties as they are.
compile_write_flatten_bfexpr()
Writes flattened expression in SMV format on a file.
compile_write_flatten_expr_pair()
Writes flattened expression pairs in SMV format on a file.
compile_write_constants()
Writes the set of non-numeric constants as CONSTANTS statement

Last updated on 2009/03/04 12h:51