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.
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.
The second outcome is that the property is proven to be k-inductive. If so, the property holds for any bound.
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.
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.
The second outcome is that the property is proven by the BDD engine. In this case, the property holds for any bound.