ŞALIŞAN YONGALAR ÜRETMEK

ÇALIŞAN YONGALAR ÜRETMEK

Y azanlar: Davld SHEPHERD, Gr *g VVİLSON** Çavlrl: Erhan Y ÜCEER'"

Kullandığınız bilgisayarın uygun olarak çalıştığını nereden biliyorsunuz?

Programlarınız virüs taşıyabileceği gibi mikroişlemcinizin tasarımı da yanlış olabilir. Matematiksel mantık üzerine kurulmuş yeni bir yaklaşım güvenilmeye değer yongalar üretebilir.

B ir söylentiye göre bilgisayar mühendisleri uçağa binmezlermiş, çünkü uçağı kontrol eden elek tronik yongaya güvenmiyorlarmış. Ortalama bir mikroişlemci, on veya yüz binlerce aktif bi leşenden oluşan çok karmaşık bir aygıttır. Tasarımdaki en küçük hata yonganın hiç çalışmamasına, daha da kötüsü her bir iki milyon işlemde bir hata yapmasına yol açar. Bir mühendis bir yongayı kağıt üzerinde doğru ola rak tasarlasa da tasarımın donanım olarak gerçekte uy gulanması yanlış olabilir. Bir mimar bir köprüyü doğru ola rak tasarlayabilir, fakat inşaatı yapan kişi ozaliti yanlış

