Towards formal evaluation and verification of probabilistic design

In the nanometer regime of integrated circuit fabrication, device variability imposes serious challenges to the design of reliable systems. A new computation paradigm of approximate and probabilistic design has been proposed recently to accept design imperfection as a resource for certain applications. Despite recent intensive study on approximate design, probabilistic design receives relatively few attentions. This paper provides a general formulation for the evaluation and verification of probabilistic design. We establish its connection to stochastic Boolean satisfiability (SSAT), (weighted) model counting, signal probability calculation, and probabilistic model checking. A comparative experimental study is performed to contrast the strengths and weaknesses of different solutions. Our study can be an essential step towards automated synthesis of probabilistic design.