Commit Graph

13346 Commits

Author SHA1 Message Date
Krystine Sherwin afc25afaf9
Minor tidying 2023-08-07 12:58:52 +12:00
Krystine Sherwin 8ade2182b0
Move (most of) ExOth and ExAdv slides 2023-08-07 12:58:40 +12:00
Krystine Sherwin 7ab051778e
Add copypaste reminder for typical_phases.rst 2023-08-07 10:40:36 +12:00
github-actions[bot] e0ba07aed3 Bump version 2023-08-05 00:16:43 +00:00
Martin Povišer ff3c7873f5 wreduce: Group reconnections
Group the reconnections, so that instead of producing

  connect $auto$wreduce.cc:455:run$24 [0] 1'0
  connect $auto$wreduce.cc:455:run$23 [31] 1'0
  connect $auto$wreduce.cc:455:run$23 [30] 1'0
  ... (40 more lines)

we produce

  connect $auto$wreduce.cc:461:run$23 [31:11] 21'000000000000000000000
  connect $auto$wreduce.cc:461:run$24 [31:10] 22'0000000000000000000000

.
2023-08-04 14:43:59 +01:00
Miodrag Milanović 701b767736
Merge pull request #3871 from jix/smtbmc-sexpr-scan
smtbmc: Avoid quadratic behavior when scanning s-exprs
2023-08-04 14:47:50 +02:00
Krystine Sherwin 330a2272da
Converting PRESENTATION_ExSyn 2023-08-04 10:29:14 +12:00
Krystine Sherwin 4b40372446
Tidy/reflow some things 2023-08-03 10:37:43 +12:00
Krystine Sherwin 2c75b103d6
Include test suites doc with note 2023-08-03 09:20:30 +12:00
Krystine Sherwin 9a9aa2c45a
Finished presentation intro
Also some other tidy up.
2023-08-03 09:20:30 +12:00
Krystine Sherwin 20c2708383
Move presentation intro example
Rework images makefile a bit to get it to import and build from resources folder(s).
Currently requires running twice from a clean build due to the way it finds `.dot` files to convert.
2023-08-03 09:20:29 +12:00
Krystine Sherwin cd6e63e1a9
Moved presentation_prog 2023-08-03 09:20:29 +12:00
Krystine Sherwin 045c04096e
Reorganising documentation
Also changing to furo theme.
2023-08-03 09:20:29 +12:00
Krystine Sherwin 4f1cd66829
New structure headings
Also adds a note to readme for installing pdflatex if it's missing.
2023-08-03 09:20:24 +12:00
github-actions[bot] f37ce5c839 Bump version 2023-08-02 00:16:17 +00:00
Jannis Harder 77c7355d53 smtbmc: Avoid quadratic behavior when scanning s-exprs
The previous implementation for finding the end of a top-level s-expr
exhibited quadratic behavior as it would re-scan the complete input for
the current expression for every new line. For large designs with
trivial properties this could easily take seconds and dominate the
runtime over the actual solving.

This change remembers the current nesting level between lines, avoiding
the re-scanning.
2023-08-01 17:19:29 +02:00
Jannis Harder b9751ef0b0 Install yw.h and json.h 2023-08-01 13:51:04 +01:00
Martin Povišer f8325f66b7 opt_expr: Fix 'signed X>=0' replacement for wide output ports
If the `$ge` cell we are replacing has wide output port, the upper bits
on the port should be driven to zero. That's not what a `$not` cell with
a single-bit input does. Instead opt for a `$logic_not` cell, which does
zero-pad its output.

Fixes #3867.
2023-08-01 13:50:12 +01:00
Miodrag Milanović 8b2a3d60f4
Merge pull request #3841 from povik/test-aigmap
tests: Extend aigmap.ys with SAT comparison
2023-08-01 09:04:47 +02:00
github-actions[bot] 6bf6e3307c Bump version 2023-08-01 00:19:43 +00:00
Martin Povišer 93988ef5df tests: Extend aigmap.ys with SAT comparison
Extend the aigmap.ys test with SAT-based comparison of the original
cells and their AIG implementations.

This tests both the usual cells and the single-bit Yosys gates.
2023-07-31 16:26:50 +02:00
Jannis Harder 0a3f805daa
Merge pull request #3840 from povik/cellaigs-cmp-cells 2023-07-31 16:23:39 +02:00
Miodrag Milanović 809466c5c5
Merge pull request #3861 from YosysHQ/verific_blackbox
Add ability to blackbox modules/units from file while reading with Verific
2023-07-31 16:11:16 +02:00
Miodrag Milanović a43e26e3e9
Merge pull request #3865 from dragonmux/fix/rtlil-teardown-segfault
Fix: RTLIL teardown segfault
2023-07-31 16:10:39 +02:00
Miodrag Milanovic 19d5293657 when blackboxing no need to know missing modules 2023-07-31 09:18:54 +02:00
dragonmux ef7e358576
kernel/rtlil: Trailing whitespace cleanup 2023-07-26 20:50:55 +01:00
dragonmux b59c717245
kernel/rtlil: Fixed the destruction guard for IdString
The guard is optimised out on some compilers under certain conditions (eg: LTO on GCC) as constant under C++ lifetime rules.
This is because the guard type's member is invalid to access (UB) after the type has been destroyed, resulting in
`destruct_guard.ok` being unable to be `false` according to the optimiser, based on the lifetime rules.

This patch still invokes UB (all accesses to the destroyed IdString instance are), but at least the optimiser
can't reason that destruct_guard_ok cannot be false and therefore it's safe to optimise out from its guard role.
2023-07-26 20:46:56 +01:00
Martin Povišer 3ec00cceaa cellaigs: Generate models for integer comparison cells
Add the case of $lt, $le, $gt, $ge to the code generating AIGs.
2023-07-25 11:45:18 +02:00
Miodrag Milanovic 372760af57 spaces to tabs 2023-07-25 09:40:30 +02:00
Miodrag Milanovic 3989181cd6 Add ability to blackbox modules/units from file while reading with verific 2023-07-25 09:40:30 +02:00
N. Engelhardt b04d0e09e8
Merge pull request #3830 from povik/cellaigs-header 2023-07-24 16:33:11 +02:00
N. Engelhardt 5e8db7000c
Merge pull request #3839 from povik/python-log-newline 2023-07-24 16:28:02 +02:00
N. Engelhardt 43780c9812
Merge pull request #3838 from povik/various-cleanup 2023-07-24 16:24:23 +02:00
N. Engelhardt 2bc0d86de7
Merge pull request #3854 from povik/abits-wide_log2-assert 2023-07-24 16:20:51 +02:00
github-actions[bot] c7670b36d4 Bump version 2023-07-24 00:17:45 +00:00
Catherine 6965abeefa abc, abc9_exe: fix build on WASI (and others with `const* stdout`).
C does not guarantee that stdout/stderr can be reassigned.
Most platforms do make them assignable, however musl and WASI that
is based on musl do not. WASI does not have `dup2()`; instead it has
its own non-portable version of it that can only assign to previously
allocated fds.

Update the stream redirection code so that it does the right thing
on WASI and other platforms.
2023-07-23 05:13:29 +01:00
Catherine 411b6e98cd abc, abc9_exe: respect `-q` when built with linked ABC.
This is mostly important for YoWASP builds, since those do not have
a way to build with external ABC (I prototyped it but for some reason
ABC always segfaults when built as an independent Wasm binary...)
2023-07-23 02:03:29 +01:00
github-actions[bot] c023b9485a Bump version 2023-07-22 00:17:24 +00:00
Zachary Snow d5d2bf815a Fix semantic merge conflict in previous two merged PRs 2023-07-21 00:08:10 -04:00
Martin Povišer 72a4022a10 ast/simplify: Retire 'at_zero' flag
Now that all the callsites pass in 'false' for the flag (or propagate
the flag on recursion), we can retire it.
2023-07-20 23:40:19 -04:00
Martin Povišer 4fceeb3b32 ast/simplify: Use clone_at_zero() for "at_zero" evaluations
The correct way of using the 'at_zero' regime of simplify is to perform
the simplification on a cloned AST subtree, otherwise the "at_zero"
evaluation seeps into the main tree.

Move the effect of the 'at_zero' flag to the cloning itself, so that
the simplify flag can be retired. We assume we can rely on id2ast in
the new clone method.
2023-07-20 23:40:19 -04:00
Martin Povišer 77d4b5230e ast: Move to a new helper method to print input errors
It's a repeating pattern to print an error message tied to an AST
node. Start using an 'input_error' helper for that. Among other
things this is beneficial in shortening the print lines, which tend
to be long.
2023-07-20 23:40:19 -04:00
Martin Povišer 1ac1b2eed5 ast/simplify: Factor out helper to determine range width 2023-07-20 23:40:19 -04:00
Dag Lem cff53d6d87 Corrected handling of nested typedefs of struct/union
This also corrects shadowing of constants in struct/union types.
2023-07-20 23:39:44 -04:00
github-actions[bot] 0b8f728590 Bump version 2023-07-21 00:17:07 +00:00
Martin Povišer f5485b59a9 sim: Bail if there are blackboxes in simulation 2023-07-20 21:01:03 +01:00
Martin Povišer 51ef942547 verilog_backend: Use hashlib dict for `auto_name_map`
This is most likely faster.
2023-07-20 21:00:33 +01:00
Martin Povišer 596743a6b6 verilog_backend: Make the keywords pool static
Do not recreate the keywords pool on every lookup of an identifier.
2023-07-20 21:00:33 +01:00
Martin Povišer f0ae046c5a opt_share: Fix input confusion with ANDNOT, ORNOT gates
Distinguish between the A, B input ports of `$_ANDNOT_`, `$_ORNOT_`
gates when considering those for sharing. Unlike the input ports of the
other supported single-bit gates, those are not interchangeable.

Fixes #3848.
2023-07-20 20:58:52 +01:00
Martin Povišer 6a553568c5 kernel/mem: Assert ABITS is not below wide_log2
Later in the check() code we check the bottom wide_log2 bits on the
address port are zeroed out. If the address port is too narrow, we crash
due to out of bounds access. Explicitly assert the address port is wide
enough, so we don't crash on input such as

    read_rtlil <<EOF
    module \top
      wire input 1 \clk

      memory width 8 size 2 \mem

      cell $memwr $auto$:1:$8
        parameter \PRIORITY 1'0
        parameter \CLK_POLARITY 1'1
        parameter \CLK_ENABLE 1'1
        parameter \MEMID "\\mem"
        parameter \ABITS 1'0
        parameter \WIDTH 6'010000
        connect \DATA 16'0000000000000000
        connect \ADDR { }
        connect \EN 16'0000000000000000
        connect \CLK \clk
      end
    end
    EOF
    memory
2023-07-19 16:50:59 +02:00