Clifford Wolf
|
1bee82ae2d
|
Fixed gcc build (c++11 stuff in ezSAT)
|
2013-06-12 10:18:01 +02:00 |
Clifford Wolf
|
4b311b7b99
|
Further improved and extended xsthammer
|
2013-06-11 19:49:35 +02:00 |
Clifford Wolf
|
8ce99fa686
|
More xsthammer improvements
|
2013-06-10 21:07:22 +02:00 |
Clifford Wolf
|
7f3f25841e
|
More sign-extension related fixes
|
2013-06-10 21:04:04 +02:00 |
Clifford Wolf
|
a5c30183b5
|
Sign-extension related fixes in SatGen and AST frontend
|
2013-06-10 17:10:06 +02:00 |
Clifford Wolf
|
9026511821
|
Progress xsthammer scripts
|
2013-06-10 16:17:09 +02:00 |
Clifford Wolf
|
7d790febb0
|
Improvements and fixes in SAT code
|
2013-06-10 16:09:29 +02:00 |
Clifford Wolf
|
15ff4cc63b
|
Added history file read/write to driver
|
2013-06-10 15:42:52 +02:00 |
Clifford Wolf
|
a6370ce857
|
Progress in xsthammer: working proof for cell models
|
2013-06-10 14:02:11 +02:00 |
Clifford Wolf
|
59dd02baa2
|
Fixes and improvements in AST const folding
|
2013-06-10 13:56:03 +02:00 |
Clifford Wolf
|
db98a18edb
|
Enabled AST/Verilog front-end optimizations per default
|
2013-06-10 13:19:04 +02:00 |
Clifford Wolf
|
af79b4bd98
|
Fixed generation of newlines in "dump" output
|
2013-06-10 12:38:02 +02:00 |
Clifford Wolf
|
95e937438f
|
Added "rename" command
|
2013-06-10 12:37:22 +02:00 |
Clifford Wolf
|
d07b32ade5
|
Progress on xsthammer
|
2013-06-10 12:37:05 +02:00 |
Clifford Wolf
|
af83ed168e
|
Added first xsthammer scripts
|
2013-06-10 01:40:20 +02:00 |
Clifford Wolf
|
08e2fa978c
|
Renamed "sat_solve" pass to "sat"
|
2013-06-09 21:55:53 +02:00 |
Clifford Wolf
|
a75b249427
|
Implemented temporal induction proofs in sat_solve
|
2013-06-09 18:07:05 +02:00 |
Clifford Wolf
|
b210234612
|
Added support for non-temporal proofs to sat_solve
|
2013-06-09 16:30:37 +02:00 |
Clifford Wolf
|
1349b845e3
|
Re-organization in sat_solver pass for temporal induction
|
2013-06-09 15:49:32 +02:00 |
Clifford Wolf
|
41932e8b64
|
Added ezSAT api support for don't care values in models
|
2013-06-09 14:21:18 +02:00 |
Clifford Wolf
|
b7ba90910d
|
Fixed handling of $_XOR_ in SAT generator
|
2013-06-09 14:01:50 +02:00 |
Clifford Wolf
|
0efde13775
|
Added sequential solving support to sat_solve
|
2013-06-09 13:35:46 +02:00 |
Clifford Wolf
|
6f330f0132
|
Set rl_basic_word_break_characters in shell
|
2013-06-09 11:51:06 +02:00 |
Clifford Wolf
|
e52c9aff1b
|
Improved readline tab completion
|
2013-06-09 01:04:23 +02:00 |
Clifford Wolf
|
bf59a28f80
|
Look for yosys-abc and yosys-svgviewer where the main exe is
|
2013-06-09 00:07:26 +02:00 |
Clifford Wolf
|
6c8a424872
|
Added "make abc" and "make install-abc"
|
2013-06-08 23:48:19 +02:00 |
Clifford Wolf
|
5a592b3739
|
Moved cmds from kernel/ to passes/cmds/
|
2013-06-08 23:16:36 +02:00 |
Clifford Wolf
|
4b7f070b69
|
Fixed typo is sat_solve help msg
|
2013-06-08 15:36:32 +02:00 |
Clifford Wolf
|
23a7973094
|
Added support for shifter cells to SAT generator
|
2013-06-08 15:12:08 +02:00 |
Clifford Wolf
|
92f04eab10
|
Added "cd" and "ls" commands for convenience
|
2013-06-08 14:45:28 +02:00 |
Clifford Wolf
|
1434312fdd
|
Various improvements in sat_solve pass and SAT generator
|
2013-06-08 14:11:50 +02:00 |
Clifford Wolf
|
99957a825f
|
Added -all and -max options to sat_solve
|
2013-06-08 12:17:30 +02:00 |
Clifford Wolf
|
25ae2d4df0
|
Fixes and improvements in ezSAT library
|
2013-06-08 12:14:20 +02:00 |
Clifford Wolf
|
c681c17038
|
Improved auto-detection of -show signals in sat_solve
|
2013-06-08 09:34:36 +02:00 |
Clifford Wolf
|
56b593b91c
|
Improved sat generator and sat_solve pass
|
2013-06-07 14:37:33 +02:00 |
Clifford Wolf
|
46fbe9d262
|
Added SAT generator and simple sat_solve command
|
2013-06-07 13:59:13 +02:00 |
Clifford Wolf
|
3371563f2f
|
Added ezSAT library
|
2013-06-07 10:38:35 +02:00 |
Clifford Wolf
|
c32b918681
|
Renamed opt_rmunused to opt_clean
|
2013-06-05 07:07:31 +02:00 |
Clifford Wolf
|
29d6ebd961
|
Implemented technology mapping for multipliers (using array multiplier)
|
2013-06-03 12:48:44 +02:00 |
Clifford Wolf
|
21d9251e52
|
Added "dump" command (part ilang backend)
|
2013-06-02 17:53:30 +02:00 |
Clifford Wolf
|
5f2c5f9017
|
Fixed techmap/flatten for positional module arguments
|
2013-05-26 12:21:17 +02:00 |
Clifford Wolf
|
b11d9408d9
|
Improved log messages generated by hierarchy pass
|
2013-05-26 12:20:51 +02:00 |
Clifford Wolf
|
cc587fb5f3
|
Added -nodetect option to fsm pass
|
2013-05-24 15:34:25 +02:00 |
Clifford Wolf
|
cc05404128
|
Fixed undef behavior in tests/asicworld/code_verilog_tutorial_fsm_full_tb.v
|
2013-05-24 15:15:59 +02:00 |
Clifford Wolf
|
66bc46b30b
|
Improved FSM one-hot encoding, added binary encoding
|
2013-05-24 14:39:19 +02:00 |
Clifford Wolf
|
ed0e2f7a6f
|
Added log_assert() api
|
2013-05-24 14:38:36 +02:00 |
Clifford Wolf
|
ccd2a93439
|
Added log_abort() api
|
2013-05-24 12:32:06 +02:00 |
Clifford Wolf
|
585fcace10
|
Fixed a gcc vs. clang determinism problem in abc pass
|
2013-05-23 16:17:23 +02:00 |
Clifford Wolf
|
f674150f1c
|
Fixed memory corruption bug in opt_rmunused
|
2013-05-23 13:19:28 +02:00 |
Clifford Wolf
|
cbe423a1fe
|
Only initialize TCL interpreter when needed
|
2013-05-23 12:56:23 +02:00 |