Review of Principles of verifiable RTL design
By Lionel Bening and Harry Foster, Kluwer Academic Publishers, 2000.
Using verifiable RTL design, an engineer can add or improve the use of cycle-based simulation, two-state simulation, formal equivalence checking, and model checking in the traditional verification flow. Furthermore, a verifiable RTL coding methodology permits the engineer to achieve greater verification coverage in minimal time, enhances cooperation and support for multiple EDA tools within the flow, clarifies RTL design intent, and facilitates emerging verification processes.
This book addresses verification of synchronous designs. It provides a comprehensive understanding of various verification processes from conceptual and practical approaches. The concepts presented in this book are drawn from author experience with large-scale system design projects. It draws a technique methodology for verifiable RTL coding. The book is divided into nine chapters as follows. Chapter 1 provides a short introduction of this book. Chapter 2 introduces four principles of RTL design (fundamental verification principle, retain useful information principle, orthogonal verification principle, and functional observation principle) and issues related to verifiable RTL (design specification, test strategies, coverage analysis, event monitoring, and assertion checking). Chapter 3 introduces the basics of the RTL methodology and addresses the problem of complexity due to competing tool coding requirements. It introduces a simplified and tool-efficient Verilog RTL verifiable subset using an object-oriented hardware design (OOHD) methodology. Moreover, it details a linting methodology, which is used to enforce project-specific coding rules and tool performance checks. Chapter 4 presents the history of logic simulation, followed by a discussion on applying RTL simulation at various stages within the design phase. Chapter 5 discusses RTL and the formal verification process. It presents the concept of finite state machine FSM and its analysis and applicability to proving machine equivalence and FSM properties. Chapter 6 discusses ideas on verifiable RTL style. Chapter 7 provides examples on the common mistakes that are involved with projects, designers, and EDA verification tool developers. Chapter 8 presents a tutorial on Verilog language elements that can be used to build a verifiable RTL model. Chapter 9 summarizes the 21 fundamental principles of verifiable RTL Design, which are discussed throughout the book.
This book is considered one of the milestones for verifiable RTL design. It shows an efficient methodology for writing a verifiable RTL, and it defines guidelines for large-scale systems. I believe that every engineer working in the area of RTL design should read this book.
Wael Badawy, “Principles of verifiable RTL design“, IEEE Circuits and Devices Magazine, Vol. 18, Issue 1, January 2002, pp. 26 -27