VIS: A System for Verification and Synthesis
作者： Robert K. Brayton , Gary D. Hachtel , Alberto Sangiovanni-Vincentelli , Fabio Somenzi , Adnan Aziz
关键词: Computer science 、 Finite-state machine 、 Formal verification 、 Formal equivalence checking 、 Model checking 、 Sequential logic 、 Data structure 、 Counterexample 、 Programming language 、 Equivalence (formal languages)
摘要: VIS (Verification Interacting with Synthesis) is a tool that integrates the verification, simulation, and synthesis of finite-state hardware systems. It uses a Verilog front end and supports fair …
springer.com
core.ac.uk
sci-hub.se 参考文章(4)
E. M. Sentovich, SIS : A System for Sequential Circuit Synthesis CTIT technical reports series. ,(1992)
E. M. Clarke, O. Grumberg, K. L. McMillan, X. Zhao, Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking design automation conference. pp. 427- 432 ,(1995) , 10.1145/217474.217565
Goichi Ootomo, Chikahiro Hori, Hiroshige Fujii, Interleaving based variable ordering methods for ordered binary decision diagrams international conference on computer aided design. pp. 38- 41 ,(1993) , 10.5555/259794.259801
Adnan Aziz, Serdar Taşiran, Robert K. Brayton, BDD Variable Ordering for Interacting Finite State Machines design automation conference. pp. 283- 288 ,(1994) , 10.1145/196244.196379