Design of embedded systems formal models, validation, and synthesis

STEPHENEDWARDS,MEMBER,IEEE,LUCIANOLAVAGNO,MEMBER,IEEE,

EDWARDA.LEE,FELLOW,IEEE,ANDALBERTOSANGIOVANNI–VINCENTELLI,MEMBER,IEEEInvitedPaper

Thispaperaddressesthedesignofreactivereal-timeembeddedsystems.Suchsystemsareoftenheterogeneousinimplementa-tiontechnologiesanddesignstyles,forexamplebycombininghardwareapplication-specificintegratedcircuits(ASIC’s)withembeddedsoftware.Theconcurrentdesignprocessforsuchem-beddedsystemsinvolvessolvingthespecification,validation,andsynthesisproblems.Wereviewthevarietyofapproachestotheseproblemsthathavebeentaken.

I.INTRODUCTION

Reactivereal-timeembeddedsystemsarepervasiveintheelectronicssystemindustry.Applicationsincludevehi-clecontrol,consumerelectronics,communicationsystems,remotesensing,andhouseholdappliances.Insuchappli-cations,specificationsmaychangecontinuouslyandtime-to-marketstronglyaffectssuccess.Thiscallsfortheuseofsoftwareprogrammablecomponentswithbehaviorthatcanbefairlyeasilychanged.Suchsystems,whichuseacomputertoperformaspecificfunction,butareneitherusednorperceivedasacomputer,aregenericallyknownasembeddedsystems.Morespecifically,weareinterestedinreactiveembeddedsystems.Reactivesystemsarethosethatreactcontinuouslytotheirenvironmentatthespeedoftheenvironment.Theycanbecontrastedwithinteractivesystems,whichreactwiththeenvironmentattheirown

ManuscriptreceivedFebruary1,1996;revisedDecember2,1996.TheworkofS.EdwardsandE.A.LeewassupportedbyARPAandtheU.S.AirForceRASSPProgramcontractF33615-93-C-1317,theStateofCaliforniaMICROprogram,andbyCadence,Dolby,Hitachi,LGElectronics,Mitsubishi,Motorola,NEC,Philips,andRockwell.TheworkofL.LavagnoandA.Sangiovanni–VincentelliwassupportedinpartbygrantsfromCadence,MagnetiMarelli,Daimler-Benz,Hitachi,ConsiglioNazionaledelleRicerche,theMICROprogram,andSRC.

S.EdwardsiswiththeUniversityofCalifornia,Berkeley,CA94720–1772USA(e-mail:sedwards@eecs.berkeley.edu).

L.LavagnoiswithCadenceBerkeleyLaboratories,Berkeley,CA94704-1144USA(e-mail:luciano@cadence.com).

E.A.LeeandA.Sangiovanni–VincentelliarewiththeElectricalEngineeringandComputerScienceDepartment,UniversityofCalifornia,Berkeley,CA94720–1770USA(e-mail:eal@eecs.berkeley.eduandalberto@leonardo.parades.rm.cnr.it).

PublisherItemIdentifierS0018-9219(97)02053-7.

speedandtransformationalsystems,whichtakeabodyofinputdataandtransformitintoabodyofoutputdata[1].Alargepercentageoftheworldwidemarketformicroprocessorsisfilledbymicrocontrollersthataretheprogrammablecoreofembeddedsystems.Inadditiontomicrocontrollers,embeddedsystemsmayconsistofapplication-specificintegratedcircuits(ASIC’s)and/orfieldprogrammablegatearrays(FPGA’s)aswellasotherprogrammablecomputingunitssuchasdigitalsignalprocessors(DSP’s).Sinceembeddedsystemsinteractcontinuouslywithanenvironmentthatisanaloginnature,theremusttypicallybecomponentsthatperformA/DandD/Aconversions.Asignificantpartofthedesignproblemconsistsofdecidingthesoftwareandhardwarearchitectureforthesystem,aswellasdecidingwhichpartsshouldbeimplementedinsoftwarerunningontheprogrammablecomponentsandwhichshouldbeimplementedinmorespecializedhardware.

Embeddedsystemsoftenareusedinlifecriticalsit-uations,wherereliabilityandsafetyaremoreimportantcriteriathanperformance.Today,embeddedsystemsaredesignedwithanadhocapproachthatisheavilybasedonearlierexperiencewithsimilarproductsandonmanualdesign.Useofhigher-levellanguagessuchasChelpssome-what,butwithincreasingcomplexity,itisnotsufficient.Formalverificationandautomaticsynthesisofimplemen-tationsarethesurestwaystoguaranteesafety.However,bothformalverificationandsynthesisfromhighlevelsofabstractionhavebeendemonstratedonlyforsmall,specializedlanguageswithrestrictedsemantics.Thisisatoddswiththecomplexityandheterogeneityfoundintypicalembeddedsystems.

Webelievethatthedesignapproachshouldbebasedontheuseofoneormoreformalmodelstodescribethebehaviorofthesystematahighlevelofabstraction,beforeadecisiononitsdecompositionintohardwareandsoftwarecomponentsistaken.Thefinalimplementationofthesystemshouldbemadeasmuchaspossibleusing

0018–9219/97$10.00©1997IEEE

366

PROCEEDINGSOFTHEIEEE,VOL.85,NO.3,MARCH1997

formalmodels.Onlythencanthesimplicityofmodelingrequiredbyverificationandsynthesisbereconciledwiththecomplexityandheterogeneityofreal-worlddesign.Theconcurrentdesignprocessformixedhardware/softwareembeddedsystemsinvolvessolvingthefollowingsubproblems:specification,validation,andsynthesis.Althoughtheseproblemscannotbeentirelyseparated,wedealwiththembelowinthreesuccessivesections.

II.SPECIFICATIONANDMODELING

Thedesignprocessisoftenviewedasasequenceofstepsthattransformsasetofspecificationsdescribedinformallyintoadetailedspecificationthatcanbeusedformanufac-turing.Alltheintermediatestepsarecharacterizedbyatransformationfromamoreabstractdescriptiontoamoredetailedone.

Adesignercanperformoneormorestepsinthisprocess.Forthedesigner,the“input”descriptionisaspecification,thefinaldescriptionofthedesignisanimplementation.Forexample,asoftwaredesignermayseeasetofroutineswritteninCasanimplementationofher/hisdesigneventhoughseveralotherstepsmaybetakenbeforethedesignisreadyformanufacturing.Duringthisprocess,verificationofthequalityofthedesignwithrespecttothedemandsplacedonitsperformanceandfunctionalityhastobecarriedout.Unfortunately,thedescriptionsofthedesignatitsvariousstagesareofteninformalandnotlogicallyconnectedbyasetofpreciserelationships.

Weadvocateadesignprocessthatisbasedonrepre-sentationswithprecisemathematicalmeaningsothatboththeverificationandthemapfromtheinitialdescriptiontothevariousintermediatestepscanbecarriedoutwithtoolsofguaranteedperformance.Suchanapproachisstandardincertaincommunities,wherelanguageswithstrongformalpropertiesareusedtoensurerobustdesign.ExamplesincludeML[2],dataflowlanguages(e.g.,Lucid[3]andHaskell[4])andsynchronouslanguages(e.g.,Lustre,Signal,andEstrel[5]).

Thereisabroadrangeofpotentialformalizationsofadesign,butmosttoolsanddesignersdescribethebehaviorofadesignasarelationbetweenasetofinputsandasetofoutputs.Thisrelationmaybeinformal,evenexpressedinnaturallanguage.Itiseasytofindexampleswhereinformalspecificationsresultedinunnecessaryredesigns.Inouropinion,aformalmodelofadesignshouldconsistofthefollowingcomponents.

1)Afunctionalspecification,givenasasetofexplicitorimplicitrelationswhichinvolveinputs,outputs,andpossiblyinternal(state)information.1

2)Asetofpropertiesthatthedesignmustsatisfy,givenasasetofrelationsoverinputs,outputs,andstates,thatcanbecheckedagainstthefunctionalspecification.

wewilldefineinputs,outputs,andstateinformation.Fornow,

considerthemassequencesofvalues.

367

1Later

Fig.1.ture.

Atypicalreactivereal-timeembeddedsystemarchitec-

automaticsynthesisfromthishighlevelofabstractiontoensureimplementationsthatare“correctbyconstruction.”Validationthroughsimulationorverificationshouldbedoneasmuchaspossibleatthehigherlevelsofabstraction.AtypicalhardwarearchitectureforanembeddedsystemisillustratedinFig.1.Thistypeofarchitecturecom-binescustomhardwarewithembeddedsoftware,lendingacertainmeasureofcomplexityandheterogeneitytothedesign.Evenwithinthesoftwareorhardwareportionsthemselves,however,thereisoftenheterogeneity.Insoft-ware,control-orientedprocessesmightbemixedunderthesupervisionofamultitaskingreal-timekernelrunningonamicrocontroller.Inaddition,hard-real-timetasksmayruncooperativelyononeormoreprogrammableDSP’s.Thedesignstylesusedforthesetwosoftwaresubsystemsarelikelytobequitedifferentfromoneanother,andtestingtheinteractionbetweenthemisunlikelytobetrivial.

ThehardwaresideofthedesignwillfrequentlycontainoneormoreASIC’s,perhapsdesignedusinglogicorbehavioralsynthesistools.Ontheotherhand,asignificantpartofthehardwaredesignmostlikelyconsistsofinter-connectionsofcommoditycomponents,suchasprocessorsandmemories.Again,thistimeonthehardwareside,wefindheterogeneity.ThedesignstylesusedtospecifyandsimulatetheASIC’sandtheinterconnectedcommoditycomponentsarelikelytobequitedifferent.Atypicalsystem,therefore,notonlymixeshardwaredesignwithsoftwaredesign,butalsomixesdesignstyleswithineachofthesecategories.

Mostoftenthesetoftasksthatthesystemimplementsarenotspecifiedinarigorousandunambiguousfashion,sothedesignprocessrequiresseveraliterationstoobtainconvergence.Moreover,duringthedesignprocess,thelevelofabstraction,detail,andspecificityindifferentpartsofthedesignvaries.Tocomplicatemattersfurther,theskillsetsanddesignstylesusedbydifferentengineersontheprojectarelikelytobedifferent.Thenetresultisthatduringthedesignprocess,manydifferentspecificationandmodelingtechniqueswillbeused.

Managingthedesigncomplexityandheterogeneityisthekeyproblem.Webelievethattheuseofformalmodelsandhigh-levelsynthesisforensuringsafeandcorrectdesignsdependsonunderstandingtheinteractionbetweendiverse

EDWARDSetal.:DESIGNOFEMBEDDEDSYSTEMS:FORMALMODELS,VALIDATION,ANDSYNTHESIS

3)Asetofperformanceindexesthatevaluatethequalityofthedesignintermsofcost,reliability,speed,size,etc.,givenasasetofequationsinvolving,amongotherthings,inputsandoutputs.

4)Asetofconstraintsonperformanceindexes,specifiedasasetofinequalities.Thefunctionalspecificationfullycharacterizestheop-erationofasystem,whiletheperformanceconstraintsboundthecost(inabroadsense).Thesetofpropertiesisredundant,inthatinaproperlyconstructeddesign,thefunctionalspecificationsatisfiestheseproperties.However,thepropertiesarelistedseparatelybecausetheyaresimplerandmoreabstract(andalsoincomplete)comparedtothefunctionalspecification.Apropertyisanassertionaboutthebehavior,ratherthanadescriptionofthebehavior.Itisanabstractionofthebehavioralongaparticularaxis.Forexample,whendesigninganetworkprotocol,wemayrequirethatthedesignneverdeadlock(thisisalsocalledalivenessproperty).Notethatlivenessdoesnotcompletelyspecifythebehavioroftheprotocol;itisinsteadapropertywerequireourprotocoltohave.Forthesameprotocol,wemayrequirethatanyrequestwilleventuallybesatisfied(thisisalsocalledfairness).Againthisdoesnotcompletelyspecifythebehavioroftheprotocolbutitisarequiredproperty.

Givenaformalmodelofthefunctionalspecificationsandoftheproperties,wecanclassifypropertiesinthreegroups:1)propertiesthatareinherentinthemodelofcomputa-tion(i.e.,theycanbeshownformallytoholdforallspecificationsdescribedusingthatmodel);

2)propertiesthatcanbeverifiedsyntacticallyforagivenspecification(i.e.,theycanbeshowntoholdwithasimple—usuallypolynomial—timeanalysisofthespecification);

3)propertiesthatmustbeverifiedsemanticallyforagivenspecification(i.e.,theycanbeshowntoholdbyexecuting,atleastimplicitly,thespecificationforallinputsthatcanoccur).Forexample,considerthepropertyofdeterminatebehav-ior,i.e.,thefactthattheoutputofasystemdependsonlyonitsinputsandnotonsomeinternal,hiddenchoice.Anydesigndescribedbyadataflownetwork(aformalmodeltobedescribedlater)isdeterminate,andhencethispropertyneednotbechecked.Ifthedesignisrepresentedbyanetworkoffinite-statemachines(FSM’s),determinacycanbeassessedbyinspectionofthestatetransitionfunction.Insomediscreteeventmodels(forexamplethoseembodiedinVerilogandVHDL)determinacyisdifficulttoprove:itmustbecheckedbyexhaustivesimulation.

Thedesignprocesstakesamodelofthedesignatalevelofabstractionandrefinesittoalowerone.Indoingso,thedesignermustensurethatthepropertiesatthatlevelofabstractionareverified,thattheconstraintsaresatisfied,andthattheperformanceindexesaresatisfactory.Therefinementprocessinvolvesalsomappingconstraints,

368

Fig.2.Anexampleofadesignrefinementstage,whichuseshardwareandsoftwaresynthesistotranslateafunctionalspeci-ficationintoamodelofhardware.

performanceindexes,andpropertiestothelowerlevelsothattheycanbecomputedforthenextleveldown.2Fig.2showsakeyrefinementstageinembeddedsystemdesign.Themoreabstractspecificationinthiscaseisanexecutablefunctionalmodelthatisclosertotheproblemlevel.Thespecificationundergoesasynthesisprocess(whichmaybepartlymanual)thatgeneratesamodelofanimplementationinhardware.Thatmodelitselfmaystillbefairlyabstract,capturingforexampleonlytimingproperties.Inthisex-amplethemodelispresumablyusedforhardware/softwarepartitioning.

WhileFig.2suggestsapurelytop-downprocess,anyrealdesignneedsmoreinteractionbetweenspecificationandimplementation.Nonetheless,whenadesigniscomplete,thebestwaytopresentanddocumentitistopdown.Thisisenoughtorequirethatthemethodologysupporttop-downdesign.

A.ElementsofaModelofComputation

Alanguageisasetofsymbols,rulesforcombiningthem(itssyntax),andrulesforinterpretingcombinationsofsymbols(itssemantics).Twoapproachestosemanticshaveevolved:denotationalandoperational.Alanguagecanhaveboth(ideallytheyareconsistentwithoneanother,althoughinpracticethiscanbedifficulttoachieve).Oper-ationalsemantics,whichdatesbacktoTuringmachines,givesmeaningofalanguageintermsofactionstakenbysomeabstractmachineandistypicallyclosertotheimplementation.Denotationalsemantics,firstdevelopedbyScottandStrachey[7],givesthemeaningofthelanguageintermsofrelations.

Howtheabstractmachineinanoperationalsemanticscanbehaveisafeatureofwhatwecallthemodelofcomputationunderlyingthelanguage.Thekindsofrelationsthatarepossibleinadenotationalsemanticsisalsoafeatureofthemodelofcomputation.Otherfeaturesincludecommunica-tionstyle,howindividualbehaviorisaggregatedtomakemorecomplexcompositions,andhowhierarchyabstractssuchcompositions.

2The

refinementprocesscanbedefinedformallyoncethemodelsof

thedesignareformallyspecifiedbyMcMillan[6].

PROCEEDINGSOFTHEIEEE,VOL.85,NO.3,MARCH1997

Adesign(atalllevelsoftheabstractionhierarchyfromfunctionalspecificationtofinalimplementation)isgener-allyrepresentedasasetofcomponents,whichcanbeconsideredasisolatedmonolithicblocks,interactingwitheachotherandwithanenvironmentthatisnotpartofthedesign.Themodelofcomputationdefinesthebehaviorandinteractionoftheseblocks.

