Overview
The attribute no_implicit_conditions asserts that the
implicit conditions of all interface methods called within the rule
must always be true, and therefore do not control its enabling. Only
the explicit rule predicate controls whether it is enabled or not. This
is statically verified by the compiler, and it will report an error if
there are implicit conditions which cannot always be true.
Attribute Syntax
(* no_implicit_conditions *) rule rulename conditions ; ... endrule
The no_implicit_conditions attribute immediately precedes the rule it is governing.
BSV Example
import FIFO :: *;
interface IfcCounter#(type t); method t readCounter; method Action setReset(t a); endinterface typedef Bit#(16) CounterType;
// Module counter using IfcCounter interface. It never contains 0. (* synthesize, always_ready = "readCounter", always_enabled= "readCounter" *) module counter (IfcCounter#(CounterType)); Reg#(CounterType) counter <- mkRegA(1); FIFO#(CounterType) valueFifo <- mkSizedFIFO(4);
/* Next rule increases the counter with each counter_clk rising edge if the maximum has not been reached */ (* no_implicit_conditions *) rule updateCounter; if (counter != '1) counter <= counter + 1; endrule
// Next rule resets the counter to a value stored in the valueFifo (* no_implicit_conditions *) rule resetCounter (counter == '1); counter <= valueFifo.first(); valueFifo.deq(); endrule // Output the counters value method CounterType readCounter; return counter; endmethod // Update the valueFifo method Action setReset(CounterType a); valueFifo.enq(a); endmethod endmodule
Compiler Output
Error: "counter.bsv", line 31, column 9: (G0005) The assertion `no_implict_conditions' failed for rule `resetCounter'
The compilation error is caused by the assertion no_implicit_conditions on the rule resetCounter.
This assertion will not be met for the rule because the rule has the
implicit condition in the FIFO module due to the fact that the deq method cannot be invoked if the fifo valueFifo is empty. Without the assertion no error would be produced.
|