aboutsummaryrefslogtreecommitdiff
path: root/src/main/resources/META-INF
AgeCommit message (Collapse)Author
2021-03-27Add NoConstantPropagationAnnotation to disable constatnt propagation (#2150)Jiuyang Liu
* add --no-constant-propagation to disable constant propagation * add test * deprecate DisableFold. Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
2020-06-23Basic 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-07Make ClockListAnnotation a RegisteredTransformSchuyler Eldridge
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@ibm.com>
2018-11-07Make InlineInstances a RegisteredTransformSchuyler Eldridge
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@ibm.com>
2018-11-07Make CheckCombLoops a RegisteredTransformSchuyler Eldridge
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@ibm.com>
2018-11-07Make DeadCodeElimination a RegisteredTransformSchuyler Eldridge
Signed-off-by: Schuyler Eldridge <schuyler.eldridge@ibm.com>
2018-11-07Add MemLibOptions RegisteredLibrarySchuyler 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>