sfcX/src/test/scala/firrtl/backends/experimental/smt/random, branch master 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
 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>
 SMT Backend: model Invalid and Division by Zero with DefRandom nodes (#2104) 2021-03-09T01:37:35+00:00 Kevin Laeufer 2021-03-09T01:37:35+00:00 8a4c156f401c8bfab5f2d595c32c20534f0722d7 This finally removes all randomization code from the transition system conversion and into a separate pass using DefRandom nodes. 
This finally removes all randomization code from the transition
system conversion and into a separate pass using DefRandom nodes.
 SMT: memory port inout fields cannot be used as RHS expressions (#2105) 2021-03-08T23:39:15+00:00 Kevin Laeufer 2021-03-08T23:39:15+00:00 29d57a612df69ae4a6db4b3755fc292e5a539e11 * SMT: memory port inout fields cannot be used as RHS expressions * smt: add end2end check for read enable modelling 
* SMT: memory port inout fields cannot be used as RHS expressions

* smt: add end2end check for read enable modelling
 SMT Backend: move undefined memory behavior modelling to firrtl IR level (#2095) 2021-03-04T19:23:51+00:00 Kevin Laeufer 2021-03-04T19:23:51+00:00 c93d6f5319efd7ba42147180c6e2b6f3796ef943 With this PR the smt backend now supports memories with more than two write ports and the conservative memory modelling can be selectively turned off with a new annotation. 
With this PR the smt backend now supports memories
with more than two write ports and the conservative
memory modelling can be selectively turned off with
a new annotation.