yosys.git
2 years agoMerge branch 'divfloor-in-write_smt2' into smtlib2-expr-support smtlib2-expr-support-old
Jacob Lifshay [Wed, 25 May 2022 01:01:52 +0000 (18:01 -0700)]
Merge branch 'divfloor-in-write_smt2' into smtlib2-expr-support

the smtlib2 support in nmigen needs $divfloor support in its tests:
https://gitlab.com/nmigen/nmigen/-/merge_requests/7

2 years agoadd $divfloor support to write_smt2 divfloor-in-write_smt2
Jacob Lifshay [Tue, 24 May 2022 08:34:25 +0000 (01:34 -0700)]
add $divfloor support to write_smt2

Fixes: #3330
2 years agoBump version
github-actions[bot] [Tue, 24 May 2022 00:18:18 +0000 (00:18 +0000)]
Bump version

2 years agoMerge pull request #3332 from YosysHQ/verific_f
Miodrag Milanović [Mon, 23 May 2022 18:01:44 +0000 (20:01 +0200)]
Merge pull request #3332 from YosysHQ/verific_f

Update Verific command file documentation

2 years agofix text to fit 80 columns
Miodrag Milanovic [Mon, 23 May 2022 17:57:21 +0000 (19:57 +0200)]
fix text to fit 80 columns

2 years agoUpdate verific command file documentation
Miodrag Milanovic [Mon, 23 May 2022 17:35:14 +0000 (19:35 +0200)]
Update verific command file documentation

2 years agoUse analysis mode if set in file
Miodrag Milanovic [Mon, 23 May 2022 17:13:45 +0000 (19:13 +0200)]
Use analysis mode if set in file

2 years agoMerge pull request #3331 from YosysHQ/git_rev_fix
Miodrag Milanović [Mon, 23 May 2022 16:33:11 +0000 (18:33 +0200)]
Merge pull request #3331 from YosysHQ/git_rev_fix

work around the new(ish) git safe.directory restrictions

2 years agoChange way to get commit sha
Jannis Harder [Mon, 23 May 2022 15:04:07 +0000 (17:04 +0200)]
Change way to get commit sha

2 years agoabc9_ops: Don't leave unused derived modules lying around
gatecat [Sun, 1 May 2022 08:24:17 +0000 (09:24 +0100)]
abc9_ops: Don't leave unused derived modules lying around

These later become accidentally used for techmap replacements for
blackboxes that we don't actually want.

Signed-off-by: gatecat <gatecat@ds0.me>
2 years agoBump version
github-actions[bot] [Sat, 21 May 2022 00:16:34 +0000 (00:16 +0000)]
Bump version

2 years agoMerge pull request #3324 from jix/confusing-select-errors
Jannis Harder [Fri, 20 May 2022 15:40:40 +0000 (17:40 +0200)]
Merge pull request #3324 from jix/confusing-select-errors

select: Fix -assert-none and -assert-any error output and docs

2 years agoactually test code that was broken
Jacob Lifshay [Fri, 20 May 2022 08:16:10 +0000 (01:16 -0700)]
actually test code that was broken

2 years agochange smtbmc to correctly handle output of $smtlib2_expr
Jacob Lifshay [Fri, 20 May 2022 08:08:41 +0000 (01:08 -0700)]
change smtbmc to correctly handle output of $smtlib2_expr

2 years agoselect: Fix -assert-none and -assert-any error output and docs
Jannis Harder [Thu, 19 May 2022 11:58:46 +0000 (13:58 +0200)]
select: Fix -assert-none and -assert-any error output and docs

Both of these options consider a selection containing only empty modules
as non-empty. This wasn't mentioned in the documentation nor did the
error message when using `select -assert-none` list those empty modules,
which produced a very confusing error message complaining about a
non-empty selection followed by an empty listing of the selection.

This fixes the documentation and changes the `-assert-none` and
`-assert-any` assertion error messages to also output fully selected
modules (this includes selected empty modules).

It doesn't change the messages for `-assert-count` etc. as they don't
count modules.

2 years agoBump version
github-actions[bot] [Thu, 19 May 2022 00:17:59 +0000 (00:17 +0000)]
Bump version

2 years agoAdd memory_bmux2rom pass.
Marcelina Kościelnicka [Wed, 18 May 2022 19:20:42 +0000 (21:20 +0200)]
Add memory_bmux2rom pass.

2 years agoAdd memory_libmap tests.
Marcelina Kościelnicka [Fri, 6 May 2022 14:30:56 +0000 (16:30 +0200)]
Add memory_libmap tests.

