Compare commits

...

3 commits

3 changed files with 71 additions and 8 deletions

View file

@ -59,7 +59,7 @@ jobs:
make -C sby install
- run: |
git clone --depth=1 --recursive --branch=0.45 https://github.com/YosysHQ/yosys.git
make -C yosys -j2
make -C yosys -j"$(nproc)"
make -C yosys install
- run: |
wget -O firrtl.tar.gz https://github.com/llvm/circt/releases/download/firtool-1.86.0/firrtl-bin-linux-x64.tar.gz

68
Cargo.lock generated
View file

@ -228,6 +228,27 @@ dependencies = [
"typenum",
]
[[package]]
name = "ctor"
version = "0.2.8"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "edb49164822f3ee45b17acd4a208cfc1251410cf0cad9a833234c9890774dd9f"
dependencies = [
"quote",
"syn",
]
[[package]]
name = "derive_destructure2"
version = "0.1.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "64b697ac90ff296f0fc031ee5a61c7ac31fb9fff50e3fb32873b09223613fc0c"
dependencies = [
"proc-macro2",
"quote",
"syn",
]
[[package]]
name = "digest"
version = "0.10.7"
@ -279,15 +300,17 @@ checksum = "e8c02a5121d4ea3eb16a80748c74f5549a5665e4c21333c6098f283870fbdea6"
[[package]]
name = "fayalite"
version = "0.2.0"
source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#3d0f95cfe5a910f79177babf8fe12483f83e96f9"
source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#cb17913004259b6e0908a477a67e5a6b621b5c1c"
dependencies = [
"bitvec",
"blake3",
"clap",
"ctor",
"eyre",
"fayalite-proc-macros",
"fayalite-visit-gen",
"hashbrown 0.14.5",
"jobslot",
"num-bigint",
"num-traits",
"os_pipe",
@ -300,7 +323,7 @@ dependencies = [
[[package]]
name = "fayalite-proc-macros"
version = "0.2.0"
source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#3d0f95cfe5a910f79177babf8fe12483f83e96f9"
source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#cb17913004259b6e0908a477a67e5a6b621b5c1c"
dependencies = [
"fayalite-proc-macros-impl",
]
@ -308,7 +331,7 @@ dependencies = [
[[package]]
name = "fayalite-proc-macros-impl"
version = "0.2.0"
source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#3d0f95cfe5a910f79177babf8fe12483f83e96f9"
source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#cb17913004259b6e0908a477a67e5a6b621b5c1c"
dependencies = [
"base16ct",
"num-bigint",
@ -323,7 +346,7 @@ dependencies = [
[[package]]
name = "fayalite-visit-gen"
version = "0.2.0"
source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#3d0f95cfe5a910f79177babf8fe12483f83e96f9"
source = "git+https://git.libre-chip.org/libre-chip/fayalite.git?branch=master#cb17913004259b6e0908a477a67e5a6b621b5c1c"
dependencies = [
"indexmap",
"prettyplease",
@ -351,6 +374,17 @@ dependencies = [
"version_check",
]
[[package]]
name = "getrandom"
version = "0.2.15"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "c4567c8db10ae91089c99af84c68c38da3ec2f087c3f82960bcdbf3656b6f4d7"
dependencies = [
"cfg-if",
"libc",
"wasi",
]
[[package]]
name = "hashbrown"
version = "0.14.5"
@ -411,6 +445,20 @@ version = "1.0.11"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b"
[[package]]
name = "jobslot"
version = "0.2.19"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "fe10868679d7a24c2c67d862d0e64a342ce9aef7cdde9ce8019bd35d353d458d"
dependencies = [
"cfg-if",
"derive_destructure2",
"getrandom",
"libc",
"scopeguard",
"windows-sys 0.59.0",
]
[[package]]
name = "libc"
version = "0.2.159"
@ -526,6 +574,12 @@ version = "1.0.18"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "f3cb5ba0dc43242ce17de99c180e96db90b235b8a9fdc9543c96d2209116bd9f"
[[package]]
name = "scopeguard"
version = "1.2.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49"
[[package]]
name = "serde"
version = "1.0.210"
@ -656,6 +710,12 @@ version = "0.9.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
[[package]]
name = "wasi"
version = "0.11.0+wasi-snapshot-preview1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423"
[[package]]
name = "which"
version = "6.0.3"

View file

@ -131,17 +131,20 @@ mod tests {
alloc_at_once: NonZeroUsize,
reg_num_width: usize,
) {
let reg_count = 1usize << reg_num_width;
// enough time to completely allocate all regs, free whatever we please,
// allocate one, then completely free the rest
let history_len = (3 + 2 * (1 << reg_num_width)).max(5);
let mut history_len = 1;
history_len += reg_count.div_ceil(alloc_at_once.get());
history_len += reg_count.div_ceil(free_at_once.get());
assert_formal(
format_args!(
"test_unit_free_regs_tracker_{free_at_once}_{alloc_at_once}_{reg_num_width}"
),
unit_free_regs_tracker_test(free_at_once, alloc_at_once, reg_num_width, history_len),
FormalMode::Prove,
history_len as u64 + 2,
None,
history_len as u64,
Some("z3"),
ExportOptions {
simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts),
..ExportOptions::default()