Result analysis

In order to investigate the effectiveness and efficiency of the proposed algorithm, compliance verification is conducted over a set of real AMBA AHB-compliant and

********************************************

Result of this compliance verification

********************************************

DESIGN VIOLATES SPEC. : Ack_Exceed_16cycles

WISHBONE-compliant [27] designs. In addition, to check whether the proposed algorithm can find the design flaws as expected, some errors are intentionally injected into the design con7 and mac as two additional benchmark designs con7_err and mac_err, respectively. The experimental results are shown in Table 1.

There are some facts worthy to be mentioned in Table 1. As it is shown, all the designs under verification support different functional modes of the protocols, but the same spec (E)FSM can be used to verify all designs of the same protocol without altering.

Furthermore, the two injected errors are successfully found. The error in the design con7_err is caused by a self-loop of the state performing the WAIT response. Thus the design may respond WAIT more than 16 cycles, which is not recommended in the AHB protocol. This is an error that designers are very likely to commit if they don’t deal with the WAIT response carefully. The other error in the design mac_err is a little more complex. When an IDLE transfer is initiated after an ERROR response, the design does not respond OKAY but respond ERROR instead, which causes a violation to the AHB protocol. This error is not uncommon because the two-cycle ERROR response is intrinsically more complicated and error-prone. With our verification approach, these errors and the reasons leading to them are clearly identified.

Table 1. The DUVs and the verification results.

I/F protocol

type DUV result supporting function reason of violation

spi [28] compliance NORMAL and

ERROR response -

WISHBONE slave

(spec FSM) ac3 ctrl[28] compliance NORMAL response -

con7 compliance

con7_err violation OKAY and WAIT

response Wait>16cycles AMBA AHB

slave (spec EFSM)

mac_err violation OKAY and ERROR

response Not_Respond_Okay The complexity comparison is shown in Table 2. It clearly demonstrates that our algorithm can correctly complete the formal compliance verification for all given designs.

The results also indicate that the actual time and space requirements are far less than the estimated ones from the worst-case analysis. As a matter of fact, each verification run listed in Table 1 finishes within just 1 second. It shows that our algorithm is capable of completing the formal compliance verification in reasonable time. Though we cannot find even larger real designs for investigation, we believe our algorithm can handle FSMs containing hundreds of states that are more complicated than FSMs of most practical designs.

Table 2. Complexity comparison.

I/F protocol type DUV stack size ( |S| )

|range(A(x))|

× |Qs|×|Qd|

iteration count

|range(A(x))|×

(|Qs|×|Qd|)²

spi [28] 14 7x3=21 180 (7×3)²=442

WISHBONE slave

(spec FSM) ac3 ctrl [28] 23 7x5=35 221 (7×5)²=1225

con7 11 16x7x4=448 204 16×(7×4)²=12544

mac 8 16x7x6=672 191 16×(7×6)²=28224

remap 8 16x7x6=672 136 16×(7×6)²=28224

con7_err 20 16x7x4=448 42 16×(7×4)²=12544

AMBA AHB slave (spec EFSM)

mac_err 6 16x7x6=672 57 16×(7×6)²=28224

Chapter 6 Conclusions and Future Work

In this thesis, we first introduce the spec FSM to systematically represent an interface protocol specification. A method of checking the correctness of the spec FSM is also given. We further show how to formulate the interface compliance verification as the compliance verification between the spec FSM and the DUV FSM. A novel branch-and-bound algorithm is then proposed to formally solve the FSM compliance problem. The proposed algorithm is further extended to handle the spec EFSM, which is capable of efficiently modeling more complicated interface protocols. Experimental results demonstrate that our approach can effectively and efficiently verify the interface compliance over a set of real designs.

6.1 Contributions

The main contributions of this work are summarized as follows:

property specification

1. A method of specifying the interface protocol specification as the specification (E)FSM is proposed.

2. A simple but effective way to check the correctness of the spec (E)FSM is given.

verification technique

1. A reasonable problem formulation that focuses on interface logic at FSM level is proposed.

2. A formal algorithm is developed for interface compliance verification.

6.2 Comparisons

In comparison with other specification styles and property languages, our specification style, the specification (E)FSM, is relatively systematic and easily comprehensible that it is more likely to specify the properties more completely. In comparison with dynamic simulation-based methods, our method is formal thus does not have the false positive problem. In comparison with static formal methods, our algorithm hardly suffers from memory explosion and excessive runtime issues in practice. Therefore, the proposed technique is extremely useful for interface compliance verification broadly demanded by modern platform-based SoC designs.

6.3 Future work

Our approach may probably be enhanced to verify designs in different abstract level.

For example, it can be used to verify RTL designs by extracting FSMs from RTL codes.

But the overhead introduced by transforming between different abstract levels needs to be considered carefully. Moreover, different verification schemes using the same spec (E)FSM can be developed. For example, in addition to this formal approach, the spec (E)FSM may turn into a monitor in simulation-based verification. Combining both simulation-based and formal approaches with the same spec (E)FSM will greatly facilitate the verification.

References

[1] VSI Alliance, Virtual Component Interface (VCI) Standard - OCB 2 1.0, http://www.vsia.org, Mar. 2000.

[2] Kanna Shimuzu, David L. Dill, and Alan J. Hu, “Monitor-Based Formal Specification of PCI,” in Proceedings of the 3th International Conference on Formal Methods in Computer-Aided Design, Nov. 2000, pp. 335-353.