2 years agogatemate: Use `memory_libmap` pass.
Marcelina Kościelnicka [Sun, 6 Mar 2022 05:49:18 +0000 (06:49 +0100)]
gatemate: Use `memory_libmap` pass.

2 years agomachxo2: Use `memory_libmap` pass.
Marcelina Kościelnicka [Sun, 6 Mar 2022 02:43:13 +0000 (03:43 +0100)]
machxo2: Use `memory_libmap` pass.

2 years agoefinix: Use `memory_libmap` pass.
Marcelina Kościelnicka [Sun, 6 Mar 2022 01:21:53 +0000 (02:21 +0100)]
efinix: Use `memory_libmap` pass.

2 years agoanlogic: Use `memory_libmap` pass.
Marcelina Kościelnicka [Sun, 27 Feb 2022 08:57:10 +0000 (09:57 +0100)]
anlogic: Use `memory_libmap` pass.

2 years agoice40: Use `memory_libmap` pass.
Marcelina Kościelnicka [Sun, 27 Feb 2022 08:29:26 +0000 (09:29 +0100)]
ice40: Use `memory_libmap` pass.

2 years agoxilinx: Use `memory_libmap` pass.
Marcelina Kościelnicka [Sun, 6 Feb 2022 09:10:40 +0000 (10:10 +0100)]
xilinx: Use `memory_libmap` pass.

2 years agogowin: Use `memory_libmap` pass.
Marcelina Kościelnicka [Wed, 9 Feb 2022 08:25:45 +0000 (09:25 +0100)]
gowin: Use `memory_libmap` pass.

2 years agonexus: Use `memory_libmap` pass.
Marcelina Kościelnicka [Tue, 8 Feb 2022 02:52:50 +0000 (03:52 +0100)]
nexus: Use `memory_libmap` pass.

2 years agoecp5: Use `memory_libmap` pass.
Marcelina Kościelnicka [Tue, 8 Feb 2022 02:52:16 +0000 (03:52 +0100)]
ecp5: Use `memory_libmap` pass.

2 years agoAdd memory_libmap pass.
Marcelina Kościelnicka [Sun, 6 Feb 2022 09:10:21 +0000 (10:10 +0100)]
Add memory_libmap pass.

2 years agoproc_rom: Add special handling of const-0 address bits.
Marcelina Kościelnicka [Wed, 18 May 2022 06:18:13 +0000 (08:18 +0200)]
proc_rom: Add special handling of const-0 address bits.

2 years agoadd $smtlib2_expr
Jacob Lifshay [Wed, 18 May 2022 04:29:58 +0000 (21:29 -0700)]
add $smtlib2_expr

2 years agoBump version
github-actions[bot] [Wed, 18 May 2022 00:16:27 +0000 (00:16 +0000)]
Bump version

2 years agoMerge pull request #3310 from robinsonb5-PRs/master master
Miodrag Milanović [Tue, 17 May 2022 07:33:20 +0000 (09:33 +0200)]
Merge pull request #3310 from robinsonb5-PRs/master

Now calls Tcl_Init after creating the interp, fixes clock format.

2 years agoopt_ffinv: Use ModIndex instead of ModWalker.
Marcelina Kościelnicka [Mon, 16 May 2022 23:52:55 +0000 (01:52 +0200)]
opt_ffinv: Use ModIndex instead of ModWalker.

This avoids using out-of-data index information.

2 years agoUse log_warning when Tcl_Init fails, report error with Tcl_ErrnoMsg.
Alastair M. Robinson [Mon, 16 May 2022 19:22:28 +0000 (20:22 +0100)]
Use log_warning when Tcl_Init fails, report error with Tcl_ErrnoMsg.

2 years agoMerge pull request #3314 from jix/sva_value_change_logic_wide
Jannis Harder [Mon, 16 May 2022 14:15:04 +0000 (16:15 +0200)]
Merge pull request #3314 from jix/sva_value_change_logic_wide

verific: Use new value change logic also for $stable of wide signals.

2 years agoBump version
github-actions[bot] [Sat, 14 May 2022 00:19:50 +0000 (00:19 +0000)]
Bump version

2 years agoAdd opt_ffinv pass.
Marcelina Kościelnicka [Fri, 13 May 2022 14:59:52 +0000 (16:59 +0200)]
Add opt_ffinv pass.

2 years agoBump version
github-actions[bot] [Fri, 13 May 2022 00:19:56 +0000 (00:19 +0000)]
Bump version

2 years agoAdd proc_rom pass.
Marcelina Kościelnicka [Thu, 12 May 2022 21:36:28 +0000 (23:36 +0200)]
Add proc_rom pass.