Inthesectionsthatfollow,wepresentaframeworkforcomparingelementsofdifferentmodelsofcomputation,calledthetagged-signalmodel,anduseittocontrastdifferentstylesofsequentialbehavior,concurrency,andisapartitionof

inputsand

-tuple

if

where

,

-tupleinopfutsifgonraplsrocess-tuploeuotfputsfigonraplrsocess

describestheinpuitss,and

thesetofbehaviorsconsis.tentwiththeicommunication.Wewillgiveprecisedefinitionsforanumberofterms,butthesedefinitionswillinevitablycon-flictwithstandardusageinsomecommunities.Wehavediscoveredthat,shortofabandoningtheuseofmostcommonterms,noterminologycanbeconsistentwithstandardusageinallrelatedcommunities.Thusweattempttoavoidconfusionbybeingprecise,evenattheriskofbeingpedantic.

1)TheTagged-SignalModel:LeeandSangiovanni–Vincentellihaveproposedthetagged-signalmodel[8],aformalismfordescribingaspectsofmodelsofcomputationforembeddedsystemspecification.ItisdenotationalintheScottandStrachey[7]sense,anditdefinesasemanticframework(ofsignalsandprocesses)withinwhichmodelsofcomputationcanbestudiedandcompared.Itisveryabstract—describingaparticularmodelofcomputationinvolvesimposingfurtherconstraintsthatmakeitmoreconcrete.

Thefundamentalentityinthetagged-signalmodelisanevent—avalue/tagpair.Tagsareoftenusedtodenotetem-poralbehavior.Asetofevents(anabstractaggregation)isasignal.Processesarerelationsonsignals,expressedassetsof

andasetoftags

,i.e.,aneventhasatagandavalue.

Asignal

.Afunctionalsignalisa(possiblypartial)

functionfrom

.Thesetofallsignalsisdenotedsignalsisdenoted

inthetagged-signalmodel.

Inparticular,inatimedsystem

onmembersof

,,andor

isonlypartiallyordered.

Aprocess

-tuplesofsignals,.Aparticular

.An

Aprocess

and

,then,where

2)State:Mostmodelsofcomputationincludecompo-nentswithstate,wherebehaviorisgivenasasequenceofstatetransitions.Inordertoformalizethisnotion,letusconsideraprocess

.Letusassumeforthemomentthat

,wecandefine

withtagsgreaterthan

,

(denotedimplies

.Thisdefinitionintuitivelymeansthatprocess

prior

totime,thentheoutputswillalsobeidentical.

.

Followingalongtradition,wecalltheseequivalenceclassesthestatesof

arecalledcombinational,

whilecomponentswithmorethanonestateforsome

inthetagged-signalmodel.Recallthatinatimedsystem

isonlypartially

ordered.Implicitcommunicationgenerallyrequirestotallyorderedtags,usuallyidentifiedwithphysicaltime.

Thetagsinametric-timesystemhavethenotionofa“dis-tance”betweenthem,muchlikephysicaltime.Formally,thereexistsapartialfunction

and

somemodelsthiseventcouldhaveavaluedenotingtheabsenceofanevent(calledbottom).Ateachclocktick,eachprocessmapsinputvaluestooutputvalues.Ifcycliccommunicationisallowed,thensomemechanismmustbeprovidedtoresolveorpreventcirculardependencies.Onepossibilityistoconstraintheoutputvaluestohavetagscorrespondingtothenexttick.Anotherpossibility(alltoocommon)istoleavetheresultunspecified,resultinginnondeterminacy(orworse,infinitecomputationwithinonetick).Athirdpossibilityistousefixed-pointsemantics,wherethebehaviorofthesystemisdefinedasasetofeventsthatsatisfyallprocesses.

Concurrencyinphysicalimplementationsofsystemsoccursthroughsomecombinationofparallelism,havingphysicallydistinctcomputationalresources,andinterleav-ing,sharingofacommonphysicalresource.Mechanismsforachievinginterleavingvarywidely,rangingfromoper-atingsystemsthatmanagecontextswitchestofullystaticinterleavinginwhichconcurrentprocessesareconverted(compiled)intoasinglenonconcurrentprocess.Wefocushereonthemechanismsusedtomanagecommunicationbetweenconcurrentprocesses.

Parallelphysicalsystemsnaturallyshareacommonno-tionoftime,accordingtothelawsofphysics.Thetimeatwhichaneventinonesubsystemoccurshasanaturalorderingrelationshipwiththetimeatwhichaneventoccursinanothersubsystem.Physicallyinterleavedsystemsalsoshareanaturalcommonnotionoftime.

Logicalsystems,ontheotherhand,needamechanismtoexplicitlyshareanotionoftime.Considertwoimperativeprogramsinterleavedonasingleprocessorunderthecontroloftime-sharingoperatingsystem.Interleavingcreatesanaturalorderingbetweeneventsinthetwoprocesses,butthisorderingisgenerallyunreliablebecauseitheavilydependsonschedulingpolicysystemload,andsoon.Somesynchronizationmechanismisrequiredifthosetwoprogramsneedtocooperate.

Moregenerally,inlogicallyconcurrentsystems,main-tainingacoherentglobalnotionoftimeasatotalorderonevents,canbeextremelyexpensive.Henceinpracticethisisreplacedwheneverpossiblewithanexplicitsynchro-nization,inwhichthistotalorderisreplacedbyapartialorder.Returningtotheexampleoftwoprocessesrunningunderatime-sharingoperatingsystem,wetakeprecautionstoensureanorderingoftwoeventsonlyiftheorderingofthesetwoeventsmatters.

Avarietyofmechanismsformanagingtheorderofevents,andhenceforcommunicatinginformationbetweenprocesses,hasarisen.Someofthemostcommononesarelistedbelow.

•Unsynchronized:Inanunsynchronizedcommunica-tion,aproducerofinformationandaconsumeroftheinformationarenotcoordinated.Thereisnoguaranteethattheconsumerreadsvalidinformationproducedbytheproducer,andthereisnoguaranteethattheproducerwillnotoverwritepreviouslyproduceddatabeforetheconsumerreadsthedata.Inthetagged-signalmodel,therepositoryforthedataismodeled

•

•

•

•

asaprocess,andthereadingandwritingeventshavenoenforcedorderingrelationshipbetweentheirtags.Read-modify-write:Commonlyusedforaccessingshareddatastructures,thisstrategylocksadatastructurebetweenareadandwritefromaprocess,preventinganyotheraccesses.Inotherwords,theactionsofreading,modifying,andwritingareatomic(indivisible).Inthetagged-signalmodel,therepositoryforthedataismodeledasaprocesswhereeventsassociatedwiththisprocessaretotallyordered(resultinginagloballypartiallyorderedmodel).Theread-modify-writeismodeledasasingleevent.

UnboundedFirst-InFirst-Out(FIFO)buffered:Thisisapoint-to-pointcommunicationstrategy,whereaproducergeneratesasequenceofdatatokensandconsumerconsumesthesetokens,butonlyaftertheyhavebeengenerated.Inthetagged-signalmodel,thisisasimpleconnectionwherethesignalontheconnectionisconstrainedtohavetotallyorderedtags.ThetagsmodeltheorderingimposedbytheFIFOmodel.Iftheconsumerimplementsblockingreads,thenitimposesatotalorderoneventsatallitsinputsignals.ThismodelcapturesessentialpropertiesofbothKahnprocessnetworksanddataflow[13].

BoundedFIFObuffered:Inthiscase,thedatarepos-itoryismodeledasaprocessthatimposesorderingconstraintsonitsinputs(whichcomefromthepro-ducer)andtheoutputs(whichgototheconsumer).Eachoftheinputandoutputsignalsareinternallytotallyordered.Thesimplestcaseiswherethesizeofthebufferisone,inwhichcasetheinputandoutputeventsmustbeinterleavedsothateachoutputeventliesbetweentwoinputevents.Largerbuffersimposeamaximumdifference(oftencalledsynchronicdistance)betweenthenumberofinputandoutputevents.

Notethatsomeimplementationsofthiscommuni-cationmechanismmaynotreallyblockthewritingprocesswhenthebufferisfull,thusrequiringsomehigherlevelofflowcontroltoensurethatthisneverhappens,orthatitdoesnotcauseanyharm.

Rendezvous:Inthesimplestformofrendezvous,im-plemented,i.e.,inOccamandLotos,asinglewritingprocessandasinglereadingprocessmustsimultane-ouslybeatthepointintheircontrolflowwherethewriteandthereadoccur.Itisaconvenientcommu-nicationmechanism,becauseithasthesemanticsofasingleassignment,inwhichthewriterprovidestheright-handside,andthereaderprovidestheleft-handside.Inthetagged-signalmodel,thisisimposedbyeventswithidenticaltags[8].Lotosoffers,inaddition,multiplerendezvous,inwhichoneamongmultiplepossiblecommunicationsisnondeterministicallyse-lected.Multiplerendezvousismoreflexiblethansinglerendezvous,becauseitallowsthedesignertospecifymoreeasilyseveral“expected”communicationportsatanygiventime,butitisverydifficultandexpensivetoimplementcorrectly.

371

EDWARDSetal.:DESIGNOFEMBEDDEDSYSTEMS:FORMALMODELS,VALIDATION,ANDSYNTHESIS

Table1AComparisonofConcurrencyandCommunicationSchemes

Transmittersmanymanyoneoneoneone

Receiversmanymanyoneoneoneone

BufferSize

oneoneunboundedboundedoneone

BlockingReads

noyesyesyesyesno

BlockingWrites

noyesnomaybeyesno

SingleReads

nonoyesyesyesyes

UnsynchronizedRead-Modify-WriteUnboundedFIFOBoundedFIFOSingleRendezvousMultipleRendezvous

Ofcourse,variouscombinationsoftheabovemodelsarepossible.Forexample,inapartiallyunsynchronizedmodel,aconsumerofdatamayberequiredtowaituntilthefirsttimeaproducerproducesdata,afterwhichthecommunicationisunsynchronized.

Theessentialfeaturesoftheconcurrencyandcommu-nicationstylesdescribedabovearepresentedinTable1.Thesearedistinguishedbythenumberoftransmittersandreceivers(e.g.,broadcastversuspoint-to-pointcommunica-tion),thesizeofthecommunicationbuffer,whetherthetransmittingorreceivingprocessmaycontinueafteranunsuccessfulcommunicationattempt(blockingreadsandwrites),andwhethertheresultofeachwritecanbereadatmostonce(singlereads).

B.CommonModelsofComputation

Wearenowreadytousetheschemedevelopedintheprevioussectiontoclassifyandanalyzeseveralmodelsofcomputationthathavebeenusedtodescribeembeddedsystems.Wewillconsiderissuessuchaseaseofmodeling,efficiencyofanalysis(simulationorformalverification),automatedsynthesizability,optimizationspaceversusover-specification,andsoon.

1)DiscreteEvent:TimeisanintegralpartofaDEmodelofcomputation.Eventsusuallycarryatotallyorderedtimestampindicatingthetimeatwhichtheeventoccurs.ADEsimulatorusuallymaintainsaglobaleventqueuethatsortseventsbytimestamp.

DigitalhardwareisoftensimulatedusingaDEapproach.TheVeriloglanguage,forexample,wasdesignedasaninputlanguageforaDEsimulator.TheVHDLlanguagealsohasanunderlyingDEmodelofcomputation.

DEmodelingcanbeexpensive—sortingtimestampscanbetime-consuming.Moreover,ironically,althoughDEisideallysuitedtomodelingdistributedsystems,itisverychallengingtobuildadistributedDEsimulator.Theglobalorderingofeventsrequirestightcoordinationbetweenpartsofthesimulation,renderingdistributedexecutiondifficult.Discrete-eventsimulationismostefficientforlargesys-temswithlarge,frequentlyidleorautonomouslyoperatingsections.UnderDEsimulation,onlythechangesinthesystemneedtobeprocessed,ratherthanthewholesystem.Astheactivityofasystemincreases,theDEparadigmbecomeslessefficientbecauseoftheoverheadinherentinprocessingtimestamps.

Simultaneousevents,especiallythosearisingfromzero-delayfeedbackloops,presentachallengeforDEmodelsofcomputation.Insuchasituation,eventsmayneedtobeordered,butarenot.

372

(a)(b)

(c)(d)

Fig.3.SimultaneouseventsinaDEsystem.(a)ProcessAproduceseventswiththesametimestamp.ShouldBorCbefirednext?(b)Zero-delayprocessBhasfired.HowmanytimesshouldCbefired?(c)Delta-delayprocessBhasfired;CwillconsumeA’soutputnext.(d)Chasfiredonce;itwillfireagaintoconsumeB’soutput.

ConsidertheDEsystemshowninFig.3.ProcessBhaszerodelay,meaningthatitsoutputhasthesametimestampasitsinput.IfprocessAproduceseventswiththesametimestamponeachoutput,thereisambiguityaboutwhetherBorCshouldbeinvokedfirst,asshowninFig.3(a).

SupposeBisinvokedfirst,asshowninFig.3(b).Now,dependingonthesimulator,Cmightbeinvokedonce,observingbothinputeventsinoneinvocation,oritmightbeinvokedtwice,processingtheeventsoneatatime.Inthelattercase,thereisnoclearwaytodeterminewhicheventshouldbeprocessedfirst.

Theadditionofdeltadelaymakessuchnondeterminacyeasiertoprevent,butdoesnotavoiditcompletely.Itintroducesatwo-levelmodeloftimeinwhicheachinstantoftimeisbrokeninto(apotentiallyinfinitenumberof)totallyordereddeltasteps.Thesimulatedtimereportedtotheuser,however,doesnotincludedeltainformation.A“zero-delay”processinthismodelactuallyhasdeltadelay.Forexample,ProcessBwouldhavedeltadelay,sofiringAfollowedbyBwouldresultinthesituationinFig.3(c).ThenextfiringofCwillseetheeventfromAonly;thefiringafterthatwillseethe(delay-delayed)eventfromB.Othersimulators,includingtheDEsimulatorinPtolemy[14],attempttostaticallyanalyzedataprecedenceswithinasingletimeinstant.Suchprecedenceanalysisissimilartothatdoneinsynchronouslanguages(Esterel,Lustre,andSignal)toensurethatsimultaneouseventsareprocesseddeterministically.Itdeterminesapartialorderingofeventswiththesametimestampbyexaminingdataprecedences.AddingafeedbackloopfromProcessCtoAinFig.3wouldcreateaproblemifeventscirculatethroughtheloopwithoutanyincrementintimestamp.Thesameproblem

PROCEEDINGSOFTHEIEEE,VOL.85,NO.3,MARCH1997

occursinsynchronouslanguages,wheresuchloopsarecalledcausalityloops.Noprecedenceanalysiscanresolvetheambiguity.Insynchronouslanguages,thecompilermaysimplyfailtocompilesuchaprogram.SomeDEsimulatorswillexecutetheprogramnondeterministically,whileotherssupporttightercontroloverthesequencingthroughgraphannotations.

2)CommunicatingFiniteStateMachines:FSM’sareanattractivemodelforembeddedsystems.Theamountofmemoryrequiredbysuchamodelisalwaysdecidable,andisoftenanexplicitpartofitsspecification.Haltingandperformancequestionsarealwaysdecidablesinceeachstatecan,intheory,beexaminedinfinitetime.Inpractice,however,thismaybeprohibitivelyexpensive.AtraditionalFSMconsistsof:

•asetofinputsymbols(theCartesianproductofthesetsofvaluesoftheinputsignals);

•asetofoutputsignals(theCartesianproductofthesetsofvaluesoftheoutputsignals);

•afinitesetofstateswithadistinguishedinitialstate;•anoutputfunctionmappinginputsandstatestoout-puts;

•anext-statefunctionmappinginputsandstatesto(next)states.

Theinputtosuchamachineisasequenceofinputsymbols,andtheoutputisasequenceofoutputsymbols.TraditionalFSM’saregoodformodelingsequentialbehavior,butareimpracticalformodelingconcurrencyormemorybecauseoftheso-calledstateexplosionproblem.Asinglemachinemimickingtheconcurrentexecutionofagroupofmachineshasanumberofstatesequaltotheproductofthenumberofstatesofeachmachine.Amemoryhasasmanystatesasthenumberofvaluesthatcanbestoredateachlocationraisedtothepowerofthenumberoflocations.Thenumberofstatesaloneisnotalwaysagoodindicationofcomplexity,butitoftenhasastrongcorrelation.

