MODULE Counter2

TITLE 'Mike Lhamon'

" BCD Counter Example #2 of a state machine design using sets.

" Nov. 13, 2003     EE481   University of Kentucky

" This example represents the most basic state machine design entry, a table
" Note: The output OUT is high for states (3,4,7) instead of (2,6) !!!!
" Also: Notice in the simulation how the output is formed after the rising
"       edge of the clock, and that the reset works both async and sync.

clock PIN;
reset PIN;

" Output pins
 a, b, c, d, out pin istype 'reg_D';
"a is the MSB,   d is the LSB 
Counter = [a,b,c,d];      " Defined a set,  (a bus structure)

x macro {.x.} ;        " Macro for dont care
" comment starts with a one, double quote
" not operator  !
" xor operator  $
" xnor operator !$
"  or operator  #
" and operator  &
" addition operator +
" combinational assignment
" registered assignment

" Because of the set notation I can use decimal numbers in the table entries
truth_table ( [reset, Counter, out] :> [Counter, out]) 
  [1, x, x] :> [0,0];  "Input Sync. reset -> 0
  [0, 0, x] :> [0,0];  "Async reset -> 0
  [0, 0, x] :> [1,0];  "0->1
  [0, 1, x] :> [2,0];  "1
  [0, 2, x] :> [3,1];  "2
  [0, 3, x] :> [4,1];  "3
  [0, 4, x] :> [5,0];  "4
  [0, 5, x] :> [6,0];  "5->6
  [0, 6, x] :> [7,1];  "6
  [0, 7, x] :> [8,0];  "7
  [0, 8, x] :> [9,0];  "8->9
  [0, 9, x] :> [0,0];  "9 ->0
 
" end truth_table;

equations
Counter.clk = clock;
out.clk = clock;
Counter.aclr = reset;
out.aclr = reset;

" This would work as well, but lets use the set notation instead, see below
"test_vectors
"  ( [clock, reset]   -> [a,b,c,d] )
"  [x, 1]   -> [x,x,x,x];
"  [.c., 1] -> [x,x,x,x];
"  etc ...

" Same test vectors as in example #1 but it is organized better with sets
" Now dont care x takes on the length of the set
test_vectors
  ( [clock, reset]   -> [Counter] )
  [x, 1]   -> [x];
  [.c., 1] -> [x];
  [.c., 0] -> [x];
  [.c., 0] -> [x];
  [.c., 1]   -> [x];
  [.c., 0] -> [x];
  [.c., 0] -> [x];
  [x, 1]   -> [x];
  [.c., 0] -> [x];
  [.c., 0] -> [x];
  [.c., 0] -> [x];
  [.c., 0] -> [x];
  [.c., 0] -> [x];
  [.c., 0] -> [x];
  [.c., 0] -> [x];
  [.c., 0] -> [x];
  [.c., 0] -> [x];
  [.c., 0] -> [x];
  [.c., 0] -> [x];
  [.c., 0] -> [x];
  [x, 1]   -> [x];
  [.c., 0] -> [x];
  [.c., 0] -> [x];
END