End-to-End Formal using Abstractions to Maximize

Coverage
(Invited Tutorial)
Prashant Aggarwal Darrow Chu Vijay Kadamby Vigyan Singhal
Oski Technology Cadence Design Systems Cisco Oski Technology
Gurgaon, India San Jose, CA, USA San Jose, CA, USA Mountain View, CA, USA
prashant@[Link] darrow@[Link] vkadamby@[Link] vigyan@[Link]

Abstract—Model checking tools are gaining traction as a tional complexity problem. Most tools deploy sophisticated
practical formal verification solution for industrial designs. abstraction-refinement algorithms under the hood [5], [19].
However, the use of abstraction models is key to overcoming On top of that, formal users can deploy manually crafted
complexity barriers in applying these tools. Coverage has been a
useful metric to determine when simulation-based verification abstractions [4], [6], [7], [11], [13] to further reduce the
is complete. In this paper, we show how similar coverage complexity of the proofs. In this paper, we will take a complex
metrics can be used to determine the completeness of a formal design with a large state space, and show how the use of
verification setup. We also show how coverage can be used to abstraction models can help achieve end-to-end formal for this
determine effectiveness of different abstraction models are. This design.
methodology can be used to set formal verification goals, and
to measure the progress of the work, thereby placing formal
verification in a chip design schedule. We use a real-world
design with a large state space, and present quantitative coverage Coverage metrics are widely used in simulation-based veri-
metrics to illustrate the methodology, and its benefits for faster fication to improve the quality of the test suite and estimate the
run-time, faster discovery of bugs, and higher coverage. progress of the verification task [9], [18]. Coverage can help
identify important gaps in the stimuli provided to the design-
I. I NTRODUCTION
under-test, although it has a known limitation that coverage
During the last decade, formal verification tools have been does not evaluate the quality of the simulation checkers. The
increasingly more popular for the pre- and post-silicon verifi- same coverage metrics can be deployed for formal verification
cation of a diverse class of IC designs, varying from custom with the same limitation [16]. Besides identifying uninten-
processor designs to general-purpose ASICs. While multiple tional over-constraints in a formal environment, formal cover-
formal verification technologies are used in the industry (e.g. age can estimate the effectiveness of the abstraction techniques
model checking, theorem proving, C-vs-RTL sequential equiv- being deployed – for example, a set of abstraction techniques
alence checking), model checking tools account for most of the is useful, if it enables many more lines or expressions of code
usage, judging from the number of available commercial tools to be reachable in the same amount of CPU time.
as well as verification users in place. Furthermore, major EDA
vendors (Cadence, Mentor Graphics and Synopsys) as well as
a few startups (Averant, Jasper, OneSpin and Real Intent) offer In this paper, we use formal coverage metrics to quanti-
competitive solutions. In this paper, we will use the term model tatively demonstrate that suitable abstraction models achieve
checking synonymously with formal verification. convergence. We begin by introducing end-to-end formal
The extent to which an ASIC design tapeout schedule verification in Section II, and the components required to
depends on formal verification is greatly contingent upon the build such an environment. We mention the role of abstraction
scope of verification addressed by formal. Most often, formal techniques to solve end-to-end formal in Section III. Next,
is used as a supplement to simulation, to prove some specific in Section IV we discuss how coverage is used for formal
difficult-to-verify behavior, local embedded RTL assertions, verification, and introduce a coverage-driven flow for formal
or interface protocol checks between blocks. Less often is verification. In Section V, we introduce the design we have.
formal used for end-to-end verification to replace simulation, This design has a state space that is fairly large for a typical
so that formal verifies most or all functionality of a design model checker to handle, more than 1 million flops. The
and simulation is used only for higher chip-level or system- design is an integral part of a large real-world ASIC switch.
level verification. End-to-end formal usually requires almost Section VI describes some of the constraints and checkers
the entire logic in the design to be analyzed by the formal needed for formal verification, including the most important
tool, and poses significant complexity barriers. end-to-end data checker. In Section VII, we describe the
Formal verification tool developers as well as users have abstraction models deployed to overcome complexity barriers.
long used abstraction techniques to overcome the computa- We present the coverage results in Section VIII.
 of the cone-of-influence of the checks and constraints. For
