Intel Keynote On Formal A Mind-Stretcher

Publisert av Platon

Følgere: 0

Synopsys har lagt ut på SolvNet-siden en fascinerende tale holdt av Dr. Theo Drane fra Intel Graphics. Emnet er datapath-ekvivalenskontroll. Kan høres ut som bare en annen Synopsys VC-formell DPV-godkjenning, men du bør se den uansett. Dette er en tankevekkende diskusjon om bruken av og vurderingene i formelle forhold, som vil ta deg utover den rutinemessige brukerveiledningen til mer fascinerende territorium.

Intel Keynote på formell

Intellektuell forståelse versus prøvetesting

Testdrevet simulering i alle dens former er utmerket og ofte uerstattelig for å verifisere riktigheten av en designspesifikasjon eller implementering. Det er også enkelt å komme i gang. Bare skriv et testprogram og begynn å simulere. Men baksiden av den enkelheten er at vi ikke trenger det fullt forstå hva vi tester for å komme i gang. Vi overbeviser oss selv om at vi har lest spesifikasjonen nøye og forstår alle hjørnesakene, men det skal ikke mye kompleksitet til for å overvelde forståelsen vår.

Formal oppfordrer deg til å forstå funksjonaliteten på et dypt nivå (i hvert fall hvis du ønsker å levere et verdifullt resultat). I eksemplet ovenfor klarer ikke et enkelt spørsmål – kan z noen gang være alle 1-er – å demonstrere et eksempel i en milliard sykluser på en simulator. Ikke overraskende, siden dette er en ekstrem hjørnesak. En formell test gir et spesifikt og svært ikke-opplagt eksempel på 188 sekunder og kan bevise at dette er det eneste tilfellet på litt kortere tid.

OK formell gjorde det dynamisk testing ikke kunne gjøre, men enda viktigere lærte du noe simulatoren kanskje aldri har fortalt deg. At det bare var ett mulig tilfelle der den tilstanden kunne skje. Formal hjalp deg med å forstå designet bedre på et intellektuelt nivå, ikke bare som sannsynlighetsoppsummering over et begrenset sett med testtilfeller.

Spesifikasjonsproblemer

Theos neste eksempel er basert på en bug-automat (såkalt fordi når du trykker på en knapp får du en bug). Dette ser ut som et ganske enkelt C til RTL-ekvivalenssjekkproblem, C-modell til venstre, RTL-modell til høyre. En overraskelse for Theo i de tidlige dagene i det formelle var at høyreskiftadferd i C-modellen ikke er fullstendig definert i C-standarden, selv om gcc vil oppføre seg rimelig. DPV vil imidlertid klage på et misforhold i en sammenligning med RTL, slik det skal. Udefinert oppførsel er en farlig ting å stole på.

Formell som en feilautomat

Spesifikasjonssammenligning mellom C og RTL kommer med andre farer, spesielt rundt bitsbredder. Trunkering eller tap av en bærebit i et mellomsignal (#3 ovenfor) er gode eksempler. Er dette spesifikasjonsproblemer? Kanskje en gråsone mellom spesifikasjon og implementeringsvalg.

Utover ekvivalenskontroll

Det ser ut til at hovedformålet med DPV er å sjekke ekvivalens mellom en C- eller RTL-referanse og en RTL-implementering. Men det behovet er relativt sjeldent, og det er andre nyttige måter en slik teknologi kan brukes på, om det er litt utenfor boksen. Først en klassiker i implementeringsverdenen – jeg gjorde en endring, fikset en feil – introduserte jeg noen nye feil som et resultat? Litt som SEQ-sjekking etter at du har lagt til klokkeport. Reachability-analyse i blokkutganger kan være en annen nyttig applikasjon i noen tilfeller.

Ikke bare ekvivalenskontroll

Theo blir enda mer kreativ, og ber traineer om å bruke moteksempler for å bedre forstå designet, løse Sudokus or faktoriser heltall. Han erkjenner at DPV er en merkelig måte å nærme seg slike problemer på, men påpeker at hans hensikt er å bryte illusjonen om at DPV kun er for ekvivalenskontroll. Interessant ide og absolutt hjernestrekkende å tenke gjennom slike utfordringer. (Jeg innrømmer at jeg umiddelbart begynte å tenke på Sudoku-problemet så snart han nevnte det.)

Wrap up

Theo avslutter med en diskusjon om metoder som er viktige i produksjonsbruk, rundt begrensninger, regresjoner og sammenligninger med eldre RTL-modeller. Også utfordringene med å vite om det du sjekker faktisk samsvarer med toppnivå spesifikasjonen for naturlig språk.

Veldig energisk snakk, vel verdt å se her på SolvNet!

Del dette innlegget via: