Space complexity

N n 1

(|eqs,n|×|eqd,n|) ) . (3-2)

In the above equations, |eqs,n| and |eqd,n| denote |eqs| and |eqd| at the n-th recursion, and N denotes the number of recursion times. For the worst case,

N = |Qs|×|Qd|, ( 3 - 3 )

|eqs,n| = |Qs|, ( 3 - 4 )

|eqd,n| = |Qd|, ( 3 - 5 )

=> worst-case iteration count = ( |Qs| × |Qd| )² , (3-6)

=> worst-case time complexity = O( ( |Qs| × |Qd| )² ) . (3-7)

Equation (3-3) holds only when all combinations of states in two FSMs are valid state pairs. Equation (3-4) and (3-5) hold only when the graph representations of two FSMs are complete graphs. However, these worst-case conditions rarely occur. Actually, experimental results show that the iteration count is typically far lower than this upper bound.

3.5.2 Space complexity

In the above algorithm, the space complexity is dominated by the size of two stacks.

One is the visited-node stack, i.e., S in the algorithm. The other is the error-trace stack, which is not explicitly specified in the algorithm. The visited-node stack contains the corresponding state pairs that are already visited. The error-trace stack contains the I/O values and state conditions from the initial node to the node that the violation occurs. Note

violation occurs.

The size of the visited-node stack is affected by the number of corresponding state pairs, where as the size of the error-trace stack is affected by the depth of the violation.

But anyhow, the worst-case space complexity of both stacks can be expressed as:

worst-case space complexity = O( |Qs| × |Qd| ). (3-8) Because |Qs|×|Qd| is equal to the maximum number of state pairs, and also equal to the maximum depth of the tree.

Chapter 4 Extension

4.1 Spec EFSM

Timing constraints are not uncommonly encountered in interface protocols. However, they cannot be easily specified in spec FSM sometimes. For example, a simple interface protocol, which defines “ack must be asserted within 16 cycles after req is asserted”, is specified as the spec FSM in Figure 4-1(a). It requires so many states to represent such a simple protocol. Instead, if we specify this protocol in EFSM by introducing a variable count as in Figure 4-1(b), the representation becomes much clearer and easier.

Similar to the spec FSM, the spec EFSM is an EFSM M=(Q, Σ, ∆, x, T, q0, x0) whose behavior is a monitor of certain interface logic where Q contains all normal states along with two extra special states vio and dc, Σ = Ictrl ∪ Octrl, and ∆ = φ. The predicates and actions provide a convenient way to specify timing constraints that are frequently encountered in interface protocols.

(a) (b)

Figure 4-1. Specify the same protocol in (a) FSM and (b) EFSM

4.2 Extended algorithm

Meanwhile, the original algorithm should also be extended to handle the spec EFSM.

Similarly, the extended algorithm grows a tree from each node unless the node has been present in the tree. The only difference now is that the node contains not only a state pair but also the values of the corresponding variables. A simple example is given in Figure 4-2. Figure 4-2(a) gives an erroneous implementation of the interface protocol in Figure 4-1. This design violates the protocol because it may not assert ack within 16 cycles if it sticks in the state wait. One possible scenario for the tree-growing process to find the violation is shown in Figure 4-2(b). The words in each node from left to right denote the spec EFSM state, the DUV state, and the value of the variable count. The nodes in the right branch illustrate the difference between the original algorithm and the extended one.

As shown, the extended algorithm does not stop at the node (ans, wait, 14) although this node has the same state pair as its parent node (ans, wait, 15). The reason is that the extra variable count needs to be considered as well.

req

(a) (b)

Figure 4-2. (a) A wrong implementation of the protocol in Figure 4-1 and (b) the tree generated by the extended algorithm.

The extended algorithm is given below (the modified parts are shaded). Similar to the algorithm in Section 3.4, S contains the nodes that have been present in the tree, and the function extended_grow_tree performs the branch-and-bound operations. But some extension is made here. The node now contains not only qs and qd but also x, the variable value because the variable value has to be considered as well. Moreover, in the function extended_grow_tree, the condition that a child node is created includes not only fqs,qi•fqd,qj

≠0 and (qi, qj, x’)∉S, but also Pqs,qi(x)==true, which means the predicate of current transition edge must be evaluated true. It is because the transitions can never take place if the predicate is not evaluated true. verify the compliance with the following algorithm:

req / ack

S=φ ;

extended_grow_tree(qs0 ,qd0, x0) ;

extended_grow_tree (qs, qd, x) { S = S ∪ (qs, qd, x) ;

for i=1 to |eqs| // for all outgoing edges of the state qs for j=1 to |eqd| { // for all outgoing edges of the state qd x’= Aqs,qi(x); // perform the action to the variable if (fqs,qi•fqd,qj ≠0 && Pqs,qi(x)==true && (qi, qj, x’)∉S) if (qi≠dc && qi≠vio )

extended_grow_tree(qi, qj, x’) ; else if (qi == vio)

give a counterexample and exit ; }

}

