Standard-cell design has always been a craft, and common field-effect transistors
span only a small design space.
This has changed with reconfigurable transistors.
Boolean functions that exhibit multiple dual product-terms in their sum-of-product
form yield various beneficial circuit implementations with
reconfigurable transistors.
In this work, we present an approach to automatically generate these implementations
through a formal modeling approach.
Using the 3-input XOR function as an example, we discuss the variations and
show how to quantify properties like worst-case delay and power
dissipation, as well as averages of delay and energy consumption per operation
over different scenarios.
The quantification runs fully automated on charge transport network models
employing probabilistic model checking.
This yields exact results instead of approximations obtained from experiments and sampling.
The highlight of our work is that the proposed approach provides a comprehensive
early technology evaluation flow.