Clifford Wolf
04e920337b
Fix a syntax bug in ilang backend related to process case statements
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-14 17:50:20 +01:00
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
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
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
Jim Lawson
c245041bfe
Removed unused variables, functions.
2019-02-15 12:00:28 -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
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
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