| Age | Commit message (Collapse) | Author |
|---|
|
The simple functionality is needed in chiseltest.
|
|
This fixes handling of signed modulus and removes some redundant work.
|
|
- Fix & test MemorySynthInit behavior with MemoryArrayInitAnnotation and MemoryScalarInitAnnotation.
Add test case for MemoryRandomInitAnnotation which is, on the contrary, expected not to leak any randomization statement in synthesis context.
- Refactor MemoryInitSpec for improved results readability
Context:
PR #2166 (commit: 4530152) introduced MemorySynthInit annotation to control whether statement generated with Memory*InitAnnotation (emitted within initial begin block in verilog) should be guarded with ifndef SYNTHESIS or not.
Unfortunately only one configuration (MemoryFileInlineAnnotation) has been tested while the others have been generating incorrect verilog statements (MemoryArrayInitAnnotation and MemoryScalarInitAnnotation).
Signed-off-by: Jean Bruant <jean.bruant@ovhcloud.com>
|
|
This fixes an off by one error, where 3 was erroneously
accepted as in-bounds for a memory of depth=3
|
|
* Add FileInfo to asyncResetAlwaysBlocks
Always blocks need three FileInfo (if, true, false) to show line numbers,
but initially, every always blocks only have one FileInfo (false).
RemoveReset adds the extra two FileInfo to sync always blocks,
so sync always blocks can have line numbers.
Async always blocks don't provide their only FileInfo, so there are no line numbers.
This commit gives async always block the extra FileInfo to show line numbers for them.
This code:
```scala
import chisel3._
import chisel3.stage._
import firrtl.CustomDefaultRegisterEmission
class Test extends Module with RequireAsyncReset {
val io = IO(new Bundle {
val in = Input(Bool())
val out = Output(Bool())
})
val valid = RegInit(false.B)
valid := io.in
io.out := valid
}
object Test extends App {
new ChiselStage().execute(Array(), Seq(
ChiselGeneratorAnnotation(() => new Test()),
CustomDefaultRegisterEmission(useInitAsPreset = false, disableRandomization = true)
))
}
```
will generate this Verilog:
```verilog
module Test(
input clock,
input reset,
input io_in,
output io_out
);
reg valid; // @[Playground.scala 10:22]
assign io_out = valid; // @[Playground.scala 12:10]
always @(posedge clock or posedge reset) begin
if (reset) begin // @[Playground.scala 10:22]
valid <= 1'h0; // @[Playground.scala 10:22]
end else begin
valid <= io_in; // @[Playground.scala 11:9]
end
end
endmodule
```
they have correct line numbers (10, 10, 11).
* Add test for async always block line numbers
* Add comment for review
|
|
* 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.
|
|
|
|
|
|
* Add compiler option (`-p`) to emit individual module protobufs
* Implement multi module combination when reading directory of protobufs
Co-authored-by: Jack Koenig <koenig@sifive.com>
|
|
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>
|
|
* Add new util "groupByIntoSeq"
* Restore annotation order when dedupping annotations
* Attribute annotations now deduplicate
* Implement doc string anno dedup
Co-authored-by: Jack Koenig <koenig@sifive.com>
|
|
* Add transform to deduplicate memory annotations
* Add annotation deduplication to Dedup stage
* ResolveAnnotationPaths and EliminateTargetPaths now invalidate the dedup annotations transform
* Verilog emitter now throws exception when memory annotations fail to dedup
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.
|
|
* Add Protocol Buffer emission export
This adds infrastructure and annotations that let a user emit a FIRRTL
circuit as a Protocol Buffer.
Fixes #1696.
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
* fixup! Add Protocol Buffer emission export
|
|
Add a compiler/emitter that can target minimal high form. This will
produce output that only has CHIRRTL constructs removed.
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>
|
|
* Fixes #2173
|
|
* bitWidth: add scaladoc
* smt: use existing bitWidth API
|
|
* Emit readwrite ports, if applicable
* Does not change VerilogMemDelays -> no effect on default flow
* Use more single-line declare-and-assign statements for mem wires
* Update error messages for too-complex memories in VerilogEmitter
* Run scalafmt on VerilogEmitter
|
|
This PR adds options for memory initialization inside or outside the
`ifndef SYNTHESIS` block.
|
|
Due to inlining of Boolean expressions, the following circuit is handled
directly by the VerilogEmitter:
input a: UInt<4>
input b: SInt<1>
output o: UInt<5>
o <= dshl(a, asUInt(cvt(b)))
Priot to this change, this could crash due to mishandling of cvt in the
logic to inject parentheses based on Verilog precedence rules.
This is a corner case, but similar bugs would drop up if we open up the
VerilogEmitter to more expression inlining.
|
|
|
|
This PR adds a new annotation allowing inline loading for memory files
in Verilog code.
|
|
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.
|
|
(#2091)
|
|
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
|
|
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>
|
|
* split big Emitter to submodules.
* fix all deprecated warning.
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.
|
