Word-level Symbolic Trajectory Evaluation
The work
| Authors | Supratik Chakraborty; Zurab Khasidashvili; Carl-Johan H. Seger; Rajkumar Gajavelly; Tanmay Haldankar; Dinesh Chhatani; Rakesh Mistry |
|---|---|
| Editors | |
| Type | misc |
| Year | 2015 |
| Citekey | chakraborty2015wordlevel |
Identifiers
| arXiv | 1505.07916 from its landing_page_url |
|---|---|
| DOI | 10.1007/s10703-017-0268-9 |
Access
| Landing page | https://arxiv.org/abs/1505.07916 |
|---|
Related
| Distinct from | aagaard1999are |
|---|---|
| Distinct from | andrici2019verifying |
| Distinct from | bryant1990ternary |
| Distinct from | bryant1991complexity |
| Distinct from | clarke1996word |
| Distinct from | een2011efficient |
| Distinct from | jacobi2005automatic |
| Distinct from | khasidashvili2009assumeguarantee |
| Distinct from | li2026arisca |
| Distinct from | lipp2018meltdown |
| Distinct from | oleary1999formally |
| Distinct from | oleary2013relational |
| Distinct from | seger1995formal |
From bibtex.
Abstract
Symbolic trajectory evaluation (STE) is a model checking technique that has been successfully used to verify industrial designs. Existing implementations of STE, however, reason at the level of bits, allowing signals to take values in {0, 1, X}. This limits the amount of abstraction that can be achieved, and presents inherent limitations to scaling. The main contribution of this paper is to show how much more abstract lattices can be derived automatically from RTL descriptions, and how a model checker for the general theory of STE instantiated with such abstract lattices can be implemented in practice. This gives us the first practical word-level STE engine, called STEWord. Experiments on a set of designs similar to those used in industry show that STEWord scales better than word-level BMC and also bit-level STE.
A copy is held
pdf, 499.7 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-16 22:33 UTC |
| Approved by | a person 2026-09-17 17:08 UTC |
Cite it as
@misc{chakraborty2015wordlevel,
title = {Word-level Symbolic Trajectory Evaluation},
author = {Supratik Chakraborty and Zurab Khasidashvili and Carl-Johan H. Seger and Rajkumar Gajavelly and Tanmay Haldankar and Dinesh Chhatani and Rakesh Mistry},
year = {2015},
doi = {10.1007/s10703-017-0268-9},
}
This record lives at https://refs.drheap.org/chakraborty2015wordlevel/ and will keep doing so.