Intel Keynote On Formal A Mind-Stretcher

Återutgiven av Platon

anhängare: 0

Synopsys har publicerat ett fascinerande föredrag på SolvNets webbplats av Dr. Theo Drane från Intel Graphics. Ämnet är datapath-ekvivalenskontroll. Kan låta som bara en annan Synopsys VC-formell DPV-godkänd men du borde titta på den ändå. Detta är en tankeexpanderande diskussion om användningen av och övervägandena i formella som tar dig bortom den rutinmässiga användarguiden till mer fascinerande territorium.

Intel Keynote på formell

Intellektuell förståelse kontra provtestning

Testdriven simulering i alla dess former är utmärkt och ofta oersättlig för att verifiera riktigheten av en designspecifikation eller implementering. Det är också lätt att komma igång. Skriv bara ett testprogram och börja simulera. Men baksidan av den enkelheten är att vi inte behöver det fullständigt förstå vad vi testar för att komma igång. Vi övertygar oss själva om att vi har läst specifikationen noggrant och förstår alla hörnfall, men det krävs inte mycket komplexitet för att överväldiga vår förståelse.

Formal uppmuntrar dig att förstå funktionaliteten på en djup nivå (åtminstone om du vill leverera ett värdefullt resultat). I exemplet ovan lyckas en enkel fråga – kan z någonsin vara alla ettor – inte visa ett exempel i en miljard cykler på en simulator. Inte förvånande, eftersom detta är ett extremt hörnfall. Ett formellt test ger ett specifikt och mycket icke-uppenbart exempel på 1 sekunder och kan bevisa att detta är det enda fallet på något kortare tid.

OK formell gjorde vad dynamisk testning inte kunde göra, men ännu viktigare lärde du dig något som simulatorn kanske aldrig har berättat för dig. Att det bara fanns ett möjligt fall där det tillståndet kunde inträffa. Formal hjälpte dig att bättre förstå designen på en intellektuell nivå, inte bara som en probabilistisk sammanfattning över en begränsad uppsättning testfall.

Specifikationsproblem

Theos nästa exempel är baserat på en buggautomat (så kallad för att när du trycker på en knapp får du en bugg). Detta ser ut som ett ganska enkelt C till RTL-ekvivalenskontrollproblem, C-modell till vänster, RTL-modell till höger. En överraskning för Theo under hans tidiga dagar i formella tider var att högerförskjutningsbeteendet i C-modellen inte är helt definierat i C-standarden, även om gcc kommer att bete sig rimligt. Däremot kommer DPV att klaga på en missmatch i en jämförelse med RTL, som sig bör. Odefinierat beteende är en farlig sak att lita på.

Formell som en buggautomat

Speciell jämförelse mellan C och RTL kommer med andra faror, särskilt kring bitsbredder. Trunkering eller förlust av en bärbit i en mellansignal (#3 ovan) är bra exempel. Är dessa specifika problem? Kanske en gråzon mellan spec och implementeringsval.

Utöver likvärdighetskontroll

Det primära syftet med DPV verkar vara att kontrollera likvärdighet mellan en C- eller RTL-referens och en RTL-implementering. Men det behovet är relativt sällsynt och det finns andra användbara sätt som en sådan teknik kan tillämpas på, om än lite utanför lådan. Först en klassiker i implementeringsvärlden – jag gjorde en förändring, fixade en bugg – introducerade jag några nya buggar som ett resultat? Lite som SEQ-kontroll efter att du lagt till clock gating. Tillgänglighetsanalys i blockutgångar kan vara en annan användbar tillämpning i vissa fall.

Inte bara likvärdighetskontroll

Theo blir ännu mer kreativ och ber praktikanter att använda motexempel för att bättre förstå designen, lösa Sudokus or faktorisera heltal. Han erkänner att DPV är ett konstigt sätt att närma sig sådana problem men påpekar att hans avsikt är att bryta illusionen att DPV bara är till för att kontrollera likvärdighet. Intressant idé och säkert hjärnanstöjande att tänka igenom sådana utmaningar. (Jag erkänner att jag omedelbart började tänka på Sudoku-problemet så fort han nämnde det.)

Sammanfatta

Theo avslutar med en diskussion om metoder som är viktiga för produktionsanvändning, kring begränsningar, regressioner och jämförelser med äldre RTL-modeller. Också utmaningarna med att veta om det du kontrollerar faktiskt matchar specifikationen för naturligt språk på högsta nivå.

Mycket energigivande prat, väl värt att se här på SolvNet!

Dela det här inlägget via: