Functional Finite State Machine Paths Coverage using SystemVerilog

By Bahaa Osman (Mentor Graphics), Mohamed Salem (University of Bristol)

I. INTRODUCTION

The functional verification process involves the development of constrained random test cases, and the technique of coverage driven verification [1] to produce, and analyze the simulation results. Finite state machines (FSMs) have finite number of states, conditions that lead to internal state transitions, and relevant behavior of the design in each machine state. An FSM generally models the behavior of the control logic. For example, standard-based layered protocols typically model each layer in terms of an FSM. An FSM’s states’ transition coverage is essential but it is not a complete verification of the entire FSM model. Multiple conditions may lead to the same state transition. States’ transition coverage does not provide full information on the generated stimulus that resulted in this transition, in terms of which particular condition lead to that transition. In addition, 100% states’ transition coverage implies that the stimulus has examined all states’ transitions, irrespective of the coverage of all the conditions (arcs) that result in the entire states’ transition. It does not guarantee that the stimulus has covered all the possible paths between the states, though it presents coverage of a particular transition through the partial or full set of the possible paths. Arc coverage provides comprehensive simulation coverage results that guarantee that the stimulus has completely exercised the full arcs of the FSM. FSM’s states’ transition coverage and states’ arc coverage provide complete verification of the FSM model behavior.

FSM coverage has been always recorded by the code coverage tools. Most tools have the ability to recognize FSM implementations without the need to write extra HDL code, and the tools then record state and arc coverage [2]. Tool dependency imposes requirements and restrictions on the written HDL code to describe the FSM in order to be correctly recognized [3-4]. The structural code coverage domain targets the design implementation, while the functional coverage domain targets the design functionality compliance with design specification. FSM coverage under the functional coverage domain enables FSM behavior verification, whenever code coverage tool does not recognize or extract a particular FSM. FSM functional coverage integrates in advanced verification methodologies due to the ability of reuse of the coverage model throughout the multiple abstraction levels from transaction level model [5] (TLM) to gate netlist level. Code coverage tools may be able to extract FSM models from RTL level only.

There are several efforts to solve the problem of modeling FSM coverage [6-7]. In this paper, we present two new methods to implement the recording of FSM coverage into the functional coverage model in a constrained random coverage-driven verification environment. These methods enable state machine coverage data implementation, interpretation, and analysis across the multi- abstraction levels from TLM, to gate level. The proposed methods are implemented in SystemVerilog [8]; in addition the first method can be implemented in an assertion-based language such as Property Specification Language [PSL] [9]. Both methods align with the advanced verification methodologies such as OVM [10], and VMM [11]. The methods are tool independent, as any tool that supports SystemVerilog can be used. In addition, they are implementation independent; since neither the FSM coding style nor the abstraction level used to describe the design specification affect the use of the methods.

The first method, the cover directive method, is based on the assertion-based verification [12] (ABV) capabilities of SystemVerilog implemented in properties, and verification directives. In this technique, FSM arcs are first defined using SystemVerilog assertion properties using any of the constructs that allow temporal expression description. Then it uses the cover directive to check for the coverage of these defined properties, and eventually checking for the FSM arc coverage results.

The second method, the covergroups method, uses the functional coverage construct of SystemVerilog, cover groups. Cover groups and cover points are defined to cover both state transitions, and the corresponding condition values that cause these transitions. Then arc coverage is defined by the cross coverage of these cover points defined earlier.

The rest of the paper elaborates on each method, applies experimentally the two methods on a case study of the state machines of the embedded multimedia card standard protocol eMMC [13], and evaluates each method. This evaluation guides for the use model of the cover directive and the cover group methods, and state advantages of each.

II. DEFINITIONS AND NOTATIONS

The following notational conventions are used throughout the paper. Boolean operators are denoted by bolded lowercase italics and, or, xor, not. FSM states are denoted by bolded capital letters STANDBY, SLEEP. FSM arc transition variables or conditions are denoted by Bolded Italic capital letters CMD. Code segments are denoted by italics, and written in SystemVerilog language syntax unless noted otherwise.

III. PROPOSED METHODS FOR IMPLEMENTING FSM ARC COVERAGE

A. First Method: Cover directives

The SystemVerilog assertions constructs are used in this method to define the properties which express all the different arcs of a state machine. An arc can be described by its initial state, final state and the input condition value that caused the state transition. For example, the following property describes a state transition from STANDBY to SLEEP that is caused by the variable CMD taking the value of 5. This is a specific arc from state STANDBY to state SLEEP. There can be other arcs, i.e. other input values or other conditions, that lead to the same state transition. However, those other arcs are not described and hence not covered by the below property.

