Content deleted Content added
+ref section |
Reconrabbit (talk | contribs) added reference |
||
Line 1:
{{short description|Form of simulation where many possible executions of a system are considered simultaneously}}{{Refimprove|date=April 2024}}
In computer science, a [[simulation]] is a computation of the execution of some appropriately modelled [[state transition system|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 [[Variable (programming)|variable]] can be used in the simulation state representation in order to index multiple executions of the system.<ref>{{Cite journal |last=Bryant |first=Randal E. |date=1990 |title=Symbolic simulation---techniques and applications |url=http://portal.acm.org/citation.cfm?doid=123186.128296 |journal=Proceedings of the 27th ACM/IEEE Design Automation Conference |language=en |publisher=ACM Press |pages=517–521 |doi=10.1145/123186.128296 |isbn=978-0-89791-363-8}}</ref> 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.
| |||