Functional Reduction to Speed Up Bounded Model Checking
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915659405852672 |
|---|---|
| author | Yu, Changyuan Che, Wenbin Zhang, Hongce |
| author_facet | Yu, Changyuan Che, Wenbin Zhang, Hongce |
| contents | Bounded model checking (BMC) is a widely used technique for formal property verification (FPV), where the transition relation is repeatedly unrolled to increasing depths and encoded into Boolean satisfiability (SAT) queries. As the bound grows deeper, these SAT queries typically become more difficult to solve, posing scalability challenges. Howevefor, many FPV problems involve multiple copies of related circuits, creating opportunities to simplify the unrolled transition relation. Motivated by the functionally reduced and-inverter-graph (FRAIG) technique, we propose FRAIG-BMC, which incrementally identifies and merges functionally equivalent nodes during the unrolling process. By reducing redundancy, FRAIG-BMC improves the efficiency of SAT solving and accelerates property checking. Experiments demonstrate that FRAIG-BMC significantly speeds up BMC across a range of applications, including sequential equivalence checking, partial retention register detection, and information flow checking |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_06643 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Functional Reduction to Speed Up Bounded Model Checking Yu, Changyuan Che, Wenbin Zhang, Hongce Logic in Computer Science Bounded model checking (BMC) is a widely used technique for formal property verification (FPV), where the transition relation is repeatedly unrolled to increasing depths and encoded into Boolean satisfiability (SAT) queries. As the bound grows deeper, these SAT queries typically become more difficult to solve, posing scalability challenges. Howevefor, many FPV problems involve multiple copies of related circuits, creating opportunities to simplify the unrolled transition relation. Motivated by the functionally reduced and-inverter-graph (FRAIG) technique, we propose FRAIG-BMC, which incrementally identifies and merges functionally equivalent nodes during the unrolling process. By reducing redundancy, FRAIG-BMC improves the efficiency of SAT solving and accelerates property checking. Experiments demonstrate that FRAIG-BMC significantly speeds up BMC across a range of applications, including sequential equivalence checking, partial retention register detection, and information flow checking |
| title | Functional Reduction to Speed Up Bounded Model Checking |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2512.06643 |