A Comparison of Three Verification Techniques: Directed
                                                                           Testing, Pseudo-Random Testing and Property Checking
           Mike G. Bartley¹                                                                   Darren Galpin    Tim Blackmore
             Elixent Ltd                                                               Infineon Technologies UK Ltd        Infineon Technologies UK Ltd
   Castlemead, Lower Castle Street                                                 Infineon House, Great Western Court Infineon House, Great Western Court
           Bristol BS1 3AG      Hunts Ground Road, Bristol BS34 8HP Hunts Ground RoadBristol BS34 8HP
                                                                                            +44(0)117 952 8741                  +44(0)117 952 8745
      Mikebartleyuk@Yahoo.co.uk                                                         Darren.Galpin@Infineon.com          Tim.Blackmore@Infineon.com

ABSTRACT versions were verified - the first version (LFI-IBC32) required that This paper describes the verification of two versions of a bridge the DUT could work with LMB:FPI clock ratios of 2:1 and 1:1. between two on-chip buses. The verification was performed just The second version (LFI-S) extended the LFI-IBC32 functionality as the Infineon Technologies Design Centre in Bristol was to support any clock frequency ratio so long as the LMB introducing pseudo-random testing (using Specman) and property frequency is equal to or greater than the FPI frequency, and as checking (using GateProp) into their verification flows and thus long as the positive edges of the clock signals align. In addition, provides a good opportunity to compare these two techniques power saving features were incorporated into the LFI-S version. with the existing strategy of directed testing using VHDL bus 2.2 Methodology functional models. Four main techniques were applied to the verification of the LFI: Categories and Subject Descriptors ß Directed testing using VHDL BFM’s for the test bench and B.5.2 [Register-Transfer-Level Implementation]: Design Aids transaction-based tests for directed tests. – Verification. ß Pseudo-random constraint driven testing using Specman from General Terms ß Verisity. Formal property checking using GateProp from Siemens. Verification. ß The LFI was placed within a larger system and verified as

1. INTRODUCTION part of that system. This system is a reference system used

The verification of two versions of a bridge between two on-chip solely for the purpose of verifying system level aspects of a busses is described. The verification methodology incorporated DUT that are hard to verify at module level. For example, the directed testing, pseudo-random testing and property checking at LFI can go into power down mode with other parts of the module level, as well as in-system testing. Only the module-level system when a certain set of conditions apply and the LFI verification is considered in detail. The incorporation of the three then engages in a complex handshake with the CPU and other techniques into a verification flow is described in Section 3. In blocks. The complete operation is better verified at system Section 4, results are used to discuss the relative strengths of each level than at module level. verification technology, as well as the strength of the verification This paper is more concerned with module level verification and provided by all three combined. Since verification is not an exact so will concentrate on the first three techniques. science, rather than trying to draw hard and fast conclusions, Figure 1 indicates when each technique was applied during the recommended use of these technologies is presented based on the project. There follows a brief explanation of why these techniques experience gained in Section 5. Some ideas as to how the three were applied at these times and how they were applied. technologies may more easily be used in conjunction are included. ß When the LFI-IBC32 project started the only infrastructure 2. BACKGROUND available was the VHDL Bus Functional Models (BFM’s). 2.1 The Design-Under-Test (DUT) The LFI is a bus bridge that connects a 32-bit address, 64-bit data Directed local memory bus to a 32-bit address, 32-bit data flexible peripheral bus. The LFI is approximately 30K gates in size. Two Random 1 Mike Bartley was with Infineon Technologies when this work was carried out Formal Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee 7 months 6 months provided that copies are not made or distributed for profit or Time commercial advantage and that copies bear this notice and the full LFI-IBC32 LFI-S citation on the first page. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific Figure 1: Verification time-line permission and/or a fee.

       Hence a directed test bench and directed tests was developed   ß              Two BFM slaves and masters, plus protocol checker and
 first.                                                                     local memory unit on the FPI bus.