Hareladvocatedtheuseofthreemajormechanismsthatreducethesize(andhencethevisualcomplexity)offiniteautomata(FA)formodelingpracticalsystems[15].Thefirstoneishierarchy,inwhichastatecanrepresentanenclosedstatemachine.Thatis,beinginaparticularstateisactive.Equivalently,beinginstate

.Underthe

latterinterpretation,thestatesof

inacycle-basedspecificationlanguage.CFE’sareanalgebraicmodelextendingregularexpressions[9]andcanbecompiledintoFSM’sthatcanbeusedinthesynthesisofacontrolunit.

3)Synchronous/Reactive:Inasynchronousmodelofcomputation,alleventsaresynchronous,i.e.,allsignalshaveeventswithidenticaltags.Thetagsaretotallyorderedandgloballyavailable.Simultaneousevents(thoseinthesameclocktick)maybetotallyordered,partiallyordered,orunordered,dependingonthemodelofcomputation.UnliketheDEmodel,allsignalshaveeventsatallclockticks,simplifyingthesimulatorbyrequiringnosorting.Simulatorsthatexploitthissimplificationarecalledcycle-basedorcycle-drivensimulators.Processingalleventsatagivenclocktickconstitutesacycle.Withinacycle,theorderinwhicheventsareprocessedmaybedeterminedbydataprecedences,whichdefinemicrosteps.Theseprecedencesarenotallowedtobecyclic,andtypicallyimposeapartialorder(leavingsomearbitraryorderingdecisionstothescheduler).Cycle-basedmodelsareexcellentforclockedsynchronouscircuitsandhavealsobeenappliedsuccessfullyatthesystemlevelincertainsignalprocessingapplications.

Acycle-basedmodelisinefficientformodelingsystemswhereeventsdonotoccuratthesamerateinallsignals.Whileconceptuallysuchsystemscanbemodeled(using,forexample,specialtokenstoindicatetheabsenceofanevent),thecostofprocessingsuchtokensisconsiderable.Fortunately,thecycle-basedmodeliseasilygeneralizedtomultiratesystems.Inthiscase,every

(a)

(b)

Fig.4.(a)Adataflowprocessnetworkand(b)asingle-processorstaticscheduleforit.

isbyunboundedFIFObuffering,andprocessesarecon-strainedtobecontinuousmappingsfrominputstreamstooutputstreams.“Continuous”inthisusageisatopologicalpropertythatensuresthattheprogramisdeterminate[13].Intuitively,itimpliesaformofcausalitywithouttime;specifically,aprocesscanusepartialinformationaboutitsinputstreamstoproducepartialinformationaboutitsoutputstreams.Addingmoretokenstotheinputstreamwillneverresultinhavingtochangeorremovetokensontheoutputstreamthathavealreadybeenproduced.Onewaytoensurecontinuityiswithblockingreads,whereanyaccesstoaninputstreamresultsinsuspensionoftheprocessiftherearenotokens.Oneconsequenceofblockingreadsisthataprocesscannottestaninputchannelfortheavailabilityofdataandthenbranchconditionallytoapointwhereitwillreadadifferentinput.

Indataflow,eachprocessisdecomposedintoasequenceoffirings,indivisiblequantaofcomputation.Eachfiringconsumesandproducestokens.Dividingprocessesintofiringsavoidsthemultitaskingoverheadofcontextswitch-ingindirectimplementationsofKahnprocessnetworks.Infact,inmanyofthesignalprocessingenvironments,amajorobjectiveistostatically(atcompiletime)scheduletheactorfirings,achievinganinterleavedimplementationoftheconcurrentmodelofcomputation.Thefiringsareorganizedintoalist(foroneprocessor)orsetoflists(formultipleprocessors).Fig.4(a)showsadataflowgraph(DFG),andFig.4(b)showsasingleprocessorscheduleforit.Thisscheduleisalistoffiringsthatcanberepeatedindefinitely.Onecyclethroughthescheduleshouldreturnthegraphtoitsoriginalstate(here,stateisdefinedasthenumberoftokensoneacharc).Thisisnotalwayspossible,butwhenitis,considerablesimplificationresults[32].Inmanyexistingenvironments,whathappenswithinafiringcanonlybespecifiedinahostlanguagewithimperativesemantics,suchasCorC

answertothestateexplosionproblemplaguingFSM-basedverificationtechniques.

C.Languages

Thedistinctionbetweenalanguageanditsunderlyingmodelofcomputationisimportant.Thesamemodelofcomputationcangiverisetofairlydifferentlanguages(e.g.,theimperativeAlgol-likelanguagesC,C

Table2AComparisonofCo-SimulationMethods

HardwareSimulationlogiccustomlogiccommerciallogiccommerciallogiccommerciallogiccommercialcycle-basedlogiccustomlogiccustomlogiccustomlogiccommercial

SoftwareSimulationbus-cyclecustomhost-compiledhost-compiledhost-compiledhost-compiledcycle-countinghost-compiledISA

host-compiled

ISAonHWsimulation

SynchronizationMechanismsinglesimulationhandshakehandshakehandshakehandshake

taggedmessagessinglesimulationsinglesimulationsinglesimulationsinglesimulation

AuthorGupta[56]Rowson[57]Wilson[58]Thomas[59]

tenHagen(1)[60]tenHagen(2)[60]Kalavade(1)[61]Kalavade(2)[61]Lee[61]

Suterwala[62]

Thebasicco-simulationproblemisreconcilingtwoap-parentlyconflictingrequirements:

•toexecutethesoftwareasfastaspossible,oftenonahostmachinethatmaybefasterthanthefinalembeddedCPUandcertainlyisverydifferentfromit;and

•tokeepthehardwareandsoftwaresimulationssyn-chronized,sothattheyinteractjustastheywillinthetargetsystem.

Oneapproach,oftentakeninpractice,istouseageneral-purposesoftwaresimulator(e.g.,basedonVHDLorVer-ilog)tosimulateamodelofthetargetCPU,executingthesoftwareprogramonthissimulationmodel.Differentmodelscanbeemployed,withatradeoffbetweenaccuracyandperformance.

•Gate-levelmodels.Theseareviableonlyforsmallvalidationproblems,whereeithertheprocessorisasimpleone,orverylittlecodeneedstoberunonit,orboth.

•Instruction-setarchitecture(ISA)modelsaugmentedwithhardwareinterfaces.AnISAmodelisastandardprocessorsimulator(oftenwritteninC)augmentedwithhardwareinterfaceinformationforcouplingtoastandardlogicsimulator.

•Bus-functionalmodels.Thesearehardwaremodelsonlyoftheprocessorinterface;theycannotrunanysoftware.Instead,theyareconfigured(programmed)tomaketheinterfaceappearasifsoftwarewererunningontheprocessor.Astochasticmodeloftheprocessorandoftheprogramcanbeusedtodeterminethemixofbustransactions.

•Translation-basedmodels.Theseconvertthecodetobeexecutedonaprocessorintocodethatcanbeexecutednativelyonthecomputerdoingthesimula-tion.Preservingtiminginformationandcouplingthetranslatedcodetoahardwaresimulatorarethemajorchallenges.

Whenmoreaccuracyisrequiredandacceptablesimula-tionperformanceisnotachievableonstandardcomputers,designerssometimesresorttoemulation.Inthiscase,configurablehardwareemulatesthebehaviorofthesystembeingdesigned.

Anotherproblemistheaccuratemodelingofacontrolledelectromechanicalsystem,whichisgenerallygovernedbyasetofdifferentialequations.Thisoftenrequiresinterfacingtoanentirelydifferentkindofsimulator.

1)Co-SimulationMethods:Inthissection,wepresentasurveyofsomeoftherepresentativeco-simulationmethods,summarizedinTable2.Aunifiedapproach,wheretheentiresystemistranslatedintoaformsuitableforasinglesimulator,isconceptuallysimple,butcomputationallyinef-ficient.Makingbetteruseofcomputationalresourcesoftenmeansdistributingthesimulation,butsynchronizationoftheprocessesbecomesachallenge.

ThemethodproposedbyGuptaetal.[56]istypicaloftheunifiedapproachtoco-simulation.Itreliesonasinglecustomsimulatorforhardwareandsoftwarethatusesasingleeventqueueandahigh-level,bus-cyclemodelofthetargetCPU.

Rowson[57]takesamoredistributedapproachthatlooselylinksahardwaresimulatorwithasoftwareprocess,synchronizingthemwiththestandardinterprocesscom-municationmechanismsofferedbythehostoperatingsys-tem.Oneoftheproblemswiththisapproachisthattherelativeclocksofsoftwareandhardwaresimulationarenotsynchronized.Thisrequirestheuseofhandshakingprotocols,whichmayimposeanundueburdenontheimplementation.Thismayhappen,forexample,becausehardwareandsoftwarewouldnotneedsuchhandshakingsincethehardwarepartrunsinrealitymuchfasterthaninthesimulation.

Wilson[58]describestheuseofacommercialhardwaresimulator.Inthisapproach,thesimulatorandsoftwarecompiledonthehostprocessorinteractviaabus-cycleemulatorinsidethehardwaresimulator.ThesoftwareandhardwaresimulatorexecuteinseparateprocessesandthetwocommunicateviaUNIXpipes.Thomasetal.[59]takeasimilarapproach.

Anotherapproachkeepstrackoftimeinsoftwareandhardwareindependently,usingvariousmechanismstosyn-chronizethemperiodically.Forexample,tenHagenetal.[60]describeatwo-levelco-simulationenvironmentthatcombinesatimedanduntimedlevel.Theuntimedlevelisusedtoverifytime-independentpropertiesofthesystem,suchasfunctionalcorrectness.Atthislevel,softwareandhardwarerunindependentofeachother,passingmessageswheneverneeded.Thisallowsthesimulationtorunatthemaximumspeed,whiletakingfulladvantageofthenativedebuggingenvironmentsbothforsoftwareandfor

377

EDWARDSetal.:DESIGNOFEMBEDDEDSYSTEMS:FORMALMODELS,VALIDATION,ANDSYNTHESIS

hardware.Thetimedlevelisusedtoverifytime-dependentproperties,requiringthedefinitionoftimeinhardwareandsoftware.Inhardware,timecanbemeasuredeitheronthebasisofclockcycles(cycle-basedsimulation,assumingsynchronousoperation)formaximumperformance,oronthebasisofestimatedorextractedtiminginformationformaximumprecision.Insoftware,ontheotherhand,timecanbemeasuredeitherbyprofilingorclockcyclecountinginformationformaximumperformance,orbyexecutingamodeloftheCPUformaximumprecision.Theauthorsproposetwobasicmechanismsforsynchronizingtimeinhardwareandsoftware.

1)Softwareisthemasterandhardwareistheslave.Inthiscase,softwaredecideswhentosendamessage,taggedwiththecurrentsoftwareclockcycle,tothehardwaresimulator.Dependingontherelationbetweensoftwareandhardwaretime,thehardwaresimulatorcaneithercontinuesimulationuntilsoft-waretimeorback-upthesimulationtosoftwaretime(thisrequirescheckpointingcapabilities,whichfewhardwaresimulatorscurrentlyhave).

2)Hardwareisthemasterandsoftwareistheslave.Inthiscase,thehardwaresimulatordirectlycallscommunicationprocedureswhich,inturn,callusersoftwarecode.KalavadeandLee[61]andLeeandRabaey[63]takeasimilarapproach.ThesimulationanddesignenvironmentPtolemy[14]isusedtoprovideaninterfacingmechanismbetweendifferentdomains.InPtolemy,objectsdescribedatdifferentlevelsofabstractionandusingdifferentsemanticmodelsarecomposedhierarchically.Eachabstractionlevel,withitsownsemanticmodel,isa“domain”(e.g.,dataflow,DE).Atomicobjects(called“stars”)aretheprimitivesofthedomain(e.g.,dataflowoperators,logicgates).Theycanbeusedeitherinsimulationmode(reactingtoeventsbyproducingevents)orinsynthesismode(producingsoftwareorahardwaredescription).“Galaxies”arecollectionsofinstancesofstarsorothergalaxies.Aninstantiatedgalaxycanbelongtoadomaindifferentthantheinstantiatingdo-main.Eachdomainincludesascheduler,whichdecidestheorderinwhichstarsareexecuted,bothinsimulationandinsynthesis.Forsynthesis,itmustbepossibletoconstructtheschedulestatically.Wheneveragalaxyinstantiatesagalaxybelongingtoanotherdomain(typicalinco-simulation),Ptolemyprovidesamechanismcalleda“wormhole”forthetwoschedulerstocommunicate.Thesimplestformofcommunicationistopasstime-stampedeventsacrosstheinterfacebetweendomains,withtheappropriatedata-typeconversion.

KalavadeandLee[61]performco-simulationatthespecificationlevelbyusingadataflowmodelandattheimplementationlevelbyusinganISAprocessormodelaugmentedwiththeinterfaceswithinahardwaresimulator,bothbuiltwithinPtolemy.

LeeandRabaey[63]simulatethespecificationbyusingconcurrentprocessescommunicatingviaqueueswithin

378

atimedmodel(thePtolemycommunicatingprocessesdomain).Thesamemessageexchangingmechanismisretainedintheimplementation(usingamixofmicroprocessor-basedboards,DSP’s,andASIC’s),thusperformingco-simulationofonepartoftheimplementationwithasimulationmodeloftherest.Forexample,thesoftwarerunningonthemicroprocessorcanalsoberunonahostcomputer,whiletheDSPsoftwarerunsontheDSPitself.

SutarwalaandPaulin[62]describeanenvironmentcou-pledwitharetargetablecompiler[64]forcycle-basedsimulationofauser-definableDSParchitecture.TheuseronlyprovidesadescriptionoftheDSPstructureandfunctionality,whiletheenvironmentgeneratesabehavioralbus-cycleVHDLmodelforit,whichcanthenbeusedtorunthecodeonastandardhardwaresimulator.B.FormalVerification

Formalverificationistheprocessofmathematicallycheckingthatthebehaviorofasystem,describedusingaformalmodel,satisfiesagivenproperty,alsodescribedusingaformalmodel.Thetwomodelsmayormaynotbethesame,butmustshareacommonsemanticinterpretation.Theabilitytocarryoutformalverificationisstronglyaffectedbythemodelofcomputation,whichdeterminesdecidabilityandcomplexitybounds.Twodistincttypesofverificationarise.

•SpecificationVerification:checkinganabstractprop-ertyofahigh-levelmodel.Anexample:checkingwhetheraprotocolmodeledasanetworkofcommu-nicatingFSM’scaneverdeadlock.

•ImplementationVerification:checkingifarelativelylow-levelmodelcorrectlyimplementsahigher-levelmodelorsatisfiessomeimplementation-dependentproperty.Forexample:checkingwhetherapieceofhardwarecorrectlyimplementsagivenFSM,orwhetheragivendataflownetworkimplementationonagivenDSPcompletelyprocessesaninputsamplebeforethenextonearrives.

Implementationverificationforhardwareisarelativelywell-developedarea,withthefirstindustrial-strengthprod-uctsbeginningtoappear.Forexample,mostlogicsynthesissystemshaveamechanismtoverifyagate-levelimplemen-tationagainstasetofBooleanequationsoranFSM,todetectbugsinthesynthesissoftware.8

Whilesimulationcouldfallunderthesedefinitions(ifthepropertyis“thebehaviorunderthisstimulusisasexpected”),thetermformalverificationisusuallyreservedforcheckingpropertiesofthesystemthatmustholdforallorabroadclassofinputs.Thepropertiesaretraditionallybrokenintotwoclasses:

•safetyproperties,whichstatethatnomatterwhatinputsaregiven,andnomatterhownondetermin-isticchoicesareresolvedinsidethesystemmodel,thesystemwillnotgetintoaspecificundesirable

8This

showsthattheneedforimplementationverificationisnot

eliminatedbytheintroductionofautomatedsynthesistechniques.

PROCEEDINGSOFTHEIEEE,VOL.85,NO.3,MARCH1997

configuration(e.g.,deadlock,emissionofundesiredoutputs,etc.);

•livenessproperties,whichstatethatsomedesiredcon-figurationwillbevisitedeventuallyorinfinitelyoften(e.g.,expectedresponsetoaninput,etc.)

