Correct by Construction Verilog RTL: Rule summary

Follow on to original post at:
http://siliconbootcamp.blogspot.com/2012/11/writing-correct-by-construction-verilog.html

Naming Conventions
All signals have suffixes of the form:
 _[r,w].[c,d].{#} : choose 1 of the letters in each [] and concatenate to build suffix

[r,w]: r=>register, w=>wire
[c,d]: c=>control,  d=>datapath
{#} : Optional. Reflects register stage number
      Eg: pop_rc1, is a cycle  delayed from pop_rc
            pop_rc2, is 2 cycles delayed from pop_rc

RULES
1. In the combinatorial block :
   1.1 Only *_w* signals must be on LHS. (get values assigned to them)
   1.2 All signals must have a default assignment, before the case
   1.3 Control signals that pulse must have a default assignment of 0
   1.4 Signals that hold their value, must have a default assignment to their registered equivalent.
       *_w* = *_r* ;
       Eg: push_pending_wc = push_pending_rc ;
   1.5 Conditional statements can use *_w* or *_r* signals.
   1.6 A conditional statement cannot use a signal in a its conditional expression and also have an assignment to it.
       Eg: if ( eom_detected_wc & fifo_full_rc )
       eom_detected_wc = 0;
       (this will create a combinational loop).

2. In the clocked block:
   2.1 All Control signals must have a reset value.,
   2.2 All Datapath signals need not have a reset value, like those registers in the middle of a pipeline.
   2.3 Only *_r* signals must be on LHS.
   2.4 Signal assignments will be of the form *_r* <= *_w* ;

GUIDELINES
1. In the combinatorial block :
   1.1 Generally datapath signals will "hold" values, whereas control signals will not.
   1.2 If a default assignment is missed, the synthesis tool will warn you about latches begin inferred.
  

Writing Correct by Construction Verilog RTL

Writing Correct by Construction Verilog RTL

Here is how I framed the problem, Lets say I have captured my solution to a problem in pseudo-code and I want to translate it into synthesizable RTL. 

The rules for writing synthesizable verilog RTL are fairly simple. The main ones are:

• Infer registers with non-blocking assigns (<=) in clocked always blocks.
• The same register may not be assigned to in multiple blocks
• Combinational logic can be described either in always @* blocks or using continuous assigns.

So obviously, there are a multitude of ways in which RTL can be written. I have seen everything from a single always block, to conditional assigns that run into paragraphs. Mish-mash of code that is sometimes incomprehensible to even the person who wrote it. While all kinds of slick methodologies have come and gone in other areas of chip design, for the most part RTL is still written the same way it was 20 years ago.

Very often it isn't design, but really design by simulation. Write stuff, simulate, make changes, repeat.
You wouldn't write an english essay by stringing together a bunch of words and then running the grammar and spell checker. You would be surprised at how often RTL code is written in this fashion though.

My approach is this:  Make every attempt at writing correct by construction RTL, this exercise will force you to give the necessary thought upfront, and producing robust code after fewer debug-recode cycles. Enough preachy talk, onto the meat of my article, outlining the framework I use. (this is for a non-pipelined design)

Establish Naming convention for rtl signals to clearly distinguish between registers and combinational wires.

Control wires : _wc  suffix (wire control)

Control registers: _rc suffix  (reg control)

Data wires: _wd suffix (wire data)

Data registers: _rd suffix (reg data)

FSM state register: fsm_cs (current state), fsm_nxt (next state)

State machine described in an always @* combinational block.

The magic or algorithm is implemented here.

This always @* block will have the following properties. System Verilog equivalent is an always_comb block.

Starts with default assignments, for all *_wc, *_rc, *_wd, *_rd signals.

Default assignment for fsm_nxt  =  fsm_cs ;

All assignments will be to _w* signals not _r* (registered signals)

Most commonly:

All _wc , control signals are assigned a default of 0. (pulsed control).

All _wd, data signals are assigned to the corresponding _rd signal (hold data value)

State machine logic, using case( fsm_cs ), within each branch of the case assign fsm_nxt for a state transition, else by default you will remain in that state.

To avoid combinatorial loops ,the if conditionals in this always block should use _rc or _rd signals.

If _wc or _ wd signals are being used take a closer look. Ideally they are only being used to improve the readability of the code, that is combinatorial expressions built up within a single case select.

Inferring registers in clocked always block

In reset section

•  all _rc control signals will be assigned 0. *_rc <= 0
• Usually, no assignments within for *_rd data signals.
• fsm_cs <=  your_start_state

Outside reset:

all _rd  & _rc signals will be assigned to their corresponding _wd & _wc  signals. *_rd <= *_wd ; *_rc <= *_wc ;

and next state assignment for state machine:  fsm_cs <= fsm_nxt ;

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

Example:

module data_splitter ( /*AUTOARG*/

   // Outputs
   idata_pop, odata1_push, odata1, odata2_pop, odata2,
   // Inputs
   clk, rst, stagecnt, num, idata_rdy, idata, odata1_rdy, odata2_rdy
   );
 

   //System clk and reset

   input clk ;
   input rst ;
 

   //Splitter parameters

   input [31:0] stagecnt ;
   input [31:0] num ;

   //Read Data from fifo interface

   input idata_rdy ;
   input [31:0] idata ;
   output               idata_pop ;

   //Output data interface

   output               odata1_push;
   input odata1_rdy;
   output [31:0] odata1;
   output               odata2_push;
   input odata2_rdy;
   output [31:0] odata2;  

   //zWidth [31:0] data ;

   //zReg
   reg [31:0] idata_pop_rc ;
   reg  chan1_cnt_rc ;
   reg [31:0] idata_pop_wc ;
   reg [31:0] odata1_push_wc ;
   reg  chan1_cnt_wc ;
   reg [31:0] idata_rd ;
   reg [31:0] odata1_rd ;
   reg [31:0] odata2_rd ;
   reg [31:0] data_rd ;
   reg [31:0] data_wd ;
   //   

  reg [1:0] fsm_cs, fsm_nxt ; 

  parameter s0=1,s1=2,s2=2;

//Inferring registers in clocked always block

   always @(posedge clk)

     if (rst)
       begin
                         //zClkReset
                         idata_pop_rc <= 0 ;
                         chan1_cnt_rc <= 0 ;

                          fsm_cs <= s0 ;

                       //zEnd
       end

     else

       begin

                        //zClkAssign

                       idata_pop_rc <=  idata_pop_wc ;

                       chan1_cnt_rc <=  chan1_cnt_wc ;
                       data_rd <=  data_wd ;

                       fsm_cs <= fsm_nxt ;

                        //zEnd

       end

 

//State machine described in an always @* combinational block. 
  //1. Is data rdy in source, yes then pop

  //2. Push stagecnt times to channel1, unless not rdy
    always @*
     begin

              //Default assignments to  *_wc and *_wd signals.

                 fsm_nxt = fsm_cs ;

               idata_pop_wc =  0 ;
                odata1_push_wc =  0 ;
                chan1_cnt_wc =  0 ;
                data_wd =  data_rd ;
               //zEnd
               

                case(fsm_cs)

                    s0:begin
                       if ( idata_rdy )
                         begin
                                       idata_pop_wc = 1;
                                       fsm_nxt = s1 ;

                         end

                    end
                  
                    s1:begin
                       if ( idata_pop_rc )
                         data_wd = idata;

                       if ( chan1_cnt_rc < stagecnt && odata1_rdy )

                         begin
                                       odata1_push_wc = 1;
                                       fsm_nxt = s2 ;
                         end
                    end
 
                    s2:begin
                       odata1 = data_rd ;
                       chan1_cnt_wc = chan1_cnt_rc + 1 ;
                       fsm_nxt = s0 ;
                    end
                endcase // case (fsm_cs) 
     end
  endmodule // data_splitter

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

FAQ:

Q. Even *_wc and *_wd signals are declared as registers, aren't they wires  ?

A.  The context in which the variables are assigned determines if registers will be inferred. They are declared as registers so that they can be assigned in the always @* block (which is combinational).

Q. In the example code, what is the //zClk/Wire stuff ?

A. Its a little pre-processor I wrote to fill in some the declarations and default assignments auto-magically. If there is sufficient interest I'll send it up to github or something.

Q. What does the example code do ?

A. Yeah, should come up with a better example rather than snipping it from an existing code base to just show the different sections. Again if there is enough interest I'll put up an example with a testbench.

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