Effective Modeling Techniques for Formal Verification of Interrupt Controllers

Please download to get full document.

View again

of 4
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Document Description
Effective Modeling Techniques for Formal Verification of Interrupt Controllers
Document Share
Document Tags
Document Transcript
  Effective Modeling Techniques for Formal Verification of Interrupt Controllers Saptarshi Biswas, Dharmendra Soni, Varun K Mohandru, Praveen Tiwari, Raj S MitraWDC, SDTC, Texas Instruments (India) Pvt. Ltd.   Abstract  Formal verification is easy to use and provides significant increases in productivity and quality when used on RTLdesigns, which fit formal verification tool capacity. However, formal verification can be challenging whenused on designs that exceed the capacity of the tools. This paper describes various techniques that were used toovercome these challenges during the verification of areal-life complex interrupt-controller using Cadence’s Incisive Formal Verifier. These techniques include divide-and-conquer to scale down the design, smart modeling of constraints, lightweight simulation, and use of advanced tool features. The collection of these techniques enabled the full verification of the interrupt-controller and saved many man-months of effort. The paper presents our resultsand concludes with pointers to areas of further improvement, currently under investigation. Keywords Formal Verification, Incisive Formal Verifier, Modelchecking, Interrupt Controller, Modeling Techniques 1.   Introduction Formal Verification is a proven technology, which whenused on RTL validation, results in significantimprovements in chip-design cycle-time. FormalVerification in the field of RTL validation is mostly ModelChecking as of today. Model checking is now being usedextensively in control logic validation e.g. protocolcompliance, arbitration, FSM etc.However, with increasing design complexity, we encounter state-explosion problems in Formal Verification. As aresult, FV becomes challenging when used on complexdesigns that exceed the capacity of the tool. Quite ofteneven fast machines with high memory resources are notadequate enough to overcome this limitation. Hence,effective modeling techniques become imperative to enableFV on these complex designs. Needless to mention, suchextra verification setup modeling necessitates easy-to-usetool-support and state-of-the-art tool engineering.This paper considers a real-world Interrupt Controller design as a case study, whose behavior has been captured by Property Specification Language (PSL) properties andrun on Incisive Formal Verifier tool (Cadence). First, anaïve verification setup is outlined and it is explained whysuch a modeling leads to capacity-limitation issues, andtherefore, is not sufficient to produce conclusive results.The paper then proceeds to show how intelligenttechniques like black-boxing and divide and conquer wereapplied to overcome this capacity issue. The resultsdemonstrate that these techniques have not only made FVa possibility on the Interrupt Controller design, but also brought about a 6X improvement in tool runtime. At theend of the exercise, Incisive Formal Verifier was able tocatch a logical bug in the sorting function and with therenewed RTL it was able to prove it fault-free.Section 2 describes the structure and functionality of theDUV i.e. the Interrupt Controller design. In Section 3, wedetail a naïve Formal Verification setup modeling of thisDUV and explain its shortcomings. Black-boxing andDivide-and-Conquer techniques have been introduced inSection 4. Finally, Section 5 concludes with results. 2.   Interrupt Controller: The DUV This section first explains the functionality of a genericInterrupt Controller from a system perspective, followed bya block-level description of the same. We then take up theInterrupt Controller case study and describe its internalworking for a better understanding of the module. 2.1.   The System Perspective The Interrupt Controller is closely coupled to the processor. From the point of view of the system, this programmable controller module takes interrupts fromother modules/peripheral, sorts them and provides thewinner to the processor. The processor then executesInterrupt Service Routine of the winner. After completionof ISR, the Processor de-asserts the winner at the input of the Interrupt controller.  2.2.   Block-level Description The Interrupt Controller (shown in Figure 1) that wastaken up as a case study has the following interfacingsignals:- Inputs •   Interrupt signals: A configurable number (32, 64, 96or 128) number of interrupt lines. •   OCP slave interface: An OCP 2.0 compliant bus towrite to the configuration registers. Outputs •   The winner: This is the address of the interrupt withthe highest priority among all active interrupts. Figure 1: Block diagram of Interrupt Controller 2.3.   Functionality The sorting engine is essentially an FSM. The number of clock cycles required by this FSM for a sorting depends onthe number of interrupts configured (32/64/96) i.e. 8 cyclesfor 32 interrupts and 9 cycles for 64/96 interruptsconfiguration. The sorter FSM starts execution when anyof the input interrupts gets asserted.Internally, the sorting is executed in bunches of four at atime. After each clock, the temporary winner is stored in aregister and used in the next cycle for comparing it againstthe next bunch of four interrupts. Figure 2 shows thesorting logic. Figure 2: Sorting Logic A timing diagram (shown in Figure 3) shows the normaloperation of the Interrupt Controller. When the “ActiveUnmasked Interrupt” line gets asserted, an internal sortingcounter starts counting up from 0. The sorter (refer Figure2) is enabled for each cycle till the counter reaches 7 (for 32 interrupts). Figure 3: Timing diagram of a sorting function 3.   Verification Setup Figure 4 shows the naïve verification setup of the aboveDUV. We are interested in black-box verification of thismodule; hence internal signal accesses have been avoidedunder this setup 3.1.   The Verification Plan The steps in the verification approach are1.   OCP protocol compliance2.   Sorting Logic Verification 3.1.1.   OCP protocol compliance OCP 2.0 protocol compliance verification is easy to set up.In this case, since the DUV OCP is a slave interface, allformal properties asserting the behavior of the master  Counter start (0)i.e. Sorting startsCounter ends (7)i.e. Sorting endsRandom Input InterruptActive Unmasked Interrupt line5:1 Sorter (Combinational)Previous winner MUX4444   FSMSeuentialEnd of SortingStart of Sorting    W   i  n  n  e  r ConfigurationRegister BankOCP WriteInterface INTERRUPTS  (With configuredpriorities)MASK Layer SORTING ENGINE   Status Register WINNER   Interrupt Controller (DUV)Slave  driven signals are assumptions; hence these are constraintsto the design. Similarly, all properties related to the slavedriven signals should be verified; hence these are modeledas assertions. Figure 4: Verification Setup 3.1.2.   Sorting Logic Verification For verifying the sorting logic, the following system-levelresponsibilities had to be modeled as constraints •   The configuration registers should not change their values during sorting à OCP write is disabled justafter sorting starts. •   Sorting results are generated after 8 cycles (for 32interrupts). Hence all the interrupts should not changefor these many clock cycles, once the sorting hasstarted. This can be modeled by appropriate stabilityconstraints along with a counter.With the above constraints modeled, the properties thatneed to be validated are •   The actual winner at the end of the sorting is theexpected winner  à the expected winner can becalculated using a function and compared against theactual winner. 3.2.   Demerits of this Verification Setup Tool runtime is heavily dependent on the cone of influenceof the property under consideration. In the verificationsetup explained above, the property that checks the sortinglogic compares the winner (output) against the interrupts(input). At the same time, the OCP interface (input) isconstrained. Thus this property contains the entire moduleend-to-end under its cone of influence. It is shown in theResults’ section (Section 5) that when this property wastried to be run on IFV, it resulted in Explored Depth (ED)after 30 hours of tool run.This suggests that the above naïve modeling is notsufficient and further improvements are required. 4.   Enabling Techniques for FV This section outlines a couple of techniques that have beenapplied to obtain significant improvement in theverification time. 4.1.   Black-boxing Black-boxing of a module is a means by which the internallogic of the module is black-boxed or removed. If asubmodule of a design is black-boxed, then the outputs of that submodule are no longer driven and can be treated as primary inputs to the top-level design.Figure 5 demonstrates the setup modification to removeirrelevant logic from the cone of influence of the property. •   The configurations register banks which are programmed through OCP Write interface are black- boxed.In IFV, black-boxing is easy. The list of modules to be black-boxed is passed on to the command line at thetime of tool-invocation. ifv -f <config.f> bb_list+<bbox_file>   •   To ensure that the configuration registers do not alter their values during the sorting process, extra stabilityconstraints are added. // psl stability_cnstrnt : assert always( sig == prev(sig) ) @ (posedge clk) ;  Thus the entire register bank along with protocolconstraints has been replaced by a single stabilityconstraint. Figure 5: Logic cone reduction using Black-box feature inIFV Sorter    C  o  n   f   i  g   R  e  g Black-box tillthis pointProtocolconstraintSorterStabilityConstraintReplaceregisters withstabilityconstraints:Leads toconsiderablelogic-coneshrinkage   InterruptController(DUV)OCP MasterConstraintsStabilityConstraints    O   C   P   I   /   F   I  n   t  e  r  r  u  p   t  s   W   i  n  n  e  r OCP SlaveAssertionsSorting Assertions  As shown in the Results’ section, this technique hasenabled the sorting property get around the ED issue. Onthe same machine, IFV showed a failure after a toolruntime of 18 hours. 4.2.   Divide and Conquer Divide and Conquer is a powerful reasoning by which acomplex problem is broken down and each of these sub- problems are tackled separately. The motivation behindthis Divide and Conquer paradigm is that the collectiveeffort in tackling all the sub-problems might beconsiderably less than that of tackling the entire problemat one go. However, applying Divide and Conquer is notstraightforward, and needs to be backed up by proper  justification so that we do not lose any functionality in the process. This section details how Divide and Conquer approach has been applied on Interrupt Controller toobtain improvement in tool run-time.The input interrupts are grouped in bunches or classes of four. So for a 32-interrupt configuration there will be 8classes, with 4 interrupts in each class. The next step is toverify that •   Interrupts within the same class (intra-class) •   Interrupts across different classes (inter-class)are getting correctly sorted in the RTL.The motivation behind such a division is derived from thestructure of the sorting logic (refer Figure 2). Intra-classchecks validate the combinational 5:1 sorter, while inter-class checks ensure correctness of the sequential carry-over logic. We argue that if there is any anomaly in the sortingfunction, it will show up in any one of these checks.Intra-class checks can be executed by tying all inputinterrupts to inactive value except those belonging to the particular class under consideration. constraint –add –pin <pin_name> = <value> On the other hand, inter-class properties can be validated by making all inputs in each class equivalent to each other.These modifications can be effected by using just singleline commands in the IFV scripting interface. // psl pin_equiv : assume always(pin1==pin2==pin3==pin4) @ (posedge clk); It was observed that these inter-class as well as intra-classchecks collectively took 3 hours of IFV tool run as against18 hours with the undivided setup, and brought the same bug caught earlier in a much lesser time. 5.   Results The following tool run-time statistics have been generatedwith IFV (engine1, halo off, vacuity on) on a 3 GHzPentium machine with 4 GB of RAM running on 64-bitRed-hat Enterprise Edition Linux OS. Table 1 shows theresults obtained with an old version of Interrupt Controller RTL, which shows detection of a bug at a depth of 110clock cranks. SetupResult(depth)IFVrun-time  Naïve setup Explored depth 30 hoursAfter black-box Fail (110) 18 hoursDivide n Conquer Fail (110) 3 hours Table 1: IFV results with old RTL This bug was fixed in the RTL and the same sets of  properties were run with the new version of the RTL.Table 2 shows IFV runtime results of these tool runs. Thedesign was proved clean. SetupResult(depth)IFVrun-time  Naïve setup Explored depth 30 hoursAfter black-box Pass 22 hoursDivide n Conquer Pass 6 hours Table 2: IFV results with new RTL References [1] “Open Core Protocol” version 2.0 specifications:http://www.ocpip.org [2] Incisive Formal Verifier :http://www.cadence.com [3] H Foster, A Krolnik, and D Lacey. “Assertion-basedDesign”. Kluwer Academic, 2003.[4] A. Roychoudhury, T. Mitra, S.R. Karri, “Using formaltechniques to debug the AMBA System-on-Chip BusProtocol”, in Proc. DATE, pp. 828-833, 2003[5] K. Shimuzu, D. Dill, and A. Hu. “Monitor-based formalspecification of PCI”, FMCAD 2000, Austin, Texas[6] “Property Specification Language”.http://www.openverificationlib.org[7] Kanna Shimizu. "Writing, Verifying, and Exploiting FormalSpecifications for Hardware Designs", Ph.D. Thesis,Department of Electrical Engineering, Stanford University,August 2002.
Similar documents
View more...
Search Related
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks