e7ee1e862e
switch ready_valid::queue formal proofs to use formal_global_clock
/ test (pull_request) Failing after 3m9s
2026-06-05 00:47:36 -07:00
5c594cbb68
reimplement fayalite::formal and add support to the simulator
...
Add support to the simulator for running hdl asserts/assumes and being
able to write to the formal global clock/reset and all any/all_const/seq that are used.
This allows you to use the exact same HDL code for running a simulation and for running a formal proof.
2026-06-05 00:46:30 -07:00
5d68885eaf
fayalite::testing: add checked_vcd_output!()
2026-06-05 00:35:19 -07:00
31353862ce
fayalite/src/module: check that expressions are visible where they are used, e.g. erroring when a wire is inside an if but used outside.
/ test (pull_request) Successful in 4m21s
/ test (push) Successful in 4m54s
2026-06-01 23:10:43 -07:00
b1116c4a1a
simplify_enums: cache folded expressions
2026-06-01 21:45:37 -07:00
6902aea3a6
firrtl: don't generate as many duplicate wires when compiling expressions
2026-06-01 20:53:22 -07:00
1880ed682f
speed up TraceAsString by caching the canonical type for can_substitute_type
2026-06-01 20:41:14 -07:00
cf3e6cfc6b
Add .to_trace_as_string() and clean up code
/ test (pull_request) Successful in 4m9s
/ test (push) Successful in 4m45s
2026-05-14 22:13:31 -07:00
ea183eac87
add TraceAsString<T> -- sim traces it as a string rather than all its internal fields
/ test (pull_request) Successful in 4m16s
/ test (push) Successful in 4m54s
2026-05-13 19:43:50 -07:00
26224abe1c
sim: properly update all VCD wires when they share simulation state
/ test (pull_request) Successful in 4m8s
/ test (push) Successful in 4m42s
2026-05-05 21:12:00 -07:00
2266315944
redo #[hdl(sim)] match/let destructuring to support matching values of type Type::SimValue
/ test (pull_request) Successful in 7m17s
/ test (push) Successful in 4m42s
2026-05-03 23:23:17 -07:00
7e9d7739fb
use #[hdl(cmp_eq)] for HdlOption and implement conversion <-> Option
/ test (pull_request) Successful in 4m6s
/ test (push) Successful in 4m40s
2026-05-01 18:46:36 -07:00
7516ec3c24
implement #[hdl(cmp_eq)] for enums
2026-05-01 18:34:49 -07:00
8e4eeef723
add support for custom debug/display formatting of #[hdl] structs/enums
...
/ test (pull_request) Successful in 4m6s
/ test (push) Successful in 4m41s
also cleans up default debug formatting to use the struct/enum name
(or MaskType<StructName>) instead of the implementation detail type name.
2026-04-30 23:10:49 -07:00
402f457c68
sim: Speed up updating traces by tracking which traces are written to
/ test (pull_request) Successful in 4m10s
/ test (push) Successful in 4m47s
2026-04-30 19:12:20 -07:00
8cff3687f7
Run Rocq tests.
/ test (pull_request) Successful in 8m7s
/ test (push) Successful in 4m58s
2026-03-30 19:36:24 -03:00
80b92c7dd3
change vcd output to have module contents under instance's name, more closely matching how it works in verilog
/ test (pull_request) Successful in 4m18s
/ test (push) Successful in 4m54s
2026-03-26 18:21:14 -07:00
2aa41137d4
add simulator tests for queue()
/ test (pull_request) Successful in 7m59s
/ test (push) Successful in 5m3s
2026-03-24 23:30:15 -07:00
a0b2dc085c
add test that simulator handles last-connect semantics properly
2026-03-24 23:29:30 -07:00
a8a541b357
sim/compiler: fix registers so they properly retain their old value when not written
2026-03-24 23:26:47 -07:00
52c41bb5db
display signals when panicking because not all inputs/outputs are written yet
2026-03-24 23:25:14 -07:00
a93e66d8ab
update ui test's expected output for having rust-src available
/ test (pull_request) Successful in 4m20s
/ test (push) Successful in 4m57s
2026-03-17 20:43:46 -07:00
eb3ca59053
add rust-src to CI
2026-03-17 20:42:54 -07:00
dbed947408
change VCD id generation to be based on hashing the path, making them better for git diff
/ test (pull_request) Successful in 7m51s
/ test (push) Failing after 5m18s
2026-02-23 20:05:10 -08:00
cb4e1f42c0
silence unused import warning
2026-02-23 16:07:46 -08:00
8c270b0e35
silence warning for enums with only one variant
2026-02-23 16:07:05 -08:00
c632e5d570
speed up simulation by optimizing SimulationImpl::read_traces
...
/ test (pull_request) Successful in 4m22s
/ test (push) Successful in 5m24s
this makes cpu/crates/cpu/tests/next_pc.rs take 56s instead of 168s
2026-02-04 15:41:09 -08:00
1bc835803b
speed up LazyInterned by redoing caching using RwLock and add a thread-local cache
/ test (pull_request) Successful in 4m28s
/ test (push) Successful in 5m32s
2026-02-03 18:00:36 -08:00
9db3240644
fix UI test's expected output
2026-02-03 18:00:36 -08:00
caa097db0b
change rust version to 1.93.0
2026-02-03 17:29:59 -08:00
a96efa9696
cache interned UInt/SInt types
/ test (pull_request) Successful in 4m8s
/ test (push) Successful in 4m44s
2026-02-02 17:51:30 -08:00
4ac1bcbc0a
change Interner to use a sharded hash table
2026-02-02 15:49:26 -08:00
39810043ea
move Interner into new mod interner
2026-02-02 15:44:37 -08:00
26b0dc3fd8
change Interner to pub(crate)
2026-02-02 15:42:12 -08:00
11281a9842
add a thread-local cache when using TypeIdMap
2026-02-01 21:19:32 -08:00
e366793204
don't compare function pointers -- they're non-deterministic
/ test (pull_request) Successful in 4m5s
/ test (push) Successful in 4m36s
2026-01-12 03:11:36 -08:00
a398f8f185
Define design safety, and prove it for 1-step and 2-step induction.
/ test (pull_request) Successful in 4m8s
/ test (push) Successful in 4m35s
2025-12-22 22:30:13 -03:00
4fd4371054
Spelling.
2025-12-22 22:30:06 -03:00
c97b44d9d6
simplify SimValue Debug format, making complex structures much easier to read
/ test (pull_request) Successful in 3m55s
/ test (push) Successful in 4m30s
2025-12-14 20:59:48 -08:00
fbe4585578
add FillInDefaultedGenerics<Type = Self> bound for SizeType
/ test (pull_request) Successful in 3m56s
/ test (push) Successful in 4m26s
2025-12-10 20:10:39 -08:00
e4210a672f
Check copyright header in Rocq files.
...
/ test (pull_request) Successful in 4m4s
/ test (push) Successful in 4m39s
If we ever add Verilog files, we can "or" both results, I guess.
2025-12-09 07:45:35 -03:00
e54558d848
Demonstrates state with multiple variables and hidden state.
/ test (pull_request) Failing after 22s
2025-12-08 22:00:49 -03:00
46f3519c76
Demonstrate a preliminary mapping from HDL to Rocq.
...
Starts with a very simple example, including a proof by induction.
2025-12-08 19:32:05 -03:00
9e803223d0
support operations directly on SimValue, UIntValue, and SIntValue, and shared references to those
/ test (pull_request) Successful in 3m59s
/ test (push) Successful in 4m38s
2025-11-24 00:14:53 -08:00
2a65aa2bd5
fix DynShr[SU]'s literal bits to properly shift right instead of left
2025-11-20 02:25:05 -08:00
2817cd3d58
support Rust's default binding modes when destructuring with #[hdl(sim)] let/match
/ test (pull_request) Successful in 4m47s
/ test (push) Successful in 5m25s
2025-11-14 00:20:54 -08:00
053c1b2b10
implement Display for SimValue<T>
2025-11-14 00:20:54 -08:00
17b58e8edb
add utility impls for SimValue<ArrayType<_, _>>
/ test (pull_request) Successful in 4m52s
/ test (push) Successful in 5m28s
2025-11-13 20:21:07 -08:00
df020e9c9b
add ExternModuleSimulatorState::read_past() and more output when simulator trace is enabled
/ test (pull_request) Successful in 4m52s
/ test (push) Successful in 5m28s
2025-11-12 22:31:45 -08:00
45fea70c18
add ExternModuleSimulationState::fork_join_scope
/ test (pull_request) Successful in 4m47s
/ test (push) Successful in 5m24s
2025-11-07 02:18:43 -08:00
