With the ever-increasing complexity of hardware (HW) and SoC-based designs for mobile platforms, demand for scalable formal verification tools in the semi-conductor industry is always growing. The scalability of hardware model checking tools depends on three key factors: the design representation, the verification engine, and the proof engine. Conventional SAT-based bit-level formal property checking tools for hardware, as shown in the top flow of Figure 1, converts the design into a netlist, typically represented using And-Inverter graphs (AIGs). These tools can not exploit the word-level structure of designs given at the register transfer level (RTL). Over the last decade, formal hardware verification tools have therefore implemented a word-level representation of the transition relation, typically represented using BLIF format or tool-specific word-level formats, thus enabling the use of modern solvers for Satisfiability Modulo Theories (SMT). However, the performance of word-level symbolic execution engine is determined by the level of abstraction of the symbolic expressions and the power of the rewrite engines used by the SMT solvers. State-of-the-art bitlevel and word-level formal verification tools scale up to block level or small IP level circuits. These tools generally do not scale to large IPs, subsystems, or full SoC designs. Figure 1 presents a conventional bit-level hardware/software coSAT/ SMT
C (Reference)
Transition System CFG
Unwind Transition System Unwind loops
Formula Formula verification flow in the presence of a firmware. The main limitation of this flow is that the hardware (typically represented in Verilog RTL) and software (in C) synthesis flow meet only at the level of the solver. The high-level design structure of C and RTL is already lost at this level and thus there is very limited opportunity for scalable reasoning.
In this thesis, we propose a novel approach for verifying hardware circuits, at the
heart of which is a verifier for software. To this end, we translate hardware design,
typically given in Verilog at register-transfer level into an equivalent word-level
ANSI-C program, which we call software netlist, following synthesis semantics.
The property of interest is instrumented into the C program as an assertion. This
change in the design representation at the front-end allows us to leverage the
precision and scalability of state-of-the-art software analyzers in the back-end. In
particular, we apply well known software verification techniques such as
pathbased symbolic execution [
Contributions We make the following contributions in this research.
1. We present a high-level software representation for hardware circuits
expressed at register-transfer level. To this end, we develop a tool v2c to
automatically synthesize a software netlist model in C from hardware circuits
expressed in Verilog RTL following synthesis semantics. The work is
published in TACAS 2016 [
Research Methodology
The primary motivation for the transition from bit level to word level is to gain
scalability [
v2c Verilog Translator (HW)
C (optional Software) parse
C parse
Common
IR
Software Verification Algorithms
SAT
SMT
Solver engine
This preserves the word-level structure and the control-flow information of the
input RTL design. The translation details are presented in [
Figure 2 gives an overview of the tool architecture we propose. The input Verilog design is synthesized to a software netlist model in C using v2c. This high-level representation allow us to verify hardware IP’s using different state-of-the-art software verifiers. Note that the hardware design may be augmented with software, such as firmware or high-level models of surrounding IPs given in C. The proposed tool architecture also provides an unified framework to uncover hardware/software design bugs much early in the verification process. To the best of our knowledge, this is the first attempt to perform hardware verification and hardware/software co-verification using software analyzers.
Our evaluation using different program analysis techniques show that these
techniques are competitive to the contemporary hardware verifiers based on netlist.
For example, state-of-the-art abstract interpretation tools like Astre´e was never
optimised for precise hardware analysis, and we thus believe that there is scope
for new tools that implement abstract interpretation using abstract domains
developed specifically for this task, e.g., by applying abstract conflict driven clause
learning (ACDCL) [
On the other hand, ACDCL uses decision and learning to generate the proof using simple interval domain. The analysis associates an interval with each location n1 n3: c = [0,0] n4: x = [-1,-1]
n2: ?
n5: z = [
Conflict Learn: (c != 0)
C. ACFG for P’
n6: ?
and variable. Assuming bool : c = [0; 1], ACDCL performs backward
propagation starting from n6 by computing the weakest precondition for every statement
in P and immediately infers that (n4 : x = ?), thus proving safety as shown
in red color in figure 3A. Now, let us consider program P0 in Figure 3B.
Assuming char : c, ACDCL performs both forward and backward propagations
(shown in red color in Figure 3B). The analysis then perform sequence of
decisions starting with c = [0; 255] and reaches a conflict when the decision is
(n1 : c == [0; 0]) which is connected to (n6 : ?) and suffices to prove safety.
The deductions made during fixed point iteration are represented by abstract
conflict graph shown in Figure 3C. Similar to conflict analysis phase in SAT solvers,
ACDCL learn (n1 : c = [1; 255]), that is all error traces must satisfy (c 6= 0) at n1.
The analysis backtracks discarding all assumptions. Interval analysis is run with
the learnt constraint and can prove safety. Thus, decisions and clause learning
are used to avoid case based reasoning. The advantage of ACDCL over
propositional SAT solver is that the decision heuristics in ACDCL can exploit the
program structure by making decisions on interesting program variables (for
example variables in conditional branches or loop variables). Experimental evidence
shows that this leads to significantly less number of decisions and less number
of conflicts compared to the propositional solver. Compared to classical abstract
interpretation based tools, ACDCL automatically performs program and property
driven trace partitioning using decision and clause learning to generate proofs
using simpler domain – thus, it is more precise than classical abstract interpretation.
Static program analysis based on abstract interpretation [
return unknown else assign result=deduce (P) if result == UNKNOWN then if is gamma complete() then
return unsafe else
continue else do if : conflict analysis() then
return safe assign result=deduce (P) while result ==? Moreover, ACDCL implicitly perform program and property driven trace partitioning to increase the precision of the analysis. We observe that the abstract domains necessary for hardware property checking are – booleans, constants, interval, equality and octagons domains.
Algorithm 1 presents an overview of the ACDCL algorithm. Given a program P
with properties specified as assert(c), ACDCL terminate with safe if there exist
no counterexample trace violating the assertion or unsafe otherwise. The
procedure deduce(P) is similar to BCP step in SAT solvers where it computes least
fix-point with strongest post-condition using forward analysis. If the result of
deduce(P) is BOTTOM (?), the algorithm terminates with safe. Else, the gamma
completeness check [