Symbolic simulation: Difference between revisions

Revision as of 17:40, 15 June 2006

Revision as of 17:41, 15 June 2006

Line 1:

In computer science, a [[simulation]] is a computation of the execution of some appropriately modelled state-transition system. Typically this process models the complete state of the system at individual points in a discrete linear time frame, computing each state sequentially from its predecessor. Models for computer programs or VLSI logic designs can be very easily simulated, as they often have an [[operational semantics]] which can be used directly for simulation.

Symbolic simulation is a form of simulation where many possible executions of a system are considered simultaneously. This is typically achieved by augmenting the [[___domain]] over which the simulation takes place. A symbolic [[Symbolic variablesvariable]] can be used in the simulation state representation in order to index multiple executions of the system. For each possible valuation of these variables, there is a concrete system state that is being indirectly simulated.

Because symbolic simulation can cover many system executions in a single simulation, it can greatly reduce the size of verification problems. Techniques such as [[Symbolic Trajectory Evaluation (STE)]] and [[Generalized Symbolic Trajectory Evaluation (GSTE)]] are based on this idea of symbolic simulation.