riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
13,470 Commits 81 Branches 48 Tags 63 MiB
Commit Graph

1780 Commits

Author SHA1 Message Date
Lofty b8b47f7c6c
Revert "ice40, ecp5: enable ABC9 by default" 2023-11-03 14:52:52 +00:00
Lofty 32082477b5 ice40, ecp5: enable ABC9 by default 2023-11-03 08:52:54 +00:00
N. Engelhardt 833b67af80 verific: import attributes on ports 
Co-authored-by: Miodrag Milanović <mmicko@gmail.com>
 2023-10-20 18:31:41 +02:00
N. Engelhardt 1b6d1e9419 memory_libmap: look for ram_style attributes on surrounding signals 2023-10-19 19:23:35 +02:00
Martin Povišer 62d6338688 quicklogic: Fix pp3 `dffs` test 
Fix name confusion which was making the test look into the vendor's cell
blackbox rather than into the synthesis results.
 2023-10-12 12:45:40 +02:00
Martin Povišer 4506e11d0f booth: Extend test to catch bug from previous commit 2023-10-04 23:30:29 +02:00
Jannis Harder c174597014 Fix sva_value_change_changed test for updated verific 2023-10-03 11:46:43 +02:00
Martin Povišer b0045300fd booth: Cut down the test 
Cut the test down from taking ~25 s to ~3 s.
 2023-09-28 11:55:51 +02:00
Martin Povišer c4762d930e
Merge pull request #3930 from povik/verific-test-memsemantics 
verific: Add test of accurate semantics in memory inference
 2023-09-20 11:46:42 +02:00
Martin Povišer 99a5773911
Merge pull request #3920 from zachjs/asgn-expr 
sv: support assignments within expressions
 2023-09-20 11:30:14 +02:00
Zachary Snow 28e99f2b8c fix width of post-increment/decrement expressions 2023-09-18 23:46:06 -04:00
Zachary Snow 7d07615dee allow attributes in front of ++/-- statements 2023-09-18 23:46:02 -04:00
Martin Povišer 8222121164 verific: Add test of accurate semantics in memory inference 2023-09-18 16:37:15 +02:00
andyfox-rushc 6d29dc659b renamed passname to booth, replaced connect_sigSpecToWire with connect, updated test script 2023-09-08 15:34:56 -07:00
Martin Povišer 25a33d4082 techmap: Make the Booth test deterministic 2023-09-07 14:56:56 +02:00
Martin Povišer 0c2a99ca47 techmap: Test the Booth multiplier 2023-09-07 14:46:59 +02:00
Zachary Snow 4edb1a1921 sv: support assignments within expressions 
- Add support for assignments within expressions, e.g., `x[y++] = z;` or
  `x = (y *= 2) - 1;`. The logic is handled entirely within the parser
  by injecting statements into the current procedural block.
- Add support for pre-increment/decrement statements, which are
  behaviorally equivalent to post-increment/decrement statements.
- Fix non-standard attribute position used for post-increment/decrement
  statements.
 2023-09-05 22:27:55 -04:00
Miodrag Milanovic a42c630264 put back previous test state, due to default change 2023-08-29 10:21:58 +02:00
Miodrag Milanovic 3b9ebfa672 Addressed code review comments 2023-08-25 11:10:20 +02:00
Miodrag Milanovic ea50d96135 fixed tests 2023-08-23 10:54:29 +02:00
Asherah Connor 4a475fa7a2 cxxrtl: include iostream when prints are used 2023-08-17 07:08:22 +02:00
Charlotte d130f7fca2 tests: use /usr/bin/env for bash. 2023-08-12 11:59:39 +10:00
Charlotte 860e3e4056 proc_clean: only consider fully-defined switch operands too. 2023-08-12 02:46:31 +02:00
Charlotte bf84861fc2 proc_clean: only consider fully-defined case operands. 2023-08-12 02:46:31 +02:00
Charlotte ce245b5105 cxxrtl_backend: respect sync `$print` priority 
We add a new flow graph node type, PRINT_SYNC, as they don't get handled
with regular CELL_EVALs.  We could probably move this grouping out of
the dump method.
 2023-08-11 04:46:52 +02:00
