Chapter 3 State-Oriented Language
3.7 Case study
The sequence set cross operator can provide a much more elegant but equivalent representations while the transactions become complex. This operator can reduce the transaction description complexity as well as help generate more interesting transactions easily.
3.7 Case study
To apply our methodology, the interface protocol should be given as a spec. FSM first. The details about how to construct a spec. FSM can be found in [12-13]. The AMBA AHB slave interface protocol [18] is adopted as an example here to demonstrate how to define transactions in SOL. The spec. FSM of the simplified AMBA AHB slave protocol is given in Figure 7.
31
Figure 7. The spec. FSM of the simplified AMBA AHB slave protocol.
In this spec. FSM, only several important control signals (HSEL, HTRANS, HREADY, and HRESP) are concerned. Besides, one special state is defined: DUV_ERR.
If the DUV behaves illegally, the design moves to the state DUV_ERR. Otherwise, the design moves among the other normal states excluding DUV_ERR. By traversing the spec. FSM, many defined properties can be found. For example, in the state IDLE/BUSY, if HREADY is not asserted or HRESP is not set to OKAY, the design moves to the state DUV_ERR. This infers that a slave cannot respond anything but a zero WAIT state OKAY response to an IDLE or a BUSY transfer. In addition, in the state WAIT, if HREADY is asserted but HRESP is not set to OKAY, the design moves to the state DUV_ERR. This implies that a slave can only respond OKAY when HREADY is transient to be asserted. These are explicitly defined in the AMBA AHB specification.
32
However, the spec. FSM is not omnipotent for the lack of consideration to each signal. For example, the read transactions cannot be distinguished from the write transactions. The burst mode of each transaction cannot be detected, either. To retrieve these issues, the extra signal qualification operation should be applied.
Now, use SOL to define basic transactions on the spec. FSM.
Example 1.
A 1-beat burst transaction.
The construction procedure of a 1-beat burst transaction can be decomposed into four steps.
(1) For a 1-beat burst transaction, the signal HBURST must be set to 0.
(2) The given design must move to state NSEQ/SEQ (S1) one time and cannot move to state ERROR (S4) for a complete 1-beat transfer, i.e., {S4[=0]} && {S1[Æ1]} . (3) A 1-beat burst transaction consists of two cases. One starts from the state ORIG (S0),
which indicates the slave is just selected and going to do the first transaction. The other starts from the state NSEQ/SEQ (S1), which implies the slave is already selected and going to do another transaction.
○1 starting from the state ORIG (S0) : OneBeat_S0 = {S0 “HBURST==0”;{S4[=0]}&&{S1[Æ1]}};
○2 starting from the state NSEQ/SEQ (S1) : OneBeat_S1 = {S1 “HBURST==0”;{S4[=0]}&&{S1[Æ1]}};
33
(4) A 1-beat burst transaction is either the sequence OneBeat_S0 or the sequence OneBeat_S1. Then a 1-beat burst transaction is composed of these two sequences by using the sequence OR operator. That is,
OneBeat = {{OneBeat_S0} | {OneBeat_S1}};
Example 2.
A 4-beat burst transaction.
The construction procedure of a 4-beat burst transaction is similar to that of a 1-beat burst transaction.
(1) The signal HBURST should be set to 2 or 3.
(2) The design must visit the state NSEQ/SEQ (S1) four times and cannot move to state ERROR (S4) to complete a 4-beat transfer, i.e., {S4[=0]} && S1[Æ4] .
(3) A 4-beat burst transaction also consists of two cases.
○1 starting from the state ORIG (S0) : FourBeat_S0 = {S0 “HBURST==2 || HBURST==3”;{S4[=0]}&&{S1[Æ4]}};
○2 starting from the state NSEQ/SEQ (S1) : FourBeat_S1 = {S1 “HBURST==2 || HBURST==3”;{S4[=0]}&&{S1[Æ4]}};
(4) A 4-beat burst transaction can then be defined as, FourBeat = {{FourBeat_S0} | {FourBeat_S1}};
34
Follow similar procedure, more basic transactions can be defined. For a 4-beat burst with wait transaction (FourBeatWithWAIT), the state WAIT (S3) must be visited at least one time during the transaction. That is, the sequence {S3[=1:]} must hold.
Therefore, the 2nd step of the construction procedure of the 4-beat burst with wait transaction must be written as {S3[=1:]}&&{{S4[=0]}&&{S1[Æ4]}}. For an 8-beat write burst transaction (EightBeatWrite), the signal HBURST must be set to proper values (4 or 5) and the signal HWRITE must be asserted, i.e., the 1st step:
(HBURST==4 || HBURST==5) && HWRITE . As well, the design must visit the state NSEQ/SEQ (S1) eight times during this 8-beat burst transaction, i.e., the 2nd step:
{S4[=0]} && {S1[Æ8]}.
Example 3.
A 4-beat burst transaction instantly followed by an 8-beat write burst transaction.
A 4-beat burst transaction (FourBeat) and an 8-beat write burst transaction (EightBeatWrite) are defined before. Since the required transaction can be defined by fusing these two transactions, it can be written as follows,
{{FourBeat}:{EightBeatWrite}};
More complex transactions can be constructed by the sequence fusion operator ( : ).
For example, a 1-beat burst transaction followed by an 8-beat write burst transaction, then followed by a 4-beat burst transaction can be defined as follows,
{{OneBeat}:{EightBeatWrite}:{FourBeat}};
35
In addition, the sequence set cross operator ( ** ) can be used to describe a lot of back-to-back consecutive transactions in a more easy way. The expression below can represent 12 (3*2*2) different consecutive transactions.
<{EightBeatWrite},{FourBeatWithWAIT},{OneBeat}>
** <{FourBeat},{OneBeat}> ** <{EightBeatWrite},{FourBeat}>;
If the interesting transactions are comprised by many other transactions with this complex cross behavior, the sequence set cross operator can provide a strong expressive power.
36
Chapter 4 Proposed Methodology
By means of SOL, transactions can be defined in a simpler, but still rigorous, and more systematic way. As well, the transaction-level functional coverage for the interface compliance verification can be done at the higher FSM level.
The flow of our verification methodology is illustrated in Figure 8. The interface protocol needs to be first specified as a spec. FSM by using the methods in [12-13]. Note that the spec. FSM can be translated into an interface protocol checker [13]. Meanwhile, a transaction can be thought as a specific sequence of state transitions within the spec.
FSM. The interesting transactions are manually specified by using SOL. These transactions with the spec. FSM are further translated into a functional coverage
37
analyzer automatically. Next, we simulate the whole system, including the DUV, verification patterns, checker, and coverage analyzer. According to the outcome of the checker, we can know if the DUV conforms to the interface protocol. From the coverage analyzer, the report tells how many interesting transactions have been verified.
Moreover, the coverage information can guide either direct or random patterns to hit those unverified design corner cases.
Figure 8. The flow of our verification methodology.
Coverage
38
Chapter 5 Experimental Results
5.1 Experimental environment
To demonstrate our methodology, we choose the AMBA AHB slave interface protocol [18] as an example. The spec. FSM of simplified AMBA AHB slave protocol is given in Figure 7. Figure 9 illustrates the experimental environment. It consists of three parts: a DUV, a constraint-driven random pattern generator, and the proposed work.
39
Figure 9. The experimental environment.
(1) The DUV is the slave which we want to verify. The experiments are conducted over three real AHB slave designs. The information about these three designs is shown in Table 1. The design RGB2YCrCB is a RGB-to-YCrCB color space converter. The design MAC is a multiply-accumulator. The design Convolution is a convolution calculator for discrete wavelet transfer.
40
(2) The constraint-driven random pattern generator is an AHB master which generates verification patterns based on an NEFSM (Non-deterministic Extended FSM) with the weight information about the transitions and bursts. The NEFSM is given in Figure 10. The weight of each transition and burst is configurable. For example, the weights of transition t15, t16, t27, and t41 can be assigned to a higher value to increase the probability of the occurrence of BUSY conditions. In order to balance the occurrence of total verification patterns, the transitions and bursts are assigned to be equal weight.
Figure 10. The NEFSM of the AMBA AHB master.
orig
41
(3) We develop a translator which accepts the spec. FSM and user-defined SOL transactions then produces the corresponding coverage analyzer. The coverage report tells how many interesting transactions have been verified. In addition, the coverage information is used to help statically bias the random pattern generator to create more effective verification patterns.
5.2 Results analysis
Two experiments are conducted: coverage comparison and efficiency improvement.
In the first experiment, four coverage results (State coverage, Transition coverage, M-path coverage, and our Transaction coverage) are compared for three designs, respectively. In the second experiment, the coverage information is sent back to bias the random pattern generator to produce more effective patterns.
5.2.1 Coverage comparison
Case 1
The interesting transactions are defined as 10 basic read and write transactions as
follows,
{IncrBeatRead}; {OneBeatRead}; {FourBeatRead}; {EightBeatRead}; {SixteenBeatRead};
{IncrBeatWrite}; {OneBeatWrite}; {FourBeatWrite}; {EightBeatWrite}; {SixteenBeatWrite};
The comparison results are shown in Table 2. Since the supporting responses of each design are different from each other, each takes distinct simulation time to reach 100% State/Transition/M-path/Transaction coverage. For the design RGB2YCrCb, it takes 4/16/82/492 cycles to reach 100% State/Transition/M-path/Transaction coverage.
42
As the State/Transition/M-path coverage reach 100%, the Transaction coverage is only 0/10/20%. For the other two designs, the results are similar. It is observed that the Transaction coverage is very low while the other three coverage metrics reach 100%.
Table 2. Coverage comparison for Case 1.
Design Coverage # of cycles to
Make the interesting transactions more complex by adding 15 more basic transactions with BUSY or WAIT (e.g, {OneBeatWithWAIT}; {FourBeatWithBUSY};
{FourBeatWithWAIT}; {EightBeatWithBUSY};, etc.) and 25 back-to-back consecutive transactions (i.e., <{IncrBeat},{OneBeat},{FourBeat},{EightBeat},{SixteenBeat}>**
<{IncrBeat}, {OneBeat},{FourBeat},{EightBeat},{SixteenBeat}>;).
The comparison results are shown in Table 3. Since the status of the random pattern generator is the same as that in Case 1, the design Convolution still takes 12/47/102
43
cycles to reach 100% State/Transition/M-path coverage. But it takes 11135 cycles to reach 100% Transaction coverage. As the State/Transition/M-path coverage reach 100%, the Transaction coverage is only 4/8/12%. It is shown that the Transaction coverage is even lower than that in Case 1 as the other three coverage metrics reach 100%.
Table 3. Coverage comparison for Case 2.
Design Coverage # of cycles to
From these two cases, we get some conclusions. While the interesting transactions become more complex, it needs a significantly longer simulation time to reach 100%
Transaction coverage. Besides, as the State/Transition/M-path coverage reach 100%, the Transaction coverage can still be very low. Experimental results exactly show that the classical coverage metrics are not capable of providing enough verification quality. By means of our approach, we can put more emphasis on the functionality that we want to verify and detect more errors. In other words, the verification quality can be improved in large.
5.2.2 Efficiency improvement
After analyzing the coverage report in Section 5.2.1 Case 2, we find the major reason why so many cycles are required to reach 100% Transaction coverage is the seldom occurrence of BUSY transactions. Hence, it is possible to reduce the simulation
44
time by statically biasing the constraint-driven random pattern generator.
The biasing information is shown in Table 4. In bias1, we increase the weights of transition t15, t16, t27, and t41 in the NEFSM that may generate BUSY transactions.
This is an intuitive configuration. This bias indeed decreases the simulation time to 1864 cycles, which is only 16.7% of the original one. In bias2, the weights of INCR burst, 1-beat burst, 4-beat burst, 8-beat burst, and 16-beat burst are given in a decreasing order because the BUSY transaction takes place more frequently in the long-beat transfers.
Bias2 can balance the occurrence of BUSY transactions in each burst. Combing bias1
with bias2, the simulation time can be further decreased to 981 cycles, which is only 8.8% of the original one.
Table 4. Efficiency improvement.
Design Bias # of cycles to
reach 100% Factor
equal weight 11135 1
bias1 1864 0.167
Convolution
bias1+ bias2 981 0.088
The results show that the coverage information can help bias the random pattern generator to create more effective patterns and help verify the DUV in a short time. This technique is extremely useful for the regression verification environment in which the compact and effective patterns are crucial to minimize the required simulation time.
45
Chapter 6
Conclusions and Future Works
In this thesis, we propose a transaction-level functional coverage methodology for interface compliance verification. To provide an intuitive, user-friendly, but still rigorous, and systematic way to specify transactions at the higher FSM level, we develop a new transaction description language SOL. The expressive power of SOL is stronger than that of previous regular-expression-based approaches. It is shown that SOL is capable of modeling very complex functional transactions. Meanwhile, a translator is also developed to automatically convert a set of SOL-based transactions with the spec. FSM into the corresponding functional coverage analyzer. The experimental results demonstrate that the proposed methodology can indeed improve the verification quality
46
as well as increase the verification efficiency.
6.1 Contributions
The main contributions of this work are summarized as follows:
♦ Transaction description style
1. A transaction description language, SOL, is developed to define transactions at the FSM level.
2. SOL owns a very strong expressive power to model complex transactions.
♦ Verification methodology
1. A transaction-level functional coverage methodology for interface compliance verification is proposed.
2. A translator is developed to automatically convert the user-defined transaction scenarios into a coverage analyzer.
3. The coverage report can help generate more effective verification patterns.
6.2 Future works
Our work focuses on how to define transaction at the higher FSM level and the automatic translation of user defined SOL-based transaction scenarios into a coverage analyzer. The proposed verification methodology can be further improved by the following two aspects:
47
1. In our experiment, we use a spec. NEFSM as a constraint-driven random pattern generator. However, there is another spec. FSM for the checker and the coverage analyzer. The developments of two distinct FSMs may require a huge number of man-hours. Besides, the inconsistencies may exist between these two FSMs.
Therefore, a unified FSM model for the pattern generator, checker, and coverage analyzer should be preferred.
2. The coverage report in our work is merely used to statically and manually bias the pattern generator. To increase the verification efficiency, automatically dynamic biasing approaches should be further considered and developed.
48
References
[1] Michael Keating and Pierre Bricaud, “Reuse Methodology Manual for System-On-A-Chip Designs, 3rd Edition,” Kluwer Academic Publishers, July 2002.
[2] Janick Bergeron, “Writing Testbenches: Functional Verification of HDL Models, 2nd Edition,” Kluwer Academic Publishers, February 2003.
[3] Dean Drako and Paul Cohen, “HDL Verification Coverage,” Integrated System Design Magazine, pp. 46-52, June 1998.
[4] Farzan Fallah, Srinivas Devadas, and Kurt Keutzer, “OCCOM: Efficient Computation of Observability-Based Code Coverage Metrics for Functional Verification,” Proceedings of the Design Automation Conference, pp. 152-157, June 1998.
[5] Pradip A. Thaker, Vishwani D. Agrawal, and Mona E. Zaghloul, “Validation Vector Grade (VVG): A New Coverage Metric for Validation and Test,”
Proceedings of the IEEE VLSI Test Symposium, pp. 182-188, April 1998.
[6] Byeong Min and Gwan Choi, “ECC: Extended Condition Coverage for Design Verification Using Excitation and Observation,” Proceedings of the Pacific Rim International Symposium on Dependable Computing, pp. 183-190, December 2001.
49
[7] Raanan Grinwald, Eran Harel, Michael Orgad, Shmuel Ur, and Avi Ziv, “User Defined Coverage - A Tool Supported Methodology for Design Verification,”
Proceedings of the Design Automation Conference, pp. 158-163, June 1998.
[8] Sigal Asaf, Eitan Marcus, and Avi Ziv, “Defining Coverage Views to Improve Functional Coverage Analysis,” Proceedings of the Design Automation Conference, pp. 41-44, June 2004.
[9] Avi Ziv, “Cross-Product Functional Coverage Measurement with Temporal Properties-Based Assertions,” Proceedings of the Design, Automation and Test in Europe Conference and Exhibition, pp. 834-839, March 2003.
[10] Young-Su Kwon, Young-Il Kim, and Chong-Min Kyung, “Systematic Functional Coverage Metric Synthesis from Hierarchical Temporal Event Relation Graph,”
Proceedings of the Design Automation Conference, pp. 45-48, June 2004.
[11] Young-Su Kwon and Chong-Min Kyung, “Functional Coverage Metric Generation from Temporal Event Relation Graph,” Proceedings of the Design, Automation and Test in Europe Conference and Exhibition, pp. 670-671, February 2004.
[12] Ya-Ching Yang, Juinn-Dar Huang, Chia-Chih Yen, Che-Hua Shih, and Jing-Yang Jou, “Formal Compliance Verification of Interface Protocols,” Proceedings of the IEEE International Symposium on VLSI Design, Automation, and Test, pp. 12-15, April 2005.
50
[13] Hue-Min Lin, Chia-Chih Yen, Che-Hua Shih, and Jing-Yang Jou, “On Compliance Test of On-Chip Bus for SOC,” Proceedings of the Asia and South Pacific Design Automation Conference, pp. 328-333, January 2004.
[14] Koji Ara and Kei Suzuki, “A Proposal for Transaction-Level Verification with Component Wrapper Language,” Proceedings of the Design, Automation and Test in Europe Conference and Exhibition, pp. 82-87, March 2003.
[15] Chris Browy, “Comparing TestWizard and Specman for Transaction-Level Verification,” White Paper, available at http://www.avery-design.com/twwp.html [16] Heinz-Josef Schlebusch, Gary Smith, Donatella Sciuto, Daniel Gajski, Carsten
Mielenz, Christopher K. Lennard, Frank Ghenassia, Stuart Swan, and Joachim Kunkel, “Transaction-Based Design: Another Buzzword or the Solution to a Design Problem?,” Proceedings of the Design, Automation and Test in Europe Conference and Exhibition, pp. 876-877, March 2003.
[17] http://www.eda.org/vfv/docs/psl_lrm-1.01.pdf
[18] ARM Limited, AMBA Specification (Rev 2.0), May 1999.
51
Appendix A
SOL Syntax Rule Summary
A.0 Syntax conventions
The formal syntax described here uses the following extended BNF.
(1) The initial character of each word in a nonterminal is capitalized. A nonterminal can be either a single word or multiple words separated by underscores. When a multiple-word nonterminal containing underscores is referred within the text, the underscores are replaced with spaces.
(2) Boldface words are used to denote reserved keywords, operators, and punctuation marks as a required part of the syntax. These words appear in a larger font for distinction.
(3) The ::= operator separates the two parts of a BNF syntax definition. The syntax category appears to the left of this operator and the syntax description appears to the right of the operator.
(4) A vertical bar separates alternative items (use one only) unless it appears in boldface, in which case it stands for itself.
(5) Square brackets enclose optional items unless they appear in boldface. In which case they stand for themselves.
(6) Braces enclose a repeated item unless they appear in boldface, in which case they stand for themselves. A repeated item may appear zero or more times.
(7) A comment is preceded by a colon unless it appears in boldface, in which case it stands for itself.
52
Boolean_Expression : An expression that yields a logical value
A.2 Sequential layer
SERE : State Extended Regular Expression SERE ::=
53
54
A.2.2.3 Sequence fusion ( : ) SERE ::=
Sequence
:
SequenceSequence ::=
{
SERE}
A.3 Transaction layer
Transaction_Declaration ::=
Sequence_Name
=
Sequence;
A.4 Coverage layer
Coverage_Declaration ::=
Sequence_Name
;
| Sequence_Cross
;
A.4.1 Sequence set cross ( ** ) Sequence_Cross ::=
Sequence_Set
**
Sequence_Set {**
Sequence_Set } Sequence_Set ::=< {
Sequence_Name}
{,{
Sequence_Name}
}>
55
Vita
Man-Yun Su was born in Taitung, Taiwan on January 3, 1981. She received the B.S. degree in Electrical Engineering from National Tsing Hua University in June 2003.
From September 2003, she is a graduate student advised by Professor Jing-Yang Jou in the Institute of Electronics, National Chiao Tung University. Her research interests include design methodology and functional verification of VLSIs. She received the M.S.
degree from National Chiao Tung University in June 2005.