Introduction to Formal Hardware Verification

تأیید سخت افزار یک موضوع داغ در طراحی مدار و سیستم به دلیل افزایش پیچیدگی مدار است. این کتاب درسی پیشرفته یک نمای کلی تقریباً کامل از تکنیک های تأیید سخت افزار را ارائه می دهد. تمام رویکردهای مورد استفاده در ابزارهای موجود، مانند نمودارهای تصمیم گیری باینری و سطح کلمه، روش های نمادین برای بررسی هم ارزی، و بررسی مدل منطق زمانی را پوشش می دهد و استفاده از اثبات قضیه منطقی مرتبه بالاتر را برای تأیید صحت مدار معرفی می کند. این خواننده را قادر می سازد تا مزایا و محدودیت های هر تکنیک را درک کند.
هر فصل شامل یک مقدمه و خلاصه و همچنین بخشی برای خواننده پیشرفته است. بنابراین مخاطبان وسیعی از مبتدیان در طراحی سیستم گرفته تا متخصصان مورد خطاب قرار می گیرند.

Hardware verification is a hot topic in circuit and system design due to rising circuit complexity. This advanced textbook presents an almost complete overview of techniques for hardware verification. It covers all approaches used in existing tools, such as binary and word-level decision diagrams, symbolic methods for equivalence checking, and temporal logic model checking, and introduces the use of higher-order logic theorem proving for verifying circuit correctness. It enables the reader to understand the advantages and limitations of each technique.
Each chapter contains an introduction and a summary as well as a section for the advanced reader. Thus a broad audience is addressed, from beginners in system design to experts.