Zoran Corp. (Haifa, Israel) has successfully developed a single-chip solution for playback of various types of discs, which are used across a range of video and audio products addressing the growing consumer multimedia markets. The chip decodes and displays MPEG1 and MPEG2 system bitstreams, including video and audio, as well as sub-picture and on screen display.

Previously, the verification methods used to verify the chip were based on a software simulator approach (a behavioral implementation of the chip written in software), versus the hardware implementation written in Verilog by a set of tests. The tests attempted to cover as many possible combinations as initially defined in the test plan. Although the chip was successful in the early version, several problems were identified in the original control mechanism - problems that were uncovered by the simulation environment and were later analyzed and observed with formal verification methods.

This article outlines the application of formal verification through model checking of the control unit in a DVD decoder chip. The work was initiated to evaluate and explore how formal techniques and tools could be introduced into a small to mid-size industrial company, where cost and performance are crucial. The evaluation process described here provided the basis for a strategic decision to incorporate formal verification as a mandatory part of the company's verification methodology. The work described here provides brief technical overview of the MPEG elements that were used in building the formal model of the block.

Syntax and semantics

MPEG video is a generic method for compressed representation of video sequences. The MPEG-2 concept is similar to MPEG-1, but includes extensions to cover a wider range of applications. The representation supports constant bit-rate transmission, variable bit-rate transmission, random access, channel hopping, scalable decoding, and bitstream editing, as well as special functions such as fast forward playback, fast reverse playback, slow motion, pause and still pictures.

The highest syntactic structure of the coded video bitstream is the video sequence. A video sequence commences with a sequence header which may optionally be followed by a group of pictures header and then by one or more coded frames. The order of the coded frames in the coded bitstream is the order in which the decoder processes them, but not necessarily in the correct order for display. The video sequence is terminated by a sequence_end_code.

The MPEG2 specification deals with coding of both progressive and interlaced sequences. The output of the decoding process, for interlaced sequences, consists of a series of reconstructed fields that are separated in time by a field period. The two fields of a frame may be coded separately (field-pictures). Alternatively, the two fields may be coded together as a frame (frame-pictures). Both frame pictures and field pictures may be used in a single video sequence. In progressive sequences, each picture in the sequence is a frame picture. The sequence, at the output of the decoding process, consists of a series of reconstructed frames that are separated in time by a frame period.

A frame is the union of a top field and a bottom field. The top field is the field that contains the top-most line of each of the three matrices (a luminance matrix, and two chrominance matrices). The bottom field is the other one.

Reconstructionist thinking

A reconstructed picture is obtained by decoding a coded picture (a picture header), the optional extensions immediately following it, and the picture data.

A coded picture may be a frame picture or a field picture. A reconstructed picture is either a reconstructed frame (when decoding a frame picture), or one field of a reconstructed frame (when decoding a field picture).

Figure 1 - Picture this

An obvious relationship exists among the three different picture types, intra-coded (I), predictive-coded (P), and bi-directonally predictive-coded(B).

There are three types of pictures that use different coding methods: an intra-coded (I) picture is coded using information only from itself. A predictive-coded (P) picture is a picture that is coded using motion compensated prediction from a reference frame. A bi-directionally predictive-coded (B) picture is a picture that is coded using motion compensated prediction from a past and/or future reference frame(s) (see Figure 1).

If field pictures are used, then they occur in pairs (one top field followed by one bottom field, or one bottom field followed by one top field) and together constitute a coded frame. The two field pictures that comprise a coded frame are encoded in the bitstream in the order in which they occur at the output of the decoding process.

When the first picture of the coded frame is a P-field picture, then the second picture of the coded frame is also a P-field picture. Similarly, when the first picture of the coded frame is a B-field picture, the second picture of the coded frame is also a B-field picture. When the first picture of the coded frame is an I-field picture, then the second picture of the frame is either an I-field picture or a P-field picture.