Morecomplexchecks,suchasthecorrectimplementationofaspecification,canusuallybedoneintermsofthoseba-sicproperties.Forexample,Dill[65]describesamethodtodefineandcheckcorrectimplementationforasynchronouslogiccircuitsinanautomata-theoreticframework.

Inthissectionweonlysummarizethemajorapproachesthathavebeenorcanbeappliedtoembeddedsystemver-ification.Thesecanberoughlydividedintothefollowingclasses.

•Theoremprovingmethodsprovideanenvironmentthatassiststhedesignerincarryingoutaformalproofofspecificationorimplementationcorrectness.Theassistancecanbeeitherintheformofcheckingthecorrectnessoftheproof,orinperformingsomestepsoftheproofautomatically(e.g.,GordonandMelham’sHOL[66],theBoyer–Mooresystem[67],andPVS[68]).Themainproblemswiththisapproacharetheundecidabilityofsomehigherorderlogicsandthelargesizeofthesearchspaceevenfordecidablelogics.•FAmethodsrestrictthepowerofthemodelinordertoautomateproofs.Afiniteautomaton,initssimplestform,consistsofasetofstates,connectedbyasetofedgeslabeledwithsymbolsfromanalphabet.Variouscriteriacanbeusedtodefinewhichfiniteorinfinitesequencesofsymbolsare“accepted”bytheautomaton.Thesetofacceptedsequencesisgenerallycalledthelanguageoftheautomaton.Themainverificationmethodsusedinthiscasearelanguagecontainmentandmodelchecking.

a)

Inlanguagecontainment,boththesystemandthepropertytobeverifiedaredescribedasasynchronouscompositionofautomata.Theproofiscarriedoutbytestingwhetherthelanguageofoneiscontainedinthelanguageoftheother(Kurshan’sapproachistypical[53]).Oneparticularlysimplecaseoccurswhencom-paringasynchronousFSMwithitshardwareimplementation.Thenbothautomataareonfinitestrings,andtheproofofequivalencecanbeperformedbytraversingthestatespaceoftheirproduct[69].

Simulationrelationsareanefficientsufficient(i.e.,conservative)criteriontoestablishlanguagecontainmentpropertiesbetweenau-tomata,originatingfromtheprocessalgebraiccommunity[47],[46].Informally,asimulationrelationisarelation

,foreachsymbollabelingan

edgefrom

.Thisrelationcan

becomputedmuchmorequicklythanthe

c)

exactlanguagecontainmenttest(thatinthecaseofnondeterministicautomatarequiresanexponentialdeterminizationstep),andhencecanbeusedasafastheuristiccheck.

Ifthesamesimulationrelationholdsinbothdirections(i.e.,itistruealsoforeachsymbollabelinganedgefrom),thenitiscalledabisimulation.Bisimulationcanbeusedastestforbehavioralequivalencethatdirectlysupportscompositionandabstraction(hidingofedgelabels).Moreover,self-bisimulationisanequivalencerelationamongstatesofanautomaton,andhenceitcanbeusedtominimizetheautomaton(theresultiscalledthe“quotient”automaton).

Inmodelchecking[70],[71],[54],[6],thesystemismodeledasasynchronousorasyn-chronouscompositionofautomata,andthepropertyisdescribedasaformulainsometemporallogic[72],[73].Theproofisagaincarriedoutbytraversingthestatespaceoftheautomatonandmarkingthestatesthatsatisfytheformula.

b)

•Infiniteautomatamethodscandealwithinfinitestatespaceswhensomeminimizationtoafiniteformispossible.Oneexampleofthisclassaretheso-calledtimedautomata[74],inwhichasetofreal-valuedclocksisusedtomeasuretime.Severerestrictionsareapplied,inordertomakethismodeldecidable.Clockscanonlybetested,started,andresetaspartoftheedgelabelsofafiniteautomaton.Also,clockscanonlybecomparedagainstintegervaluesandinitializedtointegervalues.Inthiscase,itispossibletoshowthatonlyafinitesetofequivalenceclassrepresentativesissufficienttorepresentexactlythebehaviorofthetimedautomaton[75],[74].McManisandVaraiya[76]introducedthenotionofsuspension,whichextendstheclassofsystemsthatcanbemodeledwithvariationsoftimedautomata.Itisthenpossible,inprinciple,toverifytimingconstraintsatisfactionbyusingpreemptivescheduling,whichallowsalow-priorityprocesstobestoppedinthemiddleofacomputationbyahigh-priorityone.

ThemainobstaclestothewidespreadapplicationofFA-basedmethodsaretheinherentcomplexityoftheproblem,andthedifficultyfordesigners,generallyaccustomedtosimulation-basedmodels,toformallymodelthesystemoritsproperties.Thesynchronouscompositionofautomata,whichisthebasisofallknownautomata-basedmethods,isinherentlysensitivetothenumberofstatesinthecomponentautomata,sincethesizeofthetotalstatespaceistheproductofthesizesofthecomponentstatespaces.Abstractionisthemostpromisingtechniquetotacklethisproblem,generallyknownasstate-spaceexplosion.Abstractionreplaces(generallyrequiringextensiveuserin-tervention)somesystemcomponentswithsimplerversions,exhibitingnondeterministicbehavior.Nondeterminismis

379

EDWARDSetal.:DESIGNOFEMBEDDEDSYSTEMS:FORMALMODELS,VALIDATION,ANDSYNTHESIS

usedtoreducethesizeofthestatespacewithoutlosingthepossibilityofverifyingthedesiredproperty.Thebasicideaistobuildprovablyconservativeapproximationsoftheexactbehaviorofthesystemmodel,suchthatthecomplexityoftheverificationislower,butnofalsepositiveresultsarepossible.Forexample,theverificationsystemmaysaythattheapproximatemodeldoesnotsatisfytheproperty,whiletheoriginalonedid,thusrequiringabetterapproximation,butitwillneversaythattheapproximatemodelsatisfiestheproperty,whiletheoriginalonedidnot[75],[77],[78].Thequotientwithrespecttobisimulationcanalsobeusedinplaceofeverycomponent,thusprovidinganothermechanism(withoutfalsenegativeresults)tofightspaceexplosion.

Thesystematicapplicationofformalverificationtech-niquessincetheearlystagesofadesignmayleadtoanewdefinitionof“optimal”sizeforamodule(apartfromthosecurrentlyinuse,thataregenerallyrelatedtohumanunderstanding,synthesisorcompilation).A“good”leaf-levelmodulemustbesmallenoughtoadmitverification,andlargeenoughtopossessinterestingverifiableproperties.Thepossibilityofmeaningfullyapplyingabstractionwouldalsodeterminetheappropriatesizeandcontentsofmodulesattheupperlevelsofthehierarchy.

Anotherinterestingfamilyofformalverificationtech-niques,usefulforheterogeneoussystemswithmultipleconcurrentagents,isbasedonthenotionofpartialorderingbetweencomputationsinanexecutionofaprocessnetwork.Directuseofavailableconcurrencyinformationcanbeusedduringtheverificationprocesstoreducethenumberofexplicitlyexploredstates[6],[51],[50].Somesuchmethodsarebasedontheso-called“Mazurkiewicztraces,”inwhicha“trace”isanequivalenceclassofsequencesofstatetransitionswhereconcurrenttransitionsarepermuted[79],[80].

Modelcheckingandlanguagecontainmenthavebeenespeciallyusefulinverifyingthecorrectnessofprotocols,whichareparticularlywell-suitedtothefiniteautomatonmodelduetotheirrelativedataindependence.Onemayclaimthatthesetwo(closelyrelated)paradigmsrepresentabouttheonlysolutionstothespecificationverificationproblemthatarecurrentlyclosetoindustrialapplicability,thanksto:

•Thedevelopmentofextremelyefficientimplicitrep-resentationmethodsforthestatespace,basedonBinaryDecisionDiagrams[81],[69],thatdonotneedtorepresentandstoreeveryreachablestateofthemodeledsystemexplicitly.

•Thegooddegreeofautomation,atleastofthepropertysatisfactionorlanguagecontainmentchecksthem-selves(onceasuitableabstractionhasbeenfoundbyhand).

•Thegoodmatchbetweentheunderlyingsemantics(state-transitionobjects)andthefinite-statebehaviorofdigitalsystems.

Theverificationproblembecomesmuchmoredifficultwhenonemusttakeintoaccounteithertheactualvalueof

380

dataandtheoperationsperformedonthem,orthetimingpropertiesofthesystem.Thefirstproblemcanbetackledbyfirstassumingequalityofarithmeticfunctionswiththesamenameusedatdifferentlevelsofmodeling(e.g.,specificationandimplementation[82])andthenseparatelyverifyingthatagivenpieceofhardwareimplementscorrectlyagivenarithmeticfunction[83].Thetimingverificationproblemforsequentialsystems,ontheotherhand,stillneedstobeformulatedinawaythatpermitsthesolutionofpracticalproblemsinareasonableamountofspaceandtime.Onepossibility,proposedalmostsimultaneously[84]and[85],istoincrementallyaddtimingconstraintstoaninitiallyuntimedmodel,ratherthanimmediatelybuildingthefull-blowntimedautomaton.Thisadditionshouldbedoneiteratively,tograduallyeliminateall“false”violationsofthedesiredpropertiesduetothefactthatsometimingpropertiesofthemodelhavebeenignored.Theiterationcanbeshowntoconverge,butthespeedofconvergencestilldependsheavilyontheingenuityofthedesignerinproviding“hints”totheverificationsystemaboutthenexttiminginformationtoconsider.

Aswithmanyyoungtechnologies,optimismaboutver-ificationtechniquesinitiallyledtoexcessiveclaimsabouttheirpotential,particularlyintheareaofsoftwareverifi-cation,wheretheterm“provingprograms”wasbroadlytouted.Formanyreasons,includingtheundecidabilityofmanyverificationproblemsandthefactthatverificationcanonlybeasgoodasthepropertiesthedesignerspecifies,thisoptimismhasbeenmisplaced.Berryhassuggestedusingtheterm“automaticbugdetection”inplaceof“verification”tounderscorethatitistoomuchtohopeforaconclusiveproofofanynontrivialdesign.Instead,thegoalofverificationshouldbeatechnologythatwillhelpdesignerspreventingproblemsindeployedsystems.IV.SYNTHESIS

By“synthesis,”wemeanbroadlyastageinthedesignrefinementwhereamoreabstractspecificationistranslatedintoalessabstractspecification,assuggestedinFig.2.Forembeddedsystems,synthesisisacombinationofmanualandautomaticprocesses,andisoftendividedintothreestages:mappingtoarchitecture,inwhichthegeneralstruc-tureofanimplementationischosen;partitioning,inwhichthesectionsofaspecificationareboundtothearchitecturalunits;andhardwareandsoftwaresynthesis,inwhichthedetailsoftheunitsarefilledout.

Weinformallydistinguishbetweensoftwaresynthesisandsoftwarecompilation,accordingtothetypeofinputspecification.ThetermsoftwarecompilationisgenerallyassociatedwithaninputspecificationusingC-orPascal-likeimperative,generallynonconcurrent,languages.Theselanguageshaveasyntaxandsemanticsthatisveryclosetothatoftheimplementation(assemblyorexecutablecode).Insomesense,theyalreadydescribe,atafairlydetailedlevel,thedesiredimplementationofthesoftware.Wewillusethetermsoftwaresynthesistodenoteanoptimizedtranslationprocessfromahigh-levelspecificationthat

PROCEEDINGSOFTHEIEEE,VOL.85,NO.3,MARCH1997

describesthefunctionthatmustbeperformed,ratherthanthewayinwhichitmustbeimplemented.Examplesofsoftwaresynthesiscanbe,forexample,theCorassemblycodegenerationcapabilitiesofdigitalsignalprocessinggraphicalprogrammingenvironmentssuchasPtolemy[86],ofgraphicalFSMdesignenvironmentssuchasStateCharts[87],orofsynchronousprogrammingenvironmentssuchasEsterel,Lustre,andSignal[5].

Recently,higherandhigherlevelsynthesisapproacheshavestartedtoappear.Oneparticularlypromisingtech-niqueforembeddedsystemsissupervisorycontrol,pio-neeredbyRamadgeandWonham[88].Whilemostsyn-thesismethodsstartfromanexplicitmodelofhowthesystemthatisbeingdesignedmustbehave,supervisorycontroldescribeswhatitmustachieve.Itcleverlycombinesaclassicalcontrolsystemviewoftheworldwithautomata-theoretictechniques,tosynthesizeacontrolalgorithmthatis,insomesense,optimum.

Supervisorycontroldistinguishesbetweentheplant(anabstractionofthephysicalsystemthatmustbecontrolled)andthecontroller(theembeddedsystemthatmustbesynthesized).Givenafinite-automatonmodeloftheplant(possiblyincludinglimitationsonwhatacontrollercando)andoftheexpectedbehaviorofthecompletesystem(plantpluscontroller),itispossibletodetermine:

•ifafinite-statecontrollersatisfyingthatspecificationexists,and

•a“best”finite-statecontroller,undersomecostfunc-tion(e.g.,minimumestimatedimplementationcost).Recentpapersdealingwithvariationsonthisproblemare[89]and[90].

A.MappingfromSpecificationtoArchitecture

Theproblemofarchitectureselectionand/ordesignisoneofthekeyaspectsofthedesignofembeddedsystems.Supportingthedesignerinchoosingtherightmixofcomponentsandimplementationtechnologiesisessentialtothesuccessofthefinalproduct,andhenceofthemethod-ologythatwasusedtodesignit.Generallyspeaking,themappingproblemtakesasinputafunctionalspecificationandproducesasoutputanarchitectureandanassignmentoffunctionstoarchitecturalunits.

Anarchitectureisgenerallycomposedof:

•hardwarecomponents(e.g.,microprocessors,mi-crocontrollers,memories,I/Odevices,ASIC’s,andFPGA’s),

•softwarecomponents(e.g.,anoperatingsystem,devicedrivers,procedures,andconcurrentprograms),and•interconnectionmedia(e.g.,abstractchannels,busses,andsharedmemories).

Partitioningdetermineswhichpartsofthespecificationwillbeimplementedonthesecomponents,whiletheiractualimplementationwillbecreatedbysoftwareandhardwaresynthesis.

Thecostfunctionoptimizedbythemappingprocessincludesamixtureoftime,area,componentcost,andpowerconsumption,wheretherelativeimportancedepends

heavilyonthetypeofapplication.Timecostmaybemeasuredeitherasexecutiontimeforanalgorithm,orasmisseddeadlinesforasoftreal-timesystem.9Areacostmaybemeasuredaschip,board,ormemorysize.Thecomponentsofthecostfunctionmaytaketheformofahardconstraintoraquantitytobeminimized.

Currentsynthesis-basedmethodsalmostinvariablyim-posesomerestrictionsonthetargetarchitectureinordertomakethemappingproblemmanageable.Forexample,thearchitecturemaybelimitedtoalibraryofpre-definedcomponentsduetovendorrestrictionsorinterfacingcon-straints.Fewpapershavebeenpublishedonautomatingthedesignof,say,amemoryhierarchyoranI/Osubsystembasedonstandardcomponents.Notableexceptionstothisrulearepapersdealingwithretargetablecompilation[91],orwithaveryabstractformulationofpartitioningforco-design[92]–[95].Thestructureoftheapplication-specifichardwarecomponents,ontheotherhand,isgenerallymuchlessconstrained.

Often,thecommunicationmechanismsarealsostan-dardizedforagivenmethodology.Fewchoices,oftencloselytiedtothecommunicationmechanismusedatthespecificationlevel,areofferedtothedesigner.Nonetheless,someworkhasbeendoneonthedesignofinterfaces[96].B.Partitioning

Partitioningisaproblemwithanydesignusingmorethanonecomponent.Itisaparticularlyinterestingprob-leminembeddedsystemsbecauseoftheheterogeneoushardware/softwaremixture.Partitioningmethodscanbeclassified,asshowninTable3,accordingtofourmaincharacteristics:1)thespecificationmodel(s)supported,2)thegranularity,3)thecostfunction,and4)thealgorithm.Exploredalgorithmclassesincludegreedyheuristics,clusteringmethods,iterativeimprovement,andmathemat-icalprogramming.

Sofar,thereseemstobenoclearwinneramongparti-tioningmethods,partlyduetotheearlystageofresearchinthisarea,andpartlyduetotheintrinsiccomplexityoftheproblem,whichseemstoprecludeanexactformulationwitharealisticcostfunctioninthegeneralcase.