(*) "Making Chips That Work", New Scientist. 13 Mayis 1989, sf. 61 64 (**) D. Shephard İnmos şirketi için yonga tasarlamaktadır. G. VVilson Edinburgh Üniversitesi'ndeki Edinburgh sayar (supercomputer) projesi'nde çalışmaktadır. (" *) ODTÜ Elektrik Elektronik Müh. Bolümü 4. Sınıf öğrencisi

olarak tasarlayabilir, fakat inşaatı yapan kişi ozaliti yan lış okur ve kirişleri mimarın belirttiğinin yarı kalınlığında kutlanırsa köprü germe ve gerilme kuvvetleriyle çekebi lir. Bu örneklere benzer olarak da, kağıttaki tasarımdan • : jygu amaya hatalı olarak geçirilen bir yonga \ : ıı birasında yanılabilir.

Mikroişlemciler yaşam destek sistemleri, tren ve uçak kontrolları gibi bir çok uygulama alanları bulurlar ve bun dan dolayı güvenilir olmak zorundadırlar. Hatta sıradan bir çamaşır makinasına bile yanlış bir parça koymak üre ticinin çok para kaybetmesine yol açabilir. Günümüzde bazı yonga üreticileri matematiksel mantık kullanarak yonga tasarımında yeni tekniklere geçmişlerdir. Ağırlığını İngiltere ve ABD'nin oluşturduğu bir düzineye yakın araştır ma grubu biçimsel yöntem adını verdikleri bu yön temi geliştirmekedirler. Bu teknikler yongaları daha gü venli kılacaktır.

İngiliz yonga üreticisi olan Inmos firması ticari olarak yonga üretiminde biçimsel yöntemi kullanan Hk şirketler den biridir. Şirket 1986 yılında serisinin üçüncüsü olan ve geleneksel işlemcilerden daha güçlü ve hızlı işlem ya pabilen bir paralel işlemci olan T800 yongasını piyasaya çıkardı. Bu yonga çok büyük sayıların yer aldığı bilimsel hesaplamalar için idealdir.

T800 bir çok yongadan daha karmaşıktır. İçinde bir ana işlemci ünite, dört iletişim hattı ve dört kilobayt bellek vardır ve bunların hepsi bir çok tasarımda olduğu gibi ayrı değil bir tek yonga üzerindedir.

Ayrıca yongada kesirleri de içeren ve bilgisayarın çok büyük sayı gruplarını saklayıp işletebilmesine yardımcı olan bir ünite de yer almaktadır. Buna uçuşan nokta (floating polnt) aritmetiği adı verilmektedir. Herhangi bir sayıyı, bir tam sayının onun kuvvetleriyle çarpımı ola rak gösterir. Örneğin 4096 sayısını 4.096x 103 şeklinde göstermek olasıdır. Bilgisayar üs olan 3'ü 4.096'dan ayrı olarak saklar ve 4.096 sayısı ondalık noktası "uçuşan" olarak 4096 şeklinde saklanır. Ne yazık ki uçuşan nok talı sayılarla işlem yapmak daha karmaşık olduğundan tam sayılarla işlem yapmaktan daha yavaştır. Bilgisayar dan 1.2x 103 ve 3.3 x 10"1 gibi iki sayıyı toplaması isten diği zaman 4.5 x 102 cevabını almamak için bilgisayarın bazı kaydırma ve düzenlemeler yapması gerekmektedir. Büimsel hesaplamaların hızı bilgisayarın uçuşan nokta aritmetiğini başarma hızına bağlı olduğu için yonga ta sarımcıları bu hesaplamaları hızlandırmak için özel uçuşan nokta aritmetiği üniteleri (FPU floating point units) kullanmaktadırlar.

T tarımcılar FPU'yu bilgisayarın diğer parçalarıyla aynı yonga üzerine koymakla bu yonganın kullanıldığı sistem nn genel hızını artırmayı umuyorlar. Yonga üzerindeki : ı ^J'nun içinde, yazmaç adı verilen ve çok hızlı olan bel li.k hücreleri, uçuşan nokta aritmetiği yapacak olan

• e ve bu üniteleri birleştiren iletişim hatları (bus)

vardır. Küçük ve değiştirilemeyen bir program olan mik rokod FPU'nun veri oluşturan rakamlara neler yaptığını, bu değerlerin hangi yoldan yazmaçlara, oradan bilgi sayarın belleğine gittiğini ve geri döndüğünü kontrol eder.

Mikrokod FPUya gönderilen komutları mikrokomutlar dü zeyine böler. Bu komutların her biri tek bir ünite veriyi bir yazmaçtan ötekine aktarır veya veriyi toplayıcı veya çarpıcı gibi aritmetik ünitelerden birine yollar. FPU'yu bu kadar karmaşık yapan şey, maksimum hız elde edebil mek için üreticilerin her bir mikrokomuta olası en çok işi yaptırma çabalarıdır. Bir tek komut, bir sayının bir par çasını bir yazmaca kaydırırken, ötekinin işaretini kontrol edip diğer bir üçüncü sayıyla toplama işlemine girebilir.

T800 gibi bir yonganın doğru tasarlanıp tasarlanmadığını görmenin en açık yolu onu yoğun biçimde denemektir. Yongaya olası tüm girdileri verip çıktıları inceleyerek teo ride yonganın doğru çalıştığı söylenebilir. Örneğin topla mayı kontrol etmek için yongaya tüm olası sayı çiftleri girdi olarak verilip her bir çıktı incelenerek yonganın doğru çalıştığı söylenebilir. Fakat harcanması gereken çabanın büyüklüğü bu denemeyi olanaksız kılar.

Bunu görebilmek için bit'lik bilgiyi ele alalım. Bu bilgi iki durumda olabilir; 0 veya 1. iki bit birarada dört olası du rumda bulunabilir: 00, 0 1 , 10, 11. üç bit birarada sekiz olası durumda bulunabilir. Genelde, n bit kendi arasında

2" değişik şekilde dizilebilir. T800 gibi birçok iç bellek bitlerine, artı, değişik giriş ve çıkış sinyal yollarına sahip bir mikroişlemcide ise tüm evrendeki parçacıklardan daha çok durum olabilir. Saniyede milyonlarca test ya pılsa bile, bu yolla yonganın doğru çalıştığı kanıtlana maz.

Sonuç olarak tasarımcılar yongayı tüm olası durumları temsil ettiğine inandıkları durumların küçük bir alt küme siyle test ederler. Bu küçültülmüş alt küme bile, hala bir kaç milyon test kapsıyor olabilir, bundan dolayı yongayı işletebilmek birkaç gün alabilir. Durumu daha da kötüleş tirmek gerekirse, tasarım sırasında denemek için bir yonga bulunmadığından, yongaya benzeşen (simulate) bilgisayar pogramları kullanılmaktadır. Bu bilgisayarlar, tasarlanan yongadan yüzlerce hatta binlerce kez daha yavaş çalıştıkları için test zamanını aylara çıkarırlar. T800'ün taklit edilmesi sırasında, uçuşan nokta aritme tiğini test etmek için yapılan ve gerçeğin 1/500 hızında olan bir test neredeyse üç hafta sürmüştür.

Doğruluğu test ederek göstermenin doğuracağı en son sorun da test sonuçlarının değerlendirilmesidir. Milyon larca test sonucunu tek tek incelemenin hiç bir pratik so nucu olmadığından, tasarımcılar yeni yongayı ya bilgi sayardaki taklidiyle ya da piyasada bulunan başka bir yongayla karşılaştırmak zorundadırlar. Ama bu kez de tasarımcılar karşılaştırmada kullandıkları yonganın hatalı olabilmesi sorunuyla karşılaşabilirler. Inmos'da yapılan

2 0 4 375 ELEKTRİK MÜHENDİSLİĞİ

ilk çalışmalarda böyle bir sorunla karşılaşılmış, referans olarak kul lanılan yonga birkaç kez hatalı çık mıştır. Inmos'un tasarım ve deneme yerine geliştirmekte olduğu yöntem lerle yonganın son halinin doğru ola rak çalışması garanti altına alına caktır. Bu yöntemler bilim adam larının yüzeysel olarak benzemeyen iki terimin aslında aynı olduğunu göstermek için matematik eşitlikleri yeniden düzenlemelerine benze mektedir. Tasarımcılar yongaya yüksek düzeyli bir tanımlama yapa rak işe başlarlar. Bu tanimlama her işlemden önce ve sonra hangi bi leşen tarafından ve nasıl yapıldığını açıklamaksızm yonga bileşenlerinin durumlarını açıklar. Daha sonra ta sarımcılar matematik teoremlerin açıklanmasına benzer yöntemler kullanarak bu tanımlamayı yonganın nasıl yapacağını ona çevirirler (translate). Bu anlatıma genellik le işlemsel anlatım adı verilir, çünkü matematiksel mantıkla oluşturulmuş ve hesap yapmada kullanılan bir dizi işlemden meydana gelmektedir.

Son olarak tasarımcılar bu işlemler deki komutları düşük düzeyli mikro kom utlar olarak, bir başka deyişle yonganın okuyabileceği bir bilgi sayar koduna çevirirler. Bu yon ganın her bir bileşenini kontrol ede cektir. Çünkü bu işlemin her basamağındaki dönüşümler sadece tanımlamanın belirtildiği yolla değişir, yani ortaya çıkan mikrokod özgün tasarımın doğru bir çevirisi ol malıdır.

Inmos'taki tasarımcıların karşılaş tıkları ilk sorun FPU yapısını oluştur duktan sonra, onu doğru çalıştıra cak mikrokodun nasıl yazılacağı ol muştur. Başlangıç olarak tasarımcılar Amerikan. Elektrik ve Elektronik Mühendisliği Ensti tü'sünden uçuşan nokta aritmetiği için bir standart aldılar. IEEE 754 olarak bilinen bu standart detaylı olarak her aritmetik işlemin sonucu nun nasıl hesaplanacağını anlat maktadır. Uygulayıcının lisansı için bir şey öngörülmemiştir, bir uygula ma başarılı sonuç da verebilir, tersi de olabilir. Ne yazık ki IEEE bu standardı işe yaramayacak bir dil

Bölüm 1: Uçuşan Noktalar İçin Bir Mantık Testi

Geotf Barrett ve Inmos'taki tasarımcıların belirli bir komut için nasıl mikrokod geliştirdiklerini anlamak amacıyla, bir uçuşan nokta sayısının eşdeğer bir tam sayıya çevrilişi örneğini ele alalım. Bu iş genellikle daha önce ı saklan mış bir tam sayıyla toplama yapabilmek amacıyla yapılır. Bu çevirim yapıl ırken, öncelikle FPU uçuşan nokta sayısının değerinin bir tam sayiya çevrilip çevri lemeyeceğini test eder. Bunun yapılma nedeni saklanabilen uçuşan nokta sayılarının sınırının tam sayıların sınırından çok büyük olmasıdır.

Eğer uçuşan nokta sayısının değeri bilgisayarın saklayabileceği en büyük artı sayı dan büyük, ya da en küçük eksi sayıdan küçükse, çevirimi yapmak anlamsız bir sonuç ortaya çıkarır. Bu test "Test Integer Range" adı verilen bir komut tarafından yapılmıştır. Buna ait Z ta nımlaması, yazmaç X ve hata belirleyicisi FLAG olarak FPU üzerine bir bellek hücresi şeklinde yazılır. Eğer X'te saklanan değer bilgisayarın tam sayı saklama sınırının dışındaysa, FLAG TRUE (doğru) vererek bir hata olduğunu gösterir. Tersi durumlarda FLAG değişmeden kalır. Z mantık gösteriminde bu olay aşağıdaki gibi gösterilir.

Test Integer Range X,X': Ftoating Point Register FLAG, FLAG: {TRUE, FALSE} value (X) e (valid floating point representations of 32 bit integers}

Minlnt S value (X) <, Maxlnt=> (FLAG'=FLAG) (value'(X)<Minlnt)or(Maxlnt< value (X))=>(FLAG1=TRUE)

Bu tanımlamaya "şema" adı verilir. Şemanın üst yarısı kullanılan değişkenleri verir burada X sayısı ve hata belirteci FLAG olduğu gibi. İlk satır X'in uçuşan nokta sayısı kapsayan bir yazmaç olduğunu belirtir ve FLAG sadece TRUE (doğru) veya FALSE (yanlış) durumlarında olabilir. (Gerçek Z tanımlamasında "valid floating point repre sentations of 32 bit registers* (uçuşan nokta sayılarının geçerli 32 bit'lik gösterimi) deyimi bu düşünceyi daha iyi açıklayan matematiksel bir gösterimle verilmiştir.) Üs işareti işlemden sonra değişkenin değerini belirtir.