end-to-end formal verification, the model checking engine
which is often the most effective is Bounded Model Checking
(BMC) [1]. Although BMC can only find counterexamples,
and not establish the full proof of any checks, the bounded
proofs are good enough if the bounds are greater than the
interesting corner-case behavior of the design, as judged by
the verification or the design engineer.
Two complexity problems can interfere with BMC reaching
Fig. 1. End-to-end verification setup
acceptable proof bounds:
• the size of the logic in the cone-of-influence, including
II. E ND - TO -E ND F ORMAL the number of flops as well as the combinational logic;
and
A. Checkers and Constraints
• the state space diameter of the design, especially in
Besides reading the design-under-test (DUT), a model presence of large counters, or sequentially deep logic.
checker requires a set of checkers and constraints as inputs. The use of abstraction techniques, discussed in the next
The checkers and constraints can be written as properties in section, is the best strategy to overcome these complexity
SystemVerilog Assertion language (SVA) [8]. However, often problems.
these checkers and constraints require supporting modeling
code written in synthesizable SystemVerilog. III. A BSTRACTION T ECHNIQUES
Checkers can vary widely in scope:
Abstraction techniques [3] are used to reduce the state space
• Local checkers, also known as assertions. These checkers
of the design, so that formal verification tools can solve a
verify local properties of the design, and belong to one computationally easier problem. An abstraction is considered
of the following: sound if does not reduce any design behavior, even if it adds to
– Embedded RTL assertions. These assertions are local the design behaviors. We will only consider sound abstractions
properties about the implementation details in the in this paper. Such abstractions can find proofs or failures
DUT, such as a state machine always stays one-hot faster. Every proof is guaranteed to be a proof on the original
encoded, or that a full FIFO is never written to. These design. Each failure can be debugged to determine if it is a true
assertions are typically written by the RTL designer, counterexample due to an RTL bug, or a false counterexample
and embedded in the RTL code [21]. due to an over-abstraction.
– Interface assertions. These assertions encode the Examples of various abstraction techniques include:
handshake protocol requirements for any of the in-
1) Cut-points. Any internal logic in the design can be
terfaces of a design. These requirements can vary
replaced by a cut-point, allowing that net to freely take
from a simple request-acknowledgement protocol to
a random value at any time [6], [12]. If a checker proves
a more complex ARM AMBA AXI [15] or DDR2
with such an abstraction, we can achieve significant
protocol [6].
reductions in run-time (of course, it also implies the
• End-to-end checkers (Fig. 1). These checkers primarily need for additional checkers, since the proven checker
use a significant modeling code to encode a reference is clearly independent of the excised logic).
model for the required behavior of the design, by relating 2) Counter abstraction. Many designs have deep counters,
the correctness of the output data path of a design, given for example, the initialization phase for DDR2 memory
the transactions on the input datapath. controllers last for hundreds of milliseconds, consuming
Bugs found through any of these checkers are useful. However, millions of clock cycles. Many useful checks can be
if formal is to be relied upon as a primary verification proved by abstracting the 2n -state graph of an n-bit
methodology for a design, simply verifying local checkers counter to a few states, e.g. 0, 1, at-least-one, at-least-
is not enough – a significant number of end-to-end checkers zero [14].
must be used to achieve adequate verification. Not surprisingly, 3) Symmetric datatypes. Certain systems [7], [13] allow
proving the end-to-end checkers is usually computationally the users to specify that certain data types in the design
much more complex than local checkers, although there may are symmetric, and the values of these types are used
be exceptions to this, and some local checkers may be difficult only in certain symmetric ways (e.g. only compared for
to prove too. equality, or used as indices for arrays). This allows the
system to reduce multiple symmetric proofs into a single
B. Complexity one.
The largest barrier to formal verification achieving the 4) Data independence. When data moves across a design,
desired results is the complexity barrier faced by the tools. and the design does not use the data contents for control-
All known algorithms are worst-case exponential in the size ling the movement of the data, a few finite instantiations
 of data values are sufficient to establish the correctness
