Development Trends of System-Level Design and Verification Languages

To solve the system-level design problem, we must first solve the system and function description problem. The competition for system-level design languages ​​is in full swing. A language is needed to describe the entire system, including embedded software and analog circuits. The current register-level hardware description language will become the assembly language of hardware design. Design and verification engineers will only use them in key parts to achieve higher performance, and generally will mainly use systems and languages ​​for design and verification.

This paper will comprehensively review the current system-level design and verification languages ​​and their development trends. Sections 2 and 3 will review the development of system and design languages ​​and verification languages ​​respectively. Section 4 discusses the current mainstream verification methods.

2 System-level design language

2.1 Requirements for system-level design language

The characteristics of system-level design are: more and more complex functional integration and synthesis, functional modules or IP cores, including memory, processors, analog modules, interface modules, high-speed, high-frequency input and output and software modules. Therefore, it is necessary to consider the division and optimization of software and hardware, as well as collaborative design and collaborative verification. According to the characteristics of system-level design, it is generally believed that the system-level design language should have the following characteristics:

1) It has formal semantics.

2) Support the integration of special domain specifications.

3) Support the composition of computational models that describe systems and components.

4) Support more abstract modeling.

5) Support the representation and integration of restriction information.

6) Explore the design space consistently and continuously throughout the design process, from design specification to design implementation.

7) Support preliminary analysis and verification in specific fields and multiple cross-cutting fields.

2.2 Development of System-Level Design Language

The early 21st century was the period of the most rapid development and change of system-level design languages. Various system design languages ​​have sprung up like mushrooms after a rain, and the existing system-level languages ​​can be divided into three categories.

The first category is languages ​​that are derived from the extension of classic languages, such as SystemVerilog[1]. SystemVerilog has made fundamental changes to the original Verilog in terms of its development towards a higher level. It combines Verilog, C/C++, and CoDesign Automation's SuperLog to provide designers with the most powerful capabilities. SystemVerilog is an extension of IEEE 13642001 Verilog to assist in providing abstract system structure-level models for generating and verifying them. Its outstanding feature in terms of interfaces is that it can realize module connections at a high level of abstraction. Structures similar to C language, such as assertion structures, support property verification. The main purpose of the extension is to enable the Verilog language to support large-scale designs and achieve a higher level of abstraction. It also borrows C data types such as "char" and "int". All C codes can be directly used in Verilog models and verification programs. The advantage of this type of extension method for traditional languages ​​is that it facilitates a smooth transition for designers, but those who advocate the use of C language as a system-level language doubt that this "improved" method will not be able to achieve satisfactory results in terms of efficiency during simulation.

The second category is to use the languages ​​and methods in the software field, such as C/C++, Java, UML, etc. Those who advocate using C/C++ as a system-level design language believe that over time, C's automatic compiler and other automated tools will eventually be used to achieve the compilation from C/C++ models to chips. In the current situation where the tools are not perfect, manual and step-by-step refinement of the design is necessary. In other words, C/C++ currently needs to expand the hardware expression components instead of only describing them at the algorithm level. For example, SpecC (the University of California, Irvine), ardwareC (Stanford University) HandelC (originally at Oxford University, now transferred to Embedded Solutions Ltd) SystemC++ (C Level Design Inc) SystemC (Synopsys Inc) Cynlib (CynApps), etc. These languages ​​can be divided into two categories: one is to expand on the standard C language, represented by SpecC; the other is to use the extensibility of C++, represented by SystemC, which provides a set of basic hardware components that can be expanded to support hardware at a higher level. These two complementary methods support hardware description at four levels, namely algorithm, module, cycle accurate and register transfer (RTL) levels. Before SystemC20, some people believed that SystemC focused on simulation and SpecC focused on specification and structural modeling, with synthesis and verification as the goal, but after SystemC20, these statements are no longer accurate, because the current SystemC2.0 can support all system-level requirements. SystemC fills the gap between traditional HDL and C/C++-based software development methods. It contains C++ class libraries and a simulation kernel that is used to generate behavioral and register-level models. It is managed and supported by leading EDA manufacturers and integrated with commercial synthesis tools. It supports general software and hardware development environments.

We believe that C++ is a better choice than C. This is because C++ is extensible, and because the concurrency concept in hardware is easy to express using class libraries, and the object-oriented nature of C++ corresponds well to the hierarchical nature of HDL.

