sfcX/src/main/scala/firrtl/backends/experimental/smt, branch master Scala FIRRTL Compiler for chiselX smt: make SMTExprMap object public (#2534) 2022-08-03T16:05:36+00:00 Kevin Laeufer 2022-08-03T16:05:36+00:00 ad0dd6a2808789d0eda3665d5f565f0988db2c77 The simple functionality is needed in chiseltest. 
The simple functionality is needed in chiseltest.
 [smt] correct comparison for out-of-bounds memory access check (#2463) 2022-01-17T23:29:14+00:00 Kevin Laeufer 2022-01-17T23:29:14+00:00 5569c72c1b6246efd203e00f7af6041567575eec This fixes an off by one error, where 3 was erroneously accepted as in-bounds for a memory of depth=3 
This fixes an off by one error, where 3 was erroneously
accepted as in-bounds for a memory of depth=3
 smt: deal correctly with negative SInt literals (#2447) 2021-12-21T17:07:30+00:00 Kevin Laeufer 2021-12-21T17:07:30+00:00 2d197c841c5400c6deaa1592525be6a1d81dc1e2 






smt: correctly serialize array index on read (#2446)
2021-12-17T20:04:52+00:00

Kevin Laeufer

2021-12-17T20:04:52+00:00

57ce615d73995a29f89c2f9b11482fe80442439b

This should fix issue #2436




This should fix issue #2436






Deprecate all mutable methods on RenameMap (#2444)
2021-12-17T18:07:25+00:00

Jack Koenig

2021-12-17T18:07:25+00:00

37c8528cfed4395924820b54498ef761ded17393

* Add renamemap.MutableRenameMap which includes these methods without
  deprecation
* Deprecate Stringly typed RenameMap APIs which were accidentally
  undeprecated a while ago

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>




* Add renamemap.MutableRenameMap which includes these methods without
  deprecation
* Deprecate Stringly typed RenameMap APIs which were accidentally
  undeprecated a while ago

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>






smt: fix handling of div primitive in formal backend (#2409)
2021-11-10T14:33:39+00:00

Kevin Laeufer

2021-11-10T14:33:39+00:00

18b9a987552492928aa1199d8cf498fe561c2f03

We never tested the case where the width of the
numerator was less than the denominator.
This should fix any issue with this combination.




We never tested the case where the width of the
numerator was less than the denominator.
This should fix any issue with this combination.






Bump Scala to 2.12.14 and 2.13.6 (#2356)
2021-09-14T03:42:27+00:00

Jack Koenig

2021-09-14T03:42:27+00:00

8421e96f04831fc61ddd5efa30f0ebc84f27c596

This required also bumping sbt-scalafix to bring in a newer version of
semanticdb. The new version of semanticdb had an issue with a regex in
SMTLib, fixed by fixing the way '$' is escaped in the regex.




This required also bumping sbt-scalafix to bring in a newer version of
semanticdb. The new version of semanticdb had an issue with a regex in
SMTLib, fixed by fixing the way '$' is escaped in the regex.






smt: make SMT + TransitionSystem lib public (#2350)
2021-09-08T22:18:53+00:00

Kevin Laeufer

2021-09-08T22:18:53+00:00

441930e2ad03f48adc052cd1d00af3d10d786dca












smt: refactor SMT expression library (#2347)
2021-09-08T22:00:46+00:00

Kevin Laeufer

2021-09-08T22:00:46+00:00

f76640d9dc4620a3b61975d54e5783c36e7c6936












[smt] treat stop with non-zero ret like an assertion (#2338)
2021-08-30T20:41:24+00:00

Kevin Laeufer

2021-08-30T20:41:24+00:00

de56a19b0a240e39366dc2d979ec05c65e0ada63

We treat it as an assertion that the stop will
never be enabled. stop(0) will still be ignored
(but now demoted to a info from a warning).




We treat it as an assertion that the stop will
never be enabled. stop(0) will still be ignored
(but now demoted to a info from a warning).