Advertisement

Symbolic Checking of Signal-Transition Consistency for Verifying High-Level Designs

  • Kiyoharu Hamaguchi
  • Hidekazu Urushihara
  • Toshinobu Kashiwabara
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1954)

Abstract

This paper deals with verification of high-level designs, in particular, symbolic comparison of register-transfer-level descriptions and behavioral descriptions. As models of those descriptions, we use state ma- chines extended by quantifier-free first-order logic with equality. Since the signals in the corresponding outputs of such descriptions rarely change simultaneously, we cannot adopt the classical notion of equivalence for state machines. This paper defines a new notion of consistency based on signal-transitions of the corresponding outputs, and proposes an algo- rithm for checking consistency of those descriptions, up to a limited num- ber of steps from initial states. A simple hardware/software codesign is taken as an example of high-level designs. A C program for digital signal processing called PARCOR filter was compared with its corresponding design given as a register-transfer-level description, which is composed of a VLIW architecture and assembly code. Since this example terminates within approximately 4500 steps, symbolic exploration of a finite num- ber of steps is sufficient to verify the descriptions. Our prototype verifier succeeded in the verification of this example in 31 minutes.

Keywords

State Machine Model Check Boolean Function Predicate Symbol Assembly Code 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    R. A. Bergamaschi and S. Raje. Observable Time Windows: Verifying The Results of High-Level Synthesis. IEEE Design and Test of Computers, 14(2):40–50, 1997.CrossRefGoogle Scholar
  2. 2.
    R. E. Bryant, S. German, and M. N. Velve. Exploiting positive equality in a logic of equality with uninterpreted functions. In Conference on Computer-Aided Verification, LNCS 1633, pages 470–482, July 1999.Google Scholar
  3. 3.
    J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill. Symbolic Model Checking for Sequential Circuit Verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(4), April 1994.Google Scholar
  4. 4.
    J. R. Burch and D. L. Dill. Automatic Verification of Pipelined Microprocessor Control. In Proceedings of International Conference on Computer-Aided Design, pages 68–80, June 1994.Google Scholar
  5. 5.
    O. Coudert, C. Berthet, and J.-C. Madre. Verification of Sequential Machines Using Boolean Functional Vectors. In Proceedings of the IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, November 1990.Google Scholar
  6. 6.
    D. Cyrluk and P. Narendran. Ground temporal logic: A logic for hardware verification. In Conference on Computer-Aided Verification, LNCS 818, pages 247–259, July 1994.Google Scholar
  7. 7.
    S. Devadas and K. Keutzer. An Automata-Theoretic Approach to Behavioral Equivalence. In Proc. of ICCAD, pages 30–33, 1990.Google Scholar
  8. 8.
    M. Genoe, L. Claesen, E. Verlind, F. Proesmans, and H. De Man. Illustration of the SFG-Tracing Multi-Level Behavioral Verification Methodology, by the Correctness Proof of a High to Low Level Synthesis Application in CATHEDRAL-II. In Proc. of IEEE International Conference on Computers and Design, pages 338–341, 1991.Google Scholar
  9. 9.
    M. Genoe, L. Claesen, E. Verlind, F. Proesmans, and H. De Man. Automatic Formal Verification of Cathedral-II Circuits from Transistor Switch Level Implementations up to High Level Behavioral Specifications by the SFG-Tracing Methodology. In Proc. of European Conference on Design Automation (EDAC-92), pages 16–19, 1992.Google Scholar
  10. 10.
    J. L. Henny and D. A. Paterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann, 1990.Google Scholar
  11. 11.
    R. Hojati, A. Isles, D. Kirkpatrick, and R. K. Brayton. Verification using uninterpreted functions and finite instantiations. In Formal Methods in Computer-Aided Design, LNCS 1166, pages 218–232, November 1996.CrossRefGoogle Scholar
  12. 12.
    M. Imai, Y. Takeuchi, N. Ohtsuki, and N. Hikichi. Compiler Generation Techniques for Embedded Processors and Their Application to HW/SW Codesign. In Ahmed A. Jerraya and Jean Mermet, editors, System-Level Synthesis, pages 293–320. Kluwer Academic Publishers, 1999.Google Scholar
  13. 13.
    R. B. Jones, D. L. Dill, and J. R. Burch. Efficient Validity Checking for Processor Verification. In Proceedings of International Conference on Computer-Aided Design, pages 2–6, November 1995.Google Scholar
  14. 14.
    N. Mansouri and R. Vemuri. A Methodology for Automated Verification of Syn-thesized RTL Designs and Its Integration with a High-Level Synthesis Tool. In Formal Methods in Computer-Aided Design (FMCAD 98), pages 204–221, 1998.Google Scholar
  15. 15.
    G. Nelson and D. C. Oppen. Simplification by Cooperating Decision Procedure. ACM Trans. on Programming Languages and Systems, 1(2):245–257, 1979.zbMATHCrossRefGoogle Scholar
  16. 16.
    R. E. Shostak. A Practical Decision Procedure for Arithmetic with Function Symbols. Journal of ACM, 26(2):351–360, 1979.zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    Y. Xu, E. Cerny, X. Song, F. Corella, and O. Ait Mohamed. Model checking for a first-order temporal logic using multiway decision graphs. In Conference on Computer-Aided Verification, LNCS 1427, pages 219–231, July 1998.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Kiyoharu Hamaguchi
    • 1
  • Hidekazu Urushihara
    • 1
  • Toshinobu Kashiwabara
    • 1
  1. 1.Dept. of Informatics and Mathematical Science, Graduate School of Engineering ScienceOsaka University ToyonakaOsakaJapan

Personalised recommendations