Untitled

Testing the F ormalCheckTM Query Library
email: doron,gerard,k @research.bell-labs.com Abstract
(for given coverage) and ease of application than is possi-ble using simulation.
FormalCheckT M is a Computer-Aided Design tool devel- Verification in the context of FormalCheck consists of oped jointly by Lucent Technologies’ Bell Labs Research an algorithmic check that the formal language of a circuit and its Advanced Technologies Design Automation Lab, for model is contained in the formal language of an automa- the automatic verification of hardware designs. Design Au- ton which captures the query or properties to be verified on tomation supports FormalCheck both internally and com- the circuit model. When this language containment check mercially. The utility of this tool lies in its ability to offer a passes, it means that the circuit design satisfies the proper- more reliable means for checking the correctness of a con- ties stated in the given query, under all conditions consistent trol circuit than is afforded with simulation, together with a with the query. This is much more general than simulation greater speed and ease of application than is possible using which can check a circuit design only for selected input se- simulation. It is applied to a circuit by posing queries about the circuit (relating to its proper operation) which the tool FormalCheck employs COSPAN [KH90, HHK96] as its then answers either in the affirmative, or in the negative– verification engine. COSPAN, a general-purpose automata- presenting a trace to a point where the circuit fails to exhibit based tool for coordination specification analysis, con- the behavior defined in the query. Internally to the tool, tains the algorithms to perform the language containment each query is translated into an automaton model, against which the circuit is checked. It therefore is absolutely criti- FormalCheck is applied to a circuit by posing queries cal that the automata models generated by the queries con- about the circuit (relating to its proper operation) which form to the intentions of the designers who formulate thequeries. We have tested this conformance and established the tool then answers either in the affirmative, or in the a regression test bench for the query mechanism, by estab- negative– presenting a trace to a point where the circuit fails lishing two unrelated automata generators for queries, and to exhibit the behavior defined in the query. Internally tothe tool, each query is translated into an automaton model, a means to test that the generated automata are equivalent. against which the circuit is checked by COSPAN. A queryconsists of two parts: properties for which the circuit modelis checked, and constraints on the environment of the cir-cuit, which are assumptions about the behavior of compan-ion components. In order to verify the given circuit, it is Introduction
assumed that the companion components fulfill their behav-ioral requirements. Without such an assumption, the given circuit may not behave properly (and it is not required to be- tool developed jointly by Lucent Technologies’ Bell Labs Research and its Advanced Technologies Design Automa- The user of FormalCheck defines each query (its prop- tion Lab, for the automatic verification of hardware designs.
erties and constraints) through a graphical interface (Figure Design Automation supports FormalCheck both internally 1) which supports a very simple logical idiom. In this id- and commercially. The utility of this tool lies in its ability to iom, each property and constraint is constructed from three offer a more reliable means for testing a control circuit than qualified conditions: a fulfilling condition which defines a is afforded with simulation, together with a greater speed required or assumed event, an enabling condition which de- translation rule for each possible format. All the possibleformats are stored in a “format library” named QRY.h andFormalCheck performs the translation by invoking the ap-propriate format, instantiating each of its Boolean parame-ters with the respective user-provided condition for whichit is substituted, and writing out the resulting automaton inthe input language of COSPAN.
All queries (properties and constraints) are constructed the automata models generated by the queries conform tothe intentions of the designers who formulate the queries.
This note describes how we have tested this conformanceand established a regression test for the query automaton-generation mechanism by establishing a second unrelatedautomaton generator for queries, and a means to test thatthe respective automata generated by FormalCheck and thesecond generator are equivalent.
The second automaton generator starts with the En- glish language query idiom supported by the FormalCheckgraphical interface. The plan was to (hand-)translate eachproperty and constraint format into a parameterized for-mula of linear-time temporal logic (LTL) [VW86, Eme90], Figure 1: The FormalCheck Property panel.
a logic well-suited for capturing temporal behavior. Theseformulas then could be translated into automata using analgorithm [GPVW95] developed for that purpose and im- fines a precondition for starting the check of the fulfilling plemented into the SPIN verification tool [Hol91, HP96].
condition, and finally, a discharging condition, after which The implementation in SPIN was augmented in order to the fulfilling condition no longer is required or assumed. An generate automata in the input language of COSPAN. Hav- ing done this, an algorithm in COSPAN could be used tocheck the equivalence of each pair of automata: one gen- erated by FormalCheck and the other generated by SPIN.
Although the automata are parameterized by the respective Boolean conditions, it suffices to treat each Boolean condi-tion as an independent Boolean input read by each of the which defines a property that requires a BusRequestFlag two automata. In this way, the equivalence of any pair of to remain high after a BusRequest event, until a BusGrant automata could be checked once and for all, for any instan- event. This behavior is required ad infinitum, whenever the Interestingly, it soon was discovered that virtually none In this example, the three qualifiers After, Always and of the automata formats in QRY.h could be translated into mediate the effect of the enabling, fulfilling and dis- LTL. It is generally known that the expressive power of LTL charging conditions, respectively. This property would be- is strictly weaker than that of automata [Eme90], and as it come a constraint by changing the Always qualifier to As-sumeAlways happens, this fact is exemplified by most of the automata of QRY.h (as was proved formally [Kup96, Wil96]). The In general, each condition is a Boolean parameter and particular reason the QRY.h automata cannot be translated into LTL lies in the “phase” nature of the QRY.h format: LTL is incapable of keeping track of whether the particu- lar automaton is in the phase where the fulfilling condition is required to hold, or not. However, this phase is imple-mented by a very simple 2-state machine: starting in state format of the example gets translated into a parameterized 0, it moves to state 1 when the enabling condition becomes automaton whose parameters are the respective conditions.
true, and moves back to state 0 when the discharging con- Once the user has defined a query, FormalCheck trans- dition becomes true. Referring to the state of this PHASE lates that query into an automaton against which COSPAN machine, each QRY.h format then could be translated into checks the circuit model. The translation follows a separate LTL, and this was done. The rest of the test was carried out respectively. In the later case, it is not required that it stays As a technical point, it should be noted that all the au- true the first time it becomes true.
The enabling condition qualifier IfRepeatedly is sup- Kur94]. These are finite-state automata which define non- ported only with the fulfilling condition qualifiers Eventu- terminating behaviors, accepting (infinite) sequences of let- ally and AssumeEventually. With the first, the resulting ters rather than (finite) strings as do conventional automata.
property is called “strong liveness” while with the second, There are many similarities (and some crucial differences) the resulting constraint is called “strong fairness”. On ac- between the two classes of automata.
count of the ability to express strong fairness together withany finite state machine (which may be implemented by asufficient number of copies of the PHASE machine), the au- The Query Format Library QRY.h
tomata of QRY.h are capable of expressing any property [Kur94]. The -regular properties form the largest Each property and each constraint format in QRY.h has a class of properties expressible with finite state automata.
fulfilling condition and an optional enabling condition and Each property/constraint pair (formats which differ only an optional discharging condition. The query format sup- by the Assume) define automata which accept complemen- ports two qualifiers for enabling conditions: tary languages. Thus, another check on the validity of the QRY.h library is to check this requirement with COSPAN, as well. This additional check also was performed.
Thus, the validity of QRY.h was tested by the following and two main qualifiers for discharging conditions: equivalence of each QRY.h automaton with the corre-sponding LTL+Phase formula the difference being that Until requires that the dischargingcondition eventually become true, whereas with Unless, respective property automaton/constraint automaton discharge is not mandatory. Each discharging qualifier also A script was written to invoke COSPAN to perform each check for each parameterized automaton, in succession.
This script is used to perform regression tests on QRY.h if which requires fulfillment at discharge: the fulfilling con- any changes are made to its elements. In fact, more efficient dition must be true at the instant the discharging condition implementations for some of the QRY.h automata were sub- becomes true (but may become false thereafter).
sequently discovered, and these were tested using the test For properties, the fulfilling condition has two “safety” The QRY.h library and the COSPAN and SPIN tools are freely available to Lucent Technologies employees.
For QRY.h and COSPAN, requests should be addressed to k@research.bell-labs.com. For SPIN, requests shouldbe addressed to gerard@research.bell-labs.com. The FormalCheck tool is available under arrangement from Ad- vanced Technologies’ Design Automation Lab. Requests should be addressed to gdepalma@lucent.com.
For constraints, the corresponding qualifiers are Conclusion
A method was devised and implemented to test the va- lidity of the FormalCheck query library QRY.h, by compar- ing two independent implementations using a script which The safety qualifiers define behaviors which may be fal- later served as a regression tester. In the course of the orig- sified by a finite trace, whereas liveness qualifiers define be- inal test, a few typographical errors were found in QRY.h haviors which can be falsified only by an infinite trace. The elements, and were corrected. On account of this test, the liveness qualifiers define behaviors in which the fulfilling anticipated reliability of QRY.h has been enhanced signifi- condition eventually becomes true, or eventually stays true, References
G. DePalma and A. B. Glaser. Formal verifi-cation augments simulation. Electronic Engi-neering Times, pages 56, 66, Jan. 1996.
Handbook of Theoretical Computer Science,Vol B, 1990.
[GPVW95] R. Gerth, D. Peled, M. Vardi, and P. Wolper.
Simple on-the-fly automatic verification of lin-ear temporal logic. In Proceedings ProtocolSpecification Testing and Verification, War-saw, Poland, pages 3–18, 1995.
R. H. Hardin, Z. Har’El, and R. P. Kurshan.
COSPAN.
Computer Protocols. Prentice Hall, 1991.
G. J. Holzmann and D. Peled. The State ofSPIN. In Proc. CAV’96, volume 1102, pages385–389. LNCS, 1996.
R. P. Kurshan and Z. Har’El. Software for an-alytical development of communication proto-cols. AT&T Tech. J., 69(1):45–59, 1990.
of Coordinating Processes : The Automata-Theoretic Approach.
M. Y. Vardi and P. Wolper. An automata the-oretic approach to automatic program verifi-cation. In IEEE Logic In Computer Science,1986.
T. Wilke. personal correspondence, 1996.

Source: http://spinroot.com/gerard/pdf/qry.pdf