hledat:

SystemVerilog verification of VHDL design

CESNET technical report number 35/2007
also available in PDF, PostScript, and XML formats.

Petr Kobierský, Tom Málek, Viktor Puš, David Šafránek
30.11.2007

1   Abstract

This document describes digital design verification methods used in Liberouter project. Because of the high effort required for employing exhaustive formal verification method of model checking on large and rapidly developed designs, we have explored possibilities of supplementing this method by a relatively easily practicable simulation method based on the notion of testbenches. In particular, we report on SystemVerilog framework for automated and manageable tests and we highlight the most interesting aspects of both mentioned verification methods. Finally, we evaluate the SystemVerilog simulation on complex Internal Bus design. Very good results of SystemVerilog simulation encourage use of this approach to all critical and complex designs. We also state some preliminary ideas of how to combine both verification methods together to gain maximum of their features.

Keywords: VHDL, SystemVerilog, Verification, Simulation

2   Introduction

Owing to inherent intricacies of designing firmware using the VHDL language, in our case for the purpose of developing a modular FPGA-based high-speed network monitoring and routing hardware in the Liberouter project, we employ various verification techniques to minimise the amount of logical errors. In particular, we have adapted methods of two principally different kinds - exhaustive formal verification, i.e., model checking, and simulation.

The former method is characteristic by its very strong property - completeness. More precisely, when a specific property of a design is formally verified, all the possible runs of the design are checked [MC]. However, from our experiences [KRS], [HTF], it follows that formal verification requires a very significant effort to be satisfactorily applied in the sense of an automatised phase in the entire development process. Especially, the important assumption of this method requires verification experts to deeply understand subtleties of VHDL code. In such a setting, it is often impossible to respond quickly enough to fulfil the needs of dynamic VHDL development. This is not the case for the latter method. The simulation method, although it is incomplete, has an advantage that it can be realised directly by VHDL developers and thus it can be applied with rapidly shorter response time.

Because of the reasons mentioned above, we have decided to accompany the formal verification method by the simulation method. Due to its compatibility with the VHDL language, we have chosen a simulation method based on SystemVerilog. The future direction of verification in our projects tends towards a general verification framework in which both methods are used in suitable collaboration.

In this report we describe our approach of adapting the SystemVerilog simulation method to the needs of FPGA-based VHDL design. Before we introduce the SystemVerilog method, we briefly summarize our formal verification framework and highlight its advantages and disadvantages. We also put some preliminary ideas towards a collaborative framework of the formal verification we have used by now and the simulation method introduced in this report. Finally, in the main part of the report we evaluate the suggested simulation method based on SystemVerilog.

3   Formal verification method

Formal verification is a verification method which supplements classical testing methods. It can be especially useful for proving safety critical properties of the system under development. The preliminary assumption for doing any kind of formal verification is existence of a formal specification. In particular, all crucial properties of a design have to be explicitly given in some formal logic. We employ the model checking method which is the only formal method that can be performed fully automatically. In this case, the formal specification has to be realised in terms of temporal logic formulas [CLK].

The workflow [VP] according to which we employ model checking is illustrated in Figure. In particular, VHDL code of the design under verification (DUV) is synthesised to the gate level and the resulting code is translated into the verification model. We use a specific model checking tool suitable for hardware verification - Cadence SMV.

The way of how we get the temporal logic specification of a particular DUV relies on special lines which developers can insert into the original VHDL code - the so-called assertions. The most basic form of assertions is just the formula of a temporal logic. However, because of the complexity of temporal logic formalisms and thus their practical limitation, we have developed a framework of Verification Cookbook [CBK] which allows developers to use assertions stated in a natural language. However, every such informal assertion must be translated by verification experts to a temporal logic formula in order to perform model checking.

Our experiences with model checking show that the need for temporal logic specification and the need for modelling the environment at the verification model level are the phases which require a lot of effort. Verification experts has to go deeply into hardware principles in order to develop the correct environment and formulas of the formal specification. This fact slows down the verification process rapidly. Thus in spite of the availability of sophisticated methods for hardware model checking, e.g. [CFR], it is still long way to gain all the power hidden in formal verification in order to satisfy the needs of the fast state-of-the-art hardware development.

