يک مدل سطح بالا برای وارسی خواص CTL در طرح توصيف شده توسط VHDL
الموضوعات : electrical and computer engineeringبيژن عليزاده 1 , زین العابدین نوابی 2
1 - دانشگاه تهران
2 - دانشگاه تهران
الکلمات المفتاحية: توابع انتقال حالتحلکننده معادلات صحيحمعادلات چندجملهای با متغيرهای صحيحBDD و Boolean Satisfiability ,
ملخص المقالة :
در اين مقاله قصد داريم مدل سطح بالايي بر پاية معادلات چندجملهاي با متغيرهاي صحيح ارائه دهيم كه مناسب براي وارسي خواص بر پاية CTL (Computational Temporal Logic) ميباشد. اكثر ابزارهاي وارسي از ساختمان دادههاي سطح پاييني مانند BDD استفاده ميكنند و اين ساختمان دادهها به علت نياز به حافظه زياد، قابل اعمال به بخش مسير داده از يك طرح نميباشند، در حالي كه مدل سطح بالاي پيشنهادی در اين مقاله قادر است بخشهاي مسير داده و كنترلر را با هم مورد ارزيابي قرار دهد. ضمن اينكه روش پيشنهادي به گونهاي است كه نياز به حل صريح معادلات نميباشد و اين كار توسط عمليات جايگزيني و سادهسازي انجام ميگيرد. در انتها نتايج كارمان با ابزار VIS، بعنوان يك ابزار وارسي بر پاية BDD، مقايسه ميگردند.