module SMEX4 
title 'Combination-Lock State Machine' 

" Input and output pins 
CLOCK, X                        pin;
Q1..Q3                          pin istype 'reg';
UNLK, HINT                      pin istype 'com';

" Definitions 
S        = [Q1,Q2,Q3];          " State variables 
ZIP      = [ 0, 0, 0];          " State encodings 
X0       = [ 0, 0, 1]; 
X01      = [ 0, 1, 0]; 
X011     = [ 0, 1, 1]; 
X0110    = [ 1, 0, 0]; 
X01101   = [ 1, 0, 1]; 
X011011  = [ 1, 1, 0]; 
X0110111 = [ 1, 1, 1]; 

state_diagram S

state ZIP:      IF X==0 THEN X0    WITH {UNLK = 0; HINT = 1}
                ELSE ZIP           WITH {UNLK = 0; HINT = 0}
                
state X0:       IF X==0 THEN X0    WITH {UNLK = 0; HINT = 0}
                ELSE X01           WITH {UNLK = 0; HINT = 1}
                
state X01:      IF X==0 THEN X0    WITH {UNLK = 0; HINT = 0}
                ELSE X011          WITH {UNLK = 0; HINT = 1}
                
state X011:     IF X==0 THEN X0110 WITH {UNLK = 0; HINT = 1}
                ELSE ZIP           WITH {UNLK = 0; HINT = 0}
                
state X0110:    IF X==0 THEN X0    WITH {UNLK = 0; HINT = 0}
                ELSE X01101        WITH {UNLK = 0; HINT = 1}
                
state X01101:   IF X==0 THEN X0    WITH {UNLK = 0; HINT = 0}
                ELSE X011011       WITH {UNLK = 0; HINT = 1}
                
state X011011:  IF X==0 THEN X0110 WITH {UNLK = 0; HINT = 0}
                ELSE X0110111      WITH {UNLK = 0; HINT = 1}
                
state X0110111: IF X==0 THEN X0    WITH {UNLK = 1; HINT = 1}
                ELSE ZIP           WITH {UNLK = 0; HINT = 0}

equations
S.CLK = CLOCK;

test_vectors 
([CLOCK, X] -> [   S    , UNLK, HINT])
 [ .C. , 1] -> [.X.     , .X. , .X. ]; " Since no reset input, apply
 [ .C. , 1] -> [.X.     , .X. , .X. ]; "   a 'synchronizing sequence'
 [ .C. , 1] -> [.X.     , .X. , .X. ]; "   to reach a known starting
 [ .C. , 1] -> [ZIP     , .X. , .X. ]; "   state
 [  0  , 0] -> [ZIP     ,  0  ,  1  ]; " Test Mealy outputs for both
 [  0  , 1] -> [ZIP     ,  0  ,  0  ]; "   values of X
 [ .C. , 1] -> [ZIP     , .X. , .X. ]; " Test ZIP-->ZIP (X==1)
 [ .C. , 0] -> [X0      , .X. , .X. ]; "   and ZIP-->X0 (X==0)
 [  0  , 0] -> [X0      ,  0  ,  0  ]; " Test Mealy outputs for both
 [  0  , 1] -> [X0      ,  0  ,  1  ]; "   values of X
 [ .C. , 0] -> [X0      , .X. , .X. ]; " Test X0-->X0 (X==0)
 [ .C. , 1] -> [X01     , .X. , .X. ]; "   and X0-->X01 (X==1)
 [  0  , 0] -> [X01     ,  0  ,  0  ]; " Test Mealy outputs for both
 [  0  , 1] -> [X01     ,  0  ,  1  ]; "   values of X
 [ .C. , 0] -> [X0      , .X. , .X. ]; " Test X01-->X0 (X==0)
 [ .C. , 1] -> [X01     , .X. , .X. ]; " Get back to X01
 [ .C. , 1] -> [X011    , .X. , .X. ]; " Test X01-->X011 (X==1)


END SMEX4