Unbounded Proof Using EBMC

Unbounded Proof with k-induction

We discuss how to perform unbounded safety verification of a circuit using the k-induction 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 k-induction engine is given below.

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.

Unbounded Proof with BDDs

We discuss how to perform unbounded safety verification of a circuit using the BDD engine in EBMC. We use the ring buffer ring_buffer.sv. The BDD engine in EBMC uses the Mini-BDD package.

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. 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.