Using word-level information in formal hardware verification

DOI10.1023/B:AURC.0000030907.28679.82MaRDI QIDQ2487686zbMATH OpenWikidataFDO

Authors Yanyan Li

Publication date 8 August 2005

Published in Automation and Remote Control (Search for Journal in Brave)

zbMATH Keywords

register-transfer-level specifications

Mathematics Subject Classification ID

Computer system organization (68M99)

Recommendations

• scientific article; zbMATH DE number 1506311
• scientific article; zbMATH DE number 1796146
• Word level bitwidth reduction for unbounded hardware model checking
• A Practical Approach to Word Level Model Checking of Industrial Netlists
• scientific article; zbMATH DE number 2113572

Cited in

(11)

• Encoding RTL constructs for \textsc{MathSAT}: a preliminary report
• A Practical Approach to Word Level Model Checking of Industrial Netlists
• Formal verification of arithmetic RTL: translating Verilog to C++ to ACL2
• Automatic Merge-Point Detection for Sequential Equivalence Checking of System-Level and RTL Descriptions
• scientific article; zbMATH DE number 5718039 (Why is no real title available?)
• scientific article; zbMATH DE number 1506311 (Why is no real title available?)
• Dominant controllability check using QBF-solver and netlist optimizer
• A study about the efficiency of formal high-level synthesis applied to verification
• Word level bitwidth reduction for unbounded hardware model checking
• scientific article; zbMATH DE number 1796146 (Why is no real title available?)
• Level-up -- from bits to words

Describes a project that uses

Uses Software

• Velev SAT Benchmarks

This page was built for publication: Using word-level information in formal hardware verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2487686)