| Age | Commit message (Collapse) | Author |
|---|
|
The simple functionality is needed in chiseltest.
|
|
This fixes an off by one error, where 3 was erroneously
accepted as in-bounds for a memory of depth=3
|
|
* Fix unreachable code warning by changing match order
Simulation Statements did not previously extend IsDeclaration, but now
they do so their match blocks need to be above IsDeclaration.
* Handle MemoryNoInit case in RtlilEmitter
* Remove use of deprecated logToFile
* Fix uses of LegalizeClocksTransform
Replaced all uses of LegalizeClocksTransform with
LegalizeClocksAndAsyncResetsTransform.
* Remove use of CircuitForm in ZeroWidth
|
|
|
|
This should fix issue #2436
|
|
* 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 option to disable random mem/reg init
Co-authored-by: Jiuyang Liu <liu@jiuyang.me>
* fix for code review.
Co-authored-by: SharzyL <me@sharzy.in>
|
|
We never tested the case where the width of the
numerator was less than the denominator.
This should fix any issue with this combination.
|
|
+ correct the Error Info of "At least one dedupable annotation..."
|
|
* 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.
|
|
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.
|
|
|
|
|
|
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).
|
|
This will make it easier for formal verification
libraries to make use of these emitters.
|
|
|
|
* 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: include firrtl statement names in SMT and btor2 output
* smt: remove println
* smt: make tests run again and fix stale ones
Apparently `private` classes aren't found by th sbt test runner.
|
|
* bitWidth: add scaladoc
* smt: use existing bitWidth API
|
|
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
* smt: add end2end check for read enable modelling
|
|
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.
|
|
Fix scalafmtCheckAll failures that snuck through
|
|
|
|
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
|
|
|
|
* smt: add test for write port collision
* smt: add missing call to insertDummyAssignsForMemoryOutputs
* smt: fix typo in write port code
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
|
|
* smt: add tests for assert name clashes
* smt: ensure unique signal names with a namespace
this fixes issues #1934
|
|
|
|
If there is more than one clock, this will be detected and
the user will be promted to run the StutteringClock transform.
|
|
|
|
This adds an experimental new SMTLib and Btor2 emitter
that converts a firrtl module into a format
suitable for open source model checkers.
The format generally follows the behavior of yosys'
write_smt2 and write_btor commands.
To generate btor2 for the module in m.fir run
> ./utils/bin/firrtl -i m.fir -E experimental-btor2
for SMT:
> ./utils/bin/firrtl -i m.fir -E experimental-smt2
If you have a design with multiple clocks
or an asynchronous reset, try out the new StutteringClockTransform.
You can designate any input of type Clock to be your
global simulation clock using the new GlobalClockAnnotation.
If your toplevel module instantiates submodules,
you need to inline them if you want the submodule
logic to be included in the formal model.
|
