mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-26 01:14:37 +00:00
Code Activity
14768 commits 122 branches 59 tags 72 MiB
Commit graph

1618 commits

Author SHA1 Message Date
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