FPGA Verification and Validation
Jason G. Cooper, MS1; Heath
W. Haga2; Sam R. Brown2
2Titan Systems
Corporation
Abstract
Field
programmable gate arrays (FPGAs) are configurable, digital integrated circuits. The configuration occurs in programmable
blocks of logic and those block’s interconnections. The “field programmable” designation simply
means that the internal functionality is not hard-wired until a final design is
established, and then the chip set is hard-wired for increased performance. In the world of digital integrated circuits,
FPGAs fall between programmable logic devices (PLDs) and application-specific
integrated circuits (ASICs) – their robust functionality allows them to be
field customizable, if necessary, while also containing a large amount of logic
gates with extreme complexity.1
While
similar in many respects, the verification and validation techniques necessary
for FPGAs (and their specific hardware description languages) do differ from
the standard techniques used for software analysis. These systems are unique in their design
aspects and require special attention to the logic embedded in hardware
controls. We aim to address some of
these issues and highlight areas of specific consideration when performing
analyses on mission critical FPGA-inclusive systems.
Verification and Validation
Prior
to exploring FPGA analysis details, one must understand the underlying
framework of software verification and validation (V&V), and what the
objectives of such a framework are.
Verification is typically explained using the catchphrase “are we
building the product right?” whereas validation is explained similarly by “are
we building the right product?”
Verification aims to prove that a software item conforms to its
specifications and processes used to build that software item are sound. Validation aims to prove that the end-user
requirements are being met.2 These methods are classically employed during
each phase of the software lifecycle.
The
overarching objectives of V&V can be summed as the discovery of system
defects and the overall assessment that the software is safe, reliable,
maintainable, and ultimately usable to complete its assigned mission. In the context of FPGAs, the objectives
remain the same; however, the definitions of V&V might be stated somewhat
differently.
General Considerations
FPGA
Verification could be stated as white-box analysis, to include pre-silicon
testing which verifies the design is correct as represented in the hardware
description language (HDL). There are
both static and dynamic aspects to this verification, which will be explored
later. FPGA Validation could be stated
as black-box analysis, to include post-silicon end-to-end testing to validate
the chip design is correct for the stated mission parameters.
Interestingly,
due to recent advances in co-simulation capabilities, validation will
eventually be performed in pre-silicon phases as well. Another general concern is that FPGA designs
are typically committed quite early in project lifecycles. This makes early, up-front V&V efforts
essential to success. Changes to FPGA
design, later in the overall system development, are expensive and can cause
effort duplication.
Static Considerations
The
two principle FPGA definition languages, VHDL and Verilog, were originally
derived from design simulation packages which contained internal static code
analysis tools of varying effectiveness.
A certain number of independent Verilog design verification tools have
appeared over the last several years.
Commercial pressures for fast time-to-market and verification have led
to highly integrated and costly development suites.
Static
HDL analysis, on the surface less engaging than dynamic analysis, remains a
useful process in FPGA verification.
Lint- like analysis, a familiar tool used with other languages, has the
potential to capture poor coding practices in HDL. One specific area of interest would be
identification of synthesis latch generation scenarios. These errors are realized post-synthesis as
nonequivalent implementations. An analysis focusing on assertions specified in
the HDL can be effective for both model and algorithm scrutiny.
Dynamic Considerations
Dynamic
verification can be performed by utilizing both functional and timing
simulations. The functional simulations
can be applied to pre-synthesis design as functional Register Transfer Level
(RTL) tests and post-synthesis as gate-level testing. Timing simulations are performed post-synthesis
on the generated ‘netlist’ – a list of nets which connect flippers and gates,
usually specified as an Electronic Design Interchange Format (EDIF) file. The focus of these simulations on the
‘netlist’ is to target best and worst case timing scenarios. These scenarios are likely targets failing to
meet the design requirements. Post-synthesis
dynamic verification should also involve equivalence checking to guarantee the
HDL implementation met the design intent.
Most
verification tools offer simulation of the basic functions such that the
general characteristics of the design may be viewed graphically to see the
relationships between the various signals.
However, FPGAs are often used in time-critical applications where signal
propagation through the design, and even internal routing, can make critical
differences in the performance and suitability of the design. These timing nuances must be measured and
mitigated.
Modeling
PROMELA
(PROcess MEta LAnguage) is a language used to build formal verification
models. The specification language is
designed to allow the user to abstract from computational design details and
focus on system-level process interaction.
Due to PROMELAs applicability to distributed systems and
non-deterministic control structures, it is well situated for use in FPGA
modeling. The language can also include worst-case
assumptions, allowing for exploration of off-nominal scenarios.
The
HDL assertions could be used to generate PROMELA code, fed into Spin*
(the verification tool which executes the model code), and thus verify system
correctness. Basic safety and liveness
properties could also be expressed and verified. An extremely interesting exercise would be to
explore an automated tool which could produce PROMELA from the HDL and feed
directly into Spin without manual guidance.
There are several options for consideration since Spin can be used as a
simulator, an exhaustive verifier, as well as a proof approximation system.3
Conclusion
FPGA
V&V requires early insertion into the development lifecycle. This is imperative to ensure design
correctness and reduce potentially costly changes in the chip set. The methods used are similar to software
V&V, yet the unique characteristics of FPGAs require additional
analyses. As this field continues to
expand, and both manned and autonomous spacecraft take advantage of FPGAs, the methods
used to provide high quality V&V will need to grow as well. Active research in this field should be
encouraged and pursued.
References
1.
Maxfield C. The
Design Warrior’s Guide to FPGAs.
2.
Sommerville
I. Software
Engineering.
3.
Spin – Formal Verification. Retrieved
July 18, 2005, from http://spinroot.com.
Contact Information
Jason
Cooper, jason.cooper@matric.cc
Heath
Haga, heath.haga@es3.titan.com
Sam
Brown, sam.brown@titan.com