The above mentioned strict format of the specification is required because of the completeness of the model checking method. On the other hand, when dealing with incomplete simulation methods, the environment and the specification must be also given, but in a human-readable form. This allows the simulation method to be applied more quickly and directly by developers.

To conclude, we suggest for the nearest future to use the formal verification method for ensuring the correctness only of the most crucial modules of the design. On the other hand, we believe that a supplementary simulation (testbench driven) method could very rapidly increase the overall quality of the entire design. For future work, we aim to develop a mechanism which would adapt the simulation environment and the specification to the respective counterparts in the formal verification framework.

4   Simulation methods

Simulation is not exact mathematical approach. It instead examines design behaviour under certain conditions and then checks if design outputs are correct. Simulation environment usually consist of two basic components - device under test(DUT) and testbench. Testbench is responsible for driving DUT inputs and checking correct DUT behaviour.

Simple approach to write testbench is to directly set signal values. This gives us ultimate control over all inputs of the DUT. However, it becomes extremely complicated to write inputs for complex DUT by hand. Typically, designs may have hundreds of input signals, and there is a communication protocol which has to be satisfied. Also, check for correct DUT function involves manual checking of DUT output signals, which is tedious and ineffective.

Basic improvement of this process introduces Bus Functional Models (BFMs). BFM is a simulation component, which is used to transform high-level protocol units (packets, transactions, commands...) to actual signals values. Designer have to only create high-level description of the protocol unit (ie. data structure) which is passed to BFM. This models can be also used for automatic behaviour testing, but designer have to provide expected result during test specification.

Bus functional models can be implemented in VHDL language, but VHDL lacks some higher-level language features which would be useful to raise testbench effectiveness. So there is a need for a simulation language which support high level construct and is also suitable for VHDL simulation. Language which best suits this requirements is SystemVerilog.

5   SystemVerilog language

SystemVerilog is a complex programming language for hardware description and verification. While created as a next generation of the Verilog language, it has adopted features from many other languages, with great impact on its simulation and verification strength. SystemVerilog object orientation enables advantages known from other OO languages. It gives us the potability to use standard design patterns for complex application design. As for code reuse, it is also well supported using inheritance.

Designers can take advantages of direct language support for constrained random variables. This feature is a simple but still powerful way of generating random inputs for DUT. Together with it, we want to check whether some important input combinations (or all of them) were exercised. So also internal design states coverage is important measure of the quality of verification. This is called functional coverage and it is supported by this verification language.

SystemVerilog provides smart mechanism known as Interfaces, which is very useful especially if there is a greater number of signals to be connected. Basically, it is the grouping of several signals to one identifier, but the strength of SystemVerilog interfaces is much greater. Usually, interfaces are used together with powerful temporal logic assertions.

Currently the major commercial EDA vendors (Cadence, Mentor, Synopsys) have publically pledged support for SystemVerilog. Because SystemVerilog embodies a large number of new language constructs and concepts, vendors will rollout SystemVerilog features in stages. SystemVerilog was evaluated using Mentor ModelSim tool, which have support for all mentioned SystemVerilog features.

SystemVerilog was evaluated on the Internal Bus Switch component and later on whole Internal Bus [ISN]. The internal bus is a high throughput bus dedicated for transferring data between FPGA components internally as well as between FPGA components and the PCI interface. This bus was developed for NetCope platform and it also represent most critical part of it, so bug free design was requested. In the following chapter we describe testbench architecture which has been used for Internal Bus switch testing. Similar testbench architecture can be used for testing of most Liberouter components.

5.1   System Verilog Testbench architecture

For verification of Internal Bus Switch component the following testbench architecture was designed (see Figure 2). The testbench gets benefits from SystemVerilog features, it is automatic but also manageable. It can be used for random as well as for direct testcases. Thanks to OOP paradigm the BFM models can be easily used in next projects or can be extended for another functionality using inheritance.

