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.