Formal Verification of Totally Self-Checking Properties of Combinational Circuits
Summary :
In this paper we propose a method of formal verification of totally self-checking (TSC) properties of combinational circuits using logic function manipulation. We show that the problem of verification of TSC properties can be transformed to a satisfiability problem of decision functions formed from characteristic functions of a circuit's output code words. Then the problem can be solved using binary decision diagrams (BDD). Experimental results show the effectiveness of the proposed method.
- Publication
- IEICE TRANSACTIONS on Information Vol.E80-D No.1 pp.57-62
- Publication Date
- 1997/01/25
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- Special Section PAPER (Special Issue on Fault-Tolerant Computing)
- Category
- Verification
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Kazuo KAWAKUBO, Koji TANAKA, Hiromi HIRAISHI, "Formal Verification of Totally Self-Checking Properties of Combinational Circuits" in IEICE TRANSACTIONS on Information,
vol. E80-D, no. 1, pp. 57-62, January 1997, doi: .
Abstract: In this paper we propose a method of formal verification of totally self-checking (TSC) properties of combinational circuits using logic function manipulation. We show that the problem of verification of TSC properties can be transformed to a satisfiability problem of decision functions formed from characteristic functions of a circuit's output code words. Then the problem can be solved using binary decision diagrams (BDD). Experimental results show the effectiveness of the proposed method.
URL: https://global.ieice.org/en_transactions/information/10.1587/e80-d_1_57/_p
Copy
@ARTICLE{e80-d_1_57,
author={Kazuo KAWAKUBO, Koji TANAKA, Hiromi HIRAISHI, },
journal={IEICE TRANSACTIONS on Information},
title={Formal Verification of Totally Self-Checking Properties of Combinational Circuits},
year={1997},
volume={E80-D},
number={1},
pages={57-62},
abstract={In this paper we propose a method of formal verification of totally self-checking (TSC) properties of combinational circuits using logic function manipulation. We show that the problem of verification of TSC properties can be transformed to a satisfiability problem of decision functions formed from characteristic functions of a circuit's output code words. Then the problem can be solved using binary decision diagrams (BDD). Experimental results show the effectiveness of the proposed method.},
keywords={},
doi={},
ISSN={},
month={January},}
Copy
TY - JOUR
TI - Formal Verification of Totally Self-Checking Properties of Combinational Circuits
T2 - IEICE TRANSACTIONS on Information
SP - 57
EP - 62
AU - Kazuo KAWAKUBO
AU - Koji TANAKA
AU - Hiromi HIRAISHI
PY - 1997
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E80-D
IS - 1
JA - IEICE TRANSACTIONS on Information
Y1 - January 1997
AB - In this paper we propose a method of formal verification of totally self-checking (TSC) properties of combinational circuits using logic function manipulation. We show that the problem of verification of TSC properties can be transformed to a satisfiability problem of decision functions formed from characteristic functions of a circuit's output code words. Then the problem can be solved using binary decision diagrams (BDD). Experimental results show the effectiveness of the proposed method.
ER -
English
