Sökning: onr:"swepub:oai:research.chalmers.se:b88353b3-6f10-4bac-9c8c-70c5a6b856e8" >
Symbolic trajectory...
Symbolic trajectory evaluation for word-level verification: theory and implementation
-
- Chakraborty, S. (författare)
- Indian Institute of Technology
-
Khasidashvili, Z. (författare)
-
- Seger, Carl-Johan, 1961 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
visa fler...
-
- Gajavelly, R. (författare)
- Indian Institute of Technology
-
- Haldankar, T. (författare)
- Indian Institute of Technology
-
- Chhatani, D. (författare)
- Indian Institute of Technology
-
- Mistry, R. (författare)
- Indian Institute of Technology
-
visa färre...
-
(creator_code:org_t)
- 2017-02-14
- 2017
- Engelska.
-
Ingår i: Formal Methods in System Design. - : Springer Science and Business Media LLC. - 1572-8102 .- 0925-9856. ; 50:2-3, s. 317-352
- Relaterad länk:
-
http://dx.doi.org/10...
-
visa fler...
-
https://doi.org/10.1...
-
https://research.cha...
-
visa färre...
Abstract
Ämnesord
Stäng
- Symbolic trajectory evaluation (STE) is a model checking technique that has been successfully used to verify many industrial designs. Existing implementations of STE reason at the level of bits, allowing signals in a circuit to take values from a lattice comprised of three elements: 0, 1, and X. This limits the amount of abstraction that can be achieved, and presents limitations to scaling STE to even larger designs. The main contribution of this paper is to show how much more abstract lattices can be derived automatically from register-transfer level descriptions, and how a model checker for the general theory of STE instantiated with such abstract lattices can be implemented in practice. We discuss several implementation issues, including how word-level circuits can be symbolically simulated using a new encoding for words that allows representing X values of sub-words succinctly. 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 bit-level STE, as well as word-level bounded model checking.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Programvaruteknik (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Software Engineering (hsv//eng)
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Inbäddad systemteknik (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Embedded Systems (hsv//eng)
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Datorsystem (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Computer Systems (hsv//eng)
Nyckelord
- X-based abstraction
- SMT solving
- Symbolic trajectory evaluation
- Word-level verification
Publikations- och innehållstyp
- art (ämneskategori)
- ref (ämneskategori)
Hitta via bibliotek
Till lärosätets databas