Complexity of Hardware Design and Model-Checking: An Asymptotic Analysis of State-Machine MetricsSuleiman Abu Kharmeh, Kerstin Eder, David May, Complexity of Hardware Design and Model-Checking: An Asymptotic Analysis of State-Machine Metrics. CSTR-12-002, University of Bristol. March 2012. PDF, 598 Kbytes.
The investigation of viable and objective hardware system complexity formulas is discussed in this paper. The definition of State Space Complexity and Communication Space Complexity are specified in terms of underlying hardware system metrics. This enables the quantification of the State Space Explosion problem. In addition, it enables the identification and subsequent quantification of a Communication Space Explosion phenomenon. A detailed case study is presented to show how such formulas can be developed through the use of current model-checking tools coupled with automated equation solving techniques. This involved the analysis of the complexity and scalability of the model-checking tool itself (namely FDR) in handling exponentially growing complex systems.