arXiv.itsnick.co

an independent field guide to 23 million papers from arXiv & OpenAlex — not affiliated with arXiv.org

Author

Marc Messing

2 papers · 2008–2009

2008: 12009: 1
2008peak 1 in 20082009

Frequent co-authors

Papers

showing 1–2 of 2 RSS

Identifying a Subset of System Verilog Assertions for Efficient Bounded Model Checking

Robert Wille, Görschwin Fey, Marc Messing +3 more

Computational Theory and Mathematics · · cited 6× · DOI ↗ · more like this ·

Integrating design and verification becomes more and more important due to the increasing complexity of today's circuits and systems. SystemVerilog is a description language that embeds verification goals with the help of SystemVerilog assertions (SVAs). Often SVAs are used in simulation-based verification. But in the past first applications in formal verification have been considered, too. In this paper we present an approach to prove SVAs by induction based bounded model checking (BMC). Since checking SVAs is computationally very complex, we define a subset which is sufficient for many practical purposes. For each restriction a rationale is given.The creation of the BMC instance for this subset is explained in detail. Case studies show the application of our approach.

Using a two-dimensional fault list for compact Automatic Test Pattern Generation

Marc Messing, Andreas Glowatz, Friedrich Hapke +1 more

Hardware and Architecture · · cited 4× · DOI ↗ · more like this ·

Automatic Test Pattern Generation (ATPG) is one of the core algorithms in testing of digital circuits and systems. Based on a given fault model a list of all faults to be tested, i.e. the fault list, is being created. For each fault in this list, one test pattern is generated (this pattern may cover other faults). Thereby, the order of the faults is crucial. In industrial ATPG, typically a simple list is used as fault list until today. In this work, we introduce a two-dimensional fault list and different strategies to order this list. The target is to reduce the number of generated patterns. The techniques are implemented in an industrial ATPG-framework. They are evaluated on industrial circuits. The results are discussed and a general purpose strategy is given.