Hardware can be formally verified by describing both the implementation and the specification using finite automata and checking to see if the language of the specification contains the language of the implementation. This type of formal verification is called language containment [Kur90]. Most language containment tools use languages that are not popular, which increases the learning curve for new users. We propose performing language containment on designs and specifications written in the Verilog HDL. Our hope is that formal verification will be accepted more readily by hardware designers if they can use a familiar language and a modeling style consistent with existing design tools, such as synthesis and simulation. One type of finite automata is called an L-process. We will describe how they can be modeled in Verilog. Because L-processes frequently contain non-deterministic state transitions and outputs, we propose a natural method consistent with the language definition, current simulators, and current synthesis tools for modeling non-determinism in Verilog. In addition, L-processes can be extended to include restrictions on the time an L-process remains in a sequence of states. We propose methods to model timed L-processes in Verilog using existing timing constructs. We formally define the model of L-processes and show how the simulation model of Verilog is consistent with the formal verification model.
Requirements for new systems and products that are generally expressed in a variety of graphical and textual notations can be translated to conceptual graphs (semantic networks) for integration, consistency checking, and synthesis functions. In this paper, the capture, translation and integration of natural language, block diagrams, timing diagrams and state diagrams as used in specifying digital systems requirements are considered. For each of these source notations a set of basic concepts and their interrelationships are identified, and algorithms for automatically generating conceptual graphs from the notations are given. Mechanisms for integrating the resulting conceptual graphs and consistency are discussed.
The major difficulty in using HDL's to represent design information is that model preparation is a labor intensive task. Also, with VHDL, the large number of possible modeling approaches can lead to models that are unstructured and difficult to understand. In order for HDL's to be used effectively, systematic techniques for model creation must be developed. Some techniques for decreasing the time required to create a HDL model include: providing a means of partial graphical entry of the model; providing the modeler with a library of common, user-definable primitives; and supporting a well-defined modeling style. A CAD tool called Modeler's Assistant that utilizes these techniques to allow rapid development of VHDL behavioral models will be discussed.
Binary decision diagrams (BDDs) are a well known method for representing and comparing boolean functions. Although BDDs are known to be very compact, in all known approaches for hardware verification, BDD-based calculi are restricted to propositional logic. This logic is insufficient for the verification of abstract data types, time abstraction and also for hierarchical verification. In this paper, the lifting of graphs based on shannon expansions and the related binary decision diagrams to first order logic is described and the soundness and correctness theorems are stated. The power of these techniques in the domain of hardware verification is shown by a case study using a hierarchial circuit.
One difficulty in using conventional hardware description languages such as VHDL is the cumbersome nature of the textual syntax. We are developing a visual hardware description language, called vVHDL, based on VHDL. A Visual approach is very natural for expressing the concurrency inherent in hardware designs. vVHDL allows the graphical specification of both structure and behavior of hardware components in a uniform framework. This paper presents an overview of the vVHDL language and design system.
The Software Engineering Institute (SET) is a Federally Funded Research and Development Center (FFRDC) sponsored by the U.S. Department of Defense. The SEI was established in 1984 to improve the state of the practice in the development of software systems. A central component of the SEI strategy is technology transition. For the SEI to be effective at technology transition, we need to help organizations improve both their organizational processes as well as their technology basis. Process and technology improvements will reduce the risk associated with the development of industrial computing systems. To illustrate some of these risks we describe the current technical projects within the SEI Real-time Distributed Systems program, a feasibility study on a Science and Technology Maturity Model, and a planned Handbook for Industrial Computing Developers.
A method of modeling CMOS logic circuits for an accurate prediction of timing and logic operations is presented. In this methodology the ''lego'' concept is used for modeling logic gates and interconnection delays. The model contains complete timing properties integrated with logic operations. These timing properties are used to adjust the timing behavior of a logic circuit in simulation. An important application of this modeling method is in a synthesis process where lego timing models can be assembled as their corresponding hardware blocks are being placed and routed. All input and output values are represented in a discrete 10-region responsive logic value system. The models react to input values that cross the boundary of a region. This modeling method is implemented in VHDL.
In a formalism of top-down design, we consider the decomposition of behavioral specifications into interacting sequential components. The higher level of description specifies the operations to be performed in a major computation step. The goal is to incorporate a given interface specification in a lower-level specification that accounts for interactions with and among sequential components. This construction generalizes the earlier formalism of system factorization [14] to include interface protocols. It expands on the objectives of high-level synthesis by considering control-synchronization loops in scheduling. This paper presents a specification language for sequential process interaction and develops an interpretation based on finite-state-machines. Operations of minimization, composition and complementation are defined; the last of these being the key to top-down decomposition. A small example is used to illustrate the ideas.
This paper examines a sample top-down design of a simple CPU starting with a system-level specification in VHDL and ending with an RT-level VHDL description that suits a commercial synthesis tool. Based on the requirement specification captured in a natural language, the design process starts with the creation of a system-level VHDL model, continues with several partitioning steps on system level and the transformation step from system down to RT level, and proceeds over several RT-level optimizations to the final VHDL description. Some of the RT-level optimizations are new in this context. The case study demonstrates the advantages of using VHDL for system-level specification and design and describes a design path comprising both manual interaction and state-of-the-art EDA tools.
The specification, design and verification of interface circuits with mixed timing (synchronous and asynchronous) represent an important aspect of VLSI ASIC design, where a complex TC device needs to communicate with other components such as memory, disk drive, graphic display, etc. This paper proposes a formal notation and methodology for the specification and simulation of mixed timing circuits. It can serve as a basis for future work in synthesis and verification. The new salient features of this framework include: a formal semantics for the specification language in terms of a fundamental state transition structure called state graphs; a two-level specification methodology which permits the separation of choice and concurrency; and finally the use of Boolean guards as a general mechanism for abstraction, for specifying state-dependent behavior, and for describing non-determinism.
A library of basic elements of hybrid electronic circuits has been developed and implemented in VHDL at Stuttgart University. It was shown, that VHDL, designed for digital circuits, can also handle the behaviour of analog components.
To compose sequential systems, designers usually have to devise a synchronization mechanism which coordinates constituents of the composition in order to achieve certain goals of computation. In this paper, we present a simple language for specifying sequential behaviors. An advantage of the language is that a specification of synchronization, when composition is required, can be easily obtained from specifications of subsystems. We also briefly describe an algorithm which converts a specification of synchronization to a description of synchronization in our language. Our approach illustrates that, with a proper sequential descriptions of subsystems, necessary synchronization can be obtained automatically. This frees designers from control design, thus leaving more time and energy to consider architectural improvement and timing efficiency.
This paper describes Prevail-DM, a framework-based design environment for formal hardware verification. Prevail-DM is a platform for the definition and execution of proof strategies. It provides various provers that are applicable to different types of circuits, description styles, and abstraction levels. Proof tools are integrated around a conceptual schema based on VHDL, according to a black-box approach. Design methods maintain application-related integrity constraints. Prevail-DM is implemented upon the Cadlab framework and uses most of its services.
We describe the application of VHDL simulators to check the conformance of a design with Design for Testability (DFT) rules. The basic idea is to define a special DFT logic using VHDL's powerful logic modeling capabilities and to perform a kind of symbolic simulation based on this DFT logic.
Simulation is most widely used for the verification of VLSI circuits design. This paper highlights the importance of mixed-mode digital-analog simulation and describes its basic principles. The second topics of this paper is hardware description languages that cover both the digital and the electrical levels. The last part presents the current standardization effort for Analog-VHDL. The main requirements are presented, and a complete example is given.
SDL is a CCITT standard for the specification of distributed software systems. It is widely used mainly in the telecommunication area. Although one goal during the development of SDL was to support the specification and description of communication systems consisting of both hardware and software, SDL is mainly used in the software design process today. One reason why SDL did not gain acceptance among hardware designers might be the big gap between specification and hardware implementation. In the software domain code generators for several programming languages, e.g., CHILL, C, C++, or PASCAL have been made available to close the gap between design and implementation. Similar tools for hardware are missing so far. This paper describes the application of SDL to system-level design of hardware. A translation of SDL descriptions into the standard hardware description language VHDL is presented. This translation allows one to implement SDL descriptions in hardware with state-of-the-art synthesis tools.
The major purpose of this paper is to present a general redesigning methodology, which is able to optimize the circuit area and processing speed simultaneously under the constraints of time and area at a speed of O(nlog(n)). Our methodology first designs the most serial data-path with the smallest area, and then, repeats the stepwise modification of the data-path based on an efficient redesigning method employing the Time-Area ratio (T-A ratio in short) until a nealy optimized one is obtained.
A ‘Practical Concurrent Design Environment’, CODES, for the design of hard-ware/software systems is described. It is shown that hard-ware/software Co-Design can be based on an abstract model of communicating parallel random access machines (PRAMs). Major design phases of CODES such as modeling, component design, simulation, and integration into a working prototype are outlined. CODES contains a novel framework that governs the flow-, data-, and task-management of Co-Design processes. The description of the framework illustrates the integration of new tools into CODES, and the modeling the design process with Petri nets. A sample application proves the feasibility of our approach.
Formal verification methods provide a way to prove that a circuit structure correctly implements its specification. Low level gate and transistor logic circuits can be verified using methods such as symbolic simulation. Higher level circuits can be verified using theorem-proving methods, providing a multi-leveled approach to complex device verification. Correct modeling of many VLSI circuits requires a signal value data type that includes some degree of strength indeterminacy. The VHDL Standard Logic Package includes such a signal value data type, t(-)wlogic, that includes 46 unique values. In this paper we provide a foundation for the t(-)wolgic values and their resolution function that provides a possible link between simulation and theorem-proving. A formalization of the low level signal values used by design tools also facilitates reasoning about CAD tools.
