Using word-level information in formal hardware verification

DOI10.1023/B:AURC.0000030907.28679.82zbMATH Open1073.68539WikidataQ59242893 ScholiaQ59242893MaRDI QIDQ2487686FDOQ2487686

Authors: Yanyan Li 

Publication date: 8 August 2005

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

Recommendations

• Publication:4504717
• 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

zbMATH Keywords

register-transfer-level specifications

Mathematics Subject Classification ID

Computer system organization (68M99)

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
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• Level-up -- from bits to words

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)