Abstract
We describe a framework for dynamic verification of temporal assertions based on assertion compilation into deterministic automata. The novelty of our approach is that it allows efficient dynamic verification of general linear temporal formulas written in formal property specification languages such as LTL, ForSpec, PSL, and SVA, while the existing approaches are applicable to limited subsets only. We also show an advantage of the described framework over industrial simulators, which typically use transaction-based verification. Another advantage of our approach is its ability to use deterministic checkers directly for hardware emulation. Finally, we compare the deterministic compilation with the OBDD-based on-the-fly simulation of deterministic automata. We show that although the OBDD-based simulation method is much slower, the two methods may be efficiently combined for hybrid simulation, when the RTL signals in assertions are mixed with symbolic variables.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abarbanel, Y., Beer, I., Gluhovsky, L., Keidar, S., Wolfstal, Y.: FoCs - automatic generation of simulation checkers from formal specifications. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 538–542. Springer, Heidelberg (2000)
Albin, K., et al.: Property specification language reference manual. Technical Report Version 1.1, Accellera (2004)
Armoni, R., Bustan, D., Kupferman, O., Vardi, M.Y.: Resets vs. aborts in linear temporal logic. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 65–80. Springer, Heidelberg (2003)
Armoni, R., Egorov, S., Fraer, R., Korchemny, D., Vardi, M.Y.: Efficient LTL compilation for SAT-based model checking. In: Proc. Int’l Conf. on Computer-Aided Design, pp. 877–884 (2005)
Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: The ForSpec temporal logic: A new temporal property-specification logic. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 211–296. Springer, Heidelberg (2002)
Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Program monitoring with LTL in EAGLE. In: Proc. 18th Int’l Parallel and Distributed Processing Symp. IEEE Computer Society Press, Los Alamitos (2004)
Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic Sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 363–367. Springer, Heidelberg (2001)
Bening, L., Foster, H.: Principles of verifiable RTL design – a functional coding style supporting verification processes. Springer, Heidelberg (2001)
Bentley, B.: High level validation of next-generation microprocessors. In: Proc. IEEE Int’l Workshop on High Level Design Validation and Test, pp. 31–35 (2002)
Bergeron, J., Cerny, E., Hunter, A., Nightingale, A.: Verification Methodology Manual for SystemVerilog. Springer, Heidelberg (2005)
Biesse, P., Leonard, T., Mokkedem, A.: Finding bugs in an alpha microprocessor using satisfiability solvers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 454–464. Springer, Heidelberg (2001)
Boule, M., Zilic, Z.: Incorporating efficient assertion checkers into hardware emulation. In: Proc. 23rd Int’l Conf. on Computer Design, pp. 221–228. IEEE Computer Society Press, Los Alamitos (2005)
Bryant, R.E.: Graph-based algorithms for boolean-function manipulation. IEEE Trans. on Computers C-35(8) (1986)
Bustan, D., Flaisher, A., Grumberg, O., Kupferman, O., Vardi, M.Y.: Regular vacuity. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 191–206. Springer, Heidelberg (2005)
Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. Journal of the Association for Computing Machinery 28(1), 114–133 (1981)
Chang, K.H., Tu, W.T., Yeh, Y.J., Kuo, S.Y.: A simulation-based temporal assertion checker for PSL. In: Proc. 46th IEEE Int’l Midwest Stmp. on Circuits and Systems, pp. 1528–1531. IEEE Computer Society Press, Los Alamitos (2003)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Cohen, B.: Using PSL/Sugar with Verilog and VHDL, Guide to Property Specification Language for ABV. Addison-Wesley, Reading (2003)
Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.Y.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 436–453. Springer, Heidelberg (2001)
d’Amorim, M., Rosu, G.: Efficient monitoring of omega-languages. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 364–378. Springer, Heidelberg (2005)
Daniele, N., Guinchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 249–260. Springer, Heidelberg (1999)
Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003)
Emerson, E.A.: Temporal and modal logic. In: Van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, ch.16, vol. B, pp. 997–1072. Elsevier, MIT Press (1990)
Etessami, K., Holzmann, G.J.: Optimizing Büchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 153–167. Springer, Heidelberg (2000)
Finkbeiner, B., Sipma, H.: Checking finite traces using alternating automata. Electr. Notes Theor. Comput. Sci. 55(2) (2001)
Fisman, D.: The Subset of Linear Violation.The Weizmann Institute of Science, IBM Haifa Research Lab (2005)
Geilen, M.: On the construction of monitors for temporal logic properties. Electr. Notes Theor. Comput. Sci. 55(2) (2001)
Gheorghita, S.V., Grigore, R.: Constructing checkers from PSL properties. In: Proc. 15th Int’l Conf. on Control Systems and Computer Science, vol. 2, pp. 757–762 (2005)
Giannakopoulou, D., Havelund, K.: Automata-based verification of temporal properties on running programs. In: Proc. 16th International Conference on Automated Software Engineering, pp. 412–416. IEEE Computer Society, Los Alamitos (2001)
Hoffmann, D.W., Ruf, J., Kropf, T., Rosenstiel, W.: Simulation meets verification: Checking temporal properties in SystemC. In: Proc. 26th EUROMICRO 2000 Conference, p. 1435. IEEE Computer Society, Los Alamitos (2000)
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)
Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal methods in System Design 19(3), 291–314 (2001)
Latvala, T.: Efficient model checking of safety properties. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 74–88. Springer, Heidelberg (2003)
Miyano, S., Hayashi, T.: Alternating finite automata on ω-words. Theoretical Computer Science 32, 321–330 (1984)
Pidan, D., Keider-Barner, S., Moulin, M., Fisman, D.: Optimized algorithms for dynamic verification. Technical Report FP6-IST-507219, PROSYD (2005)
Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. on Foundation of Computer Science, pp. 46–57 (1977)
Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000)
Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996)
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st Symp. on Logic in Computer Science, Cambridge, pp. 332–344 (June 1986)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)
Vijayaraghavan, S., Ramanathan, M.: A Practical Guide for SystemVerilog Assertions. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Armoni, R., Korchemny, D., Tiemeyer, A., Vardi, M.Y., Zbar, Y. (2006). Deterministic Dynamic Monitors for Linear-Time Assertions. In: Havelund, K., Núñez, M., Roşu, G., Wolff, B. (eds) Formal Approaches to Software Testing and Runtime Verification. FATES RV 2006 2006. Lecture Notes in Computer Science, vol 4262. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11940197_11
Download citation
DOI: https://doi.org/10.1007/11940197_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-49699-1
Online ISBN: 978-3-540-49703-5
eBook Packages: Computer ScienceComputer Science (R0)