The formal verification chain at BULL
作者： J.-C. Madre , O. Coudert , M. Currat , A. Debreil , C. Berthet
DOI: 10.1109/EASIC.1990.207991
关键词:
摘要: Presents the chain of tools developed at BULL for verification circuit designs. For several years, has been a leading site in field formal hardware. Until now, main concern was validation VLSI circuits its mainframe CPUs. The effort is currently extended to board components such as PLDs and ASICs. >
dissem.in 参考文章(9)
Olivier Coudert, Jean Christophe Madre, Christian Berthet, Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams computer aided verification. pp. 23- 32 ,(1990) , 10.1007/BFB0023716
Jean Christophe Madre, Olivier Coudert, Jean Paul Billon, Automating the diagnosis and the rectification of design errors with PRIAM international conference on computer aided design. pp. 30- 33 ,(1989) , 10.1007/978-1-4615-0292-0_2
Bryant, Graph-Based Algorithms for Boolean Function Manipulation IEEE Transactions on Computers. ,vol. 35, pp. 677- 691 ,(1986) , 10.1109/TC.1986.1676819
J.P. Queille, J. Sifakis, Fairness and related properties in transition systems -- a temporal logic to deal with fairness Acta Informatica. ,vol. 19, pp. 195- 220 ,(1983) , 10.1007/BF00265555
S. Devadas, H.-K.T. Ma, A.R. Newton, On the verification of sequential machines at differing levels of abstraction IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. ,vol. 7, pp. 713- 722 ,(1988) , 10.1109/43.3210
Jean-Paul Billon, Jean-Christophe Madre, Proving circuit correctness using formal comparison between expected and extracted behaviour design automation conference. pp. 205- 210 ,(1988) , 10.5555/285730.285764
E M Clarke, O Grumberg, Research on Automatic Verification of Finite-State Concurrent Systems Annual Review of Computer Science. ,vol. 2, pp. 269- 290 ,(1987) , 10.1146/ANNUREV.CS.02.060187.001413
Olivier Coudert, Christian Berthet, Jean Christophe Madre, Formal Boolean manipulations for the verification of sequential machines european design automation conference. pp. 57- 61 ,(1990) , 10.5555/949970.949984
J.-C. Madre, J.-P. Billon, Proving circuit correctness using formal comparison between expected and extracted behaviour design automation conference. pp. 205- 210 ,(1988) , 10.1109/DAC.1988.14759