Formal Analysis of SystemC Designs in Process Algebra

• Autorzy: Hojjat H. , Mousavi M. R. , Sirjani M.
• Języki publikacji: EN

Abstrakty

EN

SystemC is an IEEE standard system-level language used in hardware/software co-design and has been widely adopted in the industry. This paper describes a formal approach to verifying SystemC designs by providing a mapping to the process algebra mCRL2. Our mapping formalizes both the simulation semantics as well as exhaustive state-space exploration of SystemC designs. By exploiting the existing reduction techniques of mCRL2 and also its model-checking tools, we efficiently locate the race conditions in a system and resolve them. A tool is implemented to automatically perform the proposed mapping. This mapping and the implemented tool enabled us to exploit process-algebraic verification techniques to analyze a number of case-studies, including the formal analysis of a single-cycle and a pipelined MIPS processor specified in SystemC.

Słowa kluczowe

EN

SystemC; process algebras; formal verification; mCRL2

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 107, nr 1
• Strony: 19--42
• Opis fizyczny: Bibliogr. 37 poz., tab., wykr.

Twórcy

autor

Hojjat H.

autor

Mousavi M. R.

autor

Sirjani M.

• Department of Computer Science, TU/Eindhoven, P.O. Box 513, Eindhoven, NL-5600MB, The Netherlands,

Bibliografia

• [1] 1666-2005, IEEE SystemC LRM, available at www.systemc.org, 2005.
• [2] Baeten J. C. M., Basten T., and Reniers M. A.: "Process Algebra: Equational Theories of Communicating Processes", Cambridge, 2010.
• [3] Behjati R., Sabouri H., Razavi N., and Sirjani M.: "An effective approach for model checking SystemC designs.", Proc. of ACSD'08, pp. 56-61, IEEE CS, 2008.
• [4] Black D.C., Donovan J.: "SystemC: From the Ground Up", Kluwer Academics, 2005.
• [5] Blanc N., Kroening D.: "Speeding Up Simulation of SystemC Using Model Checking", Proc. of SBMF'09, vol. 5902 of LNCS, pp. 1-16, Springer, 2009.
• [6] Burch J.R. and Dill D.L.: "Automatic verification of pipelined microprocessor control.", Proc. of CAV'94, vol. 818 of LNCS, pp. 68-80, Springer, 1994.
• [7] Brock B., Kaufmann M. and Moore J.S.: "ACL2 theorems about commercial microprocessors." Proc. Of FMCAD'96, pp. 275-293, IEEE CS, 1996.
• [8] Campbell C., GrieskampW., Nachmanson L., SchulteW., Tillmann N., and VeanesM.: "Model-based testing of object-oriented reactive systems with Spec Explorer." Technical Report MSR-TR-2005-59,Microsoft Research, 2005.
• [9] Fernandez J.-C., Garavel H., Kerbrat A., Mounier L., Mateescu R., and Sighireanu M.: "CADP - a protocol validation and verification toolbox." Proc. of CAV'96, pp. 437-440, 1996.
• [10] Gurevich Y., Rossman B., and Schulte W.: "Semantic essence of AsmL." Theoretical Computer Science, 343(3):370-412, 2005.
• [11] Ghenassia F.: "Transaction-level modeling with Systemc: TLM concepts and applications for embedded systems." Springer, 2006.
• [12] Große D. and Drechsler R.: "Formal verification of LTL formulas for SystemC designs." Proc. of ISCAS'03, pp. V-245-248, IEEE, 2003.
• [13] Groote J.F. and Ponse A.: "The syntax and semantics of μCRL, Proc. of ACP'94, pp. 26-62, 1995.
• [14] Groote J.F., Mathijssen A., Reniers M., Usenko Y., and van Weerdenburg M.: "The formal specification language mCRL2." Proc. of Dagstuhl'07, 2007. www.mcrl2.org.
• [15] Habibi A., and Tahar S.: "An approach for the verfication of SystemC designs using AsmL." Proc. Of ATVA'05, vol. 3707 of LNCS, pp. 69-83, Springer, 2005.
• [16] Hennessy J.L. and Patterson D.A.: "Computer architecture: A quantitative approach." 4th Ed., Morgan Kaufmann, 2006.
• [17] Herber P., Fellmuth J. and Glesner S. : "Model checking SystemC designs using timed automata", Proc. Of CODES/ISSS'08, pp. 131-136, ACM Press, 2008.
• [18] Hojjat H., Sirjani M. and Mousavi, M.R.: Process algebraic verification of SystemC codes. Proc. Of ACSD'08, pp. 62-67, IEEE CS, 2008.
• [19] Hojjat H., Sirjani M., Mousavi, M.R. and Groote J.F.: Sarir: A Rebeca to mCRL2 Translator (Tool Paper). Proc. of ACSD'07, pp. 216-222, IEEE CS, s2007.
• [20] Holzmann G.J.: "The Spin Model Checker - Primer and Reference Manual." Addison-Wesley, 2003.
• [21] Karlsson D., Eles O., and Peng Z.: "Formal verification of SystemC designs using a Petri-Net based representation." Proc. of DATE'06, pp. 1228-1233, ACM Press, 2006.
• [22] Keutzer K., Malik S., Newton R., Rabaey J. and Sangiovanni-Vincentelli A.: "System level design: orthogonalization of concerns and platform-based design." IEEE TCAD, 19(12):1523-1543, 2000.
• [23] Kroening D., and Sharygina N.: "Formal verification of SystemC by automatic hardware/software partitioning." Proc. of MEMOCODE'05, pp. 101-110, IEEE CS, 2003.
• [24] Larsen K.G., Pettersson P. and Yi W.: "Uppaal in a nutshell", Journal on Software Tools for Technology Transfer (STTT), 1(1-2): 134-152, 1997.
• [25] Man K.L: "SystemCFL : a formalism for hardware/software co-design." Proc. of ECCTD'05, pp. 193-196, IEEE, 2005.
• [26] Moy M., Maraninchi F., and Maillet-Contoz L.: "LusSy: A toolbox for the analysis of systems-on-a-chip at the transactional level." Proc. of ACSD'05, pp. 26-35, IEEE CS, 2005.
• [27] Müller W., Ruf J., and Rosenstiel W.: "An ASM based systemC simulation semantics." Chapter 4 of SystemC: methodologies and applications, pp. 97-126, Kluwer, 2003.
• [28] Panda P.R.: "SystemC: a modeling platform supporting multiple design abstractions." Proc. of ISSS'01, pp. 75-80, ACM Press, 2001.
• [29] Patel H.D., and Shukla S.K.: "Model-driven validation of SystemC designs." Proc. of DAC'07, pp. 29-34, IEEE, 2007.
• [30] Raffelsieper M., Mousavi M.R., Roorda J.-W., Strolenberg C. and Zantema H.: "Formal Analysis of Non-Determinism in Verilog Cell Library Simulation Models." Proc. of FMICS'09, pp. 133-148, 2009
• [31] Razavi N., Behjati R., Sabouri H. , Khamespanah E., Shali A., and SirjaniM.: "Sysfier: Actor-based Formal Verification of SystemC", ACM Transactions on Embedded Computing Systems, 2010. To appear.
• [32] Sirjani M., Movaghar A., Shali A., and de Boer F.S.: "Modeling and verification of reactive systems using Rebeca." Fundamenta Informaticae, 63(4):385-410, 2004.
• [33] Srinivasan S.K., and Velev M.N.: "Formal verification of an Intel XScale processor model with scoreboarding, specialized execution pipelines, and impress data-memory exceptions." Proc. of MEMOCODE'03, pp. 65-74, IEEE CS, 2003.
• [34] SystemC to mCRL2 toolkit, http://www.win.tue.nl/~mousavi/sysc08/.
• [35] Traulsen C., Cornet J., Moy M. and Maraninchi F.: "A SystemC/TLMsemantics in Promela and its possible applications." Proc. of SPIN'07, vol. 4595 of LNCS, pp. 204-222, Springer, 2007.
• [36] Velev M.N. and Bryant R.E.: "Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors." J. Symb. Comput. 35(2):73-106, 2003.
• [37] VardiM.Y.: "Formal techniques for SystemC verification.", Proc. of DAC'07, pp. 188-192, IEEE CS,