The VHDL SLIB System Library

The VHDL B-Toolkit is supplied with a set of reusable machines which encapsulate basic state and data-structures, and provide basic abstract types.

The Role of the System Library

Static and persistent data of an implementation must be held by an imported machine. Ultimately, the bottom level implementation must import a Library machine if static or persistent data is required (i.e. if you are implementing a state-machine).

A library machine is used simply by INCLUDING or SEEING the machine in a construct. When a predefined machine is INCLUDED into an implementation, actual parameters must be supplied. However when seeing an existing machine no parameters should be supplied.

Each library machine is formally specified, and the readable formal specification is available in the development environment after the machine has been committed.

The naming library machines and their operations follows a uniform scheme.

Library machines with state have to be renamed when they are imported into a development. These machines and their operations, therefore, all have names starting with Rename_ , which is automatically replaced by a new prefix supplied in the importing machine at the time that the library machine is committed from the library. The VHDL system library may be extended and local copies may be created.

VHDL Code Modules

Some VHDL Library machines have an associated VHDL code module, which is incorporated in the code that is produced when the importing construct is translated.

Hand-written VHDL code may be incorporated into a development through the Create VHDL SLIB With Code Module facility of the B-Toolkit.

The Package Machines

VHDL Package

The VHDL_Package Machine defines the 2-valued 'standard logic', and introduces the general 'vectors' of 'standard logic'. This Package also gives the type of some vector functions. The vector function are not specified in the package itself, but constructive definitions are provided in an accompanying Animation theory file : VHDL.thy.

MACHINE           VHDL_PK

SETS              std_logic = {'0','1'}

CONSTANTS         
                  exp,
                  STD_LOGIC_VECTOR,
                  Vec2Nat,
                  Nat2Vec,
                  vec_conc

PROPERTIES

   exp : NAT * NAT --> NAT &
   !(xx,nn). ( xx : NAT & nn : NAT => ( 
               exp(xx,0) = 1 &
               exp(xx,nn+1) = exp(xx,nn) * xx )
             ) &
   
   STD_LOGIC_VECTOR = UNION(ll).(ll : NAT | 0..ll --> std_logic) &

   Vec2Nat : STD_LOGIC_VECTOR --> NAT &

   Nat2Vec : NAT --> STD_LOGIC_VECTOR &

   vec_conc : STD_LOGIC_VECTOR * STD_LOGIC_VECTOR --> STD_LOGIC_VECTOR 

DEFINITIONS

  (a ** b) == exp(a,b);

  num_range(m,n) == (m..n);

  std_logic_vector(m,n) == (m..n --> std_logic);

  (v ^^ u) == vec_conc(v,u)

END

Renamable Number Package

The Number Package defines a general Number Range Type. The package will be SEEN from Simple Modules, Process Modules or their refinements.


MACHINE          Rename_number_PK(maxnum)

SEES             VHDL_PK

CONSTANTS

   Rename_Ran 

/*" {\em 0 .. maxnum\/} also recognized as {\em Rename\_range} "*/

PROPERTIES       Rename_Ran = 0..maxnum 

OPERATIONS

/* need all other ops from Scalar_type */

  nn <-- Rename_EXP(n1:0..maxnum & p1:0..maxnum) =
  PRE
    n1 ** p1 : 0..maxnum
  THEN
    nn := n1 ** p1
  END

END

Renamable Vector Package

The Vector Package defines a general 'standard logic vector' Type. The package will be SEEN from Simple Modules, Process Modules or their refinements. Functions for manipulating a vector and for querying the contents of a vector are provided.


MACHINE           Rename_vector_PK(lb,ub)

CONSTRAINTS       lb=0 & lb std_logic &
   Rename_Vec2Nat : Rename_Vec --> NAT &
   Rename_Nat2Vec : NAT +-> Rename_Vec &

/*   Rename_Vec2Nat = 
           %(vec). ( vec : Rename_Vec | (
               SIGMA(nn).( nn:0..ub & vec(nn)='1' | exp(2,nn) ) 
           )) & */

  !(vec).(
        vec : Rename_Vec =>
        Rename_Vec2Nat(vec) = SIGMA(nn).( nn:0..ub & vec(nn)='1' | exp(2,nn) )
          ) &

   Rename_Nat2Vec = Rename_Vec2Nat~

OPERATIONS


/* conversions */

  nn <-- Rename_vec_VEC2NAT(vec:Rename_Vec) =
  BEGIN
    nn := Rename_Vec2Nat(vec)
  END;

  vec <-- Rename_vec_NAT2VEC(nn:NAT) =
  PRE nn : dom(Rename_Nat2Vec) THEN
    vec := Rename_Nat2Vec(nn)
  END;