4.3 Complexity analysis

4.3.1 Time complexity

The time complexity analysis of the extended algorithm is similar to the discussions in Section 3.5.1. The iteration count is equal to (3-1). That is,

iteration count = (|eqs,n|×|eqd,n|) ( 3 - 1 ) where |eqs,n| and |eqd,n| denote |eqs| and |eqd| at the n-th recursion, and N denotes the number of recursion times.

∑

= N n 1

For the worst case,

N = |Qs|×|Qd|×|range(A(x))|, ( 4 - 1 )

|eqs,n| = |Qs|, ( 4 - 2 )

|eqd,n| = |Qd|, ( 4 - 3 )

=> worst-case iteration count = |range(A(x))| × (|Qs|×|Qd|)² , (4-4)

=> worst-case time complexity = O( |range(A(x))| × (|Qs|×|Qd|)² ) . (4-5)

The term range(A(x)) denotes the value range of the function A(x), and thus

|range(A(x))| denotes the number of possible values of x. Equation (4-1) holds when all combinations of two states and variable values are possible, and equation (4-2) and (4-3) holds when the graphic representations of two FSMs are complete graphs. Worst case like this rarely happens.

How exactly does the complexity change after this extension? Let us compare (4-5) to (3-7), although (4-5) is multiplied by a factor of |range(A(x))|, |Qs| of (4-5) is greatly reduced in general. Hence, the complexity does not increase significantly as expected.

4.3.2 Space complexity

Since the original state pair (qs, qd) is modified as (qs, qd, x), the original maximum number of state pairs |Qs|×|Qd| should be modified as |range(A(x))|×|Qs|×|Qd| as well.

This is the same case for the maximum depth of the tree. These modifications directly affect the maximum size of the visited-node stack and the error-trace stack, which further changes the worst-case space complexity. Therefore, the worst-case space complexity becomes:

worst-case space complexity = O( |range(A(x))| × |Qs| × |Qd| ). (4-6)

4.4 Other extensions

Except for the EFSM, the FSM has other variations, for example, the interacting FSM.

Theoretically, these variations can be transformed into the equivalent FSMs. Therefore, they can be candidates of other extensions to our approach. For example, some concurrent behaviors of interface protocols can be modeled by the interacting FSM easily. However, the transformation process imposes a heavy burden on the algorithm but improves only little expressing ability. Therefore, only the EFSM extension is implemented since the trade is worthwhile.

Chapter 5 Experimental Results

5.1 Program implementation

The proposed approach has been implemented in C. Our implementation can either formally prove that the given design is fully compliant with certain interface protocol or report a precise input sequence as a counterexample to show how the given design fails in the compliance verification. Additionally, the program can automatically check the correctness of the spec (E)FSM with the method in Section 2.5.2.

5.1.1 Input file format

Both the spec (E)FSM and the DUV FSM are accepted in the enhanced BLIF(Berkeley Logic Interchange Format) [26]. This format extends the BLIF with some syntax capable to describe the reasons of each transition as well as predicates and actions required by the EFSM model. Figure 5-1 shows an example in this format. The words after the character

# are comments. These comments clearly explain the syntax.

Figure 5-1. The spec EFSM of Figure 4-1 in the enhanced BLIF.

The reason column in the enhanced BLIF provides a way to specify the meaning of each transition. With these reasons, we can provide more meaningful counterexamples to improve the compliance verification.

5.1.2 Input file check

Our implementation can check the input files with the schemes described in Section 2.5.2. In the experiments, it really catches several bugs in the original spec FSMs of the

.model the_req_ack_protocol #model name

.inputs req ack #input names

.variables count 0 #variable and its initial value

AHB slave and the WISHBONE slave protocols. One of the bugs is shown in Figure 5-2.

This bug is arisen from omitting the edge e4 in Figure 2-4. That is, this transition is accidentally ignored in the original spec FSM. If we do not check with this method and neglect this transition in the spec FSM, the verification result may not be correct.

Figure 5-2. The report of catching a bug in the spec FSM of AHB slave protocol.

5.1.3 Counterexample

Our implementation gives very useful error-trace messages. It tells not only the I/O values and the state transitions, but also the reason of each transition. The error-trace message when verifying the design in Figure 4-2(a) is given in Figure 5-3. As we can see,

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

Result of pre-processing

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

Pre-process file golden_AHB_slave.txt ...

ERROR!In state orig :

Input 1100000 not specified!

Please modify input file golden_AHB_slave.txt!

Verification aborted! No result reported.

Figure 5-3. The verification result of the design in Figure 4-2(a).

the reason column tells the physical meaning of the current status. These reasons, along with the detail I/O sequence and state transitions, greatly facilitates the debugging of the interface design.

5.2 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.

在文檔中 應用於系統單晶片中介面相符驗證之正規方法 (頁 30-0)