- 
                Notifications
    You must be signed in to change notification settings 
- Fork 11
          Add ReqResp Protocol
          #83
        
          New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
          
     Open
      
      
            lmbollen
  wants to merge
  1
  commit into
  main
  
    
      
        
          
  
    
      Choose a base branch
      
     
    
      
        
      
      
        
          
          
        
        
          
            
              
              
              
  
           
        
        
          
            
              
              
           
        
       
     
  
        
          
            
          
            
          
        
       
    
      
from
req-resp-protocol
  
      
      
   
  
    
  
  
  
 
  
      
    base: main
Could not load branches
            
              
  
    Branch not found: {{ refName }}
  
            
                
      Loading
              
            Could not load tags
            
            
              Nothing to show
            
              
  
            
                
      Loading
              
            Are you sure you want to change the base?
            Some commits from the old base branch may be removed from the timeline,
            and old review comments may become outdated.
          
          
  
     Open
                    Changes from all commits
      Commits
    
    
  File filter
Filter by extension
Conversations
          Failed to load comments.   
        
        
          
      Loading
        
  Jump to
        
          Jump to file
        
      
      
          Failed to load files.   
        
        
          
      Loading
        
  Diff view
Diff view
There are no files selected for viewing
  
    
      This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
      Learn more about bidirectional Unicode characters
    
  
  
    
              
  
    
      This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
      Learn more about bidirectional Unicode characters
    
  
  
    
              | Original file line number | Diff line number | Diff line change | ||||
|---|---|---|---|---|---|---|
| @@ -0,0 +1,53 @@ | ||||||
| {- | | ||||||
| Simplest possible protocol for request-response communication. | ||||||
|  | ||||||
| The forward channel channel has type @Signal dom (Maybe req)@ and is used to send requests. | ||||||
| The backward channel has type @Signal dom (Maybe resp)@ and is used to send responses. | ||||||
|  | ||||||
| The protocol must obey the following rules: | ||||||
| * When the forward channel is @Just a@, it must not change until the transaction is completed. | ||||||
| * The forward channel can not depend on the backward channel. | ||||||
| * When the forward channel is @Nothing@, the backward channel may be undefined. | ||||||
|  | ||||||
| This protocol can not be pipelined, for pipelined request-response communication see `Protocols.BiDf`. | ||||||
| -} | ||||||
| module Protocols.ReqResp where | ||||||
|  | ||||||
| import qualified Clash.Prelude as C | ||||||
| import Data.Kind (Type) | ||||||
| import Protocols | ||||||
| import Protocols.Internal.Classes | ||||||
| import Prelude as P | ||||||
|  | ||||||
| {- | | ||||||
| Simplest possible protocol for request-response communication. | ||||||
|  | ||||||
| The forward channel channel has type @Signal dom (Maybe req)@ and is used to send requests. | ||||||
| The backward channel has type @Signal dom (Maybe resp)@ and is used to send responses. | ||||||
|  | ||||||
| The protocol must obey the following rules: | ||||||
| * When the forward channel is @Just a@, it must not change until the transaction is completed. | ||||||
| * The forward channel can not depend on the backward channel. | ||||||
| * When the forward channel is @Nothing@, the backward channel may be undefined. | ||||||
| -} | ||||||
| data ReqResp (dom :: C.Domain) (req :: Type) (resp :: Type) | ||||||
|  | ||||||
| instance Protocol (ReqResp dom req resp) where | ||||||
| -- \| Forward channel for ReqResp protocol: | ||||||
| There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 
        Suggested change
       
 What happened here? | ||||||
| type Fwd (ReqResp dom req resp) = C.Signal dom (Maybe req) | ||||||
|  | ||||||
| -- \| Backward channel for ReqResp protocol: | ||||||
| type Bwd (ReqResp dom req resp) = C.Signal dom (Maybe resp) | ||||||
|  | ||||||
| instance IdleCircuit (ReqResp dom req resp) where | ||||||
| idleFwd _ = pure Nothing | ||||||
| idleBwd _ = pure Nothing | ||||||
|  | ||||||
| {- | Force a @Nothing@ on the backward channel and @Nothing@ on the forward | ||||||
| channel if reset is asserted. | ||||||
| -} | ||||||
| forceResetSanity :: | ||||||
| forall dom req resp. | ||||||
| (C.HiddenReset dom) => | ||||||
| Circuit (ReqResp dom req resp) (ReqResp dom req resp) | ||||||
| forceResetSanity = forceResetSanityGeneric | ||||||
  Add this suggestion to a batch that can be applied as a single commit.
  This suggestion is invalid because no changes were made to the code.
  Suggestions cannot be applied while the pull request is closed.
  Suggestions cannot be applied while viewing a subset of changes.
  Only one suggestion per line can be applied in a batch.
  Add this suggestion to a batch that can be applied as a single commit.
  Applying suggestions on deleted lines is not supported.
  You must change the existing code in this line in order to create a valid suggestion.
  Outdated suggestions cannot be applied.
  This suggestion has been applied or marked resolved.
  Suggestions cannot be applied from pending reviews.
  Suggestions cannot be applied on multi-line comments.
  Suggestions cannot be applied while the pull request is queued to merge.
  Suggestion cannot be applied right now. Please check back later.
  
    
  
    
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This implies that this protocol can not be pipelined. We can relax this constraint and do two versions of ReqResp (pipelined and not pipelined). Or we can use DSignal to enforce different pipeline depths on the type level.
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why couldn't it be pipelined? I think you can write a component that handles this. Essentially store forward in a register. Send contents of the register to the sink. When the sink responds either send it directly to the source and clear the register or put the response in a register as well. The main problem is that you no longer can have full throughput between source and sink.
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Perhaps we should then just have
a kind of Axi4LiteLite
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Enforcing pipeline depth on the type level seems to be more useful than just a blanket declaration "you can send stuff, which we call a request, and you can receive stuff, which we call a response", which seems to be what Christiaans
ReqRespPipelinedis.Avalon Stream does pre-negotiated pipelining. You can configure that when you drop ready, you can still receive data in the next n cycles, so the pipeline of the sender can empty. Constructions like that. Maybe it can serve as inspiration.
Alternatively, we can tackle pipelining in a different PR.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't think separating the channels is a good idea as it directly contradicts the purpose of
circuit-notation(Combining forward and backward channels in a single binder).How about separating request acknowledgement and response timing?:
Here the
Boolwould indicate a request acknowledgement andMaybe respcould beJust resplater.Combinatorial circuits could then return
(isJust resp, resp).Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
How would you still be able to tell which response corresponds to which request?Never mind, that's not a very clever comment.
It does seem to me that you need a whole bunch more protocol specification for two pipelined implementations to be able to communicate. Where's the guarantees? I want to know I can still get rid of all the data currently in my pipeline; if I can't get a guarantee I can deliver it all, I will need buffers to deal with the case that I cannot, or I need to be able to stall the whole pipeline at any random moment, and we're back at square one.
Personally, I think a "simple" protocol that doesn't allow pipelining at the protocol level¹ and a separate more complex protocol that tackles pipelining in a neat and efficient way is a perfectly fine solution. This PR can be the simple variant.
¹ As Rowan indicates above, you can still accomodate pipelining with constructions like skid buffers, but the protocol would be oblivious to this and it would in general be less efficient than pipelining being part of the protocol.