Jannis Harder
fb1c2be76b
verilog: Support void functions
...
The difference between void functions and tasks is that always_comb's
implicit sensitivity list behaves as if functions were inlined, but
ignores signals read only in tasks. This only matters for event based
simulation, and for synthesis we can treat a void function like a task.
2023-03-20 12:52:46 +01:00
Miodrag Milanovic
61da330a38
Update tests
2023-03-20 09:58:41 +01:00
Jannis Harder
390d1c583a
verific: Fix enum_values support and signed attribute values
...
This uses the same constant parsing for enum_values and for attributes
and extends it to handle signed values as those are used for enums that
implicitly use the int type.
2023-03-15 09:51:36 +01:00
Jannis Harder
c50f641812
Merge pull request #3682 from daglem/struct-member-out-of-bounds
...
Out of bounds checking for struct/union members
2023-03-10 16:14:56 +01:00
Dag Lem
1af7d6121f
Added test for dynamic indexing within struct members
2023-03-08 20:25:39 +01:00
Dag Lem
0d3423ddea
Index struct/union members within corresponding wire chunks
...
This guards against access to bits outside of struct/union
members via dynamic indexing.
2023-03-05 14:54:17 +01:00
Miodrag Milanović
21e87f7986
Merge pull request #3646 from YosysHQ/lofty/fix-3591
...
muxcover: do not add decode muxes with x inputs
2023-02-27 16:26:57 +01:00
N. Engelhardt
842cdad575
Merge pull request #3674 from YosysHQ/fix_wide_case
2023-02-27 16:04:11 +01:00
gatecat
2ab3747cc9
fabulous: Add support for mapping carry chains
...
Signed-off-by: gatecat <gatecat@ds0.me>
2023-02-27 09:50:34 +01:00
Miodrag Milanovic
d8cefec169
Added ranged case check
2023-02-27 09:24:04 +01:00
Miodrag Milanovic
53a4f0fb56
Add test example
2023-02-27 09:24:04 +01:00
KrystalDelusion
f80920bd9f
Genericising bug1836.ys
2023-02-21 05:23:16 +13:00
KrystalDelusion
445a801a85
bug3205.ys removed
...
Made redundant by TDP test(s) in memories.ys
2023-02-21 05:23:16 +13:00
KrystalDelusion
51c2d476c2
Removing extra `default_nettype` lines
2023-02-21 05:23:16 +13:00
KrystalDelusion
8f6a06951c
Fix for sync_ram_sdp not being final module
...
Explicitly declare -top in synth_intel_alm.
2023-02-21 05:23:16 +13:00
KrystalDelusion
7f033d3c1f
More tests in memlib/generate.py
...
Covers most of the todo list, at least functionally. Some minor issues with not always using hardware features.
2023-02-21 05:23:15 +13:00
KrystalDelusion
af1b9c9e07
Tests for ram_style = "huge"
...
iCE40 SPRAM and Xilinx URAM
2023-02-21 05:23:15 +13:00
KrystalDelusion
de2f140c09
Testing TDP synth mapping
...
New common sync_ram_tdp.
Used in ecp5 and gatemate mem*.ys.
2023-02-21 05:23:15 +13:00
KrystalDelusion
48f4e09202
Asymmetric port ram tests with Xilinx
...
Uses verilog code from User Guide 901 (2021.1)
2023-02-21 05:23:14 +13:00
KrystalDelusion
ac5fa9a838
Addings tests for #1836 and #3205
2023-02-21 05:23:14 +13:00
Dag Lem
79043cb849
Out of bounds checking for struct/union members
...
Currently, only constant indices are checked.
2023-02-19 23:25:08 +01:00
Jannis Harder
1cedad7a68
Merge pull request #3675 from daglem/struct-item-queries
...
Support for data and array queries on struct/union item expressions
2023-02-15 13:33:34 +01:00
Jannis Harder
68480dfa19
Merge pull request #3671 from zachjs/master
...
Add test for typenames using constants shadowed later on
2023-02-15 13:04:43 +01:00
Dag Lem
f8219289b2
Corrected tests for data and array queries on struct/union item expressions
2023-02-15 12:36:29 +01:00
Dag Lem
c1e12877f0
Support for data and array queries on struct/union item expressions
...
For now, $bits, $left, $right, $low, $high, and $size are supported.
2023-02-15 11:44:24 +01:00
Jannis Harder
53bda9de54
Merge pull request #3661 from daglem/struct-array-range-offset
...
Handle range offsets in packed arrays within packed structs
2023-02-15 11:21:56 +01:00
Jannis Harder
ec94703619
Merge pull request #2995 from georgerennie/cover_precond
...
chformal: Add -coverenable option
2023-02-14 17:46:31 +01:00
Jannis Harder
85f611fb23
Merge pull request #3126 from georgerennie/equiv_make_assertions
...
equiv_make: Add -make_assert option
2023-02-14 17:15:55 +01:00
Jannis Harder
d2032ac6fd
Merge pull request #3669 from jix/fix-xprop-tests-yosys-call
...
tests: Fix path of yosys invocation in xprop tests
2023-02-13 17:55:36 +01:00
Jannis Harder
55ad3fe6c7
xprop tests: Make iverilog invocation more portable
2023-02-13 16:54:11 +01:00
Jannis Harder
2a68eee5f1
xprop: Test fixes and abort on test failure
...
Use `$finish(0)` to silently exit even when using recent iverlog
versions. Run `write_verilog -noexpr` before `write_verilog` as the
latter can modify the design.
This also enables checking the tests results, as xprop should be in a
state where the existing tests pass.
2023-02-13 14:05:16 +01:00
Jannis Harder
9f20beb7df
xprop: Smaller subset of tests to run by default
2023-02-13 14:02:02 +01:00
Dag Lem
615adc4253
Resolve package types in interfaces ( #3658 )
...
* Resolve package types in interfaces
* Added test for resolving of package types in interfaces
2023-02-12 18:25:39 -05:00
Zachary Snow
26a6c60478
Add test for typenames using constants shadowed later on
...
This possible edge case came up while reviewing #3555 . It is currently
handled correctly, but there is no clear test coverage.
2023-02-12 17:03:37 -05:00
Jannis Harder
6d021f04d4
tests: Fix path of yosys invocation in xprop tests
...
For now xprop test failures are still expected and ignored, but without
this change, they did not even run unless the yosys build was in path.
2023-02-10 19:17:16 +01:00
Jannis Harder
d31d5da69f
tests: in xprop tests, use MAKE variable if set
2023-02-10 15:01:04 +01:00
Dag Lem
777c589e85
Handle range offsets in packed arrays within packed structs
...
This brings the metadata for packed arrays in packed structs
in line with the metadata for unpacked arrays, and correctly
handles the case when both lsb and msb in an address range are
non-zero.
2023-02-05 17:09:51 +01:00
Jannis Harder
c235802f4a
Merge pull request #3650 from jix/rtlil_roundtrip_z_bits
...
backends/rtlil: Do not shorten a value with z bits to 'x
2023-01-30 16:14:24 +01:00
N. Engelhardt
ecfa7e9fbc
add pmux option to bmuxmap for better fsm detection with verific frontend
2023-01-30 16:12:53 +01:00
Dag Lem
26db5a11d3
Resolve struct member package types
2023-01-29 13:51:44 -05:00
Dag Lem
db13c6df2b
Handle struct members of union type ( #3641 )
2023-01-29 13:45:45 -05:00
Jannis Harder
b08a880704
backends/rtlil: Do not shorten a value with z bits to 'x
2023-01-29 14:02:25 +01:00
Lofty
822c7b0341
muxcover: do not add decode muxes with x inputs
2023-01-26 05:19:45 +00:00
Jannis Harder
5abaa59080
Merge pull request #3537 from jix/xprop
...
New xprop pass
2023-01-11 16:26:04 +01:00
Jannis Harder
3ebc50dee4
Merge pull request #3467 from jix/fix_cellarray_simplify
...
simplify: Do not recursively simplify AST_CELL within AST_CELLARRAY
2022-12-19 16:05:13 +01:00
Jannis Harder
cf3570abde
simplify: regression test for AST_CELLARRAY simplification issue
2022-12-07 18:41:55 +01:00
Dag Lem
f94eec952f
Support for packed multidimensional arrays within packed structs
2022-12-03 19:54:47 +01:00
Jannis Harder
4a2b7287ca
Merge pull request #3551 from daglem/struct-array-swapped-range
...
Support for arrays with swapped ranges within structs
2022-12-01 00:58:32 +01:00
Jannis Harder
ce708122a5
New xprop pass to encode 3-valued x-propagation using 2-valued logic
2022-11-30 19:01:28 +01:00
Jannis Harder
661fa5ff92
simplemap: Map `$xnor` to `$_XNOR_` cells
...
The previous mapping to `$_XOR_` and `$_NOT_` predates the addition of
the `$_XNOR_` cell.
2022-11-29 19:06:45 +01:00
Dag Lem
a460e0b31c
Tests for unpacked arrays in packed structs are for the Yosys frontend only
2022-11-23 16:37:51 +01:00
Dag Lem
ddb12148e7
Support for swapped ranges in second array dimension
2022-11-23 16:31:08 +01:00
Jannis Harder
239ecf9185
Merge branch 'zachjs-master'
2022-11-21 17:47:43 +01:00
gatecat
b6467f0801
fabulous: Allow adding extra custom prims and map rules
...
Signed-off-by: gatecat <gatecat@ds0.me>
2022-11-17 13:34:58 +01:00
gatecat
f111bbdf40
fabulous: improvements to the pass
...
Signed-off-by: gatecat <gatecat@ds0.me>
2022-11-17 13:34:58 +01:00
Dag Lem
bab88630c2
Support for arrays with swapped ranges within structs
...
This also corrects the implementation of C type arrays within structs.
Fixes #3550
2022-11-12 08:48:25 +01:00
Zachary Snow
71e7e09092
verilog: Support module-scoped task/function calls
...
This is primarily intended to enable the standard-permitted use of
module-scoped identifiers to refer to tasks and non-constant functions.
As a side-effect, this also adds support for the non-standard use of
module-scoped identifiers referring to constant functions, a feature
that is supported in some other tools, including Iverilog.
2022-10-29 15:14:11 -04:00
Lloyd Parkes
49945ab1c2
Replace GNU specific invocation of basename(1) with the equivalent
...
POSIX one. The tests now complete on BSD as well as GNU/Linux.
2022-10-23 11:02:18 +13:00
Jannis Harder
4d334fd3e3
smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFs
...
The witness metadata was missing fine grained FFs completely and for
coarse grained FFs where the output connection has multiple chunks it
lacked the offset of the chunk within the SMT expression. This fixes
both, the later by adding an "smtoffset" field to the metadata.
2022-10-12 19:48:36 +02:00
Jannis Harder
fcf742837e
Merge pull request #3502 from jix/equiv_opt_fixes
...
equiv_opt and clk2fflogic fixes
2022-10-11 12:02:16 +02:00
Miodrag Milanović
e8ce9442a6
Merge pull request #3452 from ALGCDG/master
...
Add BLIF names command input plane size check
2022-10-10 16:29:27 +02:00
Jannis Harder
0113f44faa
Reenable existing equiv_opt tests
2022-10-07 16:04:51 +02:00
Jannis Harder
81906aa627
Fix tests for check in equiv_opt
2022-10-07 16:04:51 +02:00
Claire Xenia Wolf
f0478c520d
Re-enable opt_dff_sr equiv_opt checks
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-10-07 16:04:51 +02:00
Miodrag Milanovic
1ecf6aee9b
Test fixes for latest iverilog
2022-09-21 15:46:43 +02:00
Miodrag Milanovic
5b5fe76966
Add test for bug 3462
2022-08-29 10:10:09 +02:00
Archie
15a0697c70
Adding check for BLIF names command input plane size.
2022-08-21 23:18:20 -05:00
Jannis Harder
5142fb3b5c
write_aiger: Fix non-$_FF_ FFs
...
This broke while switching sby's formal flows to always use $_FF_'s.
2022-08-18 13:56:22 +02:00
Jannis Harder
f041e36c6e
smtbmc: Add native json based witness format + smt2 backend support
...
This adds a native json based witness trace format. By having a common
format that includes everything we support, and providing a conversion
utility (yosys-witness) we no longer need to implement every format for
every tool that deals with witness traces, avoiding a quadratic
opportunity to introduce subtle bugs.
Included:
* smt2: New yosys-smt2-witness info lines containing full hierarchical
paths without lossy escaping.
* yosys-smtbmc --dump-yw trace.yw: Dump results in the new format.
* yosys-smtbmc --yw trace.yw: Read new format as constraints.
* yosys-witness: New tool to convert witness formats.
Currently this can only display traces in a human-readable-only
format and do a passthrough read/write of the new format.
* ywio.py: Small python lib for reading and writing the new format.
Used by yosys-smtbmc and yosys-witness to avoid duplication.
2022-08-16 13:37:30 +02:00
N. Engelhardt
63fca0dbc2
Merge pull request #3277 from YosysHQ/lofty/rename-scramble_name
2022-08-11 12:06:04 +02:00
Miodrag Milanovic
f4a1906721
support file locations containing spaces
2022-08-08 20:30:50 +02:00
Lofty
a48dcd1d40
rename: add -scramble-name option to randomly rename selections
2022-08-08 16:03:28 +01:00
gatecat
48efc9b75c
gatemate: Add test for LUT tree mapping
...
Signed-off-by: gatecat <gatecat@ds0.me>
2022-06-27 10:09:48 +01:00
George Rennie
fbf5d89587
equiv_make: Add -make_assert option
...
This adds a -make_assert flag to equiv_make. When used, the pass generates
$eqx and $assert cells to encode equivalence instead of $equiv.
2022-06-24 00:17:02 +01:00
Archie
f69c2c802c
Adding expected error message.
2022-06-22 00:34:49 +01:00
Archie
c8cd4f468a
Adding testcase for issue 3374
2022-06-22 00:34:49 +01:00
George Rennie
5dfad5101d
chformal: Rename -coverprecond to -coverenable
2022-06-18 18:28:12 +01:00
Jannis Harder
e39c422734
chformal: Test -coverprecond and reuse the src attribute
2022-06-18 18:19:26 +01:00
Jannis Harder
ac22f1764d
smt2: emit smtlib2_comb_expr outputs after all inputs
2022-06-07 19:06:45 +02:00
Jacob Lifshay
0b0123e003
don't use sed -i because it won't work on macos
2022-06-03 01:09:57 -07:00
Jacob Lifshay
b7c19b1c88
smtlib2_module: try to fix test on macos
2022-06-02 23:12:07 -07:00
Jacob Lifshay
cd57c5adb3
smt2: Add smtlib2_comb_expr attribute to allow user-selected smtlib2 expressions
2022-06-02 22:37:29 -07:00
Zachary Snow
a650d9079f
verilog: fix width/sign detection for functions
2022-05-30 16:45:39 -04:00
Jannis Harder
4bfaaea0d5
verilog: fix size and signedness of array querying functions
...
genrtlil.cc and simplify.cc had inconsistent and slightly broken
handling of signedness for array querying functions. These functions are
defined to return a signed result. Simplify always produced an unsigned
and genrtlil always a signed 32-bit result ignoring the context.
Includes tests for the the relvant edge cases for context dependent
conversions.
2022-05-30 09:11:31 -04:00
Jannis Harder
b75fa62e9b
verilog: fix $past's signedness
2022-05-25 16:32:08 -04:00
Jannis Harder
cffec1f95f
verilog: fix signedness when removing unreachable cases
2022-05-24 23:03:31 -04:00
Marcelina Kościelnicka
606f1637ae
Add memory_bmux2rom pass.
2022-05-18 22:48:55 +02:00
Marcelina Kościelnicka
982a11c709
Add memory_libmap tests.
2022-05-18 17:32:56 +02:00
Marcelina Kościelnicka
9d11575856
efinix: Use `memory_libmap` pass.
2022-05-18 17:32:56 +02:00
Marcelina Kościelnicka
d7dc2313b9
ice40: Use `memory_libmap` pass.
2022-05-18 17:32:56 +02:00
Marcelina Kościelnicka
3b2f95953c
xilinx: Use `memory_libmap` pass.
2022-05-18 17:32:56 +02:00
Marcelina Kościelnicka
0a8eaca322
nexus: Use `memory_libmap` pass.
2022-05-18 17:32:56 +02:00
Marcelina Kościelnicka
a04b025abf
ecp5: Use `memory_libmap` pass.
2022-05-18 17:32:56 +02:00
Marcelina Kościelnicka
9450f308f0
proc_rom: Add special handling of const-0 address bits.
2022-05-18 17:32:30 +02:00
Jannis Harder
2864f2826a
Merge pull request #3314 from jix/sva_value_change_logic_wide
...
verific: Use new value change logic also for $stable of wide signals.
2022-05-16 16:15:04 +02:00
Marcelina Kościelnicka
990c9b8e11
Add proc_rom pass.
2022-05-13 00:37:14 +02:00
Jannis Harder
fada77b8cf
verific: Use new value change logic also for $stable of wide signals.
...
I missed this in the previous PR.
2022-05-11 13:05:27 +02:00
Jannis Harder
587e09d551
Merge pull request #3305 from jix/sva_value_change_logic
...
verific: Improve logic generated for SVA value change expressions
2022-05-09 16:40:34 +02:00
Jannis Harder
5ca2ee0c31
Merge pull request #3297 from jix/sva_nested_clk_else
...
verific: Fix conditions of SVAs with explicit clocks within procedures
2022-05-09 16:07:39 +02:00
Jannis Harder
a855d62b42
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
2022-05-09 15:04:01 +02:00