Automatic verification of asynchronous circuits using temporal logic
作者:
D.L.Dill,
E.M.Clarke,
期刊:
IEE Proceedings E (Computers and Digital Techniques)
(IET Available online 1986)
卷期:
Volume 133,
issue 5
页码: 276-282
年代: 1986
DOI:10.1049/ip-e.1986.0034
出版商: IEE
数据来源: IET
摘要:
A method is presented for automatically verifying asynchronous sequential circuits using temporal logic specifications. The method takes a circuit desctibed in terms of Boolean gates and Muller elements, and derves a state graph that summaries all possible circuit executions resulting from any set of finite delays on the outputs of the components. The correct behaviour of the circuit is expressed in CTL, a temporal logic. This specification is checked against the state graph using a model checker program. Using this method, a timing error in a published arbiter design is discovered. A corrected arbiter is given and verified
点击下载:
PDF
(964KB)
返 回