در اين مقاله قصد داريم مدل سطح بالايي بر پاية معادلات چندجمله‏اي با متغيرهاي صحيح ارائه دهيم كه مناسب براي وارسي خواص بر پاية CTL (Computational Temporal Logic) مي‏باشد. اكثر ابزارهاي وارسي از ساختمان داده‏هاي سطح پاييني مانند BDD استفاده مي‏كنند و اين ساختمان داده‏ها به علت نياز به حافظه زياد، قابل اعمال به بخش مسير داده از يك طرح نمي‏باشند، در حالي كه مدل سطح بالاي پيشنهادی در اين مقاله قادر است بخش‏هاي مسير داده و كنترلر را با هم مورد ارزيابي قرار دهد. ضمن اينكه روش پيشنهادي به گونه‏اي است كه نياز به حل صريح معادلات نمي‏باشد و اين كار توسط عمليات جايگزيني و ساده‏سازي انجام مي‏گيرد. در انتها نتايج كارمان با ابزار VIS، بعنوان يك ابزار وارسي بر پاية BDD، مقايسه مي‏گردند. پرونده مقاله