Commit graph

21 commits

Author SHA1 Message Date
whitequark 2da0133d52 lib.fifo: change FIFOInterface() diagnostics to follow Memory(). 2019-09-23 11:03:50 +00:00
whitequark ca6b1f2f1c lib.fifo: round up AsyncFIFO{,Buffered} depth to lowest valid value.
Unless exact_depth=True is specified.

The logic introduced in this commit is idempotent: that is, if one
uses the depth of one AsyncFIFOBuffered in the constructor of another
AsyncFIFOBuffered, they will end up with the same depth. More naive
logic would result in an unbounded, quadratic growth with each such
step.

Fixes #219.
2019-09-23 10:58:20 +00:00
whitequark a57b76fb5d lib.fifo: make simulation read() and write() functions compat-only.
These functions were originally changed in 3ed51938, in an attempt
to make them take one cycle instead of two. However, this does not
actually work because of drawbacks of the simulator interface.

Avoid committing to any specific implementation for now, and instead
make them compat-only extensions.
2019-09-23 08:46:12 +00:00
whitequark 276e9c2fad test.test_lib_fifo: fix typo. 2019-09-20 11:53:05 +00:00
whitequark da4b810fe1 lib.fifo: adjust properties to have consistent naming. 2019-09-13 12:33:41 +00:00
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