Şemanın alt yarısı değişkenlere bazı sınırlamalar getirir. Bu sınırlamalar işîamin etki lerini tanımlar. İlk satır işlemin geçerliliğim onaylamak için bir testtir eğer X'in uçuşan nokta sayısı olarak değeri 32 bit'lik bir tam sayı değeri vermiyorsa hiç bir iş lemin bir anlamı kalmaz. Bu komutu kullanan kişi yukarıdaki koşulu mutlaka sağla malıdır.

Şemanın alt yarısındaki ikinci satır X'in değerinin işlemden sonra aynı kaldığını söy lemektedir, başka bir deyişle X geçerli olmayan bir sayı olsa bile değişmemiştir. Bu işlem sırasında kazara sayının değişmesi yan etkilerden kurtulmak için tanımlamaya verilmiştir, tersi durumda olayları izlemek güçleşir.

Üçüncü satır, eğer X doğru sınırlar içindeyse, yani value (X) Minlnt ve Maxlnt arası

nda ise, FLAG değişmez ve bu önceki durumunu korur Tersi durumda, yani X doğru

sınırların dışındaysa, dördüncü satır FLAG'in TRUE (doğru) sınırların dışındaysa,

dördüncü satır FLAG'in TRUE (doğru) durumunu göstereceğini belirtir. Value () fonk

