Commit graph

158 commits

Author SHA1 Message Date
Jacob Lifshay 479d59b287
WIP implementing simulator 2024-11-20 22:53:54 -08:00
Jacob Lifshay 6f904148c4
WIP adding simulator 2024-11-20 22:53:54 -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 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 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 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 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 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 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 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
Jacob Lifshay d089095667
change default to --simplify-enums=replace-with-bundle-of-uints
All checks were successful
/ test (push) Successful in 4m42s
2024-10-01 00:07:48 -07:00
Jacob Lifshay 9d66fcc548
improve ExportOptions support in assert_export_firrtl! 2024-10-01 00:05:39 -07:00
Jacob Lifshay 186488a82e
remove FIXME now that simplify_enums is fixed 2024-09-30 23:31:45 -07:00
Jacob Lifshay edcea1adc3
add firrtl comments when connecting expressions with different types
All checks were successful
/ test (push) Successful in 4m44s
2024-09-30 22:33:27 -07:00
Jacob Lifshay 30a38bc8da
fix simplify_enums to properly handle nested enums and connects with different types 2024-09-30 22:31:16 -07:00
Jacob Lifshay 1e2831da47
add validation of connects and matches when validating module
this is useful for catching errors in transformation passes
2024-09-30 21:20:35 -07:00
Jacob Lifshay d2ba313f0f
fix simplify_memories trying to connect Bool with UInt 2024-09-30 21:19:20 -07:00
Jacob Lifshay 04752c5037
add test for connect_any with nested enums with different-sized variant bodies
All checks were successful
/ test (push) Successful in 4m42s
simplify_enums is currently broken in that case
2024-09-25 21:55:52 -07:00
Jacob Lifshay e661aeab11
add WIP formal proof for queue()
All checks were successful
/ test (push) Successful in 5m27s
2024-09-25 02:00:06 -07:00
Jacob Lifshay 5fc7dbd6e9
add assert_formal helper for running formal proofs in rust tests 2024-09-25 02:00:06 -07:00
Jacob Lifshay 45dbb554d0
add formal subcommand 2024-09-25 02:00:06 -07:00
Jacob Lifshay bb860d54cc
add command line options for selecting which transforms to apply when generating firrtl 2024-09-25 02:00:06 -07:00
Jacob Lifshay efc3a539ed
support redirecting subprocesses' stdout/stderr to print!() so it gets captured for rust tests 2024-09-25 02:00:06 -07:00
Jacob Lifshay f32c0a7863
switch to #[derive(Parser)] instead of #[derive(Args)] 2024-09-25 01:28:11 -07:00
Jacob Lifshay 4ff01690a7
clean up deps and move missed deps to workspace 2024-09-25 01:22:35 -07:00
Jacob Lifshay 28aad19bf5
add assert/assume/cover
All checks were successful
/ test (push) Successful in 4m33s
2024-09-23 19:10:51 -07:00
Jacob Lifshay 716c65edcd
add WIP version of queue()
All checks were successful
/ test (push) Successful in 4m36s
2024-09-22 18:59:12 -07:00
Jacob Lifshay f6146048d1
add memory::splat_mask to generate mask types from a Bool 2024-09-22 18:57:30 -07:00
Jacob Lifshay a701f99fd6
add repeat() 2024-09-22 18:56:26 -07:00
Jacob Lifshay 78edfc97b2
split int::IntCmp into expr::HdlPartialEq and expr::HdlPartialOrd
All checks were successful
/ test (push) Successful in 4m32s
2024-09-22 17:28:46 -07:00
Jacob Lifshay 9ad4ec0f39
add ty.uninit()
All checks were successful
/ test (push) Successful in 4m30s
2024-09-22 17:26:23 -07:00
Jacob Lifshay 8449854cac
add ToExpr for usize/isize/NonZero<T>
All checks were successful
/ test (push) Successful in 4m32s
2024-09-22 17:19:58 -07:00
Jacob Lifshay 790bb15408
remove reset_default from proc-macro, forgot to remove when removing from RegBuilder 2024-09-22 16:03:20 -07:00
Jacob Lifshay 10ae95fac1
add missing copyright headers 2024-09-22 15:30:05 -07:00
Jacob Lifshay 51ce7b079e
add ReadyValid<T>
All checks were successful
/ test (push) Successful in 4m26s
2024-09-20 19:11:30 -07:00
Jacob Lifshay ff269e5def
add utility functions on HdlOption, inspired by Option's API 2024-09-20 18:49:12 -07:00
Jacob Lifshay df55a514e4
add support for incomplete_wire -- a wire that you can supply the type of later 2024-09-20 18:46:56 -07:00
Jacob Lifshay ff94dda922
support #[hdl] on functions -- enables #[hdl] usage in function body 2024-09-20 18:42:24 -07:00
Jacob Lifshay a8c804ef4a
some final cleanups
All checks were successful
/ test (push) Successful in 5m43s
2024-09-19 23:52:32 -07:00
Jacob Lifshay 2d293ae87b
#[hdl] match works! 2024-09-19 23:51:54 -07:00
Jacob Lifshay 9887d70f41
fix handling of const and size type generics when generating Index impls
All checks were successful
/ test (push) Successful in 5m1s
2024-09-19 18:45:04 -07:00
Jacob Lifshay 2c1afd1cd6
const generics on hdl_module work!
All checks were successful
/ test (push) Successful in 4m54s
2024-09-17 15:39:23 -07:00
Jacob Lifshay 76ea7f82c3
WIP adding const generics
Some checks failed
/ test (push) Failing after 1m3s
2024-09-16 16:47:10 -07:00
Jacob Lifshay 5835b995a9
WIP: use HdlOption[the_type_var] or UInt[123 + n] for creating types
All checks were successful
/ test (push) Successful in 4m56s
2024-08-21 22:27:21 -07:00
Jacob Lifshay cd99dbc849
properly bound with StaticValue or StaticType<MaskType: StaticType>
All checks were successful
/ test (push) Successful in 14m38s
2024-07-30 20:25:37 -07:00
Jacob Lifshay 2dce478d48
rename FixedType->StaticType, fixed_type()->static_type(), hdl(fixed_type)->hdl(static), IsFixedLen->IsStaticLen 2024-07-30 20:16:00 -07:00
Jacob Lifshay be025c14ca
split up util.rs
All checks were successful
/ test (push) Successful in 14m43s
2024-07-28 22:08:51 -07:00
Jacob Lifshay 14a9c23697
change raw url to a link 2024-07-28 22:08:22 -07:00
Jacob Lifshay 305805d237
fix wire example to actually be about wires, not registers
All checks were successful
/ test (push) Successful in 14m43s
2024-07-26 14:15:34 -07:00
Jacob Lifshay b33566841d
make #[hdl_module] support functions with generic parameters
All checks were successful
/ test (push) Successful in 14m40s
2024-07-25 22:20:38 -07:00
Jacob Lifshay ef4b3b4081
make [T; N]: ToExpr for any N instead of a fixed list 2024-07-25 22:08:28 -07:00
Jacob Lifshay 7963f0a5cd
add Iterator<Item = Pair<T, P>> helpers 2024-07-25 22:07:23 -07:00
Jacob Lifshay c94a437686
add cli option to set verilog dialect
All checks were successful
/ test (push) Successful in 14m49s
2024-07-24 23:13:56 -07:00
Jacob Lifshay f582013c1b
add cli for compiling to verilog
All checks were successful
/ test (push) Successful in 15m23s
2024-07-23 23:49:39 -07:00
Jacob Lifshay 0611044941
Fix typo
All checks were successful
/ test (push) Successful in 14m36s
Fixes: #1
2024-07-22 15:58:05 -07:00
Jacob Lifshay 180ecad017
fix doctests to use Expr<UInt<1>> instead of bool for example conditions
All checks were successful
/ test (push) Successful in 14m40s
2024-07-22 02:20:06 -07:00
Jacob Lifshay 0edf380c79
refactor fayalite::cli to expose subcommands
Some checks failed
/ test (push) Failing after 13m29s
2024-07-22 01:41:45 -07:00
Jacob Lifshay 37d03cec33
change #[hdl] if to only accept Expr<T> instead of accepting bool, this prevents using == by accident 2024-07-22 00:52:48 -07:00
Jacob Lifshay 79031ccf88
fix blinky example to use cmp_eq instead of == 2024-07-22 00:52:29 -07:00
Jacob Lifshay 5707ede2ae
support IntCmp with primitive integer types 2024-07-22 00:50:53 -07:00
Jacob Lifshay 422330d195
fix doc test
All checks were successful
/ test (push) Successful in 15m15s
2024-07-21 21:09:31 -07:00
Jacob Lifshay a191ece9a5
add blinky example
Some checks failed
/ test (push) Failing after 7m59s
2024-07-21 20:48:43 -07:00
Jacob Lifshay 23a77368b3
add beginnings of simple CLI 2024-07-21 20:47:52 -07:00
Jacob Lifshay 8080cc7b5c
add utility functions for getting smallest integer type that fits a range/value 2024-07-21 20:46:23 -07:00
Jacob Lifshay bdfa18e11d
add IntTypeTrait::literal utility function 2024-07-21 20:45:36 -07:00
Jacob Lifshay 8ca0cd56c4
fix warning 2024-07-21 20:44:29 -07:00
Jacob Lifshay 1809fccb45
clarify docs some more
All checks were successful
/ test (push) Successful in 14m27s
2024-07-21 17:38:54 -07:00
Jacob Lifshay 5cf638c74a
fix broken doc tests
All checks were successful
/ test (push) Successful in 14m25s
2024-07-19 17:14:09 -07:00
Jacob Lifshay dba883e300
split <int>.cast() into cast_as_type and cast to be more useful when casting to deduced fixed types 2024-07-19 17:12:29 -07:00
Jacob Lifshay af95bb2f58
write docs for #[hdl] expressions
All checks were successful
/ test (push) Successful in 8m53s
2024-07-18 00:51:01 -07:00
Jacob Lifshay 153dc261e3
WIP writing docs -- refactor #[hdl] docs to be a module tree for easier navigation
All checks were successful
/ test (push) Successful in 9m51s
2024-07-18 00:13:28 -07:00
Jacob Lifshay 190e440b35
WIP adding docs
All checks were successful
/ test (push) Successful in 9m6s
2024-07-16 19:46:52 -07:00
Jacob Lifshay 86827def91
rename ClockDomain fields to clk and rst for consistency 2024-07-16 19:46:08 -07:00