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.
  

Xilinx Coregen and EDK

 Adding Xilinx Coregen macros to EDK designs

1. Generate coregen macro, enable generation of .v files. The netlist will be a .ngc file

2. Look at .v file, will have a synthesis translate_off  and on directive around the behavioral simulation model

3. Synthesis will take any module with an io port definition and treat it as a blackbox.

   eg black box definition:

             module foo ( clk , rst, datain, dataout) ;

                input clk, rst;

                input datain ;

                output dataout;

             //If you want to include behavioral simulation code here 

             //do so within synthesis translate off and on

             // XST and synplicity should recognize this

             //synthesis translate_offf

              ....

              ....

              ....

             //synthesis translate_on

 

             endmodule

4. Synthesize using XST. This will create an .ngc file

5. In pcores/<ip_name>/data directory create a .bbd file

          This is just a comma separated list of the coregen.ngc files

          eg: cam_v6_1.ngc, srlfifo39.ngc

6. In the .mpd file add

          OPTION STYLE = MIX

          OPTION RUN_NGCBUILD = TRUE

7. Create pcores/<ip_name>/netlist directory and copy the .ngc files listed in step (5) here.

8. Invoke EDK build flow.

 

Xilinx commands and Filetypes

Xilinx commands and filetypes One-pager

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

Xilinx File Types 

.ngc : Netlist file

.ngo : Similar to .ngc, output of Coregen, EDIF2NGD

 

.ncd : Mapped, placed , routed file

 

.ucf : User constraint file, read by NGDBUILD .

 

.pcf : Physical constraints file, output by MAP and used by PAR.

 

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

NGCBUILD: Merges multiple .ngc (synthesized netlist files) into a single .ngc file. Useful for chipscope core insertion.

syntax:

ngcbuild -i <top_level_input_file>.ngc  <output_file>.ngc  

Options:

-sd : specify source directories? if all .ngc files not in the same directory as <top_level_input_file>.ngc

 

NGDBUILD: Reads (multiple) .ngc files to create and single .ngd file. This file is the entry point for MAP,PAR.

 

MAP: Reads .ngd file, output mapped .ncd file and optionally .pcf files.

 

PAR: Place and route, reads mapped .ncd file and outputs routed .ncd file

 

TRCE: Trace, reads .ncd file and what else.

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

Chipscope Core Inserter

Once you have .cdc file, can run inserter from the command line.

syntax:

inserter -insert <file.cdc> <input_file>.ngc <output_file>.ngc

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

Example windows script:

 

rem Clean up the results directory

rmdir /S /Q results

mkdir results

echo 'Synthesizing HDL example design with XST';

xst -ifn xst.scr

move xilinx_pci_exp_ep.ngc .\results\endpoint_blk_plus_v1_9_top.ngc

cd results

echo 'Running ngdbuild'

rem   ngdbuild -verbose -uc ..\xilinx_pci_exp_blk_plus_1_lane_ep_xc5vlx50t-ff1136-1.ucf endpoint_blk_plus_v1_9_top.ngc -sd ..\..\..\..\..\

ngdbuild -verbose -uc ..\xupv5-lx110t_pcie_x1_plus.ucf endpoint_blk_plus_v1_9_top.ngc -sd ..\..\..\..\

 

echo 'Running map'

map -timing -ol high -xe c -pr b -o mapped.ncd endpoint_blk_plus_v1_9_top.ngd mapped.pcf

echo 'Running par'

par -ol high -xe c -w mapped.ncd routed.ncd mapped.pcf

echo 'Running trce'

trce -u -v 100 routed.ncd mapped.pcf

echo 'Running design through netgen'

netgen -sim -ofmt verilog -ne -w -tm xilinx_pci_exp_ep -sdf_path ..\..\implement\results routed.ncd 

echo 'Running design through bitgen'

bitgen -w routed.ncd

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

command to create ace file.

impact -batch pcie_ace.cmd

pcie_ace.cmd >>

setMode -acecf

addCollection -name "ML509"

addDesign -version 6 -name "cfg4"

addDeviceChain -index 0

setCurrentDesign -version 6

setCurrentDeviceChain -index 0

addDevice -p 1 -file "./pcie_dma_top.bit"

generate -active ML509

quit

<< 

From xapp859 for ml505

bitgen -g ConfigRate:20 <file>

Xilinx EDK and Synplify

 Using Synplify to synthesize pcore logic in EDK

 

Pcores are user defined custom cores to hook up to to a Microblaze or PPC based embedded system in Xilinx FPGAs. Synplify often produces better results than XST (the Xilinx synthesis tool) both in terms of timing and area. 

1. Generate pcore, enable the generate in verilog option

2. This will create user_logic.v

 

3. Create a synplify project file for user_logic.v and all modules underneath it.

4. In synplify go to File->New, then select new project file. 

5. Add user_logic.v and other modules referenced by it. Synplify will also treat modules with only IO declaration as a blackbox. These blackbox modules will be resolved in the ngcbuild step.

6. Go under implementation options, select the right xilinx part no.

7. Most important under implementation options, disable automatic IO insertion.

8. Run in synplify

9. Synplify generates an .edf file

10. Copy to pcores<ip_name>/netlist directory and run edif2ngd user_logic.edf, rename output from user_logic.ngo to user_logic.ngc.

11. In pcores/hdl/verilog, edit user_logic.v to remove all code between the IO declaration and endmodule. Synthesis will take any module with an io port definition and treat it as a blackbox.

            eg black box definition:

             module foo ( clk , rst, datain, dataout) ;

                input clk, rst;

                input datain ;

                output dataout;

  

             //If you want to include behavioral simulation code here 

             //do so within synthesis translate off and on

             // XST and synplicity should recognize this

             //synthesis translate_offf

              ....

              ....

              ....

             //synthesis translate_on

             endmodule         

12. Edit the pcores/<ip_name>/data/.pao  file , if need be , it should only reference user_logic.v (in addition to the the other edk libraries and vhdl wrapper).

13. In pcores/<ip_name>/data directory create a .bbd file

          This is just a comma separated list of the coregen.ngc files, with a first line saying Files

          eg bbd file:

 

          # This is a comment, must have Files keyword below

          Files

          srlfifo39.ngc , user_logic.ngc 

14. In the .mpd file add

          OPTION STYLE = MIX

          OPTION RUN_NGCBUILD = TRUE

15. Invoke EDK build flow. 

16. If it fails MAP , it could be because synplify has not optimized away unconnected inputs. Create dummy connection to the problem LUTs. Rerun synplify.

17. Complete build.

This has been tested on the sample ml509_dpi  design with fifo read logic.

It ran into a problem with MAP. Issue was traced to the Intr_Event not being driven, drove it with a dummy register and then it worked.

(should try a simply tie off and see)

Sample synplify project file:

#-- Synplicity, Inc.

#-- Version C-2009.06-SP1

#-- Written on Wed Apr 14 12:30:27 2010

 

#project files

add_file -verilog "./srlfifo39.v"

add_file -verilog "./tag_data_splitter.v"

add_file -verilog "./tag_parser.v"

add_file -verilog "./user_logic.v"

 

#implementation: "rev_1"

impl -add rev_1 -type fpga

#device options

set_option -technology Virtex5

set_option -part XC5VLX110T

set_option -package FF1136

set_option -speed_grade -1

set_option -part_companion ""

 

#compilation/mapping options

set_option -use_fsm_explorer 0

set_option -top_module "user_logic"

 

# sequential_optimization_options

set_option -symbolic_fsm_compiler 1

 

# Compiler Options

set_option -compiler_compatible 0

set_option -resource_sharing 1

 

# mapper_options

set_option -frequency auto

set_option -write_verilog 0

set_option -write_vhdl 0

 

# Xilinx Virtex2

set_option -run_prop_extract 1

set_option -maxfan 10000

set_option -disable_io_insertion 1

set_option -pipe 1

set_option -update_models_cp 0

set_option -retiming 0

set_option -no_sequential_opt 0

set_option -fixgatedclocks 3

set_option -fixgeneratedclocks 3

# Xilinx Virtex5

set_option -enable_prepacking 1 

#VIF options

set_option -write_vif 1

#automatic place and route (vendor) options

set_option -write_apr_constraint 1

 

#set result format/file last

project -result_file "./rev_1/user_logic.edf"

#

#implementation attributes

set_option -vlog_std v2001

set_option -project_relative_includes 1

impl -active "rev_1"

 

 

 

 

 

 

 

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.

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