Structure-Aware Computing, Partial Quantifier Elimination And SAT
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914554711113728 |
|---|---|
| author | Goldberg, Eugene |
| author_facet | Goldberg, Eugene |
| contents | Typically, a practical algorithm of hardware verification obtains a semantic result by being applied to a particular formula $F$. That is, although this algorithm uses the specifics of $F$ (sometimes inadvertently), its result holds for all formulas logically equivalent to $F$. We refer to computations that get a semantic result by intentionally exploiting the specifics of $F$ as structure-aware computing (SAC). Arguably, using SAC allows one to get a semantic result faster. We show that partial quantifier elimination (PQE), a generalization of quantifier elimination, can be used for SAC. The objective of this paper is twofold. First, we explain how SAC is performed by PQE by the example of three verification problems (property generation, equivalence checking and model checking). Second, we argue that PQE solving itself can benefit from SAC. We use SAT solving to introduce a technique that can be also applied in structure-aware PQE solving. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_05928 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Structure-Aware Computing, Partial Quantifier Elimination And SAT Goldberg, Eugene Logic in Computer Science Typically, a practical algorithm of hardware verification obtains a semantic result by being applied to a particular formula $F$. That is, although this algorithm uses the specifics of $F$ (sometimes inadvertently), its result holds for all formulas logically equivalent to $F$. We refer to computations that get a semantic result by intentionally exploiting the specifics of $F$ as structure-aware computing (SAC). Arguably, using SAC allows one to get a semantic result faster. We show that partial quantifier elimination (PQE), a generalization of quantifier elimination, can be used for SAC. The objective of this paper is twofold. First, we explain how SAC is performed by PQE by the example of three verification problems (property generation, equivalence checking and model checking). Second, we argue that PQE solving itself can benefit from SAC. We use SAT solving to introduce a technique that can be also applied in structure-aware PQE solving. |
| title | Structure-Aware Computing, Partial Quantifier Elimination And SAT |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2403.05928 |