×

zbMATH — the first resource for mathematics

Analog property checkers: a DDR2 case study. (English) Zbl 1207.68208
Summary: The formal specification component of verification can be exported to simulation through the idea of property checkers. The essence of this approach is the automatic construction of an observer from the specification in the form of a program that can be interfaced with a simulator and alert the user if the property is violated by a simulation trace. Although not complete, this lighter approach to formal verification has been effectively used in software and digital hardware to detect errors. Recently, the idea of property checkers has been extended to analog and mixed-signal systems.
In this paper, we apply the property-based checking methodology to an industrial and realistic example of a DDR2 memory interface. The properties describing the DDR2 analog behavior are expressed in the formal specification language stl/psl in form of assertions. The simulation traces generated from an actual DDR2 interface design are checked with respect to the stl/psl assertions using the amt tool. The focus of this paper is on the translation of the official (informal and descriptive) specification of two non-trivial DDR2 properties into stl/psl assertions. We study both the benefits and the current limits of such approach.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
FoCs; JPAX; LTL2BA
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abarbanel Y, Beer I, Glushovsky L, Keidar S, Wolfsthal Y (2000) FoCs: automatic generation of simulation checkers from formal specifications. In: Proc CAV’00. LNCS, vol 1855. Springer, Berlin, pp 538–542 · Zbl 0974.68552
[2] Accelera Standard. SystemVerilog 3.1a Language reference manual
[3] Asarin E, Dang T, Frehse G, Girard A, Le Guernic C, Maler O (2006) Recent progress in continuous and hybrid reachability analysis. In: CACSD
[4] Alur R, Etessami K, La Torre S, Peled D (1999) Parametric temporal logic for ”model measuring”. In: ICALP’99, pp 159–168 · Zbl 0939.03021
[5] Alur R, Feder T, Henzinger TA (1996) The benefits of relaxing punctuality. J Assoc Comput Mach 43:116–146 · Zbl 0882.68021
[6] Al Sammane G, Zaki MH, Dong ZJ, Tahar S (2007) Towards assertion based verification of analog and mixed signal designs using PSL. In: FDL’07
[7] Dastidar TR, Chakrabarti PP (2005) Verification system for transient response of analog circuits using model checking. In: VLSID’05, pp 195–200
[8] Drusinsky D (2000) The temporal rover and the ATG rover. In: Proc SPIN’00. LNCS, vol 1885. Springer, Berlin, pp 323–330 · Zbl 0976.68571
[9] Fainekos G, Girard A, Pappas G (2006) Temporal logic verification using simulation. In: Proc FORMATS’06. LNCS, vol 4202. Springer, Berlin, pp 171–186 · Zbl 1141.68463
[10] Gerth R, Peled DA, Vardi MY, Wolper P (1995) Simple on-the-fly automatic verification of linear temporal logic. In: PSTV, pp 3–18
[11] Gastin P, Oddoux D (2001) Fast LTL to Büchi automata translation. In: CAV’01. LNCS, vol 2101. Springer, Berlin, pp 53–65 · Zbl 0991.68044
[12] Havlicek J, Fisman D, Eisner C (2004) Basic results on the semantics of Accelera PSL 1.1 foundation language. In: Technical report 2004.02, Accelera
[13] Hartong W, Hedrich L, Barke E (2002) Model checking algorithms for analog verification. In: DAC’02 · Zbl 1010.68512
[14] Havelund K, Rosu G (2001) Java PathExplorer–a runtime verification tool. In: Proc. ISAIRAS’01
[15] JEDEC Standard. JESD79-2C DDR2 SRAM specification
[16] Jesser A, Lämmermann S, Pacholik A, Weiss R, Ruf J, Fengler W, Hedrich L, Kropf T, Rosenstiel W (2007) Analog simulation meets digital verification–a formal assertion approach for mixed-signal verification. In: SASIMI’07, pp 507–514
[17] Kim M, Lee I, Sammapun U, Shin J, Sokolsky O (2002) Monitoring, checking, and steering of real-time systems. In: Proc. RV’02. ENTCS 70(4)
[18] Little S, Seegmiller N, Walter D, Myers CJ, Yoneda T (2006) Verification of analog/mixed-signal circuits using labeled hybrid petri-nets. In: ICCAD’06, pp 275–282 · Zbl 1108.68511
[19] Maler O, Manna Z, Pnueli A (1992) From timed to hybrid systems. In: Real-time: theory in practice. LNCS, vol 600. Springer, Berlin, pp 447–484
[20] Maler O, Nickovic D (2004) Monitoring temporal properties of continuous signal. In: FORMATS/FTRTFT’04, pp 152–166 · Zbl 1109.68518
[21] Manna Z, Pnueli A (1995) Temporal verification of reactive systems: safety. Springer, Berlin · Zbl 0844.68079
[22] Nickovic D (2008) Checking timed and hybrid properties: theory and practice. PhD thesis · Zbl 1133.68378
[23] Nahhal T, Dang T (2007) Test coverage for continuous and hybrid systems. In: CAV’07, pp 449–462 · Zbl 1135.68346
[24] Nahhal T, Dang T (2007) Guided randomized simulation. In: HSCC’07, pp 731–735
[25] Nickovic D, Maler O (2007) AMT: a property-based monitoring tool for analog systems. In: FORMATS’07, pp 304–319
[26] Somenzi F, Bloem R (2000) Efficient Büchi automata from LTL formulae. In: CAV’00. LNCS, vol 1855. Springer, Berlin, pp 248–263 · Zbl 0974.68086
[27] Steinhorst S, Hedrich L (2008) Model checking of analog systems using an analog specification language. In: DATE’08, pp 324–329
[28] Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification. In: LICS’86, pp 322–331
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.