Before we describe our compiler algorithm, we first formally describe how we model the traditional dynamic simulation process. During simulation, the state of the computation is captured by a quadruple , where

- is the set of sensitive events,
- is the set of events ready to be executed,
- is the set of all
such that event has time steps left before it can execute,
- is the memory store that maps each variable to its current value.

We assume the existence of the following operations:

- deterministically chooses an event from the set of ready events .
- applies the code associated with event to the memory store and returns a new memory store. It may also produce side effects such as generating output.
- evaluates the boolean expression using the memory store and returns or .
- indicates if the execution of event with initial memory store changes the value of expression .

We define by , where

- (Type I Transition)
- This represents the execution of an event
in the current simulation time step:
if , then

Let in - (Type II Transition)
- This represents incrementing the
simulation time to the next time during which an event can occur.
if and , then

Letin

- (Type III Transition)
- This represents the end of simulation:
if and , then

, denoting no next state.

The *dynamic simulation* of an event graph is a sequence of
states , where

- ,
where represents the initial memory store that maps every
variable to an appropriate initial value (for Verilog, all variables
are initially
`x`).