-
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:
- undefined symbols
- multiple definition of symbols
- circular definition of symbols
- assignment to input variables
-
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:
- Creation of the boolean variables.
- Creation of the BDD representing the inertia of the system when
there are processes. In fact when a process is running the
other processes are stopped, and their state variables don't
change.
- Creation of the BDD representing what does not change in the
system, i.e. the set of invariance. These are introduced in the
model by the keyword "INVAR" or by the normal
assignments (i.e. "ASSIGN x : = y & z;"). These
states are not stored in the transition relation, they are
stored in an a doc variable.
- Creation of the BDD representing the set of initial states.
- Creation of the BDD representing the transition relation.
Various ways of representing the transition relation are offered
the users.
- Monolithic: the monolithic transition relation is
computed.
- Conjunctive Partioned (Threshold): the transition
relation is stored as an implicitly conjoined list of
transition relation. This kind of partitioning can be
used only if the model considered is a synchronous one.
- Conjunctive Partioned IWLS95: as the above, but the
heuristic proposed in [1] is used to order partition clusters.
- Computes the fairness constraints. I.e. each fairness constraint
(which can be a CTL formula) is evaluated and the resulting BDD
is stored in the list fairness_constraints_bdd to be
then used in the model checking phase.
[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/01/30 15h:04