People are also discussing whether Java can be used as a system and high-level hardware description language [2]. For example, LavaLogic first proposed JHDL, which converts Java language descriptions into comprehensive HDL programs and then uses the provided tools to convert them into gate-level descriptions. Those who support Java as a system-level description language believe that Java can improve description and operation efficiency. Compared with current HDL, it can express high-level concepts in very short programs. C/C++ has an inherent ability to express concurrency, while Java can express concurrency explicitly using threads. However, Java does not support templates and operator overloading, so a large number of procedure calls may be generated.

The third category is a brand new system-level language. For example, Rosetta, with this language, users can describe the behavior and constraints of almost any engineering field, including analog, digital, software, microfluidics and mechanics. However, it cannot replace and implement Verilog, VHDL and C. It was developed by the US DARPA to provide designers with the ability to describe large and complex computing systems, especially systems that mix multiple technologies. It can define, capture and verify the constraints and requirements of the system and its components at a high level. It provides semantic models that define and combine multiple fields for modeling and analysis. Its semantics is formalized, extensible, and can adapt to the requirements of new systems.

Rosetta's design methodology is based on the concept of facets of a polyhedron. A facet is a model of a component or system that provides specific information about the domain of interest. To support the design of heterogeneous systems, each facet provides domain-specific vocabulary and semantics. It is used to define views of the system from different perspectives, and then different facets are combined to form component models. Component models are then combined to form system models.

Rosetta's facets syntax should be familiar to users of existing hardware description languages. Its syntax is almost the same as VHDL. The main difficulty in designing this language is to unify information from multiple fields in a design activity. For different fields, such as analog, digital, mechanical, and optical components, Rosetta provides a mechanism to define and understand the system. Not only that, it also provides technology for modeling the expansion of new fields, which is very important for the future development of the language. Failure to correctly understand the interaction between different fields is often the root cause of system failure. Therefore, Rosetta provides explicit interaction modeling and methods to evaluate these interactions.

3 System-level verification language

3.1 Transaction-based Verification and Assertion-based Verification

The introduction of verification language needs to explain transaction-based verification and assertion-based verification. One of the strategies to solve the so-called "verification crisis" of system chips is transaction-based verification (TBV). A transaction is a conceptually single transfer of data or control. This transfer is determined by the start time, end time and all related information of the transaction. This information is stored together with the transaction as the attribute of the transaction. Transaction processing can be a simple memory read and write, or it can be the transmission of complex structured datagrams in network channels. Raising the level of verification from the signal level to the transaction level makes testing more intuitive, which is conducive to the measurement of test generation, error correction process and functional coverage. Designing system structure is not about imagining how enable signals and address buses work, but about imagining how data flows and is stored in the system. TBV is the natural development of this high-level design process. The qualitative verification process includes three steps: test generation, design error checking and functional coverage analysis. Each stage must be raised to the abstract level of transaction processing. Transactions can be constructed using the Verilog language task. This may be acceptable for basic testing, but when complex data structures, complex test plans and dynamic test generation are required, too many restrictions will be generated. High-level verification languages ​​(HLV), such as TestBuilder (C++), Vera, and E, developed in recent years, are designed to solve these complex problems.

Assertion-based verification (ABV) is an effective way to integrate formal methods into traditional simulation processes. The design team inserts design intent (assertions) into the RTL design and performs simulations. Then, formal techniques are used to check assertions, constraints, that is, assertions of legal interface behaviors, and other assertions at the same time in the simulation. The results of assertion checking improve the effectiveness of simulation. Even with traditional simulation verification, assertions can greatly improve the efficiency of simulation. Assertion-based verification requires users to write assertions, which represent the properties to be verified, so a property description language is required. For example, logical and timing properties. These are also problems that verification languages ​​need to solve.

3.2 Overview of Current System-Level Verification Languages

The IC design and EDA communities need a standardized verification methodology with an open interface. In 2000, Open Verilog International and VHDL International joined together to form the Accellera organization. Its purpose is to promote, develop and foster new international standards in the system, semiconductor and design tool industries. This is to strengthen the language-based design automation process. Faced with several formal property description languages ​​that were not perfect in terms of syntax and semantics, Accellera conducted a selection process. The four candidate languages ​​were Motorola's CBV, IBM's Sugar, Intel's ForSpec and Verisity's e language. After discussion, the focus was on Sugar and CBV, and IBM's Sugar 2.0 was selected in April 2002[3]. The victory of Sugar 2.0 caused a split in the Accellera organization. Most EDA tool vendors, including Cadence, supported Accellera's decision. Another part turned to support Syopsys' OpenVera 2.0. As a true industrial standard language, Sugar 2.0 has simple and clear syntax and semantics. It is basically based on Linear Temporal Logic Language (LTL), which is an evolution of Sugar 1.0 based on Branching Temporal Logic (Computational Tree Logic CTL). Its key idea is to use an extended regular expression component. Therefore, it is easy to understand Sugar in the field of formal verification.