When coding interlaced sequences using frame pictures, the two fields of the frame are interleaved with one another and then the entire frame is coded as a single frame-picture.

Frame reordering

When the sequence contains coded B-frames, the number of consecutive coded B-frames is variable and unbounded. The first coded frame after a sequence header can not be a B-frame. Meanwhile, a sequence may not contain any coded P-frames. A sequence must also not contain any coded I frames. Therefore, some care is required at the start of the sequence, and within the sequence, to affect both random access and error recovery.

The order of the coded frames in the bitstream, also called the decoding order, is the order in which a decoder reconstructs them. The order of the reconstructed frames at the output of the decoding process, also called the display order, isn't always the same as the coded order. This section defines the rules of frame reordering that shall happen within the decoding process. When the sequence contains no coded B-frames, the coded order is the same as the display order.

When B-frames are present in the sequence, re-ordering is performed according to the following rules:

• If the current frame is coded order is a B-frame, the output frame is the frame reconstructed from that B-frame.
• If the current frame in coded order is an I-frame or P-frame, the output frame is the frame reconstructed from the previous I-frame or P-frame if one exists.
• If the final frame has been decoded at the end of the sequence, the frame reconstructed from the previous I-frame or P-frame is output.

The repeat first field (RFF) flag is applicable only in a frame picture. In a field picture it is set to 0 and doesn't affect the decoding process. When this flag is set to 0, the output of the decoding process corresponding to this reconstructed frame consists of two fields. The other field follows the first field (top or bottom field as identified by top_field_first).

If it's set to 1, the output of the decoding process corresponding to this reconstructed frame consists of three fields. The first field (top or bottom field as identified by top_field_first) is followed by the other field, then the first field is repeated (see Figure 2).

The MPEG decoder chip consists of a demultiplex processor, video decoder, reconstruction unit, memory management unit, control block, and video-out logic and audio decoder. The on-chip processor is responsible for demultiplexing the system stream into video, audio, and sub-picture layers to separate streams. The video layer data is processed by the video-out logic and controlled by the CONTROL block. The CONTROL block gets the video stream information from the on-chip processor, and several synchronization signals from the video logic. It's responsible for controlling the flow of data block (picture content) from the input (decoding order) into the memory, and from the memory into the video-out interface (display order).

The CONTROL block simulation environment needed to contain several models: a processor for initializing the block with the various commands and a video interface to provide the relevant syncs. The implementation of such suitably robust models was difficult. As a result, a large set of full-chip tests was defined and implemented to try and test as logic combinations many as possible. The tests run-time was very long (each test ran more than 4 hours). Although the number of tests was quite impressive (40 full-chip tests only for this function), the post-silicon validation found some major bugs, which one of them even eliminated one of the main functions of the chip (one of the trick command). Those problems were later fixed in the final step of the validation phase (see Figure 3).

Enabling technology

Formal verification (model checker) is a technology that allows designers to check some properties of their design and then to prove that it are true under all circumstances. Today, two formal verification approaches are available, namely model checking and theorem proving. Here we exclude the description of equivalence checking that is used to compare between two levels of logic representations in formal methods.

Rule-base is a model checking-based formal verification tool developed by the IBM Haifa Research Laboratory [1]. It uses an enhanced version of SMV[3] as its verification engine. SMV is a symbolic model checker that uses binary decision diagrams (BDD) to represent the unit under test (UUT). With the tool, the user provides the design model in VHDL or Verilog RTL code and also provides the design specification in the form of queries. A query describes a property of the design to be verified. The query may also specify a set of constraints on primary inputs of the design. The constraints limit the set (or sequence) of possible values on those inputs consistent with the legal operation of the design. The tool either verifies that the property is true under all possible and allowable conditions or provides an error trace showing a case where the property fails.

The main goal here was to provide a fast and exhaustive unit verification environment of the CONTROL block. The classic alternative (a unit simulation environment) was considered hard to achieve due to the need of developing behavioral models that simulate the rest of the chip. Thus, only the chip-level simulation environment was available for testing the block behavior. The second goal was to conduct an evaluation of using the formal verification tool as part of the chip verification methodology.

Tool evaluation process

Various amounts of effort were required during the evaluation of the formal verification tool:

Training: Three Zoran engineers presented the 3-day course to IBM, which covered all typical and extensive usage of the tool's language structures. Two of them were the designers of the CONTROL block and the third was the verification engineer.

Development: The rest of the evaluation process was devoted to the development of the CONTROL environment and properties. It's important to emphasize that this relatively long period of formal environment development resulted from the complicated nature of the block interface. Initially, the information used to formally define the environment was based on long interaction with the designers who described the function of the block in the full chip and extraction of the various signals from previous simulations timing diagrams. In addition, the environment was incrementally enhanced and corrected according to the examination of the waveforms associated with the property results.

Analysis: After the environment was stable (properties passed or real bugs found), incremental enhancement were added to create a more robust definition for previously defined input signals. The amount of time required from the designers was minor. Except for a couple of false alarms (due to incomplete definition of the property or insufficient representation of the input environment), the designer was only called to review the results when real bugs where found.

As the environment became more mature with complicated properties that involved larger parts of the design and a greater number of registers, the run-time of each iteration became longer (as long as 24 hours for a property check). Formal implementation

The first step was to implement the basic environment of the CONTROL block. This task was accomplished within three days (the relative simulation environment bring-up was estimated at two weeks).

Figure 2 - Swimming upstream

Optional combinations of MPEG2 bitstream video syntax enhance system performance.

One of the most important advantages of using a formal environment was the ability to use an MPEG video encoder (partial ordering information only) capable of generating all possible combinations of bitstreams. The various combinations can include: sequence length varying from one to an endless sequence of picture types (I, P, or B pictures in any combinations), RFF on any interlaced frame, and TFF to maintain correct display order.

The approach used in the simulation environment cannot provide as rich a set of options because of the limited number of tests possible to run, and due to the need to generate those bitstreams sequences manually. Encoding MPEG with RFF and TFF necessitates "looking into the future." Since RFF impacts the polarity of the displayed field order, and the chosen displayed frame is determined by the sequence of pictures which is preceding the current picture, it's impossible to set the value of the RFF without knowing what the properties of the following pictures are.

In formal verification we solved the problem by using the "invar" statement.

MPEG formal encoder

The formal MPEG encoder is the basic element of the formal model. It's capable of generating a non-deterministic set of control sequences associated with the encoded bitstream. This implementation enables a full coverage of all possible bitstreams that could be issued by an MPEG encoder - a complex proposition when the number of different bitstreams and their lengths is unlimited.

Without this formal implementation and the reduction features of the rule-base tool, there was no way to cover all the testing combinations in a simulation environment. The development of such simulation model is a very complicated task. The simulation-based testing model requires usage of a predefined set of bitstreams (or video sequences). Each bitstream isn't limited in length, or in its content (for example, any legal sequence of picture types). Thus, an enormous number of tests are required.

The formal model definition approach enabled fast development of such an encoder (sample of the code related to the MPEG encoder is given below). Based on an efficient search procedure, the formal verification tool is used to automatically determine the correctness of the properties for all the possible input combinations.

The following code describing the MPEG formal encoder is written in EDL (rule-base environment description language). It starts with the video sequence structure generation, which includes the picture type, picture structure, and other parameters related to the picture header. In order to generate only legal bitstreams in respect to "top field always followed bottom field," we used the invar statement, which removed all the illegal bitstreams from the reachable states.

var
picture_type_id: {I,P,B};
assign
init (picture_type_id):= I;
next (picture_type_id):=
case
(processor_state=first_field)&processor_
write&first_picture : I;
(processor_state=first_field)&processor_
write: {I,P,B};
(processor_state=second_field)&processor_
write:
case picture_type_id=I : {I,P};
picture_type_id=P : P;
picture_type_id=B : B;
else : picture_type_id;
esac;
else : picture_type_id;
esac;