property STANDBY_SLEEP_CMD5 ;
   @(posedge clk)
   ((state == STANDBY) |=> ((state == SLEEP) && (cmd == 5) ) ) ;
endproperty

The property uses the non-overlapped implication operator (|=>) to describe the state transition [14]. The antecedent expression (the expression before the implication operator) is a simple non temporal condition that checks the value of the current state. The consequent expression (the complete expression after the implication operator) is an and operation between the state variable and the input variable that caused this transition. The non-overlapped implication means that when the antecedent expression occurs, the consequent expression will be evaluated one clock cycle later. The implementation of the property can be coded in several ways; for example, the ##1 operator can be used.

Note that one might think that the property should have the input condition in the antecedent expression, i.e. current state && input |=> next state. However, due to the scheduling semantics of Systemverilog and when expressions in properties get sampled, the syntax shown above shall result in the correct implementation of the property as intended.

Since a property describes one arc in the state machine, the number of properties required to describe the complete space of arcs in the state machine is equal to the actual number of arcs between all adjacent states of the state machine. This number will linearly grow versus the number of states given that there is only one path from one state to another. The number will grow in an exponential fashion if the number of paths between adjacent states is more than one.

The next phase after the properties declaration is to define specific actions for each defined property. These actions are defined in SystemVerilog by the three verification directives: assert, assume and cover. Since the main concern in this case is coverage, then the cover directive will be applied to each property. For example,

ARC1: cover property (STANDBY_SLEEP_CMD5);

B. Second Method: Cover groups

The functional coverage construct, “covergroup”, of SystemVerilog is used in this method. The covergroup construct is built by defining one or more cover points as well as one or more cross coverage targets between the cover points. A cover point is defined to cover an integral expression or a transition in the values of an expression. It contains a set of bins, user-defined or automatically generated, associated with certain or all values of the expression. A cross is used to specify cross coverage between two or more cover points or variables.

Cross coverage will be used to describe the arc coverage. The complete list of arcs between two adjacent states is the cross product of the state transition and all the values of the variables or conditions causing this transition. This can be implemented using the cross coverage between two cover points. The first cover point covers the transition from the initial state to the final state. The second cover point covers all the values of the variable or condition that can cause the state transition. Crossing these two cover points will automatically produce bins that cover the state transition and all the values of the input variable that could cause this transition. This presents coverage of all the arcs from the initial state to the final state.

Consider the simple state machine shown in figure 1. The FSM consists of three states, two state transitions, one from STANDBY to SLEEP when the variable cmd takes values from 1 to 12 and another from TRANSFER to STANDBY when cmd is within the range from 11 to 22, and hence it contains 24 arcs. The implementation of the arc coverage model for this state machine using the cover directive method requires a cover group declaration with two cover points and one cross.

Figure 1: Simple 3-state 24-arc FSM

The state transition cover point is constructed by defining bins which cover e ach and every state transition of interest. It is recommended that each state transition is put in one bin. This will enable an elaborated cross operation performed in the final stage. For example, the below state transition cover point has two bins, one that describes the transition from STANDBY to SLEEP, and the second describes the transition from TRANSFER to STANDBY.

state: coverpoint state
{
  bins stdby_to_sleep = ( STANBDY => SLEEP );
  bins tx_to_stdby = ( TRANSFER => STANBDY );
}

The variable values cover point will include all the values of the variable that can cause the state transitions. It is recommended that values causing one transition from one state to another be grouped into one bin. This may result in values being repeated in some bins, the different state transitions according to the initial state. Grouping the values into bins this way will also facilitate the cross operation. For example, the below cover point includes two bins covering values 1 through 12 and 11 through 22 of the variable state transition, i.e. STANDBY to SLEEP, and bin b covers the values that cause another state transition, i.e. TRANSFER to STANDBY. Note that the cmd values 11 and 12 are included in both bins, and this is because these values can cause different state transitions depending on the initial state. For example, if the current state is STANDBY and cmd takes the value 11, then the next state will be SLEEP, but if the current state is TRANSFER, the next will be STANDY, given that cmd has the same value of 11. The other thing to note is that the bins are defined as arrays with automatic number of locations defined by the values to be covered. This is because we are interested in each and every value, and not just the range of values.

cmd: coverpoint cmd
{
bins a[] = {[1:12]};
bins b[] = {[11:22]};
}