siyonunun ve yazmacın 32 biflik geçerli bir sayı kapsadığının test edilmesi tüm FPU

tanımlamasının bir parçasıdır.

FPU'nun yapması gerekenin yukandaki tanımlamalara uymak olduğu occam prog

ramlama dili kullanarak yazılan aşağıdaki işlem basamaklanyla kanıtlanabilir:

IF (Minlnt<= value (X)) AND (value (X) <=Maxlnt)

"eğer X'in değeri"

SKIP

"tamamsa birşey yapma"

"mUE

"fakat tüm diğer durumlarda"

FLAG:=TRUE

"FLAG1 TRUE (doğru) konumuna getir."

Testi değerlendirmek için aşağıdaki satıra ve bu basit programın FPU mikrokomutları cinsinden yazılmış biçimine gerek vardır. (Minlnt<= value (X)) AND (value (X) <= Maxlnt)

**

ları haline getirebilirsiniz. Bu işin içeriği sırasında bol

kitap edinme gerekliliği ve hata yapma olasılığı vardır,

örneğin Bölüm 1'deki dört satırlık program, her biri daha

sonra bir düzine ya da daha fazla mikrokomutlara

dönüşecek olan yarım sayfa dolusu bilgisayar komutuna

dönüşebilir. Bunları kalem ve kağıtla izlemek ise tasarım

