Commit Graph

477 Commits

Author SHA1 Message Date
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
Clifford Wolf 67b1026297
Merge pull request #591 from hzeller/virtual-override
Consistent use of 'override' for virtual methods in derived classes.
2018-08-15 14:05:38 +02:00
Clifford Wolf dfc0c8ffc8
Merge pull request #576 from cr1901/no-resource
Gate POSIX-only signals and resource module to only run on POSIX Pyth…
2018-08-15 14:00:19 +02:00
Clifford Wolf 1dd156f516 Fix use of signed integers in JSON back-end
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-08-14 23:31:25 +02:00
jpathy 7db05b2cc1
Use `realpath`
Use `os.path.realpath` instead to make sure symlinks are followed. This is also required to work for nix package manager.
2018-08-06 06:51:07 +00:00
Henner Zeller 3aa4484a3c Consistent use of 'override' for virtual methods in derived classes.
o Not all derived methods were marked 'override', but it is a great
  feature of C++11 that we should make use of.
o While at it: touched header files got a -*- c++ -*- for emacs to
  provide support for that language.
o use YS_OVERRIDE for all override keywords (though we should probably
  use the plain keyword going forward now that C++11 is established)
2018-07-20 23:51:06 -07:00
William D. Jones 0caa62802c Gate POSIX-only signals and resource module to only run on POSIX Python implementations. 2018-07-06 01:44:34 -04:00
Sergiusz Bazanski 1690dafde1 Fix protobuf build 2018-06-20 19:28:43 +01:00
Serge Bazanski 53e9a1549c Add Protobuf backend
Signed-off-by: Serge Bazanski <q3k@symbioticeda.com>
2018-06-19 13:34:56 +01:00
Clifford Wolf d9a2b43014 Add $dlatch support to write_verilog
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-04-22 16:03:26 +02:00
Clifford Wolf 5ca91ca019 Add "write_blif -inames -iattr"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-04-15 14:07:21 +02:00
Clifford Wolf 4d6af2969c Add smtio.py support for parsing SMT2 (_ bvX n) syntax for BitVec constants
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-04-04 18:12:27 +02:00
Clifford Wolf 25a864fc73 Fixed -stbv handling in SMT2 back-end 2018-04-04 17:28:07 +02:00
Clifford Wolf dd5fab69c1 Add smtio status msgs when --progress is inactive
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-29 21:59:30 +02:00
Clifford Wolf a48c7e5abf Bugfix in smtio.py VCD file generator
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-29 12:45:31 +02:00
Clifford Wolf 77bd645c35 Add $mem support to SMT2 clock tagging
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-27 02:11:20 +02:00
Clifford Wolf 3f00702475 Improve yosys-smtbmc log output and error handling
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-17 18:06:17 +01:00
Clifford Wolf 4d4e3a8ca6 Improve handling of invalid check-sat result in smtio.py
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-17 12:17:53 +01:00
Clifford Wolf 3545c0fffb Remove debug prints from yosys-smtbmc VCD writer
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-08 16:24:35 +01:00
Clifford Wolf 8b604004da Check results of (check-sat) in yosys-smtbmc
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-07 22:54:19 +01:00
Clifford Wolf cedbc35f4b Imporove yosys-smtbmc error handling, Improve VCD output
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-05 12:17:22 +01:00
Clifford Wolf 8b7602e660 Improve SMT2 encoding of $reduce_{and,or,bool}
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-04 21:22:20 +01:00
Clifford Wolf 45a6fce92c Fix a hangup in yosys-smtbmc error handling
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-04 21:13:30 +01:00
Clifford Wolf ae4e204c76 Improved error handling in yosys-smtbmc
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-03 20:00:07 +01:00
Clifford Wolf a44e1edaa3 Terminate running SMT solver when smtbmc is terminated
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-03 14:50:40 +01:00
Clifford Wolf 3ced2cca6e Fix smtbmc smtc/aiw parser for wire names containing []
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-03 14:15:49 +01:00
Clifford Wolf 90ae426078 Mangle names with square brackets in VCD files to work around issues in gtkwave
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-01 14:15:27 +01:00
Clifford Wolf 675dd5347a Small fixes and improvements in $allconst/$allseq handling
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-02-26 11:58:44 +01:00
Clifford Wolf b13e6bd375 Add smtbmc support for exist-forall problems
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-02-23 19:33:30 +01:00
Clifford Wolf 17583b6a21 Add support for mockup clock signals in yosys-smtbmc vcd output
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-02-20 17:45:22 +01:00
Clifford Wolf c9672e2e2e Fix handling of zero-length cell connections in SMT2 back-end
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-02-08 19:12:12 +01:00
Clifford Wolf e4f0218907 Fixed gcc 7.2 "statement will never be executed" warning 2018-02-03 14:31:47 +01:00
Clifford Wolf e97f10b142 Fix smtio.py for large SMT2 S-expressions 2018-01-29 12:34:28 +01:00
Clifford Wolf 54aeca0983 Move user-provided smt2 info stmts to the top of the yosys-smtbmc smt2 output 2018-01-18 14:25:22 +01:00
Clifford Wolf 9804ebedbf Add "no driver for signal bit" error msg to btor back-end 2017-12-24 17:30:36 +01:00
Clifford Wolf 292984896b Simple fix BTOR memory encoding 2017-12-17 18:57:54 +01:00
Clifford Wolf bbdcc1f9d4 Improve BTOR memory encoding 2017-12-17 18:55:17 +01:00
Clifford Wolf 30f23281ed Add array support to btor back-end 2017-12-15 02:19:06 +01:00
Clifford Wolf ad901671c5 Add $anyconst/$anyseq support to btor back-end 2017-12-15 00:40:24 +01:00
Clifford Wolf 162c29bd6b Merge branch 'master' into btor-ng 2017-12-14 03:13:47 +01:00
Clifford Wolf 9419de3e37 Add yosys-smtbmc VCD writer support for memories with async writes 2017-12-14 03:06:00 +01:00
Clifford Wolf a48ec49017 Merge branch 'master' into btor-ng 2017-12-14 02:17:01 +01:00