2005 · 116 citations · 21 references
Hardware ModelingEngineeringHardware Verification LanguageVerificationComputer ArchitectureComputer-aided VerificationSoftware EngineeringSystem-level DesignSoftware AnalysisHardware SystemsFormal VerificationSoftware PartsHardware Verification LanguagesFlexible PartitioningArchitecture Description LanguageSystems EngineeringProgramming LanguagesHardware VerificationRuntime VerificationUniform System DescriptionComputer EngineeringComputer ScienceSoftware DesignSoftware VerificationProgram AnalysisFormal MethodsSystem SoftwareSystem Specification
SystemC and similar system-level languages are increasingly used to describe designs that combine hardware and software, enabling flexible partitioning, but many properties depend on the hardware/software interaction and existing tools either use non‑formal methods or only address low‑level language parts. The paper proposes a technique that simultaneously handles both hardware and software parts of a system description. The technique automatically partitions a uniform SystemC description into synchronous hardware and asynchronous software components, and has been implemented and tested on several industrial examples. The partitioning improves verification performance relative to a monolithic approach.
Variants of general-purpose programming languages, like SystemC, are increasingly used to specify system designs that have both hardware and software parts. The system-level languages allow a flexible partitioning in the design of the hardware and software. Moreover, many properties depend on the combination of hardware and software and cannot be verified on either part alone. Existing tools either apply non-formal approaches or handle only the low-level parts of the language. This papers presents a new technique that handles both hardware and software parts of a system description. This is done by automatically partitioning the uniform system description into synchronous (hardware) and asynchronous (software) parts. This technique has been implemented and applied to system level descriptions of several industrial examples. The hardware/software partitioning improves the performance of the verification compared to the monolithic approach.
21
E. M. Clarke, Orna Grümberg, D. Long · 1996 · 6.9K citations
Matthew W. Moskewicz, Conor Madigan, Ying Zhao et al. · 2001 · 2.9K citations
Mathematical Programming, Artificial Intelligence, Constraint Solving +14
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar et al. · 2002 · 1.1K citations
Symbolic model checking using SAT procedures instead of BDDs
Armin Biere, Alessandro Cimatti, E. M. Clarke et al. · 1999 · 688 citations
Theory Of Computing, Article Symbolic Model, Engineering +15
Model checking and abstraction
Edmund M. Clarke, Orna Grümberg, David E. Long · 1992 · 348 citations · Full text