Intel Keynote over formeel A Mind-Stretcher

Heruitgegeven door Plato

volgers: 0

Synopsys heeft op de SolvNet-site een fascinerende lezing geplaatst van Dr. Theo Drane van Intel Graphics. Het onderwerp is het controleren van de gegevenspadequivalentie. Klinkt misschien als gewoon weer een Synopsys VC Formele DPV-goedkeuring, maar je moet het toch bekijken. Dit is een geestverruimende discussie over het gebruik van en de overwegingen in formele zin die je verder brengt dan de routinematige gebruikershandleiding-soort pitch naar meer fascinerend terrein.

Intel Keynote op Formeel

Intellectueel begrip versus steekproeftesten

Testgestuurde simulatie in al zijn vormen is uitstekend en vaak onvervangbaar bij het verifiëren van de juistheid van een ontwerpspecificatie of implementatie. Het is ook gemakkelijk om te beginnen. Schrijf gewoon een testprogramma en begin met simuleren. Maar de keerzijde van die eenvoud is dat dat niet nodig is geheel begrijpen wat we testen om aan de slag te gaan. We overtuigen onszelf ervan dat we de specificatie zorgvuldig hebben gelezen en alle hoekgevallen begrijpen, maar er is niet veel ingewikkelde complexiteit voor nodig om ons begrip te overweldigen.

Formal moedigt je aan om de functionaliteit op een diep niveau te begrijpen (tenminste als je een waardevol resultaat wilt leveren). In het bovenstaande voorbeeld is een simpele vraag – kan z ooit allemaal 1-en zijn – geen voorbeeld in een miljard cycli op een simulator. Niet verwonderlijk, aangezien dit een extreem hoekgeval is. Een formele test geeft in 188 seconden een specifiek en niet voor de hand liggend voorbeeld en kan in iets minder tijd bewijzen dat dit het enige geval is.

Oké, formeel deed wat dynamisch testen niet kon, maar wat nog belangrijker is, je leerde iets dat de simulator je misschien nooit had verteld. Dat er maar één mogelijk geval was waarin die toestand kon voorkomen. Formeel heeft u geholpen het ontwerp op intellectueel niveau beter te begrijpen, niet alleen als probabilistische samenvatting van een eindige reeks testgevallen.

Spec-problemen

Het volgende voorbeeld van Theo is gebaseerd op een bug-automaat (zo genoemd omdat je een bug krijgt als je op een knop drukt). Dit ziet eruit als een vrij eenvoudig C naar RTL-equivalentiecontroleprobleem, C-model aan de linkerkant, RTL-model aan de rechterkant. Een verrassing voor Theo in zijn vroege dagen in het formele was dat het gedrag bij het verschuiven naar rechts in het C-model niet volledig is gedefinieerd in de C-standaard, ook al zal gcc zich redelijk gedragen. Wel zal DPV klagen over een mismatch in een vergelijking met de RTL, zoals het hoort. Ongedefinieerd gedrag is gevaarlijk om op te vertrouwen.

Formeel als een bug-automaat

Spec-vergelijking tussen C en RTL brengt andere gevaren met zich mee, vooral rond bitbreedtes. Afkappen of verlies van een draagbit in een tussenliggend signaal (#3 hierboven) zijn goede voorbeelden. Zijn dit specificatieproblemen? Misschien een grijs gebied tussen specificatie- en implementatiekeuzes.

Voorbij gelijkwaardigheidscontrole

Het primaire doel van DPV, zo lijkt het, is om de gelijkwaardigheid tussen een C- of RTL-referentie en een RTL-implementatie te controleren. Maar die behoefte komt relatief zelden voor en er zijn andere handige manieren waarop een dergelijke technologie kan worden toegepast, zij het een beetje kant-en-klaar. Eerst een klassieker in de implementatiewereld – ik heb een wijziging aangebracht, een bug verholpen – heb ik daardoor nieuwe bugs geïntroduceerd? Een beetje zoals SEQ-controle nadat je klokgating hebt toegevoegd. Bereikbaarheidsanalyse in blokuitvoer kan in sommige gevallen een andere nuttige toepassing zijn.

Niet alleen gelijkwaardigheidscontrole

Theo wordt nog creatiever en vraagt stagiairs om tegenvoorbeelden te gebruiken om het ontwerp beter te begrijpen, Sudoku's oplossen or gehele getallen ontbinden in factoren. Hij erkent dat DPV een vreemde manier is om dergelijke problemen te benaderen, maar wijst erop dat het zijn bedoeling is om de illusie te doorbreken dat DPV alleen bedoeld is om de gelijkwaardigheid te controleren. Interessant idee en zeker hersenstrekkend om over dergelijke uitdagingen na te denken. (Ik moet bekennen dat ik meteen begon na te denken over het Sudoku-probleem zodra hij het ter sprake bracht.)

Afronden

Theo besluit met een discussie over methodologieën die belangrijk zijn bij productiegebruik, rond beperkingen, regressies en vergelijkingen met oudere RTL-modellen. Ook de uitdagingen om te weten of wat u controleert daadwerkelijk overeenkomt met de natuurlijke taalspecificatie op het hoogste niveau.

Zeer energieke talk, zeker de moeite waard om te bekijken hier op SolvNet!

Deel dit bericht via: