cesar/fayalite
1
0
Fork 0
forked from libre-chip/fayalite
Code Pull requests Activity
192 commits 4 branches 2 tags 6.4 MiB
Commit graph

192 commits

Author SHA1 Message Date
Cesar Strauss
fef7fea3ea 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-24 07:06:28 -03:00
Jacob Lifshay
9b06019bf5
make sim::Compiler not print things to stdout unless you ask for it 2024-12-18 21:15:09 -08:00
Jacob Lifshay
36bad52978
sim: fix sim.write to struct 2024-12-18 20:50:50 -08:00
Jacob Lifshay
21c73051ec
sim: add SimValue and reading/writing more than just a scalar 2024-12-18 01:39:35 -08:00
Jacob Lifshay
304d8da0e8
Merge remote-tracking branch 'origin/master' into adding-simulator 2024-12-13 15:06:45 -08:00
Jacob Lifshay
2af38de900
add more memory tests 2024-12-13 15:04:48 -08:00
Jacob Lifshay
c756aeec70
tests/sim: add test for memory rw port 2024-12-12 20:50:41 -08:00
Jacob Lifshay
903ca1bf30
sim: simple memory test works! 2024-12-12 19:47:57 -08:00
Jacob Lifshay
8d030ac65d
sim/interpreter: add addresses to instruction listing 2024-12-12 16:25:38 -08:00
Jacob Lifshay
562c479b62
sim/interpreter: fix StatePartLayout name in debug output 2024-12-12 15:06:17 -08:00
Jacob Lifshay
393f78a14d
sim: add WIP memory test 2024-12-11 23:28:15 -08:00
Jacob Lifshay
8616ee4737
tests/sim: test_enums works! 2024-12-11 00:01:04 -08:00
Jacob Lifshay
5087f16099
sim: fix assignments graph by properly including conditions as assignment inputs 2024-12-11 00:00:21 -08:00
Jacob Lifshay
6b31e6d515
sim: add .dot output for Assignments graph for debugging 2024-12-10 23:40:33 -08:00
Jacob Lifshay
564ccb30bc
sim/vcd: fix variable identifiers to follow verilog rules 2024-12-10 23:39:17 -08:00
Jacob Lifshay
ca759168ff
tests/sim: add WIP test for enums 2024-12-10 23:37:26 -08:00
Jacob Lifshay
e4cf66adf8
sim: implement memories, still needs testing 2024-12-09 23:03:01 -08:00
Jacob Lifshay
cd0dd7b7ee
change memory write latency to NonZeroUsize to match read latency being usize 2024-12-09 23:01:40 -08:00
Cesar Strauss
2e7d685dc7 add module exercising formal verification of memories 2024-12-08 17:13:26 -03:00
Jacob Lifshay
9654167ca3
sim: WIP working on memory 2024-12-06 15:53:34 -08:00
Jacob Lifshay
3ed7827485
sim: WIP adding memory support 2024-12-05 21:35:23 -08:00
Jacob Lifshay
e504cfebfe
add BoolOrIntType::copy_bits_from_bigint_wrapping and take BigInt arguments by reference 2024-12-05 20:32:15 -08:00
Jacob Lifshay
9f42cab471
change to version 0.3.0 for breaking change 2024-12-05 20:26:28 -08:00
Jacob Lifshay
259bee39c2
tests/sim: split expected output text into separate files 2024-12-05 18:17:13 -08:00
Jacob Lifshay
643816d5b5
vcd: handle enums with fields 2024-12-04 21:03:29 -08:00
Jacob Lifshay
42afd2da0e
sim: implement enums (except for connecting unequal enum types) 2024-12-04 20:58:39 -08:00
Jacob Lifshay
15bc304bb6
impl ToExpr for TargetBase 2024-12-04 20:57:44 -08:00
Jacob Lifshay
4422157db8
WIP adding enums to simulator 2024-12-02 21:06:23 -08:00
Jacob Lifshay
d3f52292a1
test doc tests in CI 2024-12-01 20:21:26 -08:00
Jacob Lifshay
fd45465d35
sim: add support for registers 2024-12-01 20:14:13 -08:00
Jacob Lifshay
5e0548db26
vcd: single bit signals have no spaces in their value changes 2024-12-01 20:12:43 -08:00
Jacob Lifshay
12b3ba57f1
add some ExprCastTo supertraits to ResetType to make generic code easier 2024-12-01 20:10:25 -08:00
Jacob Lifshay
965fe53077
deduce_resets: show more debugging info on assertion failure 2024-12-01 20:09:17 -08:00
Jacob Lifshay
3abba7f9eb
simulating circuits with deduced resets works 2024-11-27 23:52:07 -08:00
Jacob Lifshay
6446b71afd
deduce_resets works! 2024-11-27 23:24:11 -08:00
Jacob Lifshay
d36cf92d7f
make ToReset generic over the reset type 2024-11-27 23:19:55 -08:00
Jacob Lifshay
d744d85c66
working on deduce_resets 2024-11-27 01:31:18 -08:00
Jacob Lifshay
358cdd10c8
add more expr casts 2024-11-27 01:30:28 -08:00
Jacob Lifshay
9128a84284
Merge remote-tracking branch 'origin/master' into adding-simulator 2024-11-26 21:28:22 -08:00
Jacob Lifshay
546010739a
working on deduce_resets 2024-11-26 21:26:56 -08:00
Jacob Lifshay
9b5f1218fd
make ClockDomain and Reg generic over reset type 2024-11-26 20:47:03 -08:00
Jacob Lifshay
89d84551f8
add ResetType to the list of recognized type bounds 2024-11-26 18:52:03 -08:00
Jacob Lifshay
c45624e3c2
Fix SInt::for_value not accounting for sign bit for positive values 
Fixes:
2024-11-26 16:26:29 -08:00
Jacob Lifshay
7851bf545c
working on deduce_resets.rs 2024-11-26 00:07:11 -08:00
Jacob Lifshay
3e3da53bd2
working on deduce_resets 2024-11-25 00:01:02 -08:00
Jacob Lifshay
fa50930ff8
update petgraph dependency to include UnionFind::new_set() 2024-11-25 00:00:26 -08:00
Jacob Lifshay
9516fe03a1
increase rust version in CI too 2024-11-24 14:46:25 -08:00
Jacob Lifshay
52ab134673
increase rust version to support omitting match arms with uninhabited types 2024-11-24 14:41:39 -08:00
Jacob Lifshay
698b8adc23
working on deduce_resets pass 2024-11-24 14:39:32 -08:00
Jacob Lifshay
59be3bd645
WIP working on implementing deduce_resets pass 2024-11-24 03:44:31 -08:00