Where this assertion-based verification originate?

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.1, Item 12.0)

From: Dan Paley

Does anyone know where the idea of assertion based testing originated?
Is there an original or initial paper/patents which begins to describe
this idea?

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.2, Item 6.0)

From: Adam Krolnik

The earliest reference is from Robert Floyd.

Floyd, R. W. (1967) "Assigning meanings to programs". Proceedings
of Symposia in Applied Mathematics. American Mathematical Society,
Vol. 19, 19-32.

But also, Dijkstra (1968)

"A constructive approach to the problem of program correctness"

Oops, here's a reference to two (haven't seen these.)

Turing (1950)

On checking a large routine. Also,

McCarthy (1963), "A basis for mathematical theory of computation".

Of course Bertrand Meyer, creator of Eiffel has developed the most
thorough language to incorporate the principles of assertions via his
"design by contract" principles...

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.2, Item 6.1)

From: Richard C. Ho

I think it is safe to say that hardware designers have been applying
early forms of assertion-based verification for as long as hardware
description languages have been around. After all, when designers say
$display("Error") in their Verilog code, they are making an assertion
about how their design should (should not) behave.

But one of the earliest papers that clearly expounded the use of
assertions as part of a functional verification methodology is:

"I'm Done Simulating; Now What?: Verification Coverage Analysis and
Correctness Checking of the DECchip 21164 Alpha Microprocessor" by
Michael Kantrowitz and Lisa M. Noack (Proc. 33rd Design Automation
Conference, June 1996, page 325-330)

In this paper, the authors talk about "Assertion Checkers," which they
define as follows:

"Assertion checkers are segments of code added to a model to check
that various properties or rules of design behavior are not
violated."

From a commercial perspective, 0-In Design Automation was founded in
1996 to productize the use of assertion checkers for functional
verification and the use of formal verification to prove or disprove
the assertion checkers. In 1997, 0-In filed a fundamental patent in
this area, entitled "Method for Automatically Generating Checkers for
Finding Functional Defects in a Description of a Circuit", which
issued as U.S. Patent No. 6,175,946 B1 in January of 2001.

A large number of papers, articles, printed material appeared in the
years following 1997 from a number of sources. We've collected
references to a number of these on the 0-In web site (www.0-In.com).

Newsletter · Original Contribution Joined: Dec 08, 2003 Posts: 1107

(Originally from Issue 4.3, Item 7.0)

From: Adam Krolnik

ere are Turing's words from his short paper on "Checking a large
routine."

"How can one check a large routine in the sense of making sure that
it's right?

In order that the man who checks may not have too difficult a task,
the programmer should make a number of definite assertions which can
be checked individually, and from which the correctness of the whole
program easily flows"

Alan Turing - June 24, 1949

- Adam Krolnik, LSI Logic Corp