| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-06-23 | Basic model checking API (#1653) | Tom Alcorn | |
| * Add assume, assert, cover statements * Assert submodule assumptions * Add warning when removing verification statements * Remove System Verilog behaviour emitter warning * Add option to disable AssertSubmoduleAssumptions * Document verification statements in the spec The syntax for the new statements is assert(clk, cond, en, msg) assume(clk, cond, en, msg) cover(clk, cond, en, msg) With assert as a representative example, the semantics is as follows: `clk` is the clock, `cond` is the expression being asserted, `en` is the enable signal (if `en` is low then the assert is not checked) and `msg` is a string message intended to be reported as an error message by the model checker if the assertion fails. In the Verilog emitter, the new statements are handled by a new `formals` map, which groups the statements by clock domain. All model checking statements are then emitted within the context of an `ifdef FORMAL` block, which allows model checking tools (like Symbiyosys) to utilize the statements while keeping them out of synthesis flows. Co-authored-by: Albert Magyar <albert.magyar@gmail.com> | |||
| 2018-11-07 | Make ClockListAnnotation a RegisteredTransform | Schuyler Eldridge | |
| Signed-off-by: Schuyler Eldridge <schuyler.eldridge@ibm.com> | |||
| 2018-11-07 | Make InlineInstances a RegisteredTransform | Schuyler Eldridge | |
| Signed-off-by: Schuyler Eldridge <schuyler.eldridge@ibm.com> | |||
| 2018-11-07 | Make CheckCombLoops a RegisteredTransform | Schuyler Eldridge | |
| Signed-off-by: Schuyler Eldridge <schuyler.eldridge@ibm.com> | |||
| 2018-11-07 | Make DeadCodeElimination a RegisteredTransform | Schuyler Eldridge | |
| Signed-off-by: Schuyler Eldridge <schuyler.eldridge@ibm.com> | |||
| 2018-11-07 | Add MemLibOptions RegisteredLibrary | Schuyler Eldridge | |
| This shows an example of using a RegisteredLibrary, with the appropriate META-INF ServiceLoader entry, that adds options from the InferReadWrite and ReplSeqMem transforms. Signed-off-by: Schuyler Eldridge <schuyler.eldridge@ibm.com> | |||
| 2016-11-04 | Cleanup license at top of every file (#364) | Jack Koenig | |
| Replace with more sensible comment to see LICENSE rather than including the whole license in every file | |||
| 2016-08-01 | Change default log level to warn | Jack Koenig | |
| 2016-04-19 | Change pass name printing to info. Print pass runtime. | jackkoenig | |
| Change default print level to info. | |||
| 2016-02-22 | Change default log-level to warn, users should change manually if so desired | Jack | |
| 2016-02-09 | Added license to FIRRTL files | azidar | |
| 2016-01-16 | Import a logging library so we don't reinvent the wheel and have implicits ↵ | ducky | |
| flying around everywhere | |||
