Tutorial T3
Title: How to Use Model Checking to Analyze Circuits at the Transistor Level
Abstract: Model checking can be a valuable addition to industry-standard approaches to perform quantitative and qualitative analysis of circuits at the transistor level. The device models are simple yet powerful enough to capture essential electrical characteristics. With its unique approach to formally specify the experimental setup and query quantitative measures, model checking provides you definitive answers to questions about energy consumption, power dissipation and delay properties. With the advent of reconfigurable transistors, systematic investigation and comparison becomes even more important, as reconfigurable logic gates come in different implementations with varying trade-offs. This tutorial will give you a hands-on introduction into the possibilities of investigating logic circuits that use reconfigurable transistors. You will both, design a single circuit graphically, and synthesize a whole family of reconfigurable circuits automatically from a Boolean function. You then analyze their netlist specifications with respect to various properties.
Presenters
Michael Raitza received his Dr.-Ing. in computer science from TU Dresden, Germany, in 2022, for his thesis “Analytical Exploration and Quantification of Nanowire-Based Reconfigurable Digital Circuits”. Since then, he is working as a post-doc researcher at TU Dresden, currently at the Chair of Processor Design. His research interests include hardware architectures, hardware and software design, and programming language design.
Steffen Märcker received his Dr.-Ing. in computer science from TU Dresden, Germany in 2020, for his thesis “Model-Checking Techniques for Design and Analysis of Future Hardware and Software Systems”. He then joined the chair of Processor Design and works on the design and analysis of RFET-based digital circuits. His research interests include probabilistic model checking, formal verification, logics and circuit design.