cıların ilk başta biçimsel yöntem kullanarak kaçındıkları

kadar hata yapılmasına yol açar. Fakat kitap edinmek ol

dukça mekanik bir işlemdir ve bir bilgisayar destekli ta

sarım (CAD) sistemi işin ,oğunu halleder.

Bir kelime işlemcinin içerlek yazma, satır uzunluğu, sayfa biçemi gibi bilgileri aklında tutması gibi Oxford Programlama Araştırma Grubu tarafından geliştirilen bir CAD sistemi de program dönüşümlerini aklında tutar. Hangi kuralların kullanıldığını ve o ana kadar tanımla manın ne kadarının çevrildiğini hatırlar. Bu sistem bir occam programını okur ve sonra programın bölümlerinde dönüşüm dizilerini uygular. Sistem programın o anki du rumunu gösterir ve tasarımcıya hangi kuralların uygula nacağını soran bilgisayar daha sonra seçilen kuralı uy gular, sonucu yazar ve tasarımcıyı tekrar uyarır. Tasarımcılar sık kullanılan kural kombinasyonlarına isim verebilir ve onları gerekli aritmetik teoremleri işleme koy madan kaydedebilirler.

olan İngilizce ile yazdı. Bir fizik probleminin çözümünün ilk aşamasının onu, bir dizi denkleme çevirmek olması gibi, FPU tasarımındaki ilk iş IEEE 754 standardının ma tematiksel mantığa çevrilmesi oldu. Oxford Programlama Araştırma Grubu'ndan Geoff Barett IEEE 754 stan dardını "Z" adıyla özel bir mantıksal gösterime çevirdi. Z gösteriminde her bir ayrı kural bir işlemin yapılması için sağlanması gereken koşullar ve FPU bileşenlerinin du rumları cinsinden o işlemi tanımlar. Barrett, bundan sonra uçuşan nokta aritmetiğini IEEE tanımlamasına göre yürütecek bir program tasarlayabilmiş ve bu prog ramın doğruluğunu kanıtlayabilmiştir. Barrett ve Inmoslaki tasarımcılar bir uçuşan nokta sayısını eş değer tam sayıya çevirme örneğinde olduğu gibi FPU ko mutlarına mikrokod geliştirmek için kullandılar.

Tasarımcılar IEEE 754 standartmdaki her işlem için bu şekilde Z tanımlamaları yazdılar. Bu tanımlamalar ne yapılması gerektiğini söylerken, nasıl yapılacağını belirt mezler. Mikrokod yazıcılarına daha sonra gereken şey ise, her Z tanımlamasını karşılayacak ve FPU'nun sürdü rebileceği işlemler cinsinden yazılmış işlem basamakları oldu. Bu yazıcılar işlem basamaklarını yazmak için occam adı verilen basit bir bilgisayar dili kullandılar ve daha sonra geriye doğru çalışarak occam kodunun özgün Z tanımlamalarını sağladığını gösterdiler. Tasarım lardaki kanıtlamaları ekibin bir diğer üyesi David Shep herd tamamladı.

Occam'ın dönüşüm kurallarını kullanarak yüksek dü zeyli işlem basamaklarını daha uzun ve FPU'nun mikro kod komutlarını kullanan düşük düzeyli işlem basamak