Ernstetal.[110],[111],[97]useagraph-basedmodel,withnodescorrespondingtoelementaryoperations(state-mentsinC

Table3AComparisonofPartitioningMethods

Model

CDFG(C*)HDLset-basedtasklistacyclicDFGUnity(HDL)OccamacyclicDFGHDL(?)VHDL

Ruby(HDL)

CDFG(HDL,C)

communicatingprocessesFSM’s

timingdiagramCDFG(HDL)

Granularityoperationtasktasktask

operationoperationoperationhierarchyoperationtasktask

operationhierarchyoperationtasktask

operationoperation

CostFunction

profiling(SW)

synthesisandsimilarity(HW)communicationcostprofiling(SW)synthesis(HW)profiling

profilingschedulinganalysisprofiling(SW)

processorcost(HW)communicationcostsimilarity

concurrent/sequencesimilarity

concurrence/sequenceschedulabilityprofiling(SW)synthesis(HW)profiling

ratematchingprofiling??

time(SW)area(HW)time

Algorithm

hand(outer)

simulatedannealing(inner)KernighanandLinmathematicalprogrammingbranchandboundmixed

integer-linearprogrammingclusteringclustering

heuristicwithlook-aheadhand

simulatedannealinghandhandhandhandmin-cutheuristic

AuthorHenkel[97]Olokutun[98]Kumar[93]Hu[99]Vahid[95]Barros(1)[100]Barros(2)[101]Kalavade[102]Adams[103]Eles[104]Luk[105]Steinhausen[106]BenIsmail[107]Antoniazzi[108]Chou[96]Gupta[56],[109]

closeness(thesimilarities,e.g.,anaddandasubtractareclose);

•byestimatingthecommunicationoverheadincurredwhenblocksaremovedacrosspartitions.Thisisapproximatedbythe(static)numberofdataitemsex-changedamongpartitions,assumingasimplememory-mappedcommunicationmechanismbetweenhardwareandsoftware.

Partitioningisdoneintwoloops.Theinnerloopusessimulatedannealing,withaquickestimationofthegainderivedbymovinganoperationbetweenhardwareandsoftware,toimproveaninitialpartition.Theouterloopusessynthesistorefinetheestimatesusedintheinnerloop.Olokutunetal.[98]performperformance-drivenparti-tioningworkingonablock-by-blockbasis.Thespecifica-tionmodelisahardwaredescriptionlanguage.Thisallowsthemtousesynthesisforhardwarecostestimation,andprofilingofacompiled-codesimulatorforsoftwarecostestimation.Partitioningisdonetogetherwithscheduling,sincetheoverallgoalistominimizeresponsetimeinthecontextofusingemulationtospeedupsimulation.Aninitialpartitionisobtainedbyclassifyingblocksaccordingtowhethertheyaresynthesizable,andwhetherthecommu-nicationoverheadjustifiesahardwareimplementation.Thisdeterminessomeblockswhichmusteithergointosoftwareorhardware.Uncommittedblocksareassignedtohardwareorsoftwarestartingfromtheblockwhichhasmosttogainfromaspecificchoice.TheinitialpartitionisthenimprovedbyaKernighanandLin-likeiterativeswappingprocedure.Kumaretal.[92],[93],ontheotherhand,considerpartitioninginaverygeneralandabstractform.Theyuseacomplex,set-basedrepresentationofthesystem,itsvariousimplementationchoicesandthevariouscosts

382

associatedwiththem.Costattributesaredeterminedmainlybyprofiling.Thesystembeingdesignedisrepresentedbyfoursets:availablesoftwarefunctions;hardwareresources;communicationsbetweenthe(softwareand/orhardware)units;andfunctionstobeimplemented,eachofwhichcanbeassignedasetofsoftwarefunctions,hardwareresourcesandcommunications.Thismeansthatthegivensoftwarerunsonthegivenhardwareandusesthegivencommunica-tionstoimplementthefunction.Thepartitioningprocessisfollowedbyadecompositionofeachfunctionintovirtualinstructionsets,followedbydesignofanimplementationforthesetusingtheavailableresources,andfollowedagainbyanevaluationphase.

D’Ambrosioetal.[112],[99]tackletheproblemofchoosingasetofprocessorsonwhichasetofcooperatingtaskscanbeexecutedwhilemeetingreal-timeconstraints.Theyalsouseamathematicalformulation,butprovideanoptimalsolutionprocedurebyusingbranch-and-bound.Thecostofasoftwarepartitionisestimatedasalowerandanupperboundonprocessorutilization.Theupperboundisobtainedbyrate-monotonicanalysis[113],whilethelowerboundisobtainedbyvariousrefinementsofthesumoftaskcomputationtimesdividedbytaskperiods.Thebranch-and-boundprocedureusestheboundstoprunethesearchspace,whilelookingforoptimalassignmentsoffunctionstocomponents,andsatisfyingthetimingconstraints.Otheroptimizationcriteriacanbeincludedbesideschedulability,suchasresponsetimestotaskswithsoftdeadlines,hardwarecosts,andexpandability,whichfavorssoftwaresolutions.

Barrosetal.[100]useagraph-basedfine-grainedrepre-sentation,witheachunitcorrespondingtoasimplestate-mentintheUnityspecificationlanguage.Theyclusterunits

PROCEEDINGSOFTHEIEEE,VOL.85,NO.3,MARCH1997

accordingtoavarietyofsometimesvaguecriteria:similar-itybetweenunits,basedonconcurrency(controlanddataindependence),sequencing(controlordatadependence),mutualexclusion,andvectorizationofasequenceofrelatedassignments.Theyclustertheunitstominimizethecostofcutsintheclusteringtree,andthenimprovetheclusteringbyconsideringpipeliningopportunities,allocationsdoneatthepreviousstage,andcostsavingsduetoresourcesharing.KalavadeandLee[102]useanacyclicdependencygraphderivedfromaDFGtosimultaneouslymapeachnode(task)tosoftwareorhardwareandscheduletheexecutionofthetasks.Theapproachisheuristic,andcangiveanapproximatesolutiontoverylargeprobleminstances.Toguidethesearchprocess,itusesbothcriticalpathinformationandthesuitabilityofanodetohardwareorsoftware.Forexample,bitmanipulationsarebettersuitedtohardwarewhilerandomaccessestoadatastructurearebettersuitedtosoftware.

Vahid,Gajskietal.[95],[114]performgraph-basedparti-tioningofavariable-grainedspecification.ThespecificationlanguageisSpecCharts,ahierarchicalmodelinwhichtheleavesare“states”ofahierarchicalStatecharts-likeFSM.These“states”cancontainarbitrarilycomplexbehavioralVHDLprocesses,writteninahigh-levelspecificationstyle.Costfunctionestimationisdoneattheleaflevel.EachlevelisassignedanestimatednumberofI/Opins,anestimatedarea(basedonperformingbehavioral,RTL,andlogicsynthesisinisolation),andanestimatedexecutiontime(obtainedbysimulatingthatinitialimplementation,andconsideringcommunicationdelayaswell).Theareaestimatecanbechangedifmoreleavesaremappedontothesamephysicalentity,duetopotentialsharing.Thecostmodelisattachedtoagraph,inwhichnodesrepresentleavesandedgesrepresentcontrol(activation/deactivation)anddata(communication)dependencies.Classicalcluster-ingandpartitioningalgorithmsarethenapplied,followedbyarefinementphase.Duringrefinement,eachpartitionissynthesized,togetbetterareaandtimingestimates,and“peripheral”graphnodesaremovedamongpartitionsgreedilytoreducetheoverallcost.Thecostofagivenpartitionisasimpleweightedsumofarea,pin,chipcount,andperformanceconstraintsatisfactionmeasures.

Steinhausenetal.[106],[91],[115]describeacompleteco-synthesisenvironmentinwhichacontroldataflowgraph(CDFG)representationisderivedfromanarrayofspecificationformats,suchasVerilog,VHDL,andC.TheCDFGispartitionedbyhand,basedontheresultsofprofiling,andthenmappedontoanarchitecturethatcanin-cludegeneral-purposemicroprocessors,application-specificinstructionprocessors(ASIP’s),software-programmablecomponentsdesignedadhocforanapplication,andASIC’s.Aninterestingaspectofthisapproachisthatthearchitectureitselfisnotfixed,butsynthesisisdrivenbyauser-definedstructuraldescription.ASICsynthesisisdonewithacommercialtool,whilesoftwaresynthesis,bothforgeneral-purposeandspecializedprocessors,isdonewithanexistingretargetablecompilerdevelopedbyHoogerbruggeetal.[116].

BenIsmailetal.[107]andVossetal.[117]startfromasystemspecificationdescribedinSDL[118].Thespecifica-tionisthentranslatedintotheSolarinternalrepresentation,basedonahierarchicalinterconnectionofcommunicatingprocesses.Processescanbemergedandsplit,andthehier-archycanbechangedbysplitting,movingandclusteringofsubunits.Thesequencingoftheseoperationsiscurrentlydonebytheuser.

Finally,Chouetal.[96]andWalkupandBorriello[119]describeaspecialized,scheduling-basedalgorithmforinterfacepartitioning.Thealgorithmisbasedonagraphmodelderivedfromaformalizedtimingdiagram.Nodesrepresentlow-leveleventsintheinterfacespecification.Edgesrepresentconstraints,andcaneitherbederivedfromcausalitylinksinthespecification,orbeaddedduringthepartitioningprocess(forexampletorepresenteventsthatoccuronthesamewire,andhenceshouldbemovedtogether).Thecostfunctionistimeforsoftwareandareaforhardware.Thealgorithmisbasedonamin-cutprocedureappliedtothegraph,inordertoreducecongestion.Congestioninthiscaseisdefinedassoftwarebeingrequiredtoproduceeventsmorerapidlythanthetargetprocessorcando,whichimpliestheneedforsomehardwareassistance.

C.HardwareandSoftwareSynthesis

Afterpartitioning(andsometimesbeforepartitioning,inordertoprovidecostestimates)thehardwareandsoftwarecomponentsoftheembeddedsystemmustbeimplemented.Theinputstotheproblemareaspecification,asetofresourcesandpossiblyamappingontoanarchitecture.Theobjectiveistorealizethespecificationwiththeminimumcost.

Generallyspeaking,theconstraintsandoptimizationcri-teriaforthissteparethesameasthoseusedduringpartitioning.Areaandcodesizemustbetradedoffagainstperformance,whichoftendominatesduetothereal-timecharacteristicsofmanyembeddedsystems.Costconsid-erationsgenerallysuggesttheuseofsoftwarerunningonoff-the-shelfprocessors,wheneverpossible.Thischoice,amongotherthings,allowsonetoseparatethesoftwarefromthehardwaresynthesisprocess,relyingonsomeformofpre-designedorcustomizedinterfacingmechanism.Oneexceptiontothisruleareauthorswhoproposethesimultaneousdesignofacomputerarchitectureandoftheprogramthatmustrunonit[120],[121],[115].Sincethedesignersofgeneral-purposeCPU’sfacedifferentproblemsthanthedesignersofembeddedsystems,wewillonlycon-siderthoseauthorswhosynthesizeanASIP[122],andthemicrocodethatrunsonit.Thedesignerofageneral-purposeCPUmustworryaboutbackwardcompatibility,compilersupport,andoptimalperformanceforawidevarietyofapplications,whereastheembeddedsystemdesignermustworryaboutadditionofnewfunctionalityinthefuture,userinteraction,andsatisfactionofaspecificsetoftimingconstraints.

NotethatbyusinganASIPratherthanastandardASIC,whichgenerallyhasverylimitedprogrammingcapabili-383

EDWARDSetal.:DESIGNOFEMBEDDEDSYSTEMS:FORMALMODELS,VALIDATION,ANDSYNTHESIS

Table4AComparisonofSoftwareSchedulingMethods

ModeltasklisttasklistInterfacenonesynthesized

ConstraintGranularity

task

task,operationSchedulingAlgorithmRMA(runtime)heuristic(static)

AuthorCochran[130]Chou[96]Gupta[109]CDFG?

Chiodo[131]tasklistsynthesized

Menez[120]

CDFG

?

ties,theembeddedsystemdesignercancouplesomeoftheadvantagesofhardwareandsoftware.Forexample,performanceandpowerconsumptioncanbeimprovedwithrespecttoasoftwareimplementationonageneral-purposemicrocontrollerorDSP,whileflexibilitycanbeim-provedwithrespecttoahardwareimplementation.Anothermethodtoachievethesamegoalistousereprogrammablehardware,suchasFPGA’s,whichcanbereprogrammedeitheroff-line(justlikeembeddedsoftwareisupgradedbychangingaROM),orevenon-line(tospeedupthealgorithmthatiscurrentlybeingexecuted).

ThehardwaresynthesistaskforASIC’susedinembed-dedsystems(whethertheyareimplementedonFPGA’sornot)isgenerallyperformedaccordingtotheclassicalhigh-levelandlogicsynthesismethods.Thesetechniqueshavebeenworkedonextensively;forexample,recentbooksbyDeMicheli[123],Devadasetal.[124],andCamposanoandWolf[125]describethemindetail.MarwedelandGoossens[126]presentagoodoverviewofcodegenerationstrategiesforDSP’sandASIP’s.

Thesoftwaresynthesistaskforembeddedsystems,ontheotherhand,isarelativelynewproblem.Tradition-ally,softwaresynthesishasbeenregardedwithsuspicion,mainlyduetoexcessiveclaimsmadeduringitsinfancy.Infact,theproblemismuchmoreconstrainedforem-beddedsystemscomparedtogeneral-purposecomputing.Forexample,embeddedsoftwareoftencannotusevirtualmemory,duetophysicalconstraints(e.g.,theabsenceofaswappingdevice),toreal-timeconstraints,andtotheneedtopartitionthespecificationbetweensoftwareandhardware.Thisseverelylimitstheapplicabilityofdynamictaskcreationandmemoryallocation.Forsomehighlycriticalapplicationseventheuseofastackmaybeforbidden,andeverythingmustbedealtwithbypollingandstaticvariables.Algorithmsalsotendtobesimpler,withacleardivisionintocooperatingtasks,eachsolvingonespecificproblem(e.g.,digitalfilteringofagiveninputsource,protocolhandlingoverachannel,andsoon).Inparticular,theproblemoftranslatingcooperatingfinite-statemachinesintosoftwarehasbeensolvedinanumberofways.

Softwaresynthesismethodsproposedintheliteraturecanbeclassified,asshowninTable4,accordingtothefollowing:1)thespecificationformalism,2)interfacingmechanisms(atthespecificationandtheimplementationlevels),3)whentheschedulingisdone,and4)thesched-ulingmethod.

Almostallsoftwaresynthesismethodsperformsomesortofscheduling—sequencingtheexecutionofasetoforiginallyconcurrenttasks.Concurrenttasksareanexcel-384

operationheuristicwithlook-ahead(static+runtime)

taskRMA(runtime)operation

exhaustive

lentspecificationmechanism,butcannotbeimplementedassuchonastandardCPU.Theschedulingproblem(reviewed,e.g.,byHalangandStoyenko[127])amountstofindingalinearexecutionorderfortheelementaryoperationscomposingthetasks,sothatallthetimingconstraintsaresatisfied.Dependingonhowandwhenthislinearizationisperformed,schedulingalgorithmscanbeclassifiedas

•static,whereallschedulingdecisionsaremadeatdesign-orcompile-time;

•quasistatic,wheresomeschedulingdecisionsaremadeatrun-time,someatcompile-time;

•dynamic,wherealldecisionaremadeatrun-time.Dynamicschedulerstakemanyforms,butinparticulartheyaredistinguishedaspreemptiveornonpreemptive,dependingonwhetherataskcanbeinterruptedatarbi-trarypoints.Forembeddedsystems,therearecompellingmotivationsforusingstaticorquasistaticscheduling,oratleastforminimizingpreemptiveschedulinginordertominimizeschedulingoverheadandtoimprovereliabilityandpredictability.Thereare,ofcourse,casesinwhichpreemptioncannotbeavoided,becauseitistheonlyfeasiblesolutiontotheprobleminstance[127],butsuchcasesshouldbecarefullyanalyzedtolimitpreemptiontoaminimum.

Manystaticschedulingmethodshavebeendeveloped.Mostsomehowconstructaprecedencegraphandthenapplyoradaptclassicalmethods.SeeBhattacharyyaetal.[32]andSihandLee[128],[129]asastartingpointforschedulingofDFG’s.

