CNF Encoded Isomorphic and Optimized Miters from Hardware Model Checking Competition 2020 Models

DOI10.5281/zenodo.11202461Zenodo11202461MaRDI QIDQ6700828FDOQ6700828

Dataset published at Zenodo repository.

Armin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks

Publication date: 16 May 2024

Copyright license: Creative Commons Attribution 4.0 International

Description

From the Hardware Model Checking Competition 2020 we have collected 324sequential model checking problems and for each generated an isomorphic andan optimized miter. The isomorphic miters just compares two identicalcopies while for the optimized miter one copy went through optimizationwith ABC using the `dc2` command. The CNFs are generated with a new version of `aigtocnf` which detectsXOR and ITE gates in the AIGER circuit and if detected uses a more compactencoding (4 clauses clauses instead of 9) for each detected gate.

This page was built for dataset: CNF Encoded Isomorphic and Optimized Miters from Hardware Model Checking Competition 2020 Models