High-Level specification and automatic generation of IP interface monitors

ABSTRACT

A central problem in functional verification is to check that a circuit block is producing correct outputs while enforcing that the environment is providing legal inputs. To attack this problem, several researchers have proposed monitor-based methodologies, which offer many benefits. This paper presents a novel, high-level specification style for these monitors, along with a linear-size, linear-time translation algorithm into monitor circuits. The specification style naturally fits the complex, but well-specified interfaces used between IP blocks in systems-on-chip. To demonstrate the advantage of our specification style, we have specified monitors for various versions of the Sonics OCP protocol as well as the AMBA AHB protocol, and have developed a prototype tool that automatically translates specifications into Verilog or VHDL monitor circuits.

REFERENCES

• 1: ARM Limited. AMBA Specification (Rev 2.0). 13 May 1999.
• 2: Roy Armoni , Limor Fix , Alon Flaisher , Rob Gerth , Boris Ginsburg , Tomer Kanza , Avner Landver , Sela Mador-Haim , Eli Singerman , Andreas Tiemeyer , Moshe Y. Vardi , Yael Zbar, The ForSpec Temporal Logic: A New Temporal Property-Specification Language, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.296-211, April 08-12, 2002
• 3: Ilan Beer , Shoham Ben-David , Cindy Eisner , Dana Fisman , Anna Gringauze , Yoav Rodeh, The Temporal Logic Sugar, Proceedings of the 13th International Conference on Computer Aided Verification, p.363-367, July 18-22, 2001
• 4: Lionel Bening , Harry Foster, Principles of Verifiable RTL Design, Kluwer Academic Publishers, Norwell, MA, 2001
• 5: Ashok K. Chandra , Dexter C. Kozen , Larry J. Stockmeyer, Alternation, Journal of the ACM (JACM), v.28 n.1, p.114-133, Jan. 1981 [doi>10.1145/322234.322243]
• 6: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 7: M. S. Jahanpour , E. Cerny, Compositional verification of an ATM switch module using interface recognizer/suppliers (IRS), Proceedings of the IEEE International High-Level Validation and Test Workshop (HLDVT'00), p.71, November 08-10, 2000
• 8: Matt Kaufmann , Andrew Martin , Carl Pixley, Design Constraints in Symbolic Model Checking, Proceedings of the 10th International Conference on Computer Aided Verification, p.477-487, June 28-July 02, 1998
• 9: Orna Kupferman , Moshe Y. Vardi, Module Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.75-86, August 03, 1996
• 10: Pascal Raymond, Recognizing Regular Expressions by Means of Dataflow Networks, Proceedings of the 23rd International Colloquium on Automata, Languages and Programming, p.336-347, July 08-12, 1996
• 11: Andrew Seawright , Forrest Brewer, High-level symbolic construction technique for high performance sequential synthesis, Proceedings of the 30th international conference on Design automation, p.424-428, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164961]
• 12: Kanna Shimizu , David L. Dill , Ching-Tsun Chou, A Specification Methodology by a Collection of Compact Properties as Applied to the Intel® ItaniumTM Processor Bus Protocol, Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.340-354, September 04-07, 2001
• 13: Kanna Shimizu , David L. Dill , Alan J. Hu, Monitor-Based Formal Specification of PCI, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.335-353, November 01-03, 2000
• 14: Sonics Incorporated. Open Core Protocol Specification 1.0. Document Version 1.2.
• 15: Jun Yuan , Kurt Shultz , Carl Pixley , Hillel Miller , Adnan Aziz, Modeling design constraints and biasing in simulation using BDDs, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.584-590, November 07-11, 1999, San Jose, California, United States

INDEX TERMS

Primary Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
      B.5.2 Design Aids

Additional Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids

  C. Computer Systems Organization
  C.0 GENERAL
      Subjects: Systems specification methodology

  J. Computer Applications
  J.6 COMPUTER-AIDED ENGINEERING
      Subjects: Computer-aided design (CAD)

General Terms:
Documentation, Languages, Verification

Keywords:
alternation, formal verification, pipelining, regular expressions