Manyapproachestosoftwaresynthesisforembeddedsystemsdividethecomputationintocooperatingtasksthatarescheduledatruntime.Thisschedulingcanbedoneeitherbyusingclassicalschedulingalgorithms,orbyde-velopingnewtechniquesbasedonabetterknowledgeofthedomain.Embeddedsystemswithfairlyrestrictedspecificationparadigmsareaneasiertargetforspecializedschedulingtechniquesthanfullygeneralalgorithmswritteninanarbitraryhigh-levellanguage.

Theformerapproachuses,forexample,ratemonotonicanalysis(RMA)[113]toperformschedulabilityanalysis.InthepureRMAmodel,tasksareinvokedperiodically,canbepreempted,havedeadlinesequaltotheirinvocationperiod,andsystemoverhead(contextswitching,interruptresponsetime,andsoon)isnegligible.ThebasicresultbyLiuandLaylandstatesthatunderthesehypotheses,ifagivensetoftaskscanbesuccessfullyscheduledbyastaticpriorityalgorithm,thenitcanbesuccessfullyscheduledbysortingtasksbyinvocationperiod,withthehighestprioritygiventothetaskwiththeshortestperiod.

PROCEEDINGSOFTHEIEEE,VOL.85,NO.3,MARCH1997

ThebasicRMAmodelmustbeaugmentedtobepractical.Severalresultsfromthereal-timeschedulingliteraturecanbeusedtodevelopaschedulingenvironmentsupportingprocesssynchronization,interruptserviceroutines,contextswitchingtime,deadlinesdifferentfromthetaskinvocationperiod,modechanges(whichmaycauseachangeinthenumberand/ordeadlinesoftasks),andparallelprocessors.Parallelprocessorsupportgenerallyconsistsofanalyzingtheschedulabilityofagivenassignmentoftaskstoproces-sors,providingthedesignerwithfeedbackaboutpotentialbottlenecksandsourcesofdeadlocks.

Chouetal.[96]advocatedevelopingnewtechniquesbasedonbetterknowledgeofthedomain.TheproblemtheyconsideristofindavalidscheduleofprocessesspecifiedinVerilogundergiventimingconstraints.Thisapproach,likethatofGuptaetal.describedbelow,andunlikeclassicaltask-basedschedulingmethods,cantakeintoaccountbothfine-grainedandcoarse-grainedtimingconstraints.ThespecificationstylechosenbytheauthorsusesVerilogconstructsthatprovidestructuredconcurrencywithwatchdog-stylepreemption.Inthisstyle,multiplecomputationbranchesarestartedinparallel,andsomeofthem(thewatchdogs)can“kill”othersuponoccurrenceofagivencondition.Asetof“saferecoverypoints”isdefinedforeachbranch,andpreemptionisallowedonlyatthosepoints.Timingconstraintsarespecifiedbyusingmodes,whichrepresentdifferent“states”forthecomputationasinSpecCharts,e.g.,initialization,normaloperation,anderrorrecovery.Constraintsontheminimumandmaximumtimeseparationbetweenevents(evenofthesametype,todescribeoccurrencerates)canbedefinedeitherwithinamodeoramongeventsindifferentmodes.SchedulingisperformedwithineachmodebyfindingacyclicorderofoperationswhichpreservesI/Oratesandtimingconstraints.Eachmodeistransformedintoanacyclicpartialorderbyunrolling,andpossiblysplitting(ifitcontainsparallelloopswithharmonicallyunrelatedrepetitioncounts).Thenthepartialorderislinearizedbyusingalongest-pathalgorithmtocheckfeasibilityandassignstarttimestotheoperations.

Thesamegroup[132]describesatechniqueforde-vicedriversynthesis,targetedtowardmicrocontrollerswithspecializedI/Oports.Ittakesasinputaspecificationofthesystemtobeimplemented,adescriptionofthefunctionandstructureofeachI/Oport(alistofbitsanddirections),andalistofcommunicationinstructions.Itcanalsoexploitspecializedfunctionssuchasparallel/serialandserial/parallelconversioncapabilities.Thealgorithmassignscommunicationsinthespecificationtophysicalentitiesinthemicrocontroller.Itfirsttriestousespe-cialfunctions,thenassignsI/Oports,andfinallyresortstothemoreexpensivememory-mappedI/Oforoverflowcommunications.Ittakesintoaccountresourceconflicts(e.g.,amongdifferentbitsofthesameport),andallocateshardwarecomponentstosupportmemory-mappedI/O.Theoutputofthealgorithmisanetlistofhardwarecomponents,initializationroutinesandI/Odriverroutinesthatcanbecalledbythesoftwaregenerationprocedurewheneveracommunicationbetweensoftwareandhardwaremusttakeplace.

Guptaetal.[56],[109]startedtheirworkonsoftwaresynthesisandschedulingbyanalyzingvariousimplementa-tiontechniquesforembeddedsoftware.Theirspecificationmodelisasetofthreads,extractedfromaCDFGde-rivedfromaC-likeHDLcalledHardware-C.Threadsareconcurrentloop-freeroutines,whichinvokeeachotherasabasicsynchronizationmechanism.Statementswithinathreadarescheduledstatically,atcompile-time,whilethreadsarescheduleddynamically,atrun-time.Byus-ingaconcurrentlanguageratherthanC,thetranslationproblembecomeseasier,andtheauthorscanconcentrateontheschedulingproblem,tosimulatetheconcurrencyofthreads.Theauthorscomparetheinherentadvantagesanddisadvantagesoftwomaintechniquestoimplementthreads:coroutinesandasinglecasestatement(inwhicheachbranchimplementsathread).Thecoroutine-basedapproachismoreflexible(coroutinescanbenested,e.g.,torespondtourgentinterrupts),butmoreexpensive(duetotheneedtoswitchcontext)thanthecase-basedapproach.Thesamegroup[133]developedaschedulingmethodforreactivereal-timesystems.Thecostmodeltakesintoaccounttheprocessortype,thememorymodel,andtheinstructionexecutiontime.Thelatterisderivedbottom-upfromtheCDFGbyassigningaprocessorandmemory-dependentcosttoeachleafoperationintheCDFG.Someoperationshaveanunboundedexecutiontime,becausetheyareeitherdata-dependentloopsorsynchronization(I/O)operations.TimingconstraintsarebasicallydatarateconstraintsonexternallyvisibleInput/Outputoperations.Bounded-timeoperationswithinaprocessarelinearizedbyaheuristicmethod(theproblemisknowntobeNP-complete).Thelinearizationprocedureselectsthenextoperationtobeexecutedamongthosewhosepredecessorshaveallbeenscheduled,accordingto:whetherornottheirimmediateselectionforschedulingcancausesometimingconstrainttobemissed,andameasureof“urgency”thatperformssomelimitedtimingconstraintlookahead.Unbounded-timeoperations,ontheotherhand,areimple-mentedbyacalltotheruntimescheduler,whichmaycauseacontextswitchinfavorofanothermoreurgentthread.Chiodoetal.[134]alsoproposeasoftwaresynthesismethodfromextendedasynchronousFSM’s,calledco-designfinitestatemachines(CFSM’s).Themethodtakesadvantageofoptimizationtechniquesfromthehardwaresynthesisdomain.Itusesamodelbasedonmultipleasyn-chronouslycommunicatingCFSM’s,ratherthanasingleFSM,enablingittohandlesystemswithwidelyvaryingdataratesandresponsetimerequirements.Tasksareorga-nizedwithdifferentprioritylevels,andscheduledaccordingtoclassicalrun-timealgorithmslikeRMA.ThesoftwaresynthesistechniqueisbasedonaverysimpleCDFG,representingthestatetransitionandoutputfunctionsoftheCFSM.ThenodesoftheCDFGcanonlybeoftwotypes:TESTnodes,whichevaluateanexpressionandbranchaccordingtoitsresult,andASSIGNnodes,whichevaluateanexpressionandassignitsresulttoavariable.

385

EDWARDSetal.:DESIGNOFEMBEDDEDSYSTEMS:FORMALMODELS,VALIDATION,ANDSYNTHESIS

TheauthorsdevelopamappingfromarepresentationsofthestatetransitionandoutputfunctionsusingBinaryDecisionDiagrams[81]totheCDFGform,andcanthususeabodyofwell-developedoptimizationtechniquestominimizememoryoccupationand/orexecutiontime.ThesimpleCDFGformpermitsalsoaneasyandrelativelyaccuratepredictionofsoftwarecostandperformance,basedoncostassignmenttoeachCDFGnode[135].Thecost(codeanddatamemoryoccupation)andperformance(clockcycles)ofeachnodetypecanbeevaluatedwithagooddegreeofaccuracy,basedonahandfulofsystem-specificparameters(e.g.,thecostofavariableassignment,ofanaddition,ofabranch).Theseparameterscanbede-rivedbycompilingandrunningafewcarefullydesignedbenchmarksonthetargetprocessor,oronacycle-accurateemulatororsimulator.

Liemetal.[64]tackleaverydifferentproblem,thatofretargetablecompilationforagenericprocessorarchi-tecture.Theyfocustheiroptimizationtechniquestowardhighlyasymmetricprocessors,suchascommercialDSP’s(inwhich,forexample,oneregistermayonlybeusedformultiplication,anotheroneonlyformemoryaddressing,andsoon).Theirregisterassignmentschemeisbasedonthenotionofclassesofregisters,describingwhichtypeofoperationcanusewhichregister.ThisinformationisusedduringCDFGcoveringwithprocessorinstructions[136]tominimizethenumberofmovesrequiredtosaveregistersintotemporarylocations.

Marwedel[121]alsousesasimilarCDFGcoveringapproach.ThesourcespecificationcanbewritteninVHDLorinthePascal-likelanguageMimola.Thepurposeismi-crocodegenerationforverylonginstructionword(VLIW)processors,andinthiscasetheinstructionsethasnotbeendefinedyet.Rather,aminimumencodingofthecontrolwordisgeneratedforeachcontrolstep.Controlstepsareallocatedusingan“assoonaspossible”(ASAP)policy,meaningthateachmicrooperationisscheduledtooccurassoonasitsoperandshavebeencomputed,compatiblywithresourceutilizationconflicts.Thecontrolwordcontainsallthebitsnecessarytosteertheexecutionunitsinthespecifiedarchitecturetoperformallthemicro-operationsineachstep.Registerallocationisdoneinordertominimizethenumberoftemporarylocationsinmemoryduetoregisterspills.

Tiwarietal.[137]describeasoftwareanalysis(ratherthansynthesis)methodaimedatestimatingthepowerconsumptionofaprogramonagivenprocessor.Theirpowerconsumptionmodelisbasedontheanalysisofsingleinstructions,addressingmodes,andinstructionpairs(asimplewayofmodelingtheeffectoftheprocessorstate).Themodelisevaluatedbyrunningbenchmarkprogramsforeachofthesecharacteristicsandmeasuringthecurrentflowtoandfromthepowerandgroundpins.V.CONCLUSIONS

Inthispaperweoutlinedsomeimportantaspectsofthedesignprocessforembeddedsystems,includingspecifica-386

tionmodelsandlanguages,simulation,formalverification,partitioning,andhardwareandsoftwaresynthesis.

Thedesignprocessisiterative:adesignistransformedfromaninformaldescriptionintoadetailedspecificationusableformanufacturing.Thespecificationproblemisconcernedwiththerepresentationofthedesignateachofthesesteps;thevalidationproblemistocheckthattherepresentationisconsistentbothwithinastepandbetweensteps;andthesynthesisproblemistotransformthedesignbetweensteps.

Wearguedthatformalmodelsarenecessaryateachstepofadesign,andthatthereisadistinctionbetweenthelanguageinwhichthedesignisspecifiedanditsunderlyingmodelofcomputation.Manymodelsofcomputationhavebeendefined,duenotjusttotheimmaturityofthefieldbutalsotofundamentaldifferences:thebestmodelisafunctionofthedesign.Theheterogeneousnatureofmostembeddedsystemsmakesmultiplemodelsofcomputationanecessity.Manymodelsofcomputationarebuiltbycom-biningthreelargelyorthogonalaspects:sequentialbehavior,concurrency,andcommunication.

Wepresentedanoutlineofthetagged–signalmodel[8],aframeworkdevelopedbytwooftheauthorstocontrastdifferentmodelsofcomputation.Thefundamentalentityinthemodelisanevent(avalue/tagpair).Tagsusuallydenotetemporalbehavior,anddifferentmodelsoftimeappearasstructureimposedonthesetofallpossibletags.Processesappearasrelationsbetweensignals(setsofevents).Thecharacterofsucharelationfollowsfromthetypeofprocessitdescribes.

Simulationandformalverificationaretwokeyvalidationtechniques.Mostembeddedsystemscontainbothhardwareandsoftwarecomponents,anditisachallengetoeffi-cientlysimulatebothcomponentssimultaneously.Usingseparatesimulatorsforeachisoftenmoreefficient,butsynchronizationbecomesachallenge.

Formalverificationcanberoughlydividedintotheo-remprovingmethods,FAmethods,andinfiniteautomatamethods.Theoremproversgenerallyassistdesignersinconstructingaproof,ratherthanbeingfullyautomatic,butareabletodealwithverypowerfullanguages.Finite-automataschemesrepresent(eitherexplicitlyorimplicitly)allstatesofthesystemandcheckpropertiesonthisrep-resentation.Infinite-automataschemesusuallybuildfinitepartitionsofthestatespace,oftenbyseverelyrestrictingtheinputlanguage.

Inthispaper,synthesisreferstoastepinthedesignrefinementprocesswherethedesignrepresentationismademoredetailed.Thiscanbemanualand/orautomated,andisoftendividedintomappingtoarchitecture,partitioning,andcomponentsynthesis.Automatedarchitecturemapping,wheretheoverallsystemstructureisdefined,oftenrestrictstheresulttomaketheproblemmanageable.Partitioning,wheresectionsofthedesignareboundtodifferentpartsofthesystemarchitecture,isparticularlychallengingforembeddedsystemsbecauseoftheelaboratecostfunctionsduetotheirheterogeneity.Assigninganexecutionordertoconcurrentmodulesandfindingasequenceofinstruc-PROCEEDINGSOFTHEIEEE,VOL.85,NO.3,MARCH1997

tionsimplementingafunctionalmodulearetheprimarychallengesinsoftwaresynthesisforembeddedsystems.ACKNOWLEDGMENT

TheauthorsthankH.Hsiehforhishelpwithafirstdraftofthiswork.REFERENCES

[1]G.Berry,“Realtimeprogramming:Specialpurposeorgen-eralpurposelanguages,”inInformationProcessing,vol.89.Amsterdam:NorthHolland-Elsevier,1989,pp.11–17.

[2]R.Milner,M.Tofte,andR.Harper,TheDefinitionofStandard

ML.Cambridge,MA:MITPress,1990.

[3]W.WadgeandE.A.Ashcroft,Lucid,theDataflowProgramming

Language.NewYork:Academic,1985.

[4]A.Davie,AnIntroductiontoFunctionalProgrammingSystems

UsingHaskell.London:CambridgeUniv.Press,1992.

[5]N.Halbwachs,SynchronousProgrammingofReactiveSystems.

Amsterdam:Kluwer,1993.

[6]K.McMillan,SymbolicModelChecking.NewYork:Kluwer,

1993.

[7]J.E.Stoy,DenotationalSemantics:TheScott-StracheyAp-proachtoProgrammingLanguageTheory.Cambridge,MA:MITPress,1977.

[8]E.A.LeeandA.Sangiovanni–Vincentelli,“Thetaggedsignal

model—apreliminaryversionofadenotationalframeworkforcomparingmodelsofcomputation,”Tech.Rep.,Electron.Res.Lab.,Univ.Calif.Berkeley,May1996.

[9]J.E.HopcroftandJ.D.Ullman,IntroductiontoAutomata

Theory,Languages,andComputation.Reading,MA:Addison-Wesley,1979.

[10]J.T.Buck,“Schedulingdynamicdataflowgraphswithbounded

memoryusingthetokenflowmodel,”Ph.D.dissertation,Tech.Rep.UCB/ERL93/69,Dept.ofEECS,Univ.Calif.Berkeley,1993.

[11]T.M.Parks,“Boundedschedulingofprocessnetworks,”Ph.D.