/* enquiry */

  val <-- Rename_idx_VAL(vec:Rename_Vec & idx:0..ub) =
  BEGIN
    val := vec(idx)
  END;

  sl <-- Rename_idx_EQL(val:std_logic & vec:Rename_Vec & idx:0..ub) =
  IF val = vec(idx) THEN
    sl := '1'
  ELSE
    sl := '0'
  END;

 vecout <-- Rename_vec_XTR(vecin:Rename_Vec & lo:0..ub & hi:0..ub) =
  PRE lo <= hi THEN
    vecout :=  %(nn).(nn:0..(hi-lo) | vecin(lo+nn) )  
  END;

/* modification */

  vecout <-- Rename_idx_MOD(val:std_logic & vecin:Rename_Vec & idx:0..ub) =
  BEGIN
    vecout := vecin <+ {idx |-> val}
  END

END

Renamable Vector Package Code Module


Rename_Vec == std_logic_vector(ub downto 0);

-----------------------------------

----- conversions

nn <-- Rename_vec_VEC2NAT(vec) ==
    variable acc : natural;
  acc := 0;
  for n in 0 to ub loop
    if vec(n)='1' then
      acc:=acc+2**n;
    end if;
  end loop;
  nn <-- acc;

vec <-- Rename_vec_NAT2VEC(nn) ==
    variable temp : NUM RANGE 0 to ((2**_succ_ub)-1);
  temp := nn;
  for n in ub downto 0 loop
    if temp>=(2**n) then
      temp:=temp-(2**n);
      vec(n)<--'1';
    else
      vec(n)<--'0'; 
    end if;
  end loop;


----- enquiry

val <-- Rename_idx_VAL(vec,idx) ==
  val <-- vec(idx); 

st <-- Rename_idx_EQL(val,vec,idx) ==
  if val = vec(idx) then
    st <-- '1';
  else
    st <-- '0';
  end if;

vecout <-- Rename_vec_XTR(vecin,lo,hi) ==
  vecout <-- vecin(hi downto lo);


----- modification

vecout <-- Rename_idx_MOD(val,vecin,idx) ==
  vecout <-- vecin;
  vecout(idx) <-- val;

The Renamable Event Machine

