TOC PREV NEXT INDEX  

Appendix G

Creating Properties - Worked Examples

 

This section presents some examples of how to create a set of files that can be used to check the dynamic property aspects of a simple finite state machine. It is assumed that you have already worked through Appendix F and have become familiar with using VN-Property DX to perform dynamic property checking.

Getting Organized

The following files can be obtained as a single file in `zip' format from TransEDA's web site at: www.transeda.com/vmm/

Create a directory (e.g. my-properties) on your system and then unpack the complete set of files that you obtained from TransEDA into that area.

fsm_test.v // Verilog test bench
fsm.v // Verilog code for the finite state machine
clk_gen.v // Very simple 50-50 mark space ratio clock generator
pc_collection.spec // Specifications collections file
doit.modelsim // Script to perform functional coverage via the CLI

Please take a few moments to familiarise yourself with the contents of these files.

You should also have an additional set of files with the suffix .beh in this directory. These files contain the definitions for the various behaviors that are described in the remainder of this section.

Background

A FSM is an electronic circuit that has a predictable or finite state that is based on a combination of the circuit's previous state and the circuit's current set of inputs. If you analyse the operation of today's electronic products you will discover that many of them are based on the concept of a finite state machine. A "hole in the wall" cash dispenser, a pedestrian controlled zebra crossing, a telephone answering machine, the fuel consumption distance/range recorder in a car are all examples of FSM based products.

Overview

The block diagram below shows part of the control system used to dispense hot drinks in a vending machine. It consists of a number of push buttons which are used to select the particular type of beverage (e.g. tea, coffee or hot chocolate) and additives (e.g. milk and/or sugar) required by the user. The state of the various push buttons is sensed by the control unit and used to operate a number of solenoids and pumps that heat the water and add the ingredients to the plastic cup. A set of indicator lights (also driven by the control unit) gives the user a visual indication of what is happening and when the drink is available for collection. A power-on reset signal is used to force the control unit into a known state when the vending machine is first switched-on.

Figure G-1

The state diagram, shown below, defines the five possible states of the FSM and identifies the input conditions that cause the FSM to move from one state to another. It should be noted that the FSM will only make a change of state on the positive going edge of the clock pulse.

Figure G-2

Circular Tour

The first behavior we are going to look at is a test to check one of the circular tours around the FSM. We will assume that the FSM starts from state S0 and visits states S1, S2 and S3 (in that order) before returning to state S0. In this first example you can assume that the FSM is only allowed to loop on state S0. (i.e. it does not loop on any of the intervening states.) So the Perl quantifier list is: S0+ S1 S2 S3 S0+

Figure G-3 shows a listing of the file called CircularTour.beh. This example illustrates the use of the function Vector::integer which is used to determine the numerical value of the `state' register.

You can check the operation of this behavior by simulating the design (fsm.v and clk_gen.v) with the test bench (fsm_test.v). You can either do this with VN-Property DX using the GUI or via the CLI using the script called doit.modelsim. In either case you will need to ensure that the appropriate behavior (i.e. CircularTour.beh) is called-up within the pc_collection.spec file. The results file should indicate that this particular behavior has been matched at least once.

Looping on S2

