Efficient Model-Based Diagnosis of Sequential Circuits
Authors: Alexander Feldman, Ingo Pill, Franza Wotawa, Ion Matei, Johan de Kleer2814-2821
AAAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Based on extensive tests with ISCAS-89 circuits, we found that MOAs enable Conjunctive Normal Form (CNF) encodings that are significantly more compact. These encodings lead to 19.7 to 67.6 times fewer variables and 18.4 to 62 times fewer clauses. For converting an FTNL model to CNF, we could achieve a speed-up ranging from 6.2 to 22.2. |
| Researcher Affiliation | Collaboration | 1Palo Alto Research Center Inc., 3333 Coyote Hill Road, Palo Alto, CA 94304, USA 2Institute for Software Technology, Graz Univ. of Technology, Inffeldgasse 16b/II, 8010 Graz, Austria |
| Pseudocode | Yes | Algorithm 1: Convert an FTNL formula to a propositional logic formula; Algorithm 2: SAT-based diagnostic algorithm |
| Open Source Code | No | The paper does not provide any explicit statements about releasing source code or links to a code repository for the methodology described. |
| Open Datasets | Yes | In addition to the n-counter family introduced in Sec. , we have also constructed a benchmark of real-world diagnosis problems consisting of eight synchronous circuits (see Table 1). These models are translated from ISCAS-89 netlists (Brglez, Bryan, and Kozminski 1989). ISCAS-89 is a benchmark of sequential digitial circuits for testing Automated Test Pattern Generation (ATPG) algorithms. |
| Dataset Splits | No | The paper does not explicitly provide training/validation/test dataset splits (e.g., percentages or sample counts) for reproducibility. |
| Hardware Specification | No | The paper does not provide any specific hardware specifications (e.g., GPU/CPU models, memory details) used for running the experiments. |
| Software Dependencies | No | For the SAT solving we have used LINGELING (Biere 2016). The algorithms described in this paper are implemented in a mixture of Python and C. No version numbers are provided for Python, C, or any libraries used beyond the SAT solver itself. |
| Experiment Setup | Yes | Figure 5 shows TSAT as a function of the n-counter size n and the time-horizon T. We have experimented with 1 n 16 and 1 T 16. For each combination of n and T we have generated a number of diagnostic scenarios by random fault injection for a total of 31 909 scenarios. Each sequential circuit in Table 2 was run with multiple random-fault scenarios with increasing number of injected faults and for T = 3. |