Using Symbolic State Descriptions

Symbolic state descriptions describe a state machine without having to specify actual state values. An example of a symbolic state description is shown below.

module SM
a,b,clock pin; " inputs
a_reset,s_reset pin; " reset inputs
x,y pin istype 'com'; " simple outputs

sreg1 state_register;
S0..S3 state;

equations
sreg1.clk = clock;
state_diagram sreg1
state S0:
goto S1 with {x = a & b;
y = 0; };

state S1: if (a & b)
then S2 with {x = 0;
y = 1; };

state S2: x = a & b;
y = 1;
if (a) then S1 else S2;

state S3:
goto S0 with {x = 1;
y = 0; };

async_reset S0: a_reset;

sync_reset S0: s_reset;

end

Symbolic state descriptions use the same syntax as non-symbolic state descriptions; the only difference is the addition of the State_register and State declarations, and the addition of symbolic synchronous and asynchronous reset statements.

Symbolic Reset Statements

In symbolic state descriptions, the Sync_Reset and Async_Reset statements specify synchronous or asynchronous state machine reset logic. For example, to specify that a state machine must asynchronously reset to state Start when the Reset input is true, you write

ASYNC_RESET Start : (Reset) ;

Symbolic Test Vectors

You can also write test vectors to refer to symbolic state values by entering the symbolic state register name in the test vector header (in the output sections), and the symbolic state names in the test vectors as output values.