The next behavior that we are going to look at checks that the FSM starts from state S0 and visits state S1 before looping for a number of clock cycles on state S2. The Perl quantifier list for this behavior is: S0+ S1 S2{2,} Figure G-4 shows a listing of the file called LoopingOnS2.beh. This particular behavior uses a short subroutine called get_state() to return a text string that indicates the state of the `state' register.

Counting the number of loops

The next behavior, as shown in Figure G-5, is a slightly modified version of the LoopingOnS2 behavior to count the actual number of times that S2 looped. It makes use of a User Data Block (UDB) and a user defined counter called S2Counter to record the actual number of times S2 looped.

This behavior also demonstrates how information that has been collected in the UDB can be printed out when a certain event has occurred.

Matching two lower level sequences

The next behavior, as shown in Figures G-6 to G-8, is designed to match two lower level behaviors and is implemented using three files. The first file called TopLevel.beh uses the match subsequence function (i.e. match_subseq) to check that the following two tours have been performed.

S0+ S1 S2+ S0+
S0+ S4 S3+ S0+

Using a Signals file

The final behavior, as shown in Figure G-10, that we will inspect makes use of a signals file to provide the user with a layer a of abstraction between the names of signals used within the properties and the names of signals used in the actual HDL implementation. It is effectively a mapping file. This means that if a signal name in the HDL implementation was changed then only the name in the signals file needs to be altered. This avoids having to go through every line in a behavior file looking for an out-of-date signal name.

Listing for a circular tour around the finite state machine.

package CircularTour; # Filename is “CircularTour.beh”
#define_clock fsm clk
use vars qw(@ISA);
@ISA = qw(Sequence);
sub begin
{
my $self = shift;
return
{
‘steps’ =>
[
{
‘test’ => sub { Vector::integer(@fsm:state) == 0 },
‘quantifier’ => ‘+’
},

{
‘test’ => sub { Vector::integer(@fsm:state) == 1 },
‘quantifier’ => 1
},

{
‘test’ => sub { Vector::integer(@fsm:state) == 2 },
‘quantifier’ => 1
},

{
‘test’ => sub { Vector::integer(@fsm:state) == 3 },
‘quantifier’ => 1
},

{
‘test’ => sub { Vector::integer(@fsm:state) == 0 },
‘quantifier’ => ‘+’
},
]
};
}
1; # End of package file (must return 1)

Figure G-3

Listing to check looping on state S2 within the finite state machine.

package LoopingOnS2; # Filename is “LoopingOnS2.beh”
#define_clock fsm clk
use vars qw(@ISA);
@ISA = qw(Sequence);

sub begin
{
my $self = shift;
return
{
‘steps’ =>
[
{
‘info’ => ‘Waiting for state S0’
‘test’ => sub { ($self->get_state() eg ‘S0’) },
‘quantifier’ => ‘+’
},

{
‘info’ => ‘Waiting for state S1’
‘test’ => sub { ($self->get_state() eg ‘S1’) },
‘quantifier’ => 1
},

{
‘info’ => ‘Waiting for state S2’
‘test’ => sub { ($self->get_state() eg ‘S2’) },
‘quantifier’ => ‘2,’
},
]
};
}

sub get_state
{
my $self = shift;
if (Vector::integer(@fsm:state) == 0 {return ‘S0’}
elsif (Vector::integer(@fsm:state) == 1 {return ‘S1’}
elsif (Vector::integer(@fsm:state) == 2 {return ‘S2’}
elsif (Vector::integer(@fsm:state) == 3 {return ‘S3’}
elsif (Vector::integer(@fsm:state) == 4 {return ‘S4’}
}
1; # End of package file (must return 1)

Figure G-4

Listing to count how many times the finite state machine looped on S2.

package CountS2Loops # Filename is “CountS2Loops.beh”
#define_clock fsm clk
use vars qw(@ISA);
@ISA = qw(Sequence);

sub begin
{ my $self = shift;
return
{ ‘initial_data’ => { ‘S2Counter’ => 0 },
‘steps’ =>
[
{ ‘test’ => sub { ($self->get_state() eq ‘S2’) }, ‘quantifier’ => 1},
{ ‘test’ => sub { ($self->get_state() eq ‘S2’) }, ‘quantifier’ => ‘+’,
‘post_action’ => sub
{ my ($user_data, $test_result) = @_;
if ($test_result) { $user_data->{‘S2Counter’} += 1; }
}
},

{ ‘test’ => sub { ($self->get_state() ne ‘S2’) },
‘quantifier’ => ‘+’,
‘post_action’ => sub
{ my $user_data = shift;
my $counter_value = $user_data->{‘S2Counter’};
print “\n”;
print “The number of times S2 looped was $counter_value\n”;
print “\n”;
return 1;
}
}
]
};
}

sub get_state
{
my $self = shift;
if (Vector::integer(@fsm:state) == 0 {return ‘S0’}
elsif (Vector::integer(@fsm:state) == 1 {return ‘S1’}
elsif (Vector::integer(@fsm:state) == 2 {return ‘S2’}
elsif (Vector::integer(@fsm:state) == 3 {return ‘S3’}
elsif (Vector::integer(@fsm:state) == 4 {return ‘S4’}
}
1; # End of package file (must return 1)

Figure G-5

Listing to match two lower level sequences. Three files are needed to solve this particular situation. A top level sequence that calls the two lower level sequences.

The top level sequence is shown below.

package TopLevel # Filename is “TopLevel.beh”
#define_clock fsm clk
use vars qw(@ISA);
@ISA = qw(Sequence);

# Load the lower-level sub-sequence packages
use Tour0120;
use Tour0430;

sub begin
{
my $self = shift;

# Instantiate the sub-sequences
$self->{‘0120’} = Tour0120->new();
$self->{‘0430’} = Tour0430->new();
return

# Sequence data structure
{
‘steps’ =>
[
{
‘test’ =>
sub {
$self->match_subseq
(
$self->{‘0120’}, $self->{‘0430’}
)
},
‘quantifier’ => ‘+’
}
]
};
}
1; # End of TopLevel package file (must return 1)

Figure G-6

Listing of the lower level sequence to check the circular tour S0+ S1 S2+ S0+

package Tour0120 # Filename is “Tour0120.beh”
#define_clock fsm clk
use vars qw(@ISA);
@ISA = qw(Sequence);

sub begin
{
my $self = shift;
return
{
‘steps’ =>
[
{
‘test’ => sub { ($self->get_state() eq ‘S0’) }, ‘quantifier’ => ‘+’
},

{
‘test’ => sub { ($self->get_state() eq ‘S1’) }, ‘quantifier’ => 1
},

{
‘test’ => sub { ($self->get_state() eq ‘S2’) }, ‘quantifier’ => ‘+’
},

{
‘test’ => sub { ($self->get_state() eq ‘S0’) }, ‘quantifier’ => ‘+’
},
]
};
}

sub get_state
{
my $self = shift;
if (Vector::integer(@fsm:state) == 0 {return ‘S0’}
elsif (Vector::integer(@fsm:state) == 1 {return ‘S1’}
elsif (Vector::integer(@fsm:state) == 2 {return ‘S2’}
elsif (Vector::integer(@fsm:state) == 3 {return ‘S3’}
elsif (Vector::integer(@fsm:state) == 4 {return ‘S4’}
}

1; # End of package file (must return 1)

Listing G-7

Listing of the lower level sequence to check the circular tour S0+ S4 S3+ S0+

package Tour0430 # Filename is “Tour0430.beh”
#define_clock fsm clk
use vars qw(@ISA);
@ISA = qw(Sequence);

sub begin
{
my $self = shift;
return
{
‘steps’ =>
[
{
‘test’ => sub { ($self->get_state() eq ‘S0’) }, ‘quantifier’ => ‘+’
},

{
‘test’ => sub { ($self->get_state() eq ‘S4’) }, ‘quantifier’ => 1
},

{
‘test’ => sub { ($self->get_state() eq ‘S3’) }, ‘quantifier’ => ‘+’
},

{
‘test’ => sub { ($self->get_state() eq ‘S0’) }, ‘quantifier’ => ‘+’
},
]
};
}

sub get_state
{
my $self = shift;
if (Vector::integer(@fsm:state) == 0 {return ‘S0’}
elsif (Vector::integer(@fsm:state) == 1 {return ‘S1’}
elsif (Vector::integer(@fsm:state) == 2 {return ‘S2’}
elsif (Vector::integer(@fsm:state) == 3 {return ‘S3’}
elsif (Vector::integer(@fsm:state) == 4 {return ‘S4’}
}

1; # End of package file (must return 1)

Figure G-8

Listing to check the circular tour S0+ S1 S2 S3 S0+

This sequence uses a signals file to map signal names to the HDL implementation.

package MySignalsTour # Filename is “MySignalsTour.beh”
use vars qw(@ISA);
@ISA = qw(Sequence);

use FSMsignals;

sub begin
{
my $self = shift;
return
{
‘steps’ =>
[
{ ‘test’ => sub { FSMsignals::Idle() == 1 }, ‘quantifier’ => ‘+’ },

{ ‘test’ => sub { FSMsignals::Coffee() == 1 }, ‘quantifier’ => 1 },

{ ‘test’ => sub { FSMsignals::Milk() == 1 }, ‘quantifier’ => 1 },

{ ‘test’ => sub { FSMsignals::Sugar() == 1 }, ‘quantifier’ => 1 },

{ ‘test’ => sub { FSMsignals::Idle() == 1 }, ‘quantifier’ => ‘+’ },
]
};
}
1; # End of package file (must return 1)

Figure G-9

Layout of the signals file.

package FSMsignals # Filename is “FSMsignals.beh”

#define_clock fsm clk

# Basic signals...
sub Idle { (Vector::integer(@fsm:state) == 0) }
sub Coffee { (Vector::integer(@fsm:state) == 1) }
sub Milk { (Vector::integer(@fsm:state) == 2) }
sub Sugar { (Vector::integer(@fsm:state) == 3) }
sub Tea { (Vector::integer(@fsm:state) == 4) }

1; # End of FSMsignals package

Figure G-10



    TOC PREV NEXT INDEX  
Copyright (c) 2002
Teamwork International and TransEDA Limited
http://www.transeda.com
Voice: (408) 335-1300
Fax: (408) 335-1319
info@transeda.com