| Title | Constraint-Based Platform Variants Specification for Early System Verification |
| Author | *Andreas Burger, Alexander Viehl, Andreas Braun (FZI Research Center for Information Technology, Germany), Finn Haedicke (solvertec/University of Bremen, Germany), Daniel Große (solvertec, Germany), Oliver Bringmann, Wolfgang Rosenstiel (FZI Research Center for Information Technology/University of Tübingen, Germany) |
| Page | pp. 800 - 805 |
| Keyword | Specification, Language, System-level modeling, Verification |
| Abstract | To overcome the verification gap arising from significantly increased external IP integration and reuse during electronic platform design and composition, we present a model-based approach to specify platform variants. The variants specification is processed automatically by formalizing and solving the integrated constraint sets to derive valid platforms. These constraint sets enable a precise specification of the required platform variants for verification, exploration and test. Experimental results demonstrate the applicability, versatility and scalability of our novel model-based approach. |
| Slides |
| Title | A Transaction-Oriented UVM-Based Library for Verification of Analog Behavior |
| Author | *Alexander Wolfgang Rath, Volkan Esen, Wolfgang Ecker (Infineon Technologies AG, Germany) |
| Page | pp. 806 - 811 |
| Keyword | UVM, analog, mixed signal, transaction, RNM |
| Abstract | The Universal Verification Methodology (UVM) has
become a de facto standard in today’s functional verification of
digital designs. However, it is rarely used for the verification
of Designs Under Test containing Real Number Models. This
paper presents a new technique using UVM that can be used in
order to compare models of analog circuitry on different levels
of abstraction. It makes use of statistic metrics. The presented
technique enables us to ensure that Real Number Models used
in chip projects match the transistor level circuitry during the
whole life cycle of the project. |
| Slides |
| Title | Automata-Theoretic Modeling of Fixed-Priority Non-Preemptive Scheduling for Formal Timing Verification |
| Author | *Matthias Kauer, Sebastian Steinhorst (TUM CREATE, Singapore), Reinhard Schneider (TU Munich, Germany), Martin Lukasiewycz (TUM CREATE, Singapore), Samarjit Chakraborty (TU Munich, Germany) |
| Page | pp. 812 - 817 |
| Keyword | CAN, Formal Verification, Model Checking, Timing Analysis, FPNS |
| Abstract | The design process of safety-critical systems requires formal analysis methods to ensure their correct functionality without over-sized safety margins and extensive testing.
For architectures with state-based events or scheduling, such as load-dependent frequency scaling, model checking has emerged as a promising tool.
It formally verifies timing behavior of real-time systems with minimal over-approximation of the worst case delays.
In this context, ECA have become a valuable modeling approach because they are specifically designed to handle typical arrival patterns and integrate well with analytic techniques.
In this work, we propose an extension of the ECA framework's semantics and use it in a FPNS model that correctly abstracts the intra-slot behavior in the slotted-time model of the ECA.
This is challenging because straightforward implementations cannot capture the full behavior of event-triggered scheduling with such a time model that the ECA shares with most model checking based methods.
In a case study, we obtain bounds via model checking a basic model and then our proposed model.
We compare these bounds with a SystemC simulation.
This shows that the bounds from the basic model are too optimistic -- and exceeded in practice -- because it does not capture the full behavior, while the bounds from the proposed extended model are both safe and reasonably tight. |