of any checkers [20]. This technique has been used to
prove data correctness for many data transport hardware
designs [11], [17].
5) Tagging. Often systems deal with a finite but large set of
distinct data values [13]. Portions of such systems can
be abstracted by simplifying the structure with respect
to a specific or a symbolic tag.
Often, using an abstraction technique requires cut-pointing a
section of the design, and adding constraints on the cut-points.
The abstraction can be used to prove the desired checks. To
complete the compositional proof [13] however, a second step
is required – the constraints need to be converted into checks,
and proven on the previously excised logic.
Fig. 2. Formal verification coverage flow
IV. C OVERAGE
A. Coverage in Simulation
In simulation-based verification, coverage metrics are used ((a && b) || c), in line 2, is reachable in n cycles, this
heavily to determine when simulation is complete. The most line would be reported as covered, and otherwise, not. Thus,
common coverage metric is code coverage, including line, line coverage numbers would mean the same in simulation –
expression, FSM and toggle coverage. Line coverage, for whether a certain coverage target is exercised or not. And
example, computes what percentage of RTL statements in the for formal, this would measure the quality of constraints (i.e.
DUT were exercised by a given set of tests. For example, absence of over-constraints), as well as the BMC proof depths.
consider: Abstraction techniques, described in Section III, can help in
achieving higher proof depths, improving the coverage results
1: always @(posedge clk) begin and thereby increasing the value of formal verification. Com-
2: if ((a && b) || c) mercial formal tools are beginning to support the measurement
3: e <= d1; of formal coverage.
4: else
5: e <= d2; C. Formal Coverage Flow
6: end Refer to Fig. 2 for the flow we use for a coverage-
This example results in two line coverage targets, corre- driven formal verification deployment. Like simulation, code
sponding to lines 3 and 5. If a test causes c to be 1, the line coverage results are used to identify missing gaps in the
3 will be marked as covered. If no test in a test suite covers formal verification implementation. Abstraction models are
line 5, line coverage for the suite will be reported at 50%. used heavily to increase the coverage to acceptable levels on
100% judged line coverage (given, say 99% automated cov- complex designs where formal would otherwise be infeasible.
erage) is frequently a requirement for an ASIC tapeout – each Since we are using the same coverage metrics, we can
line that is not automatically reported as covered in simulation, even merge coverage results. It is often the case that one
must be manually judged to be either redundant, or legacy block is verified end-to-end with formal, and a larger block
code, or symmetric to another tested line. Tapeout would be containing this block is verified with simulation. Even if the
delayed until more tests are written to cover the remaining line coverage with formal is not 100% for the block, as long
lines. 100% line coverage does not imply an absence of bug. as the unified simulation and formal line coverage is 100%,
Still, line coverage helps measure the continuous progress of verification is considered complete from the perspective of
verification completeness in a dynamic chip design schedule, line coverage goals. This of course relies on an important
and often points to important coverage holes. assumption – that the set of formal checkers is as complete as
the set of simulation checkers. Although formal coverage helps
B. Formal Coverage Metrics determine the quality of constraints as well as sequential depth
The same coverage metrics used in simulation can be reached, like simulation, coverage does not imply anything
applied to answer the question of whether the planned formal about the completeness of checkers. This has to be evaluated
verification tasks are complete, or how much the formal independently.
verification tasks complement the simulation effort [16].
Simulation-based line (or expression) coverage metrics can V. C ELL R EFORMATTER D ESIGN
be used to mean exactly the same in formal – given the The Packet Rewrite Module (PRM) design modifies in-
constraints used and the proof depths reached in BMC (say, n coming packets from multiple ports and reformats these
cycles), report what percentage of line (or expression) targets packets before passing them on. Fig. 3 shows the sequence
are reachable in n cycles. For the example in Section IV-A, if of operations on a packet when it passes through various
 Fig. 4. Toplevel of CellReformatter

