Directed-simulation assisted formal verification of serial protocol and bridge

ABSTRACT

Robust verification of protocol conversion and arbitration schemes of SoC bridges forms a significant component of the overall SoC verification. Formal verification provides a way to achieve this, but a naive approach often leads to explosion of the state space, and is impractical for most of today's protocols and bridges. This problem is further complicated in the presence of serial protocols, where control and data are mixed together and transactions continue for very great depths. White-box verification is not a feasible solution, since these bridges are often imported or generated from other sources, and internal information is not readily available. In this paper, we propose a black-box and hybrid approach to this problem, by judiciously mixing simulation and formal verification. We illustrate our approach by applying it to two dual stage bridges that perform serial to parallel protocol conversion and vice versa.

REFERENCES

• 1: E. Salminen, V. Lahtinen, K. Kuusilinna and T. Hamalainen, "Overview of Bus-Based System-on-Chip Interconnections," IEEE International Symposium on Circuits and Systems, 2002, vol 2, pp. II-372 -- II-375.
• 2: Open Core Protocol 2.1 Specification, www.ocpip.org
• 3: ARM Inc, AMBA AXI Protocol Specification, Mar., 2004. www.arm.com
• 4: Philips Semiconductors, "The I2C-BUS specification", Version 2.1, January, 2000. http://www.cse.ucsc.edu/classes/cmpe123/Fall02/Files/I2C_BUS_SPECIFICATION.pdf
• 5: USB Implementers Forum Inc, Universal Serial Bus Specification Revision 2.0, 2000. www.usb.org
• 6: Abhik Roychoudhury , Tulika Mitra , S. R. Karri, Using Formal Techniques to Debug the AMBA System-on-Chip Bus Protocol, Proceedings of the conference on Design, Automation and Test in Europe, p.10828, March 03-07, 2003
• 7: P. Chauhan, E. Clarke, Y. Lu and D. Wang, "Verifying IP-core based system-on-chip design," Proc. IEEE ASIC. Conf., Washington, DC, USA, Sept. 1999, pp. 27--31.
• 8: Amit Goel , William R. Lee, Formal verification of an IBM CoreConnect processor local bus arbiter core, Proceedings of the 37th conference on Design automation, p.196-200, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337384]
• 9: Shivakumar Chonnad and Balachander Needamangalam, "A Layered Approach to Behavioral Modeling of Bus Protocols," Proceedings of the 13th Annual IEEE International ASIC/SOC Conference, 2000, pp 170 -- 173.
• 10: B. Plessier and C. Pixley, "Formal verification of a commercial serial bus interface," Conference Proceedings of the 1995 IEEE Fourteenth Annual International Phoenix Conference on Computers and Communications, 1995.
• 11: C Norris Ip, "Formal interface compliance verification", Electronics Design Process Workshop, April 2003.
• 12: Jun Yuan , Ken Albin , Adnan Aziz , Carl Pixley, Constraint synthesis for environment modeling in functional verification, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775909]
• 13: Enric Pastor , Marco A. Pena, Combining Simulation and Guided Traversal for the Verification of Concurrent Systems, Proceedings of the conference on Design, Automation and Test in Europe, p.11158, March 03-07, 2003

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

General Terms:
Experimentation, Verification

Keywords:
formal verification, model checking, serial protocol