From nm@id.dth.dk Fri Oct 7 07:53:21 1994
Received: from moose.cs.indiana.edu by wobbegong.cs.indiana.edu
(5.65c/9.4jsm) id AA22004; Fri, 7 Oct 1994 07:53:19 -0500
Received: from idst.id.dtu.dk by moose.cs.indiana.edu
(5.65c/9.4jsm) id AA29777; Fri, 7 Oct 1994 07:53:00 -0500
Received: from localhost (nm@localhost) by idst.id.dtu.dk (8.6.4/8.6.4) id NAA15700; Fri, 7 Oct 1994 13:51:13 +0100
Date: Fri, 7 Oct 1994 13:51:13 +0100
From: Niels Mellergaard
Message-Id: <199410071251.NAA15700@idst.id.dtu.dk>
To: sjohnson@cs.indiana.edu
Subject: The Single Pulser
Status: RO
Steven Johnson,
Inspired by your talk at the TPCD conference we have made an attempt to
describe the Single Pulser in Synchronized Transitions. A summary of our
experiments is given below.
Niels.
--------------
Single Pulser.
==============
The following is an attempt to specify and verify the Single Pulser design
using Synchronized Transitions techniques. The observable behavior of the
Single Pulser is specified as follows [JMP94]:
The Single Pulser emits a single unit-time pulse on o for each pulse
received on i.
HHHHHHHHHHHH HHHHHHHHHH
i: LL LLLLLLLLLLLLLLLLLLLL LLLLLLLLLLL
H H
o: LLLLL LLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLL LLLLLLLLLLLLLLL
It is not specified precisely when the single pulse should be emitted.
Specification.
==============
The abstract specification is given as a design described in Synchronized
Transitions. The design is abstract in the sense that it is
non-deterministic, i.e. with respect to the emission of o.
The specification is operational and has internal state, however, seen from
the external interface it is the most abstract description, because any allowed
behavior on the interface (the i and o signals) may be observed from the
specification.
Two Synchronized Transitions specifications are given:
1) Spec1 allows the single pulse to be emitted in the "neighborhood"
of the high i-pulse (as shown in the diagram above),
2) Spec2 allows the single pulse to be emitted in the "neighborhood"
of the entire i-pulse (i may be either high or low).
The "neighborhood" is defined as follows:
-----------------------------------------
a) The earliest time that is in the neighborhood of the high/entire i-pulse
is the first "clock" period after i has changed to high:
HHHHHHHHH
i: LLLLLLL
H
o: LLLLLLLL LLLLLLL
b1) The latest time that is in the neighborhood of the high i-pulse is the
first "clock" period after i has changed to low (relevant for Spec1):
HHHHHHHHHHHHHHHHH HHHHHHHHHHHHH
i: LLLLLLL LLLLLLLLLLLLLLLL
H
o: LLLLLLLLLLLLLLLLLLLLLLLLL LLLLLLLL
b2) The latest time that is in the neighborhood of the entire i-pulse is the
first "clock" period after i has changed to high in the next input pulse
(relevant for Spec2):
HHHHHHHHHHHHHHHHH HHHHHHHHHHHHH
i: LLLLLLL LLLLLLLLLLLLLLLL
H
o: LLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLLL L
In case b2) the neighborhoods of two consecutive i-pulses overlap.
To summarize, Spec1 specifies a Single Pulser that emits a unit time pulse
non-deterministically between a) and b1); Spec2 specifies a Single Pulser
that emits a unit time pulse non-deterministically between a) and b2).
Remark on design verification.
------------------------------
Alternatively, one could imagine specifying the single pulse property with
invariants and protocols and then verify that a design descriptions
meets these. We think it is possible to find protocols and invariants
capturing the first of the two specs given above, but it is probably not
possible to characterize the more general case (Spec2), without
augmenting the specification with "history variables".
Implementations.
================
Impl1 and Impl2 are two possible implementations of both of the Single
Pulser specifications:
1) Impl1 emits a single pulse at the earliest possible time (after i goes
high).
2) Impl2 emits a single pulse after i goes low.
Remark: It turns out that Spec1 is an implementation of Spec2.
Verification.
=============
It is verified by implementation verification that the implementations
implement the specifications. The verification is done mechanically using a
translator (stref) as described in [NBM94] and a theorem prover (LP). It is
necessary to verify simple invariants (design verification) for the
implementations. This is done using the translator st2lp and LP as described
in [NMJS94].
It has been proved that Spec1 implements Spec2, that Impl1 and Impl2 implement
Spec1, and that Impl1 and Impl2 implement Spec2 (this also follows by
a transitivity rule):
. . Spec2 . .
. | .
. | .
. v .
. Spec1 .
. / \ .
. / \ .
v v v v
Impl1 Impl2
Refinement mappings.
====================
The tricky thing (as usual) is to determine the refinement mappings.
In all versions the identity mapping is made on i, o, and the local state
variable x. In Spec1 and Spec2 the additional state variable p is mapped
as follows:
Spec2-Spec1:
Spec2.p <- Spec1.p OR NOT Spec1.x
Spec1-Impl1:
Spec1.p <- Impl1.x
Spec1-Impl2:
Spec1.p <- FALSE
The refinement mappings for the implementations (Impl1 and Impl2) of the
specification Spec2 is given by composing the refinement mapping from
Spec2 to Spec1 with the refinement mappings from Spec1 to the two
implementations (Impl1 and Impl2):
Spec2-Impl1:
Spec2.p <- Spec1.p OR NOT Spec1.x
<- Impl1.x OR NOT Impl1.x
<- TRUE
Spec2-Impl2
Spec2.p <- Spec1.p OR NOT Spec1.x
<- FALSE OR NOT Impl2.x
<- NOT Impl2.x
The validity of the last refinements above also follows by transitivity of
refinement.
Statistics.
===========
The translator from Synchronized Transitions to C (st2c) was used to do
simulations on the initial design descriptions. The translator st2lp was used
to generate proof obligations for invariants. The translator stref was used to
generate proof obligations for refinement. The theorem prover LP was used to
verify invariants and refinements.
All the refinements and the design verification proofs (of invariants) are
done without any manual assistance to LP;
the CPU time for each proof is in the magnitude of one minute. The
human time used on describing and "debugging" the specifications and
implementations, and on succeeding all proofs was approx. 1 day.
References:
===========
[JMP94] Steven D. Johnson, Paul S. Miner, and Shyam Pullela. "Studies of the
Single Pulser in Various Reasoning Systems", TPCD'94.
[NBM94] Niels Maretti, "Mechanized Verification of Refinement", TPCD'94.
[NMJS94] Niels Mellergaard and Joergen Staunstrup, "Tutorial on Design
Verification with Synchronized Transitions", TPCD'94.
The design descriptions:
========================
Spec2:
------
CELL singlepulser(i, o: BOOLEAN)
STATE x, p: BOOLEAN
INITIALLY
i = FALSE
x = FALSE
o = FALSE
p = TRUE
BEGIN
<< x := i >> *
((<< o -> o := FALSE >> *
(<< i AND NOT x AND p -> p := FALSE >> || << NOT (i AND NOT x) >>)) ||
(<< NOT o >> *
((<< i AND NOT x >> *
(<< NOT p -> o, p := TRUE, FALSE >> ||
<< p -> p := FALSE >> ||
<< p -> o, p := TRUE, TRUE >>)) ||
(<< NOT (i AND NOT x) >> *
(<< NOT p -> o, p := TRUE, TRUE >> || << TRUE >>)))))
END singlepulser
Spec1:
------
CELL singlepulser(i, o: BOOLEAN)
STATE x, p: BOOLEAN
INITIALLY
i = FALSE
x = FALSE
o = FALSE
p = FALSE
INVARIANT p => x
BEGIN
<< x := i >> *
((<< o -> o := FALSE >> *
(<< NOT i AND x AND p -> p := FALSE >> || << NOT (NOT i AND x) >>)) ||
(<< NOT o >> *
((<< NOT i AND x -> p := FALSE >> *
(<< NOT p -> o := TRUE >> || << p >>)) ||
(<< NOT (NOT i AND x) >> *
(<< i AND NOT p -> o, p := TRUE, TRUE >> || << TRUE >>)))))
END singlepulser
Impl1:
------
CELL singlepulser(i, o: BOOLEAN)
STATE x: BOOLEAN
INITIALLY
i = FALSE
x = FALSE
o = FALSE
INVARIANT o => x
BEGIN
<< o, x := i AND NOT x, i >>
END singlepulser
Impl2:
------
CELL singlepulser(i, o: BOOLEAN)
STATE x: BOOLEAN
INITIALLY
i = FALSE
x = FALSE
o = FALSE
INVARIANT o => NOT x
BEGIN
<< o, x := NOT i AND x, i >>
END singlepulser