Ring

Introduction

This example describes a clocked, three address ring. The addresses are numbered 0 to 2. Initially a token is at the address 0, and at each rising edge of the clock, it goes to the next address (modulo 3).

VHDL Description

entity RING is
  port(CLOCK: in BIT);
end;

architecture THREE of RING is
  signal AT_ZERO : BIT := '1';
  signal AT_ONE, AT_TWO : BIT := '0';
begin
  LOAD_ZERO: process
  begin
    wait until CLOCK = '1';
    AT_ZERO <= AT_TWO;
  end process LOAD_ZERO;
  LOAD_ONE: process
  begin
    wait until CLOCK = '1';
    AT_ONE <= AT_ZERO;
  end process LOAD_ONE;
  LOAD_TWO: process
  begin
    wait until CLOCK = '1';
    AT_TWO <= AT_ONE;
  end process LOAD_TWO;
end;

Specification

A property that is interesting to check is that at any given time the token is at one and exactly one address. The following specification states exactly this: 
specification SAFETY of EXAMPLES.RING(THREE) is
  commit token_at_one_place: ag ((AT_ZERO = '1') xor 
                                 (AT_ONE = '1') xor 
                                 (AT_TWO = '1'));
end specification;
Another interesting property that one would want to check is that the token actually circulates, so that it visits each address infinitely often. In other words, we want to check that for each address i it is always the case that the token will reach the address i in a finite time. This progress property can be valid if and only if the input signal CLOCK actually behaves like a clock and changes its value infinitely often. The following specification states these assumptions and commitments: 
specification PROGRESS of EXAMPLES.RING(THREE) is
  assume recurring (CLOCK = '0');
  assume recurring (CLOCK = '1');
  commit progress_0 : ag af (AT_ZERO = '1');
  commit progress_1 : ag af (AT_ONE = '1');
  commit progress_2 : ag af (AT_TWO = '1');
end specification;
An equivalent specification would be: 
specification PROGRESS2 of EXAMPLES.RING(THREE) is
  assume recurring (CLOCK = '0');
  assume recurring (CLOCK = '1');
  commit progress : ag(af(AT_ZERO = '1') and
                       af(AT_ONE = '1') and
                       af (AT_TWO = '1'));
end specification;

Comments

This simple example illustrates the use of the always recurring to express fairness constraints. Verification of progress properties will often require to assert such type of conditions on the inputs of the system. It is possible to scale this example to an arbitrary number of addresses. This is mostly interesting to study the evolution of the performances of CVC as the size of the design grows.

Examples: Latch  Ring  Stack 

Main sections: Introduction   Installation   Documentation   Examples

CV / Carnegie Mellon University / cmuvhdl@cs.cmu.edu / Revised December 1996