Assertion'lar her girdi için kanıtlanır ya da kısa bir izle çürütülür.
Lumina Formal, Lumina Lint ve Lumina Sim ile aynı kaynakları okur; her eşzamanlı assertion, assume ve cover'ı denetleyici mantığa derler ve bunlar üzerinde üç motor çalıştırır. Her karşı örnek Lumina Sim'de tekrar oynatılır; yani raporladığı her hatayı simülatör de doğrular.
Lumina Formal başlangıç kılavuzundan
- BMC
- en kısa hatayı bulur
- k-induction
- kanıtlar
- IC3/PDR
- bir değişmezle kanıtlar
- Tekrar oynatılır
- her karşı örnek, simülasyonda
Lumina Formal ne yapar
Sırayla üç motor
Sınırlı model denetimi (BMC) en kısa hatayı arar, k-induction kanıtlayabildiğini kanıtlar, IC3/PDR de geri kalanı için tümevarımsal bir değişmez kurar ya da sınırdan daha derindeki bir hatayı bulur.
Güvenebileceğiniz karşı örnekler
Bir testbench tasarımı karşı örneğin yaptığı gibi sürer ve simülatörün kendi assertion motoru aynı hatayı raporlamak zorundadır. Tekrar oynatılamayan bir karşı örnek asla doğrulanmış hata olarak raporlanmaz.
Saatlerin her sıralaması
Birden fazla saat girişi varsa her adım, saat kenarlarının herhangi bir birleşimidir; böylece saatlerin vurabileceği her sıra denetlenir.
X her değer demektir
Sürülmeyen sinyaller, reset almamış flop'lar ve x sabitleri serbest değerlerdir; bir kanıt, X'in alabileceği her değer için geçerlidir.
Yazdığınız SVA
Sequence'ler, implication, disable iff, $past, $rose, $stable, $onehot ve diğerleri; sınırsız tekrar ve goto operatörleri otomatlarla denetlenir.
Canlılık (liveness)
s_eventually ve strong sequence'ler de kanıtlanır; bir hata, bir yükümlülüğün sonsuza dek beklemede kaldığı bir yol olan kement (lasso) olarak gösterilir.
CDC ve multicycle kanıtları
Lumina CDC'nin işaretlediği geçişler ve kısıtlarınızdaki multicycle yollar aynı tasarım modeli üzerinde kanıtlanır.
Sınırlarını açıkça söyler
Henüz denetleyemediği bir yapı, nedeniyle birlikte UNSUPPORTED olarak raporlanır; asla sessizce geçilmez.
Bir sonuç ne anlama gelir
- PROVED
Reset'ten itibaren her girdi dizisi için geçerli; kanıtlayan motorla birlikte
- FAILED at step n
Her adımda her girdiyi gösteren bir karşı örnek ve simülasyonda tekrar oynatmanın sonucu
- No failure up to step k
BMC hata bulmadı, kanıtlar da sonuca ulaşmadı
- COVERED at step n
Cover özelliğine ulaşılabilir; ulaşan izle birlikte
- UNSUPPORTED
Özellik henüz denetlenmeyen bir yapı kullanıyor; nedeni belirtilir
Denetlenen özellikler
- Direktifler
Modüllerde ve örneklerinde assert property, assume property, cover property
- Sequence'ler
##n, ##[m:n], [*n], [*m:n], and, or, intersect, throughout, within, first_match
- Özellikler
|->, |=>, #-#, #=#, not, and, or, iff, implies, if/else, nexttime, always [m:n], s_eventually
- Fonksiyonlar
$past, $rose, $fell, $stable, $changed, $onehot, $onehot0, $countones
- Sınırsız
##[m:$], [*m:$], goto [->n] ve ardışık olmayan [=n] tekrar, otomatlarla
- Reset
disable iff ve default disable iff, IEEE 1800'ün tanımladığı gibi asenkron
Sık sorulan sorular
Formal doğrulama nedir?
Tasarımın bir özelliğinin, yalnızca bir testbench'in sürdüğü girdiler için değil, olası her girdi dizisi için geçerli olduğunun matematiksel olarak denetlenmesidir. Özellik geçerli değilse araç, onu bozan girdi dizisini tam olarak verir.
Simülasyondan farkı ne?
Simülasyon, tasarımın çalıştırdığınız testlerde doğru çalıştığını gösterir. Formal ise bir assertion'ın asla başarısız olamayacağını kanıtlar ya da onu başarısız kılmanın en kısa yolunu bulur. İkisi birbirini tamamlar: Lumina her formal karşı örneği simülasyonda tekrar oynatır.
Yeni özellikler yazmam gerekir mi?
Hayır. Lumina Formal, SystemVerilog kodunuzda zaten bulunan eşzamanlı assertion, assume ve cover'ları denetler. Aynı assertion'lar simülasyonda da denetlenir.
Henüz desteklenmeyen yapılarda ne olur?
Özellik, nedeniyle birlikte UNSUPPORTED olarak raporlanır. Hiçbir şey sessizce atlanmaz ya da kanıtlanmış gibi raporlanmaz.
Kendi tasarımınızı Lumina'da ilk siz çalıştırın.
Lansmandan önce küçük bir grup tasarım ekibiyle çalışıyoruz. Siz gerçek tasarımlarınızı çalıştırırsınız, bulduğunuz sorunları biz düzeltiriz; test senaryolarınız da her derlemenin geçmesi gereken testlerin parçası olur.