Riding the Technology Curve Dec. 1, 1998Impact of TechnologyMoore’s LawSemiconductor Industry ForecastImpact of Moore’s LawSolving Hard ProblemsSolving with a Y2K ComputerMoore’s Law ComputerSlide 9Solving with a Moore’s Law ComputerEffect of Step ComplexityImplications of Moore’s LawHow to Be a VisionaryTruly Hard ProblemsMotivation for Formal VerificationThe Pentium FiascoResolutionIs There a Better Way?CMU’s Research ContributionsTemporal Logic Model CheckingWord-Level AbstractionsWord-Level Verification*BMD Representations of IntegersWord-Level *BMDsUsing Word-Level VerificationRecent Result on Arithmetic CircuitsFormal Verification TasksLong Term Verification ChallengesRiding the Technology CurveDec. 1, 1998TopicsTopicsMoore’s LawAre exponential problems intractable?Impact on real-world problemsThe verification challenge15-213– 2 –Impact of TechnologyImpact of TechnologyIt’s the Technology, Stupid!It’s the Technology, Stupid!Computer science has ridden the waveThings Aren’t Over YetThings Aren’t Over YetTechnology will continue to progress along current growth curvesFor at least 10 more yearsDifficult technical challenges in doing soEven Technologists Can’t Beat Laws of PhysicsEven Technologists Can’t Beat Laws of Physics– 3 –Moore’s LawMoore’s LawGordon MooreGordon MooreCo-founded Intel in early 70’sObserved in 1972 that number of transistors / chip doubled ~ every 1.5 yearsReally a “trend” rather than a “law”Exponential Growth TrendsExponential Growth TrendsDRAM technologyCapacity 4X every 3 yearsSpeed 3X in 10 yearsMagnetic disk technologyCapacity 4X every 3 yearsMicroprocessor PerformanceSPEC performance 2X every 1.5 yearsSoftware complexityTypical program sizes growing 1.5--2X per year– 4 –Semiconductor Industry ForecastSemiconductor Industry ForecastSemiconductor Industry Association, 1992 Technology WorkshopYear 1992 1995 1998 2001 2004 2007Feature size 0.5 0.35 0.25 0.18 0.12 0.10DRAM cap 16M 64M 256M 1G 4G 16GGates/chip 300K 800K 2M 5M 10M 20MChip cm22.5 4.0 6.0 8.0 10.0 12.5I/Os 500 750 1500 2000 3500 5000off chip MHz 60 100 175 250 350 500on chip MHz 120 200 350 500 700 1000– 5 –Impact of Moore’s LawImpact of Moore’s LawMoore’s LawMoore’s LawPerformance factors of systems built with integrated circuit technology follow exponential curveE.g., computer speed / memory capacities double every 1.5 yearsImplicationsImplicationsComputers 10 years from now will run 100 X fasterProblems that appear intractable today will be straightforwardMust not limit future planning with today’s technologyExample Application DomainsExample Application DomainsSpeech recognitionWill be routinely done with handheld devicesBreaking secret codesNeed to use large enough encryption keys– 6 –Solving Hard ProblemsSolving Hard ProblemsConventional WisdomConventional WisdomExponential problems are intractableOperationOperationAssume problem of size n requires 2n stepsEach step takes k years on a Y2K computerY2K Computer PerformanceY2K Computer PerformanceStart computation Jan. 1, 2000Keep running same machine until problem solvedWould take k 2n years– 7 –Solving with a Y2K ComputerSolving with a Y2K ComputerY2K Computer1.E-051.E-031.E-011.E+011.E+031.E+051.E+071.E+091.E+111.E+131.E+151.E+171.E+191.E+211.E+231.E+251.E+271.E+291.E+3110 20 30 40 50 60 70 80 90 100Problem Size (n)CPU YearssecondminutehourdayweekyearTimeperOperation– 8 –Moore’s Law ComputerMoore’s Law ComputerOperationOperationStart computing on Jan. 1, 2000Keep upgrading machine being usedIn year y, would have performance 1.587y relative to Y2K machinePerformancePerformanceAfter y years of operation, would have performed as much computation as Y2K machine would do in time:Examplesy = 1 1.27y = 2 3.29y = 5 20.y = 10 218.y = 100 2.53 X 1020)1587.1(16.2587.10yyxdx– 9 –Solving Hard ProblemsSolving Hard ProblemsSolution TimeSolution TimeProblem of size nRunning y years on Moore’s Law computerFor large values of n:ComplexityComplexityLinear in problem size)2462.01ln(16.2nky )(67.1ln16.25.1nOkny– 10 –Solving with a Moore’s Law ComputerSolving with a Moore’s Law ComputerMoore's Law Computer02040608010012014016010 20 30 40 50 60 70 80 90 100Problem size (n)CPU YearssecondminutehourdayweekyearTimeperOperation– 11 –Effect of Step ComplexityEffect of Step ComplexityObserveObserveStep complexity k adds only additive factor of 2.16 ln k to running timeExampleExampleFor n = 100k y1 second 1111 minute 1201 hour 1291 day 1361 week 1401 year 148ExplanationExplanationFinal years of computation will be on exponentially faster machines– 12 –Implications of Moore’s LawImplications of Moore’s LawP=NP (Effectively)P=NP (Effectively)Problems of exponential complexity can be solved in linear timeCaveatCaveatCannot hold foreverFundamental LimitFundamental LimitArgument due to Ed FredkinClaim that ultimate limit to growth in memory capacity is cubicCannot build storage device with less than one electronAssume consume all available material to build memoriesWould soon exhaust planetary resourcesCannot travel into outer space faster than speed of lightTotal amount of material available at time t is (t3)This limit will be hit in ~400 years– 13 –How to Be a VisionaryHow to Be a VisionaryPick a Really Hard ProblemPick a Really Hard ProblemSequencing of human genomeAccurate weather predictionFlying helicopter autonomouslyMake ProclamationsMake Proclamations“In 20 years, problem X will be solved”WaitWaitBut make sure everyone credits you with the visionMaybe make a few contributions to technologyAmass GloryAmass GloryTuring Award Citation:“He/She had the foresight to see that this problem could be solved.”– 14 –Truly Hard ProblemsTruly Hard ProblemsThose That Get Harder over TimeThose That Get Harder over TimeTrack Moore’s law growthHow do I make sure my chip will operate correctly?How do I make sure my programs are correct?How do I manufacture state-of-the-art chips?HighlightHighlightResearch at CMU on formal verification of hardware– 15 –Motivation for Formal VerificationMotivation for Formal VerificationIntel’s Challenge, (ca. 1992)Intel’s Challenge, (ca. 1992)Design a high performance,
View Full Document
Unlocking...