CellReformatting (Stage #3) reformats the modified cells

so that they satisfy the desired ValidBytes properties and can
be repacked into a packet in the next stage. The number of
cells for a packet at end of Stage #3 may be different than
the number of cells at the beginning of the stage, depending
Fig. 3. Various stages of PRM
upon reformatting. In our example, the payload of the non-
EOP cell #2, at start of stage #3, does not satisfy the non-
EOP ValidBytes property. So, in the CellFormatter stage, this
stages of PRM. The four stages are Fragmentation (Stage #1),
cell gets reformatted to comprise of the first 128 bytes of the
Insert/Strip/Replace operations on packet payload (Stage #2),
input cell. The remaining 16 (= 144−128) bytes are appended
CellReformatting (Stage #3) and Repacking (Stage #4).
before the payload of cell #3, resulting a modified cell #3 of
A. Functional Specification 128 bytes. The 8 (= 120 + 16 − 128) trailing bytes of the
original cell #3 constitute a new cell #4.
By the end of Stage #1, each packet is fragmented into
Repacking (Stage #4) repacks the reformatted cells into a
single/multiple subpacket(s), called cells, depending upon the
packet that can be forwarded to port(s).
payload size. A cell has three main attributes: start of packet
(SOP), end of packet (EOP) and number of payload bytes B. Micro-Architecture
carried (ValidBytes). Some desired properties of the cells are:
1) The first and only the first cell has SOP as 1 CellReformatter supports reformatting of cells for packets
2) The last and only the last cell has EOP as 1 from 56 different concurrent ports. Cells for a packet on one
3) A cell with EOP as 0 will have ValidBytes as 128 port may be interleaved with cells from other ports. This
4) A cell will have ValidBytes greater than 0 increases the design and verification complexity. Fig. 4 shows
the interfaces of the CellReformatter design, the interface to
e.g. As an example, suppose at the end of Stage #1, cell #1 Stage #2 on the left side, and the interface to the Stage #4
has SOP as 1, EOP as 0 and ValidBytes as 128, cell #2 has on the right side. portIdIn refers to incoming port. cellIn
SOP as 0 and EOP as 0 and ValidBytes as 128 and cell #N represents incoming cell, varying between 1 and 256 bytes
(N = 3) has SOP as 0, EOP as 1 and ValidBytes as 120. long. cellInAttri is a structure consisting of cell attributes,
Stage #2 modifies bytes of payload of a cell by performing including SOP, EOP, ValidBytes. validIn and validOut indicate
insert, strip and replace operations. ValidBytes of each cell the validity of inputs and outputs of CellReformatter respec-
also gets modified accordingly. In Fig. 3, for the simplicity tively. Inputs are valid if they are transmitted when validIn is
of illustration, we show that only cell #2 is being modified – high. Similarly, outputs are valid if they arrive when validOut
i.e., the payloads of other cells do not undergo any change. is high. flowCtrlOut is a feedback to Stage #2 to stop it from
Payload of cell #2 gets modified to payload #2’ by insertion sending more cells for the relevant port. Thus this acts as
of two new payloads, one before, and one after the original a throttle and prevents the overflow of internal FIFO(s) for
payload, as depicted by Modified cell in the figure. In the the port. flowCtrlOut is a 56-bit wide signal with each bit
actual design, Stage #2 can modify any or all N cells. With a corresponding to a port.
combination of insert, strip and replace operations, ValidBytes
Memory Design: CellReformatter has FIFOs for storing
of a modified cell can vary between 1 and 256. Suppose, in
the reformatted cells (dataFifo) and its attributes (statusFifo).
our example, after Stage #2, ValidBytes of cell #2 is 144,
Each of dataFifo and statusFifo is implemented as an SRAM
resulting in ValidBytes of 128, 144 and 120, respectively,
memory, with separate regions for different ports. The least-
for the three cells. Due to these modifications, a cell may
significant bit of portId, called oddBank, is used to determine
not satisfy the desired properties on ValidBytes listed in the
which of the two banks is used, while the remaining higher-
previous paragraph, at the end of Stage #2. The purpose of the
significant bits, called streamId, are used as memory address:
next Stage #3, which constitutes our DUT, the CellReformatter
design, is to rectify this. portId = {streamId, oddBank}
 TABLE I
D ESIGN SUMMARY OF C ELL R EFORMATTER

Parameters Values
Inputs 4,425
Outputs 3,488
Total flops 1,048,481

C. Challenges to Formal
The major challenges to achieving convergence with formal
are:
1) Large number of flops. Greater than 1 million storage
elements (Table I) is enough to create a state space
search problem that cannot be solved without the use
of abstraction models. This large count is dominated by
the number of flops needed for dataFifo: due to number
of ports (56), number of per-port cells stored (16) and
the size of each cell (128 bytes).
2) High sequential depth due to latency. No input port
at input is allowed to appear more than once in 4
consecutive clock cycles. This constraint, along with
the latency of CellReformatter and the FIFOs depths,
implies that a high sequential depth is required for
Fig. 5. Banked architecture of dataFifo proofs.

