Stack

• Introduction
• VHDL description
• Specification
• Comments

Introduction

VHDL Description

entity STACK is
  port(PUSH, POP: in BOOLEAN;
       PUSH_RDY, POP_RDY: out BOOLEAN);
end STACK;

architecture THREE of STACK is
  type STATE_TYPE is (EMPTY, HALF, FULL);
  signal STATE: STATE_TYPE;
begin
  PUSH_RDY <= STATE /= FULL;
  POP_RDY <= STATE /= EMPTY;
  CONTROL: process
  begin
    if (STATE = EMPTY) then
      if PUSH then
        STATE <= HALF;
        wait until not PUSH;
      else
        wait until PUSH;
      end if;
    elsif (STATE = HALF) then
      if PUSH then
        STATE <= FULL;
        wait until not PUSH;
      elsif POP then
        STATE <= EMPTY;
        wait until not POP;
      else
        wait until PUSH or POP;
      end if;
    else
      if POP then
        STATE <= HALF;
        wait until not POP;
      else
        wait until POP;
      end if;
    end if;
  end process CONTROL;
end THREE;

Specification

specification BEHAVIOR of STACK(THREE) is
  assume always not (PUSH and POP);
  commit AT_EMPTY: ag((STATE = EMPTY) => a[(STATE = EMPTY) w PUSH]);
  commit PUSH_AT_EMPTY:
    ag((not PUSH and STATE = EMPTY) => ax (PUSH => af(STATE = HALF)));
  commit AT_FULL: ag((STATE = FULL) => a[(STATE = FULL) w POP]);
  commit POP_AT_FULL:
    ag((not POP and STATE = FULL) => ax (POP => af(STATE = HALF)));
end specification BEHAVIOR;

Comments

This example first illustrates the use of invariant assumptions: assume always followed by a condition that holds at each simulation cycle. Note that only signals of mode in can appear in such conditions. Here we state that we only consider the simulations where the commands PUSH and POP are exclusive.

Examples: Latch  Ring  Stack 

Main sections: Introduction   Installation   Documentation   Examples