Multiway Decision Graphs (MDGs) have recently been proposed as an efficient representation for RTL designs. In this paper, we illustrate the MDG-based formal verification technique on the example of the Island Tunnel Controller. We investigate several techniques on how to deal with the nontermination problem of abstract state exploration, including a novel method based on retiming and circuit transformation. We provide comparative experimental results for the verification of a number of properties for the example using two well-known ROBDD-based verification tools, namely, SMV (Symbolic Model Verifier) and VIS (Verification Interacting with Synthesis), and we show the strength of the MDG approach to handling arbitrary data widths.

Keywords:

References

R. E. Bryant, IEEE Trans. Comput. 35, 677 (1986). Web of Science, Google Scholar
J. R. Burchet al., IEEE Trans. Computer-Aided Design 13, 401 (1994). Crossref, Web of Science, Google Scholar
O. Coudert , C. Berthet and J. C. Madre , Automatic Verification Methods for Finite State Systems , Lecture Notes in Computer Science 407 , ed. J. Sifakis ( Springer-Verlag , 1989 ) . Google Scholar
E. M. Clarke, O. Grumberg and D. E. Long, Model checking and abstraction, Proc. 19th ACM Symp. Principles of Programming Languages, January 1992 . Google Scholar
D. E. Long, Model checking, abstraction and compositional verification, PhD thesis, Carnegie Mellon University (1993) . Google Scholar
R. E. Bryant and Y. Chen, Verification of arithmetic circuits with binary moment diagrams, 32nd ACM/IEEE Design Automation Conf. (DAC '95), San Francisco, California, June 1995 . Google Scholar
E. Clarke, M. Fujita and X. Zhao, Hybrid decision diagrams, Proc. IEEE Int. Conf. Computer-Aided Design (ICCAD '95), San Jose, California, USA, November 1995 . Google Scholar
F. Corellaet al., Formal Meth. Syst. Design 10, 7 (1997). Crossref, Web of Science, Google Scholar
J. R. Burch and D. L. Dill , Proc. Work. on Computer-Aided Verification , Lecture Notes in Computer Science 818 , ed. D. L. Dill ( Springer-Verlag , 1994 ) . Google Scholar
D. Cyrluk and P. Narendran , Computer Aided Verification , Lecture Notes in Computer Science 818 , ed. D. L. Dill ( Springer-Verlag , 1994 ) . Google Scholar
F. Corella, M. Langevin, E. Cerny, Z. Zhou and X. Song, State enumeration with abstract descriptions of state machines, Proc. IFIP WG 10.5 Advanced Research Working Conf. Correct Hardware Design and Verification Methods (CHARME '95), Frankfurt, Germany, October 1995 . Google Scholar
R. B. Jones and D. L. Dill, Efficient validity checking for processor verification, Proc. IEEE Int. Conf. Computer-Aided Design (ICCAD '95), San Jose, California, USA, November 1995 . Google Scholar
K. Fisler and K. Johnson, Integrating design and verification environment through a logic supporting hardware diagrams, Proc. IFIP Conf. Hardware Description Languages and Their Applications (CHDL '95), Chiba, Japan, August 1995 . Google Scholar
K. D. Anon, N. Boulerice, E. Cerny, F. Corella, M. Langevin, X. Song, S. Tahar, Y. Xu and Z. Zhou, MDG tools for the verification of RTL designs, Proc. 8th Int. Conf. Computer-Aided Verification (CAV '96), New Brunswick, New Jersey, USA, July 1996 . Google Scholar
C. Leiserson and J. Saxe, Algorithmica 6, 5 (1991). Crossref, Web of Science, Google Scholar
K. L. McMillan , Symbolic Model Checking ( Kluwer Academic Publishers , Boston, Massachusetts , 1993 ) . Crossref, Google Scholar
R. K. Brayton et al. , Technical Report UCB/ERL M95 ( Electronics Research Laboratory, University of California , Berkeley , 1995 ) . Google Scholar
M. Langevin, S. Tahar, Z. Zhou, X. Song and E. Cerny, Behavioral verification of an ATM switch fabric using implicit abstract state enumeration, Proc. Int. Conf. Computer Design (ICCD '96), Austin, Texas, USA, October 1996 . Google Scholar
S. Tahar et al. , Proc. Great Lakes Symp. VLSI (GLS-VLSI '96) ( IEEE Computer Society Press , Iowa, USA , 1996 ) . Google Scholar
O. Aït Mohamed , X. Song and E. Cerny , Proc. IFIP W 10.5 Advanced Research Working Conf. Correct Hardware Design and Verification Methods (CHARME '97) ( IFIP, Chapmann & Hall , Montréal , 1997 ) . Google Scholar