Commit graph

129 commits

Author SHA1 Message Date
Jacob Lifshay c45624e3c2
Fix SInt::for_value not accounting for sign bit for positive values
All checks were successful
/ deps (pull_request) Successful in 14s
/ test (pull_request) Successful in 4m42s
/ deps (push) Successful in 13s
/ test (push) Successful in 4m39s
Fixes: #4
2024-11-26 16:26:29 -08:00
Jacob Lifshay 3ea0d98924
always write formal cache json
All checks were successful
/ deps (push) Successful in 15s
/ test (push) Successful in 4m37s
2024-11-20 22:51:40 -08:00
Cesar Strauss c1f1a8b749 Add test module exercising formal verification.
All checks were successful
/ deps (pull_request) Successful in 15s
/ test (pull_request) Successful in 4m47s
/ deps (push) Successful in 13s
/ test (push) Successful in 5m16s
2024-11-20 18:29:39 -03:00
Jacob Lifshay 3d5d8c54b6
add repository to cache key
All checks were successful
/ deps (push) Successful in 10m39s
/ test (push) Successful in 5m14s
2024-10-30 20:55:02 -07:00
Jacob Lifshay ee15fd2b94
support #[hdl] type aliases
All checks were successful
/ deps (push) Successful in 11m28s
/ test (push) Successful in 4m40s
2024-10-30 20:47:10 -07:00
Jacob Lifshay 20cf0abbcc
fix using #[hdl] types like S<{ 1 + 2 }> 2024-10-30 20:46:11 -07:00
Jacob Lifshay 5bd0de48b7
change to version 0.2.1 2024-10-30 19:36:05 -07:00
Jacob Lifshay 0c9c48a066
split out deps into separate workflow with better caching using deps.yml from cpu.git
All checks were successful
/ deps (push) Successful in 21s
/ test (push) Successful in 19m32s
2024-10-17 21:05:18 -07:00
Jacob Lifshay cb17913004
limit sby to one thread each since it seems not to respect job count in parallel mode
All checks were successful
/ test (push) Successful in 46m32s
2024-10-15 21:32:38 -07:00
Jacob Lifshay 42effd1132
switch to using a make job server for managing test parallelism
Some checks failed
/ test (push) Failing after 39m16s
2024-10-15 20:32:33 -07:00
Jacob Lifshay 3d0f95cfe5
formal: add workaround for wires disappearing because yosys optimizes them out
All checks were successful
/ test (push) Successful in 39m13s
2024-10-15 01:48:48 -07:00
Jacob Lifshay 3939ce2360
add Bundle and Enum to prelude
All checks were successful
/ test (push) Successful in 39m33s
2024-10-14 17:47:58 -07:00
Jacob Lifshay d0229fbcfb
get #[hdl] struct S<A: KnownSize, B: KnownSize> to work
All checks were successful
/ test (push) Successful in 39m2s
2024-10-11 17:30:49 -07:00
Jacob Lifshay 4909724995
add more thorough checks that bounds are properly handled on #[hdl] structs
All checks were successful
/ test (push) Successful in 37m37s
2024-10-10 23:34:46 -07:00
Jacob Lifshay d0694cbd52
add disabled test for #[hdl] struct S4<W: KnownSize, W2: KnownSize> which type errors
Some checks failed
/ test (push) Has been cancelled
2024-10-10 22:58:15 -07:00
Jacob Lifshay 1a2149b040
silence warnings for field names that start with _
All checks were successful
/ test (push) Successful in 37m30s
2024-10-10 20:53:29 -07:00
Jacob Lifshay 59cef3f398
add PhantomData as a hdl bundle
Some checks failed
/ test (push) Has been cancelled
2024-10-10 20:48:09 -07:00
Jacob Lifshay bf907c3872
cache results of formal proofs
All checks were successful
/ test (push) Successful in 39m54s
2024-10-07 23:31:24 -07:00
Jacob Lifshay 99180eb3b4
fix clippy lints in generated code
All checks were successful
/ test (push) Successful in 37m34s
2024-10-07 22:06:59 -07:00
Jacob Lifshay 017c14a2f1
don't use #[allow(..., reason = "...")] since that's not stable yet on rust 1.80.1 2024-10-07 22:06:59 -07:00
Jacob Lifshay ed1aea41f3
clean up some clippy warnings
Some checks failed
/ test (push) Failing after 3m41s
2024-10-07 21:49:18 -07:00
Jacob Lifshay f12322aa2a
remove interning contexts 2024-10-07 21:33:56 -07:00
Jacob Lifshay 44ca1a607a
remove unused AGCContext 2024-10-07 21:23:13 -07:00
Jacob Lifshay 30b9a5e48d
change NameId to have an opaque Id so output firrtl doesn't depend on how many modules of the same name were ever created
All checks were successful
/ test (push) Successful in 39m6s
2024-10-07 19:06:01 -07:00
Jacob Lifshay eed0afc6ab
add some utility From<Interned<T>> impls 2024-10-07 19:05:20 -07:00
Jacob Lifshay aec383c0af
try to fix ccache
All checks were successful
/ test (push) Successful in 1h19m11s
2024-10-06 20:57:42 -07:00
Jacob Lifshay f403eed7c0
only run tests once, since they are quite slow
Some checks failed
/ test (push) Has been cancelled
2024-10-06 20:08:39 -07:00
Jacob Lifshay 2e8b73d2fc
rename fire/fire_data to firing/firing_data 2024-10-06 19:04:48 -07:00
Jacob Lifshay e05c368688
change register names to end in _reg by convention 2024-10-06 18:50:09 -07:00
Jacob Lifshay ec77559e2b
fix cache action name
All checks were successful
/ test (push) Successful in 1h44m43s
2024-10-04 17:10:06 -07:00
Jacob Lifshay 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)
Some checks failed
/ test (push) Has been cancelled
2024-10-04 17:03:51 -07:00
Jacob Lifshay 487af07154
yosys build runs out of memory
Some checks failed
/ test (push) Failing after 1h8m27s
2024-10-04 01:03:17 -07:00
Jacob Lifshay c0d4de56a9
try to make yosys build faster
Some checks failed
/ test (push) Failing after 24m17s
2024-10-03 23:40:44 -07:00
Jacob Lifshay 9f154e6b96
try caching ccache manually
Some checks are pending
/ test (push) Waiting to run
2024-10-03 23:36:39 -07:00
Jacob Lifshay 0d54b9a2a9
queue formal proof passes!
Some checks are pending
/ test (push) Has started running
2024-10-03 23:07:14 -07:00
Jacob Lifshay 343805f80b
fix #[hdl] to work with unusual identifier hygiene from macros 2024-10-03 23:04:14 -07:00
Jacob Lifshay 15a28aa7a7
install python3-click -- needed by symbiyosys
All checks were successful
/ test (push) Successful in 33m5s
2024-10-03 01:44:06 -07:00
Jacob Lifshay 4084a70485
switch default solver to z3 2024-10-03 01:43:46 -07:00
Jacob Lifshay 3e2fb9b94f
WIP getting queue formal to pass -- passes for capacity <= 2
Some checks failed
/ test (push) Has been cancelled
2024-10-03 01:08:01 -07:00
Jacob Lifshay bc26fe32fd
add ccache and clean up deps
Some checks failed
/ test (push) Has been cancelled
2024-10-03 01:01:06 -07:00
Jacob Lifshay eb65bec26e
add yosys deps
Some checks failed
/ test (push) Has been cancelled
2024-10-03 00:44:04 -07:00
Jacob Lifshay 4497f09ea0
fix wrong build steps
Some checks failed
/ test (push) Failing after 1m2s
2024-10-03 00:39:18 -07:00
Jacob Lifshay 1c63a441a9
add needed tools to CI
Some checks failed
/ test (push) Failing after 1m5s
2024-10-03 00:35:43 -07:00
Jacob Lifshay 0cf01600b3
add mod formal and move assert/assume/cover stuff to it 2024-10-01 19:56:17 -07:00
Jacob Lifshay f3d6528f5b
make annotations easier to use 2024-10-01 19:54:17 -07:00
Jacob Lifshay f35d88d2bb
remove unused valueless.rs 2024-10-01 18:41:41 -07:00
Jacob Lifshay e8c393f3bb
sort pub mod items 2024-10-01 18:40:52 -07:00
Jacob Lifshay d0b406d288
add more annotation kinds
All checks were successful
/ test (push) Successful in 4m45s
2024-10-01 18:33:32 -07:00
Jacob Lifshay 2a25dd9d7b
fix annotations getting lost 2024-10-01 18:31:44 -07:00
Jacob Lifshay 6e0b6c000d
remove stray debugging prints 2024-10-01 18:30:46 -07:00