使用函数式语言与命令式语言混合开发EDA程序的一次探索

相较于命令式语言,函数式语言有两个明显的优点:安全性好、开发周期短.但一般而言,函数式语言的代码性能不够好,妨碍了它的推广和实践应用,尤其是在性能要求很高的领域.基于上述问题进行了一次函数式语言和命令式语言混合编程的探索,试图在同一个项目中结合两类编程语言混合编程,一方面用函数式语言OCaml快速编写复杂度较高的算法核心代码;另一方面,用C语言编写难度不大但是对性能影响比较大的代码,通过这种混合编程方式在较短的时间内可以实现一个结构比较复杂但在性能上接近C语言编写的同类代码的软件.选用海量图形数据的高速区域化查询这一案例,该EDA问题对运算效率有较高的要求,所以在数据结构上选择四叉树结构来实现区域查询,因此是一个比较有代表性的使用高效数据结构来满足性能要求的问题.实验结果表明,OCaml和C的混合编程能将核心算法的研发周期明显缩短,同时性能与C语言编写的同类型的代码相仿,这也就说明了函数式语言和命令式语言的混合编程可以成为EDA软件开发的一个可行的方案.

多阶段编程定制数字电路

硬件描述语言在描述数字电路时面临抽象层次低、难以验证、工作量大等困难。以快速傅立叶变换电路设计为例,提出多阶段编程定制数字电路的方法,规避这些不便。利用高层次描述方法为应用系统建模,消除冗余计算和递归,产生简单函数。从简单函数中提取简化操作序列。最后,选择合适的电路设计方案,转化为硬件描述语言的代码,并自动生成可综合的电路。该方法适于自动定制系列电路。

函数式程序设计语言的教学研究与探讨

本文主要研究以OCaml为核心语言的函数式程序设计语言的课程教学设计,填补国内计算机专业在程序设计语言课程设置上的空白,以培养程序设计人员的程序设计全面素质和能力。

面向形式化验证的联锁翻译器软件设计

根据联锁系统的形式化验证系统需求,设计一种联锁数据翻译器软件的总体方案,实现站点接口文件、T LE文件和布尔逻辑文件等文件的翻译转换,生成形式化验证所需要的LCF文件。最后详细说明翻译器软件基于函数式语言OCaml的代码实现。

Kaputt在核安全级软件单元测试上的应用研究

在核安全级软件的测试中,单元测试是必不可少的测试手段之一。目前,部分核安全级软件采用函数式编程语言OCaml开发,但针对该语言开发的核安全级软件进行单元测试,尚缺乏具体的执行标准,通过确认测试来补充。本文提出采用第三方测试工具Kaputt对OCaml开发的核安全软件进行单元测试的方法,介绍Kaputt的测试模式、测试执行过程,及测试后分析关键字的覆盖率,以判断测试是否完备。该方法已在自主化核安全级软件测试中进行实践,取得良好的效果。

多旋翼飞控推进子系统的Coq形式化验证

飞行器需要高可靠的飞行控制系统软件(飞控)来控制其运行.在传统开发模式下,先由人工将领域知识描述为自然语言形式的模型,再根据模型手动编写代码,然后使用软件测试技术来排除软件错误,这种模式由于人工易出错、自然语言存在二义性、测试技术的不完备性,导致难以构建出高可靠的飞控软件.基于形式验证技术的新型软件开发方法可从多方面提高飞控系统的可靠性.使用Coq定理证明器对全权提出的多旋翼飞控推进子系统进行了完整的形式验证,生成了一个可用的高可靠函数式软件库.主要工作有:首先将领域知识整理为具有层次结构以适合进行形式验证的文档,分离了基本函数和复合函数,并提出最简形式函数概念;再根据该文档进行形式化描述,定义常量、变量、基本函数、复合函数、最简形式函数和公理等;其次对各类导出函数的推导正确性建立为引理并予以证明;再次对多旋翼最长悬停时间等实际问题给出了求解算法;最后利用Coq程序抽取功能生成了OCaml语言的函数式软件库.后续将对飞控更多子系统进行基于形式验证的开发,并最终建立完整的经形式化验证的高可靠飞控系统.