Getting started with the nuXmv C API

This short guide provides an overview of how to use the nuXmv C API to programmatically build and verify formal models.

1. Environment Initialization

Interaction with the API begins with the creation of a nuxmv_env object, which serves as the primary container for all model data and internal state.

• Create: Use nuxmv_create_env() to initialize the system.
• Error Handling: If an operation fails, nuxmv_env_get_last_error_message() can be used to retrieve the diagnostic message.
• Cleanup: Call nuxmv_destroy_env() at the end of the program to free all resources.

2. Basic Types and Constants

Before defining logic, you must establish the expression types and symbols that will populate your expressions.

3. Creating a Functional Module

A model is built using nuxmv_module objects.

Parameters and Variables

Modules can accept parameters, such as a carry_in bit.

1. Add Parameters: Use nuxmv_module_add_params() to define inputs for the module.
2. State Variables: Use nuxmv_module_add_state_var() to declare internal state, such as the bit's current value.

Assignments and Transition Logic

Logic can be defined through direct assignments or transition relations:

• Initial State: Use nuxmv_module_add_init() to set the starting condition (e.g., value = FALSE).
• Transitions: Use nuxmv_module_add_trans() to define how variables change in the next step using operators like NUXMV_OP_XOR and NUXMV_OP_NEXT_FUNCTION.
• Definitions: Use nuxmv_module_add_define() for combinational logic like carry_out := value & carry_in.

4. Building the Model Hierarchy

Complex systems are constructed by instantiating submodules within a main module.

• Submodule Instantiation: nuxmv_module_add_submodule() creates an instance of a module (e.g., bit0) and maps its parameters to local expressions.
• Scoped Symbols: To access a variable within a submodule, use nuxmv_make_scoped_symbol(), which allows referencing paths like bit0.carry_out.

5. Verification and Model Checking

Once the hierarchy is complete, the model must be compiled and checked against properties.

1. Flattening the Model: Call nuxmv_create_model() to instantiate the module hierarchy into a flattened structure ready for formal analysis.
2. Defining Properties: Properties are created using nuxmv_make_property(), supporting types like LTLSPEC (Linear Temporal Logic) or INVARSPEC (Invariants).
3. Checking: nuxmv_model_check_property() runs the verification engine using provided options, such as the specific algorithm or maximum verification bound.

6. Analyzing Results and Traces

The verification returns a nuxmv_result, which contains a status code.

• Result Codes: The check may return NUXMV_RESULT_TRUE, NUXMV_RESULT_FALSE, or NUXMV_RESULT_UNKNOWN.
• Counterexamples: If a property is false, use nuxmv_result_get_trace() to extract the execution path leading to the violation.
• Inspecting Steps: You can iterate through trace steps via nuxmv_trace_get_step_num() and inspect specific variable values at each state with nuxmv_trace_get_step_state().

Example: a simple hardware-like counter

The example_counter.c file demonstrates how to build and verify a hardware-like counter model using the nuXmv C API.

1. Initializing the Environment

Every nuXmv application starts by creating an environment object, which manages the lifecycle of all subsequent objects.

nuxmv_env env = nuxmv_create_env();

2. Defining Basic Types and Constants

Before building logic, you must define the data types (like Booleans) and the specific values (TRUE/FALSE) the model will use.

nuxmv_expr_type bool_type = nuxmv_make_boolean_type(env);
nuxmv_symbol false_sym = nuxmv_make_symbol(env, "FALSE");
nuxmv_symbol true_sym = nuxmv_make_symbol(env, "TRUE");
nuxmv_expr false_expr = nuxmv_make_value(env, false_sym, bool_type);
nuxmv_expr true_expr = nuxmv_make_value(env, true_sym, bool_type);

3. Creating the counter_cell Module

The example defines a reusable counter_cell. It adds a parameter (carry_in) and a state variable (value).

nuxmv_module counter_cell = nuxmv_create_module(env, "counter_cell");

// Parameter: carry_in
nuxmv_symbol carry_in_sym = nuxmv_make_symbol(env, "carry_in");
nuxmv_expr carry_in_expr = nuxmv_make_identifier(env, carry_in_sym, bool_type);
nuxmv_module_add_params(env, counter_cell, &carry_in_expr, 1);

// State variable: value
nuxmv_symbol value_sym = nuxmv_make_symbol(env, "value");  
nuxmv_var_decl value_decl = {value_sym, nuxmv_make_simple_var_type(env, bool_type)};
nuxmv_module_add_state_var(env, counter_cell, value_decl);

4. Defining State Transitions

The logic for how value changes is defined using initial conditions and transition relations. next(value) is represented using the NUXMV_OP_NEXT_FUNCTION operator.

// init(value) := FALSE
nuxmv_expr eq_init \= nuxmv_make_bin_op(env, NUXMV_OP_EQ, value_id, false_expr);
nuxmv_module_add_init(env, counter_cell, eq_init);

// next(value) := value xor carry_in
nuxmv_expr lhs_next \= nuxmv_make_un_op(env, NUXMV_OP_NEXT_FUNCTION, value_id);
nuxmv_expr rhs_next \= nuxmv_make_bin_op(env, NUXMV_OP_XOR, value_id, carry_in_expr);
nuxmv_expr eq_trans \= nuxmv_make_bin_op(env, NUXMV_OP_EQ, lhs_next, rhs_next);
nuxmv_module_add_trans(env, counter_cell, eq_trans);

5. Instantiating Submodules in main

The main module connects multiple counter_cell instances. It uses scoped symbols to access the carry_out of one bit and pass it as a parameter to the next.

nuxmv_module main_module = nuxmv_create_module(env, "main");

// bit0 : counter_cell(TRUE)  
nuxmv_module_add_submodule(env, main_module, "bit0", counter_cell, &true_expr, 1);

// bit1 : counter_cell(bit0.carry_out)  
nuxmv_symbol b0_co_symb = nuxmv_make_scoped_symbol(env, "carry_out", bit0_symb);  
nuxmv_expr b0_co_id = nuxmv_make_identifier(env, b0_co_symb, bool_type);  
nuxmv_module_add_submodule(env, main_module, "bit1", counter_cell, &b0_co_id, 1);

6. Adding Properties and Model Checking

After defining the hierarchy, an LTL property is added. The model is then instantiated and checked using specified algorithms.

// Property: G F bit2.carry_out
nuxmv_expr f_expr = nuxmv_make_un_op(env, NUXMV_OP_FINALLY, bit2_carry_out);
nuxmv_expr gf_expr = nuxmv_make_un_op(env, NUXMV_OP_GLOBALLY, f_expr);
nuxmv_property prop = nuxmv_make_property(env, "carry_out_eventually", NUXMV_PROPERTY_LTLSPEC, gf_expr);
nuxmv_module_add_property(env, main_module, prop);

// Create model and check
nuxmv_model model = nuxmv_create_model(env, main_module, NULL, 0);
nuxmv_result result = nuxmv_model_check_property(env, model, prop, myopts, num_opts);

7. Inspecting Counterexamples

If a property is false, you can extract a trace to see the step-by-step state changes that led to the violation.

if (nuxmv_result_get_code(env, result) == NUXMV_RESULT_FALSE) {
    nuxmv_trace trace = nuxmv_result_get_trace(env, result);
    int steps = nuxmv_trace_get_step_num(env, trace);
    for (int i = 0; i < steps; ++i) {
        nuxmv_trace_value v = nuxmv_trace_get_step_state(env, trace, i, var_idx);
        // Print variable and its value...
    }
}