Computer-aided design and analysis of circuits and semiconductor – Nanotechnology related integrated circuit design
Reexamination Certificate
1998-10-14
2001-03-27
Smith, Matthew (Department: 2825)
Computer-aided design and analysis of circuits and semiconductor
Nanotechnology related integrated circuit design
Reexamination Certificate
active
06209120
ABSTRACT:
BACKGROUND
This invention relates to hardware and software design verification.
One facet of hardware/software co-design is dealing with verification at the hardware/software interface. In the typical case where the hardware and software are designed separately, a common problem is that the expectations of each design group do not match the implementation of the other. This is particularly true in situations where the hardware and the software interact extensively, with each part controlling the behavior of the other. When such interfaces are not properly handled, logical failures are likely to result, with attendant costly delays in production. The familiar presumption that the hardware and the software each can be designed successfully with only a sketchy understanding of the other side is unwarranted in complex systems. Each design team needs a precise description of its “environment” as defined by the other design. If formal models of the hardware design and the software design are used in support of this need, the problem of interface mismatch is moved to a problem of how to develop a design in the context of a formal environment description.
Conceptually, formal verification could offer a solution to this problem. However, direct application of model-checking in this context is mostly infeasible, because each side individually is often near the limit of feasible verification. Moreover, there is an intrinsic difficulty in applying finite-state verification to software, which often is viewed as an infinite-state system on account of its dependence on memory.
While hardware/software co-design has been treated extensively in terms of methodology, no viable methods have been published on formal co-verification. The co-verification problem is treated mainly as a testing problem, and a number of commercial tools have appeared for testing software in the context of hardware, and vice versa.
Apart from the above, partial order reduction and symbolic state space search have been applied widely to cope with the intrinsic computational complexity of modelchecking. Typically, these techniques are applied separately—only one or the other—since they appear to be incompatible. Partial order reduction algorithms found in the literature are based intrinsically on explicit state enumeration in the context of a depth-first search. The partial order reduction found in the prior art is derived dynamically in the course of enumerating the states. Symbolic verification deals only with sets of states defined by respective Boolean functions. State reachability is expressed in terms of the convergence of a monotone state set operator which implements a breadth-first search of the state space.
What makes partial order reduction problematic in this context has to do with guaranteeing that certain transitions which may be deferred in the course of the state space search (thus giving rise to the desired reduction), are not deferred indefinitely (resulting in an incomplete search). The usual way this is implemented in the context of explicit-state enumeration, is to explore all such deferred transitions in the course of closing any cycle during a depth-fist search.
Nonetheless, there is no intrinsic reason that partial order reduction and symbolic verification cannot be combined. Perhaps the first published proposal for such a combination is presented by R. Alur, R. K. Brayton, T. A. Henzinger, S. Qadeer, and S. K. Rajarnani, in “Partial order reduction in symbolic state space exploration,”
Conference on Computer Aided Verification
(CAV 97), LNCS 1254, Springer-Verlag, (1997) pp 340-351. In that paper, the cycle-closing condition is replaced by some additional steps in the course of the symbolic breadth-first search, and those additional steps require the normal modelchecking algorithm to be altered.
SUMMARY
The obstacles of hardware/software co-verification are overcome with a method that employs partial order reduction and symbolic verification without requiring the existing model checking algorithms to be altered. Specifically, the hardware is specified in a hardware-centric language, the software is specified in a software-centric language, and the two specifications are applied to a single design verification tool that is adapted to operate with both languages. Functionally, the co-design is verified by identifying properties that are to be verified, and by verifying each of the properties individually. In verifying each property, only those components are considered in the hardware and software parts of the system that influence the behavior of the property. In the verification process, static partial order reduction is employed to identify the software states that need to be considered, which allows disregarding other software states. The static partial order reduction disclosed is completely isolated from the model-checking algorithm and it therefore does not depend on a specific search technique.
In order to have the partial order reduction of the asynchronous software model be compatible with the synchronous hardware model, the asynchronous model is transformed to an equivalent synchronous model and the partial order reduction is implemented in terms of constraints defined by automata. These automata are defined at compile time. The synchronous transformation uses non-determinism to simulate asynchrony and the constraints remove transitions which are redundant with respect to the partial order reduction. Thus, an implicit form of the entire partial order reduction is created statically by the compiler, without any need to modify the verification tool.
Illustratively, the software model employs the SDL language. The hardware is expressed in a synthesizable subset of VHDL or Verilog. The two models coordinate through interfaces, each of which looks like an SDL process to the software side, and an HDL module to the hardware side. Both the software and hardware models are then applied to a verification tool. Illustratively, the verification tool COSPAN is employed, and both the software and hardware models are pre-compiled into SIR, which is the input language of COSPAN. The reduced model is checked by COSPAN in the same manner as any synchronous model.
REFERENCES:
patent: 5537580 (1996-07-01), Giomi
patent: 6044211 (2000-03-01), Jain
Kurshan Robert Paul
Levin Vladimir
Minea Marius
Peled Doron A.
Yenigun Husnu
Brendzel Henry T.
Do Thuan
Lucent Technologies - Inc.
Smith Matthew
LandOfFree
Verifying hardware in its software context and vice-versa does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Verifying hardware in its software context and vice-versa, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Verifying hardware in its software context and vice-versa will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2459924