By default tools automatically generate bins for the cross coverage. These bins will cover all the possible combinations of cross coverage between the two cover points. For example, there will be bins covering all occurrences of the state transition STANDBY to SLEEP with all values of cmd from 1 to 22. This is more information than what arc coverage is interested in. Arc coverage between states STANDBY and SLEEP is only concerned with values of cmd from 1 to 12. Hence, only a subset of the automatically generated bins is useful. Therefore, specific user-defined bins are required to be defined in order to limit the combinations from the complete space to the valid combinations which describe particularly the possible paths from one state to another. This is a mechanism to guide the bins’ automatic generation process, such that it will ignore the bins that are not of interest for the coverage goals. This makes use of the ignore_bins construct which specifies the set of bins that is out of the scope of the FSM arc coverage, and will be excluded from the coverage measurements.

The ignore_bins bin is constructed to define the irrelevant combinations of state transitions, and condition values to the possible arcs of that particular transition. For example, any bins other than cmd.a should not be associated with the state transition specified in the bin state.stdby_to_sleep. Hence, the ignore_bins bin will include the expressions binsof(state.stdby_to_sleep) && (! binsof (cmd.a)). Note that the negation operator is used with cmd.a to indicate that any other bins should be ignored. The same concept will apply to all the other state transitions. Finally, the ignore_bins bin will be an or operation of all the resulting statements as shown below.

cmdXstate: cross cmd, state
{
    ignore_bins ignore = binsof(state.stdby_to_sleep) && (!binsof (cmd.a)) ||
b                   insof(state.tx_to_stdby) && (!binsof (cmd.b));
}

In general application, the first coverpoint can be expanded to include all the different state transitions, each in a separate bin. Also, the second coverpoint can be expanded to include bins which cover all conditions’ values that cause all possible state transitions. Bins in the second coverpoint may have overlapping values; these are the values that can cause different state transitions depending on the initial state. Finally, the covergroup will be sampled on the appropriate edge of each clock.

IV. CASE STUDY

This section presents an experimental case study conducted using the two methods introduced earlier. The experimental study has been conducted on a complex FSM of the embedded multimedia card standard protocol. The eMMC standard has five variants of the FSM in the five variants of the bus operation modes: data transfer mode, boot mode, card identification mode, interrupt mode and inactive mode. The testbench environment is a simple module-based environment in which an eMMC card RTL model is instantiated and random stimulus is applied to it. The section also presents the experimental results of cover directive and cover groups methods application on the eMMC FSM along three variants of the eMMC bus operation modes.

A. eMMC Data Transfer FSM

The data transfer state machine depicted in figure 2 contains 40 unique paths between adjacent states (arcs) and 18 state transitions.

Fig. 2 – The eMMC data transfer mode FSM

In order to model the coverage of this state machine using the cover directive method, 40 different properties are defined and a cover directive for each property will be applied. Below are three of the properties for illustration only, the complete list would contain 37 more. Each property describes one path from a state to another. The antecedent expression checks the value of the state variable to evaluate the current state. The consequent expression is the and between the value of the final state variable and the input variable that caused this transition to check a certain arc’s coverage.

property SEND_TRANSFER_CMD12 ;
  @(posedge clk)
     ((state == SENDING_DATA) |=> ((state == TRANSFER) && (cmd == 12) ) ) ;
endproperty

property TRANSFER_SEND_CMD8 ;
  @(posedge clk)
     ((state == TRANSFER) |=> ((state == SENDING_DATA) && (cmd == 8) ) ) ;
endproperty

property TRANSFER_TRANSFER_CMD816 ;
   @(posedge clk)
       ((state == TRANSFER) |=> ((state == TRANSFER) && (cmd == 16) ) ) ;
endproperty

cover property (SEND_TRANSFER_CMD12);
cover property (TRANSFER_SEND_CMD8);
cover property (TRANSFER_TRANSFER_CMD816);

 

On the other hand, using the cover groups method will result in code similar to that snippet shown below, which will cover all the possible paths when applied to the full state machine. The CMD cover point covers the values of the variable cmd which causes the state transitions, grouped such that each bin contains all the values that cause one state transition. The STATE cover point covers the state variable state, and hence covers the state transitions. Finally, the cross coverage has one ignore_bins bin which ignores the crosses that are out of the scope of arc coverage of the FSM under analysis.

covergroup data_transfer_fsm ;
CMD: coverpoint cmd
{
    bins p1[] = {12};
    bins p2[] = {11, 17, 18, 30, 56};
    bins p3[] = {16, 23, 35, 36};
}
STATE: coverpoint state
{
    bins s1 = ( SENDING_DATA => TRANSFER );
    bins s2 = ( TRANSFER => SENDING_DATA );
    bins s3 = ( TRANSFER => TRANSFER );
}
path_cov: cross CMD, STATE
{
   ignore_bins ignore = binsof (STATE.s1) && ( ! binsof (CMD.p1)) ||   binsof (STATE.s2) && ( !
            binsof (CMD.p2)) || binsof (STATE.s3) && ( ! binsof (CMD.p3));

}
endgroup