In hardware systems the notion of `events' plays a central role. For example, a state transition can be conditional on the occurrence of an event (e.g. `a rising edge' is the event where a 2-valued logic signal changes from `low' to `high'). This notion of events is supported by the use of EVENT Machines - which allow for event value changes to be used in conditional statements.

Several Event machines can be INCLUDED into a 'Simple Module', and each of these machines models a separate event in a Hardware system. Typical usages of an Event Machines are: the provision of a clock, where the 'tick' of the clock is the condition upon other activities will happen, or a 'reset' which 'trigger' a system to take a particular action.

In order to Animate a Simple Module, which INCLUDES an Event Machine the operation which simulates the change ( .._chg ) in the the 2-valued logic state must be PROMOTED, and the operation which ensures that the change is ONLY 'acknowledged' once ( .._ack ), must be one of the components in the parallel construct within the Simple Modules Architecture Operation.


MACHINE           Rename_EV

SEES              VHDL_PK

VARIABLES         Rename, Rename_event
/*"
The variable {\em Rename\/} holds the current value of a source,
while the variable {\em Rename\_event\/} will indicate whether the
value of that source has changed
"*/

INVARIANT         Rename: std_logic & Rename_event: std_logic

INITIALISATION    BEGIN Rename := '0' || Rename_event := '0' END

OPERATIONS

/*"
{\bf Rename\_chg} is a synchronous event which changes Rename's value.
"*/

  Rename_chg =
  BEGIN 
    IF Rename = '1' THEN  Rename := '0' ELSE  Rename := '1' END ||
    Rename_event := '1'
  END;

/*"
{\bf Rename\_ack\/} is the event of another agent (a process
in an architecture) observing (or using) the value of {\em Rename\/}.
"*/

  Rename_ack = BEGIN Rename_event := '0' END

DEFINITIONS

  Rename_EVENT == (Rename_event = '1')

END

The Signal Machines

Renamable Number Signal

The general Number Signal Library machine encapsulates a Number; it will be INCLUDED IN Simple Modules, Process Modules or their refinements.


MACHINE           Rename_number_SG(maxnum)

SEES              VHDL_PK

CONSTANTS         Rename_Ran 

/*" {\em 0 .. maxnum\/} also recognized as {\em Rename\_Ran} "*/

PROPERTIES        Rename_Ran = 0..maxnum 

VARIABLES         Rename_num

INVARIANT         Rename_num : Rename_Ran

INITIALISATION    Rename_num :: Rename_Ran

OPERATIONS

/* need all other ops from Scalar_type */

  Rename_EXP(num:0..maxnum & p1:0..maxnum) =
  PRE
    num ** p1 : 0..maxnum
  THEN
    Rename_num := num ** p1
  END

END

Renamable Vector Signal

The Vector Signal encapsulates a general 'standard logic vector'. The package will be INCLUDED into Simple Modules, Process Modules or their refinements. Functions for manipulating the vector and for querying the contents of the vector are provided.


MACHINE           Rename_vector_SG(lb,ub)

CONSTRAINTS       lb=0 & lb std_logic &
   Rename_Vec2Nat : Rename_Vec --> NAT &
   Rename_Nat2Vec : NAT +-> Rename_Vec &


/*   Rename_Vec2Nat = 
           %(vec). ( vec : Rename_Vec | (
               SIGMA(nn).( nn:0..ub & vec(nn)='1' | exp(2,nn) ) 
           )) &
*/
   !(vec).(
        vec : Rename_Vec =>
        Rename_Vec2Nat(vec) = SIGMA(nn).( nn:0..ub & vec(nn)='1' | exp(2,nn) )
          ) &

   Rename_Nat2Vec = Rename_Vec2Nat~
              
VARIABLES         Rename_vec

INVARIANT         Rename_vec : Rename_Vec 

INITIALISATION    Rename_vec :: Rename_Vec 

OPERATIONS


/* vector store/retrieve/equality */

  Rename_vec_STO(vec:Rename_Vec) = BEGIN Rename_vec := vec END;

  vec <-- Rename_vec_VAL = BEGIN  vec := Rename_vec END;

  sl <-- Rename_vec_EQL(vec:Rename_Vec) =
  IF vec=Rename_vec THEN
    sl := '1'
  ELSE
    sl := '0'
  END;


/* index modify/retrieve/equality */

  Rename_idx_MOD(val:std_logic & idx:0..ub) =
  BEGIN
    Rename_vec := Rename_vec <+ {idx |-> val}
  END;

  val <-- Rename_idx_VAL(idx:0..ub) = BEGIN val := Rename_vec(idx) END;

  sl <-- Rename_idx_EQL(val:std_logic & idx:0..ub) =
  IF val = Rename_vec(idx) THEN
    sl := '1'
  ELSE
    sl := '0'
  END;


/* vector/nat conversions */

  nn <-- Rename_vec_VEC2NAT =
  BEGIN
    nn := Rename_Vec2Nat(Rename_vec)
  END;

  Rename_vec_NAT2VEC(nn:NAT) =
  PRE nn : dom(Rename_Nat2Vec) THEN
    Rename_vec := Rename_Nat2Vec(nn)
  END;

/* vector extract */

  vec <-- Rename_vec_XTR(lo,hi) =
  PRE lo:0..ub & hi:0..ub & lo <= hi THEN
     vec := %(nn).(nn:0..(hi-lo) | Rename_vec(lo+nn) )
  END;

/*  vector mask */

  Rename_vec_MASK(lo:0..ub & hi:0..ub) =
  PRE lo <= hi THEN
    Rename_vec := ((0..ub) * {'0'}) <+ ( lo..hi <| Rename_vec ) 
  END

END

Renamable Vector Signal Code Module


signal Rename_vec: std_logic_vector(ub downto 0);

-----------------------------------------------


----- vector store/retrieve/equality

Rename_vec_STO(vec) ==
  Rename_vec <= vec after 1 ns;

vec <-- Rename_vec_VAL ==
  vec <-- Rename_vec;

sl <-- Rename_vec_EQL(vec) ==
    variable v1 : std_logic;
  v1 := '1';
  for n in 0 to ub loop
    if vec(n) /= Rename_vec(n) then
      v1 := '0';
    end if;
  end loop;
  sl <-- v1;


----- index store/retrieve/equality

Rename_idx_MOD(val,idx) ==
  Rename_vec(idx) <= val after 1 ns;

val <-- Rename_idx_VAL(idx) ==
  val <-- Rename_vec(idx);

st <-- Rename_idx_EQL(val,idx) ==
  if val = Rename_vec(idx) then
    st <-- '1';
  else
    st <-- '0';
  end if;


----- vector/nat conversions

nn <-- Rename_vec_VEC2NAT ==
    variable acc : natural;
  acc := 0;
  for n in 0 to ub loop
    if Rename_vec(n)='1' then
      acc:=acc+2**n;
    end if;
  end loop;
  nn<--v1;

Rename_vec_NAT2VEC(nn) ==
    variable temp : NUM RANGE 0 to ((2**_succ_ub)-1);
  temp := nn;
  for n in ub downto 0 loop
    if temp>=(2**n) then
       temp:=temp-(2**n);
       Rename_vec(n) <= '1' after 1 ns;
    else
      Rename_vec(n) <= '0' after 1 ns; 
    end if;
  end loop;


----- vector extract

vec <-- Rename_vec_XTR(lo,hi) ==
  vec <= Rename_vec(hi downto lo) after 1 ns;


----- vector mask

Rename_vec_MASK(lo,hi) ==
  for n in 0 to lo-1 loop
    Rename_vec(n) <= '0' after 1 ns;
  end loop;
  for n in hi+1 to ub loop
    Rename_vec(n) <= '0' after 1 ns;
  end loop

A full on-line help listing is available in the Contents Page Also available in the form of a complete Index. Blogo