Unbounded Proof Using EBMC

Unbounded Proof with BDDs

We discuss how to perform unbounded safety verification of a circuit using the BDD engine in EBMC. We use an implementation of a controller for a ring buffer, given as ring_buffer.sv, as example.

The command to invoke the BDD engine is given below.

ebmc ring_buffer.sv --top ring_buffer --bdd 

Note that we added the --bdd switch to enable the BDD engine in EBMC. No bound is required for the BDD engine since it performs unbounded verification. There can be two possible outcomes when the BDD engine is used.

1. The fist outcome is that there exists a counterexample that refutes the property. When given the --trace command-line option, the tool returns a concrete counterexample trace that demonstrates the violation of the property.

2. The second outcome is that the property is proven by the BDD engine. In this case, the property holds for any bound.

The BDD engine is applicable to both safety and liveness properties. For further background, we recommend chapter 8 in the Model Checking book.

Unbounded Proof with k-induction

BDD-based reachability analysis is known to suffer scalability limits, which means that EBMC does not terminate or that it runs out of memory. As an alternative, unbounded safety verification of a circuit can be performed using the k-induction engine in EBMC. Inductive reasoning can scale to bigger circuits than BDD-based reasoning. Inductive reasoning is applicable to safety properties only.

We continue to use the ring buffer ring_buffer.sv.

ebmc ring_buffer.sv --top ring_buffer --k-induction 

Note that we added the --k-induction switch to enable the k-induction engine in EBMC. No bound is given, which means that EBMC will use 1-induction.

The k-induction engine first checks the base case. If the base case fails, the counterexample is reported to the user.

If the base case holds, then the tool checks the step case. There can be three possible outcomes when the k-induction engine is used.

1. The fist outcome is that there exists a counterexample to the base case. If so, the property is refuted and the tool return a concrete counterexample trace that demonstrates the violation of the property.

2. The second outcome is that the property is proven to be k-inductive. If so, the property holds for any bound.

3. The third outcome is that the base case holds but the step case fails. If so, k-induction is inconclusive. The property is neither proven nor refuted. The user may specify a higher bound with the --bound option to check if the property can be proven to be k-inductive with this higher value of k.

For further background on k-induction, and to learn how to strengthen properties to address the third outcome, we recommend section 10.2 in the Model Checking book.