bluespec.com Forum Index bluespec.com
Bluespec Forums
 
 FAQFAQ   SearchSearch   MemberlistMemberlist   UsergroupsUsergroups   RegisterRegister 
 ProfileProfile   Log in to check your private messagesLog in to check your private messages   Log inLog in 

conditional to satisfy no_implicit_conditions

 
Post new topic   Reply to topic    bluespec.com Forum Index -> Designing with BSV's Rules, Interfaces, ...
View previous topic :: View next topic  
Author Message
tspalink



Joined: 05 Nov 2015
Posts: 12

PostPosted: Sun Nov 22, 2015 3:36 pm    Post subject: conditional to satisfy no_implicit_conditions Reply with quote

Suppose I would like to create a wrapper around FIFO such that put() and get() for the wrapper are always ready, like so:

Code:
interface Buffer#(type a);
   (* always_ready *)
   interface Get#(Maybe#(a)) get;

   (* always_ready *)
   interface Put#(a) put;
endinterface


Which maybe I would then implement like this:

Code:
module mkBuffer(Buffer#(a) ifc) provisos (Bits#(a, as));
   FIFOF#(a) fifo <- mkSizedFIFOF(4);

   interface Get get;
      method ActionValue#(Maybe#(a)) get();
         if (fifo.notEmpty) begin
            let data = fifo.first();
            fifo.deq();
            return tagged Valid data;
         end
         else return Invalid;
      endmethod
   endinterface

   interface Put put;
      method Action put(a data);
         if (fifo.notFull) fifo.enq(data);
      endmethod
   endinterface
endmodule


It seems to me, that I should now be able to write a module like the following:

Code:
(* synthesize *)
module usebuffer();
   Buffer#(Bool) buffer <- mkBuffer();

   (* fire_when_enabled, no_implicit_conditions *)
   rule always_put;
      buffer.put.put(True);
   endrule
endmodule


However, verilog generation for this fails, with the complaint:

Quote:
The assertion `no_implicit_conditions' failed for rule `always_put'
During elaboration of rule `always_put' at


If I comment out the "no_implicit_conditions" attribute, it does complile and the schedule has this interesting tidbit:

Quote:
Rule: always_put
Predicate: (! buffer_fifo.notFull) || buffer_fifo.i_notFull
Blocking rules: (none)


Which is maybe interesting, as I assume that "i_notFull" is the implicit counterpart to "notFull".

QUESTION: Is there some reason these are not cancelling one another out?

BTW, a similar symmetrical thing happens if my rule is always_get instead of always_put.
Back to top
View user's profile Send private message
quark
Site Admin


Joined: 02 Nov 2007
Posts: 496

PostPosted: Tue Nov 24, 2015 4:31 pm    Post subject: Re: conditional to satisfy no_implicit_conditions Reply with quote

Adding an explicit condition doesn't change the fact that the 'enq' method still has an implicit condition. You need to instantiate a FIFO without implicit conditions on the methods. There are 'unguarded' versions of many of the FIFOs in the library. Try 'mkUGSizedFIFOF' (UG = unguarded).
Back to top
View user's profile Send private message
tspalink



Joined: 05 Nov 2015
Posts: 12

PostPosted: Thu Feb 11, 2016 2:00 pm    Post subject: Re: conditional to satisfy no_implicit_conditions Reply with quote

quark wrote:
Adding an explicit condition doesn't change the fact that the 'enq' method still has an implicit condition. You need to instantiate a FIFO without implicit conditions on the methods. There are 'unguarded' versions of many of the FIFOs in the library. Try 'mkUGSizedFIFOF' (UG = unguarded).


To follow up, as this is still causing me problems. More specifically, my compiler generated schedule description contains the following information about a key rule:

Quote:
Rule: do_all_the_stuffs
Predicate: True
Blocking rules: (none)


However, attempting to add the "no_implicit_conditions" attribute does not work -- I get the "The assertion `no_implicit_conditions' failed for rule" message.

How do I debug this? How do I figure out what the implicit conditions are for a rule?
Back to top
View user's profile Send private message
quark
Site Admin


Joined: 02 Nov 2007
Posts: 496

PostPosted: Sat Feb 13, 2016 2:34 pm    Post subject: Re: conditional to satisfy no_implicit_conditions Reply with quote

An alternative to using unguarded FIFOs would be to use the -aggressive-conditions flag. Are you using that when you compile?

I don't know why I didn't mention it in my first response. With the flag, if you have this code:
Code:
if (c)
  fifo1.enq(x);
else
  fifo2.enq(x);

then this action can only fire if both FIFOs are ready to accept data. BSC, in that case, will compute a conservative implicit condition for the action:
Code:
implicit condition = fifo1.notFull && fifo2.notFull

You can direct BSC to compute a better (but perhaps more complicated) condition by using the -aggressive-conditions flag:
Code:
implicit condition = (c ? fifo1.notFull : fifo2.notFull)

In your example, the default (conservative) condition would be 'fifo.notFull' and the aggressive condition would be True. So perhaps the answer to your original question is to use -aggressive-conditions, if you are not already.

To answer your latest question: Can you send an example that exhibits the problem that you're having? This sounds like a bug, which should be fixed.

There is a known bug that 'no_implicit_conditions' will fail if the rule or method is clocked by a gated clock. This is because BSC considers the gate to be part of the implicit condition. Is that what you are seeing? Are you using a gated clock?
Back to top
View user's profile Send private message
tspalink



Joined: 05 Nov 2015
Posts: 12

PostPosted: Mon Mar 21, 2016 7:20 pm    Post subject: Reply with quote

Maybe the issue is related to my using SyncFIFOCount, as opposed to simpler FIFO implementations.

Specific code example:

Code:
interface MyFifo;
   method ActionValue#(Maybe#(Bit#(1))) deq();
   method ActionValue#(Bool) enq(Bit#(1) data);
   method UInt#(5) count;
endinterface

module mkMyFifo(MyFifo ifc);
   Clock clock <- exposeCurrentClock();
   Reset reset <- exposeCurrentReset();

   SyncFIFOCountIfc#(Bit#(1), 16) sync_fifo <- mkSyncFIFOCount(
      clock,
      reset,
      clock);

   method ActionValue#(Maybe#(Bit#(1))) deq();
      let result = Invalid;
      if (sync_fifo.dNotEmpty) begin
         result = tagged Valid sync_fifo.first;
         sync_fifo.deq();
      end
      return result;
   endmethod

   method ActionValue#(Bool) enq(Bit#(1) data);
      let result = False;
      if (sync_fifo.sNotFull) begin
         sync_fifo.enq(data);
         result = True;
      end
      return result;
   endmethod

   method UInt#(5) count = sync_fifo.sCount;

