Intel Keynote Tentang Formal Peregangan Pikiran

Diterbitkan Ulang Oleh Plato

Followers: 0

Synopsys telah memposting di situs SolvNet ceramah menarik yang diberikan oleh Dr. Theo Drane dari Intel Graphics. Topiknya adalah pemeriksaan kesetaraan datapath. Mungkin terdengar seperti dukungan Synopsys VC Formal DPV lainnya tetapi Anda tetap harus menontonnya. Ini adalah diskusi yang memperluas pikiran tentang penggunaan dan pertimbangan dalam formal yang akan membawa Anda melampaui jenis panduan pengguna rutin ke wilayah yang lebih menarik.

Intel Keynote tentang Formal

Pemahaman intelektual versus pengujian sampel

Simulasi yang digerakkan oleh pengujian dalam segala bentuknya sangat bagus dan seringkali tidak tergantikan dalam memverifikasi kebenaran spesifikasi atau implementasi desain. Ini juga mudah untuk memulai. Cukup tulis program pengujian dan mulai simulasi. Tapi sisi lain dari kesederhanaan itu adalah kita tidak perlu melakukannya sepenuhnya memahami apa yang kami uji untuk memulai. Kami meyakinkan diri kami sendiri bahwa kami telah membaca spesifikasi dengan cermat dan memahami semua kasus sudut, tetapi tidak perlu banyak kerumitan yang rumit untuk membanjiri pemahaman kami.

Formal mendorong Anda untuk memahami fungsionalitas secara mendalam (setidaknya jika Anda ingin memberikan hasil yang berharga). Dalam contoh di atas, pertanyaan sederhana – dapatkah z semuanya 1 – gagal menunjukkan contoh dalam satu miliar siklus pada simulator. Tidak mengherankan, karena ini adalah kasus sudut ekstrim. Tes formal memberikan contoh spesifik dan sangat tidak jelas dalam 188 detik dan dapat membuktikan ini adalah satu-satunya kasus dalam waktu yang sedikit lebih singkat.

Oke formal melakukan apa yang tidak bisa dilakukan oleh pengujian dinamis, tetapi yang lebih penting Anda mempelajari sesuatu yang mungkin tidak pernah diberitahukan oleh simulator kepada Anda. Bahwa hanya ada satu kasus yang mungkin di mana kondisi itu bisa terjadi. Formal membantu Anda lebih memahami desain pada tingkat intelektual, bukan hanya sebagai ringkasan probabilistik di serangkaian kasus uji yang terbatas.

Masalah spesifikasi

Contoh berikutnya Theo didasarkan pada mesin penjual bug (disebut demikian karena ketika Anda menekan tombol Anda mendapatkan bug). Ini terlihat seperti masalah pemeriksaan kesetaraan C ke RTL yang cukup mudah, model C di sebelah kiri, model RTL di sebelah kanan. Satu kejutan bagi Theo di hari-hari awalnya secara formal adalah bahwa perilaku pergeseran kanan dalam model C tidak sepenuhnya ditentukan dalam standar C, meskipun gcc akan berperilaku wajar. Namun, DPV akan mengeluh tentang ketidakcocokan dibandingkan dengan RTL, sebagaimana mestinya. Perilaku yang tidak terdefinisi adalah hal yang berbahaya untuk diandalkan.

Formal sebagai mesin penjual otomatis serangga

Perbandingan spesifikasi antara C dan RTL hadir dengan bahaya lain, terutama di sekitar lebar bit. Pemotongan atau kehilangan bit bawaan dalam sinyal perantara (#3 di atas) adalah contoh yang baik. Apakah ini masalah spesifikasi? Mungkin area abu-abu antara pilihan spesifikasi dan implementasi.

Di luar pemeriksaan kesetaraan

Tampaknya, tujuan utama DPV adalah untuk memeriksa kesetaraan antara referensi C atau RTL dan implementasi RTL. Tetapi kebutuhan itu relatif jarang dan ada cara lain yang berguna untuk menerapkan teknologi semacam itu, jika sedikit di luar kebiasaan. Pertama klasik di dunia implementasi – saya membuat perubahan, memperbaiki bug – apakah saya memperkenalkan bug baru sebagai hasilnya? Sedikit seperti pemeriksaan SEQ setelah Anda menambahkan gating jam. Analisis reachability dalam output blok mungkin merupakan aplikasi lain yang berguna dalam beberapa kasus.

Bukan hanya pemeriksaan kesetaraan

Theo menjadi lebih kreatif, meminta peserta pelatihan menggunakan contoh tandingan untuk lebih memahami desainnya, memecahkan Sudokus or memfaktorkan bilangan bulat. Dia mengakui DPV membuat cara yang aneh untuk mendekati masalah seperti itu tetapi menunjukkan bahwa niatnya adalah untuk mematahkan ilusi bahwa DPV hanya untuk pemeriksaan kesetaraan. Ide yang menarik dan tentunya menguras otak untuk memikirkan tantangan-tantangan tersebut. (Saya akui saya segera mulai memikirkan masalah Sudoku begitu dia menyebutkannya.)

Bungkus

Theo menyimpulkan dengan diskusi tentang metodologi yang penting dalam penggunaan produksi, seputar kendala, regresi, dan perbandingan dengan model RTL lama. Juga tantangan untuk mengetahui apakah yang Anda periksa benar-benar cocok dengan spesifikasi bahasa alami tingkat atas.

Pembicaraan yang sangat berenergi, layak untuk ditonton di sini di SolvNet!

Bagikan postingan ini melalui: