Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | write_xaiger to support non-bit cell connections, and cope with COs for -O | Eddie Hung | 2019-02-16 | 1 | -13/+15 |
| | |||||
* | write_aiger -O to write dummy output as __dummy_o__ | Eddie Hung | 2019-02-16 | 1 | -2/+5 |
| | |||||
* | Tidy up write_xaiger | Eddie Hung | 2019-02-16 | 1 | -8/+6 |
| | |||||
* | write_aiger() to perform CI/CO post-processing and fix symbols | Eddie Hung | 2019-02-16 | 1 | -7/+17 |
| | |||||
* | Fixes needed for DFF circuits | Eddie Hung | 2019-02-15 | 1 | -4/+3 |
| | |||||
* | write_xaiger to cope with unknown cells by transforming them to CI/CO | Eddie Hung | 2019-02-15 | 1 | -6/+44 |
| | |||||
* | More cleanup | Eddie Hung | 2019-02-14 | 1 | -15/+6 |
| | |||||
* | More cleanup of write_xaiger | Eddie Hung | 2019-02-14 | 1 | -73/+1 |
| | |||||
* | Get rid of formal stuff from xaiger backend | Eddie Hung | 2019-02-14 | 1 | -58/+0 |
| | |||||
* | Merge remote-tracking branch 'origin/read_aiger' into xaig | Eddie Hung | 2019-02-13 | 1 | -1/+1 |
|\ | |||||
| * | Remove check for cell->name[0] == '$' | Eddie Hung | 2019-02-06 | 1 | -1/+1 |
| | | |||||
* | | Merge https://github.com/YosysHQ/yosys into xaig | Eddie Hung | 2019-02-13 | 1 | -38/+41 |
|\ \ | |||||
| * \ | Merge pull request #802 from whitequark/write_verilog_async_mem_ports | Clifford Wolf | 2019-02-12 | 1 | -38/+41 |
| |\ \ | | | | | | | | | write_verilog: correctly emit asynchronous transparent ports | ||||
| | * | | write_verilog: correctly emit asynchronous transparent ports. | whitequark | 2019-01-29 | 1 | -38/+41 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | ||||
* | | | | Add write_xaiger | Eddie Hung | 2019-02-11 | 2 | -21/+11 |
| | | | | |||||
* | | | | Copy backends/aiger/aiger.cc to xaiger.cc | Eddie Hung | 2019-02-08 | 1 | -0/+788 |
| |_|/ |/| | | |||||
* | | | Refactor | Eddie Hung | 2019-02-06 | 1 | -21/+5 |
| | | | |||||
* | | | write_verilog to cope with init attr on q when -noexpr | Eddie Hung | 2019-02-06 | 1 | -2/+32 |
|/ / | |||||
* / | Add missing blackslash-to-slash convertion to smtio.py (matching ↵ | Clifford Wolf | 2019-02-06 | 1 | -1/+1 |
|/ | | | | | | Smt2Worker::get_id() behavior) Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Merge pull request #800 from whitequark/write_verilog_tribuf | Clifford Wolf | 2019-01-27 | 1 | -0/+12 |
|\ | | | | | write_verilog: write $tribuf cell as ternary | ||||
| * | write_verilog: write $tribuf cell as ternary. | whitequark | 2019-01-27 | 1 | -0/+12 |
| | | |||||
* | | write_verilog: escape names that match SystemVerilog keywords. | whitequark | 2019-01-27 | 1 | -0/+27 |
|/ | |||||
* | Add "write_edif -gndvccy" | Clifford Wolf | 2019-01-17 | 1 | -5/+13 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Fix handling of $shiftx in Verilog back-end | Clifford Wolf | 2019-01-15 | 1 | -3/+6 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Fix typographical and grammatical errors and inconsistencies. | whitequark | 2019-01-02 | 4 | -7/+7 |
| | | | | | | | | | | | | 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. | ||||
* | Squelch a little more trailing whitespace | Larry Doolittle | 2018-12-29 | 1 | -3/+3 |
| | |||||
* | Minor style fixes | Clifford Wolf | 2018-12-18 | 2 | -1/+1 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Add btor ops for $mul, $div, $mod and $concat | makaimann | 2018-12-17 | 2 | -2/+38 |
| | |||||
* | write_verilog: handle the $shift cell. | whitequark | 2018-12-16 | 1 | -0/+29 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 | ||||
* | Merge pull request #736 from whitequark/select_assert_list | Clifford Wolf | 2018-12-16 | 1 | -1/+1 |
|\ | | | | | select: print selection if a -assert-* flag causes an error | ||||
| * | write_verilog: add a missing newline. | whitequark | 2018-12-16 | 1 | -1/+1 |
| | | |||||
* | | Merge pull request #729 from whitequark/write_verilog_initial | Clifford Wolf | 2018-12-16 | 1 | -0/+2 |
|\ \ | | | | | | | write_verilog: correctly map RTLIL `sync init` | ||||
| * | | write_verilog: correctly map RTLIL `sync init`. | whitequark | 2018-12-07 | 1 | -0/+2 |
| |/ | |||||
* | | Add yosys-smtbmc support for btor witness | Clifford Wolf | 2018-12-10 | 1 | -15/+100 |
| | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | | Add "yosys-smtbmc --btorwit" skeleton | Clifford Wolf | 2018-12-08 | 1 | -1/+19 |
| | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | | Fix btor init value handling | Clifford Wolf | 2018-12-08 | 1 | -9/+13 |
|/ | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Add "write_aiger -I -O -B" | Clifford Wolf | 2018-11-12 | 1 | -2/+36 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Merge pull request #693 from YosysHQ/rlimit | Clifford Wolf | 2018-11-07 | 1 | -8/+11 |
|\ | | | | | improve rlimit handling in smtio.py | ||||
| * | Limit stack size to 16 MB on Darwin | Clifford Wolf | 2018-11-07 | 1 | -1/+4 |
| | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Fix for improved smtio.py rlimit code | Clifford Wolf | 2018-11-06 | 1 | -1/+1 |
| | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Improve stack rlimit code in smtio.py | Clifford Wolf | 2018-11-06 | 1 | -8/+8 |
| | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | | Run solver in non-incremental mode whem smtio.py is configured for ↵ | Clifford Wolf | 2018-11-06 | 1 | -3/+12 |
|/ | | | | | | non-incremental solving Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Use conservative stack size for SMT2 on MacOS | Arjen Roodselaar | 2018-11-04 | 1 | -1/+6 |
| | |||||
* | Add proper error message for when smtbmc "append" fails | Clifford Wolf | 2018-11-04 | 1 | -2/+10 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Add support for signed $shift/$shiftx in smt2 back-end | Clifford Wolf | 2018-11-01 | 1 | -1/+3 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | adding offset info to memories | rafaeltp | 2018-10-18 | 1 | -1/+1 |
| | |||||
* | adding offset info to memories | rafaeltp | 2018-10-18 | 1 | -2/+3 |
| | |||||
* | Merge pull request #663 from aman-goel/master | Clifford Wolf | 2018-10-17 | 1 | -32/+51 |
|\ | | | | | Update to .smv backend | ||||
| * | Minor update | Aman Goel | 2018-10-15 | 1 | -1/+1 |
| | | |||||
| * | Update to .smv backend | Aman Goel | 2018-10-01 | 1 | -33/+52 |
| | | | | | | | | 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). |