whitequark [Tue, 22 Jan 2019 07:03:46 +0000 (07:03 +0000)]
lib.fifo: in FIFOInterface.read(), check readable on the right cycle.
whitequark [Tue, 22 Jan 2019 06:56:46 +0000 (06:56 +0000)]
compat.genlib.fifo: adjust _FIFOInterface shim to not require fwft=.
whitequark [Tue, 22 Jan 2019 05:47:50 +0000 (05:47 +0000)]
lib.fifo: fix typo in AsyncFIFO documentation.
whitequark [Mon, 21 Jan 2019 16:02:46 +0000 (16:02 +0000)]
lib.fifo: add AsyncFIFO and AsyncFIFOBuffered.
whitequark [Mon, 21 Jan 2019 16:00:25 +0000 (16:00 +0000)]
back.pysim: wake up processes before ever committing any values.
Otherwise, the contract of the simulator to sync processes is not
always fulfilled.
whitequark [Sun, 20 Jan 2019 03:03:48 +0000 (03:03 +0000)]
compat.genlib.cdc: add missing import.
whitequark [Sun, 20 Jan 2019 02:29:08 +0000 (02:29 +0000)]
compat.genlib.cdc: add GrayCounter and GrayDecoder shims.
whitequark [Sun, 20 Jan 2019 02:20:34 +0000 (02:20 +0000)]
lib.coding: add GrayEncoder and GrayDecoder.
Unlike the Migen ones, these are purely combinatorial.
whitequark [Sun, 20 Jan 2019 01:59:09 +0000 (01:59 +0000)]
lib.coding: add width as attribute to all coders.
whitequark [Sat, 19 Jan 2019 09:27:13 +0000 (09:27 +0000)]
lib.fifo: use memory in the FIFO model.
This is unfortunately more complicated, but results in a much faster
proof.
whitequark [Sat, 19 Jan 2019 08:57:18 +0000 (08:57 +0000)]
lib.fifo: use model equivalence to simplify formal specification.
This is unfortunately slow, and should probably be using theory
of arrays.
whitequark [Sat, 19 Jan 2019 09:26:26 +0000 (09:26 +0000)]
hdl.ast: implement shape for modulo operator.
whitequark [Sat, 19 Jan 2019 08:56:44 +0000 (08:56 +0000)]
hdl.ast: add Value.implies.
whitequark [Sat, 19 Jan 2019 06:02:04 +0000 (06:02 +0000)]
hdl.xfrm: mark internal registers used in lowering Sample().
whitequark [Sat, 19 Jan 2019 01:01:32 +0000 (01:01 +0000)]
doc: update COMPAT_SUMMARY.
whitequark [Sat, 19 Jan 2019 02:19:06 +0000 (02:19 +0000)]
fhdl.specials: add compatibility shim for Tristate.
whitequark [Sat, 19 Jan 2019 01:37:58 +0000 (01:37 +0000)]
lib.fifo: fix simulation read/write methods to take only one cycle.
whitequark [Sat, 19 Jan 2019 01:06:27 +0000 (01:06 +0000)]
compat.genlib.fifo: add aliases for SyncFIFO, SyncFIFOBuffered.
whitequark [Sat, 19 Jan 2019 00:52:56 +0000 (00:52 +0000)]
lib.fifo: formally verify FIFO contract.
whitequark [Sat, 19 Jan 2019 00:08:51 +0000 (00:08 +0000)]
hdl.ast: give Assert and Assume their own src_loc.
This helps with patterns like `Assert(fsm.ongoing("IDLE"))`, which
would otherwise point into nMigen internals.
whitequark [Fri, 18 Jan 2019 01:27:17 +0000 (01:27 +0000)]
back.rtlil: only emit each AnyConst/AnySeq cell once.
These are semantically like signals, not like constants.
Alain Péteut [Thu, 17 Jan 2019 20:32:47 +0000 (21:32 +0100)]
cli: add missing default for `generate`
whitequark [Thu, 17 Jan 2019 05:26:54 +0000 (05:26 +0000)]
lib.fifo: add basic formal specification.
whitequark [Thu, 17 Jan 2019 05:23:06 +0000 (05:23 +0000)]
hdl.ast: allow sampling ClockSignal, ResetSignal.
whitequark [Thu, 17 Jan 2019 04:31:27 +0000 (04:31 +0000)]
hdl.ast: add Past, Stable, Rose, Fell.
whitequark [Thu, 17 Jan 2019 01:43:07 +0000 (01:43 +0000)]
formal: extract from toplevel module.
The nMigen formal language is about to get *much* larger and will
keep growing faster than the rest of nMigen language, so it makes
good sense to extract it. Further, this makes it easier to qualify
formal keywords like `formal.AnyConst()` without directly importing
hdl.ast.
whitequark [Thu, 17 Jan 2019 01:41:02 +0000 (01:41 +0000)]
hdl.xfrm: add SampleLowerer.
whitequark [Thu, 17 Jan 2019 01:36:27 +0000 (01:36 +0000)]
hdl.ast: add Sample.
whitequark [Wed, 16 Jan 2019 17:19:46 +0000 (17:19 +0000)]
lib.fifo: port sync FIFO queues from Migen.
whitequark [Wed, 16 Jan 2019 15:55:28 +0000 (15:55 +0000)]
hdl.ast: fix naming of Signal.like() signals when tracer fails.
whitequark [Wed, 16 Jan 2019 17:20:30 +0000 (17:20 +0000)]
back.rtlil: slightly nicer naming for $next signals. NFC.
whitequark [Wed, 16 Jan 2019 14:51:20 +0000 (14:51 +0000)]
back.rtlil: rename \sig$next to $next$sig.
These used to serve a useful purpose being public, back when the RTLIL
backend was immature. Not anymore; now they merely clutter up views
in gtkwave and so on.
whitequark [Wed, 16 Jan 2019 00:57:09 +0000 (00:57 +0000)]
Travis: install SymbiYosys and Yices2.
In preparation for adding formal tests.
whitequark [Tue, 15 Jan 2019 23:09:10 +0000 (23:09 +0000)]
William D. Jones [Tue, 15 Jan 2019 21:06:19 +0000 (16:06 -0500)]
back.rtlil: Generate $anyconst and $anyseq cells.
William D. Jones [Tue, 15 Jan 2019 21:05:25 +0000 (16:05 -0500)]
hdl.xfrm: Add on_AnyConst and on_AnySeq abstract methods for ValueVisitor and children.
William D. Jones [Tue, 15 Jan 2019 20:13:47 +0000 (15:13 -0500)]
hdl.ast: Add AnyConst and AnySeq value types.
Sebastien Bourdeauducq [Tue, 15 Jan 2019 07:58:38 +0000 (15:58 +0800)]
README: add LambdaConcept sponsorship
whitequark [Mon, 14 Jan 2019 21:39:19 +0000 (21:39 +0000)]
lib.io: pass pin to platform.get_tristate().
whitequark [Mon, 14 Jan 2019 17:04:23 +0000 (17:04 +0000)]
hdl.ir: allow explicitly requesting flattening.
whitequark [Mon, 14 Jan 2019 16:50:04 +0000 (16:50 +0000)]
lib.io: lower to platform-independent tristate buffer.
whitequark [Mon, 14 Jan 2019 15:38:16 +0000 (15:38 +0000)]
hdl: make ClockSignal and ResetSignal usable on LHS.
Fixes #8.
whitequark [Sun, 13 Jan 2019 08:51:49 +0000 (08:51 +0000)]
hdl.dsl: cases wider than switch test value are unreachable.
In
3083c1d6 they were erroneously fixed via truncation.
whitequark [Sun, 13 Jan 2019 08:46:28 +0000 (08:46 +0000)]
hdl.dsl: accept (but warn on) cases wider than switch test value.
Fixes #13.
whitequark [Sun, 13 Jan 2019 08:31:38 +0000 (08:31 +0000)]
back.pysim: handle non-driven, non-port signals.
Fixes #20.
whitequark [Sun, 13 Jan 2019 08:10:23 +0000 (08:10 +0000)]
back.verilog: better error message if Yosys is not found.
Fixes #17.
whitequark [Tue, 8 Jan 2019 20:42:56 +0000 (20:42 +0000)]
back.verilog: remove undriven check.
This check no longer finds bugs and is prone to false positives.
Instead, we should do integration tests on the entire stack, from
fragments to Verilog.
Fixes #23.
Adam Greig [Sun, 6 Jan 2019 00:10:37 +0000 (00:10 +0000)]
Give the top level scope a name to fix VCD hierarchy.
whitequark [Wed, 2 Jan 2019 18:14:57 +0000 (18:14 +0000)]
hdl.ast: allow slicing [n:n] into n-bit value.
whitequark [Wed, 2 Jan 2019 18:14:29 +0000 (18:14 +0000)]
back.rtlil: translate empty slices correctly.
William D. Jones [Tue, 1 Jan 2019 06:31:54 +0000 (01:31 -0500)]
back.rtlil: Generate RTLIL for Assert/Assume statements.
William D. Jones [Sun, 30 Dec 2018 10:17:39 +0000 (05:17 -0500)]
hdl.xfrm: Add Assert and Assume abstract methods for StatementVisitor, implement for children.
William D. Jones [Fri, 28 Dec 2018 07:10:15 +0000 (02:10 -0500)]
hdl.dsl: Support Assert and Assume where an Assign can occur.
William D. Jones [Fri, 28 Dec 2018 06:33:19 +0000 (01:33 -0500)]
hdl.ast: Add Assert and Assign statements.
whitequark [Tue, 1 Jan 2019 09:50:39 +0000 (09:50 +0000)]
hdl.ast: experimentally add Value._as_const.
Useful for writing e.g. decoders that accept Cat, etc as argument.
whitequark [Tue, 1 Jan 2019 08:50:28 +0000 (08:50 +0000)]
back.rtlil: fix typo.
whitequark [Tue, 1 Jan 2019 03:39:12 +0000 (03:39 +0000)]
hdl.rec: include record name in error message.
whitequark [Tue, 1 Jan 2019 03:35:34 +0000 (03:35 +0000)]
hdl.rec: use a helpful error on unknown field reference.
whitequark [Tue, 1 Jan 2019 03:08:10 +0000 (03:08 +0000)]
hdl.mem: add DummyPort, for testing and verification.
whitequark [Mon, 31 Dec 2018 03:43:34 +0000 (03:43 +0000)]
back.rtlil: match shape of Array elements to ArrayProxy shape.
Fixes #15.
whitequark [Mon, 31 Dec 2018 03:37:38 +0000 (03:37 +0000)]
back.rtlil: fix typo.
whitequark [Sat, 29 Dec 2018 15:02:44 +0000 (15:02 +0000)]
lib.cdc: fix tests to actually run.
whitequark [Sat, 29 Dec 2018 15:02:04 +0000 (15:02 +0000)]
back.pysim: warn if simulation is not run.
This would have prevented
3ea35b85.
whitequark [Fri, 28 Dec 2018 13:22:10 +0000 (13:22 +0000)]
hdl.rec: add basic record support.
whitequark [Fri, 28 Dec 2018 01:31:24 +0000 (01:31 +0000)]
tracer: factor out get_src_loc().
whitequark [Thu, 27 Dec 2018 21:45:55 +0000 (21:45 +0000)]
lib.coding: fix tests to actually run, and fix code to fix tests.
whitequark [Thu, 27 Dec 2018 16:02:31 +0000 (16:02 +0000)]
hdl.dsl: add support for fsm.ongoing().
whitequark [Wed, 26 Dec 2018 17:15:54 +0000 (17:15 +0000)]
hdl.mem: add missing __all__.
Jean-François Nguyen [Wed, 26 Dec 2018 14:29:48 +0000 (15:29 +0100)]
compat.genlib.coding: fix import.
whitequark [Wed, 26 Dec 2018 13:19:34 +0000 (13:19 +0000)]
lib.coding: port from Migen.
whitequark [Wed, 26 Dec 2018 12:58:30 +0000 (12:58 +0000)]
lib.cdc: add tests for MultiReg.
whitequark [Wed, 26 Dec 2018 12:42:43 +0000 (12:42 +0000)]
hdl.dsl: forbid m.next= inside of FSM but outside of FSM state, too.
whitequark [Wed, 26 Dec 2018 12:39:05 +0000 (12:39 +0000)]
hdl.dsl: provide generated values for FSMs.
whitequark [Wed, 26 Dec 2018 12:35:27 +0000 (12:35 +0000)]
hdl.ir: add an API for retrieving generated values, like FSM signal.
This is useful for tests.
whitequark [Wed, 26 Dec 2018 10:10:27 +0000 (10:10 +0000)]
examples: add an FSM usage example (UART receiver).
whitequark [Wed, 26 Dec 2018 09:45:12 +0000 (09:45 +0000)]
hdl.dsl: add signal decoder to FSM state signal.
whitequark [Wed, 26 Dec 2018 08:55:04 +0000 (08:55 +0000)]
hdl.dsl: implement FSM.
whitequark [Wed, 26 Dec 2018 06:45:57 +0000 (06:45 +0000)]
back.rtlil: clarify $verilog_initial_trigger behavior. NFC.
whitequark [Mon, 24 Dec 2018 19:11:07 +0000 (19:11 +0000)]
back.rtlil: unbreak
d47c1f8a.
whitequark [Mon, 24 Dec 2018 09:31:51 +0000 (09:31 +0000)]
hdl.mem: allow omitting memory simulation logic.
Trying to transform very large arrays is slow.
whitequark [Mon, 24 Dec 2018 09:30:47 +0000 (09:30 +0000)]
back.rtlil: use one $meminit cell, not one per word.
This is *far* more efficient.
whitequark [Mon, 24 Dec 2018 02:17:28 +0000 (02:17 +0000)]
hdl.xfrm, back.rtlil: implement and use LHSGroupFilter.
This is a refactoring to simplify reusing the filtering code in
simulation, and separate that concern from backends in general.
whitequark [Mon, 24 Dec 2018 02:02:59 +0000 (02:02 +0000)]
hdl.xfrm: implement SwitchCleaner, for pruning empty switches.
whitequark [Mon, 24 Dec 2018 01:38:32 +0000 (01:38 +0000)]
back.rtlil: always output negative values as two's complement.
- is valid in RTLIL but means something entirely different.
whitequark [Sun, 23 Dec 2018 10:14:05 +0000 (10:14 +0000)]
back.rtlil: emit dummy logic to work around Verilog deficiencies.
whitequark [Sun, 23 Dec 2018 09:20:02 +0000 (09:20 +0000)]
back.rtlil: do not translate empty fragments.
The resulting Verilog confuses some frontends.
whitequark [Sun, 23 Dec 2018 07:17:33 +0000 (07:17 +0000)]
back.rtlil: only translate switch tests once.
This seems to affect synthesis with Yosys but only marginally.
It is mostly a speed and readability improvement.
whitequark [Sun, 23 Dec 2018 07:13:17 +0000 (07:13 +0000)]
cli: generate: guess file type from extension.
whitequark [Sun, 23 Dec 2018 06:47:38 +0000 (06:47 +0000)]
back.rtlil: fix swapped operands in mux codegen.
whitequark [Sat, 22 Dec 2018 23:56:02 +0000 (23:56 +0000)]
cli: new module, for basic design generaton/simulation.
whitequark [Sat, 22 Dec 2018 22:19:14 +0000 (22:19 +0000)]
hdl.xfrm: avoid cycles in union-find graph in LHSGroupAnalyzer.
whitequark [Sat, 22 Dec 2018 22:00:58 +0000 (22:00 +0000)]
compat.genlib.fsm: fix naming for non-Signal LHS.
whitequark [Sat, 22 Dec 2018 21:43:46 +0000 (21:43 +0000)]
hdl.ir: flatten hierarchy based on memory accesses, too.
whitequark [Sat, 22 Dec 2018 19:04:35 +0000 (19:04 +0000)]
hdl.ir: factor out _merge_subfragment. NFC.
whitequark [Sat, 22 Dec 2018 10:03:16 +0000 (10:03 +0000)]
back.rtlil: split processes as finely as possible.
This makes simulation work correctly (by introducing delta cycles,
and therefore, making the overall Verilog simulation deterministic)
at the price of pessimizing mux trees generated by Yosys and Synplify
frontends, sometimes severely.
whitequark [Sat, 22 Dec 2018 07:24:15 +0000 (07:24 +0000)]
back.rtlil: remove useless condition. NFC.
whitequark [Sat, 22 Dec 2018 06:50:32 +0000 (06:50 +0000)]
hdl.xfrm: implement LHSGroupAnalyzer.
whitequark [Sat, 22 Dec 2018 06:03:38 +0000 (06:03 +0000)]
hdl.xfrm: Abstract*Transformer→*Visitor
whitequark [Sat, 22 Dec 2018 05:27:42 +0000 (05:27 +0000)]
back.rtlil: always initialize the entire memory.
This avoids reading 'x from the memory in simulation. In general,
FPGA memories can only be initialized in block granularity, and
zero-initializing is cheap, so this is not a significant issue with
resource consumption.
whitequark [Sat, 22 Dec 2018 02:05:49 +0000 (02:05 +0000)]
compat: use nicer names for next_value/next_value_ce signals.