dissertation,Tech.Rep.UCB/ERL95/105,Dept.EECS,Univ.Calif.Berkeley,Dec.1995.

[12]J.C.ShepherdsonandH.E.Sturgis,“Computabilityofrecursive

functions,”J.ACM,vol.10,no.2,pp.217–255,1963.

[13]G.Kahn,“Thesemanticsofasimplelanguageforparallel

programming,”inProc.IFIPCongress74.1974,North-Holland.[14]J.T.Buck,S.Ha,E.A.Lee,andD.G.Messerschmitt,“Ptolemy:

Aframeworkforsimulatingandprototypingheterogeneoussystems,”specialissueonsimulationsoftwaredevelopment,Int.J.ComputerSimul.,vol.4,no.155,pp.155–182,Apr.1994;http://ptolemy.eecs.berkeley.edu/papers/JEurSim.ps.Z.

[15]D.Harel,H.Lachover,A.Naamad,A.Pnueli,M.Politi,R.

Sherman,A.Shtull–Trauring,andM.Trakhtenbrot,“Statemate:Aworkingenvironmentforthedevelopmentofcomplexreactivesystems,”IEEETrans.SoftwareEng.,vol.16,Apr.1990.

[16]D.DrusinskiandD.Harel,“Onthepowerofboundedconcur-rency.I.Finiteautomata,”J.Assoc.forComputingMachinery,vol.41,no.3,pp.517–539,May1994.

[17]M.vonderBeeck,“Acomparisonofstatechartsvariants,”in

Proc.FormalTechn.inRealTimeandFaultTolerantSyst.,vol.863,LNCS,Springer-Verlag,1984,pp.128–148.

[18]W.TakachandA.Wolf,“Anautomatonmodelforscheduling

constraintsinsynchronousmachines,”IEEETrans.Computers,vol.44,pp.1–12,Jan.1995.

[19]M.Chiodo,P.Giusto,H.Hsieh,A.Jurecska,L.Lavagno,

andA.Sangiovanni–Vincentelli,“Aformalmethodologyforhardware/softwarecodesignofembeddedsystems,”IEEEMicro,Aug.1994.

[20]W.-T.Chang,A.Kalavade,andE.A.Lee,“Effectiveheteroge-neousdesignandcosimulation,”inNATOAdvancedStudyInst.WorkshoponHardware/SoftwareCodesign,LakeComo,Italy,June1995;http://ptolemy.eecs.berkeley.edu/papers/effective.[21]C.N.CoelhoandG.DeMicheli,“Analysisandsynthesisof

concurrentdigitalcircuitsusingcontrol-flowexpressions,”IEEETrans.Comp.-AidedDes.,vol.15,pp.854–876,Aug.1996.[22]A.BenvenisteandG.Berry,“Thesynchronousapproachtoreac-tiveandreal-timesystems,”Proc.IEEE,vol.79,pp.1270–1282,Sept.1991.

[23]F.BoussinotandR.DeSimone,“TheESTERELlanguage,”

Proc.IEEE,vol.79,no.9,1991.

[24]N.Halbwachs,P.Caspi,P.Raymond,andD.Pilaud,“The

synchronousdataflowprogramminglanguageLUSTRE,”Proc.IEEE,vol.79,pp.1305–1319,Sept.1991.

[25]A.BenvenisteandP.LeGuernic,“Hybriddynamicalsystems

theoryandthe{SIGNAL}language,”IEEETrans.Automat.Contr.,vol.35,pp.525–546,May1990.

[26]F.Maraninchi,“TheArgoslanguage:Graphicalrepresentation

ofautomataanddescriptionofreactivesystems,”inProc.IEEEWorkshoponVisualLanguages,Kobe,Japan,Oct.1991.

[27]D.Harel,“Statecharts:Avisualformalismforcomplexsys-tems,”Sci.Comput.Program,vol.8,pp.231–274,1987.

[28]G.Berry,“AhardwareimplementationofpureEsterel,”inProc.

Int.WorkshoponFormalMethodsinVLSIDesign,Jan.1991.[29]F.RocheteauandN.Halbwachs,“Implementingreactivepro-gramsoncircuits:AhardwareimplementationofLUSTRE,”inReal-Time,TheoryinPractice,REXWorkshopProceedings,Mook,Netherlands,June1992,vol.600ofLNCS,pp.195–208,Springer-Verlag.

[30]T.R.Shiple,G.Berry,andH.Touati,“Constructiveanalysisof

cycliccircuits,”inProc.Europe.DesignandTestConf.,Mar.1996.

[31]E.A.LeeandT.M.Parks,“Dataflowprocess

networks,”Proc.IEEE,vol.83,pp.773–801,May1995;http://ptolemy.eecs.berkeley.edu/papers/processNets.

[32]S.S.Bhattacharyya,P.K.Murthy,andE.A.Lee,SoftwareSyn-thesisfromDataflowGraphs.Norwood,MA:Kluwer,1996.[33]W.-T.Chang,S.-H.Ha,andE.A.Lee,“Heterogeneoussim-ulation—mixingdiscrete-eventmodelswithdataflow,”J.VLSISignalProcess.,1996.

[34]R.M.KarpandR.E.Miller,“Propertiesofamodelforparallel

computations:Determinacy,termination,queueing,”SIAMJ.,vol.14,pp.1390–1411,Nov.1966.

[35]E.A.LeeandD.G.Messerschmitt,“Synchronousdataflow,”

Proc.IEEE,vol.75,Sept.1987.[36]R.Lauwereins,P.Wauters,M.Ad´e,andJ.A.Peperstraete,

“GeometricparallelismandcyclostaticdataflowinGRAPE-II,”inProc.5thInt.WorkshoponRapidSystemPrototyping,Grenoble,France,June1994.

[37]G.Bilsen,M.Engels,R.Lauwereins,andJ.A.Peperstraete,

“Staticschedulingofmulti-rateandcyclo-staticDSPapplica-tions,”inIEEEProc.1994WorkshoponVLSISignalProcess.,1994.

[38]D.J.Kaplanetal.,“Processinggraphmethodspecification

version1.0,”TheNavalRes.Lab.,Washington,DC,Dec.1987.

[39]R.Jagannathan,“ParallelexecutionofGLUprograms,”in2nd

Int.WorkshoponDataflowComputing,HamiltonIsl.,Queens-land,Australia,May1992.

[40]W.B.Ackerman,“Dataflowlanguages,”Computer,vol.15,

no.2,1982.

[41]N.CarrieroandD.Gelernter,“Lindaincontext,”Comm.ACM,

vol.32,no.4,pp.444–458,Apr.1989.

[42]F.CommonerandA.W.Holt,“Markeddirectedgraphs,”J.

ComputerSyst.Sci.,vol.5,pp.511–523,1971.

[43]P.A.Suhler,J.Biswas,K.M.Korner,andJ.C.Browne,“TDFL:

Atask-leveldataflowlanguage,”J.ParallelDistrib.Syst.,vol.9,no.2,June1990.

[44]ArvindandK.P.Gostelow,“TheU-interpreter,”Computer,vol.

15,no.2,1982.

[45]J.RasureandC.S.Williams,“Anintegratedvisuallanguage

andsoftwaredevelopmentenvironment,”J.VisualLanguagesandComputing,vol.2,pp.217–246,1991.

[46]C.A.R.Hoare,“Communicatingsequentialprocesses,”Comm.

ACM,vol.21,no.8,1978.

[47]R.Milner,CommunicationandConcurrency.Englewood

Cliffs,NJ:Prentice-Hall,1989.

[48]J.L.Peterson,PetriNetTheoryandtheModelingofSystems.

EnglewoodCliffs,NJ:Prentice-Hall,1981.

[49]W.Reisig,PetriNets:AnIntroduction.Berlin:Springer-Verlag,1985.

[50]A.Valmari,“Astubbornattackonstateexplosion,”Formal

MethodsinSyst.Design,vol.1,no.4,pp.297–322,1992.[51]P.Godefroid,“Usingpartialorderstoimproveautomaticveri-ficationmethods,”inProc.ComputerAidedVerificationWork-shop,E.M.ClarkeandR.P.Kurshan,Eds.,1990,DIMACSSeriesinDiscreteMathemat.andTheoret.ComputerSci.,1991,pp.321–340.

387

EDWARDSetal.:DESIGNOFEMBEDDEDSYSTEMS:FORMALMODELS,VALIDATION,ANDSYNTHESIS

[52]E.Dijkstra,“Cooperatingsequentialprocesses,”inProgramming

[53]LanguagesR.P.Kurshan,,E.F.Automata-TheoreticGenuys,Ed.NewVerificationYork:Academic,ofCoordinating

1968.[54]ProcessesJ.Burch,E..Clarke,Princeton,K.McMillan,NJ:PrincetonandD.Univ.Dill,Press,“Sequential1994.

circuit

verificationusingsymbolicmodelchecking,”inProc.Design[55]Automat.R.AlurandConf.T.,A.1990,Henzinger,pp.46–51.

“Logicsandmodelsofrealtime:

Asurvey,”inReal-Time:TheoryinPractice:REXWorkshopProc.,J.W.deBakker,C.Huizing,W.P.deRoever,andG.[56]Rozenberg,R.K.Gupta,Eds.,C.N.1992.

CoelhoJr.,andG.DeMicheli,“Synthesis

andsimulationofdigitalsystemscontaininginteractinghardwareandsoftwarecomponents,”inProc.DesignAutomat.Conf.,June[57]1992.

J.Rowson,“Hardware/softwareco-simulation,”inProc.Design

[58]Automat.J.Wilson,Conf.“Hardware/software,1994,pp.439–440.

selectedcyclesolution,”inProc.

[59]Int.D.E.WorkshopThomas,onJ.Hardware-SoftwareK.Adams,andH.CodesignSchmitt,,1994.

“Amodeland

methodologyforhardware-softwarecodesign,”IEEEDesignand[60]TestK.tenofComputersHagenand,vol.H.10,Meyr,no.3,“Timedpp.6–15,andSept.untimed1993.

hard-ware/softwarecosimulation:applicationandefficientimplemen-tation,”inProc.Int.WorkshoponHardware-SoftwareCodesign,[61]Oct.A.Kalavade1993.

andE.A.Lee,“Hardware/softwareco-designusing

Ptolemy—acasestudy,”inProc.Int.WorkshoponHardware-[62]SoftwareS.SutarwalaCodesignandP.,Sept.Paulin,1992.

“Flexiblemodelingenvironmentfor

embeddedsystemsdesign,”inProc.Int.WorkshoponHardware-[63]SoftwareS.LeeandCodesignJ.M.Rabaey,,1994.

“Ahardware-softwareco-simulation

environment,”inProc.Int.WorkshoponHardware-Software[64]CodesignC.Liem,,T.Oct.May,1993.

andP.Paulin,“Registerassignmentthrough

resourceclassificationforASIPmicrocodegeneration,”inProc.[65]Int.D.L.Conf.Dill,onTraceComputer-AidedTheoryforAutomaticDesign,Nov.Hierarchical1994.

Verification

ofSpeed-IndependentCircuits.Cambridge,MA:MITPress,[66]1988M.J.(ACMC.GordondistinguishedandT.F.dissertation).

Melham,Eds.,IntroductiontoHOL:

ATheoremProvingEnvironmentforHigherOrderLogic.New[67]York:R.S.Boyer,Cambridge,M.Kaufmann,1992.

andJ.S.Moore,“TheBoyer-Moore

theoremproveranditsinteractiveenhancement,”Comput.Math-[68]ematicsS.Owre,withJ.Applicat.M.Rushby,,pp.and27–62,N.Shankar,Jan.1995.

“PVS:aprototype

verificationsystem,”in11thInt.Conf.onAutomatedDeduction.[69]JuneO.Coudert,1992.

C.Berthet,andJ.C.Madre,“Verificationofse-quentialmachinesusingBooleanfunctionalvectors,”inIMEC-IFIPInt.WorkshoponAppl.FormalMethodsforCorrectVLSI[70]DesignE.M.,Clarke,Nov.1989,E.A.pp.Emerson,111–128.

andA.P.Sistla,“Automatic

verificationoffinite-stateconcurrentsystemsusingtemporal[71]logicJ.P.specifications,”QueilleandJ.Sifakis,ACMTOPLAS“Specification,vol.8,andno.2,verification1986.

of

concurrentsystemsinCesar,”inInt.Symp.onProgramming.[72]Apr.A.Pnueli,1982,“TheLNCStemporal137,SpringerlogicsVerlag.

ofprograms,”inIEEEProc.

[73]18thZ.MannaAnnu.andSymp.A.onPnueli,FoundationsTheTemporalofComputerLogicSciof.,ReactiveMay1977.and

[74]ConcurrentR.AlurandSystemsD.Dill,.“AutomataBerlin:Springer-Verlag,formodelingreal-time1992.

systems,”

inAutomata,LanguagesandProgramming:17thAnnu.Colloq.,vol.443,LectureNotesinComputerScience,WarwickUniv.,[75]JulyP.Cousot16–20,and1990,R.pp.Cousot,322–335.

“Abstractinterpretation:aunified

latticemodelforstaticanalysisofprogramsbyconstructionorapproximationoffixpoints,”in4thACMSymp.onPrinciplesof[76]ProgrammingJ.McManisandLanguagesP.Varaiya,,Los“SuspensionAngeles,Jan.automata:1977.

adecidable

classofhybridautomata,”inProc.6thWorkshoponComputer-[77]AidedJ.R.VerificationBurch,“Automatic,1994,pp.symbolic105–117.

verificationofreal-time

concurrentsystems,”Ph.D.dissertation,CarnegieMellonUniv.,Aug.1992.

388

[78]E.Clarke,O.Grumberg,andD.Long,“Modelcheckingand

abstraction,”ACMTrans.ProgrammingLanguagesandSyst.,[79]vol.A.Mazurkiewicz,16,no.5,pp.1512–1542,“Traces,histories,Sept.1994.

graphs:Instancesofa

processmonoid,”inProc.Conf.onMathematicalFoundationsofComputerScience,M.P.ChytilandV.Koubek,Eds.1984,[80]vol.M.L.176,deLNCSSouza,Springer-Verlag.

andR.deSimone,“Usingpartialorders

forverifyingbehavioralequivalences,”inProc.CONCUR’95,[81]1995.

R.Bryant,“Graph-basedalgorithmsforbooleanfunctionmanip-ulation,”IEEETrans.Computers,vol.C-35,no.8,pp.677–691,[82]Aug.J.R.Burch1986.

andD.L.Dill,“Automaticverificationofpipelined

microprocessorcontrol,”inProc.6thWorkshoponComputer-[83]AidedR.E.BryantVerificationandY.-A.,1994,Chen,pp.68–80.

“Verificationofarithmeticcircuits

withBinaryMomentDiagrams,”inProc.DesignAutomat.[84]Conf.F.Balarin,1995,andpp.A.535–541.

Sangiovanni–Vincentelli,“Averificationstrat-egyfortiming-constrainedsystems,”inProc.4thWorkshopon[85]Computer-AidedR.Alur,A.Itai,VerificationR.Kurshan,,1992,andpp.M.148–163.

Yannakakis,“Timing

verificationbysuccessiveapproximation,”inProc.Computer[86]AidedJ.Buck,VerificationS.Ha,E.WorkshopA.Lee,and,1993,D.G.pp.Masserschmitt,137–150.

“Ptolemy:

aframeworkforsimulatingandprototypingheterogeneoussys-tems,”Int.J.ComputerSimulation,SpecialIssueonSimulation[87]SoftwareD.HarelDevelopment,etal.,“STATEMATE:Jan.1990.

aworkingenvironmentfor

thedevelopmentofcomplexreactivesystems,”IEEETrans.[88]SoftwareP.J.RamadgeEngineeringandW.,vol.M.16,Wonham,no.4,Apr.“The1990.

controlofdiscrete

[89]eventG.Hoffmannsystems,”andProc.H.IEEEWong-Toi,,vol.77,“SymbolicJan.1989.

synthesisofsu-pervisorycontrollers,”inAmer.Contr.Conf.,Chicago,June[90]1992.

M.DiBenedetto,A.Saldanha,andA.Sangiovanni–Vincentelli,

“Strongmodelmatchingforfinitestatemachines,”inProc.3rd[91]Europe.M.Theissinger,Contr.Conf.P.Stravers,,Sept.and1995.

