公开(公告)号：CN103699730B

公开(公告)日：2017-02-22

申请号：CN201310697453.X

申请日：2013-12-18

Applicant: 华侨大学

Inventor： 罗继亮 ,  陈珑 ,  黄颖坤 ,  倪慧娟

IPC: G06F17/50

Abstract: 本发明一种基于Petri网的组合逻辑FPGA系统可达图的生成方法，在组合逻辑FPGA系统的Petri网建模方法的基础上，以电路逻辑功能为考虑对象，并以电路系统在一个稳定输入状态下所对应的稳定的门电路逻辑运算输出为研究条件，通过重新定义Petri网变迁激发规则，生成组合逻辑FPGA系统可达图，从该组合逻辑FPGA系统可达图中，FPGA系统的状态空间被清晰完整地呈现出来，因此，可以通过遍历搜索来检测系统是否存在违背控制目标的状态，这是验证VHDL程序逻辑错误最直接有力的方法，为VHDL程序形式化验证提供理论基础。

公开(公告)号：CN103699730A

公开(公告)日：2014-04-02

申请号：CN201310697453.X

申请日：2013-12-18

Applicant: 华侨大学

Inventor： 罗继亮 ,  陈珑 ,  黄颖坤 ,  倪慧娟

IPC: G06F17/50

Abstract: 本发明一种基于Petri网的组合逻辑FPGA系统可达图的生成方法，在组合逻辑FPGA系统的Petri网建模方法的基础上，以电路逻辑功能为考虑对象，并以电路系统在一个稳定输入状态下所对应的稳定的门电路逻辑运算输出为研究条件，通过重新定义Petri网变迁激发规则，生成组合逻辑FPGA系统可达图，从该组合逻辑FPGA系统可达图中，FPGA系统的状态空间被清晰完整地呈现出来，因此，可以通过遍历搜索来检测系统是否存在违背控制目标的状态，这是验证VHDL程序逻辑错误最直接有力的方法，为VHDL程序形式化验证提供理论基础。