Charlotte 04582f2fb7 verilog_backend: emit sync `$print` cells with same triggers together 
Sort by PRIORITY, ensuring output order.
 2023-08-11 04:46:52 +02:00
Charlotte 4ffdee65e0 cxxrtl: store comb $print cell last EN/ARGS in module 
statics were obviously wrong -- may be multiple instantiations of any
given module.  Extend test to cover this.
 2023-08-11 04:46:52 +02:00
Charlotte 843ad9331b cxxrtl: WIP: adjust comb display cells to only fire on change 
Naming and use of statics to be possibly revised.
 2023-08-11 04:46:52 +02:00
Charlotte eb0fb4d662 tests: -std=c++11 not optional 2023-08-11 04:46:52 +02:00
Charlotte 992a728ec7 tests: CXX may be e.g. gcc, so use CC and link stdc++ explicitly 2023-08-11 04:46:52 +02:00
Charlotte f9b149fa7b cxxrtl: add "-print-output" option, test in fmt 2023-08-11 04:46:52 +02:00
Charlotte a1de898fcc fmt: merge fuzzers since we don't rely on BigInteger logic 
This is per fmt's (effective) use, as it turns out, so we're not losing
any fidelity in the comparison.
 2023-08-11 04:46:52 +02:00
Charlotte 3571bf2c2d fmt: fuzz, remove some unnecessary busywork 
Removing some signed checks and logic where we've already guaranteed the
values to be positive.  Indeed, in these cases, if a negative value got
through (per my realisation in the signed fuzz harness), it would cause
an infinite loop due to flooring division.
 2023-08-11 04:46:52 +02:00
Charlotte 2ae551c0af fmt: fuzz, fix (remove extraneous + incorrect fill) 
"blk + chunks" is often an overrun, plus the fill is unnecessary; we
throw blk away immediately.
 2023-08-11 04:46:52 +02:00
Charlotte 9f9561379b fmt: format %t consistently at initial 2023-08-11 04:46:52 +02:00
Charlotte 75b44f21d1 fmt: rudimentary %m support (= %l) 2023-08-11 04:46:52 +02:00
Charlotte c382d7d3ac fmt: %t/$time support 2023-08-11 04:46:52 +02:00
Charlotte b0f69f2cd5 tests: test cxxrtl against iverilog (and uncover bug!) 2023-08-11 04:46:52 +02:00
Charlotte 51d9b73107 fmt: tests completing again 
We need to invoke "read_verilog" manually, since the default action on
input files is to defer processing.  Under such conditions, we never
simplify the AST, and initial $prints never execute.
 2023-08-11 04:46:52 +02:00
Charlotte 1eff84cb92 fmt: ensure test exits on fail 
shebang not honoured when directly called with "bash run-test.sh".
 2023-08-11 04:46:52 +02:00
whitequark c285880684 fmt: add tests for Verilog round trip of format expressions. 2023-08-11 04:46:52 +02:00
whitequark 67052f62ec fmt: add tests for Yosys evaluation of format expressions. 2023-08-11 04:46:52 +02:00
whitequark 9f8e039a4b ast: use new format string helpers. 2023-08-11 04:46:52 +02: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
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
N. Engelhardt 43780c9812
Merge pull request #3838 from povik/various-cleanup 2023-07-24 16:24:23 +02: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
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 7c6cc4c40b tests: Fix invocation of 'help -cells' 
There's no such thing as 'help -celltypes' and there probably never was.
 2023-07-10 12:42:09 +02:00
Jannis Harder a07f8ac38a check: Also check for conflicts with constant drivers 2023-06-23 18:07:28 +02:00
Miodrag Milanovic e6f7cf3b29 Update tests 2023-06-09 14:41:45 +02:00
Eddie Hung 862631d657 Add ABC9 DSP cascade test 2023-05-25 18:42:08 +01:00
Lofty 00b0e850db intel_alm: re-enable carry chains for ABC9 2023-05-25 18:28:10 +01:00
CORRADI Quentin e7156c644d Standard compliance for tests/verilog/block_labels.ys 
genvar declaration cannot take an initial value when declared as a module_or_generate_item_declaration.
Correct this test so that it doesn't fail unexpectedly if Yosys aligns with the standard.
 2023-05-21 16:38:14 -04:00
Miodrag Milanovic c2285b3460 fix file rights 2023-05-17 13:39:57 +02:00
Muthiah Annamalai (முத்து அண்ணாமலை) 693c609eec
Merge branch 'YosysHQ:master' into main/issue2525 2023-05-16 21:21:32 -07:00
Miodrag Milanović acfdc5cc42
Merge pull request #3755 from RTLWorks/muthu/issue3498 
[YOSYS] Issue #3498 - Fix Synopsys style unquoted Liberty style
 2023-05-15 16:34:35 +02:00
Miodrag Milanović 5c7cc6ff06
Merge pull request #3745 from rfuest/gowin_alu 
gowin: Fix X output of $alu techmap
 2023-05-09 11:12:50 +02:00
Muthu Annamalai 17cfc969dd [YOSYS] Issue #3498 - Fix Synopsys style unquoted Liberty style function body parsing with unittest 2023-05-06 23:37:47 -07:00
Muthu Annamalai d2f3251528 adding unittest 2023-05-04 22:43:04 -07:00
Dag Lem fb7f3bb290 Cleaner tests for RTLIL cells in struct_dynamic_range.sv 2023-05-04 14:28:21 +02:00
Dag Lem ad437c178d Handling of attributes for struct / union variables 
(* nowrshmsk *) on a struct / union variable now affects dynamic
bit slice assignments to members of the struct / union.

(* nowrshmsk *) can in some cases yield significant resource savings; the
combination of pipeline shifting and indexed writes is an example of this.

Constructs similar to the one below can benefit from (* nowrshmsk *), and
in addition it is no longer necessary to split out the shift assignments
on separate lines in order to avoid the error message "ERROR: incompatible
mix of lookahead and non-lookahead IDs in LHS expression."

    always_ff @(posedge clk) begin
        if (rotate) begin
            { v5, v4, v3, v2, v1, v0 } <= { v4, v3, v2, v1, v0, v5 };

            if (res) begin
                v0.bytes <= '0;
            end else if (w) begin
                v0.bytes[addr] <= data;
            end
        end
    end
 2023-05-03 18:44:07 +02:00
Ralf Fuest 30f1d10948 gowin: Fix X output of $alu techmap 2023-05-01 17:56:41 +02:00
Jannis Harder cee3cb31b9
Merge pull request #3734 from jix/fix_unbased_unsized_const 
verilog: Fix const eval of unbased unsized constants
 2023-04-24 16:08:48 +02:00
Benjamin Barzen 8611429237
ABC9: Cell Port Bug Patch (#3670) 
* ABC9: RAMB36E1 Bug Patch

* Add simplified testcase

* Also fix xaiger writer for under-width output ports

* Remove old testcase

* Missing top-level input port

* Fix tabs

---------

Co-authored-by: Eddie Hung <eddie@fpgeh.com>
 2023-04-22 16:24:36 -07:00
Jannis Harder 985f4926b7 verilog: Fix const eval of unbased unsized constants 
When the verilog frontend perfomed constant evaluation of unbased
unsized constants in a context-determined expression it did not properly
extend them by repeating the bit value. This only affected constant
evaluation and not constants that made it through unchanged to RTLIL.
The latter case was already covered by tests and working before.

This fixes the const-eval issue by checking the `is_unsized` flag in
bitsAsConst and extending the value accordingly.

The newly added test also tests the already working non-const-eval case
to highlight that both cases should behave the same.
 2023-04-20 12:12:50 +02:00
Miodrag Milanovic 0f5e7c244d add additional dff and lutram tests 2023-04-06 09:10:14 +02:00
Miodrag Milanovic 54d313efc3 add test for CCU2D 2023-04-06 09:10:14 +02:00
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