whitequark
b92e967b78
lib.fifo: make fwft a keyword-only argument.
...
Because it accepts a boolean.
2019-09-12 19:38:18 +00:00
whitequark
1c091e67a4
lib.fifo: remove SyncFIFO.replace.
...
This obscure functionality was likely only ever used in old MiSoC
code, and doesn't justify the added complexity. It was also not
provided (and could not be reasonably provided) in SyncFIFOBuffered,
which made its utility extremely marginal.
2019-09-12 19:16:57 +00:00
whitequark
eb04a2509e
hdl.mem,lib,examples: use Signal.range().
2019-09-08 12:19:13 +00:00
whitequark
32bfbb11cb
formal→asserts
...
Closes #171 .
2019-08-19 20:23:24 +00:00
whitequark
ed7e07c6c1
hdl.ast: implement Initial.
...
This is the last remaining part for first-class formal support.
2019-08-15 02:53:07 +00:00
whitequark
94e8f479a5
hdl.mem: use read_port(domain="comb") for asynchronous read ports.
...
This avoids the absurdity of the combination of arguments that is
read_port(domain="sync", synchronous=True).
Fixes #116 .
2019-07-01 19:56:49 +00:00
whitequark
9f643ce005
Clean up imports.
...
This commit:
* moves lists of universally useful imports from `nmigen` to
`nmigen.hdl` and `nmigen.lib`, reimporting them in `nmigen`;
* replaces lots of imports from individual parts of `nmigen.hdl`
with a star import from `nmigen.hdl`;
* replaces imports in tests with what we expect downstream code
to use;
* adds some missing imports in `nmigen.formal`.
2019-06-04 08:18:50 +00:00
whitequark
44711b7d08
hdl.ir: detect elaboratables that are created but not used.
...
Requres every elaboratable to inherit from Elaboratable, but still
accepts ones that do not, with a warning.
Fixes #3 .
2019-04-21 08:52:57 +00:00
whitequark
4948162f33
hdl.ir: rename .get_fragment() to .elaborate().
...
Closes #9 .
2019-01-26 02:31:12 +00:00
whitequark
e33580cf4c
lib.fifo: add AsyncFIFO and AsyncFIFOBuffered.
2019-01-21 16:02:46 +00:00
whitequark
9de9272709
lib.fifo: use memory in the FIFO model.
...
This is unfortunately more complicated, but results in a much faster
proof.
2019-01-19 09:27:56 +00:00
whitequark
6ea0a12dd4
lib.fifo: use model equivalence to simplify formal specification.
...
This is unfortunately slow, and should probably be using theory
of arrays.
2019-01-19 09:27:56 +00:00
whitequark
c5d67b0461
hdl.xfrm: mark internal registers used in lowering Sample().
2019-01-19 07:27:32 +00:00
whitequark
97b990272e
lib.fifo: formally verify FIFO contract.
2019-01-19 00:52:56 +00:00
whitequark
5a831ce31c
lib.fifo: add basic formal specification.
2019-01-17 05:40:25 +00:00
whitequark
b78a2be9f6
lib.fifo: port sync FIFO queues from Migen.
2019-01-16 17:20:38 +00:00