In the IEEE Verilog 1364-2001 standard, an attribute is a way to add information to a Verilog object, statement or groups of statements that is tool-specific and does not affect simulation of that design. All Verilog-2001 attributes begin with the token (* and end with the token *). An attribute can be multi-line and is "attached" to the Verilog object, statement, or group of statements that is specified immediately beneath the attribute.

Covered uses the Verilog-2001 attribute for allowing users to specify coverage-specific information about embedded objects within a particular design. When an attribute is found, it is interrogated to see if it is a Covered attribute. If the attribute is a Covered attribute, its contents are parsed. If the attribute is not found to be a Covered attribute, it is ignored and parsing continues normally.

The rest of this chapter specifies the attributes that Covered is capable of handling, along with their use and syntax.

There are two ways that Covered currently allows the user to specify the location of and information about FSMs embedded in a particular design. The first way to specify an FSM is on the score command-line. The benefit to specifying the location of a state machine this way is that the source code does not need to be modified. The potential disadvantage to this method is that the FSM location and coverage information can get lost if the FSM is used in a different testbench (or even a different project if the FSM code is reused in a later project). For more information on specifying an FSM on the score command-line, please refer to Section 9.6, “Scoring FSMs”.

The second way that an FSM can be specified to Covered is through the use of the Verilog-2001 attribute. The advantages to using this method are that the FSM information specified in an attribute stays embedded in the design (for ease of reusing the FSM and still retaining information relevent to coverage). Additionally, at the current release of Covered, using attributes to specify an FSM is the only way to tell Covered what all of the valid states and state-transitions are for a specific FSM (the command-line specification does not allow for this). This provides a unique advantage of this method over the command-line method. The potential disadvantage of this method for specifying FSM information is that source code needs to be modified.

To learn how to specify an FSM attribute within a design, let's use an example of an FSM that is embedded in a design.

  module foo (
    input clk,
    input reset,
    input head,
    input tail,
    input valid
  );
      
    parameter STATE_IDLE = 2'b00,
              STATE_HEAD = 2'b01,
              STATE_DATA = 2'b10,
              STATE_TAIL = 2'b11;
                
    reg [1:0] state;
    reg [1:0] next_state;
      
    always @(posedge clock)
      state <= reset ? STATE_IDLE : next_state;
        
    always @(reset or state or head or valid or tail)
      begin
        case( state )
          STATE_IDLE: next_state = (valid & head) ?
                                     STATE_HEAD : STATE_IDLE;
          STATE_HEAD: next_state = (valid & tail) ?
                                     STATE_TAIL : STATE_DATA;
          STATE_DATA: next_state = (valid & tail) ?
                                     STATE_TAIL : STATE_DATA;
          STATE_TAIL: next_state = (valid & head) ?
                                     STATE_HEAD : STATE_IDLE;
        endcase
      end   
      
  endmodule 
        

This example shows an FSM that has an input FSM variable called "state" and an output FSM variable called "next_state". There are four states in the state machine that are represented with the parameters located in this module (STATE_IDLE, STATE_HEAD, STATE_DATA, STATE_TAIL). There are a total of eight (8) state transitions that this FSM can take. They are the following:

All attributes that specify information for an FSM are a comma-separated list of values that contain the following information:

To specify the FSM attribute in the above example, including input state, output state and all state transitions, the code would be modified to look like:

  (* covered_fsm, channel, is="state", os="next_state",
                           trans="STATE_IDLE->STATE_IDLE",
                           trans="STATE_IDLE->STATE_HEAD",
                           trans="STATE_HEAD->STATE_DATA",
                           trans="STATE_HEAD->STATE_TAIL",
                           trans="STATE_DATA->STATE_DATA",
                           trans="STATE_DATA->STATE_TAIL",
                           trans="STATE_TAIL->STATE_HEAD",
                           trans="STATE_TAIL->STATE_IDLE" *)
  always @(reset or state or head or tail or valid)
    ...