diff --git a/tools/README.md b/tools/README.md new file mode 100644 index 00000000..1036f1c9 --- /dev/null +++ b/tools/README.md @@ -0,0 +1,6 @@ +# SBY - Additional Tools + +This directory contains various tools that can be used in conjunction with SBY. + +* [`aigcexmin`](./aigcexmin) Counter-example minimization of AIGER witness (.aiw) files +* [`cexenum`](./cexenum) Enumeration of minimized counter-examples diff --git a/tools/aigcexmin/.gitignore b/tools/aigcexmin/.gitignore new file mode 100644 index 00000000..ea8c4bf7 --- /dev/null +++ b/tools/aigcexmin/.gitignore @@ -0,0 +1 @@ +/target diff --git a/tools/aigcexmin/Cargo.lock b/tools/aigcexmin/Cargo.lock new file mode 100644 index 00000000..828358bb --- /dev/null +++ b/tools/aigcexmin/Cargo.lock @@ -0,0 +1,562 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "addr2line" +version = "0.21.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8a30b2e23b9e17a9f90641c7ab1549cd9b44f296d3ccbf309d2863cfe398a0cb" +dependencies = [ + "gimli", +] + +[[package]] +name = "adler" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f26201604c87b1e01bd3d98f8d5d9a8fcbb815e8cedb41ffccbeb4bf593a35fe" + +[[package]] +name = "aigcexmin" +version = "0.1.0" +dependencies = [ + "clap", + "color-eyre", + "flussab", + "flussab-aiger", + "zwohash", +] + +[[package]] +name = "anstream" +version = "0.6.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2ab91ebe16eb252986481c5b62f6098f3b698a45e34b5b98200cf20dd2484a44" +dependencies = [ + "anstyle", + "anstyle-parse", + "anstyle-query", + "anstyle-wincon", + "colorchoice", + "utf8parse", +] + +[[package]] +name = "anstyle" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7079075b41f533b8c61d2a4d073c4676e1f8b249ff94a393b0595db304e0dd87" + +[[package]] +name = "anstyle-parse" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "317b9a89c1868f5ea6ff1d9539a69f45dffc21ce321ac1fd1160dfa48c8e2140" +dependencies = [ + "utf8parse", +] + +[[package]] +name = "anstyle-query" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5ca11d4be1bab0c8bc8734a9aa7bf4ee8316d462a08c6ac5052f888fef5b494b" +dependencies = [ + "windows-sys", +] + +[[package]] +name = "anstyle-wincon" +version = "3.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f0699d10d2f4d628a98ee7b57b289abbc98ff3bad977cb3152709d4bf2330628" +dependencies = [ + "anstyle", + "windows-sys", +] + +[[package]] +name = "autocfg" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa" + +[[package]] +name = "backtrace" +version = "0.3.69" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2089b7e3f35b9dd2d0ed921ead4f6d318c27680d4a5bd167b3ee120edb105837" +dependencies = [ + "addr2line", + "cc", + "cfg-if", + "libc", + "miniz_oxide", + "object", + "rustc-demangle", +] + +[[package]] +name = "bitflags" +version = "2.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "327762f6e5a765692301e5bb513e0d9fef63be86bbc14528052b1cd3e6f03e07" + +[[package]] +name = "cc" +version = "1.0.83" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f1174fb0b6ec23863f8b971027804a42614e347eafb0a95bf0b12cdae21fc4d0" +dependencies = [ + "libc", +] + +[[package]] +name = "cfg-if" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" + +[[package]] +name = "clap" +version = "4.4.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2275f18819641850fa26c89acc84d465c1bf91ce57bc2748b28c420473352f64" +dependencies = [ + "clap_builder", + "clap_derive", +] + +[[package]] +name = "clap_builder" +version = "4.4.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "07cdf1b148b25c1e1f7a42225e30a0d99a615cd4637eae7365548dd4529b95bc" +dependencies = [ + "anstream", + "anstyle", + "clap_lex", + "strsim", + "terminal_size", +] + +[[package]] +name = "clap_derive" +version = "4.4.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf9804afaaf59a91e75b022a30fb7229a7901f60c755489cc61c9b423b836442" +dependencies = [ + "heck", + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "clap_lex" +version = "0.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "702fc72eb24e5a1e48ce58027a675bc24edd52096d5397d4aea7c6dd9eca0bd1" + +[[package]] +name = "color-eyre" +version = "0.6.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5a667583cca8c4f8436db8de46ea8233c42a7d9ae424a82d338f2e4675229204" +dependencies = [ + "backtrace", + "color-spantrace", + "eyre", + "indenter", + "once_cell", + "owo-colors", + "tracing-error", +] + +[[package]] +name = "color-spantrace" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1ba75b3d9449ecdccb27ecbc479fdc0b87fa2dd43d2f8298f9bf0e59aacc8dce" +dependencies = [ + "once_cell", + "owo-colors", + "tracing-core", + "tracing-error", +] + +[[package]] +name = "colorchoice" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "acbf1af155f9b9ef647e42cdc158db4b64a1b61f743629225fde6f3e0be2a7c7" + +[[package]] +name = "errno" +version = "0.3.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7c18ee0ed65a5f1f81cac6b1d213b69c35fa47d4252ad41f1486dbd8226fe36e" +dependencies = [ + "libc", + "windows-sys", +] + +[[package]] +name = "eyre" +version = "0.6.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4c2b6b5a29c02cdc822728b7d7b8ae1bab3e3b05d44522770ddd49722eeac7eb" +dependencies = [ + "indenter", + "once_cell", +] + +[[package]] +name = "flussab" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fcd46d8f41aa1e4d79ba21282dd39a9c539d610ab336fc56a48dccdd7c82b12f" +dependencies = [ + "itoap", + "num-traits", +] + +[[package]] +name = "flussab-aiger" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "378b3a9970d0163162e8b3c9a4d9b2eef98be95d624cbac5b207278b157886d2" +dependencies = [ + "flussab", + "num-traits", + "thiserror", + "zwohash", +] + +[[package]] +name = "gimli" +version = "0.28.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6fb8d784f27acf97159b40fc4db5ecd8aa23b9ad5ef69cdd136d3bc80665f0c0" + +[[package]] +name = "heck" +version = "0.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "95505c38b4572b2d910cecb0281560f54b440a19336cbbcb27bf6ce6adc6f5a8" + +[[package]] +name = "indenter" +version = "0.3.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ce23b50ad8242c51a442f3ff322d56b02f08852c77e4c0b4d3fd684abc89c683" + +[[package]] +name = "itoap" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9028f49264629065d057f340a86acb84867925865f73bbf8d47b4d149a7e88b8" + +[[package]] +name = "lazy_static" +version = "1.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" + +[[package]] +name = "libc" +version = "0.2.150" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "89d92a4743f9a61002fae18374ed11e7973f530cb3a3255fb354818118b2203c" + +[[package]] +name = "linux-raw-sys" +version = "0.4.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "969488b55f8ac402214f3f5fd243ebb7206cf82de60d3172994707a4bcc2b829" + +[[package]] +name = "memchr" +version = "2.6.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f665ee40bc4a3c5590afb1e9677db74a508659dfd71e126420da8274909a0167" + +[[package]] +name = "miniz_oxide" +version = "0.7.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e7810e0be55b428ada41041c41f32c9f1a42817901b4ccf45fa3d4b6561e74c7" +dependencies = [ + "adler", +] + +[[package]] +name = "num-traits" +version = "0.2.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "39e3200413f237f41ab11ad6d161bc7239c84dcb631773ccd7de3dfe4b5c267c" +dependencies = [ + "autocfg", +] + +[[package]] +name = "object" +version = "0.32.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9cf5f9dd3933bd50a9e1f149ec995f39ae2c496d31fd772c1fd45ebc27e902b0" +dependencies = [ + "memchr", +] + +[[package]] +name = "once_cell" +version = "1.18.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dd8b5dd2ae5ed71462c540258bedcb51965123ad7e7ccf4b9a8cafaa4a63576d" + +[[package]] +name = "owo-colors" +version = "3.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c1b04fb49957986fdce4d6ee7a65027d55d4b6d2265e5848bbb507b58ccfdb6f" + +[[package]] +name = "pin-project-lite" +version = "0.2.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8afb450f006bf6385ca15ef45d71d2288452bc3683ce2e2cacc0d18e4be60b58" + +[[package]] +name = "proc-macro2" +version = "1.0.69" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "134c189feb4956b20f6f547d2cf727d4c0fe06722b20a0eec87ed445a97f92da" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.33" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5267fca4496028628a95160fc423a33e8b2e6af8a5302579e322e4b520293cae" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "rustc-demangle" +version = "0.1.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d626bb9dae77e28219937af045c257c28bfd3f69333c512553507f5f9798cb76" + +[[package]] +name = "rustix" +version = "0.38.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9ad981d6c340a49cdc40a1028d9c6084ec7e9fa33fcb839cab656a267071e234" +dependencies = [ + "bitflags", + "errno", + "libc", + "linux-raw-sys", + "windows-sys", +] + +[[package]] +name = "sharded-slab" +version = "0.1.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f40ca3c46823713e0d4209592e8d6e826aa57e928f09752619fc696c499637f6" +dependencies = [ + "lazy_static", +] + +[[package]] +name = "strsim" +version = "0.10.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623" + +[[package]] +name = "syn" +version = "2.0.39" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "23e78b90f2fcf45d3e842032ce32e3f2d1545ba6636271dcbf24fa306d87be7a" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "terminal_size" +version = "0.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "21bebf2b7c9e0a515f6e0f8c51dc0f8e4696391e6f1ff30379559f8365fb0df7" +dependencies = [ + "rustix", + "windows-sys", +] + +[[package]] +name = "thiserror" +version = "1.0.50" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f9a7210f5c9a7156bb50aa36aed4c95afb51df0df00713949448cf9e97d382d2" +dependencies = [ + "thiserror-impl", +] + +[[package]] +name = "thiserror-impl" +version = "1.0.50" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "266b2e40bc00e5a6c09c3584011e08b06f123c00362c92b975ba9843aaaa14b8" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "thread_local" +version = "1.1.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3fdd6f064ccff2d6567adcb3873ca630700f00b5ad3f060c25b5dcfd9a4ce152" +dependencies = [ + "cfg-if", + "once_cell", +] + +[[package]] +name = "tracing" +version = "0.1.40" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c3523ab5a71916ccf420eebdf5521fcef02141234bbc0b8a49f2fdc4544364ef" +dependencies = [ + "pin-project-lite", + "tracing-core", +] + +[[package]] +name = "tracing-core" +version = "0.1.32" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c06d3da6113f116aaee68e4d601191614c9053067f9ab7f6edbcb161237daa54" +dependencies = [ + "once_cell", + "valuable", +] + +[[package]] +name = "tracing-error" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d686ec1c0f384b1277f097b2f279a2ecc11afe8c133c1aabf036a27cb4cd206e" +dependencies = [ + "tracing", + "tracing-subscriber", +] + +[[package]] +name = "tracing-subscriber" +version = "0.3.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ad0f048c97dbd9faa9b7df56362b8ebcaa52adb06b498c050d2f4e32f90a7a8b" +dependencies = [ + "sharded-slab", + "thread_local", + "tracing-core", +] + +[[package]] +name = "unicode-ident" +version = "1.0.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b" + +[[package]] +name = "utf8parse" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "711b9620af191e0cdc7468a8d14e709c3dcdb115b36f838e601583af800a370a" + +[[package]] +name = "valuable" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "830b7e5d4d90034032940e4ace0d9a9a057e7a45cd94e6c007832e39edb82f6d" + +[[package]] +name = "windows-sys" +version = "0.48.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9" +dependencies = [ + "windows-targets", +] + +[[package]] +name = "windows-targets" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a2fa6e2155d7247be68c096456083145c183cbbbc2764150dda45a87197940c" +dependencies = [ + "windows_aarch64_gnullvm", + "windows_aarch64_msvc", + "windows_i686_gnu", + "windows_i686_msvc", + "windows_x86_64_gnu", + "windows_x86_64_gnullvm", + "windows_x86_64_msvc", +] + +[[package]] +name = "windows_aarch64_gnullvm" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8" + +[[package]] +name = "windows_aarch64_msvc" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc" + +[[package]] +name = "windows_i686_gnu" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e" + +[[package]] +name = "windows_i686_msvc" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406" + +[[package]] +name = "windows_x86_64_gnu" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e" + +[[package]] +name = "windows_x86_64_gnullvm" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc" + +[[package]] +name = "windows_x86_64_msvc" +version = "0.48.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538" + +[[package]] +name = "zwohash" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "beaf63e0740cea93ca85de39611a8bc8262a50adacd6321cd209a123676d0447" diff --git a/tools/aigcexmin/Cargo.toml b/tools/aigcexmin/Cargo.toml new file mode 100644 index 00000000..7a08f347 --- /dev/null +++ b/tools/aigcexmin/Cargo.toml @@ -0,0 +1,17 @@ +[package] +name = "aigcexmin" +version = "0.1.0" +edition = "2021" +authors = ["Jannis Harder "] + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[profile.release] +debug = true # profiling + +[dependencies] +clap = { version = "4.4.8", features = ["derive", "cargo", "wrap_help"] } +color-eyre = "0.6.2" +flussab = "0.3.1" +flussab-aiger = "0.1.0" +zwohash = "0.1.2" diff --git a/tools/aigcexmin/src/aig_eval.rs b/tools/aigcexmin/src/aig_eval.rs new file mode 100644 index 00000000..7e5543c6 --- /dev/null +++ b/tools/aigcexmin/src/aig_eval.rs @@ -0,0 +1,104 @@ +use flussab_aiger::{aig::OrderedAig, Lit}; + +use crate::util::unpack_lit; + +pub trait AigValue: Copy { + fn invert_if(self, en: bool, ctx: &mut Context) -> Self; + fn and(self, other: Self, ctx: &mut Context) -> Self; + fn constant(value: bool, ctx: &mut Context) -> Self; +} + +pub fn initial_frame( + aig: &OrderedAig, + state: &mut Vec, + mut latch_init: impl FnMut(usize, &mut Context) -> V, + mut input: impl FnMut(usize, &mut Context) -> V, + ctx: &mut Context, +) where + L: Lit, + V: AigValue, +{ + state.clear(); + state.push(V::constant(false, ctx)); + + for i in 0..aig.input_count { + state.push(input(i, ctx)); + } + + for i in 0..aig.latches.len() { + state.push(latch_init(i, ctx)); + } + + for and_gate in aig.and_gates.iter() { + let [a, b] = and_gate.inputs.map(|lit| { + let (var, polarity) = unpack_lit(lit); + state[var].invert_if(polarity, ctx) + }); + + state.push(a.and(b, ctx)); + } +} + +pub fn successor_frame( + aig: &OrderedAig, + state: &mut Vec, + mut input: impl FnMut(usize, &mut Context) -> V, + ctx: &mut Context, +) where + L: Lit, + V: AigValue, +{ + assert_eq!(state.len(), 1 + aig.max_var_index); + + for i in 0..aig.input_count { + state.push(input(i, ctx)); + } + + for latch in aig.latches.iter() { + let (var, polarity) = unpack_lit(latch.next_state); + state.push(state[var].invert_if(polarity, ctx)); + } + + state.drain(1..1 + aig.max_var_index); + + for and_gate in aig.and_gates.iter() { + let [a, b] = and_gate.inputs.map(|lit| { + let (var, polarity) = unpack_lit(lit); + state[var].invert_if(polarity, ctx) + }); + + state.push(a.and(b, ctx)); + } +} + +impl AigValue<()> for bool { + fn invert_if(self, en: bool, _ctx: &mut ()) -> Self { + self ^ en + } + + fn and(self, other: Self, _ctx: &mut ()) -> Self { + self & other + } + + fn constant(value: bool, _ctx: &mut ()) -> Self { + value + } +} + +impl AigValue<()> for Option { + fn invert_if(self, en: bool, _ctx: &mut ()) -> Self { + self.map(|b| b ^ en) + } + + fn and(self, other: Self, _ctx: &mut ()) -> Self { + match (self, other) { + (Some(true), Some(true)) => Some(true), + (Some(false), _) | (_, Some(false)) => Some(false), + _ => None, + } + } + + fn constant(value: bool, _ctx: &mut ()) -> Self { + Some(value) + } +} diff --git a/tools/aigcexmin/src/care_graph.rs b/tools/aigcexmin/src/care_graph.rs new file mode 100644 index 00000000..0f608fe2 --- /dev/null +++ b/tools/aigcexmin/src/care_graph.rs @@ -0,0 +1,730 @@ +use std::{ + cmp::Reverse, + collections::{BTreeSet, BinaryHeap}, + mem::{replace, take}, + num::NonZeroU32, +}; + +use color_eyre::eyre::bail; +use flussab::DeferredWriter; +use flussab_aiger::{aig::OrderedAig, Lit}; +use zwohash::HashMap; + +use crate::{ + aig_eval::{initial_frame, successor_frame, AigValue}, + util::{unpack_lit, write_output_bit}, +}; + +#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)] +#[repr(transparent)] +pub struct NodeRef { + code: Reverse, +} + +impl std::fmt::Debug for NodeRef { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.debug_tuple("NodeRef::new").field(&self.index()).finish() + } +} + +impl NodeRef { + const INVALID_INDEX: usize = u32::MAX as usize; + const TRUE_INDEX: usize = Self::INVALID_INDEX - 1; + const FALSE_INDEX: usize = Self::INVALID_INDEX - 2; + + pub const TRUE: Self = Self::new(Self::TRUE_INDEX); + pub const FALSE: Self = Self::new(Self::FALSE_INDEX); + + pub const fn new(index: usize) -> Self { + assert!(index < u32::MAX as usize); + let Some(code) = NonZeroU32::new(!(index as u32)) else { + unreachable!(); + }; + Self { + code: Reverse(code), + } + } + + pub fn index(self) -> usize { + !(self.code.0.get()) as usize + } +} + +#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)] +enum Gate { + And, + Or, +} + +#[derive(Debug)] +enum NodeDef { + Gate([NodeRef; 2]), + Input(u32), +} + +impl NodeDef { + fn and(inputs: [NodeRef; 2]) -> Self { + assert!(inputs[0] < inputs[1]); + Self::Gate(inputs) + } + + fn or(inputs: [NodeRef; 2]) -> Self { + assert!(inputs[0] < inputs[1]); + Self::Gate([inputs[1], inputs[0]]) + } + + fn input(id: u32) -> Self { + Self::Input(id) + } + + fn as_gate(&self) -> Result<(Gate, [NodeRef; 2]), u32> { + match *self { + NodeDef::Gate(inputs) => { + if inputs[0] < inputs[1] { + Ok((Gate::And, inputs)) + } else { + Ok((Gate::Or, [inputs[1], inputs[0]])) + } + } + NodeDef::Input(input) => Err(input), + } + } +} + +#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Default, Debug)] +enum NodeState { + #[default] + Unknown, + Nonselected, + Selected, + Required, +} + +#[derive(Debug)] +struct Node { + def: NodeDef, + priority: u32, + state: NodeState, + renamed: Option, +} + +impl Node { + fn update_state(&mut self, state: NodeState) -> NodeState { + let old_state = self.state; + self.state = self.state.max(state); + old_state + } +} + +#[derive(Default)] +pub struct AndOrGraph { + find_input: HashMap, + find_and: HashMap<[NodeRef; 2], NodeRef>, + find_or: HashMap<[NodeRef; 2], NodeRef>, + + // find_renamed: HashMap, + nodes: Vec, + queue: BinaryHeap, + stack: Vec, + + unknown_inputs: BTreeSet, + required_inputs: BTreeSet, + active_node_count: usize, + + input_order: Vec<(NodeRef, u32)>, + cache: bool, +} + +impl AndOrGraph { + pub fn input(&mut self, id: u32) -> NodeRef { + assert!(id <= u32::MAX - 2); + *self.find_input.entry(id).or_insert_with(|| { + let node_ref = NodeRef::new(self.nodes.len()); + let node = Node { + def: NodeDef::input(id), + priority: id, + state: NodeState::Unknown, + renamed: None, + }; + self.nodes.push(node); + self.unknown_inputs.insert(id); + node_ref + }) + } + + pub fn and(&mut self, mut inputs: [NodeRef; 2]) -> NodeRef { + inputs.sort_unstable(); + if inputs[1] == NodeRef::FALSE { + NodeRef::FALSE + } else if inputs[1] == NodeRef::TRUE || inputs[1] == inputs[0] { + inputs[0] + } else { + let [a, b] = inputs; + match inputs.map(|input| self.nodes[input.index()].def.as_gate()) { + [Ok((Gate::And, [a0, a1])), _] if b == a0 || b == a1 => { + return a; + } + [_, Ok((Gate::And, [b0, b1]))] if a == b0 || a == b1 => { + return b; + } + + [Ok((Gate::Or, [a0, a1])), _] if b == a0 || b == a1 => { + return b; + } + [_, Ok((Gate::Or, [b0, b1]))] if a == b0 || a == b1 => { + return a; + } + + _ => (), + } + + let mut mknode = || { + let node_ref = NodeRef::new(self.nodes.len()); + + let [a, b] = inputs.map(|input| self.nodes[input.index()].priority); + + let node = Node { + def: NodeDef::and(inputs), + priority: a.min(b), + state: NodeState::Unknown, + renamed: None, + }; + self.nodes.push(node); + node_ref + }; + + if self.cache { + *self.find_and.entry(inputs).or_insert_with(mknode) + } else { + mknode() + } + } + } + + pub fn or(&mut self, mut inputs: [NodeRef; 2]) -> NodeRef { + inputs.sort_unstable(); + + if inputs[1] == NodeRef::TRUE { + NodeRef::TRUE + } else if inputs[1] == NodeRef::FALSE || inputs[1] == inputs[0] { + inputs[0] + } else { + let [a, b] = inputs; + match inputs.map(|input| self.nodes[input.index()].def.as_gate()) { + [Ok((Gate::Or, [a0, a1])), _] if b == a0 || b == a1 => { + return a; + } + [_, Ok((Gate::Or, [b0, b1]))] if a == b0 || a == b1 => { + return b; + } + + [Ok((Gate::And, [a0, a1])), _] if b == a0 || b == a1 => { + return b; + } + [_, Ok((Gate::And, [b0, b1]))] if a == b0 || a == b1 => { + return a; + } + + _ => (), + } + + let mut mknode = || { + let node_ref = NodeRef::new(self.nodes.len()); + + let [a, b] = inputs.map(|input| self.nodes[input.index()].priority); + + let node = Node { + def: NodeDef::or(inputs), + priority: a.max(b), + state: NodeState::Unknown, + renamed: None, + }; + self.nodes.push(node); + node_ref + }; + + if self.cache { + *self.find_or.entry(inputs).or_insert_with(mknode) + } else { + mknode() + } + } + } + + pub fn pass(&mut self, target: NodeRef, shuffle: usize, mut enable_cache: bool) -> NodeRef { + if self.cache { + enable_cache = false; + } + + self.nodes[target.index()].state = NodeState::Required; + self.queue.push(target); + + let target_priority = self.nodes[target.index()].priority; + + 'queue: while let Some(current) = self.queue.pop() { + let node = &self.nodes[current.index()]; + let state = node.state; + + self.stack.push(current); + + match node.def.as_gate() { + Ok((Gate::And, inputs)) => { + if enable_cache { + self.find_and.insert(inputs, current); + } + for input in inputs { + let node = &mut self.nodes[input.index()]; + if node.update_state(state) == NodeState::Unknown { + self.queue.push(input); + } + } + } + Ok((Gate::Or, inputs)) => { + if enable_cache { + self.find_or.insert(inputs, current); + } + for input in inputs { + let node = &mut self.nodes[input.index()]; + if node.update_state(NodeState::Nonselected) == NodeState::Unknown { + self.queue.push(input); + } + } + + if state <= NodeState::Nonselected { + continue; + } + + let input_priorities = inputs.map(|input| self.nodes[input.index()].priority); + + for (i, input_priority) in input_priorities.into_iter().enumerate() { + if input_priority < target_priority { + // The other input will be false, so propagate the state + self.nodes[inputs[i ^ 1].index()].update_state(state); + continue; + } + } + + for input in inputs { + let input_state = self.nodes[input.index()].state; + if input_state >= NodeState::Selected { + // One input of the or is already marked, no need to mark the other + continue 'queue; + } + } + + // Mark the highest priority input + let input = inputs[(input_priorities[1] > input_priorities[0]) as usize]; + self.nodes[input.index()].update_state(NodeState::Selected); + } + Err(_input) => (), + } + } + + if enable_cache { + self.cache = true; + } + + let mut stack = take(&mut self.stack); + + self.active_node_count = stack.len(); + + self.unknown_inputs.clear(); + + for current in stack.drain(..).rev() { + let node = &mut self.nodes[current.index()]; + let state = replace(&mut node.state, NodeState::Unknown); + let priority = node.priority; + + match node.def.as_gate() { + Ok((gate, inputs)) => { + let new_inputs = inputs.map(|input| self.nodes[input.index()].renamed.unwrap()); + + let output = if new_inputs == inputs { + current + } else { + match gate { + Gate::And => self.and(new_inputs), + Gate::Or => self.or(new_inputs), + } + }; + + if shuffle > 0 && output != NodeRef::FALSE && output != NodeRef::TRUE { + if let Ok((gate, inputs)) = self.nodes[output.index()].def.as_gate() { + let [a, b] = inputs.map(|input| self.nodes[input.index()].priority); + + self.nodes[output.index()].priority = match gate { + Gate::And => a.min(b), + Gate::Or => a.max(b), + }; + } + } + + self.nodes[current.index()].renamed = Some(output); + } + Err(input) => match priority.cmp(&target_priority) { + std::cmp::Ordering::Less => { + self.nodes[current.index()].renamed = Some(NodeRef::FALSE); + } + std::cmp::Ordering::Equal => { + self.required_inputs.insert(input); + self.nodes[current.index()].renamed = Some(NodeRef::TRUE); + } + std::cmp::Ordering::Greater => match state { + NodeState::Required => { + self.required_inputs.insert(input); + self.nodes[current.index()].renamed = Some(NodeRef::TRUE); + } + NodeState::Selected => { + self.unknown_inputs.insert(input); + self.nodes[current.index()].renamed = Some(current); + + if shuffle > 0 { + let priority = &mut self.nodes[current.index()].priority; + let mask = !(u64::MAX << 32.min(shuffle - 1)) as u32; + + *priority ^= + !(*priority ^ priority.wrapping_mul(0x2c9277b5)) & mask; + } + } + NodeState::Nonselected => { + self.nodes[current.index()].renamed = Some(NodeRef::FALSE); + } + NodeState::Unknown => { + unreachable!(); + } + }, + }, + } + } + + self.input_order.clear(); + + let result = self.nodes[target.index()].renamed.unwrap(); + self.stack = stack; + + result + } +} + +impl AigValue for (Option, NodeRef) { + fn invert_if(self, en: bool, _: &mut AndOrGraph) -> Self { + let (value, care) = self; + (value.map(|b| b ^ en), care) + } + + fn and(self, other: Self, ctx: &mut AndOrGraph) -> Self { + let (value_a, care_a) = self; + let (value_b, care_b) = other; + + match (value_a, value_b) { + (Some(true), Some(true)) => (Some(true), ctx.and([care_a, care_b])), + (Some(false), Some(false)) => (Some(false), ctx.or([care_a, care_b])), + (Some(false), _) => (Some(false), care_a), + (_, Some(false)) => (Some(false), care_b), + _ => (None, NodeRef::FALSE), + } + } + + fn constant(value: bool, _: &mut AndOrGraph) -> Self { + (Some(value), NodeRef::TRUE) + } +} + +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +pub enum Verification { + Cex, + Full, +} + +pub struct MinimizationOptions { + pub fixed_init: bool, + pub verify: Option, +} + +pub fn minimize( + aig: &OrderedAig, + latch_init: &[Option], + frame_inputs: &[Vec>], + writer: &mut DeferredWriter, + options: &MinimizationOptions, +) -> color_eyre::Result<()> { + let Some(initial_inputs) = frame_inputs.first() else { + bail!("no inputs found"); + }; + + let mut state = vec![]; + + let mut graph = AndOrGraph::default(); + + let input_id = |frame: Option, index: usize| -> u32 { + (if let Some(frame) = frame { + latch_init.len() + frame * initial_inputs.len() + index + } else { + index + }) + .try_into() + .unwrap() + }; + + let decode_input_id = |id: u32| -> (Option, usize) { + let id = id as usize; + if id < latch_init.len() { + (None, id) + } else { + let id = id - latch_init.len(); + let frame = id / initial_inputs.len(); + let index = id % initial_inputs.len(); + (Some(frame), index) + } + }; + + initial_frame( + aig, + &mut state, + |i, ctx| { + ( + latch_init[i], + if latch_init[i].is_some() { + if options.fixed_init { + NodeRef::TRUE + } else { + ctx.input(input_id(None, i)) + } + } else { + NodeRef::FALSE + }, + ) + }, + |i, ctx| { + ( + initial_inputs[i], + if initial_inputs[i].is_some() { + ctx.input(input_id(Some(0), i)) + } else { + NodeRef::FALSE + }, + ) + }, + &mut graph, + ); + + let mut minimization_target = 'minimization_target: { + for (t, inputs) in frame_inputs.iter().enumerate() { + if t > 0 { + successor_frame( + aig, + &mut state, + |i, ctx| { + ( + inputs[i], + if inputs[i].is_some() { + ctx.input(input_id(Some(t), i)) + } else { + NodeRef::FALSE + }, + ) + }, + &mut graph, + ); + } + let mut good_state = (Some(true), NodeRef::TRUE); + + for (i, bad) in aig.bad_state_properties.iter().enumerate() { + let (var, polarity) = unpack_lit(*bad); + let inv_bad = state[var].invert_if(!polarity, &mut graph); + + if inv_bad.0 == Some(false) { + println!("bad state property {i} active in frame {t}"); + } + + good_state = good_state.and(inv_bad, &mut graph); + } + if good_state.0 == Some(false) { + println!("bad state found in frame {t}"); + + break 'minimization_target good_state.1; + } + + if t > 0 && t % 500 == 0 { + println!( + "traced frame {t}/{frames}: node count = {node_count}", + frames = frame_inputs.len(), + node_count = graph.nodes.len(), + ); + } + } + + bail!("no bad state found"); + }; + + let node_count_width = (graph.nodes.len().max(2) - 1).ilog10() as usize + 1; + let input_count_width = (graph.unknown_inputs.len().max(2) - 1).ilog10() as usize + 1; + + println!( + "input: node count = {node_count:w0$}, defined inputs = {defined_inputs:w1$}", + node_count = graph.nodes.len(), + defined_inputs = graph.unknown_inputs.len(), + w0 = node_count_width, + w1 = input_count_width, + ); + + let mut shuffle = 0; + + let mut iteration = 0; + + while minimization_target != NodeRef::TRUE { + let prev_unknown_inputs = graph.unknown_inputs.len(); + minimization_target = graph.pass(minimization_target, shuffle, iteration >= 1); + let unknown_inputs = graph.unknown_inputs.len(); + let required_inputs = graph.required_inputs.len(); + println!( + concat!( + "iter: node count = {node_count:w0$}, defined inputs = {defined_inputs:w1$}, ", + "required inputs = {required_inputs:w1$}, shuffle = {shuffle}" + ), + node_count = graph.active_node_count, + required_inputs = required_inputs, + defined_inputs = unknown_inputs + required_inputs, + shuffle = shuffle, + w0 = node_count_width, + w1 = input_count_width, + ); + + if unknown_inputs + (unknown_inputs / 4) < prev_unknown_inputs { + shuffle = 0; + } else { + shuffle += 1; + } + iteration += 1; + } + + println!("minimization complete"); + + for i in 0..aig.latches.len() { + let bit = if options.fixed_init || graph.required_inputs.contains(&input_id(None, i)) { + latch_init[i] + } else { + None + }; + + write_output_bit(writer, bit); + } + + writer.write_all_defer_err(b"\n"); + + for (t, inputs) in frame_inputs.iter().enumerate() { + for i in 0..aig.input_count { + let bit = if graph.required_inputs.contains(&input_id(Some(t), i)) { + inputs[i] + } else { + None + }; + + write_output_bit(writer, bit); + } + writer.write_all_defer_err(b"\n"); + } + + writer.write_all_defer_err(b"# DONE\n"); + writer.flush_defer_err(); + writer.check_io_error()?; + + let Some(verify) = options.verify else { + return Ok(()); + }; + + let mut check_state: Vec> = vec![]; + + let empty_set = BTreeSet::new(); + + let verify_from = match verify { + Verification::Cex => &empty_set, + Verification::Full => &graph.required_inputs, + }; + + for check in [None] + .into_iter() + .chain(verify_from.iter().copied().map(Some)) + { + check_state.clear(); + + initial_frame( + aig, + &mut check_state, + |i, _| { + let input = input_id(None, i); + if options.fixed_init + || (Some(input) != check && graph.required_inputs.contains(&input)) + { + latch_init[i] + } else { + None + } + }, + |i, _| { + let input = input_id(Some(0), i); + if Some(input) != check && graph.required_inputs.contains(&input) { + initial_inputs[i] + } else { + None + } + }, + &mut (), + ); + + let mut bad_state = false; + + 'frame: for (t, inputs) in frame_inputs.iter().enumerate() { + if t > 0 { + successor_frame( + aig, + &mut check_state, + |i, _| { + let input = input_id(Some(t), i); + if Some(input) != check && graph.required_inputs.contains(&input) { + inputs[i] + } else { + None + } + }, + &mut (), + ); + } + + for bad in aig.bad_state_properties.iter() { + let (var, polarity) = unpack_lit(*bad); + let bad_output = check_state[var].invert_if(polarity, &mut ()); + if bad_output == Some(true) { + bad_state = true; + break 'frame; + } + } + } + + if bad_state != check.is_none() { + if let Some(check) = check { + let (frame, input) = decode_input_id(check); + if let Some(frame) = frame { + bail!("minimality verification wrt. frame {frame} input {input} failed"); + } else { + bail!("minimality verification wrt. initial latch {input} failed"); + } + } else { + bail!("counter example verification failed"); + } + } + + if let Some(check) = check { + let (frame, input) = decode_input_id(check); + if let Some(frame) = frame { + println!("verified minimality wrt. frame {frame} input {input}"); + } else { + println!("verified minimality wrt. initial latch {input}"); + } + } else { + println!("verified counter example"); + } + } + + Ok(()) +} diff --git a/tools/aigcexmin/src/main.rs b/tools/aigcexmin/src/main.rs new file mode 100644 index 00000000..30874db9 --- /dev/null +++ b/tools/aigcexmin/src/main.rs @@ -0,0 +1,145 @@ +#![allow(clippy::needless_range_loop)] + +use std::{fs, mem::replace, path::PathBuf}; + +use clap::{Parser, ValueEnum}; +use color_eyre::eyre::bail; + +use flussab_aiger::binary; + +pub mod aig_eval; +pub mod care_graph; +pub mod util; + +/// AIG counter example minimization +#[derive(clap::Parser)] +#[command(author, version, about, long_about = None, help_template="\ +{before-help}{name} {version} +{author-with-newline}{about-with-newline} +{usage-heading} {usage} + +{all-args}{after-help} +")] +pub struct Options { + /// Input AIGER file + aig: PathBuf, + /// Input AIGER witness file + witness: PathBuf, + /// Output AIGER witness file + output: PathBuf, + + /// Verify the minimized counter example + #[clap(long, default_value = "cex")] + verify: VerificationOption, + + /// Minimize latch initialization values + /// + /// Without this option the latch initialization values of the witness file are assumed to be + /// fixed and will remain as-is in the minimized witness file. + /// + /// Note that some tools (including the current Yosys/SBY flow) do not use AIGER native latch + /// initialization but instead perform initialization using inputs in the first frame. + #[clap(long)] + latches: bool, +} + +#[derive(Copy, Clone, ValueEnum)] +enum VerificationOption { + /// Skip verification + Off, + /// Verify the counter example + Cex, + /// Verify the counter example and that it is minimal (expensive) + Full, +} + +fn main() -> color_eyre::Result<()> { + let options = Options::parse(); + + color_eyre::install()?; + + let file_input = fs::File::open(options.aig)?; + let file_witness = fs::File::open(options.witness)?; + let file_output = fs::File::create(options.output)?; + + let mut writer_output = flussab::DeferredWriter::from_write(file_output); + + let mut read_witness_owned = flussab::DeferredReader::from_read(file_witness); + let read_witness = &mut read_witness_owned; + + let aig_reader = binary::Parser::::from_read(file_input, binary::Config::default())?; + + let aig = aig_reader.parse()?; + + let mut offset = 0; + offset = flussab::text::next_newline(read_witness, offset); + + if offset == 2 { + read_witness.advance(replace(&mut offset, 0)); + offset = flussab::text::next_newline(read_witness, offset); + read_witness.advance(replace(&mut offset, 0)); + + offset = flussab::text::next_newline(read_witness, offset); + } + + if offset != aig.latches.len() + 1 { + bail!( + "unexpected number of initial latch states, found {} expected {}", + offset.saturating_sub(1), + aig.latches.len() + ); + } + + let latch_init = read_witness.buf()[..aig.latches.len()] + .iter() + .copied() + .map(util::parse_input_bit) + .collect::, _>>()?; + + read_witness.advance(replace(&mut offset, 0)); + + let mut frame_inputs = vec![]; + + loop { + offset = flussab::text::next_newline(read_witness, offset); + + if matches!(read_witness.buf().first(), None | Some(b'.') | Some(b'#')) { + read_witness.check_io_error()?; + break; + } + + if offset != aig.input_count + 1 { + bail!( + "unexpected number of input bits, found {} expected {}", + offset.saturating_sub(1), + aig.input_count + ); + } + + frame_inputs.push( + read_witness.buf()[..aig.input_count] + .iter() + .copied() + .map(util::parse_input_bit) + .collect::, _>>()?, + ); + read_witness.advance(replace(&mut offset, 0)); + } + + care_graph::minimize( + &aig, + &latch_init, + &frame_inputs, + &mut writer_output, + &care_graph::MinimizationOptions { + fixed_init: !options.latches, + verify: match options.verify { + VerificationOption::Off => None, + VerificationOption::Cex => Some(care_graph::Verification::Cex), + VerificationOption::Full => Some(care_graph::Verification::Full), + }, + }, + )?; + + Ok(()) +} diff --git a/tools/aigcexmin/src/util.rs b/tools/aigcexmin/src/util.rs new file mode 100644 index 00000000..fb24bc89 --- /dev/null +++ b/tools/aigcexmin/src/util.rs @@ -0,0 +1,25 @@ +use color_eyre::eyre::bail; +use flussab::DeferredWriter; +use flussab_aiger::Lit; + +pub fn unpack_lit(lit: L) -> (usize, bool) { + let lit = lit.code(); + (lit >> 1, lit & 1 != 0) +} + +pub fn parse_input_bit(byte: u8) -> color_eyre::Result> { + Ok(match byte { + b'0' => Some(false), + b'1' => Some(true), + b'x' => None, + _ => bail!("unexpected input bit {byte:?}"), + }) +} + +pub fn write_output_bit(writer: &mut DeferredWriter, bit: Option) { + writer.write_all_defer_err(match bit { + Some(false) => b"0", + Some(true) => b"1", + None => b"x", + }) +} diff --git a/tools/cexenum/cexenum.py b/tools/cexenum/cexenum.py new file mode 100755 index 00000000..3ac88916 --- /dev/null +++ b/tools/cexenum/cexenum.py @@ -0,0 +1,584 @@ +#!/usr/bin/env tabbypy3 +from __future__ import annotations +import asyncio + +import json +import traceback +import argparse +import shutil +import shlex +import os +from pathlib import Path +from typing import Any, Awaitable, Literal + +import yosys_mau.task_loop.job_server as job +from yosys_mau import task_loop as tl + + +libexec = Path(__file__).parent.resolve() / "libexec" + +if libexec.exists(): + os.environb[b"PATH"] = bytes(libexec) + b":" + os.environb[b"PATH"] + + +def arg_parser(): + parser = argparse.ArgumentParser( + prog="cexenum", usage="%(prog)s [options] " + ) + + parser.add_argument( + "work_dir", + metavar="", + help="existing SBY work directory", + type=Path, + ) + + parser.add_argument( + "--depth", + type=int, + metavar="N", + help="BMC depth for the initial assertion failure (default: %(default)s)", + default=100, + ) + + parser.add_argument( + "--enum-depth", + type=int, + metavar="N", + help="number of time steps to run enumeration for, starting with" + " and including the time step of the first assertion failure" + " (default: %(default)s)", + default=10, + ) + + parser.add_argument( + "--no-sim", + dest="sim", + action="store_false", + help="do not run sim to obtain .fst traces for the enumerated counter examples", + ) + + parser.add_argument( + "--smtbmc-options", + metavar='"..."', + type=shlex.split, + help='command line options to pass to smtbmc (default: "%(default)s")', + default="-s yices --unroll", + ) + + parser.add_argument("--debug", action="store_true", help="enable debug logging") + parser.add_argument( + "--debug-events", action="store_true", help="enable debug event logging" + ) + + parser.add_argument( + "-j", + metavar="", + type=int, + dest="jobs", + help="maximum number of processes to run in parallel", + default=None, + ) + + return parser + + +def lines(*args): + return "".join(f"{line}\n" for line in args) + + +@tl.task_context +class App: + raw_args: argparse.Namespace + + debug: bool = False + debug_events: bool = False + + depth: int + enum_depth: int + sim: bool + + smtbmc_options: list[str] + + work_dir: Path + + work_subdir: Path + trace_dir_full: Path + trace_dir_min: Path + cache_dir: Path + + +def main() -> None: + args = arg_parser().parse_args() + + job.global_client(args.jobs) + + # Move command line arguments into the App context + for name in dir(args): + if name in type(App).__mro__[1].__annotations__: + setattr(App, name, getattr(args, name)) + + App.raw_args = args + + try: + tl.run_task_loop(task_loop_main) + except tl.TaskCancelled: + exit(1) + except BaseException as e: + if App.debug or App.debug_events: + traceback.print_exc() + tl.log_exception(e, raise_error=False) # Automatically avoids double logging + exit(1) + + +def setup_logging(): + tl.LogContext.app_name = "CEXENUM" + tl.logging.start_logging() + + if App.debug_events: + tl.logging.start_debug_event_logging() + if App.debug: + tl.LogContext.level = "debug" + + def error_handler(err: BaseException): + if isinstance(err, tl.TaskCancelled): + return + tl.log_exception(err, raise_error=True) + + tl.current_task().set_error_handler(None, error_handler) + + +async def batch(*args): + result = None + for arg in args: + result = await arg + return result + + +async def task_loop_main() -> None: + setup_logging() + + cached = False + + App.cache_dir = App.work_dir / "cexenum_cache" + try: + App.cache_dir.mkdir() + except FileExistsError: + if (App.cache_dir / "done").exists(): + cached = True + else: + shutil.rmtree(App.cache_dir) + App.cache_dir.mkdir() + + App.work_subdir = App.work_dir / "cexenum" + try: + App.work_subdir.mkdir() + except FileExistsError: + shutil.rmtree(App.work_subdir) + App.work_subdir.mkdir() + + App.trace_dir_full = App.work_subdir / "full" + App.trace_dir_full.mkdir() + App.trace_dir_min = App.work_subdir / "min" + App.trace_dir_min.mkdir() + + if cached: + tl.log("Reusing cached AIGER model") + aig_model = tl.Task() + else: + aig_model = AigModel() + + Enumeration(aig_model) + + +class AigModel(tl.process.Process): + def __init__(self): + self[tl.LogContext].scope = "aiger" + (App.cache_dir / "design_aiger.ys").write_text( + lines( + "read_ilang ../model/design_prep.il", + "hierarchy -simcheck", + "flatten", + "setundef -undriven -anyseq", + "setattr -set keep 1 w:\*", + "delete -output", + "opt -full", + "techmap", + "opt -fast", + "memory_map -formal", + "formalff -clk2ff -ff2anyinit", + "simplemap", + "dffunmap", + "abc -g AND -fast", + "opt_clean", + "stat", + "write_rtlil design_aiger.il", + "write_aiger -I -B -zinit" + " -map design_aiger.aim -ywmap design_aiger.ywa design_aiger.aig", + ) + ) + super().__init__( + ["yosys", "-ql", "design_aiger.log", "design_aiger.ys"], cwd=App.cache_dir + ) + self.name = "aiger" + self.log_output() + + async def on_run(self) -> None: + await super().on_run() + (App.cache_dir / "done").write_text("") + + +class MinimizeTrace(tl.Task): + def __init__(self, trace_name: str, aig_model: tl.Task): + super().__init__() + self.trace_name = trace_name + + full_yw = App.trace_dir_full / self.trace_name + min_yw = App.trace_dir_min / self.trace_name + + stem = full_yw.stem + + full_aiw = full_yw.with_suffix(".aiw") + min_aiw = min_yw.with_suffix(".aiw") + + yw2aiw = YosysWitness( + "yw2aiw", + full_yw, + App.cache_dir / "design_aiger.ywa", + full_aiw, + cwd=App.trace_dir_full, + ) + yw2aiw.depends_on(aig_model) + yw2aiw[tl.LogContext].scope = f"yw2aiw[{stem}]" + + aigcexmin = AigCexMin( + App.cache_dir / "design_aiger.aig", + full_aiw, + min_aiw, + cwd=App.trace_dir_min, + ) + aigcexmin.depends_on(yw2aiw) + aigcexmin[tl.LogContext].scope = f"aigcexmin[{stem}]" + + self.aiw2yw = aiw2yw = YosysWitness( + "aiw2yw", + min_aiw, + App.cache_dir / "design_aiger.ywa", + min_yw, + cwd=App.trace_dir_min, + ) + aiw2yw[tl.LogContext].scope = f"aiw2yw[{stem}]" + aiw2yw.depends_on(aigcexmin) + + if App.sim: + sim = SimTrace( + App.cache_dir / "design_aiger.il", + min_yw, + min_yw.with_suffix(".fst"), + cwd=App.trace_dir_min, + ) + + sim[tl.LogContext].scope = f"sim[{stem}]" + sim.depends_on(aiw2yw) + + +def relative_to(target: Path, cwd: Path) -> Path: + prefix = Path("") + target = target.resolve() + cwd = cwd.resolve() + while True: + try: + return prefix / (target.relative_to(cwd)) + except ValueError: + prefix = prefix / ".." + if cwd == cwd.parent: + return target + cwd = cwd.parent + + +class YosysWitness(tl.process.Process): + def __init__( + self, + mode: Literal["yw2aiw"] | Literal["aiw2yw"], + input: Path, + mapfile: Path, + output: Path, + cwd: Path, + ): + super().__init__( + [ + "yosys-witness", + mode, + str(relative_to(input, cwd)), + str(relative_to(mapfile, cwd)), + str(relative_to(output, cwd)), + ], + cwd=cwd, + ) + + def handler(event: tl.process.OutputEvent): + tl.log_debug(event.output.rstrip("\n")) + + self.sync_handle_events(tl.process.OutputEvent, handler) + + +class AigCexMin(tl.process.Process): + def __init__(self, design_aig: Path, input_aiw: Path, output_aiw: Path, cwd: Path): + super().__init__( + [ + "aigcexmin", + str(relative_to(design_aig, cwd)), + str(relative_to(input_aiw, cwd)), + str(relative_to(output_aiw, cwd)), + ], + cwd=cwd, + ) + + self.log_path = output_aiw.with_suffix(".log") + self.log_file = None + + def handler(event: tl.process.OutputEvent): + if self.log_file is None: + self.log_file = self.log_path.open("w") + self.log_file.write(event.output) + self.log_file.flush() + tl.log_debug(event.output.rstrip("\n")) + + self.sync_handle_events(tl.process.OutputEvent, handler) + + def on_cleanup(self): + if self.log_file is not None: + self.log_file.close() + super().on_cleanup() + + +class SimTrace(tl.process.Process): + def __init__(self, design_il: Path, input_yw: Path, output_fst: Path, cwd: Path): + self[tl.LogContext].scope = "sim" + + script_file = output_fst.with_suffix(".fst.ys") + log_file = output_fst.with_suffix(".fst.log") + + script_file.write_text( + lines( + f"read_rtlil {relative_to(design_il, cwd)}", + "logger -nowarn" + ' "Yosys witness trace has an unexpected value for the clock input"', + f"sim -zinit -r {relative_to(input_yw, cwd)} -hdlname" + f" -fst {relative_to(output_fst, cwd)}", + ) + ) + super().__init__( + [ + "yosys", + "-ql", + str(relative_to(log_file, cwd)), + str(relative_to(script_file, cwd)), + ], + cwd=cwd, + ) + self.name = "sim" + self.log_output() + + +class Enumeration(tl.Task): + def __init__(self, aig_model: tl.Task): + self.aig_model = aig_model + super().__init__() + + async def on_run(self) -> None: + smtbmc = Smtbmc(App.work_dir / "model" / "design_smt2.smt2") + + await smtbmc.ping() + + pred = None + + i = 0 + limit = App.depth + first_failure = None + + while i <= limit: + tl.log(f"Checking assumptions in step {i}..") + presat_checked = await batch( + smtbmc.bmc_step(i, initial=i == 0, assertions=None, pred=pred), + smtbmc.check(), + ) + if presat_checked != "sat": + if first_failure is None: + tl.log_error("Assumptions are not satisfiable") + else: + tl.log("No further counter-examples are reachable") + return + + tl.log(f"Checking assertions in step {i}..") + checked = await batch( + smtbmc.push(), + smtbmc.assertions(i, False), + smtbmc.check(), + ) + pred = i + if checked != "unsat": + if first_failure is None: + first_failure = i + limit = i + App.enum_depth + tl.log("BMC failed! Enumerating counter-examples..") + counter = 0 + + assert checked == "sat" + path = App.trace_dir_full / f"trace{i}_{counter}.yw" + + while checked == "sat": + await smtbmc.incremental_command( + cmd="write_yw_trace", path=str(path) + ) + tl.log(f"Written counter-example to {path.name}") + + minimize = MinimizeTrace(path.name, self.aig_model) + minimize.depends_on(self.aig_model) + + await minimize.aiw2yw.finished + + min_path = App.trace_dir_min / f"trace{i}_{counter}.yw" + + checked = await batch( + smtbmc.incremental_command( + cmd="read_yw_trace", + name="last", + path=str(min_path), + skip_x=True, + ), + smtbmc.assert_( + ["not", ["and", *(["yw", "last", k] for k in range(i + 1))]] + ), + smtbmc.check(), + ) + + counter += 1 + path = App.trace_dir_full / f"trace{i}_{counter}.yw" + + await batch(smtbmc.pop(), smtbmc.assertions(i)) + + i += 1 + + smtbmc.close_stdin() + + +class Smtbmc(tl.process.Process): + def __init__(self, smt2_model: Path): + self[tl.LogContext].scope = "smtbmc" + super().__init__( + [ + "yosys-smtbmc", + "--incremental", + *App.smtbmc_options, + str(smt2_model), + ], + interact=True, + ) + self.name = "smtbmc" + + self.expected_results = [] + + async def on_run(self) -> None: + def output_handler(event: tl.process.StderrEvent): + result = json.loads(event.output) + tl.log_debug(f"smtbmc > {result!r}") + if "err" in result: + exception = tl.logging.LoggedError( + tl.log_error(result["err"], raise_error=False) + ) + self.expected_results.pop(0).set_exception(exception) + if "msg" in result: + tl.log(result["msg"]) + if "ok" in result: + assert self.expected_results + self.expected_results.pop(0).set_result(result["ok"]) + + self.sync_handle_events(tl.process.StdoutEvent, output_handler) + + return await super().on_run() + + def ping(self) -> Awaitable[None]: + return self.incremental_command(cmd="ping") + + def incremental_command(self, **command: dict[Any]) -> Awaitable[Any]: + tl.log_debug(f"smtbmc < {command!r}") + self.write(json.dumps(command)) + self.write("\n") + result = asyncio.Future() + self.expected_results.append(result) + + return result + + def new_step(self, step: int) -> Awaitable[None]: + return self.incremental_command(cmd="new_step", step=step) + + def push(self) -> Awaitable[None]: + return self.incremental_command(cmd="push") + + def pop(self) -> Awaitable[None]: + return self.incremental_command(cmd="pop") + + def check(self) -> Awaitable[str]: + return self.incremental_command(cmd="check") + + def assert_antecedent(self, expr: Any) -> Awaitable[None]: + return self.incremental_command(cmd="assert_antecedent", expr=expr) + + def assert_consequent(self, expr: Any) -> Awaitable[None]: + return self.incremental_command(cmd="assert_consequent", expr=expr) + + def assert_(self, expr: Any) -> Awaitable[None]: + return self.incremental_command(cmd="assert", expr=expr) + + def hierarchy(self, step: int) -> Awaitable[None]: + return self.assert_antecedent(["mod_h", ["step", step]]) + + def assumptions(self, step: int, valid: bool = True) -> Awaitable[None]: + expr = ["mod_u", ["step", step]] + if not valid: + expr = ["not", expr] + return self.assert_consequent(expr) + + def assertions(self, step: int, valid: bool = True) -> Awaitable[None]: + expr = ["mod_a", ["step", step]] + if not valid: + expr = ["not", expr] + return self.assert_(expr) + + def initial(self, step: int, initial: bool) -> Awaitable[None]: + if initial: + return batch( + self.assert_antecedent(["mod_i", ["step", step]]), + self.assert_antecedent(["mod_is", ["step", step]]), + ) + else: + return self.assert_antecedent(["not", ["mod_is", ["step", step]]]) + + def transition(self, pred: int, succ: int) -> Awaitable[None]: + return self.assert_antecedent(["mod_t", ["step", pred], ["step", succ]]) + + def bmc_step( + self, + step: int, + initial: bool = False, + assertions: bool | None = True, + pred: int | None = None, + ) -> Awaitable[None]: + futures = [] + futures.append(self.new_step(step)) + futures.append(self.hierarchy(step)) + futures.append(self.assumptions(step)) + futures.append(self.initial(step, initial)) + + if pred is not None: + futures.append(self.transition(pred, step)) + + if assertions is not None: + futures.append(self.assertions(assertions)) + + return batch(*futures) + + +if __name__ == "__main__": + main() diff --git a/tools/cexenum/examples/.gitignore b/tools/cexenum/examples/.gitignore new file mode 100644 index 00000000..e69de29b diff --git a/tools/cexenum/examples/factor.sby b/tools/cexenum/examples/factor.sby new file mode 100644 index 00000000..5fe21fcd --- /dev/null +++ b/tools/cexenum/examples/factor.sby @@ -0,0 +1,49 @@ +# Run using: +# +# sby -f factor.sby +# tabbypy3 cexenum.py factor --enum-depth=0 +# +[options] +mode bmc +make_model prep,smt2 +expect unknown + +[engines] +none + +[script] +read_verilog -sv top.sv +prep -top top + +[file top.sv] +module top(input clk, input b_bit, output [15:0] acc); + reg [7:0] a; + reg [7:0] b_mask = 8'hff; + + + reg [15:0] a_shift = 0; + reg [15:0] acc = 0; + + + always @(posedge clk) begin + assume (!clk); + if ($initstate) begin + a_shift <= a; + acc <= 0; + end else begin + + if (b_bit) begin + acc <= acc + a_shift; + end + a_shift <= a_shift << 1; + b_mask <= b_mask >> 1; + end + + if (b_mask == 0) begin + a <= 0; + assert (acc != 100); + end; + + end + +endmodule