Blog
About

74
views
0
recommends
+1 Recommend
1 collections
    4
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Building SystemC waiting state automata

      , ,

      Fifth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2011) (VECOS)

      Verification and Evaluation of Computer and Communication Systems (VECoS 2011)

      15-16 September 2011

      SystemC, automata, operational semantics, symbolic execution, compostional verification

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          SystemC is becoming a de facto standard for the system-level description of system-on-chip. However most formal verification techniques used for verifying hardware components targets low level design, usually netlist or RTL, but time-to-market requirements have rushed the industry towards design paradigms that offer a very high level of abstraction. In previous works, we proposed a verification methodology based on SystemC waiting-state automata, an abstract formal model for verifying properties of SystemC at the transaction level within a delta-cycle. The main drawback of thismodel is that it should be providedmanually. In this paper, we propose a method to automatically build the SystemC waiting-state automata from the SystemC code. It is based on an extended symbolic execution of the SystemC design that takes care of synchronous as well as asynchronous communications and that preserves the semantics of SystemC up to a delta-cycle.

          Related collections

          Most cited references 5

          • Record: found
          • Abstract: not found
          • Book Chapter: not found

          Counterexample-Guided Abstraction Refinement

            Bookmark
            • Record: found
            • Abstract: not found
            • Book Chapter: not found

            Construction of abstract state graphs with PVS

              Bookmark
              • Record: found
              • Abstract: not found
              • Article: not found

              Formal Verification of SystemC Designs Using a Petri-Net Based Representation

                Bookmark

                Author and article information

                Contributors
                Conference
                September 2011
                September 2011
                : 1-12
                Affiliations
                UEI, ENSTA, 32 Bd Victor,

                75739 Paris cedex 15, Francewww.ensta-paristech.fr
                CEDRIC, CNAM, 292 rue Saint Martin,

                75141 Paris cedex 03, Francewww.cnam.fr
                Article
                10.14236/ewic/VECOS2011.11
                © Nesrine HARRATH et al. Published by BCS Learning and Development Ltd. Fifth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2011), Tunis, Tunisia

                This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

                Fifth International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2011)
                VECOS
                5
                Tunis, Tunisia
                15-16 September 2011
                Electronic Workshops in Computing (eWiC)
                Verification and Evaluation of Computer and Communication Systems (VECoS 2011)
                Product
                Product Information: 1477-9358 BCS Learning & Development
                Self URI (journal page): https://ewic.bcs.org/
                Categories
                Electronic Workshops in Computing

                Comments

                Comment on this article