H.Veit,“CASTLE:aninterac-tiveenvironmentforhardware-softwareco-design,”inProc.Int.[92]WorkshopS.Kumar,onJ.Hardware-SoftwareH.Aylor,B.W.CodesignJohnson,,1994.

andW.A.Wulf,

“Aframeworkforhardware/softwarecodesign,”inProc.Int.WorkshoponHardware-SoftwareCodesign,Sept.[93]

1992.

,“Exploringhardware/softwareabstractionsandalter-nativesforcodesign,”inProc.Int.WorkshoponHardware-[94]SoftwareS.PrakashCodesignandA.,Oct.Parker,1993.

“Synthesisofapplication-specific

multi-processorarchitectures,”inProc.DesignAutomat.Conf.,[95]JuneF.Vahid1991.

andD.G.Gajski,“Specificationpartitioningforsystem

[96]design,”P.Chou,inE.Proc.A.DesignWalkup,Automat.andG.Conf.Borriello,,June1992.

“Schedulingfor

reactivereal-timesystems,”IEEEMicro,vol.14,no.4,pp.[97]37–47,J.Henkel,Aug.R.1994.

Ernst,U.Holtmann,andT.Benner,“Adaptation

ofpartitioningandhigh-levelsynthesisinhardware/softwareco-synthesis,”inProc.Int.Conf.onComputer-AidedDesign,Nov.[98]1994.

K.Olokutun,R.Helaihel,J.Levitt,andR.Ramirez,“Asoftware-hardwarecosynthesisapproachtodigitalsystemsimulation,”[99]IEEEX.Hu,MicroJ.G.,D’Ambrosio,vol.14,no.4,B.pp.T.Murray,48–58,Aug.andD.-L.1994.

Tang,“Code-signofarchitecturesforpowertrainmodules,”IEEEMicro,vol.[100]14,E.Barros,no.4,pp.W.48–58,Rosenstiel,Aug.and1994.

X.Xiong,“Hardware/software

partitioningwithUNITY,”inProc.Int.WorkshoponHardware-[101]SoftwareE.BarrosCodesignandA.,Sampaio,Oct.1993.

“Towardprovablycorrecthard-ware/softwarepartitioningusingOCCAM,”inProc.Int.Work-[102]shopA.KalavadeonHardware-SoftwareandE.A.Lee,Codesign“Aglobal,Oct.criticality/local1994.

phase

drivenalgorithmfortheconstrainedhardware/softwareparti-tioningproblem,”inProc.Int.WorkshoponHardware-SoftwareCodesign,1994.

PROCEEDINGSOFTHEIEEE,VOL.85,NO.3,MARCH1997

[103]J.K.Adams,H.Schmitt,andD.E.Thomas,“Amodeland

methodologyforhardware-softwarecodesign,”inProc.Int.WorkshoponHardware-SoftwareCodesign,Oct.1993.

[104]P.Eles,Z.Peng,andA.Doboli,“VHDLsystem-levelspec-ificationandpartitioninginahardware/softwarecosynthesisenvironment,”inProc.Int.WorkshoponHardware-SoftwareCodesign,Sept.1994.

[105]W.LukandT.Wu,“Towardadeclarativeframeworkfor

hardware-softwarecodesign,”inProc.Int.WorkshoponHardware-SoftwareCodesign,1994.[106]U.Steinhausenetal.,“System-synthesisusing

hardware/softwarecodesign,”inProc.Int.WorkshoponHardware-SoftwareCodesign,Oct.1993.

[107]T.B.Ismail,M.Abid,andA.A.Jerraya,“COSMOS:acodesign

approachforcommunicatingsystems,”inProc.Int.WorkshoponHardware-SoftwareCodesign,1994.

[108]S.Antoniazzi,A.Balboni,W.Fornaciari,andD.Sciuto,“A

methodologyforcontrol-dominatedsystemscodesign,”inProc.Int.WorkshoponHardware-SoftwareCodesign,1994.

[109]R.K.Gupta,C.N.CoelhoJr.,andG.DeMicheli,“Program

implementationschemesforhardware-softwaresystems,”IEEEComputer,pp.48–55,Jan.1994.

[110]R.ErnstandJ.Henkel,“Hardware-softwarecodesignofem-beddedcontrollersbasedonhardwareextraction,”inProc.Int.WorkshoponHardware-SoftwareCodesign,Sept.1992.

[111]J.Henkel,T.Benner,andR.Ernst,“Hardwaregenerationand

partitioningeffectsintheCOSYMAsystem,”inProc.Int.WorkshoponHardware-SoftwareCodesign,Oct.1993.

[112]J.G.D’AmbrosioandX.B.Hu,“Configuration-levelhard-ware/softwarepartitioningforreal-timeembeddedsystems,”inProc.Int.WorkshoponHardware-SoftwareCodesign,1994.[113]C.LiuandJ.WLayland,“Schedulingalgorithmsformultipro-gramminginahardreal-timeenvironment,”J.ACM,vol.20,no.1,pp.44–61,Jan.1973.

[114]D.D.Gajski,S.Narayan,L.Ramachandran,andF.Vahid,

“Systemdesignmethodologies:aimingatthe100hdesigncycle,”IEEETrans.VLSI,vol.4,Mar.1996.

[115]J.Wilberg,R.Camposano,andW.Rosenstiel,“Designflow

forhardware/softwarecosynthesisofavideocompressionsys-tem,”inProc.Int.WorkshoponHardware-SoftwareCodesign,1994.

[116]J.HoogerbruggeandH.Corporaal,“Transport-triggeringvs.

operation-triggering,”in5thInt.Conf.onCompilerConstruc-tion,Apr.1994.

[117]M.Voss,T.BenIsmail,A.A.Jerraya,andK.-H.Kapp,“Toward

atheoryforhardware-softwarecodesign,”inProc.Int.WorkshoponHardware-SoftwareCodesign,1994.

[118]S.Saracco,J.R.W.Smith,andR.Reed,Telecommunications

SystemsEngineeringUsingSDL.Amsterdam:NorthHolland-Elsevier,1989.

[119]E.WalkupandG.Borriello,“Automaticsynthesisofdevice

driversforhardware-softwarecodesign,”inProc.Int.WorkshoponHardware-SoftwareCodesign,Oct.1993.[120]G.Menez,M.Auguin,FBo`eri,andC.Carri`ere,“Apartitioning

algorithmforsystem-levelsynthesis,”inProc.Int.Conf.onComputer-AidedDesign,Nov.1992.

[121]P.Marwedel,“Tree-basedmappingofalgorithmstopredefined

structures,”inProc.Int.Conf.onComputer-AidedDesign,Nov.1993.

[122]P.Paulin,“DSPdesigntoolrequirementsforembeddedsystems:

atelecommunicationsindustrialperspective,”J.VLSISignalProcess.,vol.9,no.1-2,pp.22–47,Jan.1995.

[123]G.DeMicheli,SynthesisandOptimizationofDigitalCircuits.

NewYork:McGraw-Hill,1994.

[124]S.Devadas,A.Ghosh,andK.Keutzer,LogicSynthesis.New

York:McGraw-Hill,1994.

[125]R.CamposanoandW.Wolf,Eds.,High-levelVLSISynthesis.

Amsterdam:Kluwer,1991.

[126]P.MarwedelandG.Goossens,Eds.,CodeGenerationfor

EmbeddedProcessors.NewYork:Kluwer,1995.

[127]W.A.HalangandA.D.Stoyenko,ConstructingPredictable

RealTimeSystems.NewYork:Kluwer,1991.

[128]G.C.SihandE.A.Lee,“Declustering:Anewmultiprocessor

schedulingtechnique,”IEEETrans.ParallelDistrib.Syst.,vol.4,pp.625–637,June1993.

,“Acompile-timeschedulingheuristicforinterconnection-[129]

constrainedheterogeneousprocessorarchitectures,”IEEETrans.ParallelDistrib.Syst.,vol.4,Feb.1993.

[130]M.Cochran,“Usingtheratemonotonicanalysistoanalyzethe

schedulabilityofADARTSreal-timesoftwaredesigns,”inProc.Int.WorkshoponHardware-SoftwareCodesign,Sept.1992.[131]M.Chiodo,P.Giusto,H.Hsieh,A.Jurecska,L.Lavagno,

andA.Sangiovanni-Vincentelli,“Hardware/softwarecodesignofembeddedsystems,”IEEEMicro,vol.14,no.4,pp.26–36,Aug.1994.

[132]P.ChouandG.Borriello,“Softwareschedulingintheco-synthesisofreactivereal-timesystems,”inProc.DesignAu-tomat.Conf.,June1994.

[133]R.K.GuptaandG.DeMicheli,“Constrainedsoftwaregenera-tionforhardware-softwaresystems,”inProc.Int.WorkshoponHardware-SoftwareCodesign,1994.

[134]M.Chiodo,P.Giusto,H.Hsieh,A.Jurecska,L.Lavagno,andA.

Sangiovanni–Vincentelli,“SynthesisofsoftwareprogramsfromCFSMspecifications,”inProc.DesignAutomat.Conf.,June1995.

[135]K.SuzukiandA.Sangiovanni-Vincentelli,“Efficientsoftware

performanceestimationmethodsforhardware/softwarecode-sign,”inProc.DesignAutomat.Conf.,1996.

[136]C.Liem,T.May,andP.Paulin,“Instructionsetmatchingand

selectionforDSPandASIPcodegeneration,”inEurope.DesignandTestConf.,Feb.1994.

[137]V.Tiwari,S.Malik,andA.Wolfe,“Poweranalysisofembedded

software:afirststeptowardsoftwarepowerminimization,”IEEETrans.VLSISyst.,vol.2,no.4,pp.437–445,Dec.1994.

StephenEdwards(Member,IEEE)receivedtheB.S.degreeinelectricalengineeringfromtheCaliforniaInstituteofTechnology,Pasadena,in1992andtheM.S.degreeinelectricalengineer-ingfromtheUniversityofCalifornia,Berkeley,in1994.HeiscurrentlyaPh.D.candidateinelectricalengineeringattheUniversityofCali-fornia,Berkeley.

HehasbeenaninternatMicrosoft,VitesseSemiconductor,andIntervalResearchCorpora-tion.Hisresearchinterestsincludescheduling

techniquesforsynchronouslanguages,hardwareandsoftwarecompilationtechniques,andheterogeneousembeddedsystemdesignandsynthesis.

LucianoLavagno(Member,IEEE)receivedtheDoctorofEngineeringdegreeinelectricalengineering(magnacumlaude)fromthePo-litecnicodiTorino,Italy,in1983.HereceivedthePh.D.degreeinelectricalengineeringandcomputersciencefromtheUniversityofCali-fornia,Berkeley,in1992.

HeisanAssistantProfessoratthePolitecnicodiTorino,Italy,andaResearchScientistatCadenceBerkeleyLaboratories.HehasalsobeenaconsultantforvariousEDAcompanies,

suchasSynopsysandCadence.In1988hejoinedtheDepartmentofElectricalEngineeringandComputerScienceoftheUniversityofCaliforniaatBerkeley,whereheworkedonlogicsynthesisandtestingofsynchronousandasynchronouscircuits.From1984to1988hewaswithCSELTLaboratories,Torino,Italy,wherehewasinvolvedinanESPRITprojectthatdevelopedacompletehigh-levelsynthesissystem.Heistheauthorofabookonasynchronouscircuitdesignandhaspublishedover25journalandconferencepapers.Hisresearchinterestsincludethesynthesisofasynchronousandlow-powercircuits,theconcurrentdesignofmixedhardwareandsoftwaresystems,andtheformalverificationofdigitalsystems.

Dr.LavagnoreceivedtheBestPaperAwardatthe28thDesignAutomationConferencein1991.Hehasservedonthetechnicalcommit-teesofseveralinternationalconferences,namelytheDesignAutomationConference,theInternationalConferenceonComputerAidedDesign,andtheEuropeanDesignAutomationConference.

389

EDWARDSetal.:DESIGNOFEMBEDDEDSYSTEMS:FORMALMODELS,VALIDATION,ANDSYNTHESIS

EdwardA.Lee(Fellow,IEEE)receivedtheB.S.degreefromYaleUniversity,NewHaven,CT,theS.M.degreefromtheMassachusettsInstituteofTechnology,Cambridge,MA,andthePh.D.degreefromUniversityofCalifornia,Berkeley,in1979,1981,and1986,respectively.HeisaProfessorofElectricalEngineeringandComputerScienceattheUniversityofCal-ifornia,Berkeley,andDirectorofthePtolemyprojectatthesameuniversity.HeisalsoafounderofBerkeleyDesignTechnology,Inc.,

andhasconsultedforanumberofothercompanies.From1979to1982hewasaTechnicalStaffMemberatBellTelephoneLaboratories,Holmdel,NJ,intheAdvancedDataCommunicationsLaboratory.Heistheco-authoroffourbooks,numerouspapers,andtwopatents.Hisresearchinterestsincludereal-timesoftware,discrete-eventsystems,parallelcomputation,architectureandsoftwaretechniquesforsignalprocessing,anddesignmethodologyforheterogeneoussystems.

Dr.LeewasanNSFPresidentialYoungInvestigator.

390AlbertoSangiovanni–Vincentelli(Member,IEEE)receivedtheDoctorofEngineeringdegree(summacumlaude)inelectricalengineeringandcomputersciencefromthePolitecnicodiMilano,Italyin1971.

HeisaProfessorofElectricalEngineeringandComputerSciencesattheUniversityofCalifornia,Berkeley,wherehehasbeenafacultymembersince1976.HewasAssistantProfessorfrom1971to1974anda“ProfessoreIncaricato”from1974to1976atthePolitecnico

diMilano.During1980–1981,hewasaVistingScientistattheMathematicalSciencesDepartmentoftheIBMT.J.WatsonResearchCenter.In1987,hewasaVisitingProfessoratMIT.HehasheldanumberofVisitingProfessorpositionsattheUniversityofTorino,UniversityofBologna,UniversityofPavia,UniversityofPisa,andtheUniversityofRome.HehelpedfoundCadenceandSynopsysandisScientificDirectorandGeneralManageroftheCadenceEuropeanLaboratoriesinRome.HewasaDirectorofViewLogicandPieDesignSystemsandChairoftheTechnicalAdvisoryBoardofSynopsys.HeisontheBoardofDirectorsofCadenceandafounderandmemberoftheMangementBoardoftheCadenceBerkeleyLaboratories.HehasconsultedforIBM,Intel,AT&T,GTE,GE,Harris,Nynex,Teknekron,DEC,HP,KawasakiSteel,Fujitsu,SGS-Thomson,Alcatel,Magneti-Marelli,ENI,Montedison,FIAT,andBull.HeisontheAdvisoryBoardoftheLesterCenteroftheHaasSchoolofBusiness,oftheCenterforWesternEuropeanStudies,andamemberofBerkeleyRoundtablefortheInternationalEconomy(BRIE),alloftheUniversityofCalifornia.Hisresearchinterestsarerelatedtotheapplicationofmathematicalideasandapproachestothedesignofelectronicsystems.Recently,hehasbeenfocusingondesignmethodologiesandtoolsformixedsignalintegratedcircuitsincludinghigh-frequencyandlowpowercircuits,andforemebeddedcontrollers.Inthislatestarea,heisinterestedinmethodsforsoftwaresynthesisandformalverification.Hehaspublishedover350papersandfivebooksintheareaofdesignmethodologiesandtools.HehasbeenontheprogramcommitteeofseveralconferencesandhasbeenontheeditorialboardoftheIEEETRANSACTIONSONCIRCUITSANDSYSTEMS,theIEEETRANSACTIONSONCOMPUTER-AIDEDDESIGN,andofseveralotherjournals.

Dr.Sangiovanni–VincentellireceivedtheDistinguishedTeachingAwardoftheUniversityofCaliforniain1981.Hereceivedthe1995GraduateTeachingAwardoftheIEEE,threeBestPaperAwards(1982,1983,and1990),aBestPresentationAward(1982)attheDesignAutomationConference.Heistheco-recipientoftheGuillemin–CauerAward(1982–1983),theDarlingtonAward(1987–1988),andtheBestPaperAwardoftheCircuitsandSystemsSocietyoftheIEEE(1989–1990).HeholdstheVIPgrantfromtheItalianNationalResearchCouncilandwastheTechnicalProgramChairpersonoftheInternationalConferenceonCADandhisGeneralChair.

PROCEEDINGSOFTHEIEEE,VOL.85,NO.3,MARCH1997