Tutorial: How to Use Model Checking to Analyze Circuits at the Transistor Level

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.