Symbolic trajectory evaluation for word-level verification: theory and implementation

DOI10.1007/S10703-017-0268-9MaRDI QIDQ526779zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

hardware verificationSMT solvingsymbolic trajectory evaluationinvalid-bit encodingRTL verificationsymbolic simulationword-level verificationX-based abstraction

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Symbolic trajectory evaluation
• Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation
• 3-Valued Circuit SAT for STE with Automatic Refinement
• scientific article; zbMATH DE number 1979544
• Explaining Symbolic Trajectory Evaluation by Giving It a Faithful Semantics

Cites work

• scientific article; zbMATH DE number 177501 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• Correct Hardware Design and Verification Methods
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Graph-Based Algorithms for Boolean Function Manipulation
• Matching multiplications in bit-vector formulas
• Symbolic trajectory evaluation for word-level verification: theory and implementation
• The MathSAT5 SMT solver

Cited in

(8)

• A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL
• Verifying the implementation of an error control code
• 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

Describes a project that uses

Uses Software

• STEWord
• ABC
• MathSAT5
• CVC4
• CUDD
• Yices
• MiniSat
• Boolector
• Beaver

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)