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

DOI10.1007/S10703-017-0268-9zbMATH Open1360.68582OpenAlexW2588803340MaRDI QIDQ526779FDOQ526779

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)

Cites Work

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

Cited In (3)

• Verifying the implementation of an error control code
• 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

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)