Prepare the following nuXmv batch script, commands.cmd
set verbose_level 2; set pp_list cpp; set counter_examples 0; set dynamic_reorder 1;
set on_failure_script_quits;
set reorder_method sift; set enable_sexp2bdd_caching 0; set bdd_static_order_heuristics basic;
set cone_of_influence; set use_coi_size_sorting 1;
read_model -i model.smv;
flatten_hierarchy; encode_variables; build_flat_model;
build_model -f; check_invar -s forward;
show_property -o property.rpt;
time; quit
And we can launch a verification run by using nuXmv -int commands.cmd
The current implementation prints a netlist and a library of units in the SMV format to stdout.
Since this language does not support parametrized instantiation, we generate one implementation for each parametrization of a unit, e.g., it generates one implementation for 2-output, 3-output, and 4-output eager fork.
This PR introduces the export-smv tool, which converts a handshake-level IR to the nuXmv input format,
.smv(https://nuxmv.fbk.eu/).This allows us to run model-checking on an abstracted dataflow circuit model.
Example use:
Prepare the following nuXmv batch script,
commands.cmdAnd we can launch a verification run by using
nuXmv -int commands.cmdThe current implementation prints a netlist and a library of units in the SMV format to stdout.
Since this language does not support parametrized instantiation, we generate one implementation for each parametrization of a unit, e.g., it generates one implementation for 2-output, 3-output, and 4-output eager fork.