| Authors: NamDo Kim - Samsung Electronics Co., Ltd.JunHyuk Park - Samsung Electronics Co., Ltd.Byeong Min - Samsung Electronics Co., Ltd.Wesley Park - Mentor Graphics Abstract: We propose a new register verification method that leverages formal verification to automatically generate a complete access policy specification for IP memory-mapped registers. While traditional register verification uses simulation to check IP compliance with a manually written specification, our method uses formal verification to automatically generate an IP compliant specification that designers manually check against their design intent. We introduce a register model that overcomes limitations in the expressiveness of the predefined UVM and IPXACT access polices. And, we present results from the successful application of our method to the register verification of three industrial designs. Introduction: IP designs contain many externally accessible registers, referred to as memory-mapped registers, that are used to control behavior, check status, and transmit and receive data. The implementation complexity of memory-mapped registers is relatively low compared with other design elements. Hence, register verification, the verification of memory-mapped registers, is mostly done by directed or lightly randomized simulation test benches and is viewed as a tedious job. Accessing memory-mapped registers is often no different from accessing general-purpose memory. Techniques used to verify general-purpose memory are a good starting point for register verification. However, to improve efficiency, memory-mapped registers can have complex access policies. For example, a readto- clear policy automatically clears the content of a register after reading it. The contents of a memory-mapped register may also be modified by internal operations. These complicate the task of register verification. Another practical difficulty is the lack of a reliable specification. The specification documents not uncommonly omit details, such as precisely when a memory-mapped register can be modified by internal operations. Developing a quality verification environment from an insufficient specification is a painful task: designers and verification engineers will be frustrated by many test failures resulting from undocumented behavior. To complete the verification task, they may mask or ignore failures. In the best scenario, the verification environment will be tediously updated until no more failures are observed. In this paper, we use formal verification to overcome the practical challenges of producing a reliable specification. We start register verification assuming no specification is available. Instead of verifying a target design based on a given specification, we use formal verification to explore all possible behaviors for each memory-mapped register. To embrace the wide-range of register behaviors, we developed a register model based on four aspects of register behavior. A small program post-processes the formal verification results and determines how each register behaves. Then, it identifies the access policies consistent with that behavior. If the identification matches the designer's intention, the verification is already done, since formal verification has thoroughly verified all possible behaviors. If it doesn't match, then there is either a design bug or an overlooked aspect of the registers' behavior. In Section 2, we give an overview and describe the benefits of our proposed register verification method. The implementation is introduced at a high-level in Section 3. In Section 4, we show a few different approaches to developing properties for formal verification, and discuss the implementation and the instantiation of the properties. The post-processing required after formal verification is described in Section 5. We present results in Section 6 and conclude in Section 7. View & Download: Read the entire Register Verification: Do We Have Reliable Specification? technical paper. Source: DVCon 2013 | |