RTL生成语言Confluence增加了开放源模型校验器新链接,该校验器主要用于验证复杂软件系统。据Launchbird Design Systems公司总裁、该语言创建者称,这项功能是校验系统特性的一种全新方式。
Confluence 0.7.0包含一个新代码生成器,能从Confluence设计中创建Promela模型。Promela是Spin模型校验器使用的系统规范语言。Confluence作为一种系统级逻辑设计语言,与HDL不同,它能生成输出RTL结构的算法。据称它比VHDL或Verilog更为简练。除了Promela,Confluence还能生成Verilog、VHDL、C 和Python。
Confluence 0.7.0能生成周期及位精确Promela模型及测试台电路。Hawkins表示,与HDL或C不同的是,Promela测试台可能有零、1或许多时域,还可能包括顶级输入和in/out端口。
尽管状态空间爆炸(state space explosion) 是Spin及其它模型校验器存在的问题,而Confluence能生成一个更抽象的模型,状态及输入较少,Hawkins指出。
据了解,Confluence的单个版本可从Launchbird Design Systems网站上免费下载。后续版本每月收费240美元。
京公网安备 11011202001138号