B. eMMC Card Identification mode FSM

The card identification state machine shown in figure 3 contains 11 unique paths between adjacent states (arcs) and 6 state transitions.

Figure 3 – The eMMC card identification mode FSM

Using the cover directives method, 6 different properties are defined and a cover directive for each property will be applied. Below are 2 of the properties for illustration only, the complete list would contain 9 more.

property prop_fsm_IDLE_READY_CMD2 ;
   @(posedge clk)
      ((main_card_state == IDLE) |=>
      ((main_card_state == READY) && (cmd_identity == CMD1_SEND_OP_COND))) ;
endproperty

property prop_fsm_READY_IDENTIFICATION_CMD2 ;
    @(posedge clk)
         ((main_card_state == READY) |=>
         ((main_card_state == IDENTIFICATION) && (cmd_identity == CMD2_ALL_SEND_CID))) ;
endproperty

fsm_IDLE_READY_CMD2 : cover property (prop_fsm_IDLE_READY_CMD1);
fsm_READY_IDENTIFICATION_CMD2 : cover property (prop_fsm_READY_IDENTIFICATION_CMD2);

Using the cover groups method will result in code similar to that snippet shown below, which will cover all the possible paths when applied to the full state machine. The CMD cover point covers the values of the variable cmd which causes the state transitions, grouped such that each bin contains all the values that cause one state transition. The STATE cover point covers the state variable state, and hence covers the state transitions. Finally, the cross coverage has one ignore_bins bin which ignores the crosses that are out of the scope of arc coverage of the FSM under analysis.

covergroup card_identification_fsm_coverage;
CMD: coverpoint cmd
{
   bins p1[] = {1};
   bins p2[] = {2};
}
STATE: coverpoint state
{
    bins s1 = ( IDLE => READY );
    bins s2 = ( READY => IDENTIFICATION );
}
path_cov: cross CMD, STATE
{
    ignore_bins ignore = binsof (STATE.s1) && (! binsof (CMD.p1)) || binsof (STATE.s2) && (! binsof
(CMD.p2));
}
endgroup

C. eMMC Interrupt mode FSM

The data transfer state machine depicted in figure 4 contains 7 unique paths between adjacent states (arcs) and 3 state transitions.

Figure 4 – The eMMC Interrupt mode FSM

To model the coverage of this state machine using the cover directive method, 7 different properties are defined and a cover directive for each property will be applied. Below are 2 of the properties for illustration only, the complete list would contain 5 more.

property prop_fsm_STANDBY_STANDBY_CMD4 ;
   @(posedge clk)
      ((main_card_state == STANDBY) |=>
           ((main_card_state == STANDBY) && (cmd_identity == CMD4_SET_DSR))) ;
endproperty

property prop_fsm_WAITIRQ_STANDBY ;
    @(posedge clk)
          ((main_card_state == WAIT_IRQ |=> (main_card_state == STANDBY) )) ;
endproperty

fsm_STANDBY_STANDBY_CMD4 : cover property (prop_fsm_STANDBY_STANDBY_CMD4);
fsm_WAITIRQ_STANDBY : cover property (prop_fsm_WAITIRQ_STANDBY);

On the other hand, using the cover groups method will result in code similar to that snippet shown below, which will cover all the possible paths when applied to the full state machine.

covergroup interrupt_fsm_coverage;
CMD: coverpoint cmd
  {
     bins p1[] = {9, 10, 39};
     bins p2[] = {40};
}
STATE: coverpoint state
{
   bins s1 = ( STANDBY => STANDBY);
   bins s2 = ( STANDBY => WAIT_IRQ );
}
path_cov: cross CMD, STATE
{
    ignore_bins ignore = binsof (STATE.s1) && (! binsof (CMD.p1)) || binsof (STATE.s2) && (! binsof
(CMD.p2));
}
endgroup

The following table summarizes the statistical numbers for each method versus the experiments conducted on the three different FSMs; the data transfer mode, card identification mode, and interrupt mode.

Table1- Methods Statistics versus eMMC FSMs

V. FSM FUNCTIONAL COVERAGE METHODS EVALUATION

This section presents an evaluation of the two methods; cover directive, and the cover groups. In general, there is no one method to adopt, thus the evaluation will show that each method is suitably used in specific situations.