This machine starts with the first picture which is always I. It saves the value of its TFF and RFF in IDEAL_SAVED_TFF, IDEAL_SAVED_RFF. It then goes to the second picture which can be I, P, or B. If it's I or P, then it display the previous TFF (T if SAVED_TFF=1).

Figure 3 - A sense of control

The control block environment manages the video stream from the on-chip processor and synchronization signals from the video logic.

If it had SAVED_RFF=1, then it will increment the TOPorBOTTOM from T to B and back to T again. It will also save the values of TFF and RFF of the current reference picture. If the second picture was B, it will start the display according to the TFF value of the B picture. Whenever there is a contradiction between the previous decision and the current (RFF caused next phase to be Top but the next decoded picture has TFF=1 which means Top again), the ERROR_IN_BITSTREAM will be set. This rule is based on the assumption that the display order should be always Top after Bottom or vice-versa.

var Ideal_First_Field : {T,B};
assign (Ideal_First_Field):=
case
processor_write&picture_type_id=B&TFF : T;
processor_write&picture_type_id=B&!TFF : B;
processor_write&(picture_type_id=I|picture_
type_id=P)&Saved_TFF : T;
processor_write&(picture_type_id=I|picture_
type_id=P)&!Saved_TFF : B;
else : T ;
esac;
var Ideal_Last_Field : {T,B};
assign NEXT (Ideal_Last_Field):=
case
processor_write&picture_type_id=B&TFF
& !RFF: B;
processor_write&picture_type_id=B&TFF
& RFF: T;
processor_write&picture_type_id=B&!TFF
& !RFF: T;
processor_write&picture_type_id=B&!TFF
& RFF: B;
processor_write&(picture_type_id=I|picture_
type_id=P)&Saved_TFF&!Saved_RFF : B;
processor_write&(picture_type_id=I|picture_
type_id=P)&Saved_TFF&Saved_RFF : T;
processor_write&(picture_type_id=I|picture_
type_id=P)&!Saved_TFF & !Saved_RFF: T;
processor_write&(picture_type_id=I|picture_
type_id=P)&!Saved_TFF & Saved_RFF: B;
else : Ideal_Last_Field;
esac;

This part of the code will act to decode the expected field type (Top or Bottom) according to the set of rules described above. The ideal_first_field and ideal_last_field represent the outputs of a decoder model which follow the specification rules.

var Saved_TFF: boolean;
Saved_RFF: boolean;
assign
INIT (Saved_TFF):=0;
NEXT (Saved_TFF):=
case
picture_type1=FRAME:
case
processor_write&(picture_type_id=I|
processor_write&picture_type_id=P)&TFF : 1;
processor_write&(picture_type_id=I|
processor_write&picture_type_id=P)&!TFF : 0;
else : Saved_TFF;
esac;
picture_type1=FIELD_PAIR:
case
processor_write&(picture_type_id=I|picture_type_id=P)&TOPorBOTTOM=TOP : 1;
processor_write&(picture_type_id=I|picture_type_id=P)&TOPorBOTTOM=BOTTOM : 0;
else : Saved_TFF;
esac;
esac;
INIT (Saved_RFF):=0;
NEXT (Saved_RFF):=
case
processor_write&(picture_type_id=I|
processor_write&picture_type_id=P)&RFF : 1;
processor_write&(picture_type_id=I|
processor_write&picture_type_id=P)&!RFF : 0;
else : Saved_RFF;
esac;

The solution for the "look into the future" problem is provided here. The following lines are responsible to take out all the bitstreams that are not legal. The error_in_bitstream will be 1 when the Ideal field order will show Top after Top or Bottom after Bottom fields.

var ERROR_In_Bitstream: boolean;
assign (ERROR_In_Bitstream) :=
(Ideal_First_Field=Ideal_Last_Field)&
!first_picture&processor_write;
invar (ERROR_In_Bitstream=0);