VI. C HECKERS AND C ONSTRAINTS

As shown in Fig. 5, the memory in each bank is logically The CellReformatter design has following interface con-
divided into 28 streamId’s. Each bank of the dataFifo memory straints:
is further divided into two separate single-port SRAMs 128- 1) For a port, between 2 cells at input with SOP as 1, there
bytes wide, called MSB and LSB. Further, each port occupies should be a cell with EOP as 1
a depth of 8 entries in each of MSB and LSB. Note that in one 2) For a port, between 2 cells at input with EOP as 1, there
clock at most 256 bytes will arrive from Stage #2 for a given should be a cell with SOP as 1
port. Depending on where we wrote the last data for this port, 3) For a port, the next valid cell after an EOP as 1 must
this data will cause one or two writes into the MSB and/or have SOP as 1
the LSB section for that port. For the example in Section V-A, 4) For a port, input cell should have ValidBytes > 0
when cell #1 arrives, all of its 128 bytes are written into LSB, 5) For a port, input cell should have ValidBytes < 256
at depth of 0. When cell #2 arrives, 128 of its least significant 6) The oddBank should toggle each cycle
bytes are written to MSB at depth of 0, and the remaining 16 7) A port at input should appear no more than once in 4
bytes are written to LSB at depth of 1. Finally, when cell #3 consecutive clock cycles
arrives, its 112 (= 128 − 16) least significant bytes are shifted The interface checkers are as follows:
up by 16 bytes and written to LSB at depth of 1, and the
1) For a port, between 2 cells at output with SOP as 1,
remaining 8 (= 120 − 112) bytes are written to MSB at depth
there should be a cell with EOP as 1
1.
2) For a port, between 2 cells at output with EOP as 1,
CellReformatter has another FIFO (stateFifo) for remember- there should be a cell with SOP as 1
ing the current write and read address pointers into dataFifo 3) For a port, the next valid cell after an EOP as 1 must
for a port. This FIFO is also implemented by a single-port have SOP as 1
two-bank SRAM memory. 4) For a port, output cell should have ValidBytes > 0
Latency: The fastest end-to-end latency of CellReformatter 5) For a port, output cell with EOP as 0 should have
is 6 clock cycles; the FIFO write operation has a 4-cycle ValidBytes as 128
latency and the FIFO read operation has a 3-cycle latency. End-to-end checkers are written using a reference model that
A constraint on the design, that oddBank toggles every clock tracks the outstanding cells for a port, and also reformats
cycle, ensures that bank contention is avoided for simultaneous them into 128-byte cell boundaries. Examples of end-to-end
read and write operations. checkers:
 1) For a port, the valid output (validOut) can be 1 only if