FPU'nun ilk tasarımı dokuz ay almıştır. Geleneksel tek niklerle, eşdeğer bir ünite tasarlamak ise iki yıl sürmek tedir. Tasarım ekibinde bir mimar, üç elektrik mühendisi, bir bilgisayar uzmanı ve iki matematikçi vardı. Biçimsel yöntem kullanılarak yazılan tüm mikrokodlar ilk seferinde çalıştı, fakat biçimsel yöntem kullanılmadan yazılan bazı FPU konutları çalışmadı. Buna ek olarak da ekip biçimsel yöntemi kullanmaya başlamadan önce FPU'nun donanım tasarımında bir çatlak meydana geldi.

Yonganın ikinci kez gözden geçirilişinde, daha önce elle yazılan tüm FPU komutları bu kez biçimsel yöntem kulla narak yeniden yazıldı. Ne yazık ki bu yeni bir hata getir di.Son anda elle yazılmış bir mikrokod değiştirilirken yanlışlıkla iki mikrokomutun adlarının yerlerini değiştirdi ler. Sonuç olarak tüm yenileme boşa gitti. Çünkü böyle hatalar gelişme süresinden altı ile sekiz hafta götürürler ve böylece biçimsel metodun yonga tasarımının her tür işi için geliştirilmesi gerektiği ortaya çıktı.

Günümüzde Inmoslaki ekip İngiltere'deki tüm araştırma grupları gibi bu işle uğraşmakta. Inmos'un geliştirdiği ve "Şişman Freddie" olarak bilinen CAD sistemi, toplayıcılar gibi üniteleri, daha küçük ve basit altüniteier olarak yon gaya tanımlayan hiyerarşik bir donanım tasarım dili (hardware design language HDL) kullanmaktadır. Bu alt üniteler ilerde mantıksal "VE" (a nd) ve "VEYA" (or) işlem çıktılarını veren en düşük düzeyli transistöre kadar bölünürler. (Mantık geçitleri iki sinyal alırlar: iki sin yal "açık" "TOPLA" (add); bir sinyal "açık" "VEYA" (or) demektir.) Bu şekilde çalışmak tasarımcıların sık kullanı lan bileşenler hakkında daha sonraki tasarımlarda kul lanmak üzere bir kitaplık oluşturmasını sağlar.

206 375 ELEKTRİK MÜHENDİSLİĞİ

Bölüm 2: Occam ile Program Kanıtlanması

Araştırmacılar iki nedenden ötürü oceam'ı biçimsel yöntem programlama dili olarak seçtiler. İlk olarak, diğer dillerin aksine, occam'la birkaç işin birarada yapıldığı programlar yazmak olasıdır. Bu olay, eğer FPU'daki bazı yazmaç ların ve aritmetik ünitelerin sıralı hareketlerinin program tarafından anlatımı içinse kesinlikle gereklidir.

Örneğin occam'ın SEQ

ve PAR adı verilen iki

işlemi vardır. SEQ ar

PAR

dışık (sequentlal) an lamına gelir ve bir grup işlemin arka arkaya yapılacağını belirtir.

SEQ

B

PAR ise koşut ( p a r ı l

lel) anlamındadır ve bir

grup işlemin aynı anda yapılacağını belirtir. Aşağıdaki tanımlama

IF testi / \ test2

A,B ve C işlemlerinin Şekil Vdeki gibi yapıla

actionl

actton2

cağını anlatır.

(Occam'da içeriye ya zarak SEQ işleminin B ve C Özerinde, PAR iş

finalAcöon

J

leminin ise A ve ŞEQ

üzerinde etkili olduğu belirtilir.)

B Time

\ IF test 1 / \ test 2

/ action 1 linalAction

\ action 2 fınalAction

I

İkinci olarak, occam'ın çok iyi tanımlanmış matematiksel özellikleri vardır ve bunlar occam programlarıyla kanıtlamayı Basic ve Fortran gibi dillerle yapıl mış programlarla kanıtlamaktan daha kolay kılar. Bu kanıtlara ait kurallar, Edinburgh'tan Robin Milner ve Oxford'dan Tony Hoare'un teorik çalışmaları esas alınarak, yine Tony Hoare ve Bili Roscoe tarafından Oxford'da geliştiril* di.

