Alberto Gonzalez
|
57f48f94c2
|
Clean up `passes/cmds/show.cc`.
|
2020-04-06 08:51:25 +00:00 |
Alberto Gonzalez
|
fdeeb48e62
|
Clean up private member usage in `passes/cmds/bugpoint.cc`.
|
2020-04-06 08:35:09 +00:00 |
Alberto Gonzalez
|
2dd09ab611
|
Clean up private member usage in `passes/cmds/copy.cc`.
|
2020-04-06 08:26:10 +00:00 |
Alberto Gonzalez
|
5e9c88501e
|
Clean up `passes/cmds/splice.cc`.
|
2020-04-06 07:42:46 +00:00 |
Alberto Gonzalez
|
2e27ddd511
|
Clean up `passes/cmds/setattr.cc`.
|
2020-04-06 06:52:18 +00:00 |
Alberto Gonzalez
|
968230261f
|
Clean up `passes/cmds/connwrappers.cc`.
|
2020-04-06 06:11:25 +00:00 |
Alberto Gonzalez
|
1226d41c61
|
Clean up `passes/cmds/delete.cc`.
|
2020-04-06 05:09:43 +00:00 |
Alberto Gonzalez
|
b39a0d77ab
|
Clean up `passes/cmds/stat.cc`.
|
2020-04-06 04:39:18 +00:00 |
Alberto Gonzalez
|
438d2e0025
|
Clean up `passes/tests/test_autotb.cc`.
|
2020-04-06 04:25:21 +00:00 |
Alberto Gonzalez
|
f3e282a97c
|
Clean up `passes/techmap/dfflibmap.cc`.
|
2020-04-06 03:02:40 +00:00 |
Alberto Gonzalez
|
9168701881
|
Clean up pseudo-private member usage and simplify `passes/techmap/abc.cc`.
|
2020-04-05 21:31:18 +00:00 |
Alberto Gonzalez
|
64a32ead38
|
Clean up `passes/techmap/extract.cc`.
|
2020-04-05 19:36:23 +00:00 |
Alberto Gonzalez
|
5431ce694c
|
Clean up `passes/hierarchy/submod.cc`.
|
2020-04-05 04:39:54 +00:00 |
Alberto Gonzalez
|
5fedd0931c
|
Use newly-renamed `-push-copy` option.
|
2020-04-04 22:22:54 +00:00 |
Alberto Gonzalez
|
0ca3a8e94f
|
Improve style in `passes/sat/qbfsat.cc`.
|
2020-04-04 22:13:27 +00:00 |
Alberto Gonzalez
|
1db73e8dd2
|
Gracefully report error when module has nothing to prove.
|
2020-04-04 22:13:27 +00:00 |
Alberto Gonzalez
|
8f0f13cad2
|
Suppress `yosys-smtbmc` output unless the new `-show-smtbmc` option is provided.
|
2020-04-04 22:13:27 +00:00 |
Alberto Gonzalez
|
ce033a8e36
|
Fix handling of `-sat` and `-unsat` options when the solver returns `unknown`.
|
2020-04-04 22:13:26 +00:00 |
Alberto Gonzalez
|
6af8b767b4
|
Use `log_push()` and `log_pop()` and show the satisfiable model when `-specialize` is not specified.
Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
|
2020-04-04 22:13:26 +00:00 |
Alberto Gonzalez
|
d311a80222
|
Clean up `qbfsat` command and fix AND-reduction of miter outputs.
|
2020-04-04 22:13:26 +00:00 |
Alberto Gonzalez
|
125a583c57
|
Use the `-duplicate` option rather than `-save` and `-load` with an explicit name.
Co-Authored-By: Claire Wolf <claire@symbioticeda.com>
|
2020-04-04 22:13:26 +00:00 |
Alberto Gonzalez
|
86fc49a9d6
|
Use internal `run_command()` API instead of `popen()`.
Co-Authored-By: Claire Wolf <claire@symbioticeda.com>
|
2020-04-04 22:13:26 +00:00 |
Alberto Gonzalez
|
09b2264837
|
Clean up manual casting.
Co-Authored-By: David Shah <dave@ds0.me>
|
2020-04-04 22:13:26 +00:00 |
Alberto Gonzalez
|
acf96b6b0b
|
Remove unimplemented `-timeout` option.
|
2020-04-04 22:13:26 +00:00 |
Alberto Gonzalez
|
bb101e0b3a
|
Implement the `-assume-outputs`, `-sat`, and -unsat` options for the `qbfsat` command.
|
2020-04-04 22:13:26 +00:00 |
Alberto Gonzalez
|
5527063f66
|
Add NDEBUG guards to `qbfsat` assertions.
|
2020-04-04 22:13:26 +00:00 |
Alberto Gonzalez
|
3a4fd4a999
|
Implement `-specialize-from-file` option for the `qbfsat` command.
|
2020-04-04 22:13:26 +00:00 |
Alberto Gonzalez
|
b9e79e0bb7
|
Implement `-write-solution` option for the `qbfsat` command.
|
2020-04-04 22:13:26 +00:00 |
Alberto Gonzalez
|
d07ac2612b
|
Clean up `passes/sat/qbfsat.cc`.
|
2020-04-04 22:13:26 +00:00 |
Alberto Gonzalez
|
437afa1f0c
|
Updated `yosys-smtbmc` to optionally dump raw bit strings, and fixed hole value recovery using that mode.
|
2020-04-04 22:13:25 +00:00 |
Alberto Gonzalez
|
a4598d64ef
|
Hole value recovery and specialization implementation for `qbfsat` command.
|
2020-04-04 22:13:25 +00:00 |
Alberto Gonzalez
|
2fff574741
|
Barebones implementation of `qbfsat` command.
|
2020-04-04 22:13:25 +00:00 |
Alberto Gonzalez
|
fb878b2a70
|
Initial skeleton for `qbfsat` command.
|
2020-04-04 22:13:25 +00:00 |
Alberto Gonzalez
|
a0416fe167
|
Rename `-duplicate` to `-push-copy`.
Co-Authored-By: whitequark <whitequark@whitequark.org>
|
2020-04-04 21:26:11 +00:00 |
Eddie Hung
|
d61a6b81fc
|
Merge pull request #1648 from YosysHQ/eddie/cmp2lcu
"techmap -map +/cmp2lcu.v" for decomposing arithmetic compares to $lcu
|
2020-04-03 16:28:25 -07:00 |
Eddie Hung
|
7b38cde2df
|
cmp2lcu: rename _90_lcu_cmp -> _80_lcu_cmp
|
2020-04-03 14:28:22 -07:00 |
Eddie Hung
|
7b09a20c0c
|
cmp2lcu: fail if `LUT_WIDTH < 2
|
2020-04-03 14:28:22 -07:00 |
Eddie Hung
|
34c9b83854
|
synth: only techmap cmp2{lut,lcu} if -lut
|
2020-04-03 14:28:22 -07:00 |
Eddie Hung
|
5b87720b16
|
synth: use +/cmp2lcu.v in generic 'synth' too
|
2020-04-03 14:28:22 -07:00 |
Eddie Hung
|
2bf03c6ae0
|
Cleanup +/cmp2lut.v
|
2020-04-03 14:28:22 -07:00 |
Eddie Hung
|
051aefc3c2
|
synth_xilinx: techmap +/cmp2lut.v and +/cmp2lcu.v in 'coarse'
|
2020-04-03 14:28:22 -07:00 |
Eddie Hung
|
99a32432aa
|
+/cmp2lcu.v to work efficiently for fully/partially constant inputs
|
2020-04-03 14:28:22 -07:00 |
Eddie Hung
|
92d70cafec
|
+/cmp2lcu.v to work efficiently for fully/partially constant inputs
|
2020-04-03 14:28:22 -07:00 |
Eddie Hung
|
f68d723cdc
|
Refactor +/cmp2lcu.v into recursive techmap
|
2020-04-03 14:28:22 -07:00 |
Eddie Hung
|
8e851badc4
|
Cleanup
|
2020-04-03 14:28:22 -07:00 |
Eddie Hung
|
da880d5016
|
Cleanup cmp2lcu.v
|
2020-04-03 14:28:22 -07:00 |
Eddie Hung
|
9b63700678
|
techmap +/cmp2lcu.v for decomposing arithmetic compares to $lcu
|
2020-04-03 14:28:22 -07:00 |
Eddie Hung
|
fffe42d4c1
|
cmp2lut: comment out unused since 362f4f9
|
2020-04-03 14:28:04 -07:00 |
Alberto Gonzalez
|
409e2ac09d
|
Add `-duplicate` option to the `design` command.
|
2020-04-03 16:46:35 +00:00 |
whitequark
|
745251a31f
|
splitnets: skip modules with processes.
|
2020-04-03 11:27:19 +00:00 |