there are outstanding cells in flight that have not been
sent out
2) For a port, payload of a cell at the output should
correspond to payload of expected cell in the reference
model, computed based on payloads that arrived at the
input in the past
Consider this last end-to-end checker, the most important
checker for this DUT. The checker is written in SVA as:
property cellOutMatch_a;
@(posedge clk) disable iff(reset)
(validOut &&
(portIdOut == watchedPort)) |->
(cellOut[watchedByte][watchedBit] ==
referenceBit);
endproperty
cellOutMatch_A:
assert property(cellOutMatch_a);
We used the following symbolic variables in this checker:
Fig. 6. Deploying memory abstraction for dataFifo
1) watchedPort. This variable, varying between 0 and 55,
represents the specific port that is being verified. While
the design interleaves the inputs and outputs across
A. Memory Abstraction
multiple ports, in one trace, we can verify the outputs
for a specific port. The dataFifo memory stores up to 16 cells for every port, 8
2) watchedByte. This variable, varying between 0 and 127, cells in LSB, and 8 in MSB. The memory stores the reformatted
represents the specific byte number in an output cell that cells, after performing the necessary shifting, described in Sec-
is being verified in this trace. tion V-B. Since the main end-to-end checker (cellOutMatch A
3) watchedBit. This variable, varying between 0 and 7, rep- in Section VI) uses symbolic watched variables for the port
resents the specific bit being verified in the watchedByte number and the verified bit in a cell, each flop in dataFifo is
byte. essential to establish the correctness of the proof. This places
Since these variables are symbolic, all possible output data a tremendous burden on a formal verification tool.
bits from all possible ports are verified with the end-to-end Using the three watched symbolic variables, we create an
checker. In any given trace of execution, these variables can abstraction for dataFifo, shown in Fig. 6. This abstraction
be kept constant with SVA constraints like the following: model contains only 16 flops, 8 for an abstraction of the LSB
section of the memory banks, and 8 for an abstraction for the
property watchedPort_r: MSB section.
@(posedge clk) disable iff(reset) We tie the inputs of the abstract dataFifo to the inputs
(##1 $stable(watchedPort)); of the RTL dataFifo (implemented by the SystemVerilog
endproperty bind construct). In addition, watchedPort, watchedByte and
watchedPort_R: watchedBit are extra inputs to the abstract dataFifo.
assume property(watchedPort_r); When there is write to the RTL memory, if the write address
This end-to-end checker also depends on the predicted value input matches watchedPort, we pick the watchedBit bit from
of the output bit from the reference model, referenceBit. The the watchedByte of the write data input to the memory, and
reference model is implemented in SystemVerilog, and using store that in one of the 16 bits in the abstract memory (4 least
the three watched symbolic variables, implementing a queue of significant bits of the write address input determine which of
watched bits in flight in the design. The value of referenceBit the 16 per-port cells was being written by the write command).
equals the bit at the top of the queue. We will discuss an To enable the abstraction, we add cut-points at the read data
abstraction in Section VII-B, that shows how to implement outputs of the RTL dataFifo. Further, we add a constraint that
this reference model more efficiently. if the read address input matches watchedPort, then watchedBit
bit of watchedByte read data output byte equals the value
VII. A BSTRACTION M ODELS stored in the i-th (of 16) abstract dataFifo bits (where i equals
We have a design with more than 1 million flops. This will the 4 least significant bits in the read address input). This
lead to state space explosion with any existing formal verifi- enables the read data for the watched bit to be faithful to
cation tool. Abstractions are essential to achieve convergence what is in the RTL, and the remaining bits or read data output
on a design like this. for a non-watched port to be arbitrary. But, since the checker
 the preservation of infinite streams of the form 0? 110ω across
