Combining System Level Modeling with Assertion Based Verification

 This paper describes the use of a PSLbased
ABV methodology in a C++-based system level
modeling and simulation environment. We describe the
considerations of porting a tool which translates PSL to
VHDL/Verilog, to support C++, a language which was
designed for software and does not have concurrent language
constructs. The translation scheme is shown to be
adaptable to all C-based environments. We exemplify the
wide applicability of this scheme by detailing its successful
deployment in a SystemC-based industrial System-on-Chip
(SoC) project.
1. Introduction and Motivation
As the complexity of hardware designs has grown to the
degree that the traditional approaches have limitations, the
need for a better verification methodology, one with
improved levels of observability of the design behavior and
controllability of the verification process has become clear.
Assertion-Based Verification (ABV) has been identified as
a modern, powerful verification paradigm that can assure
enhanced productivity, higher design quality and, ultimately,
faster time to market and higher value to engineers
and end-users of electronics products. With ABV, assertions
are used to capture the required temporal behavior of
the design, in a formal and unambiguous way. The design
then can be verified against those assertions using simulation
and/or static verification (e.g. model checking) techniques
to assure that it indeed conforms to the intended
design intent, as captured by the assertions.
ABV has gained a very strong momentum over the last
years, as evident by the increasing number of verification
of experience reports and case studies, books, commercial
offerings, and standard activities and academic research
efforts in this area. A significant ingredient of this momentum
has been the official selection of the language PSL [3],
based on the Sugar language from IBM, as an industry
standard. Over 50% of the respondents of a recent survey
conducted by John Cooley, on the proliferation of ABV [4]
said they use or plan to use ABV on their next project. Of
those that responded positively, PSL was by far the most
popular assertion language of choice.
In most industrial settings, an evolutionary approach to
ABV has been taken where first and foremost assertions
are used as a part of the traditional simulation methodology
– with which most engineers feel more comfortable with.
In accordance with this tendency, and to enable effective
deployment of ABV in a simulation environment, we have
developed a platform called FoCs ("Formal Checkers") [7].
FoCs takes PSL/Sugar properties as input and translates
them into assertion checking modules ("checkers") which
are integrated into the simulation environment and monitor
simulation on a cycle-by-cycle basis for violations of the
property. For each property of the specification, represented
as a PSL Property, FoCs generates a checker for
simulation. This checker essentially implements a state
machine which will enter an error state in a simulation run
if the formula fails to hold in this run. In Section 3 we will
describe the checker generation process in more detail.
The philosophy behind the development of FoCs has
been to provide enhanced productivity to simulation
through automation of the checker creation effort. Checkers
are, in fact, a traditional part of simulation environments
([9]). They facilitate effective testing, as they
automate test results analysis. Moreover, checkers facilitate
the analysis of intermediate results, and therefore save
debugging effort by identifying problems directly - "as
they happen", and by pointing more accurately to the
source of the problems. However, the manual development
and maintenance of checkers is a notoriously high-cost and
labor-intensive effort, especially if the rules to be verified
are complex temporal ones. This has been an impeding factor
to verification productivity. For instance, in the case of
a checker for a design with overlapping transactions
(detailed in Section 3), writing a checker manually is an
excruciating error-prone effort.
Several solutions have been proposed over the last five
years to avoid the inefficiencies involved with manual
checker writing. Generally speaking, these approaches
include libraries of checkers such as the popular publicdomain
OVL library [2] and proprietary libraries such as
CheckerWare from 0-in [1]. These libraries serve as repositories
of checking modules which can be instantiated as
necessary in test-benches and facilitate specific checking
Combining System Level Modeling with Assertion Based Verification
Anat Dahan, Daniel Geist, Leonid Gluhovsky, Dmitry Pidan, Gil Shapir, YaronWolfsthal
IBM Haifa Research Lab, Haifa Israel
Lyes Benalycherif, Romain Kamdem, Younes Lahbib
ST Microelectronics, Grenoble, France
Proceedings of the Sixth International Symposium on Quality Electronic Design (ISQED’05)
0-7695-2301-3/05 $ 20.00 IEEE
goals. For example, OVL has a module for checking that a
specified expression must not change its value for a specified
period of time; and CheckerWare has modules for
checking various arbitration policies. While very useful
when applied for checking specific situations, the largest
deficiency of libraries such as OVL is that they are fixedform
and thus generally inflexible (though some of them
offer a certain degree of configurability).
Observing the inefficient process of manual checker
writing in ongoing projects, and the limited remedy offered
by libraries of checkers, we recognized that for best results,
and effective ABV solution needs to include two components:
a formal declarative language for defining the
desired checks, and a mechanism for automatically transforming
the definition of the checks into effective checking
modules. This has inspired the development of FoCs as a
means for automatically generating checkers from simple
specifications. For example, SystemVerilog [12] also has a
set of language constructs for writing assertions, called
simply SystemVerilog Assertions (SVA). A similar
approach to ours is proposed by [10] to augment SystemC
with SVA but only considering a subset of SVA and relying
for the translation of SVA into SystemC modules on internal
SystemC [5] was developed about six years ago as the
verification platform for SoC verification and hardwaresoftware
co-verification. SystemC is a set of C++ libraries
that let designers and verification engineers write hardware
like modules in C++. SystemC contains classes that imitate
low level hardware constructs like registers and also higher
level hardware constructs like channels. Despite the energy
and momentum that vendors and chip developers put into
SystemC, the acceptance of SystemC as a way to implement
verification was slower than expected. However, the
last two years have seen a growing interest in the platform
since SoC development is on the rise and is becoming more
popular in design starts [11].
FoCs has been put to multiple types of successful use by
engineering teams in the industry. In those past project,
FoCs was used to translate the assertions directly to native
language of the design (VHDL or Verilog) which have
built-in temporal and concurrent semantics. Generation
Checkers for SystemC required the definition of PSL
semantics for C++. Instead of developing a PSL to SystemC
translator, we developed a translation mechanism
that is suitable for any C++ based modeling environment
and not necessarily SystemC. We used this version of FoCs
to implement PSL based ABV on a industrial System-on-
Chip (SoC) which had a SystemC high-level.
The rest of this paper is as follows. Section 2 gives a
brief overview of PSL. Section 3 describes our translation
method to C++. In Section 4 we describe the SoC and the
results of using FoCs for implementing PSL based ABV on
top its SystemC based verification platform. The final section
details our conclusions and future plans.

Tags :
Your rating: None Average: 3 (3 votes)