Homework 4: Design a circular buffer with NuSMV

Due Monday, May 24, 2004

This assignment is to design and verify a circular buffer using NuSMV. The description will be pretty close to the actual hardware design.

I encourage you to discuss this problem and your solutions with others, but I don't want you to share code. So don't borrow from the text of others solutions.

Written homework questions about CTL

Quadruple-check your answers to these questions. It is extremely easy to make a mistake.

The weak until operator is like until, except A[f u g] allows infinite paths where no state satisfies "g" so long as every state satisfies "f". The weak until can be expressed using only the constructs I have described in lecture. What is the abbreviation? Your answer should only use one temporal operator .
Write a CTL specification for the following simple behavior: There are two Boolean signals, P and Q. Initially, both are 0. Then P goes to 1 and back to 0. Then Q goes to 1 and back to 0. P and Q continue to do this alternately forever.

What to do for the programming problem

Write a FIFO description in NuSMV, and verify it using the data independence trick below (values 0, 1, and 2).

Do not use the PROCESS or TRANS constructs in NuSMV. Do not use temporal operators in fairness constraints. Fairness constraints should be simple propositional formulas.

How to turn in your answers.

Create a public directory on the epic systems called cs356-hw4 and email me a message when you are done with the problem with the relative path name of the directory with your solution. The directory should contain your formulas (answers to first two problems), your NuSMV file(s), and a description of the most interesting bug you found in your circular buffer (if any).

Circular buffer

First-in/first-out (FIFO) queues are used all over the place in hardware designs. A common implementation of a FIFO in hardware (as well as software) is the so-called circular buffer. A circular buffer is an array, with head and tail pointers. The head pointer is the index of the oldest queue entry, which will be the next to be removed, and the tail pointer points to the next free entry in the array (where the next value will be inserted). The circular buffer implementation has the advantage of requiring more-or-less constant-time insertion and removal of values.

The circular buffer you should design should have three "input side" signals for interfacing to the producer of data: load, full, and data_in, and three "output side" signals for interfacing to the consumer of data, unload, empty, and data_out.

The protocol on the producer (input) side is that load can be set to 1 at any time when full = 0 to load new data into the FIFO. When load = 1, data_in is stored in the appropriate array location at the next clock edge.

On the consumer (output) side, whenever the FIFO is nonempty, data_out is set to the oldest value in the FIFO. unload can be set to 1 whenever empty = 0; on the next cycle, data_out will be set to the next oldest value (and the previous value will be lost forever).

The assignment

The assignment is to describe a circular buffer implementation of the FIFO in the NuSMV language, and formally verify it using NuSMV.

Describing the FIFO

Unlike Murphi, the NuSMV language does not make it easy to make descriptions scalable. In particular, arrays can only have constant indices. You will basically need to assign each array element separately, and cut and paste to increase the number of array elements. I.e., to assign to an array element, when you would say in a normal programming language,

data[i] := newvalue;

you have to say something like this in NuSMV:

data[0] := case
             i = 0 : newvalue;
	     1 : data[0];
	   esac;

data[1] := case
             i = 1 : newvalue;
	     1 : data[1];
	   esac;

data[2] := case
             i = 1 : newvalue;
	     1 : data[2];
	   esac;

...

For reading out of an array, the following type of kludge works:

data_out := case
	      head = 0: data[0];
	      head = 1: data[1];
	      head = 2: data[2];
	      head = 3: data[3];
	      1: 0;
	     esac;

Modelling the environment

The environment of the FIFO consists of a producer, which connects to the input-side signals, and a consumer, which connects to the output-side signals. The producer should not raise the load signal unless full=0, and the consumer should not raise unload unless empty=0.

In addition, the producer and consumer need to do some bookkeeping to make specification possible. Somehow, data must be tracked from the producer to the consumer to see if it is lost, duplicated, or reordered.

Data independence

It is not easy to write a full specification for the FIFO in NuSMV. The FIFO has the interesting property that it is data independent. Intuitively, this means that it just moves data around without looking at it. In particular, there are no conditionals that depend on the data values. Also, the specification must be a conjunction of properties that check whether data values are equal. For example, a property that says that a data value received is the same that is sent might be written in this form.

There is a theorem, due to Pierre Wolper, that says that, to verify a data independent system, it is only necessary to use two data values. Furthermore, the data values are used in a special way. In a data independent system, all data values must come from data sources, such as inputs. Let us assume that there is only one source. It is sufficient to verify the system when the source generates the same default value (e.g. 0) almost all the time, so long as it nondeterministically chooses to generate exactly one non-default value (e.g. 1). By "nondeterministically generates", I mean that the source at any point can inject 1 (any value can be the 1).

Since a data independent system just moves data around, the only errors are if the data ends up in the wrong place at the wrong time. Since formal verification will exhaustively examine all of the possible ways to inject 1, it will check whether the 1 ends up some place where there should have been a 0, or vice versa.

Here is a somewhat more formal argument: Suppose a system there is a reachable error state, so there is a path to the error state from a start state. We construct a new path that can happen when all injected values are 0 except for exactly one 1.

Find the two values in the specification that were supposed to be equal but aren't. Pick one of these values, find where it first appeared in the trace, and inject a "1" instead. Find where all other values first appear, and inject "0" instead. The constructed sequence of states will be a path, because if q' is a next state of q in the original trace, the states obtained by replacing values will have the same relationship in the new trace. The last state of the new trace will be an error state, because the two data values that violated the specification by not being equal will still not be equal.

Unfortunately, this trick is not sufficient for a complete specification of the FIFO. It would be equally happy if you gave it a stack (a LIFO queue) instead of a FIFO (it should be easy to modify your FIFO to be LIFO if you want to give it a try). There are two properties that it misses:

The FIFO delivers data in the right order.
The FIFO can store 4 values.

The first property can be checked by using a default value of 0, then nondeterministically inserting a 1, possibly followed by more 0s, then nondeterministically inserting a 2, possibly followed by more 0s. The consumer should check that the 1 and 2 are not lost, duplicated, or received in the wrong order.

The second property could be checked by keeping track of the difference between the number of loaded and unloaded values, and making sure that full is high only when the difference is 4.

NuSMV guidelines

You may want to get a FIFO of size 1 working, the copy and edit the various parts to scale it up to a queue of size 4.

Getting and running NuSMV

It's available at http://nusmv.irst.itc.it/

Download the tar file for the latest version, untar it, and follow the directions. It compiled effortlessly on my linux system. There is a long user manual in the docs subdirectory.

Copyright © by David L. Dill, 1998-2004. All rights reserved. This material may be freely distributed for educational purposes, so long as (1) this copyright notice remains, (2) the notes are not modified in any way, and (3) no fee is charged. Other uses require the express written consent of the author.