Latch

Jump to:

Introduction
VHDL description
Specification
Comments

Introduction

This example is a simple latch with a data input D, two control inputs LOAD and RESET, and two data output signals Q and QB. Whenever LOAD goes high, the value of D is fetched to Q, unless the RESET goes high. In this situation, Q is set to FALSE. QB is equal to the negation of Q.


VHDL Description

entity LATCH is
  port(D   : in BOOLEAN ;
       LOAD, RESET : in BOOLEAN;
       Q: out BOOLEAN := FALSE;
       QB: out BOOLEAN := TRUE);
end entity LATCH;

architecture D of LATCH is
begin
  process
  begin
    if RESET then
      Q <= FALSE ;
      QB <= TRUE ;
    elsif LOAD then
      Q <= D ;
      QB <= not D ;
    end if ;
    wait on LOAD, RESET ;
  end process;
end architecture D;



Specification

specification SAFETY of EXAMPLES.LATCH(D) is
  commit INVERSED_OUTPUTS: ag(Q xor QB);
  commit RESET: ag(RESET => ax(not Q));
  commit LOAD: ag((not LOAD) =>
                  ax((LOAD and not RESET) => ((D => ax(Q)) and
                                              ((not D) => ax(not Q)))));
end specification SAFETY;


The specification SAFETY contains three properties
of the latch:

 INVERSED_OUTPUTS states that QB is
always the negation of Q.
 RESET states that (it is always the case that) if
RESET is true then at the next simulation cycle, 
Q is be false.
 LOAD specifies that whenever signal LOAD
goes high while RESET is low, then the value of D
is propagated to Q in one simulation cycle.



Comments


The purpose of this example is to show the expressive power of
temporal logic on whic the specification language is built. It
is possible to express properties on states as well as on events
expressed as sequences of states.



Examples:
Latch 
Ring 
Stack 

Main sections:
 Introduction  
 Installation  
 Documentation  
 Examples 


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