sfcX/src/test/scala/firrtl/backends, branch 1.6.x Scala FIRRTL Compiler for chiselX [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 






Remove some printlns in tests (#2445)
2021-12-17T17:39:34+00:00

Jack Koenig

2021-12-17T17:39:34+00:00

6b82bcf6690e38ff472a39eaae7e6375ff7085e4

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




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.






Add RTLIL Backend. (#2331)
2021-09-29T03:18:48+00:00

Nicolas Machado

2021-09-29T03:18:48+00:00

e70ee5367c864e55ff16637430b712666b7dbd2b

* Added RTLIL Backend.

* Add test for Rtlil Backend, fix per-module file emission, scalafmt, and apply bugfixes for inconsistencies found during testing.

* Fix build on scala 2.13

* Add additional equivalence test, make some bugfixes and perf opts to the emitter.

* Final changes as requested by Kevin, code cleanup, add support for formal cells.




* Added RTLIL Backend.

* Add test for Rtlil Backend, fix per-module file emission, scalafmt, and apply bugfixes for inconsistencies found during testing.

* Fix build on scala 2.13

* Add additional equivalence test, make some bugfixes and perf opts to the emitter.

* Final changes as requested by Kevin, code cleanup, add support for formal cells.






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).






[smt] make SMTLib + Btor2 emitters public objects (#2326)
2021-08-10T18:29:35+00:00

Kevin Laeufer

2021-08-10T18:29:35+00:00

b629e234e94c24ca04273b3322ce9200df873ce2

This will make it easier for formal verification
libraries to make use of these emitters.




This will make it easier for formal verification
libraries to make use of these emitters.






[smt] PropagatePresetAnnotations is now a real prereq (#2325)
2021-08-10T16:36:33+00:00

Kevin Laeufer

2021-08-10T16:36:33+00:00

78ae5e4ae9b35678d25328accb3beda8c28d3d4d












add emitter for optimized low firrtl (#2304)
2021-08-02T20:46:29+00:00

Kevin Laeufer

2021-08-02T20:46:29+00:00

e04f1e7f303920ac1d1f865450d0e280aafb58b3

* rearrange passes to enable optimized firrtl emission

* Support ConstProp on padded arguments to comparisons with literals

* Move shr legalization logic into ConstProp

Continue calling ConstProp of shr in Legalize.

Co-authored-by: Jack Koenig <koenig@sifive.com>

Co-authored-by: Jack Koenig <koenig@sifive.com>




* rearrange passes to enable optimized firrtl emission

* Support ConstProp on padded arguments to comparisons with literals

* Move shr legalization logic into ConstProp

Continue calling ConstProp of shr in Legalize.

Co-authored-by: Jack Koenig <koenig@sifive.com>

Co-authored-by: Jack Koenig <koenig@sifive.com>