the design. Each stream in this set has a finite but arbitrary
number of 0’s followed by two consecutive 1’s, followed by
an infinite sequence of 0’s; for example, input sequences like
11000 · · ·, 011000 · · ·, and 000 · · · 011000 · · ·. Note that given
the three watched symbolic variables, we need to apply this
abstraction only to the consecutive bits that will be written to
the abstract dataFifo from the previous section.
We add a constraint to the inputs of the DUT so that watched
bits create this sequence by using the state machine in Fig. 7.
We constrain the inputs so that the error state S3 is never
reachable. Next, we use an identical state machine to verify
the output watched bit from the DUT. We modify the checker
Fig. 7. State machine for pattern 0? 110ω detection so that the expected referenceBit is not allowed to be 0 is state
S1, or to be 1 in state S2 – all other values are allowed for
referenceBit.
is checking only the watched port and the watched bit, the Using this data independence abstraction, we do not have
abstraction should not give a false negative. to implement a reference FIFO, whose depth is design-
Using this abstraction model, we have reduced 917,504 flops dependent. We save additional flops in the cone-of-influence,
in the RTL dataFifo that were in the cone-of-influence of the and proofs run much faster.
end-to-end checker to the 16 flops in the abstract dataFifo.
More important, this abstraction does not introduce any false VIII. E XPERIMENTAL R ESULTS
negatives with respect to the end-to-end checker. Similar We used the Cadence R
Incisive
R
Enterprise Verifier (IEV)
abstraction models were built for statusFifo and stateFifo, tool [2] for this verification. Since the un-abstracted design
albeit only with respect to watchedPort. See Table II for the has more than 1 million flops, hence it is not feasible to run
reductions in the cone-of-influence; note that there are other formal without deploying the abstraction models described in
peripheral flops in the memories because the memories have Section VII.
additional flops due to the latency, as well as some parity- The verification setup for the DUT consists of the CellRe-
checking flops. formatter RTL, checkers and constraints (using the necessary
Note that to complete the proof with abstractions using reference models), and the abstraction models described in
compositional reasoning, we also need to separately prove Section VII. There are 23 checkers and 21 constraints. We
that the abstract dataFifo is a sound abstraction of the RTL found 15 bugs in the RTL design.
dataFifo. We do this by removing the cut-points on the read As expected, BMC was the most effective engine for ver-
data outputs, and reversing the constraints on the read data ifying the main end-to-end checker. For the shortest possible
outputs to checkers, then proving them independently of the packet, the data can be seen at the output of the design at
main end-to-end checker. a BMC proof depth of 7 clock cycles. However, the most
interesting behavior of the design occurs when dataFifo is full
B. Data Independence Abstraction before data is unloaded to the outputs. By understanding the
The main end-to-end checker (cellOutMatch A in Sec- design micro-architecture, including the latencies and memory
tion VI) requires a reference model for the expected behavior depths, it was determined that a proof depth of 63 cycles
of the referenceBit bit. Even after the memory abstraction in is sufficient to hit this extreme behavior (the constraint that
the previous section, we know that there are at least 16 bits in successive input data for the same port must be 4 cycles apart
flight for the watched bit we want to track. However, this is is responsible for much of this depth).
just a lower bound, since there may be additional bits on the We use the IEV code coverage feature to report the amount
way to dataFifo, or on the way from dataFifo. Suppose there of coverage hit to determine if the use of abstractions was suc-
are at most n bits in flight we need to track; to implement the cessful in covering the design. Coverage results are reported
reference model with a FIFO, we will need at least n entries in Table III. We notice that the expression coverage is 100%
in the reference model FIFO. and the line coverage is almost 100% at a proof depth of 63.
Fortunately, we can use a variant of the data independence The missing coverage holes need to be judged and possibly
abstraction [20], to avoid the dependence on the unknown n, waived by the design engineers. For the un-abstracted design,
and more importantly to verify with more efficient state space. the BMC proof depths reached at similar run-times are close
The data independence theorems state that for certain data- to 0, hence the corresponding coverage results are close to 0%
independent designs (when data is merely transported across (not surprising given the amount of state in the DUT).
the design, and not queried to make the routing decisions), The level of coverage reached is very much in line with the
a small set of finite data values is sufficient for end-to-end desired verification coverage, if we were verifying this design
proofs. For our end-to-end checker, it is sufficient to prove using simulation. We must remind the reader that the desired
 TABLE II
