Contents | Zoom in | Zoom out For navigation instructions please click here Search Issue | Next Page __________________ Contents | Zoom in | Zoom out For navigation instructions please click here Search Issue | Next Page PreviousPage | Contents | Zoomin | Zoomout | FrontCover | SearchIssue | NextPage ABEFMaGS ___________________________________ PreviousPage | Contents | Zoomin | Zoomout | FrontCover | SearchIssue | NextPage ABEFMaGS PreviousPage | Contents | Zoomin | Zoomout | FrontCover | SearchIssue | NextPage ABEFMaGS Call for Papers Special Issue on Design and Test of RFIC Chips Guest Editors: Bruce Kim and Craig Force Thewirelesselectronicsmarkethasbeengrowing & MEMS for RFIC design and test rapidly in conjunction with computer, automotive, & Automotive RFIC applications biomedical,andmilitaryapplications.RFintegrated- & Reliability issues circuit (IC) chips in these areas require greater & Tutorials density,higherspeed,lowerpower,lowercost,and better reliability. However, designing and testing Submission and review procedures RFIC chips is becoming increasingly more compli- Prospective authors should follow the submis- cated and challenging. In fact, the process of sion guidelines for IEEE Design & Test. All manu- integratingRFICsintoSoCsandsystemsinpackage scripts must be submitted electronically to the (SiPs) has caused a major bottleneck in the IEEE Manuscript Central Web site at https://mc. _______ production of high-performance systems. Although manuscriptcentral.com/cs-ieee. Indicate that you considerable research is underway to reduce the are submitting your article to the special issue on design and test overhead for RFIC chips, this ‘‘Design and Test of RFIC Chips.’’ All articles will bottleneck remains the major obstacle to efficient undergo the standard IEEE Design & Test review RFIC chip product manufacturing. Therefore, the process.Submittedmanuscriptsmustnothavebeen mostcriticalchallengeincreatingRFICstodayisto previously published or currently submitted for developinnovationsindesignandtestmethods. publicationelsewhere.Manuscriptsmustnotexceed IEEEDesign&Testseeksoriginalmanuscriptsfor 5,000 words, including figures (with each average- aspecialissueonthedesignandtestofRFICchips, size figure counting as 150 words) and including scheduledforpublicationinJanuary-February2008. amaximumof12References(50forsurveys).This We invite submissions of unpublished, original amounts to about 4,200 words of text and five articles that showcase the state of the art in this figures. Accepted articles will be edited for clarity, area for system integration in computers, wireless structure, conciseness, grammar, passive to active communication,andautomobiles.Topicsofinterest voice, logical organization, readability, and adher- include,butarenotlimitedto,thefollowingareas: encetostyle.PleaseseeIEEED&TAuthorResources & Semiconductor device technology (silicon, at http://www.computer.org/dt/author.htm, then gallium arsenide, CMOS, and so on) scroll down and click on Author Center for sub- & Small-andlarge-signalcircuits(suchaslow-noise missionguidelinesandrequirements. amplifiers, mixers, and filters) or frequency generation circuits (such as voltage-controlled Schedule oscillators,phase-lockedloops,andsynthesizers) & Submission deadline: 1 August 2007 & Packaging,characterization,andICtechnologies & Reviews completed: 15 September 2007 & RFIC modeling and CAD (RFIC simulation & Notification of final acceptance: 1 October tools, device and behavioral modeling, and 2007 design methodologies) & Submission of final version: 19 October 2007 & Communication interfaces and integrated smart antennas in RFICs & DesignandtestofRFreceiverandtransmitterICs Questions & BIST and embedded testing with RFICs Pleasedirectquestionsregardingthisspecialissue & Wireless-system architectures (Bluetooth, toGues tEditorsBruceKim,bruc_e_.k_im_@__ie_e_e._o_rg_;__ RFID, GPS, IEEE 802.1x, and so on) andCraigForce,_fo_rc_e_@_t_i.c_o_m_. PreviousPage | Contents | Zoomin | Zoomout | FrontCover | SearchIssue | NextPage ABEFMaGS PreviousPage | Contents | Zoomin | Zoomout | FrontCover | SearchIssue | NextPage ABEFMaGS March–April 2007 Volume 24 Number 2 http://www.computer.org/dt Special-Issue Features 154 Hybrid Approach to 110 Guest Editors’ Faster Functional Verifi cation with Full Introduction: Visibility Attacking Functional Chin-Lung Chuang, Verifi cation through Hybrid Wei-Hsiang Cheng, Dong-Jung Lu, Copublished by the Techniques and Chien-Nan Jimmy Liu Jayanta Bhadra, Magdy S. Abadir, IEEE Computer Society and Li-C. Wang Other Features and the IEEE Circuits and Systems Society 164 Economic Aspects of 112 AS urvey of Hybrid Memory Built-in Techniques for Self-Repair Functional Verifi cation Rei-Fu Huang, Chao-Hsun Chen, and Jayanta Bhadra, Magdy S. Abadir, Cheng-Wen Wu Li-C. Wang, and Sandip Ray Roundtable 124 Hybrid Verifi cation of 174 Envisioning the Future for Protocol Bridges Multiprocessor SoC Praveen Tiwari and Raj S. Mitra Ahmed Amine Jerraya (moderator), Olivier Franza, Markus Levy, 132 Combining Theorem Masao Nakaya, Pierre Paulin, Proving with Model Ulrich Ramacher, Deepu Talla, and Checking through Predicate Wayne Wolf Abstraction Perspectives Sandip Ray and Rob Sumners 184 FSA SiP Market and 140 Hybrid, Incremental Patent Analysis Report Assertion-Based FSA SiP subcommittee Verifi cation for TLM Design Flows 193 On the Cusp of a Nicola Bombieri, Franco Fummi, Validation Wall Graziano Pravadelli, and Priyadarsan Patra Andrea Fedeli ISSN 0740-7475 PreviousPage | Contents | Zoomin | Zoomout | FrontCover | SearchIssue | NextPage ABEFMaGS PreviousPage | Contents | Zoomin | Zoomout | FrontCover | SearchIssue | NextPage ABEFMaGS Cover design by Alexander Torres Departments 108 From the EIC 197 TTTC Newsletter 198 Book Reviews 200 CEDA Currents 202 Conference Reports 204 Panel Summaries 207 DATC Newsletter 208 The Last Byte PreviousPage | Contents | Zoomin | Zoomout | FrontCover | SearchIssue | NextPage ABEFMaGS PreviousPage | Contents | Zoomin | Zoomout | FrontCover | SearchIssue | NextPage ABEFMaGS Cocktail approach to functional verification & FUNCTIONAL VERIFICATIONREMAINS a major bot- subcommitteerecentlyconductedthisSiPmarketand tleneck of the design process. Despite tremendous patentanalysis study and released its findings to FSA advances in both formal and simulation-based member companies. We thank FSA for sharing this approaches, functional-verification technology still informationwithourreaders. cannotkeep pace with the rapid increases that have Second,Intel’sPriyadarsanPatradiscussessomeof taken place in design complexity. The number of the challenges and new requirements for effective presilicon logic bugs has consistently increased for validation of future system chips. Our industry is eachnewdesigngeneration.Onelogicalapproachto reaching the point at which a worst-case design combating this verification bottleneck is to combine approach is way too conservative, and a better-than- multiple, complementary techniques so that their worst-casedesignisgraduallybecominganecessityto combined strength is superior to the sum of the further reduce the chip’s power consumption and individualtechniques.Inthisissue,weexaminerecent increase its clock rate. Such a shift in underlying progress in this direction. Our guest editors—Jayanta design principles poses new validation and test Bhadra,MagdyAbadir,andLi-C.Wang(incollabora- challenges: A system could malfunction even in the tionwiththeircolleague,SandipRay)—havecontrib- absence of any bug or defect. Some sort of error uted a comprehensive survey article on this subject resilience needs to be considered and designed into and have selected four additional articles that thesystemsothatitcantoleratesuchfailures,caused demonstrate different ways to use this cocktail bycornerconditions. approach to achieve higher verification coverage Finally, there is an interesting roundtable on andlowercomputationaltime. multiprocessor SoC design. Organized by Bill Joyner In addition to these special-issue articles, you will (our roundtables editor) and moderated by Ahmed also find an article on memory built-in self-repair Jerrayaatthe6thInternationalForumonApplication- (BISR).Thisarticledescribesacostandbenefitmodel Specific Multi-Processor SoC (MPSoC 06), this round- for evaluating the economic effectiveness of various tablesummarizessevenpanelists’viewsonthecurrent memoryBISRschemesandimplementations. state of multiprocessor SoC technology and new This issue of D&T also features two interesting opportunitiesinthisarea. contributions to our Perspectives department. First, I hope you enjoy this issue! If you have any thereisanextendedsummaryofareportonsystem-in- feedback,pleaseshareitwithus. package (SiP) technology written by FSA’s SiP sub- committee.ThisreporthighlightsSiP’suniquevaluein bringing together several IC, package, assembly, and test technologiesto createhighly integrated products with optimized cost, size, and performance. FSA formed the SiP subcommittee in 2004 to investigate Tim Cheng SiPtechnologyissuesandchallengesandtostudyits Editor in Chief main applications and business opportunities. The IEEE Design & Test 108 0740-7475/07/$25.00G2007IEEE CopublishedbytheIEEECSandtheIEEECASS IEEEDesign&TestofComputers PreviousPage | Contents | Zoomin | Zoomout | FrontCover | SearchIssue | NextPage ABEFMaGS PreviousPage | Contents | Zoomin | Zoomout | FrontCover | SearchIssue | NextPage ABEFMaGS TECHNICALAREAS ____ DEPARTMENTS__________ ManagingEditor EditorinChief AnalogandMixed-Signal BookReviews:ScottDavidson, ThomasCentrella TimCheng Test:MichelRenovell,LIRMM; SunMicrosystems, _tc_en_t_re_lla_@_in_b_ox_.c_o_m Univ.ofCalifornia,SantaBarbara _re_n_ov_e_ll@_l_irm_m__.fr _sc_o_tt._da_v_id_so_n_@_su_n_.c_om_; GroupManagingEditor _tim__ch_e_ng_@_e_ce_.u_c_sb_.e_d_u CAE/CAD:DwightHill,Synopsys; GrantMartin,Tensilica, RobinBaldwin EditorinChiefEmeritus _h_ill_@_sy_n_op_s_ys_.c_om_ _gm_a_rt_in_@_ie_e_e._or_g;andSachin IEEEComputerSociety RajeshK.Gupta Sapatnekar,Univ.ofMinnesota, 10662LosVaquerosCircle Univ.ofCalifornia,SanDiego CKuorndfaighui,rUanbilveeCrsoitymopfuCtianligfo:rFnaiad,i _sa_c_hi_n@_e_c_e._um__n._ed_u LPohsonAela:m+1ito7s1,4C8A21908732800-1314 _gu_p_ta_@_c_s.u_c_sd_.e_d_u Irvine;_ku_r_da_h_i@_e_ce_.u_c_i.e_d_u CEDACurrents:RajeshK.Gupta, Fax:+17148214010 EditorinChiefEmeritus DanedepA-Snualbymsiisc:roSannIiCNDasessifi,gInBM; _Ugu_npi_vtae_@rs_ict_sy.u_ocf_sCd_a.e_lidf_ournia,SanDiego; S_trba_af_lfd_wEi_dni_@to_cor_m_p_ut_er_.o_rg _Yzoe_rriv_aan_n@t_vZ_iora_riga_enl_o,gV_iic_r.ac_goe_mLogic _n_as_si_f@_u_s._ib_m_.c_o_m ConferenceReportsand RitaScanlan AssociateEIC DefectandFaultTolerance: PZoarniaenl,SVuimragmeaLroiegsic:;Yervant SocietyPublications MFraegedscyaAlebSaedmiriconductor Mim_Ri_ioccChh_aaT_eeell_c.nNh_iincc_ooo_lllaoa_igiddi_ieisss@_,;i_ro_c_te_ch_.c_o_m __zDjoo__Aerpi__TadCn__a@m__Nvo__eirrwa__egs@__elael__oottg__le.icc__ro:.c__mJoo_meDamore; C_Adotl_o-kmer_dan_@iian_cWao_mti_nops_ruto_ten_r.o_rg C_mJSo_.naP_bGu_a.bd_Rilri_o@ck_fanr_eetei_(oscc_nha_salei_r.Bc)_oom_ard Defect-BasedTest:AditSingh, International: ContributingEditors MikeR.Blaha AuburnUniversity, SohaHassoun,TuftsUniversity, CherylBaltes DorisL.Carver _ad_s_in_gh_@_e_ng_.a_u_bu_r_n._ed_u _so_h_a@_c_s_.tu_ft_s.e_d_u BobCarlson MarkJ.Christensen DYDPiiieremaslediitgur,inssa;dnGf_godii_zrzoYoM_ppie_ao@lnud_uluon_Afsiap_,nciUa_.tgulnyr_irsvineisrgs:,ityof _TSsPcuh_eonre_tstM.Lp_daiea_cscvr_tiotdis_vBsyeoy_ssntte_e:@m:_RssSua_;cjne_o.sct_hto_DmKa.vGiduspotna,, NALJoonoauneniliseeDTLaeOuye’lblDoeironynskayld DRFPrhoaaibvnllieikdprtESAE....FELFebairelrpmraltnaantnete DesignReuse:GrantMartin, UniversityofCalifornia,SanDiego, CoverDesign DonF.Shafer Tensilica;_gm__ar_tin_@_ie_e_e._o_rg _gu_p_ta_@_cs_.u_cs_d_.e_du; AlexTorres LStienvdeanI.LS.hTaafneirmoto DesignValidationand AlbertoSangiovanni-Vincentelli, Publisher WenpingWang Debugging:MichaelHsiao, UniversityofCalifornia,Berkeley, AngelaBurgess VirginiaPolytechnicandState _al_be_rt_o_@_ee_c_s.b_e_rk_e_ley_.e_d_u;and _ab_u_rg_es_s@_c_o_m_p_ut_er_.o_rg CSMagazineOperations University;_m_h_sia_o_@_v_t.e_d_u YervantZorian,VirageLogic, AssociatePublisher Committee DesignVerificationand _zo_ri_an_@_v_ira_g_el_og_ic_.c_o_m DickPrice RobertE.Filman(chair) Validation:CarlPixley,Synopsys; TheRoadAhead:Andrew DavidH.Albonesi _cp_ix_le_y_@_sy_n_op_s_ys_.c_om_ KSaanhnDgi,eUgon;iv_aeb_rks_i@ty_uoc_sf_dC._eadl_ifuornia, SMra.nMaegmerber/Circ.Marketing JAerannolBdaWco.n(Jay)Bragg EconomicsofDesignand Roundtables:WilliamH.Joyner GeorgannCarter CarlChang _Tme_.as_bt:a_dM_iar_@g_dfry_eeA_sbc_aa_dlei_.rc,_oFm_reescale; JCro.,rpSe.;m_wi_iclol_ian_mdu_.jco_tyon_re_Rr@e_sse_rac_r.oc_hrg BMuasniangeesrsDevelopment TNFriomerdmCDahnoeunCgghliosnacky EmbeddedSystemsand Standards:VictorBerman, SandyBrown HakanErdogmus _SPshr_oianf_rtcaw_edat@_ornee_e:U_.Spn_hriiavn_reca_redsit_toMy_n;a._elidk_u, _CvTb_aTedT_reCm_nac_Nnee_@Dw_cesa_sldie_getnt_necS_rey:_.scBt_eormum_cse; Kim, SrM.aAriadnveAnrtdiesrisnongCoordinator DJCaaamrvliedEs.AHLleaannnddGlwerreiehrr EmbeddedTest:Cheng-WenWu, UniversityofAlabama; SethuramanPanchanathan NationalTsingHuaUniversity; _br_u_ce_.k_im_@_i_ee_e_.o_rg MaureenStone _cw_w_@_e_e_.n_th_u_.e_du_.t_w RoyWant EmergingDevices:Krishnendu D&TALLIANCE Chakrabarty,DukeUniversity; PROGRAM_______________ _kr_is_h@_e_e_e._du_k_e._ed_u DTAPchair: InfrastructureIP:Andre´ Ivanov, YervantZorian,VirageLogic; SubmissionInformation:SubmitaWord,pdf,text,orPostScriptversionofyoursubmissionto UniversityofBritishColumbia; _zo_ri_an_@_v_ira_g_el_og_ic_.c_o_m ManuscriptCentral,http://mc.manuscriptcentral.com/cs-ieee _iv_an_o_v_@_ec_e_.u_bc_.c_a Asia:HidetoshiOnodera,Kyoto Editorial:Unlessotherwisestated,bylinedarticlesandcolumns,aswellasproductandservice LowPower:AnandRaghunathan, University;_on_o_d_er_a@_i_.k_yo_to_-u_.a_c_.jp NECUSA;_an_a_n_d@_n_e_c-_la_bs_.c_om_ CANDE:RichardC.Smith, descriptions,reflecttheauthor’sorfirm’sopinions.InclusioninIEEEDesign&TestofComputers MemoryTest:FabrizioLombardi, EDAandApplicationProcess doesnotnecessarilyconstituteendorsementbytheIEEEComputerSocietyortheIEEECircuits NortheasternUniversity; Consulting;_ds_m_it_h@_t_op_h_er_.n_et andSystemsSociety.Allsubmissionsaresubjecttoeditingforclarityandspaceconsiderations. _lo_m_b_ar_di_@_ec_e_.n_eu_._ed_u DAC:LucianoLavagno, Copyrightandreprintpermissions:CopyrightG2007bytheInstituteofElectricaland MicroelectronicICPackaging: PolitecnicodiTorino, ElectronicsEngineers,Inc.Allrightsreserved.Abstractingispermittedwithcredittothesource. BruceKim,UniversityofAlabama; _la_va_g_no_@_p_o_lit_o._it; LibrariesarepermittedtophotocopybeyondthelimitsofUSCopyrightLawforprivateuseof _br_u_ce_.k_im_@_i_ee_e_.o_rg aUnndiveArnsditryeowfKCaahlinfogr,nia,SanDiego patronsthosepost-1977articlesthatcarryacodeatthebottomofthefirstpage,providedtheper- MultiprocessorSoC: copyfeeindicatedinthecodeispaidthroughtheCopyrightClearanceCenter,222Rosewood AhmedJerraya,CEA-Leti; DATC:JoeDamore; Drive,Danvers,MA01923;forothercopying,reprint,orrepublicationpermission,writeto _ah_m_e_d_.je_rr_ay_a_@_ce_a_.fr _jo_ep_d_a_m_or_e@_a_o_l.c_o_m CopyrightsandPermissionsDepartment,IEEEPublicationsAdministration,445HoesLane,PO NanotechnologyArchitectures DATE:AhmedJerraya,CEA-Leti; Box1331,Piscataway,NJ08855-1331. andDesignTechnology: _ah_m_e_d._je_rr_ay_a@_c_e_a._fr SethGoldstein, Europe:BernardCourtois,TIMA-CMP; IEEEDesign&TestofComputers(ISSN0740-7475)iscopublishedbimonthlybytheIEEE CarnegieMellonUniversity; _be_r_na_rd_.c_o_ur_to_is_@_im_a_g_.fr ComputerSocietyandtheIEEECircuitsandSystemsSociety.IEEEHeadquarters:345East47th _se_th_.g_o_ld_st_ei_n@_c_s._cm_u_._ed_u LatinAmerica:RicardoReis, St.,NewYork,NY10017-2394.IEEEComputerSocietyPublicationsOffice:10662LosVaqueros PerformanceIssuesin UniversidadeFederaldoRio Circle,POBox3014,LosAlamitos,CA90720-1314;phone+17148218380.IEEEComputerSociety ICDesign: GrandedoSul;_re_is_@_in_f.u_f_rg_s.b_r Headquarters:1730MassachusettsAve.NW,Washington,DC20036-1903.IEEECircuitsand SachinSapatnekar,Universityof TTTC:Andre´ Ivanov, SystemsSocietyExecutiveOffice,445HoesLane,Piscataway,NJ08854;phone+17324655853. Minnesota;_sa_c_hi_n@_e_c_e._um_n_.e_d_u UniversityofBritishColumbia; Annualsubscriptionrates:IEEEComputerSocietymembersgetthelowestrates:$39US(print SoCDesign:SohaHassoun, _iv_an_o_v@_e_c_e._u_bc_.c_a andelectronic).Gotohttp://www.computer.org/subscribetoorderandformoreinformationon TuftsUniversity; othersubscriptionprices.Backissues:members,$25;nonmembers,$99.TheBiomedical _so_h_a@_c_s_.tu_ft_s.e_d_u ADVISORY BOARD ______ EngineeringCitationIndexonCD-ROMlistsIEEEDesign&TestofComputersarticles. SystemSpecificationand AnthonyAmbler, Modeling:SandeepShukla, UniversityofTexasatAustin Postmaster:SendundeliveredcopiesandaddresschangestoIEEEDesign&TestofComputers, VirginiaPolytechnicandState IvoBolsens,Xilinx CirculationDept.,POBox3014,LosAlamitos,CA90720-1314.PeriodicalspostagepaidatNewYork, University;_sh_u_kl_a@_v_t._ed_u WilliamMann NY,andatadditionalmailingoffices.CanadianGST#125634188.CanadaPostCorp.(Canadian MemberatLarge:KaushikRoy, distribution)PublicationsMailAgreement#40013885.ReturnundeliverableCanadian PurdueUniversity; TomWilliams,Synopsys addressesto4960-2WalkerRoad;Windsor,ONN9A6J3.PrintedinUSA. _ka_u_sh_ik_@_e_cn_.p_u_rd_u_e._ed_u YervantZorian,VirageLogic PreviousPage | Contents | Zoomin | Zoomout | FrontCover | SearchIssue | NextPage ABEFMaGS PreviousPage | Contents | Zoomin | Zoomout | FrontCover | SearchIssue | NextPage ABEFMaGS Advances in Functional Validation through Hybrid Techniques Guest Editors’ Introduction: Attacking Functional Verification through Hybrid Techniques Jayanta Bhadra and Magdy S. Abadir Li-C. Wang Freescale Semiconductor University of California, Santa Barbara & IN INDUSTRIAL DESIGN environments, verification help explain some of thedifferent facetsofthisarea, engineers are typically not required to write formal we present this special issue, which includes five properties for system correctness, but they are articles. expected to maximize verification coverage. They Theissuebeginswithasurveyarticleonthetopic, mustdothisunderthedualconstraintsofdesigncost whichwewrotealongwithourcolleague,SandipRay. andtimetomarket.Intheabsenceofcompleteformal- Thissurveyarticleoutlinessomeoftherecentworkin verification solutions for industrial-strength designs, this rapidly developing area. Next, in ‘‘Hybrid Verifi- andgiventhatsimulationisstillthemainstayforreal- cation of Protocol Bridges,’’ Praveen Tiwari and Raj life verification issues, a new breed of hybrid Mitra demonstrate that a hybrid framework can find validation tools and techniques has come to the bugs that individual techniques are unable to find forefront. The scalability of simulation, along with its alone. They have developed a technique that uses universal appeal of being easily applicable to practi- simulation and formal verification to complement cally any design, makes it useful for all verification scalabilityandcompleteness.Theapplicationdomain tasks. Its drawbacks are being addressed through isprotocolverification. powerful analysis tools such as formal verification, In ‘‘Combining Theorem Proving with Model automatic test-pattern generators, symbolic tech- Checking through Predicate Abstraction,’’ Sandip niques, satisfiability (SAT) checkers, bounded model RayandRobSumnerspresentaprocedureforproving checking,anddatamining.Theproblemhasbecome invariants of infinite-state reactive systems using oneofefficientlycombiningthedisparatetechniques a combination of two formal verification techniques: so that they can cooperate with one another in theorem proving and model checking. This method ameaningfulway. usestermrewritingtoreduceaninvariantproofofthe Hybridtechniqueshaveproveneffectiveinexplor- target system to reachability analysis on a finite inginterestingcornercases,coverageholes,invariant predicateabstractionthatcanbedischargedbymodel variations,andsoforth,inthegeneralareaofdirected checking.Themethodaffordssubstantialautomation functional validation. Despite the emergence of in invariant proofs, while preserving the expressive- severaldemonstrablyeffectivehybridvalidationtech- nessandcontrolaffordedbytheoremproving. niques, both industrial and academic, several ques- ‘‘Hybrid, Incremental Assertion-Based Verification tions remain: Do hybrid techniques enable fast and for TLM Design Flows,’’ by Nicola Bombieri et al., improved design validation? Have the supporting addresses problems that arise in refining now-ubiqui- methodologies that can maximize the gain from toustransaction-levelmodelstoefficientRTLmodels. hybrid techniques matured? What major issues are The authors present a hybrid, incremental, assertion- beingaddressedbyteamsofengineersworkinginthe basedverificationtechniquetocheckthecorrectness area of directed functional validation in industry? To oftherefinement.Owingtothemanualnatureofthe 110 0740-7475/07/$25.00G2007IEEE CopublishedbytheIEEECSandtheIEEECASS IEEEDesign&TestofComputers PreviousPage | Contents | Zoomin | Zoomout | FrontCover | SearchIssue | NextPage ABEFMaGS PreviousPage | Contents | Zoomin | Zoomout | FrontCover | SearchIssue | NextPage ABEFMaGS translation process, this method is an important tool and verification of digital systems, mathematical forcatchingbugsearlyinthedesigncycle.Theauthors logic, VLSI algorithms, and multicore verification. also demonstrate the effectiveness of their technique Bhadra has a PhD in electrical and computer onanindustrial-strengthdesign. engineering from the University of Texas at Austin. Finally, in ‘‘Hybrid Approach to Faster Functional Heis amemberof theIEEE. VerificationwithFullVisibility,’’Chin-LungChuanget al. present an interesting technique that combines MagdyS.Abadiristhemanagerof simulation and emulation to achieve a faster, more EDA strategy, EDA vendor relations, efficient front-end debugging environment. Logic and customer collaboration at Free- simulators provide controllability and observability, scale Semiconductor. He is also an and emulators offer speed. To achieve faster debug- adjunctfacultymemberattheUniver- ging, the authors present a platform in which an sity of Texas at Austin, and he is Associate EIC of emulator’s internal states are recorded and later IEEE Design & Test. His research interests include played back through a software simulation environ- microprocessortestandverification,testeconomics, ment. They demonstrate that the technique provides andDFT.AbadirhasaBSincomputersciencefrom excellentspeedup. the University of Alexandria, Egypt, an MS in computer science from the University of Saskatch- ALTHOUGH A COMPREHENSIVE verification methodo- ewan, and a PhD in electrical engineering from the logyforarbitrarydesignsremainsanelusivegoal,there University of Southern California. He coedited the is an encouraging trendto enhance the capability of IEEE Design & Test special issue on functional verification methodologies through the cross-pollina- verificationin 2004.He isan IEEEFellow. tion of hybrid techniques. Some of these hybrid techniques are even supported today by a variety of Li-C.Wangisanassociateprofessor commercial tools. Perhaps it will be through these in the Department of Electrical and cross-pollination efforts that one day we will achieve Computer Engineering of the Univer- that elusive goal of a comprehensive verification sity of California, Santa Barbara. His methodology. Of course, it is impractical to address research interests include micropro- all hybrid verificationwithinasingleissue.However, cessor test and verification, statistical methods for wehopethesefivearticlescanprovideagoodsource timing analysis, speed test and performance valida- forfurtherreferencesandfutureresearch.Wethankall tion, and applications of data mining and statistical the authors and referees for their contributions in learning in EDA. Wang has an MS in computer creatingthisspecialissue.Wealsoexpressoursincere science and a PhD in electrical and computer thankstoourcolleagueandfriendTimCheng(EICof engineering, both from the University of Texas at IEEEDesign&Test)forhissupportandguidance.We Austin. He coedited the IEEE Design & Test special hope that you enjoy this special issue and that it issueonfunctional verificationin 2004. inspiresmoreresearchtoovercomefutureverification challenges. & &Direct questionsand commentsaboutthisspecial issue to Jayanta Bhadra, Freescale Semiconductor, 7700 W. Parmer Lane, MD PL34, Austin, TX 78729; Jayanta Bhadra is the technical [email protected]. ________________ lead of formal verification and valida- tion at Freescale Semiconductor. He has worked on the verification of For further information on this or any other computing several generations of PowerPC mi- topic,visitourDigitalLibraryathttp://www.computer.org/ croprocessors.Hisresearchinterestsincludetesting _pu_b_li_ca_ti_on_s_/d_li_b. 111 March–April2007 PreviousPage | Contents | Zoomin | Zoomout | FrontCover | SearchIssue | NextPage ABEFMaGS PreviousPage | Contents | Zoomin | Zoomout | FrontCover | SearchIssue | NextPage ABEFMaGS Advances in Functional Validation through Hybrid Techniques A Survey of Hybrid Techniques for Functional Verification Jayanta Bhadra and Magdy S. Abadir Sandip Ray Freescale Semiconductor University of Texas at Austin Li-C. Wang University of California, Santa Barbara scalability, along with its easy applica- Editor’s note: bilitytopracticallyanydesignatalmost This article surveys recent advances in hybrid approaches for functional everyabstractionlevel,makesituseful verification. These approaches combine multiple verification techniques so for allverification tasks. Whenusedas that they complement one another, resulting in superior verification a stand-alone technique, simulation effectiveness. candetectsimpleandeasy-to-findbugs. —TimCheng, Editorin Chief However,overtime,itseffectivenessin finding corner-case bugs significantly & THEINCREASINGSIZEand complexity of industry decreases because generating stimuli that target hardwaredesigns,alongwithstringenttime-to-market interestingcornercasesisdifficult.Ontheotherhand, requirements,haveputaheavyburdenonverification although traditional formal techniques (broadly, to ensure that designs are relatively bug free. Late model checking and theorem proving) can, in detectionoferrorstypicallyleadstohighercostsdue principle,analyzeandfindallbugsinadesignmodel, toassociateddelaysandproductionlosses.Although their applicability in practice is limited. The well- bugfreedomremainsanunfulfilleddream,inindustry known state explosion problem limits model check- practicecatchingmorebugsearlierinthedesigncycle ing, and the cost of theorem proving is prohibitive is a top priority. Verification techniques that have becauseoftheamountofskilledmanualguidanceit maturedovertheyearshaveaddressedtheverification requires. bottleneck—that is, the bug detection problem—to Wedefineanyverificationtechniquesthatdon’tfall variouslevelsofsatisfaction.Ageneralthemesuccess- under the formal category as informal. Although the fullyadoptedbyacademiaaswellasseveralvendors capabilities of formal verification paradigms have istoapplymultipleverificationtechniquessothatthey beenincreasingovertime,theneedforanimmediate complement one another, resulting in an increase of practical solution has increased interest in hybrid the verification tool’s overall effectiveness. (The techniques, which combine formal and informal ‘‘Commercial hybrid verification tools’’ sidebar lists techniques. The general goal of a typical hybrid some examples of commercially available tools techniqueistoaddresstheverificationbottleneckby offered by various vendors.) Such integration must enhancingcoverageofthestatespacetraversed. be carried out delicately and precisely so that the overalltechniquebecomesmorethanmerelyasumof Taxonomy of hybrid methods thetechniques.Inthisarticle,wesurveytheresearch Intermsofcomputationalcomplexity,theverifica- thathastakenplaceinthisarea. tion problem ranges from NP-hard to undecidable, In industry practice, simulation remains the main- depending on system class, desired properties, and stay for most real-life verification issues. Simulation’s formal-guarantee strength. Thus, we cannot hope to 112 0740-7475/07/$25.00G2007IEEE CopublishedbytheIEEECSandtheIEEECASS IEEEDesign&TestofComputers PreviousPage | Contents | Zoomin | Zoomout | FrontCover | SearchIssue | NextPage ABEFMaGS