programmerjake
  • Joined on 2024-07-08
programmerjake pushed to master at libre-chip/fayalite 2024-10-05 00:10:22 +00:00
ec77559e2b fix cache action name
programmerjake pushed to master at libre-chip/fayalite 2024-10-05 00:04:57 +00:00
b7f1101164 reduce parallelism to fit within the number of available cpus even when running sby in prove mode (which likes to run 2 smt solvers in parallel)
programmerjake pushed to master at libre-chip/fayalite 2024-10-04 08:03:55 +00:00
487af07154 yosys build runs out of memory
programmerjake pushed to master at libre-chip/fayalite 2024-10-04 06:40:56 +00:00
c0d4de56a9 try to make yosys build faster
programmerjake pushed to master at libre-chip/fayalite 2024-10-04 06:37:07 +00:00
9f154e6b96 try caching ccache manually
programmerjake pushed to master at libre-chip/fayalite 2024-10-04 06:08:41 +00:00
0d54b9a2a9 queue formal proof passes!
343805f80b fix #[hdl] to work with unusual identifier hygiene from macros
Compare 2 commits »
programmerjake pushed to master at libre-chip/fayalite 2024-10-03 08:44:37 +00:00
15a28aa7a7 install python3-click -- needed by symbiyosys
4084a70485 switch default solver to z3
Compare 2 commits »
programmerjake pushed to master at libre-chip/fayalite 2024-10-03 08:08:33 +00:00
3e2fb9b94f WIP getting queue formal to pass -- passes for capacity <= 2
programmerjake pushed to master at libre-chip/fayalite 2024-10-03 08:01:40 +00:00
bc26fe32fd add ccache and clean up deps
programmerjake pushed to master at libre-chip/fayalite 2024-10-03 07:44:28 +00:00
eb65bec26e add yosys deps
programmerjake pushed to master at libre-chip/fayalite 2024-10-03 07:39:39 +00:00
4497f09ea0 fix wrong build steps
programmerjake pushed to master at libre-chip/fayalite 2024-10-03 07:35:54 +00:00
1c63a441a9 add needed tools to CI
0cf01600b3 add mod formal and move assert/assume/cover stuff to it
f3d6528f5b make annotations easier to use
f35d88d2bb remove unused valueless.rs
e8c393f3bb sort pub mod items
Compare 5 commits »
programmerjake pushed to master at libre-chip/fayalite 2024-10-02 01:33:58 +00:00
d0b406d288 add more annotation kinds
2a25dd9d7b fix annotations getting lost
6e0b6c000d remove stray debugging prints
Compare 3 commits »
programmerjake pushed to master at libre-chip/fayalite 2024-10-01 07:08:48 +00:00
d089095667 change default to --simplify-enums=replace-with-bundle-of-uints
9d66fcc548 improve ExportOptions support in assert_export_firrtl!
186488a82e remove FIXME now that simplify_enums is fixed
Compare 3 commits »
programmerjake pushed to master at libre-chip/fayalite 2024-10-01 05:34:53 +00:00
edcea1adc3 add firrtl comments when connecting expressions with different types
30a38bc8da fix simplify_enums to properly handle nested enums and connects with different types
1e2831da47 add validation of connects and matches when validating module
d2ba313f0f fix simplify_memories trying to connect Bool with UInt
Compare 4 commits »
programmerjake pushed to master at libre-chip/fayalite 2024-09-26 04:56:38 +00:00
04752c5037 add test for connect_any with nested enums with different-sized variant bodies
programmerjake pushed to master at libre-chip/fayalite 2024-09-25 09:00:37 +00:00
e661aeab11 add WIP formal proof for queue()
5fc7dbd6e9 add assert_formal helper for running formal proofs in rust tests
45dbb554d0 add formal subcommand
bb860d54cc add command line options for selecting which transforms to apply when generating firrtl
efc3a539ed support redirecting subprocesses' stdout/stderr to print!() so it gets captured for rust tests
Compare 5 commits »
programmerjake pushed to master at libre-chip/fayalite 2024-09-25 08:58:32 +00:00
57aa849615 add WIP formal proof for queue()
d477252bde add assert_formal helper for running formal proofs in rust tests
Compare 2 commits »
programmerjake pushed to master at libre-chip/fayalite 2024-09-25 08:56:13 +00:00
6b0eea8295 add WIP formal proof for queue()
programmerjake pushed to master at libre-chip/fayalite 2024-09-25 08:54:56 +00:00
8489bd06f0 add assert_formal helper for running formal proofs in rust tests
37bc6eb639 add formal subcommand
e2de8c3d99 add command line options for selecting which transforms to apply when generating firrtl
42945b1f9c support redirecting subprocesses' stdout/stderr to print!() so it gets captured for rust tests
f32c0a7863 switch to #[derive(Parser)] instead of #[derive(Args)]
Compare 6 commits »