2 years agoverific: Use new value change logic also for $stable of wide signals.
Jannis Harder [Wed, 11 May 2022 10:55:53 +0000 (12:55 +0200)]
verific: Use new value change logic also for $stable of wide signals.

I missed this in the previous PR.

2 years agoNow calls Tcl_Init after creating the interp, fixes clock format.
Alastair M. Robinson [Tue, 10 May 2022 17:48:54 +0000 (18:48 +0100)]
Now calls Tcl_Init after creating the interp, fixes clock format.

2 years agoBump version
github-actions[bot] [Tue, 10 May 2022 00:16:26 +0000 (00:16 +0000)]
Bump version

2 years agoMerge pull request #3305 from jix/sva_value_change_logic
Jannis Harder [Mon, 9 May 2022 14:40:34 +0000 (16:40 +0200)]
Merge pull request #3305 from jix/sva_value_change_logic

verific: Improve logic generated for SVA value change expressions

2 years agoMerge pull request #3297 from jix/sva_nested_clk_else
Jannis Harder [Mon, 9 May 2022 14:07:39 +0000 (16:07 +0200)]
Merge pull request #3297 from jix/sva_nested_clk_else

verific: Fix conditions of SVAs with explicit clocks within procedures

2 years agoverific: Improve logic generated for SVA value change expressions
Jannis Harder [Mon, 9 May 2022 13:04:01 +0000 (15:04 +0200)]
verific: Improve logic generated for SVA value change expressions

The previously generated logic assumed an unconstrained past value in
the initial state and did not handle 'x values. While the current formal
verification flow uses 2-valued logic, SVA value change expressions
require a past value of 'x during the initial state to behave in the
expected way (i.e. to consider both an initial 0 and an initial 1 as
$changed and an initial 1 as $rose and an initial 0 as $fell).

This patch now generates logic that at the same time

a) provides the expected behavior in a 2-valued logic setting, not
   depending on any dont-care optimizations, and

b) properly handles 'x values in yosys simulation

2 years agoNext dev cycle
Miodrag Milanovic [Mon, 9 May 2022 08:12:32 +0000 (10:12 +0200)]
Next dev cycle

2 years agoRelease version 0.17 yosys-0.17
Miodrag Milanovic [Mon, 9 May 2022 08:11:04 +0000 (10:11 +0200)]
Release version 0.17

2 years agoUpdate CHANGELOG
Miodrag Milanovic [Mon, 9 May 2022 08:06:15 +0000 (10:06 +0200)]
Update CHANGELOG

2 years agoUpdate manual
Miodrag Milanovic [Mon, 9 May 2022 07:53:01 +0000 (09:53 +0200)]
Update manual

2 years agoMerge pull request #3299 from YosysHQ/mmicko/sim_memory
Miodrag Milanović [Mon, 9 May 2022 07:28:09 +0000 (09:28 +0200)]
Merge pull request #3299 from YosysHQ/mmicko/sim_memory

sim pass: support for memories

2 years agoFix running sva tests
Miodrag Milanovic [Mon, 9 May 2022 07:01:57 +0000 (09:01 +0200)]
Fix running sva tests

2 years agoBump version
github-actions[bot] [Sun, 8 May 2022 00:16:45 +0000 (00:16 +0000)]
Bump version

2 years agoopt_mem: Remove constant-value bit lanes.
Marcelina Kościelnicka [Fri, 6 May 2022 21:29:16 +0000 (23:29 +0200)]
opt_mem: Remove constant-value bit lanes.

2 years agoBump version
github-actions[bot] [Sat, 7 May 2022 00:15:38 +0000 (00:15 +0000)]
Bump version

2 years agoinclude latest abc changes
Miodrag Milanovic [Fri, 6 May 2022 13:52:24 +0000 (15:52 +0200)]
include latest abc changes

2 years agoinclude latest abc changes
Miodrag Milanovic [Fri, 6 May 2022 13:42:39 +0000 (15:42 +0200)]
include latest abc changes

2 years agoMerge pull request #3300 from imhcyx/master
Miodrag Milanović [Fri, 6 May 2022 07:17:59 +0000 (09:17 +0200)]
Merge pull request #3300 from imhcyx/master

memory_share: fix wrong argidx in extra_args

2 years agoInclude abc change to fix FreeBSD build
Miodrag Milanovic [Fri, 6 May 2022 06:08:06 +0000 (08:08 +0200)]
Include abc change to fix FreeBSD build

2 years agoHandle possible non-memory indexed data
Miodrag Milanovic [Fri, 6 May 2022 06:05:23 +0000 (08:05 +0200)]
Handle possible non-memory indexed data