On the highest testbench level there is only Internal Bus Switch (DUT) connected to test component through interfaces. The test component is represented by sequential program where it is necessary to create test environment at first. The instances of BFM models and needed mailboxes are allocated and correctly set (e.g. callbacks). Then there can be an arbitrary number of test cases to verify particular features of DUT. The test cases can be random or direct. The random test cases set the transaction constrains and run random transaction generators for a specified time. The direct testcases disable the random generators and can send user defined transactions - useful for testing edge values of transactions (max length, border addresses etc.). Individual test cases can be separated by design reset.

In Figure, there is the full architecture of test program. The instances of three BFM models for sending (ib_driver) and receiving (ib_monitor) transactions are connected to specified switch ports. Three instances of generator randomly generate transactions within given constrains and send them through Mailboxes (communication channels) to driver BFMs. After driver successfully sends the transaction to switch, it passes transaction by callback to scoreboard instance. The instances of monitor BFM waits for incoming transaction on target switch ports. After successful receiving of transaction from physical interface, the transaction object is created. The object is sent via callback to scoreboard.

The scoreboard represents here a self-checking mechanism. Actually it implements the same functionality as a DUT component, using higher level constructs. After receiving a transaction the scoreboard decides what switch have to do with the transaction. If the transaction won't be dropped, it is stored into expected transaction list with expected receive port number. If incoming transaction matches the expected one, it is deleted from the expected transaction list, otherwise error is reported. After finishing test, the expected transaction list must be empty otherwise the switch doesn't work correctly and error must be reported.

Another benefit of SystemVerilog is functional coverage capabilities. Functional coverage gives a feedback for automatic test control. When coverage is constant for a small amount of time, it's a right moment to change parameters (constrains) of generator, driver, etc. to get higher coverage. In our test we measure transaction and command coverage. Transaction coverage deals with types of transactions, length of transaction, addresses etc. It exactly checks if all transactions in all lengths were send. The command coverage checks if control signals of internal bus protocol were set in all acceptable combinations. For functional coverage block schema see Figure 4.

6   Conclusion

This report presented how even a complex hardware design can be verified with the help of SystemVerilog language. Main advantages of this approach were:

• Object Oriented Programming - Easier design, possible use of common design pattern, better code reuse.

• Interfaces and Assertions - More protocol checking, readable code.

• Constrained Random Variables and Functional Coverage - Better design state exploration.

Thanks to SystemVerilog automated testbench, which exercise all relevant input combinations the several bugs were found. For each Internal Bus component about 5-10 bugs were located and fixed even when the components passed many hardware tests under heavy load before. We are not denying the importance of formal verification methods, we even believe that these methods will gain popularity in the future. But this case study shows that simulation approach is also very efficient and can help with finding many bugs in design phase, so development cycle can be much shorter.

References

[CLK]	Clarke E.M et al.: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications, ACM Transactions On Programming Languages and Systems 8(2): 244-263, 1986
[CBK]	Kratochvíla T.: Verification cookbook (Liberouter policy WWW Pages), available online.
[KRS]	Kratochvíla T., Řehák V., Šimeček P.: Verification of COMBO6 VHDL Design, Technical report 17/2003, Praha: CESNET, 2003
[ISN]	Martínek T., Tobola J.: Interconnection System for the NetCOPE Platform. Technical report 34/2006, Praha: CESNET, 2006
[MC]	Clarke E.M., Grumberg O., Peled D.A.: Model checking, MIT Press, 1999
[HTF]	Holeček J. et al.: How to Formalize a FPGA Hardware Design. Technical report 4/2004, Praha: CESNET, 2004
[CFR]	Clarke E.M. et al.: Program slicing for VHDL. International Journal on Software Tools and Technology Transfer 4(1): 125-137, 2002
[VP]	Holeček J. et al.: Verification Process of Hardware Design in Liberouter Project, Technical report 5/2004, Praha: CESNET, 2004