Garanterat rätt med formell verifiering på transistornivå
•
Av: Charlotta von Schultz
Verktygsleverantören Compass presenterade nyligen en verktygssvit som garanterar att kretsens fysiska nätlista har samma funktion som tidigare konstruktionsbeskrivningar.
Oanslutna nät, felvridna bussar och utgångar med fel polaritet är bara några smakprov på de problem som kan gömma sig i kretsens layoutade nätlista.
Men nu drar Compass sitt strå till stacken för att sådana fel skall upptäckas innan de hamnar på kisel. På Eurodac presenterade företaget en verktygssvit för formell, matematisk verifiering som klarar allt från register- till transistornivån. Företagets befintliga verifieringsverktyg VFormal spelar där en nyckelroll.
Ny på scenen är däremot Laybool, ett verktyg som skapar VHDL- eller Verilogkod utifrån en nätlista på transistornivå.
Hjälpmedlet, som sägs vara marknadens första, har utvecklats av SGS-Thomson. Det utgår från en Edif- eller Spicenätlista och granskar varenda nät för att se hur de logiskt påverkar konstruktionens övriga nät. Utdata är en fil med boolesk VHDL- eller Verilogkod som med VFormals hjälp sedan kan jämföras med den ursprungliga registernivåbeskrivningen. På så vis garanterar man att inga fel smugit sig in under konstruktionsarbetets gång.
Bara digital logik
Laybool bygger på så kallade binära beslutsdiagram och hanterar alla tänkbara digitala logiska funktioner - hundratusentals transistorer skall klaras av på några minuter. Det går däremot bet på analoga funktioner samt minneselement av DRAM-typ.
Verktyget kan även användas för att flytta en befintlig konstruktion till en ny kiselprocess eller kiselteknologi. Den nyskapade koden omsyntetiseras då mot den önskade målprocessen.
Compass passade även på att lansera en Verilogutökning av VFormal, som hittills enbart stött VHDL. Användaren kan numera exempelvis jämföra Verilogkod, VHDL-kod samt tvåspråkiga konstruktioner. Verktyget kostar runt 800 000 kronor för en tvåspråkig version eller 400 000 för ett enda språk. Laybool, som skall vara tillgängligt i början av 1997, väntas kosta drygt 600 000 kronor.