ß The directed tests were completed about halfway through Once the directed tests have been written and run on the DUT, LFI-IBC32 but were continually run in regression and were structural coverage is performed using a suitable third party tool enhanced to achieve the structural coverage targets. to provide defined coverage metrics such as Statement Coverage, ß The LFI-IBC32 directed test bench and tests were ported to Branch Coverage and Toggle Coverage. Pre-defined targets of LFI-S and used for regression and structural coverage there 100% justified statement coverage (“justified” as some statements too. are unexecutable, such as some “when others” statements), >95% ß e language Verification Components (eVCs) for the FPI and branch coverage and 100% toggle coverage. These structural LMB became available during the LFI-IBC32 project and coverage targets form a necessary but not a sufficient quality were then used to build a LFI Specman test bench (this target. They are a safety net – whilst your verification has not accounts for starting the random testing later for LFI-IBC32). reached the targets you know you haven’t done enough, but This test bench was then ported to the LFI-S project. reaching the targets does not mean completion of verification. Experience shows that the tests derived from the black box test ß GateProp was a new tool to the Infineon Technologies spec are insufficient to reach these structural coverage targets and Design Centre in Bristol and some training and infrastructure so extra tests are specified and implemented using a “white box” development was required before it could be used (this approach. The white box approach works by looking at the accounts for starting the property checking later for LFI- coverage holes with a designer and specifying specific transaction IBC32). The GateProp environment and properties were sequences that need to be performed in order to hit the previously however very quickly ported to LFI-S. uncovered holes. This results in a set of very targeted tests. . As well as relying on structural coverage metrics, directed testing also aims to demonstrate bus compliance. The bus protocol 3. VERIFICATION TECHNOLOGIES specifies certain scenarios that have to be performed correctly in 3.1 Directed testing order for bus compliance to be achieved. A compliance document Directed testing started with the writing of a test specification with tick boxes is used, and for each sequence the test which document and a test bench description document by a separate demonstrates this is supplied. verification team to give the independent interpretation discussed in Bergeron (2000). The test specification is written using a “black 3.2 Random testing box” approach from the verification engineers understanding of the Random testing was performed using Specman Elite and dedicated DUT spec. The document aims to test fully all of the stated in-house eVC’s (e language verification components – comparable functionality in the DUT spec, and it is from this that the directed to BFM’s). The testbench was constructed using configurable tests are written. The writing of the test spec forms a very good numbers of eVC masters and slaves on both busses, together with review of the DUT spec and can uncover discrepancies or holes in an e-protocol checker on each bus. The system clocks were driven the DUT spec. The test bench spec is aimed at describing the test from the VHDL top level in order to improve simulation bench features such that the tests to be run on it are able to performance, but otherwise all stimuli were generated from the e- exercise all of the design features and to allow for the code itself. implementation of the test specification. The design and verification teams reviewed both specifications. A test specification is again written in advance based on the DUT The directed test bench is built from internally supplied BFM’s, spec - the document describes the scenarios that need to be written in VHDL. These are driven by a simple test language that covered. Similarly a test bench specification is written. Both are allows the test to perform read and write transactions plus idle reviewed with the designers who may suggest additional scenarios. cycles. The test is thus written at the transaction level and the Coverage scenarios fell into two main types for both of the BFM translates the transactions to the appropriate signal DUT’s considered in this paper. behaviour on the bus. The BFM’s allow the DUT to be stimulated 1) Transaction coverage. On a per-master and per-slave basis, across the full range of functionality specified in the bus protocol. the types of transactions applied and received are recorded, Adherence to the protocol by all parties is monitored by a along with associated information such as acknowledge codes, protocol checker - another VHDL module which plugs directly byte lanes used, wait states observed. Cross-coverage of onto the bus. these transaction types is then performed, in order to ensure The directed test bench used consisted of: that for each opcode type we have observed every error ß Four BFM Masters and Slaves, plus a protocol checker on condition, every type of wait state and so on. the LMB bus. 2) FSM transition coverage. We hook Specman to the internal state machines within the DUT itself, and define what the

     legal transitions are. During the course of the testing, we can   sequences of values, in order to find corner cases. Of course,
       measure coverage of every legal transition, and check that we   random testing   also  chooses  inputs from      inside a set      of
did not cause any illegal transitions.                                 constraints. The difference here is that the property checker

The combination of ensuring that we apply every possible cross- ‘intelligently’ tries to find a counter-example, or else prove, a coverage point and FSM transition ensures that we achieve a high property. However since the property checker is potentially functional coverage of the DUT, and any areas that we initially exhaustive, it moves through clock cycles considerably slower miss during random testing are rapidly highlighted in the coverage than directed or random testing. results. The creation of new test scenarios with modified We split properties into two types - ‘bus protocol properties’ transaction constraints can then be added to ensure that we and ‘transaction properties’. Transaction properties drove explicit achieve 100% of the coverage that we have defined. transactions across the bridge, checking that addresses, control Cross-coverage of all opcode types with all byte lanes and all signals and data passed through correctly, and that the bridge errors is impossible, as it can generate impossible to hit responded appropriately to the various acknowledgements from combinations. All impossible combinations and FSM transitions bus slaves. The property checker has the advantages that all legal were removed from the coverage targets, so that a simple check for behaviour around the transaction was allowed, and the address and 100% coverage can be made at sign-off. data were checked symbolically - in effect testing all possible 3.3 Formal values. The slowness of moving through clock cycles was a big limitation however. The transaction properties were sensitive to Formal verification was carried out using the Siemen’s property timing (e.g. the number of clock cycles it took each type of checker, GateProp (see Bormann and Spalinger (2001) for details transaction to pass through the bridge). This made them more time of this tool). The main tasks involved in property checking are consuming to write, with a degree of trial and error being writing and testing constraints and writing and running properties. necessary, and also to maintain since cycle timings were not Earlier property checkers could not easily deal with large designs, specified and so could change with design updates. suffering ‘state space explosion’. One of the ways that GateProp Bus protocol properties checked that the LFI obeyed the overcomes this is not to do any reachable state analysis¹. Hence it protocols of the FPI and LMB. Since the bus protocol properties is the responsibility of the user to ensure that there are no false were checking that certain behaviour always, or never, happened negatives due to internal signals in the design being in an they were not sensitive to timing. This also meant that they could unreachable state. This involves checking each failing property and exercise the design further just by running for longer. Another developing a set of constraints on the internal signals so that they advantage they have is that, like the input constraints, they are re- remain in a suitable superset of all possible reachable states. Both usable on any module with a similar interface (discussed later). of these are very time consuming. Also, the constraints are not The transaction properties and protocol properties each found going to be re-usable on other designs, and in fact may be difficult bugs. Exact numbers are given later in Section 4.2. to maintain across changes in design. It was therefore decided to start all properties from reset, this being the simplest valid state to 3.4 Combining the techniques define. It should be stated that more general approaches have Directed Testing, Random Testing and Formal Verification are not successfully been applied in other industrial applications of completely orthogonal techniques. During both the LFI projects GateProp, where a very high functional coverage has been the random test bench was used to seed both property checking achieved. In most of these projects the always-start-from-reset and directed testing. approach would not have touched the most interesting When a failure occurs in directed or random testing, a specific set functionality, e.g. in telecommunication systems where you have of circumstances have caused the observed failure, and it may be frame lengths of thousands of cycles with corresponding serial possible that there are other similar signal combinations which synchronisation protocols. Admittedly, these approaches make expose the same or similar errors. Thus when the bug is “fixed” limited use of some internal states, yet important ones only which and the test re-run, the bug may no longer be observed, but a make sense at an abstract level. They allow at least a certain degree similar or new bug may still be present in the code but it is of reusability of properties. reachable only via another set of input stimuli. Consequently it is Given our always-start-from-reset approach, to ensure that the useful to test a wider set of signal inputs using property checking. design did not reach an invalid state it was only necessary to If the bug failure is carefully observed, a set of properties can be constrain the inputs to model the DUT’s environment. The goal deduced which must be satisfied for the bug to occur, and thus we here is to allow the inputs to take any legal combinations and can write a property to prove that the bug cannot possibly occur. In this way we can prove that the bug has been fixed over all 1 Note that versions of GateProp subsequent to that used on the circumstances, rather than the one circumstance observed in the LFI include approximation of the reachable state space and directed or random test. However, not all directed test bench analysis of unreachable counter-traces.

failures may be able to be analysed in the manner needed, so we curve shape, as the number of bugs found rapidly increases as the may not be able to prove all bugs in all cases. verification effort is increased, and gradually reduces as the DUT Thus, many failing tests were converted to properties. These reaches maturity. Thus if the levelling out in the curve is not seen, properties were used to check the fix and often found new bugs or it can be an indication that more time is needed to debug the that the fix had introduced a new bug. This raises the question as design. to why such properties were not specified initially. The reason for Overall Cumulative Bug Find Rate this is that the set of all possible properties is too large – so using 120 this approach helps to prioritise the properties to be written and LMB Testbench run. 100 FPI Testbench In addition, a random test may exercise a piece of code that has LFI-S not been exercised by directed testing before, and it may prove to 80 LFI_S TB be a particularly problematic piece of code. The random test gives the verification engineer a set of input conditions which need to be 60 applied to the DUT in order to reach that piece of code, so these can then be applied via the directed test bench to explore the 40 behaviour of this previously untested code. This can free up the random test bench resource to explore and verify other areas of the 20 DUT while the directed test bench is used to fix the bugs that 0 cause the random test bench to fail every time it enters this area.

