Commit Graph

602 Commits

Author SHA1 Message Date
Clifford Wolf 53b28b3f01
Merge pull request #869 from cr1901/win-shell
Install launcher executable when running yosys-smtbmc on Windows.
2019-03-14 16:43:23 +01:00
William D. Jones ff15cf9b1f Install launcher executable when running yosys-smtbmc on Windows.
Signed-off-by: William D. Jones <thor0505@comcast.net>
2019-03-13 13:49:16 -04:00
Clifford Wolf 20c6a8c9b0 Improve determinism of IdString DB for similar scripts
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-11 20:12:28 +01:00
Clifford Wolf 94f995ee37 Fix signed $shift/$shiftx handling in write_smt2
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-09 13:19:41 -08:00
Clifford Wolf 5dfc7becca Use SVA label in smt export if available
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-07 11:31:46 -08:00
Jim Lawson d6c4dfb902 Ensure fid() calls make_id() for consistency; tests/simple/dff_init.v fails
Mark dff_init.v as expected to fail since it uses "initial value".
2019-03-04 13:37:23 -08:00
Clifford Wolf 03237de686 Fix "write_edif -gndvccy"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-01 12:59:07 -08:00
Clifford Wolf 241901461a Add "write_verilog -siminit"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-02-28 15:03:03 -08:00
Larry Doolittle e2fc18f27b Reduce amount of trailing whitespace in code base 2019-02-28 14:58:11 -08:00
Clifford Wolf 6d143c9a01
Merge pull request #827 from ucb-bar/firrtlfixes
Fix FIRRTL to Verilog process instance subfield assignment.
2019-02-28 14:45:04 -08:00
Clifford Wolf f570aa5e1d Fix smt2 code generation for partially initialized memowy words, fixes #831
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-02-28 12:15:58 -08:00
Eddie Hung 8e883d92ed write_xaiger to behave for undriven/unused inouts 2019-02-26 12:17:51 -08:00
Eddie Hung c492a3a1c4 write_xaiger duplicate inout port into out port with $inout.out suffix 2019-02-25 18:39:36 -08:00
Jim Lawson 171c425cf9 Fix FIRRTL to Verilog process instance subfield assignment.
Don't emit subfield assignments: bits(x, y, z) <= ... - but instead, add them to the reverse-wire-map where they'll be treated at the end of the module.
Enable tests which were disabled due to incorrect treatment of subfields.
Assume the `$firrtl2verilog` variable contains any additional switches to control verilog generation (i.e. `--no-dedup -X mverilog`)
2019-02-25 16:18:13 -08:00
Eddie Hung 292f80d231 Cleanup abc9 code 2019-02-25 15:20:56 -08:00
Eddie Hung 5180338e80 write_xaiger to write __dummy_o__ for -symbols too 2019-02-21 17:03:18 -08:00
Eddie Hung 085ed9f487 Add attribution 2019-02-21 14:40:13 -08:00
Eddie Hung 2f96a0ed32 write_xaiger to use original bit for co, not sigmap()-ed bit 2019-02-21 11:15:25 -08:00
Eddie Hung 01f8d50ba2 Remove swap file 2019-02-20 16:17:01 -08:00
Eddie Hung f89b112fbf write_aiger: fix CI/CO and symbols 2019-02-20 15:35:32 -08:00
Eddie Hung ef60ca1717 write_xaiger to not write latches, CO/PO fixes 2019-02-20 11:09:13 -08:00
Eddie Hung f9af902532 Merge branch 'master' into xaig 2019-02-19 14:20:04 -08:00
Eddie Hung 11480b4fa3 Instead of INIT param on cells, use initial statement with hier ref as
per @cliffordwolf
2019-02-17 12:18:12 -08:00
Eddie Hung 17cd5f759f Merge https://github.com/YosysHQ/yosys into dff_init 2019-02-17 11:49:06 -08:00
Eddie Hung 30f1204721 Cleanup 2019-02-16 22:22:17 -08:00
Eddie Hung 76c35f80f4 Cleanup 2019-02-16 21:09:48 -08:00
Eddie Hung 6a57de9013 write_xaiger to support non-bit cell connections, and cope with COs for -O 2019-02-16 21:00:39 -08:00
Eddie Hung b9a305b85d write_aiger -O to write dummy output as __dummy_o__ 2019-02-16 20:08:59 -08:00
Eddie Hung 0c409e6d8c Tidy up write_xaiger 2019-02-16 08:48:33 -08:00
Eddie Hung 2c1655ae94 write_aiger() to perform CI/CO post-processing and fix symbols 2019-02-16 08:46:25 -08:00
Eddie Hung 486a270415 Fixes needed for DFF circuits 2019-02-15 15:22:18 -08:00
Jim Lawson c245041bfe Removed unused variables, functions. 2019-02-15 12:00:28 -08:00
Eddie Hung 3ac5b65197 write_xaiger to cope with unknown cells by transforming them to CI/CO 2019-02-15 11:51:21 -08:00
Jim Lawson fc1c9aa11f Update cells supported for verilog to FIRRTL conversion.
Issue warning messages for missing parameterized modules and attempts to set initial values.
Replace simple "if (cell-type)" with "else if" chain.
Fix FIRRTL shift handling.
Add support for parameterized modules, $shift, $shiftx.
Handle default output file.
Deal with no top module.
Automatically run pmuxtree pass.
Allow EXTRA_FLAGS and SEED parameters to be set in the environment for tests/tools/autotest.mk.
Support FIRRTL regression testing in tests/tools/autotest.sh
Add xfirrtl files to test directories to exclude files from FIRRTL regression tests that are known to fail.
2019-02-15 11:14:17 -08:00
Eddie Hung c69fba8de5 More cleanup 2019-02-14 14:52:47 -08:00
Eddie Hung 7328775584 More cleanup of write_xaiger 2019-02-14 14:48:38 -08:00
Eddie Hung afa4389445 Get rid of formal stuff from xaiger backend 2019-02-14 13:27:26 -08:00
Eddie Hung f0f5d8a5cc Merge remote-tracking branch 'origin/read_aiger' into xaig 2019-02-13 14:09:36 -08:00
Eddie Hung 06cf0555ee Merge https://github.com/YosysHQ/yosys into xaig 2019-02-13 14:08:31 -08:00
Clifford Wolf 1f2548a564
Merge pull request #802 from whitequark/write_verilog_async_mem_ports
write_verilog: correctly emit asynchronous transparent ports
2019-02-12 14:41:34 +01:00
Eddie Hung ecd2446132 Add write_xaiger 2019-02-11 15:18:42 -08:00
Eddie Hung db08afe146 Copy backends/aiger/aiger.cc to xaiger.cc 2019-02-08 14:53:12 -08:00
Eddie Hung 20ca795b87 Remove check for cell->name[0] == '$' 2019-02-06 14:53:40 -08:00
Eddie Hung c373640a3a Refactor 2019-02-06 14:28:44 -08:00
Eddie Hung 8241db6960 write_verilog to cope with init attr on q when -noexpr 2019-02-06 14:17:09 -08:00
Clifford Wolf e112d2fbf5 Add missing blackslash-to-slash convertion to smtio.py (matching Smt2Worker::get_id() behavior)
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-02-06 16:35:59 +01:00
whitequark da65e1e8d9 write_verilog: correctly emit asynchronous transparent ports.
This commit fixes two related issues:
  * For asynchronous ports, clock is no longer added to domain list.
    (This would lead to absurd constructs like `always @(posedge 0)`.
  * The logic to distinguish synchronous and asynchronous ports is
    changed to correctly use or avoid clock in all cases.

Before this commit, the following RTLIL snippet (after memory_collect)

    cell $memrd $2
      parameter \MEMID "\\mem"
      parameter \ABITS 2
      parameter \WIDTH 4
      parameter \CLK_ENABLE 0
      parameter \CLK_POLARITY 1
      parameter \TRANSPARENT 1
      connect \CLK 1'0
      connect \EN 1'1
      connect \ADDR \mem_r_addr
      connect \DATA \mem_r_data
    end

would lead to invalid Verilog:

    reg [1:0] _0_;
    always @(posedge 1'h0) begin
      _0_ <= mem_r_addr;
    end
    assign mem_r_data = mem[_0_];

Note that there are two potential pitfalls remaining after this
change:
  * For asynchronous ports, the \EN input and \TRANSPARENT parameter
    are silently ignored. (Per discussion in #760 this is the correct
    behavior.)
  * For synchronous transparent ports, the \EN input is ignored. This
    matches the behavior of the $mem simulation cell. Again, see #760.
2019-01-29 02:24:00 +00:00
Clifford Wolf 81581f24fc
Merge pull request #800 from whitequark/write_verilog_tribuf
write_verilog: write $tribuf cell as ternary
2019-01-27 09:23:41 +01:00
whitequark 3d7925ad9f write_verilog: write $tribuf cell as ternary. 2019-01-27 00:24:06 +00:00
whitequark 42c47a83da write_verilog: escape names that match SystemVerilog keywords. 2019-01-27 00:03:53 +00:00
Clifford Wolf 54dc33b905 Add "write_edif -gndvccy"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-01-17 13:33:11 +01:00
Clifford Wolf 6c5049f016 Fix handling of $shiftx in Verilog back-end
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-01-15 10:55:27 +01:00
whitequark efa278e232 Fix typographical and grammatical errors and inconsistencies.
The initial list of hits was generated with the codespell command
below, and each hit was evaluated and fixed manually while taking
context into consideration.

    DIRS="kernel/ frontends/ backends/ passes/ techlibs/"
    DIRS="${DIRS} libs/ezsat/ libs/subcircuit"
    codespell $DIRS -S *.o -L upto,iff,thru,synopsys,uint

More hits were found by looking through comments and strings manually.
2019-01-02 13:12:17 +00:00
Larry Doolittle 99706b3bf4 Squelch a little more trailing whitespace 2018-12-29 12:46:54 +01:00
Clifford Wolf 23bb77867f Minor style fixes
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-12-18 20:02:39 +01:00
makaimann abf5930a33 Add btor ops for $mul, $div, $mod and $concat 2018-12-17 10:45:17 -08:00
whitequark ca866d384e write_verilog: handle the $shift cell.
The implementation corresponds to the following Verilog, which is
lifted straight from simlib.v:

    module \\$shift (A, B, Y);

    parameter A_SIGNED = 0;
    parameter B_SIGNED = 0;
    parameter A_WIDTH = 0;
    parameter B_WIDTH = 0;
    parameter Y_WIDTH = 0;

    input [A_WIDTH-1:0] A;
    input [B_WIDTH-1:0] B;
    output [Y_WIDTH-1:0] Y;

    generate
        if (B_SIGNED) begin:BLOCK1
            assign Y = $signed(B) < 0 ? A << -B : A >> B;
        end else begin:BLOCK2
            assign Y = A >> B;
        end
    endgenerate

    endmodule
2018-12-16 18:46:32 +00:00
Clifford Wolf ddff75b60a
Merge pull request #736 from whitequark/select_assert_list
select: print selection if a -assert-* flag causes an error
2018-12-16 16:45:49 +01:00
whitequark fccaa25ec1 write_verilog: add a missing newline. 2018-12-16 15:22:34 +00:00
Clifford Wolf f481ad4d44
Merge pull request #729 from whitequark/write_verilog_initial
write_verilog: correctly map RTLIL `sync init`
2018-12-16 15:50:16 +01:00
Clifford Wolf 0b9bb852c6 Add yosys-smtbmc support for btor witness
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-12-10 03:43:07 +01:00
Clifford Wolf 47a5dfdaa4 Add "yosys-smtbmc --btorwit" skeleton
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-12-08 06:59:27 +01:00
Clifford Wolf ed3c57fad3 Fix btor init value handling
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-12-08 06:21:31 +01:00
whitequark 7fe770a441 write_verilog: correctly map RTLIL `sync init`. 2018-12-07 18:55:08 +00:00
Clifford Wolf 82aaf6d908 Add "write_aiger -I -O -B"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-11-12 09:27:33 +01:00
Clifford Wolf 825b4c1aa9
Merge pull request #693 from YosysHQ/rlimit
improve rlimit handling in smtio.py
2018-11-07 20:16:40 +01:00
Clifford Wolf b54bf7c0f9 Limit stack size to 16 MB on Darwin
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-11-07 15:32:34 +01:00
Clifford Wolf f6c4485a3a Run solver in non-incremental mode whem smtio.py is configured for non-incremental solving
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-11-06 11:11:05 +01:00
Clifford Wolf 4c50e3abb9 Fix for improved smtio.py rlimit code
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-11-06 10:09:03 +01:00
Clifford Wolf 79075d123f Improve stack rlimit code in smtio.py
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-11-06 10:05:23 +01:00
Arjen Roodselaar 2b93542171 Use conservative stack size for SMT2 on MacOS 2018-11-04 21:58:09 -08:00
Clifford Wolf d0acea4f2e Add proper error message for when smtbmc "append" fails
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-11-04 14:41:28 +01:00
Clifford Wolf b6781c6f4b Add support for signed $shift/$shiftx in smt2 back-end
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-11-01 11:40:58 +01:00
rafaeltp c7770d9eea adding offset info to memories 2018-10-18 16:22:33 -07:00
rafaeltp 609f46eeb7 adding offset info to memories 2018-10-18 16:20:21 -07:00
Clifford Wolf f4ad05e133
Merge pull request #663 from aman-goel/master
Update to .smv backend
2018-10-17 12:18:57 +02:00
Aman Goel 749b3ed62a Minor update 2018-10-15 13:54:12 -04:00
Clifford Wolf 115ca57647 Add "write_edif -attrprop"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-10-05 09:41:30 +02:00
Aman Goel 90e0938f9a Update to .smv backend
Splitting VAR and ASSIGN into IVAR, VAR, DEFINE and ASSIGN. This allows better handling by nuXmv for post-processing (since now only state variables are listed under VAR).
2018-10-01 19:03:10 -04:00
Miodrag Milanovic 41affeeeb9 added prefix to FDirection constants, fixing windows build 2018-09-21 20:43:49 +02:00
acw1251 efac8a45a6 Fixed typo in "verilog_write" help message 2018-09-18 13:34:30 -04:00
Clifford Wolf 12440fcc8f Add $lut support to Verilog back-end
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-09-06 00:18:01 +02:00
Jim Lawson 380c6f0e97 Remove unused functions. 2018-08-27 10:18:33 -07:00
Jim Lawson 93d19dc2fb Add support for module instances.
Don't pad logical operands to one bit.
Use operand width and signedness in $reduce_bool.
Shift amounts are unsigned and shouldn't be padded.
Group "is invalid" with the wire declaration, not its use (otherwise it is incorrectly wired to 0).
2018-08-23 14:35:11 -07:00
Clifford Wolf 67b1026297
Merge pull request #591 from hzeller/virtual-override
Consistent use of 'override' for virtual methods in derived classes.
2018-08-15 14:05:38 +02:00
Clifford Wolf dfc0c8ffc8
Merge pull request #576 from cr1901/no-resource
Gate POSIX-only signals and resource module to only run on POSIX Pyth…
2018-08-15 14:00:19 +02:00
Clifford Wolf 1dd156f516 Fix use of signed integers in JSON back-end
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-08-14 23:31:25 +02:00
jpathy 7db05b2cc1
Use `realpath`
Use `os.path.realpath` instead to make sure symlinks are followed. This is also required to work for nix package manager.
2018-08-06 06:51:07 +00:00
Henner Zeller 3aa4484a3c Consistent use of 'override' for virtual methods in derived classes.
o Not all derived methods were marked 'override', but it is a great
  feature of C++11 that we should make use of.
o While at it: touched header files got a -*- c++ -*- for emacs to
  provide support for that language.
o use YS_OVERRIDE for all override keywords (though we should probably
  use the plain keyword going forward now that C++11 is established)
2018-07-20 23:51:06 -07:00
William D. Jones 0caa62802c Gate POSIX-only signals and resource module to only run on POSIX Python implementations. 2018-07-06 01:44:34 -04:00
Sergiusz Bazanski 1690dafde1 Fix protobuf build 2018-06-20 19:28:43 +01:00
Serge Bazanski 53e9a1549c Add Protobuf backend
Signed-off-by: Serge Bazanski <q3k@symbioticeda.com>
2018-06-19 13:34:56 +01:00
Clifford Wolf d9a2b43014 Add $dlatch support to write_verilog
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-04-22 16:03:26 +02:00
Clifford Wolf 5ca91ca019 Add "write_blif -inames -iattr"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-04-15 14:07:21 +02:00
Clifford Wolf 4d6af2969c Add smtio.py support for parsing SMT2 (_ bvX n) syntax for BitVec constants
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-04-04 18:12:27 +02:00
Clifford Wolf 25a864fc73 Fixed -stbv handling in SMT2 back-end 2018-04-04 17:28:07 +02:00
Clifford Wolf dd5fab69c1 Add smtio status msgs when --progress is inactive
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-29 21:59:30 +02:00
Clifford Wolf a48c7e5abf Bugfix in smtio.py VCD file generator
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-29 12:45:31 +02:00
Clifford Wolf 77bd645c35 Add $mem support to SMT2 clock tagging
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-27 02:11:20 +02:00
Clifford Wolf 3f00702475 Improve yosys-smtbmc log output and error handling
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-17 18:06:17 +01:00