endmodule

(* synthesize *)
module top(Empty ifc);

   MyFifo fifo <- mkMyFifo();

   Reg#(Maybe#(Bit#(1))) deq_value <- mkReg(Invalid);

   (* fire_when_enabled, no_implicit_conditions *)
   rule do_deq;
      let x <- fifo.deq();
      deq_value <= x;
   endrule

   (* fire_when_enabled, no_implicit_conditions *)
   rule do_enq;
      let x <- fifo.enq(1'b0);
   endrule

endmodule


Which fails when no_implicit_conditions is specified, despite the (once that requirement is commented out) schedule saying:

Quote:
=== Generated schedule for top ===

Rule schedule
-------------
Rule: do_deq
Predicate: True
Blocking rules: (none)

Rule: do_enq
Predicate: True
Blocking rules: (none)

Logical execution order: do_deq, do_enq

===================================


Note that my actual code requires the clock boundary crossing, and hence the use of SyncFIFOCount, but multiple clocks are not necessary to demonstrate the issue with the conditions, allowing for the above fairly simple example code.
Back to top
View user's profile Send private message
quark
Site Admin


Joined: 02 Nov 2007
Posts: 496

PostPosted: Sun Apr 10, 2016 3:42 am    Post subject: Reply with quote

What version of BSC are you using? When I remove the attributes, I see this schedule, which shows that the rules do have implicit conditions:
Code:
Rule: do_deq
Predicate: fifo_sync_fifo.dNotEmpty
Blocking rules: (none)
 
Rule: do_enq
Predicate: fifo_sync_fifo.sNotFull
Blocking rules: (none)
Back to top
View user's profile Send private message
tspalink



Joined: 05 Nov 2015
Posts: 12

PostPosted: Wed Apr 13, 2016 2:04 pm    Post subject: Reply with quote

Looks like I am using version 2014.07.A.

Could you explain why the schedule you are showing is correct? The code for do_deq() has a valid execution path for fifo_sync_fifo.dNotEmpty -- specifically, it should be setting deq_value to Invalid...
Back to top
View user's profile Send private message
quark
Site Admin


Joined: 02 Nov 2007
Posts: 496

PostPosted: Wed Apr 13, 2016 6:17 pm    Post subject: Reply with quote

Ah, I did not compile with the -aggressive-conditions flag. When I do that, I observe the behavior that you reported. It appears that the expression has not been reduced at the point where the check is being made, and the check is looking explicitly for "True" rather than accepting any expressions that reduce to True. That is a bug that will need to be fixed. Unfortunately, I don't know a workaround to give you.
Back to top
View user's profile Send private message
Display posts from previous:   
Post new topic   Reply to topic    bluespec.com Forum Index -> Designing with BSV's Rules, Interfaces, ... All times are GMT - 4 Hours
Page 1 of 1

 
Jump to:  
You cannot post new topics in this forum
You cannot reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot vote in polls in this forum
You can attach files in this forum
You can download files in this forum
bluespec.com topic RSS feed 


Powered by phpBB © 2001, 2005 phpBB Group
Protected by Anti-Spam ACP