go_bmc - Initializes the system for the BMC verification.


go_bmc [-h] | [-f]

This command initializes the system for verification. It is equivalent to the command sequence read_model, flatten_hierarchy, encode_variables, build_boolean_model, bmc_setup. If some commands have already been executed, then only the remaining ones will be invoked.

Command options:

-f
Forces the model construction.

-h
Prints the command usage.


Last updated on 2012/11/18 14h:37