Raised when parsing PPX nodes

guard s builds an guard from a string representation. The syntax of the string is exp, where exp denotes a boolean expression.

For example : start='1' or k<2

Raises Error if parsing s or if exp does not denote a boolean expression.

The Parse.guard function can be invoked using the %fsm_guard PPX extension. In this case, Parse.guard s is denoted [%fsm_guard s]

When using the PPX extension, syntax errors in the transition description are detected and reported at compile time.

guard s builds a list of guards from a string representation. The syntax of the string is exp1,...,expn, where each expi denotes a boolean expression.

For example : start='1', k<2

Raises Error if parsing s or if expi does not denote a boolean expression.

The Parse.guards function can be invoked using the %fsm_guards PPX extension. In this case, Parse.guards s is denoted [%fsm_guards s]

When using the PPX extension, syntax errors in the transition description are detected and reported at compile time.

action s builds an action from a string representation. The syntax of the string is var := exp

For example : rdy:=0

Raises Error if parsing s fails.

The Parse.action function can be invoked using the %fsm_action PPX extension. In this case, Parse.action s is denoted [%fsm_action s]

When using the PPX extension, syntax errors in the transition description are detected and reported at compile time.

action s builds a list of actions from a string representation. The syntax of the string is act1, ..., actn where act is an action.

For example : rdy:=0, s:=1

Raises Error if parsing s fails.

The Parse.actions function can be invoked using the %fsm_actions PPX extension. In this case, Parse.actions s is denoted [%fsm_actions s]

When using the PPX extension, syntax errors in the transition description are detected and reported at compile time.

transition s builds a transition from a string representation. The syntax of the string is

src -> dst [ when guard₁ , ... , guard_m ] [ with act₁ , ... , act_n ]

where

• src is the name of the source state
• dst is the name of the destination state
• guard is a boolean expression
• act is an action, of the form var := exp

For example : t = Parse.transition "S0 -> S1 when s=0 with rdy:=0, k:=k=1"

Raises Error if parsing s fails.

The Parse.transition function can be invoked using the %fsm_trans PPX extension. In this case, Parse.transition s is denoted [%fsm_trans s].

When using the PPX extension, syntax errors in the transition description are detected and reported at compile time.

fsm s builds a FSM from a string representation. The syntax of the string is

"name: name ;

states: state₁, ..., state_ns ;

inputs: in₁, ..., in_ni ;

outputs: out₁, ..., out_no ;

[vars: var₁, ..., var_nv ;]

trans: t₁; ...; t_nt ;

itrans: -> state [with act₁, ..., act_na]"

where

• name is the name of defined FSM
• state₁, ..., state_ns is a comma-separated list of state names
• in₁, ..., in_ni is a comma-separated list of input names
• out₁, ..., out_no is a comma-separated list of output names
• var₁, ..., out_nv is an optional, comma-separated list of local variable names
• t₁, ..., t_nt is a semicolon-separated list of transitions (with syntax defined in transition)
• act₁, ..., act_na is an optional, comma-separated list of initial actions

For example : "name: f1; states: E0, E1; inputs: e; outputs: s; trans: E0 -> E1 when e=1 with s:=1; E1 -> E0 when e=0 with s:=0; itrans: -> Init with s:=0;"

Raises Error if parsing s fails.

The Parse.fsm function can be invoked using the %fsm PPX extension. In this case, Parse.fsm s is denoted [%fsm s].

When using the PPX extension, syntax errors in the transition description are detected and reported at compile time.

stimuli s builds a sequence of stimuli from a string representation. The syntax of the string is

"name : t₁ , v₁ ; ..., ; t_m , v_m"

where t is a clock cycle counter and v a value.

For example, the sequence stimuli "start: 0,'1'; 2,'0'", where start is a signal of type bool

• set start to '1' (true) at time step 0
• set start to '0' (false) at time step 2

The Parse.stimuli function can be invoked using the %fsm_stim PPX extension. In this case, Parse.stimuli s is denoted [%fsm_stim s].

Raises Error if parsing s fails.

When using the PPX extension, syntax errors in the transition description are detected and reported at compile time.