Sugar was developed by IBM's Haifa lab after eight years of research [4]. It is a descriptive formal property specification language. Its semantics are strict, but easy to understand and use. The properties to be verified can be described in a theorem-like form. These descriptions can be used as input for model checking and theorem proving, or as input for checking programs in simulation programs. Sugar consists of four layers:

Boolean layers consist of Boolean expressions.

The temporal layer describes the nature of logical values ​​changing over time.

The validation layer consists of some indicators that describe how the validation software uses the properties of tense. Some validation indicators also assume that certain properties hold. The validation layer also provides a way to divide Sugar statements into validation units.

The model layer provides methods for modeling input behaviors, describing auxiliary signals and variables and defining their behaviors. The model layer can also be defined as the names of properties and entities of the temporal layer.

Sugar has three flavors, corresponding to the hardware description languages ​​Verilog, VHDL, and environment description language EDL (the language used by IBM's RuleBase model checker). When using different styles, the syntax at the Boolean and model levels can be different, but the syntax at the temporal and verification levels is the same.

OpenVera 1.0 is a public verification language donated by Synopsys. For simulation, it has the ability to describe assertions. OpenVera 2.0, which was produced by the combination of Synopsys and Intel's ForSpec, can also support formal verification. OpenVeraForespec was jointly launched with Intel as an industry standard assertion language, but it was rejected because it was difficult for engineers to accept. However, its concept is still unique. Its goal is to be a property description language that supports simulation and formal verification. Components and operations borrowed from ForSpec include "assume", "restrict", "model", "assert", etc., which all serve formal verification. The language component "assumeguarantee" can use assertions as module properties and as monitors at a high level. When OpenVera is used to describe assertions, it can accurately describe the timing behavior over multiple cycles. Hardware description languages ​​such as Verilog and VHDL are used to describe the process behavior of hardware. This process model is difficult to effectively express the temporal behavior over multiple cycles. Using OpenVera's assertion language OVA, users can conveniently and intuitively describe input and output behaviors, bus protocols, and other complex hardware behaviors and relationships. Compared with the description of hardware description language, it is 3 to 5 times more concise. Compared with the 4-level structure of Sugar language, OpenVera 2.0 is divided into 5 main levels:

The context (environment) helps define the scope (or range) of the assertion.

Designator words describe the property to be inspected or monitored.

Boolean expression.

Event expressions represent time series.

The formula represents the relationship between time series.

Sugar and Open Vera 2.0 have two common layers, the Boolean layer and the temporal layer. These layers form the core of assertions. Their differences are in other layers. Open Vera 2.0 emphasizes the detailed structure of properties, and users can interact deeply with assertions to examine and explore the knowledge of formal verification. The other two layers of Sugar serve to "format" properties and simplify the interaction with users. In short, no matter which language is used, Open Vera 2.0 or Sugar, they all provide a means to efficiently verify complex system chips.

4 Review of current verification methods

Current design verification methods are developing rapidly, and design and verification languages ​​are emerging in an endless stream. However, the following views and conclusions are clear:

1) Formal methods have made great progress, especially equivalence checking has been integrated into the standard verification process. The main reasons why model checking technology and theorem proving cannot become the mainstream verification method in the design environment are as follows [3]:

① Lack of widely accepted property description language.

② Lack of commercial tools.

③There is still a lack of guiding principles for the effective use of formal methodology.

④ Still waiting to see whether the benefits of changing the verification method are obvious.

2) Formal methods need to be combined with traditional methods to be effective. The progress of design and verification methods should be gradual and revolutionary. Therefore, in the foreseeable few years, hybrid verification methods should become the mainstream verification method. Assertions have a profound effect and influence on the expression of interface restrictions, design properties and design assumptions. These will contribute to the discovery of design errors that could not be discovered by previous methods. It is particularly suitable for combining test coverage to greatly improve verification efficiency.

3) Assertion-based verification is a feasible approach to combine formal verification and traditional simulation verification [5]. The unified design and verification language that supports this approach is SystemVerilog. It is a transitional system-level design language developed by expanding the system description component on the new Verilog language standard. This language can uniformly describe complex design and test scenarios (testbenches). SystemVerilog supports multi-level interface design and assertions, making full use of current design verification technology and practices. It is backward compatible with Verilog and has inheritance, making it a combined design and verification language. This language has been supported by many EDA vendors and users and is expected to become popular.