Integrating design and verification environments through a logic supporting hardware diagrams
Integrating design and verification environments through a logic supporting hardware diagrams
复制标题
通过支持硬件图的逻辑集成设计和验证环境
DOI：
10.1109/aspdac.1995.486385
复制
发表时间：
1995
期刊：
影响因子：
--
通讯作者：
Steven D. Johnson
中科院分区：
文献类型：
--
作者：
Kathi Fisler;Steven D. Johnson
对于设计者来说，形式化的方法和验证工具很难使用。研究一直集中在处理大量证据上，同时对推理过程关注不够。我们认为，支持硬件图和语句逻辑的异类逻辑为推理以及设计和验证环境的形式化集成提供了一个自然的框架。我们提出了这样一种逻辑，并在交通灯控制器设计和验证问题的片断上演示了它的灵活性。
Formal methods and verification tools are difficult for designers to use. Research has been concentrated on handling large proofs; meanwhile, insufficient attention has been paid to the reasoning process. We argue that a heterogeneous logic supporting hardware diagrams and sentential logic provides a natural framework for reasoning and for the formal integration of design and verification environments. We present such a logic and demonstrate its flexibility on fragments of a traffic light controller design and verification problem.