Fayalite is a Rust library for designing digital hardware. Published at https://crates.io/crates/fayalite
Find a file
Cesar Strauss 31d01046a8
Initial queue formal proof based on one-entry FIFO equivalence
For now, only check that the basic properties work in bounded model check
mode, leave the induction proof for later.

Partially replace the previously existing proof.

Remove earlier assumptions and bounds that don't apply for this proof.

Use parameterized types instead of hard-coded types.
2024-12-29 13:04:01 -03:00
.forgejo/workflows test doc tests in CI 2024-12-01 20:21:26 -08:00
crates Initial queue formal proof based on one-entry FIFO equivalence 2024-12-29 13:04:01 -03:00
scripts tests/sim: split expected output text into separate files 2024-12-05 18:17:13 -08:00
.gitignore add missing copyright headers 2024-09-22 15:30:05 -07:00
Cargo.lock upgrade syn version 2024-12-28 23:39:08 -08:00
Cargo.toml upgrade syn version 2024-12-28 23:39:08 -08:00
LICENSE.md initial public commit 2024-06-10 23:09:13 -07:00
Notices.txt initial public commit 2024-06-10 23:09:13 -07:00
README.md add missing copyright headers 2024-09-22 15:30:05 -07:00

Fayalite

Fayalite is a library for designing digital hardware -- a hardware description language (HDL) embedded in the Rust programming language. Fayalite's semantics are based on FIRRTL as interpreted by LLVM CIRCT.