Occam'ın kuralları, programlar arasındaki bir grup cebirsel eşitliktir. Cebirde ax(b+c)=(axb)+(axc) eşitlikleri olduğu gibi, occa m programları işlemleri arasında da benzer eşitlikler vardır.

SEQ IF tMt acttonl (NOT**)

«Cüon2

«naMctton

III

IF tast acüonl (NOT test)

actkxı2 «naMction

Bu eşitliklerin en basitlerinden biri de yukarıdaki dağılma özelliğine benzerlik gösterir. Bir programın, uygulanan test doğruysa action 1 tarafına, eğer test yanlışsa action 2 tarafına, ama so nuçta kesinlikle final action tarafına hareket ettiği bir sapak noktasını (branchlng polnt) ele alalım.

Final Action, eğer test doğruysa önce a ct i onl daha sonra flnal actıon veya eğer test yanlışsa önce ac tlon2 daha sonra flnal actıon durumunu belirtmekle eşdeğerdir. Y ukarı daki kural, programların ortak noktalarında onların boyutunu küçültmek için kullanılır. Diğer kurallar ve kombinasyonları, programın yaptığı işi değiştirme den yolunu değiştirmek açısından kullanıcıya yardımcı olur.

D

"HDL'nin doğruluğunu kanıtlamak hala bir sorundur. HDL bileşenlerin nasıl davrandıklarını değil ne şekilde bağlanacaklarını tanımlar. ,.

Inmos'un bugünkü CAD sistemi kural ları otomatik olarak kontrol edebilir. Her bileşenin tanımında o bileşenin nasıl kullanılacağını anlatan bir yönetmelik vardır. Örneğin bazı bileşenlerin sınırlarında üretim toleransları için boş yer bırakmak gereklidir. Eğer tasarımcı bu tip bileşenleri çok yakına getirirse CAD sistemi tasarımcıyı uyarır ve ta sarımı veritabanma eklemeyi reddeder. Buna ek olarak, tasarımcı bir modülün planını bitirdiği zaman, doğru bileşenle rin kullanılıp doğru bağlan dıkları HDL tanımlamalarına göre kontrol edilir. Bu sistem tasarımcıların HDL sistemine uygun devreler üretmelerini sağlar.

HDL'nin doğruluğunu kanıtlamak hala bir sorundur. HDL bileşenlerin nasıl davrandıklarını değil ne şekilde bağla nacaklarını tanımlar. Günümüzde ta sarımcılar bunu kontrol etmek için bilgi sayar kullanmaktadırlar. Fakat Inmos'un T800 deneyiminde olduğu gibi bu da hataları önleme konusunda güve nilir olmaktan uzaktır. Inmos ekibi bugün her bileşenin özelliklerinin Z tanı mlamalarını HDL kitaplığına eklemekte dirler, Tasarımcılar bir kere yongayı planladılar mı, tanımlamaları kullanarak yonganın tasarımda beklenen özellikle ri karşıladığı kanıtlanabilir. Sistem ta sarımcıların donanım ve yazılım, yük sek düzeyle düşük düzey arasında hareket etmesine izin verir. Bu büyük ölçüde verimlürği artırır.

Bütün bunlar Kapalı bir kutu olan mo

dern bilgisayar bilimini mühendislik di

siplinine çevirmek için harcanan büyük

çabanın bir parçasıdır, Kimse bir inşaat

mühendisinden bir köprüyü ayakta du

rana kadar iki üç kez yapmasını bekle

mez. Biçimsel yöntemin yayılmasıyla,

elektronik mühendisleri tarasımlarında

aynı güvenilirliğe u^JşıfiByıt< ummakta,

ürünlerini daha güv«B&)V$ rucuza üret

meye çalışmaktadırlar.^ ; 6 I ı L

MÜHENDİSLİĞİ