Formal verification is a vast and interesting topic. One of the biggest issues is tools to support SVA. I recently found hw-cbmc, an open source tool to run SVA or SMV on Verilog. This is a deep dive into hw-cbmc.
Hello World Link to heading
This is a summary of commands to build hw-cbmc. This is based on COMPILING.md and Dockerfile.
apt-get install g++ gcc flex bison make git curl patch
git clone https://github.com/diffblue/hw-cbmc
git submodule init; git submodule update
make -C lib/cbmc/src minisat2-download
make -C src
To run hello world, ebmc is called with --top and --bound with 3.
ebmc main.sv --top main --bound 3
module main(input clk, x, y);
reg [1:0] cnt1;
reg z;
initial cnt1=0;
initial z=0;
always @(posedge clk) cnt1=cnt1+1;
always @(posedge clk)
casex (cnt1)
2'b00:;
2'b01:;
2'b1?: z=1;
endcase
p1: assert property (@(posedge clk) (z==0));
endmodule
Engines Link to heading
I asked copilot to explain the methods used in ebmc and I got the following list. Technically, completeness threshold is not an engine. It is a metric that can be used with heuristics to choose an engine, if not provided on the command line.
- __Bounded Model Checking (BMC)__:
- BMC checks properties within a fixed bound (e.g., a number of steps or timeframes).
- It uses SAT or SMT solvers to find counterexamples within the bound.
- Suitable for finding bugs quickly but does not guarantee correctness beyond the bound.
- __1-Induction__:
- A proof-based method that attempts to prove properties by induction.
- It checks the base case and the inductive step to ensure the property holds for all states.
- Useful for proving correctness but may fail if the inductive step cannot be established.
- __Completeness Threshold__:
- Evaluates properties based on a completeness threshold, which determines the maximum depth or complexity of the system.
- It is a heuristic approach that tries to simplify the verification process.
- May not always succeed in proving or disproving properties.
- __BDD Engine__:
- Uses Binary Decision Diagrams (BDDs) to represent and manipulate boolean functions.
- Efficient for certain types of properties but can suffer from memory issues for large systems.
- __IC3__:
- Incremental Construction of Inductive Clauses (IC3) is a SAT-based method for proving safety properties.
- It incrementally builds inductive invariants to prove properties.
- Effective for safety properties but not applicable to liveness properties.
- __Word-Level BMC__:
- Operates at a higher abstraction level, using word-level constructs (e.g., integers, arrays) directly.
- Typically employs SMT (Satisfiability Modulo Theories) solvers, which can handle complex data types and arithmetic operations.
- Suitable for systems with high-level constructs, as it avoids the overhead of bit-level encoding.
- __Bit-Level BMC__:
- Works at the lowest level of abstraction, representing everything as individual bits.
- Uses SAT (Boolean Satisfiability) solvers, which are optimized for boolean logic.
- Ideal for hardware verification and systems where bit-level precision is critical.
Deep Dive into ebmc Link to heading
Starting with src/ebmc/main.cpp with ebmc where it calls ebmc_parse_options.
int main(int argc, const char **argv)
{
ebmc_parse_optionst ebmc_parse_options(argc, argv);
return ebmc_parse_options.main();
}
Then doit is called from src/ebmc/ebmc_parse_options.cpp to register languages.
int ebmc_parse_optionst::doit()
{
if(cmdline.isset("verbosity"))
ui_message_handler.set_verbosity(
unsafe_string2unsigned(cmdline.get_value("verbosity")));
else
ui_message_handler.set_verbosity(messaget::M_STATUS); // default
if(config.set(cmdline))
{
usage_error();
return CPROVER_EXIT_USAGE_ERROR;
}
register_languages();
Then doit creates the transition system from the Verilog design.
auto transition_system = get_transition_system(cmdline, ui_message_handler);
The next step is extracting the assertion and related properties by calling from_command_line and property_checker.
auto properties = ebmc_propertiest::from_command_line(
cmdline, transition_system, ui_message_handler);
auto checker_result = property_checker(
cmdline, transition_system, properties, ui_message_handler);
The next step is calling the engine from src/ebmc/property_checker.cpp. The engine is picked up from command line options. If none is given, it goes to engine_heuristic.
if(cmdline.isset("bdd") || cmdline.isset("show-bdds"))
{
return bdd_engine(
cmdline, transition_system, properties, message_handler);
}
else if(cmdline.isset("aig") || cmdline.isset("dimacs"))
{
// bit-level BMC
return bit_level_bmc(
cmdline, transition_system, properties, message_handler);
}
else if(cmdline.isset("k-induction"))
{
return k_induction(
cmdline, transition_system, properties, message_handler);
}
else if(cmdline.isset("ic3"))
{
#ifdef _WIN32
throw ebmc_errort() << "No support for IC3 on Windows";
#else
return ic3_engine(
cmdline, transition_system, properties, message_handler);
#endif
}
else if(cmdline.isset("bound"))
{
// word-level BMC
return word_level_bmc(
cmdline, transition_system, properties, message_handler);
}
else
{
// heuristic engine selection
return engine_heuristic(
cmdline, transition_system, properties, message_handler);
}
Transition System Link to heading
Circling back to get_transition_system in src/ebmc/transition_system.cpp, where Verilog (or VHDL) files are parsed and represented in the form of a transition system.
int get_transition_system(
const cmdlinet &cmdline,
message_handlert &message_handler,
transition_systemt &transition_system)
{
messaget message(message_handler);
if(cmdline.isset("preprocess"))
return preprocess(cmdline, message_handler);
//
// parsing
//
language_filest language_files;
if(parse(cmdline, language_files, message_handler))
return 1;
if(cmdline.isset("show-parse"))
{
language_files.show_parse(std::cout, message_handler);
return 0;
}
Properties Link to heading
Once we have the transition system parsed and built, it needs to extract the assertions and properties. from_transition_system, src/ebmc/ebmc_properties.cpp, is called to extract properties.
auto properties =
from_transition_system(transition_system, message_handler);
std::string value_as_string = from_expr(ns, symbol.name, symbol.value);
message.debug() << "Property: " << value_as_string << messaget::eom;
properties.properties.push_back(propertyt());
properties.properties.back().number = properties.properties.size() - 1;
properties.properties.back().identifier = symbol.name;
properties.properties.back().name = symbol.display_name();
properties.properties.back().original_expr = symbol.value;
properties.properties.back().location = symbol.location;
properties.properties.back().mode = symbol.mode;
properties.properties.back().description =
id2string(symbol.location.get_comment());