The invar statement stands for: analyze all the paths and extract only those that follow the condition within the brackets.

Formal properties

The first set of properties covers the basic behavior of the CONTROL block (the decoding and display order). These properties helped to bring up a stable environment by means of synchronization with the various external inputs coming from the various blocks in the full-chip environment. Although these properties are basically the most important feature of the block and were exhaustively checked in the simulation based environment, it also turned out to have the first bug - found after the second day of running the tool (first rule). The guideline in writing a formal property is to leave as many environment variables free as possible.

This rule was the key element to finding the first bug as the function of one of the basic assumptions: Processor command has no timing relevance. All of the other properties (a total of 70) covered other aspects of the CONTROL functions such as on-line commands and status bits.

Before rule-base optimizations, the design included 407 flip-flops, 6700 gates, and 88 inputs.

Examples of formal properties

The first five rules were written during the first week of the environment bring-up. Notice that the number of flip-flops each property uses is high. It shows that although the basic environment was able to provide only a subset of the block features, it needed many of its flip-flops (see Table 2). Rules 4 and 5 check the MPEG2 display order. Due to the large number of environment variables, this process required a partitioning of the original rule into two parts with each part covering different modeling aspects of the inputs.

Rule 6 is an example of a property that required a large environment definition. Most of the rules used an environment that was capable of running only one bitstream (no end/start commands). This was due to the large number of environment variables associated with this feature. The Rule 6 property needed to use multiple bitstreams environment (an addition of around 15 environment variables). For all rules, notice that the user time values are depended on the particular machine power.

Lessons learned

The formal verification process can be made more effective if the design architecture and its implementation follow a set of guidelines, which fall into three distinct categories:

Reduction: Symbolic model checking addressed the state explosion problem by using BDDs. While several techniques are incorporated in the Rule-Base tool, the size problem still requires you to follow some guidelines. Most of the reduction guidelines focus on design partitioning and modularity, with the goal of isolating the control logic from the data path that can be replaced by abstract models. It was found that these guidelines are very effective from design point of view and design for verifiability.

Documentation: Keeping well-defined and documented interfaces between partitions to ease the development and maintenance of environment models. This is also a good design practice that often leads to better design qualities.

Formal Specification: Translating the informal specification, usually written in natural language, into a set of formal properties. This task often assumes background knowledge and ability to formulate sentences into formal structures.

In addition to the CONTROL block we verified during the evaluation period, we also verified a few other blocks as well. The VIP [5] interface is a protocol-based logic, which had to be compliant with the VIP specification. The closed-caption [6] block is part of the video-out logic (data-path oriented) and applies the closed caption data into the video stream. The work on this block uncovered various architectural problems that would not have been found using other methods.

Our experience indicated that the amount of time required for building a formal environment and associated rules is grew shorter with each project we worked on (see Table 3). We also proved that there are blocks that can be verified only by formal verification, thus saving additional effort to build a simulation environment. These results led us to assimilate formal verification into all our projects as an integral and mandatory part of the verification methodology. It also affected the way we wrote our specifications, applying greater consideration to formality and simplification of rules and logic descriptions.

This verification methodology shares both design verification (pre-silicon verification activities) and validation (post-silicon verification activities). An exhaustive design verification - based on simulations - can provide a cleaner chip but it may also precipitate the loss of a short window of opportunity with which to launch a product to market. Formal verification methods offer not only a larger coverage of the verified properties, but also a better design methodology.

Acknowledgments

The author would like to thank Uzi Zangi from Zoran and Tali Yatzkar-Haham from IBM Haifa, whose cooperation contributed to the work presented here, as well as Yaron Wolfsthal from IBM Haifa, and Aharon Aharon and Ram Ofir from Zoran for supporting this work.

To voice an opinion on this or any other article in Integrated System Design, please e-mail your comments to sdean@cmp.com.