4.  RESULTS                                                                                       Date
   

4.1 Coverage Figure 2 – LFI-S Bug Curves The coverage achieved from the three approaches enabled us to Figure 2 shows the bug curve seen during the LFI-S project. It release a DUT with a high degree of confidence in its design. Our clearly shows the progression of the project through its life cycle. directed testbench achieved the following structural coverage At the beginning of the project the test bench is constructed and metrics: debugged, then testing of the DUT begins and the bug curve • 100% Justified Statement Coverage rapidly moves upwards. Bugs are found in all parts of the design, and as new parts of the DUT functionality are tested, new areas • 98.4% Branch Coverage of the verification IP are also tested, resulting in more test bench • 95.2% Condition Coverage bugs. Eventually the test bench reaches maturity, and the DUT • 84.2% Trigger Coverage reaches maturity shortly afterwards. The cumulative total flattening out completely for a sufficient time can thus be used as • 100% Toggle Coverage a sign-off criteria, as it suggests that maturity has been reached. The random testing achieved 100% FSM transition coverage, but 4.2.2 What technique found what bug did not attain 100% cross-coverage of the FSM’s. This proved to Table 1 gives a breakdown of bugs found in the LFI-S by type, be impossible because of the design of the DUT. The bus and by the method used to find them. transaction coverage targets were met (the target was 100% after removal of impossible transactions as discussed earlier). Coverage for Property Checking is far harder to measure as Bug Type Prop.Chk Direct. Rnd. GateProp has no coverage metric. A review of the properties by Bus Protocol violations 11 4 8 the verification team established that we were convinced that all the practical transactions and all protocol issues had been covered. Internal DUTqueue 0 2 4 Indeed it is possible to establish full protocol compliance via deallocation issues review of the properties, or better still mathematically (see Barrett Livelock/Deadlock 0 5 2 and McIsaac (1997)). Other DUT issues 7 3 8 4.2 Bug Analysis Total 18 14 22 4.2.1 Bug Graph Table 1 : Breakdown of LFI-S bugs Bugs were recorded using an issue tracking system that allowed When reading these figures the reader is reminded that the various statistics to be gathered such as the cumulative number of bugs verification techniques were started at different times in the found, the number fixed, and whether they occurred in the design project. As stated at the start of the paper, for the LFI-S project or test bench. Bug find rates are often expected to follow an S-

16/05/2001 Number of Bugs 23/05/2001 30/05/2001 06/06/2001 13/06/2001 20/06/2001 27/06/2001 04/07/2001 11/07/2001 18/07/2001 25/07/2001 01/08/2001 08/08/2001 15/08/2001 22/08/2001 29/08/2001 05/09/2001 12/09/2001

