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
