Automated RTL verification based on predicate calculus

DOI10.1007/BFB0023725MaRDI QIDQ4037377zbMATH OpenFDO

Authors Michel Langevin

Publication date 18 May 1993

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0023725

zbMATH Keywords

acyclic graphregister transfer leveltransfer formulasverifying synchronous circuits

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Circuits, networks (94C99)

Recommendations

• An exercise in the automatic verification of asynchronous designs
• Automatic Verification of Sequential Circuits Using Temporal Logic
• scientific article; zbMATH DE number 3991420
• scientific article; zbMATH DE number 3861073
• scientific article; zbMATH DE number 868112

Cited in

(11)

• An exercise in the automatic verification of asynchronous designs
• Indentification of inductive properties during verification of synchronous sequential circuits
• Rewrite based hardware verification with ReDuX
• scientific article; zbMATH DE number 4018390 (Why is no real title available?)
• scientific article; zbMATH DE number 3991420 (Why is no real title available?)
• scientific article; zbMATH DE number 516995 (Why is no real title available?)
• Formally-based design evaluation
• Verification of basic block schedules using RTL transformations
• Automatic Abstraction of RTL IPs into Equivalent TLM Descriptions
• Comparing generic state machines
• Formal verification of arithmetic RTL: translating Verilog to C++ to ACL2

This page was built for publication: Automated RTL verification based on predicate calculus

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