the directed tests from LFI-IBC32 were used to prove initial 4.3 Combined Effectiveness functionality, and once basic functionality of the DUT had been Both the LFI-IBC32 and LFI-S have now been manufactured in demonstrated, random testing was started. However, property silicon as part of larger SOC’s and no bugs have reported against checking was started almost immediately, although time was either. required to modify the transaction properties due to changes in internal DUT timing. 5. RECOMMENDATIONS AND FUTURE In theory all of the bugs found by random testing could be found USE by directed testing. Random testing generates large sequences of 5.1 Directed testing vs. random testing transactions that can easily be replicated in the directed test bench. However, in practise there is not enough resource (to generate The combination of approaches improved the quality of the such large numbers of self-checking sequences) or ingenuity (to verification, but also increased the resources applied, especially as think of the corner cases that random generation creates). two test benches were built and maintained. One future course of Similarly, most of the bugs found by random testing could have action will be to become less reliant on directed testing (and thus been found using property checking given the resource to write an more reliant on random testing and functional coverage) and to use extensive set of properties (less ingenuity is required because the random test bench to perform the directed testing. However, property checking probes corner cases automatically). However, this does result in compromise, as it requires the verification some bugs did require a number of cycles to cause the failure (e.g. engineer to heavily constrain the random testbench and results in a those caused by filling up internal queues and then trying to add loss of controllability compared to a pure directed testbench. This further transactions). The number of simulated cycles needed to raises the question of whether to start with unconstrained random get to this point can result in an excessively long run time for tests and constrain them to more directed tests over the project or properties. For the same reason, property checking is unlikely to vice-versa (Verisity recommend the former). find the livelock or deadlock bugs, although if we create a livelock Also, without a large set of directed tests, a repeatable regression or deadlock by initial conditions we can prove that we cannot run of tests which can demonstrate DUT functionality becomes escape. more problematic. Although the use of seeds in Specman allows Property checking was most effective at demonstrating that the repeatability, we require a list of seeds per scenario in order to DUT does not violate bus protocols. Many of the violations guarantee full coverage. This also requires that the eVC’s used are would require a directed test to be written with a knowledge of stable, and that the same version of Specman is also used each what is happening cycle by cycle on the bus, and are generally time the regression is run. If this requirement is not met, then the found more by luck than judgement during random testing and repeatability of the regression run cannot be guaranteed. than during directed testing. Finally, the structural coverage targets still need to be met and this Thus, during the two LFI projects, the verification strategies requires Specman to be run with an appropriate structural proved to be complementary – all stressed different areas of the coverage tool. DUT in different ways, and speeded the finding of bugs. They 5.2 Productisation of verification IP also allowed the verification manager to have several quantitative If users are to gain the benefits of verification IP reuse, then the and qualitative measures on which to assess confidence in the productisation of the verification IP itself is very important. quality of the DUT. Indeed, the following were all used in the The random test bench elements have been developed into re- sign-off criteria: usable IP (using the eVC approach recommended by Verisity). ß directed and random test bench and test specifications Indeed, these have been re-used successfully on a number of other reviewed and signed off by design and verification teams; projects with big reductions in test bench construction times ß structural and functional coverage targets met; Some of the property checking deliverables have also been turned ß all directed tests passing; into re-usable verification IP. As already noted the property ß a certain number of random transactions run successfully checking effort can be divided between the writing of constraints since last bug found; and the writing of properties. Each of these can be further divided. Constraints can be internal, i.e. constraining the internal signals of ß property specification reviewed and signed off by design and the design to avoid unreachable states, or external i.e. constraining verification teams; the inputs to the design to reflect its environment. We’ve already ß all properties passing; divided the properties into bus protocol and transaction ß bug curve flattened off and no bugs found for a given period properties. of time. Clearly the internal constraints are not going to be re-usable, and may in fact be difficult to maintain across changes in a design during development. This was a major factor in our decision not to

develop such constraints (and rely on reset to ensure properties ß The random test bench and property checking both use used valid internal states). However the external constraints can be constraints to first define the legal sequences of inputs and re-used, with appropriate modifications to signal names, on other then to further restrict them to a smaller set of sequences of modules that have a similar interface. The most commonly used interest to test or property in question. interfaces are the busses, so constraints modeling busses give the ß Properties should also hold during simulation. largest opportunity for re-use. ß Dynamic verification can get the design into legal internal Similarly the transaction properties will not be re-usable and may states from where it would be useful to start a property take some effort to maintain, due to small changes in timing. check (as opposed to always starting it from reset). However the bus protocol properties are easily re-usable. A little care should be taken to monitor run times to ensure that the design Fortunately, all three of these areas are being addressed in various is really being exercised, since some designs may have a ramp up ways. Accellera (www.accellera.org) are trying to define an time after reset where they do little and so are unlikely to break industry standard formal language that can be used in both formal any protocols. and dynamic verification. This should allow the first two to be So it is the constraints on, and properties for, bus protocols that realised. There are also tools appearing that enable the third (so- are re-usable. Indeed those developed for the LFI have been used called semi-formal tools), such as 0-In Search. on other modules that interface with the FPI and LMB busses, 6. REFERENCES namely a peripheral control processor and an external bus unit. [1] Bergeron, J. Writing Testbenches; functional verification of This experience of re-use will be used to develop bus protocol HDL models (2000), Kluwer Academic Publishers packages for these busses, using a simple wrapper to standardise signal names. These packages will be easy to use for someone with [2] Bormann, J. and Spalinger, C. (2001) Formale Verifikation no experience of property checking. Of course such packages are fuer Nicht-Formalisten (Formal Verification for Non- applicable to any standardised protocol and there are also plans to Formalists), Informationstechnik und Technische Informatik, develop them for other busses, such as the AHB. volume 43, issue 1/2001, Oldenbourg Verlag 5.3 Easier re-use between dynamic and static [3] Barrett, G. and McIsaac, A. (1997) Model Checking in a verification MicroProcessor Design Project9ₜₕ , CAV'97 (Proceedings of the International Conference on Computer-Aided Verification, During the LFI projects a set of constraints and properties were Haifa, Israel 1997, Orna Grumberg (Ed.), Springer Lecture developed and maintained. There is much scope for re-use from Notes in Computer Science 1254) random/directed testing to property checking and vice-versa. For example: