Synopsys的MagellanTM是一種混合式的RTL設(shè)計規(guī)則形式驗(yàn)證產(chǎn)品，有助于工程師快速查找隱藏較深且不易發(fā)現(xiàn)的錯誤，縮短功能驗(yàn)證周 期，保證高質(zhì)量的設(shè)計。Magellan獨(dú)特的混合式架構(gòu)結(jié)合了先進(jìn)的形式分析引擎和內(nèi)置VCS仿真引擎可以處理復(fù)雜的大規(guī)模Verilog和VHDL的 設(shè)計。

主要優(yōu)點(diǎn)：

• 查找不易發(fā)現(xiàn)的功能錯誤，提高設(shè)計質(zhì)量

• 在驗(yàn)證周期的初期，查出功能錯誤，降低驗(yàn)證成本

• 通過重用動態(tài)和形式驗(yàn)證環(huán)境之間的斷言，提高驗(yàn)證的工作效率

• 通過驗(yàn)證復(fù)雜的設(shè)計規(guī)則以提高驗(yàn)證的可信