2 years agomemory_share: fix wrong argidx in extra_args
imhcyx [Thu, 5 May 2022 08:58:39 +0000 (16:58 +0800)]
memory_share: fix wrong argidx in extra_args

2 years agoBump version
github-actions[bot] [Thu, 5 May 2022 00:15:34 +0000 (00:15 +0000)]
Bump version

2 years agoabc: Use dict/pool instead of std::map/std::set
Marcelina Kościelnicka [Wed, 4 May 2022 18:43:59 +0000 (20:43 +0200)]
abc: Use dict/pool instead of std::map/std::set

2 years agomap memory location to wire value, if memory is converted to FFs
Miodrag Milanovic [Wed, 4 May 2022 11:08:16 +0000 (13:08 +0200)]
map memory location to wire value, if memory is converted to FFs

2 years agofix crash when no fst input
Miodrag Milanovic [Wed, 4 May 2022 09:21:39 +0000 (11:21 +0200)]
fix crash when no fst input

2 years agoStart restoring memory state from VCD/FST
Miodrag Milanovic [Wed, 4 May 2022 08:41:04 +0000 (10:41 +0200)]
Start restoring memory state from VCD/FST

2 years agoAdd propagated clock signals into btor info file
Claire Xenia Wolf [Wed, 4 May 2022 06:10:18 +0000 (08:10 +0200)]
Add propagated clock signals into btor info file

2 years agoverific: Fix conditions of SVAs with explicit clocks within procedures
Jannis Harder [Tue, 3 May 2022 11:22:18 +0000 (13:22 +0200)]
verific: Fix conditions of SVAs with explicit clocks within procedures

For SVAs that have an explicit clock and are contained in a procedure
which conditionally executes the assertion, verific expresses this using
a mux with one input connected to constant 1 and the other output
connected to an SVA_AT. The existing code only handled the case where
the first input is connected to 1. This patch also handles the other
case.

2 years agoBump version
github-actions[bot] [Tue, 3 May 2022 00:16:24 +0000 (00:16 +0000)]
Bump version

2 years agoAIM file could have gaps in or between inputs and inits
Miodrag Milanovic [Mon, 2 May 2022 09:18:30 +0000 (11:18 +0200)]
AIM file could have gaps in or between inputs and inits

2 years agoBump version
github-actions[bot] [Sat, 30 Apr 2022 00:18:55 +0000 (00:18 +0000)]
Bump version

2 years agoMerge pull request #3294 from YosysHQ/micko/verific_merge_past_ff
Miodrag Milanović [Fri, 29 Apr 2022 12:35:46 +0000 (14:35 +0200)]
Merge pull request #3294 from YosysHQ/micko/verific_merge_past_ff

Ignore merging past ffs that we are not properly merging

2 years agoIgnore merging past ffs that we are not properly merging
Miodrag Milanovic [Fri, 29 Apr 2022 12:35:02 +0000 (14:35 +0200)]
Ignore merging past ffs that we are not properly merging

2 years agoBump version
github-actions[bot] [Tue, 26 Apr 2022 00:18:47 +0000 (00:18 +0000)]
Bump version

2 years agoAdd missing parameters for ecp5
Rick Luiken [Fri, 8 Apr 2022 12:41:48 +0000 (14:41 +0200)]
Add missing parameters for ecp5

2 years agoMerge pull request #3287 from jix/smt2-conditional-store
Jannis Harder [Mon, 25 Apr 2022 14:23:21 +0000 (16:23 +0200)]
Merge pull request #3287 from jix/smt2-conditional-store

smt2: Make write port array stores conditional on nonzero write mask

2 years agoMerge pull request #3257 from jix/tribuf-formal
Jannis Harder [Mon, 25 Apr 2022 14:23:06 +0000 (16:23 +0200)]
Merge pull request #3257 from jix/tribuf-formal

tribuf: `-formal` option: convert all to logic and detect conflicts

2 years agoMerge pull request #3290 from mpasternacki/bugfix/freebsd-build
Miodrag Milanović [Mon, 25 Apr 2022 08:16:50 +0000 (10:16 +0200)]
Merge pull request #3290 from mpasternacki/bugfix/freebsd-build

Fix build on FreeBSD, which has no alloca.h

2 years agoMerge pull request #3289 from YosysHQ/micko/sim_improve
Miodrag Milanović [Mon, 25 Apr 2022 08:16:25 +0000 (10:16 +0200)]
Merge pull request #3289 from YosysHQ/micko/sim_improve

Simulation improvements

