Funksjonell verifisering - Functional verification

I elektronisk designautomasjon er funksjonell verifisering oppgaven å verifisere at den logiske designen samsvarer med spesifikasjonen. I hverdagslige termer forsøker funksjonell bekreftelse å svare på spørsmålet "Gjør dette foreslåtte designet det som er ment?" Dette er en kompleks oppgave, og tar mesteparten av tid og krefter i de fleste store elektroniske systemdesignprosjekter. Funksjonell verifisering er en del av mer omfattende designverifisering , som foruten funksjonell verifisering, vurderer ikke-funksjonelle aspekter som timing, layout og strøm.

Funksjonell verifisering er veldig vanskelig på grunn av det store volumet av mulige testcases som finnes i til og med en enkel design. Ofte er det mer enn 10 ^ 80 mulige tester for å verifisere en design omfattende - et tall som det er umulig å oppnå i løpet av livet. Denne innsatsen tilsvarer programverifisering , og er NP-hard eller enda verre - og det er ikke funnet noen løsning som fungerer bra i alle tilfeller. Imidlertid kan det angripes ved mange metoder. Ingen av dem er perfekte, men hver kan være til hjelp under visse omstendigheter:

  • Logisk simulering simulerer logikken før den bygges.
  • Simulasjonsakselerasjon bruker maskinvare med spesielle formål på logikksimuleringsproblemet.
  • Emulering bygger en versjon av systemet ved hjelp av programmerbar logikk. Dette er dyrt, og fremdeles mye tregere enn den virkelige maskinvaren, men størrelsesordrer raskere enn simulering. Det kan for eksempel brukes til å starte opp operativsystemet på en prosessor.
  • Formell bekreftelse forsøker å bevise matematisk at visse krav (også uttrykt formelt) er oppfylt, eller at visse uønskede oppførsler (for eksempel dødelås) ikke kan oppstå.
  • Intelligent verifisering bruker automatisering for å tilpasse testbenken til endringer i registeroverføringsnivåkoden .
  • HDL-spesifikke versjoner av lo og annen heuristikk brukes til å finne vanlige problemer.

Simuleringsbasert verifisering (også kalt ' dynamisk verifisering ') er mye brukt for å "simulere" designen, siden denne metoden skalerer opp veldig enkelt. Stimulus er gitt for å utøve hver linje i HDL-koden. En testbenk er bygget for å funksjonelt verifisere designet ved å gi meningsfulle scenarier for å sjekke at gitt visse innspill, utfører designen til spesifikasjon.

Et simuleringsmiljø er vanligvis sammensatt av flere typer komponenter:

  • Den generatoren genererer inngangs vektorer som brukes til å søke etter uregelmessigheter som eksisterer mellom den hensikt (spesifikasjoner) og gjennomføringen (HDL Code). Denne typen generator benytter en NP-komplett type SAT Solver som kan være beregningsdyktig. Andre typer generatorer inkluderer manuelt opprettede vektorer, grafiske baserte generatorer (GBM) proprietære generatorer. Moderne generatorer lager direkte-tilfeldige og tilfeldige stimuli som er statistisk drevet for å verifisere tilfeldige deler av designet. Tilfeldigheten er viktig for å oppnå en høy fordeling over den enorme plassen til tilgjengelige innsatsstimuli. For dette formål spesifiserer brukere av disse generatorene med vilje kravene til de genererte testene. Det er generatorens rolle å tilfeldig fylle dette gapet. Denne mekanismen lar generatoren lage innganger som avslører feil som ikke blir søkt direkte etter av brukeren. Generatorer fordeler også stimuli mot design hjørne tilfeller for å stresse logikken ytterligere. Forspenning og tilfeldighet tjener forskjellige mål, og det er avveininger mellom dem, og derfor har forskjellige generatorer en annen blanding av disse egenskapene. Siden innspillene til designen må være gyldige (lovlige) og mange mål (for eksempel forspenning) skal opprettholdes, bruker mange generatorer teknikken for begrensningstilfredshet (CSP) for å løse de komplekse testkravene. Legaliteten til designinngangene og det forspenningsarsenal er modellert. De modellbaserte generatorene bruker denne modellen for å produsere riktig stimuli for målutformingen.
  • De driverne oversette de stimuli som frembringes av generatoren inn i selve innganger for utformingen i henhold til verifikasjon. Generatorer lager innspill på et høyt abstraksjonsnivå, nemlig som transaksjoner eller samlingsspråk. Driverne konverterer denne inngangen til faktiske designinnganger som definert i spesifikasjonen for designets grensesnitt.
  • Den simulatoren frembringer utgangene fra utformingen, basert på utformingen nåværende tilstand (tilstanden til flip-flops) og de injiserte innganger. Simulatoren har en beskrivelse av nettverkslisten. Denne beskrivelsen er laget ved å syntetisere HDL til en netteliste med lavt gate-nivå.
  • Den monitor omdanner tilstanden i utforming og dens utganger til en transaksjon abstraksjonsnivå slik at den kan lagres i en 'rille-board' database som skal kontrolleres senere.
  • Kontrolløren bekrefter at innholdet i 'score-boards' er lovlig. Det er tilfeller der generatoren skaper forventede resultater, i tillegg til inngangene. I disse tilfellene må kontrolløren validere at de faktiske resultatene samsvarer med de forventede.
  • Voldgiftslederen administrerer alle de ovennevnte komponentene sammen.

Ulike dekningsberegningsmetoder er definert for å vurdere at designet er utøvd tilstrekkelig. Disse inkluderer funksjonell dekning (har all funksjonalitet av designet blitt utøvd?), Uttalelsesdekning (har hver linje av HDL blitt utøvd?), Og filialdekning (har hver retning av hver gren blitt utøvd?).

Verktøy

Se også