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

DOI10.1007/s10703-017-0268-9zbMath1360.68582OpenAlexW2588803340MaRDI QIDQ526779

Zurab Khasidashvili, Carl-Johan H. Seger, Dinesh Chhatani, Rajkumar Gajavelly, Supratik Chakraborty, Rakesh Mistry, Tanmay Haldankar

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)

Related Items (2)

Matching Multiplications in Bit-Vector Formulas ⋮ Symbolic trajectory evaluation for word-level verification: theory and implementation

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Symbolic trajectory evaluation for word-level verification: theory and implementation
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Matching Multiplications in Bit-Vector Formulas
• Graph-Based Algorithms for Boolean Function Manipulation
• The MathSAT5 SMT Solver
• Correct Hardware Design and Verification Methods

This page was built for publication: Symbolic trajectory evaluation for word-level verification: theory and implementation