C OMPARISON OF RTL AND ABSTRACT MEMORIES [6] A. Datta, V. Singhal. Formal Verification of a Public-Domain DDR2
Controller Design. In Proc. VLSI Design, pp. 475–480, 2008.
[7] C. N. Ip, D. L. Dill. Better verification through symmetry. Formal
Memory Flops in Flops in Methods in System Design, 9(1/2), pp. 41–75, 1996.
RTL abstract memory [8] IEEE standard for SystemVerilog: unified hardware design, specification
and verification language. IEEE Std. 1800-2009.
dataFifo 948,636 204 [9] M. Kantrowitz, L. M. Noack. I’m done simulating; now what? Verification
coverage analysis and correctness checking of the DECchip 21164 Alpha
statusFifo 89,986 4,854 microprocessor. In Proc. Design Automation Conf., pp. 325–330, 1996.
[10] S. Katz, O. Grumberg, D. Geist. Have I written enough properties? A
stateFifo 2,394 268
method of comparison between specification and implementation. In Proc.
CHARME, LNCS 1703, pp. 280–297, 1999.
TABLE III [11] B. A. Krishna, A. Sullerey, A. Jain. Formal verification of an ASIC
F ORMAL COVERAGE RESULTS Ethernet switch block. In Proc. FMCAD, pp. 13–20, 2010.
[12] R. P. Kurshan. Formal verification in a commercial setting. In Proc.
Proof Line Expression Design Automation Conf., pp. 258–262, 1997.
[13] K. L. McMillan. Verification of an implementation of Tomasulo’s
depth coverage coverage algorithm by compositional model checking. In Proc. CAV, LNCS 1497,
pp. 110-121, 1998.
7 96.5% 100.0% [14] F. Pong, M. Dubois. A new approach for the verification of cache
15 99.5% 100.0% coherence protocols. IEEE Trans. Parallel Distrib. Syst. 6(8), pp. 773-
787, 1995.
63 99.7% 100.0% [15] C. Sayer, J. Sonander. Formal verification of AMBA 3 AXI bus systems.
In ARM Information Quarterly, pp. 15-17, 4(2), 2005.
[16] V. Singhal, P. Aggarwal. Using Coverage to Deploy Formal in a
Simulation World. In Proc. CAV, LNCS 6806, pp. 44-49, 2011.
coverage result must be considered in conjunction with the [17] C. Stangier, U. Holtmann. Applying formal verification with Protocol
Compiler. In Proc. Euromicro Symp. Digital Systems Design, pp. 165–
confidence in the completeness of checkers. Unfortunately, as 169, 2001.
with simulation, formal code coverage by itself does not yet [18] S. Tasiran, K. Keutzer. Coverage metrics for functional validation of
determine the completeness of checkers. However, we do know hardware designs. IEEE Des. Test, 18(4), pp. 36–45, 2001.
[19] C. Wang, G. D. Hachtel, F. Somenzi. Abstraction refinement for large
that with the use of the abstraction models, we were able to scale model checking. Springer, 2006.
exercise almost all the RTL code. Without these abstraction [20] P. Wolper. Expressing interesting properties of programs in propositional
models, we would not get much more than 0% coverage, temporal logic. In Proc. POPL ’86, pp. 184–193, 1986.
[21] P. Yeung. How to instrument your design with simple SystemVerilog
and formal verification would not have been able to replace assertions. EE Times DesignLine, January 26, 2011.
simulation on this design.
IX. C ONCLUSION
In this work, we show how end-to-end formal can replace
simulation efforts and provide faster verification with higher
coverage. Without the use of abstraction models, formal veri-
fication is often infeasible for end-to-end verification. With the
use of abstraction models, we can counter state space explo-
sion, and reach acceptable levels of quantifiable code coverage
metrics. These results can be integrated with simulation-based
code coverage results on neighboring designs, or the rest of
the system.
ACKNOWLEDGEMENT
The authors would like to thank Sandesh Borgaonkar, Anton
Lopatinsky and Deepak Pant for their for help and support in
making this work possible.
R EFERENCES
[1] A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, Y. Zhu. Bounded model
checking. Advances in Computers, 58, 2003.
[2] Cadence Incisive Enterprise Verifier datasheet. Cadence Design Systems,
Inc.
[3] E. M. Clarke, O. Grumberg, D. E. Long. Model checking and abstraction.
ACM Trans. Program. Lang. Syst., 16(5), pp. 1512–1542, 1994.
[4] E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long, K. L. McMil-
lan, L. A. Ness. Verification of the Futurebus+ cache coherence protocol.
Formal Methods in System Design, 6(2), pp. 217–232, 1995.
[5] E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith. Counterexample-
guided abstraction refinement for symbolic model checking. J. ACM
50(5), pp. 752–794, 2003.