Tham khảo tài liệu 'micro electronic and mechanical systems 2009 part 13', kỹ thuật - công nghệ, cơ khí - chế tạo máy phục vụ nhu cầu học tập, nghiên cứu và làm việc hiệu quả | Integration Verification in System on Chips Using Formal Techniques 411 Another approach is that of abstraction see Figure 4 and Figure 5 where the design is abstracted or simplified to remove portions of design not needed to prove a property. This can result in a substantial reduction in the number of flip-flops thereby enabling automated proof convergences of the formal properties. However for complex industrial RISC and DSP processors or SoCs based on them even these approaches are not be feasible. We will need newer formal verification approaches which are not limited by the state explosion problem. Recent research carried out by different academic and industrial research groups address these capacity issues in formal verification. Though no stable implementations of formal verification tools exist for such approaches they serve as good pointers to pursue in the future to address difficult verification problems. We give below very brief descriptions of some of the approaches. Fig. 5. Memory Abstraction to Reduce Complexity of Formal Verification Each memory bit adds to a state bit in the verification process Generalized symbolic trajectory evaluations Symbolic trajectory evaluation STE provides a means to formally verify properties of a sequential system by a modified form of symbolic simulation. In this the desired system properties or specifications are expressed in a notation combining Boolean expressions and the temporal next-time operator. If the state space of a system is a lattice the behavior of the sytem can be expressed as a trajectory a sequence of points in the lattice determined by the initial state and the system functionality. Formulas in a simple temporal logic express properties of the system. Given a formula one can derive bounds that trajectories with the desired property must obey. In its simplest form each property is expressed as an assertion A C where the antecedent A is a trajectory formula which expresses some assumed conditions on