2 years agoFix build on FreeBSD, which has no alloca.h
Maciej Pasternacki [Sun, 24 Apr 2022 17:35:50 +0000 (19:35 +0200)]
Fix build on FreeBSD, which has no alloca.h

2 years agoMatch $anyseq input if connected to public wire
Miodrag Milanovic [Fri, 22 Apr 2022 15:20:17 +0000 (17:20 +0200)]
Match $anyseq input if connected to public wire

2 years agoTreat $anyseq as input from FST
Miodrag Milanovic [Fri, 22 Apr 2022 14:23:39 +0000 (16:23 +0200)]
Treat $anyseq as input from FST

2 years agoIgnore change on last edge
Miodrag Milanovic [Fri, 22 Apr 2022 13:24:02 +0000 (15:24 +0200)]
Ignore change on last edge

2 years agoLast sample from input does not represent change
Miodrag Milanovic [Fri, 22 Apr 2022 11:46:11 +0000 (13:46 +0200)]
Last sample from input does not represent change

2 years agolatches are always set to zero
Miodrag Milanovic [Fri, 22 Apr 2022 10:04:05 +0000 (12:04 +0200)]
latches are always set to zero

2 years agoIf not multiclock, output only on clock edges
Miodrag Milanovic [Fri, 22 Apr 2022 10:03:39 +0000 (12:03 +0200)]
If not multiclock, output only on clock edges

2 years agoSet init state for all wires from FST and set past
Miodrag Milanovic [Fri, 22 Apr 2022 09:57:39 +0000 (11:57 +0200)]
Set init state for all wires from FST and set past

2 years agoFix multiclock for btor2 witness
Miodrag Milanovic [Fri, 22 Apr 2022 09:53:41 +0000 (11:53 +0200)]
Fix multiclock for btor2 witness

2 years agosmt2: Make write port array stores conditional on nonzero write mask
Jannis Harder [Wed, 20 Apr 2022 15:49:48 +0000 (17:49 +0200)]
smt2: Make write port array stores conditional on nonzero write mask

2 years agoBump version
github-actions[bot] [Tue, 19 Apr 2022 00:14:02 +0000 (00:14 +0000)]
Bump version

2 years agoMerge pull request #3280 from YosysHQ/micko/fix_readaiw
Miodrag Milanović [Mon, 18 Apr 2022 07:49:21 +0000 (09:49 +0200)]
Merge pull request #3280 from YosysHQ/micko/fix_readaiw

Fix reading aiw from other solvers

2 years agoUpdate abc
Miodrag Milanovic [Mon, 18 Apr 2022 07:27:00 +0000 (09:27 +0200)]
Update abc

2 years agoverific: allow memories to be inferred in loops (vhdl)
Miodrag Milanovic [Mon, 18 Apr 2022 07:10:28 +0000 (09:10 +0200)]
verific: allow memories to be inferred in loops (vhdl)

2 years agoMerge pull request #3282 from nakengelhardt/verific_loop_rams
Miodrag Milanović [Mon, 18 Apr 2022 07:09:36 +0000 (09:09 +0200)]
Merge pull request #3282 from nakengelhardt/verific_loop_rams

verific: allow memories to be inferred in loops

2 years agoBump version
github-actions[bot] [Sat, 16 Apr 2022 00:14:57 +0000 (00:14 +0000)]
Bump version

2 years agomemory_share: Fix up mismatched address widths.
Marcelina Kościelnicka [Fri, 15 Apr 2022 13:05:08 +0000 (15:05 +0200)]
memory_share: Fix up mismatched address widths.

2 years agoopt_dff: Fix behavior on $ff with D == Q.
Marcelina Kościelnicka [Thu, 14 Apr 2022 13:08:20 +0000 (15:08 +0200)]
opt_dff: Fix behavior on $ff with D == Q.

2 years agoverific: allow memories to be inferred in loops
N. Engelhardt [Fri, 15 Apr 2022 13:10:48 +0000 (15:10 +0200)]
verific: allow memories to be inferred in loops

2 years agoFix reading aiw from other solvers
Miodrag Milanovic [Fri, 15 Apr 2022 09:45:16 +0000 (11:45 +0200)]
Fix reading aiw from other solvers

2 years agotribuf: `-formal` option: convert all to logic and detect conflicts
Jannis Harder [Tue, 29 Mar 2022 10:11:28 +0000 (12:11 +0200)]
tribuf: `-formal` option: convert all to logic and detect conflicts

2 years agoBump version
github-actions[bot] [Sat, 9 Apr 2022 00:15:22 +0000 (00:15 +0000)]
Bump version