The cover directive technique described above may be used when the state machine is simple, or contains few arcs. As the number of arcs increase the code will become very complex and error prone since the number of SVA properties that need to be described is equal to the number of arcs between adjacent states in the state machine.

In addition, SystemVerilog does not allow SVA constructs, such as properties, to be defined inside classes. In the advanced verification methodologies, class-based object oriented capabilities provided by the class construct in SystemVerilog, enables reuse, and scalability. Therefore, the cover directive technique cannot be implemented within a class-based code.

On the other hand, cover groups have a well defined use model within the class construct which fits well with the current concepts of functional verification. Moreover, the code complexity is much less in the covergroups technique and doesn’t grow tremendously with the number of paths as is the case with the cover directive technique.

The advantages of using the cover directive method are that, it can be implemented in assertion languages other than SystemVerilog, for example Property Specification Language (PSL); it can be used for formal verification, and model checking [15]. The same exact method can be coded in PSL and will achieve the same behavior. This will be very beneficial for designs written in VHDL for example. PSL statements can be embedded in code written in either Verilog or VHDL, since there are flavors of PSL for both languages. However, the covergroups method is limited to code written in SystemVerilog or Verilog, although the code needs to be compiled as SystemVerilog, which is something simulators usually support.

The following code shows the same method defined earlier but implemented in PSL and embedded in VHDL code.

-- psl default clock is (clk'event and clk= '1');

-- psl property STANDBY_SLEEP_CMD5 is

-- always ({state = STANDBY} |=> {(state = SLEEP and cmd = 5)});

-- psl cover STANDBY_SLEEP_CMD5;

The same set of properties can be used for formal verification, and model checking as it models the behavior of the FSM in terms of properties.. Those properties when used in functional verification can be used to assert they hold as well as are covered during the simulation time. They can be used by the formal tools to check they hold and produce counter examples in case of firings. The covergroups technique cannot be used in formal verification or model checking

VI. CONCLUSION

FSM arc coverage is important for coverage closure of an FSM behavior in addition to the typical entire states’ transitions. Conventional methods for FSM arc coverage typically use the structural code coverage tools to infer the arc coverage measurements from the simulation results. This paper has presented two new methods for FSM arc coverage in the functional coverage domain rather than the conventional code coverage. The new methods leverage the cover directives, and cover groups constructs in the SystemVerilog language to enable integration in functional verification methodologies and reuse across the multi-abstraction levels. The two proposed methods have been applied extensively to an experimental case study represented by the eMMC standard protocol finite state machines that model the eMMC different bus operation modes. Code snippets are presented to illustrate samples for implementation. The two proposed methods have been evaluated based on the experimental results to state the suitable use model for each.

VII. REFERENCES

[1] Janick Bergeron, Writing Testbenches: Functional verification of HDL models, 2nd edition, Springer, 2003

[2] Andrew Piziali, Functional Verification Coverage Measurement And Analysis, Kluwer, 2004.

[3] Wang, T.-H. and Tan, C. G., “Practical Code Coverage for Verilog”, 4th International Verilog HDL Conference, 1995, 99-104.

[4] Wang, T.-H. and Edsall, T., “Practical FSM Analysis for Verilog”, Verilog HDL Conference and VHDL International Users Forum, 1998

[5] Frank Ghenassia, Transaction-Level Modeling with SystemC: TLM Concepts and Applications for Embedded Systems by, Springer, 2005

[6] Man-Yun Su ; Che-Hua Shih ; Juinn-Dar Huang ; Jing-Yang Jou, “FSM-Based Transaction-Level Functional Coverage for Interface Compliance Verification”, Design Automation, 2006

[7] Chien-Nan Jimmy Liu ; Jing-Yang Jou, “An Efficient Functional Coverage Test for HDL Descriptions at RTL”, Computer Design, 1999. (ICCD '99) International Conference.

[8] IEEE Standard for SystemVerilog 1800-2009

[9] IEEE 1850-2005, Property Specification Language.

[10] Mark Glasser, Open Verification Methodology Cookbook, Springer, 2009

[11] Janick Bergeron, et al, Verification Methodology Manual for SystemVerilog, Springer, 2005

[12] Harry D. Foster, et al, Assertion-Based Design, Kluwer, 2004

[13] Embedded Multimedia Card (e.MMC), JESD84-A44, March 2009.

[14] Ben Cohen, et al, SystemVerilog Assertions Handbook, 2nd Edition 2010.

[15] Rolf Drechsler, Advanced Formal Verification, Kluwer, 2010.