Symbolic trajectory evaluation for word-level verification: theory and implementation
DOI10.1007/S10703-017-0268-9zbMATH Open1360.68582OpenAlexW2588803340MaRDI QIDQ526779FDOQ526779
Authors: Supratik Chakraborty, Zurab Khasidashvili, Carl-Johan H. Seger, Rajkumar Gajavelly, Tanmay Haldankar, Dinesh Chhatani, Rakesh Mistry
Publication date: 15 May 2017
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10703-017-0268-9
Recommendations
hardware verificationSMT solvingsymbolic trajectory evaluationinvalid-bit encodingRTL verificationsymbolic simulationword-level verificationX-based abstraction
Cites Work
- The MathSAT5 SMT solver
- Graph-Based Algorithms for Boolean Function Manipulation
- Title not available (Why is that?)
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- Matching multiplications in bit-vector formulas
- Title not available (Why is that?)
- Symbolic trajectory evaluation for word-level verification: theory and implementation
- Correct Hardware Design and Verification Methods
Cited In (8)
- Verifying the implementation of an error control code
- A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL
- A Practical Approach to Word Level Model Checking of Industrial Netlists
- Matching multiplications in bit-vector formulas
- Efficient Automatic STE Refinement Using Responsibility
- Symbolic trajectory evaluation
- Explaining Symbolic Trajectory Evaluation by Giving It a Faithful Semantics
- Symbolic trajectory evaluation for word-level verification: theory and implementation
Uses Software
This page was built for publication: Symbolic trajectory evaluation for word-level verification: theory and implementation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q526779)