[3] Hue-Min Lin, Chia-Chih Yen, Che-Hua Shih, and Jing-Yang Jou, “On Compliance Test of On-Chip Bus for SOC,” in Proceedings of the Asia and South Pacific Design Automation Conference, Jan. 2004, pp. 328-333.

[4] Marcio T. Oliviera and Alan J. Hu, “High-Level Specification and Automatic Generation of IP Interface Monitors,” in Proceedings of the 39th Design Automation Conference, June 2002, pp. 129-134.

[5] Alan J. Hu, Jeremy Casus, and Jin Yang, “Efficient Generation of Monitor Circuits for GSTE Assertion Graphs,” in Proceedings of the 2003 IEEE/ACM International Conference on Computer-Aided Design, Nov. 2003, pp. 154-159.

[6] Jun Yuan, Kurt Shultz, Carl Pixley, Hillel Miller, and Adnan Aziz, “Modeling Design Constraints and Biasing in Simulation Using BDDs,” in Proceedings of the 1999 IEEE/ACM International Conference on Computer-Aided Design, Nov. 1999, pp.

584-589.

[7] Kanna Shimizu and David L. Dill, “Deriving a Simulation Input Generator and a Coverage Metric From a Formal Specification,” in Proceedings of the 39th Design Automation Conference, June 2002, pp. 801-806.

[8] Serdar Tasiran, Yuan Yu, and Brannon Baston, “Using a Formal Specification and a Model Checker to Monitor and Direct Simulation,” in Proceedings of the 40th Design Automation Conference, June 2003, pp. 356-361.

[9] Andy Nightingale and John Goodenough, “Testing for AMBA Compliance,” in Proceedings of the 14th Annual IEEE International ASIC/SOC Conference, Sept. 2001, pp. 301-305.

[10] ARM Limited, AMBA Specification (Rev 2.0), 13 May 1999.

[11] http://www.synopsys.com/products/designware/docs/vip/

[12] Pankaj Chauhan, Edmund M. Clarke, Yuan Lu and Dong Wang, “Verifying IP-Core Based System-On-Chip Designs,” in Proceedings of the 12th Annual IEEE International ASIC/SOC Conference, Sept. 1999, pp. 27-31.

[13] Ilan Beer, Shoham Ben-David, Cindy Eisner, Yechiel Engel, Raanan Gewitzman and Avner Landver, “Establishing PCI Compliance Using Formal Verification: A Case Study,” in Proceedings of the 14th International Phoenix Conference on Computation and Communications, Mar. 1995, pp. 373-377.

[14] Abhik Roychoudhury, Tulika Mitra, and S.R. Karri, “Using Formal Techniques to Debug the AMBA System-on-Chip Bus Protocol,” in Proceedings of the Design, Automation and Test in Europe Conference and Exhibition, 2003, pp. 828-833.

[15] Lubomir Ivanov and Ramakrishna Nunna, “Specification and Formal Verification of Interconnect Bus Protocols,” in Proceedings of the 43rd IEEE Midwest Symposium on Circuits and Systems, Aug. 2000, pp. 378-382.

[16] K. L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, 1993.

[17] http://www.eda.org/vfv/docs/psl_lrm-1.01.pdf/.

[18] http://www.verificationlib.org/.

[19] http://www.opervera.org/.

[20] http://www.systemverilog.org/.

[21] Yatin V. Hoskote, Jacob A. Abraham, and Donald S. Fussell, “Automated Verification of Teporal Properties Specified as State Machines in VHDL,” in Proceedings of the 5th Great Lakes Symposium on VLSI, Mar. 1995, pp. 100-105.

[22] Annette Bunker and Ganesh Gopalakrishnan, “Using Live Sequence Charts for Hardware Protocol Specification and Compliance Verification,” in Proceedings of the IEEE International High Level Design Validation and Test Workshop, Nov. 2001, pp.

95-100.

[23] Annette Bunker, Ganesh Gopalakrishnan, and Sally A. McKee, “Formal Hardware Specification Languages for Protocol Compliance Verification,” ACM Transactions on Design Automation of Electronic Systems, vol. 9, no. 1, Jan. 2004.

[24] Kanna Suimizu, David L. Dill, and Ching-Tsun Chou, “A Specification Methodology by a Collection of Compact Properties as Applied to the Intel^® Itanium Processor Bus Protocol,” in Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, Sept. 2001, pp.

340-354.

[25] Cedric Besse and Ana Cavalli, “An Automatic and Optimized Test Generation Technique Applying to TCP/IP Protocol,” in Proceedings of the 14th IEEE International Conference on Automated Software Engineering, Oct. 1999, pp. 73-80.

[26] University of California Berkeley, Berkeley Logic Interchange Format (BLIF), Sept.

1996.

[27] OpenCores Organization, Specification for the: WISHBONE System-on-Chip (SoC) Interconnection Architecture for Portable IP Cores, Rev. B.3, 2002.

[28] http://www.opencores.org/.

Vita

Ya-Ching Yang was born in Taipei, Taiwan on February 9, 1980. She received the B.S. degree in Electronics Engineering from National Chiao Tung University in June 2002.

From September 2002, she is a graduate student of Professor Jing-Yang Jou in the Institute of Electronics, National Chiao Tung University. Her research interests include verification and Electronic Design Automation (EDA). She received the M.S. degree from National Chiao Tung University in June 2004.