+cd tests/ice40 && bash run-test.sh $(SEEDOPT)
+cd tests/rpc && bash run-test.sh
+cd tests/xilinx && bash run-test.sh $(SEEDOPT)
- +cd tests/xilinx_ug901 && bash run-test.sh $(SEEDOPT)
@echo ""
@echo " Passed \"make test\"."
@echo ""
+++ /dev/null
-// Asymmetric port RAM\r
-// Read Wider than Write. Read Statement in loop\r
-//asym_ram_sdp_read_wider.v\r
-\r
-module asym_ram_sdp_read_wider (clkA, clkB, enaA, weA, enaB, addrA, addrB, diA, doB);\r
-parameter WIDTHA = 4;\r
-parameter SIZEA = 1024;\r
-parameter ADDRWIDTHA = 10;\r
-\r
-parameter WIDTHB = 16;\r
-parameter SIZEB = 256;\r
-parameter ADDRWIDTHB = 8;\r
-input clkA;\r
-input clkB;\r
-input weA;\r
-input enaA, enaB;\r
-input [ADDRWIDTHA-1:0] addrA;\r
-input [ADDRWIDTHB-1:0] addrB;\r
-input [WIDTHA-1:0] diA;\r
-output [WIDTHB-1:0] doB;\r
-`define max(a,b) {(a) > (b) ? (a) : (b)}\r
-`define min(a,b) {(a) < (b) ? (a) : (b)}\r
-\r
-function integer log2;\r
-input integer value;\r
-reg [31:0] shifted;\r
-integer res;\r
-begin\r
- if (value < 2)\r
- log2 = value;\r
- else\r
- begin\r
- shifted = value-1;\r
- for (res=0; shifted>0; res=res+1)\r
- shifted = shifted>>1;\r
- log2 = res;\r
- end\r
-end\r
-endfunction\r
-\r
-localparam maxSIZE = `max(SIZEA, SIZEB);\r
-localparam maxWIDTH = `max(WIDTHA, WIDTHB);\r
-localparam minWIDTH = `min(WIDTHA, WIDTHB);\r
-\r
-localparam RATIO = maxWIDTH / minWIDTH;\r
-localparam log2RATIO = log2(RATIO);\r
-\r
-reg [minWIDTH-1:0] RAM [0:maxSIZE-1];\r
-reg [WIDTHB-1:0] readB;\r
-\r
-always @(posedge clkA)\r
-begin\r
- if (enaA) begin \r
- if (weA)\r
- RAM[addrA] <= diA;\r
- end \r
-end\r
-\r
-\r
-always @(posedge clkB)\r
-begin : ramread\r
- integer i;\r
- reg [log2RATIO-1:0] lsbaddr;\r
- if (enaB) begin\r
- for (i = 0; i < RATIO; i = i+1) begin \r
- lsbaddr = i;\r
- readB[(i+1)*minWIDTH-1 -: minWIDTH] <= RAM[{addrB, lsbaddr}];\r
- end\r
- end\r
-end\r
-assign doB = readB;\r
-\r
-endmodule\r
-\r
+++ /dev/null
-read_verilog asym_ram_sdp_read_wider.v
-hierarchy -top asym_ram_sdp_read_wider
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd asym_ram_sdp_read_wider
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 2 t:BUFG
-select -assert-count 1 t:LUT2
-select -assert-count 4 t:RAMB18E1
-
-select -assert-none t:BUFG t:LUT2 t:RAMB18E1 %% t:* %D
+++ /dev/null
-// Asymmetric port RAM\r
-// Write wider than Read. Write Statement in a loop.\r
-// asym_ram_sdp_write_wider.v\r
-\r
-module asym_ram_sdp_write_wider (clkA, clkB, weA, enaA, enaB, addrA, addrB, diA, doB);\r
-parameter WIDTHB = 4;\r
-//Default parameters were changed because of slow test\r
-//parameter SIZEB = 1024;\r
-//parameter ADDRWIDTHB = 10;\r
-parameter SIZEB = 256;\r
-parameter ADDRWIDTHB = 8;\r
-\r
-//parameter WIDTHA = 16;\r
-parameter WIDTHA = 8;\r
-parameter SIZEA = 256;\r
-parameter ADDRWIDTHA = 8;\r
-input clkA;\r
-input clkB;\r
-input weA;\r
-input enaA, enaB;\r
-input [ADDRWIDTHA-1:0] addrA;\r
-input [ADDRWIDTHB-1:0] addrB;\r
-input [WIDTHA-1:0] diA;\r
-output [WIDTHB-1:0] doB;\r
-`define max(a,b) {(a) > (b) ? (a) : (b)}\r
-`define min(a,b) {(a) < (b) ? (a) : (b)}\r
-\r
-function integer log2;\r
-input integer value;\r
-reg [31:0] shifted;\r
-integer res;\r
-begin\r
- if (value < 2)\r
- log2 = value;\r
- else\r
- begin\r
- shifted = value-1;\r
- for (res=0; shifted>0; res=res+1)\r
- shifted = shifted>>1;\r
- log2 = res;\r
- end\r
-end\r
-endfunction\r
-\r
-localparam maxSIZE = `max(SIZEA, SIZEB);\r
-localparam maxWIDTH = `max(WIDTHA, WIDTHB);\r
-localparam minWIDTH = `min(WIDTHA, WIDTHB);\r
-\r
-localparam RATIO = maxWIDTH / minWIDTH;\r
-localparam log2RATIO = log2(RATIO);\r
-\r
-reg [minWIDTH-1:0] RAM [0:maxSIZE-1];\r
-reg [WIDTHB-1:0] readB;\r
-\r
-always @(posedge clkB) begin\r
- if (enaB) begin\r
- readB <= RAM[addrB];\r
- end\r
-end\r
-assign doB = readB;\r
-\r
-always @(posedge clkA)\r
-begin : ramwrite\r
- integer i;\r
- reg [log2RATIO-1:0] lsbaddr;\r
- for (i=0; i< RATIO; i= i+ 1) begin : write1\r
- lsbaddr = i;\r
- if (enaA) begin\r
- if (weA)\r
- RAM[{addrA, lsbaddr}] <= diA[(i+1)*minWIDTH-1 -: minWIDTH];\r
- end\r
- end\r
-end\r
-\r
-endmodule\r
+++ /dev/null
-read_verilog asym_ram_sdp_write_wider.v
-hierarchy -top asym_ram_sdp_write_wider
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd asym_ram_sdp_write_wider
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 2 t:BUFG
-select -assert-count 1028 t:FDRE
-select -assert-count 170 t:LUT2
-select -assert-count 6 t:LUT3
-select -assert-count 518 t:LUT4
-select -assert-count 10 t:LUT5
-select -assert-count 484 t:LUT6
-select -assert-count 157 t:MUXF7
-select -assert-count 3 t:MUXF8
-
-#RRAM128X1D will be synthesized in case when the parameter WIDTHA=4
-#select -assert-count 8 t:RAM128X1D
-
-select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXF7 t:MUXF8 %% t:* %D
+++ /dev/null
-// Asymetric RAM - TDP \r
-// READ_FIRST MODE.\r
-// asym_ram_tdp_read_first.v\r
-\r
-\r
-module asym_ram_tdp_read_first (clkA, clkB, enaA, weA, enaB, weB, addrA, addrB, diA, doA, diB, doB);\r
-parameter WIDTHB = 4;\r
-parameter SIZEB = 1024;\r
-parameter ADDRWIDTHB = 10;\r
-parameter WIDTHA = 16;\r
-parameter SIZEA = 256;\r
-parameter ADDRWIDTHA = 8;\r
-input clkA;\r
-input clkB;\r
-input weA, weB;\r
-input enaA, enaB;\r
-\r
-input [ADDRWIDTHA-1:0] addrA;\r
-input [ADDRWIDTHB-1:0] addrB;\r
-input [WIDTHA-1:0] diA;\r
-input [WIDTHB-1:0] diB;\r
-\r
-output [WIDTHA-1:0] doA;\r
-output [WIDTHB-1:0] doB;\r
-\r
-`define max(a,b) {(a) > (b) ? (a) : (b)}\r
-`define min(a,b) {(a) < (b) ? (a) : (b)}\r
-\r
-function integer log2;\r
-input integer value;\r
-reg [31:0] shifted;\r
-integer res;\r
-begin\r
- if (value < 2)\r
- log2 = value;\r
- else\r
- begin\r
- shifted = value-1;\r
- for (res=0; shifted>0; res=res+1)\r
- shifted = shifted>>1;\r
- log2 = res;\r
- end\r
-end\r
-endfunction\r
-\r
-localparam maxSIZE = `max(SIZEA, SIZEB);\r
-localparam maxWIDTH = `max(WIDTHA, WIDTHB);\r
-localparam minWIDTH = `min(WIDTHA, WIDTHB);\r
-\r
-localparam RATIO = maxWIDTH / minWIDTH;\r
-localparam log2RATIO = log2(RATIO);\r
-\r
-reg [minWIDTH-1:0] RAM [0:maxSIZE-1];\r
-reg [WIDTHA-1:0] readA;\r
-reg [WIDTHB-1:0] readB;\r
-\r
-always @(posedge clkB)\r
-begin\r
- if (enaB) begin\r
- readB <= RAM[addrB] ;\r
- if (weB)\r
- RAM[addrB] <= diB;\r
- end \r
-end\r
-\r
-\r
-always @(posedge clkA)\r
-begin : portA\r
- integer i;\r
- reg [log2RATIO-1:0] lsbaddr ;\r
- for (i=0; i< RATIO; i= i+ 1) begin \r
- lsbaddr = i;\r
- if (enaA) begin\r
- readA[(i+1)*minWIDTH -1 -: minWIDTH] <= RAM[{addrA, lsbaddr}];\r
-\r
- if (weA)\r
- RAM[{addrA, lsbaddr}] <= diA[(i+1)*minWIDTH-1 -: minWIDTH];\r
- end\r
- end\r
-end\r
-\r
-assign doA = readA;\r
-assign doB = readB;\r
-\r
-endmodule\r
+++ /dev/null
-read_verilog asym_ram_tdp_read_first.v
-hierarchy -top asym_ram_tdp_read_first
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd asym_ram_tdp_read_first
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 1 t:$mem
-select -assert-count 2 t:LUT2
-
-select -assert-none t:$mem t:LUT2 %% t:* %D
+++ /dev/null
-// Asymmetric port RAM - TDP\r
-// WRITE_FIRST MODE.\r
-// asym_ram_tdp_write_first.v\r
-\r
-\r
-module asym_ram_tdp_write_first (clkA, clkB, enaA, weA, enaB, weB, addrA, addrB, diA, doA, diB, doB);\r
-parameter WIDTHB = 4;\r
-//Default parameters were changed because of slow test\r
-//parameter SIZEB = 1024;\r
-//parameter ADDRWIDTHB = 10;\r
-parameter SIZEB = 32;\r
-parameter ADDRWIDTHB = 8;\r
-\r
-//parameter WIDTHA = 16;\r
-parameter WIDTHA = 4;\r
-//parameter SIZEA = 256;\r
-parameter SIZEA = 32;\r
-parameter ADDRWIDTHA = 8;\r
-input clkA;\r
-input clkB;\r
-input weA, weB;\r
-input enaA, enaB;\r
-\r
-input [ADDRWIDTHA-1:0] addrA;\r
-input [ADDRWIDTHB-1:0] addrB;\r
-input [WIDTHA-1:0] diA;\r
-input [WIDTHB-1:0] diB;\r
-\r
-output [WIDTHA-1:0] doA;\r
-output [WIDTHB-1:0] doB;\r
-\r
-`define max(a,b) {(a) > (b) ? (a) : (b)}\r
-`define min(a,b) {(a) < (b) ? (a) : (b)}\r
-\r
-function integer log2;\r
-input integer value;\r
-reg [31:0] shifted;\r
-integer res;\r
-begin\r
- if (value < 2)\r
- log2 = value;\r
- else\r
- begin\r
- shifted = value-1;\r
- for (res=0; shifted>0; res=res+1)\r
- shifted = shifted>>1;\r
- log2 = res;\r
- end\r
-end\r
-endfunction\r
-\r
-localparam maxSIZE = `max(SIZEA, SIZEB);\r
-localparam maxWIDTH = `max(WIDTHA, WIDTHB);\r
-localparam minWIDTH = `min(WIDTHA, WIDTHB);\r
-\r
-localparam RATIO = maxWIDTH / minWIDTH;\r
-localparam log2RATIO = log2(RATIO);\r
-\r
-reg [minWIDTH-1:0] RAM [0:maxSIZE-1];\r
-reg [WIDTHA-1:0] readA;\r
-reg [WIDTHB-1:0] readB;\r
-\r
-always @(posedge clkB)\r
-begin\r
- if (enaB) begin\r
- if (weB)\r
- RAM[addrB] = diB;\r
- readB = RAM[addrB] ;\r
- end\r
-end\r
-\r
-\r
-always @(posedge clkA)\r
-begin : portA\r
- integer i;\r
- reg [log2RATIO-1:0] lsbaddr ;\r
- for (i=0; i< RATIO; i= i+ 1) begin\r
- lsbaddr = i;\r
- if (enaA) begin\r
-\r
- if (weA)\r
- RAM[{addrA, lsbaddr}] = diA[(i+1)*minWIDTH-1 -: minWIDTH];\r
-\r
- readA[(i+1)*minWIDTH -1 -: minWIDTH] = RAM[{addrA, lsbaddr}];\r
- end\r
- end\r
-end\r
-\r
-assign doA = readA;\r
-assign doB = readB;\r
-\r
-endmodule\r
+++ /dev/null
-read_verilog asym_ram_tdp_write_first.v
-hierarchy -top asym_ram_tdp_write_first
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd asym_ram_tdp_write_first
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 2 t:BUFG
-select -assert-count 200 t:FDRE
-select -assert-count 10 t:LUT2
-select -assert-count 44 t:LUT3
-select -assert-count 81 t:LUT4
-select -assert-count 104 t:LUT5
-select -assert-count 560 t:LUT6
-select -assert-count 261 t:MUXF7
-select -assert-count 127 t:MUXF8
-
-
-select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXF7 t:MUXF8 %% t:* %D
+++ /dev/null
-// Black Box\r
-// black_box_1.v\r
-// \r
-(* black_box *) module black_box1 (in1, in2, dout);\r
-input in1, in2;\r
-output dout;\r
-endmodule\r
-\r
-module black_box_1 (DI_1, DI_2, DOUT);\r
-input DI_1, DI_2;\r
-output DOUT;\r
-\r
-black_box1 U1 (\r
- .in1(DI_1),\r
- .in2(DI_2),\r
- .dout(DOUT)\r
- );\r
-\r
-endmodule\r
+++ /dev/null
-read_verilog black_box_1.v
-hierarchy -top black_box_1
-proc
-tribuf
-flatten
-synth
-#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-cd black_box_1 # Constrain all select calls below inside the top module
-#Vivado synthesizes 1 black box.
-#stat
-#select -assert-count 0 t:LUT1
-#select -assert-count 1 t:$_TBUF_
-#select -assert-none t:LUT1 t:$_TBUF_ %% t:* %D
+++ /dev/null
-// Single-Port BRAM with Byte-wide Write Enable\r
-// Read-First mode\r
-// Single-process description\r
-// Compact description of the write with a generate-for \r
-// statement\r
-// Column width and number of columns easily configurable\r
-//\r
-// bytewrite_ram_1b.v\r
-//\r
-\r
-module bytewrite_ram_1b (clk, we, addr, di, do);\r
-\r
-parameter SIZE = 1024; \r
-parameter ADDR_WIDTH = 10; \r
-parameter COL_WIDTH = 8; \r
-parameter NB_COL = 4;\r
-\r
-input clk;\r
-input [NB_COL-1:0] we;\r
-input [ADDR_WIDTH-1:0] addr;\r
-input [NB_COL*COL_WIDTH-1:0] di;\r
-output reg [NB_COL*COL_WIDTH-1:0] do;\r
-\r
-reg [NB_COL*COL_WIDTH-1:0] RAM [SIZE-1:0];\r
-\r
-always @(posedge clk)\r
-begin\r
- do <= RAM[addr];\r
-end\r
-\r
-generate genvar i;\r
-for (i = 0; i < NB_COL; i = i+1)\r
-begin\r
-always @(posedge clk)\r
-begin\r
- if (we[i])\r
- RAM[addr][(i+1)*COL_WIDTH-1:i*COL_WIDTH] <= di[(i+1)*COL_WIDTH-1:i*COL_WIDTH];\r
- end \r
-end\r
-endgenerate\r
-\r
-endmodule\r
+++ /dev/null
-read_verilog bytewrite_ram_1b.v
-hierarchy -top bytewrite_ram_1b
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd bytewrite_ram_1b
-stat
-#Vivado synthesizes 1 RAMB36E1.
-select -assert-count 1 t:BUFG
-select -assert-count 32 t:LUT2
-select -assert-count 8 t:RAMB36E1
-
-select -assert-none t:BUFG t:LUT2 t:RAMB36E1 %% t:* %D
+++ /dev/null
-//\r
-// True-Dual-Port BRAM with Byte-wide Write Enable\r
-// No-Change mode\r
-//\r
-// bytewrite_tdp_ram_nc.v\r
-//\r
-// ByteWide Write Enable, - NO_CHANGE mode template - Vivado recomended\r
-module bytewrite_tdp_ram_nc\r
- #(\r
- //---------------------------------------------------------------\r
- parameter NUM_COL = 4,\r
- parameter COL_WIDTH = 8,\r
- parameter ADDR_WIDTH = 10, // Addr Width in bits : 2**ADDR_WIDTH = RAM Depth\r
- parameter DATA_WIDTH = NUM_COL*COL_WIDTH // Data Width in bits\r
- //---------------------------------------------------------------\r
- ) (\r
- input clkA,\r
- input enaA, \r
- input [NUM_COL-1:0] weA,\r
- input [ADDR_WIDTH-1:0] addrA,\r
- input [DATA_WIDTH-1:0] dinA,\r
- output reg [DATA_WIDTH-1:0] doutA,\r
- \r
- input clkB,\r
- input enaB,\r
- input [NUM_COL-1:0] weB,\r
- input [ADDR_WIDTH-1:0] addrB,\r
- input [DATA_WIDTH-1:0] dinB,\r
- output reg [DATA_WIDTH-1:0] doutB\r
- );\r
-\r
- \r
- // Core Memory \r
- reg [DATA_WIDTH-1:0] ram_block [(2**ADDR_WIDTH)-1:0];\r
- \r
- // Port-A Operation\r
- generate\r
- genvar i;\r
- for(i=0;i<NUM_COL;i=i+1) begin\r
- always @ (posedge clkA) begin\r
- if(enaA) begin\r
- if(weA[i]) begin\r
- ram_block[addrA][i*COL_WIDTH +: COL_WIDTH] <= dinA[i*COL_WIDTH +: COL_WIDTH];\r
- end\r
- end\r
- end\r
- end\r
- endgenerate\r
- \r
- always @ (posedge clkA) begin\r
- if(enaA) begin\r
- if (~|weA)\r
- doutA <= ram_block[addrA];\r
- end\r
- end\r
- \r
- \r
- // Port-B Operation:\r
- generate\r
- for(i=0;i<NUM_COL;i=i+1) begin\r
- always @ (posedge clkB) begin\r
- if(enaB) begin\r
- if(weB[i]) begin\r
- ram_block[addrB][i*COL_WIDTH +: COL_WIDTH] <= dinB[i*COL_WIDTH +: COL_WIDTH];\r
- end\r
- end\r
- end\r
- end\r
- endgenerate\r
- \r
- always @ (posedge clkB) begin\r
- if(enaB) begin\r
- if (~|weB)\r
- doutB <= ram_block[addrB];\r
- end\r
- end\r
- \r
-endmodule // bytewrite_tdp_ram_nc\r
+++ /dev/null
-read_verilog bytewrite_tdp_ram_nc.v
-hierarchy -top bytewrite_tdp_ram_nc
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd bytewrite_tdp_ram_nc
-stat
-#Vivado synthesizes 1 RAMB36E1.
-select -assert-count 1 t:$mem
-select -assert-count 8 t:LUT2
-select -assert-count 64 t:LUT3
-select -assert-count 2 t:LUT5
-select -assert-none t:LUT2 t:LUT3 t:LUT5 t:$mem %% t:* %D
+++ /dev/null
-// ByteWide Write Enable, - Alternate READ_FIRST mode template - Vivado recomended\r
-// bytewrite_tdp_ram_readfirst2.v\r
-module bytewrite_tdp_ram_readfirst2\r
- #(\r
- //-------------------------------------------------------------------------\r
- parameter NUM_COL = 4,\r
- parameter COL_WIDTH = 8,\r
- parameter ADDR_WIDTH = 10, // Addr Width in bits : 2**ADDR_WIDTH = RAM Depth\r
- parameter DATA_WIDTH = NUM_COL*COL_WIDTH // Data Width in bits\r
- //-------------------------------------------------------------------------\r
- ) (\r
- input clkA,\r
- input enaA, \r
- input [NUM_COL-1:0] weA,\r
- input [ADDR_WIDTH-1:0] addrA,\r
- input [DATA_WIDTH-1:0] dinA,\r
- output reg [DATA_WIDTH-1:0] doutA,\r
- \r
- input clkB,\r
- input enaB,\r
- input [NUM_COL-1:0] weB,\r
- input [ADDR_WIDTH-1:0] addrB,\r
- input [DATA_WIDTH-1:0] dinB,\r
- output reg [DATA_WIDTH-1:0] doutB\r
- );\r
- \r
- \r
- // Core Memory \r
- reg [DATA_WIDTH-1:0] ram_block [(2**ADDR_WIDTH)-1:0];\r
- \r
- // Port-A Operation\r
- generate\r
- genvar i;\r
- for(i=0;i<NUM_COL;i=i+1) begin\r
- always @ (posedge clkA) begin\r
- if(enaA) begin\r
- if(weA[i]) begin\r
- ram_block[addrA][i*COL_WIDTH +: COL_WIDTH] <= dinA[i*COL_WIDTH +: COL_WIDTH];\r
- end\r
- end\r
- end\r
- end\r
- endgenerate\r
- \r
- always @ (posedge clkA) begin\r
- if(enaA) begin\r
- doutA <= ram_block[addrA];\r
- end\r
- end\r
- \r
- \r
- // Port-B Operation:\r
- generate\r
- for(i=0;i<NUM_COL;i=i+1) begin\r
- always @ (posedge clkB) begin\r
- if(enaB) begin\r
- if(weB[i]) begin\r
- ram_block[addrB][i*COL_WIDTH +: COL_WIDTH] <= dinB[i*COL_WIDTH +: COL_WIDTH];\r
- end\r
- end\r
- end\r
- end\r
- endgenerate\r
- \r
- always @ (posedge clkB) begin\r
- if(enaB) begin\r
- doutB <= ram_block[addrB];\r
- end\r
- end\r
-\r
-endmodule // bytewrite_tdp_ram_readfirst2\r
+++ /dev/null
-read_verilog bytewrite_tdp_ram_readfirst2.v
-hierarchy -top bytewrite_tdp_ram_readfirst2
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd bytewrite_tdp_ram_readfirst2
-stat
-#Vivado synthesizes 1 RAMB36E1.
-select -assert-count 1 t:$mem
-select -assert-count 8 t:LUT2
-select -assert-count 64 t:LUT3
-select -assert-none t:LUT2 t:LUT3 t:$mem %% t:* %D
+++ /dev/null
-// True-Dual-Port BRAM with Byte-wide Write Enable\r
-// Read-First mode \r
-// bytewrite_tdp_ram_rf.v\r
-//\r
-\r
-module bytewrite_tdp_ram_rf\r
- #(\r
-//--------------------------------------------------------------------------\r
-parameter NUM_COL = 4,\r
-parameter COL_WIDTH = 8,\r
-parameter ADDR_WIDTH = 10, \r
-// Addr Width in bits : 2 *ADDR_WIDTH = RAM Depth\r
-parameter DATA_WIDTH = NUM_COL*COL_WIDTH // Data Width in bits\r
- //----------------------------------------------------------------------\r
- ) (\r
- input clkA,\r
- input enaA, \r
- input [NUM_COL-1:0] weA,\r
- input [ADDR_WIDTH-1:0] addrA,\r
- input [DATA_WIDTH-1:0] dinA,\r
- output reg [DATA_WIDTH-1:0] doutA,\r
-\r
- input clkB,\r
- input enaB,\r
- input [NUM_COL-1:0] weB,\r
- input [ADDR_WIDTH-1:0] addrB,\r
- input [DATA_WIDTH-1:0] dinB,\r
- output reg [DATA_WIDTH-1:0] doutB\r
- );\r
-\r
-\r
- // Core Memory \r
- reg [DATA_WIDTH-1:0] ram_block [(2**ADDR_WIDTH)-1:0];\r
-\r
- integer i;\r
- // Port-A Operation\r
- always @ (posedge clkA) begin\r
- if(enaA) begin\r
- for(i=0;i<NUM_COL;i=i+1) begin\r
- if(weA[i]) begin\r
- ram_block[addrA][i*COL_WIDTH +: COL_WIDTH] <= dinA[i*COL_WIDTH +: COL_WIDTH];\r
- end\r
- end\r
- doutA <= ram_block[addrA]; \r
- end\r
- end\r
-\r
- // Port-B Operation:\r
- always @ (posedge clkB) begin\r
- if(enaB) begin\r
- for(i=0;i<NUM_COL;i=i+1) begin\r
- if(weB[i]) begin\r
- ram_block[addrB][i*COL_WIDTH +: COL_WIDTH] <= dinB[i*COL_WIDTH +: COL_WIDTH];\r
- end\r
- end \r
- \r
- doutB <= ram_block[addrB]; \r
- end\r
- end\r
-\r
-endmodule // bytewrite_tdp_ram_rf\r
+++ /dev/null
-read_verilog bytewrite_tdp_ram_rf.v
-hierarchy -top bytewrite_tdp_ram_rf
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd bytewrite_tdp_ram_rf
-stat
-#Vivado synthesizes 1 RAMB36E1.
-select -assert-count 1 t:$mem
-select -assert-count 8 t:LUT2
-select -assert-count 64 t:LUT3
-select -assert-none t:LUT2 t:LUT3 t:$mem %% t:* %D
+++ /dev/null
-// True-Dual-Port BRAM with Byte-wide Write Enable\r
-// Write-First mode\r
-// File: HDL_Coding_Techniques/rams/bytewrite_tdp_ram_wf.v\r
-//\r
-// ByteWide Write Enable, - WRITE_FIRST mode template - Vivado recomended\r
-module bytewrite_tdp_ram_wf\r
- #(\r
- //----------------------------------------------------------------------\r
-parameter NUM_COL = 4,\r
-parameter COL_WIDTH = 8,\r
-parameter ADDR_WIDTH = 10, \r
-// Addr Width in bits : 2**ADDR_WIDTH = RAM Depth\r
-parameter DATA_WIDTH = NUM_COL*COL_WIDTH // Data Width in bits\r
- //----------------------------------------------------------------------\r
- ) (\r
- input clkA,\r
- input enaA, \r
- input [NUM_COL-1:0] weA,\r
- input [ADDR_WIDTH-1:0] addrA,\r
- input [DATA_WIDTH-1:0] dinA,\r
- output reg [DATA_WIDTH-1:0] doutA,\r
- \r
- input clkB,\r
- input enaB,\r
- input [NUM_COL-1:0] weB,\r
- input [ADDR_WIDTH-1:0] addrB,\r
- input [DATA_WIDTH-1:0] dinB,\r
- output reg [DATA_WIDTH-1:0] doutB\r
- );\r
- \r
- \r
- // Core Memory \r
- reg [DATA_WIDTH-1:0] ram_block [(2**ADDR_WIDTH)-1:0];\r
- \r
- // Port-A Operation\r
- generate\r
- genvar i;\r
- for(i=0;i<NUM_COL;i=i+1) begin\r
- always @ (posedge clkA) begin\r
- if(enaA) begin\r
- if(weA[i]) begin\r
- ram_block[addrA][i*COL_WIDTH +: COL_WIDTH] <= dinA[i*COL_WIDTH +: COL_WIDTH];\r
- doutA[i*COL_WIDTH +: COL_WIDTH] <= dinA[i*COL_WIDTH +: COL_WIDTH] ;\r
- end else begin\r
- doutA[i*COL_WIDTH +: COL_WIDTH] <= ram_block[addrA][i*COL_WIDTH +: COL_WIDTH] ;\r
- end\r
- end\r
- end\r
- end\r
- endgenerate\r
- \r
- // Port-B Operation:\r
- generate\r
- for(i=0;i<NUM_COL;i=i+1) begin\r
- always @ (posedge clkB) begin\r
- if(enaB) begin\r
- if(weB[i]) begin\r
- ram_block[addrB][i*COL_WIDTH +: COL_WIDTH] <= dinB[i*COL_WIDTH +: COL_WIDTH];\r
- doutB[i*COL_WIDTH +: COL_WIDTH] <= dinB[i*COL_WIDTH +: COL_WIDTH] ;\r
- end else begin \r
- doutB[i*COL_WIDTH +: COL_WIDTH] <= ram_block[addrB][i*COL_WIDTH +: COL_WIDTH] ;\r
- end\r
- end \r
- end\r
- end\r
- endgenerate\r
- \r
-endmodule // bytewrite_tdp_ram_wf\r
+++ /dev/null
-read_verilog bytewrite_tdp_ram_wf.v
-hierarchy -top bytewrite_tdp_ram_wf
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd bytewrite_tdp_ram_wf
-stat
-#Vivado synthesizes 1 RAMB36E1.
-select -assert-count 1 t:$mem
-select -assert-count 2 t:BUFG
-select -assert-count 64 t:FDRE
-select -assert-count 8 t:LUT2
-select -assert-count 128 t:LUT3
-select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:$mem %% t:* %D
+++ /dev/null
-// Complex Multiplier with accumulation (pr+i.pi) = (ar+i.ai)*(br+i.bi)\r
-// File: cmacc.v\r
-// The RTL below describes a complex multiplier with accumulation\r
-// which can be packed into 3 DSP blocks (Ultrascale architecture)\r
-//Default parameters were changed because of slow test\r
-//module cmacc # (parameter AWIDTH = 16, BWIDTH = 18, SIZEOUT = 40)\r
-module cmacc # (parameter AWIDTH = 4, BWIDTH = 5, SIZEOUT = 9)\r
- (\r
- input clk,\r
- input sload,\r
- input signed [AWIDTH-1:0] ar,\r
- input signed [AWIDTH-1:0] ai,\r
- input signed [BWIDTH-1:0] br,\r
- input signed [BWIDTH-1:0] bi,\r
- output signed [SIZEOUT-1:0] pr,\r
- output signed [SIZEOUT-1:0] pi);\r
-\r
- reg signed [AWIDTH-1:0] ai_d, ai_dd, ai_ddd, ai_dddd;\r
- reg signed [AWIDTH-1:0] ar_d, ar_dd, ar_ddd, ar_dddd;\r
- reg signed [BWIDTH-1:0] bi_d, bi_dd, bi_ddd, br_d, br_dd, br_ddd;\r
- reg signed [AWIDTH:0] addcommon;\r
- reg signed [BWIDTH:0] addr, addi;\r
- reg signed [AWIDTH+BWIDTH:0] mult0, multr, multi;\r
- reg signed [SIZEOUT-1:0] pr_int, pi_int, old_result_real, old_result_im;\r
- reg signed [AWIDTH+BWIDTH:0] common, commonr1, commonr2;\r
-\r
- reg sload_reg;\r
-\r
- `ifdef SIM\r
- initial\r
- begin\r
- ai_d = 0;\r
- ai_dd = 0;\r
- ai_ddd = 0;\r
- ai_dddd = 0;\r
- ar_d = 0;\r
- ar_dd = 0;\r
- ar_ddd = 0;\r
- ar_dddd = 0;\r
- bi_d = 0;\r
- bi_dd = 0;\r
- bi_ddd = 0;\r
- br_d = 0;\r
- br_dd = 0;\r
- br_ddd = 0;\r
- end\r
- `endif\r
-\r
- always @(posedge clk)\r
- begin\r
- ar_d <= ar;\r
- ar_dd <= ar_d;\r
- ai_d <= ai;\r
- ai_dd <= ai_d;\r
- br_d <= br;\r
- br_dd <= br_d;\r
- br_ddd <= br_dd;\r
- bi_d <= bi;\r
- bi_dd <= bi_d;\r
- bi_ddd <= bi_dd;\r
- sload_reg <= sload;\r
- end\r
-\r
- // Common factor (ar ai) x bi, shared for the calculations of the real and imaginary final products\r
- //\r
- always @(posedge clk)\r
- begin\r
- addcommon <= ar_d - ai_d;\r
- mult0 <= addcommon * bi_dd;\r
- common <= mult0;\r
- end\r
-\r
- // Accumulation loop (combinatorial) for *Real*\r
- //\r
- always @(sload_reg or pr_int)\r
- if (sload_reg)\r
- old_result_real <= 0;\r
- else\r
- // 'sload' is now and opens the accumulation loop.\r
- // The accumulator takes the next multiplier output\r
- // in the same cycle.\r
- old_result_real <= pr_int;\r
-\r
- // Real product\r
- //\r
- always @(posedge clk)\r
- begin\r
- ar_ddd <= ar_dd;\r
- ar_dddd <= ar_ddd;\r
- addr <= br_ddd - bi_ddd;\r
- multr <= addr * ar_dddd;\r
- commonr1 <= common;\r
- pr_int <= multr + commonr1 + old_result_real;\r
- end\r
-\r
- // Accumulation loop (combinatorial) for *Imaginary*\r
- //\r
- always @(sload_reg or pi_int)\r
- if (sload_reg)\r
- old_result_im <= 0;\r
- else\r
- // 'sload' is now and opens the accumulation loop.\r
- // The accumulator takes the next multiplier output\r
- // in the same cycle.\r
- old_result_im <= pi_int;\r
-\r
- // Imaginary product\r
- //\r
- always @(posedge clk)\r
- begin\r
- ai_ddd <= ai_dd;\r
- ai_dddd <= ai_ddd;\r
- addi <= br_ddd + bi_ddd;\r
- multi <= addi * ai_dddd;\r
- commonr2 <= common;\r
- pi_int <= multi + commonr2 + old_result_im;\r
- end\r
-\r
- assign pr = pr_int;\r
- assign pi = pi_int;\r
-\r
-endmodule // cmacc\r
+++ /dev/null
-read_verilog cmacc.v
-hierarchy -top cmacc
-proc
-flatten
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-
-cd cmacc
-#Vivado synthesizes 5 DSP48E1, 32 FDRE, 18 LUT.
-stat
-select -assert-count 1 t:BUFG
-select -assert-count 77 t:FDRE
-select -assert-count 5 t:LUT1
-select -assert-count 46 t:LUT2
-select -assert-count 25 t:LUT3
-select -assert-count 8 t:LUT4
-select -assert-count 16 t:LUT5
-select -assert-count 85 t:LUT6
-select -assert-count 54 t:MUXCY
-select -assert-count 8 t:MUXF7
-select -assert-count 2 t:MUXF8
-select -assert-count 22 t:SRL16E
-select -assert-count 62 t:XORCY
-
-select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:SRL16E t:XORCY %% t:* %D
+++ /dev/null
-//\r
-// Complex Multiplier (pr+i.pi) = (ar+i.ai)*(br+i.bi)\r
-// file: cmult.v\r
-\r
-module cmult # (parameter AWIDTH = 16, BWIDTH = 18)\r
- (\r
- input clk,\r
- input signed [AWIDTH-1:0] ar, ai,\r
- input signed [BWIDTH-1:0] br, bi,\r
- output signed [AWIDTH+BWIDTH:0] pr, pi\r
- );\r
-\r
-reg signed [AWIDTH-1:0] ai_d, ai_dd, ai_ddd, ai_dddd ; \r
-reg signed [AWIDTH-1:0] ar_d, ar_dd, ar_ddd, ar_dddd ; \r
-reg signed [BWIDTH-1:0] bi_d, bi_dd, bi_ddd, br_d, br_dd, br_ddd ; \r
-reg signed [AWIDTH:0] addcommon ; \r
-reg signed [BWIDTH:0] addr, addi ; \r
-reg signed [AWIDTH+BWIDTH:0] mult0, multr, multi, pr_int, pi_int ; \r
-reg signed [AWIDTH+BWIDTH:0] common, commonr1, commonr2 ; \r
- \r
-always @(posedge clk)\r
- begin\r
- ar_d <= ar;\r
- ar_dd <= ar_d;\r
- ai_d <= ai;\r
- ai_dd <= ai_d;\r
- br_d <= br;\r
- br_dd <= br_d;\r
- br_ddd <= br_dd;\r
- bi_d <= bi;\r
- bi_dd <= bi_d;\r
- bi_ddd <= bi_dd;\r
- end\r
- \r
-// Common factor (ar ai) x bi, shared for the calculations of the real and imaginary final products\r
-// \r
-always @(posedge clk)\r
- begin\r
- addcommon <= ar_d - ai_d;\r
- mult0 <= addcommon * bi_dd;\r
- common <= mult0;\r
- end\r
-\r
-// Real product\r
-//\r
-always @(posedge clk)\r
- begin\r
- ar_ddd <= ar_dd;\r
- ar_dddd <= ar_ddd;\r
- addr <= br_ddd - bi_ddd;\r
- multr <= addr * ar_dddd;\r
- commonr1 <= common;\r
- pr_int <= multr + commonr1;\r
- end\r
-\r
-// Imaginary product\r
-//\r
-always @(posedge clk)\r
- begin\r
- ai_ddd <= ai_dd;\r
- ai_dddd <= ai_ddd;\r
- addi <= br_ddd + bi_ddd;\r
- multi <= addi * ai_dddd;\r
- commonr2 <= common;\r
- pi_int <= multi + commonr2;\r
- end\r
-\r
-assign pr = pr_int;\r
-assign pi = pi_int;\r
- \r
-endmodule // cmult\r
+++ /dev/null
-read_verilog cmult.v
-hierarchy -top cmult
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd cmult
-#Vivado synthesizes 3 DSP48E1, 68 FDRE.
-select -assert-count 1 t:BUFG
-select -assert-count 281 t:FDRE
-select -assert-count 18 t:LUT1
-select -assert-count 467 t:LUT2
-select -assert-count 187 t:LUT3
-select -assert-count 98 t:LUT4
-select -assert-count 165 t:LUT5
-select -assert-count 1596 t:LUT6
-select -assert-count 222 t:MUXCY
-select -assert-count 393 t:MUXF7
-select -assert-count 121 t:MUXF8
-select -assert-count 85 t:SRL16E
-select -assert-count 230 t:XORCY
-
-select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:SRL16E t:XORCY %% t:* %D
+++ /dev/null
-// 32-bit dynamic shift register.\r
-// Download: \r
-// File: dynamic_shift_registers_1.v\r
-\r
-module dynamic_shift_register_1 (CLK, CE, SEL, SI, DO);\r
-parameter SELWIDTH = 5;\r
-input CLK, CE, SI;\r
-input [SELWIDTH-1:0] SEL;\r
-output DO;\r
-\r
-localparam DATAWIDTH = 2**SELWIDTH;\r
-reg [DATAWIDTH-1:0] data;\r
-\r
-assign DO = data[SEL];\r
-\r
-always @(posedge CLK)\r
- begin\r
- if (CE == 1'b1)\r
- data <= {data[DATAWIDTH-2:0], SI};\r
- end \r
-endmodule\r
+++ /dev/null
-read_verilog dynamic_shift_registers_1.v
-hierarchy -top dynamic_shift_register_1
-proc
-flatten
-#ERROR: Found 1 unproven $equiv cells in 'equiv_status -assert'.
-#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-cd dynamic_shift_register_1 # Constrain all select calls below inside the top module
-#Vivado synthesizes 1 BUFG, 3 SRLC32E.
-stat
-select -assert-count 1 t:BUFG
-select -assert-count 1 t:SRLC32E
-select -assert-none t:BUFG t:SRLC32E %% t:* %D
+++ /dev/null
-// Pre-add/subtract select with Dynamic control\r
-// dynpreaddmultadd.v\r
-//Default parameters were changed because of slow test.\r
-//module dynpreaddmultadd # (parameter SIZEIN = 16)\r
-module dynpreaddmultadd # (parameter SIZEIN = 8)\r
- (\r
- input clk, ce, rst, subadd,\r
- input signed [SIZEIN-1:0] a, b, c, d,\r
- output signed [2*SIZEIN:0] dynpreaddmultadd_out\r
- );\r
-\r
-// Declare registers for intermediate values\r
-reg signed [SIZEIN-1:0] a_reg, b_reg, c_reg;\r
-reg signed [SIZEIN:0] add_reg;\r
-reg signed [2*SIZEIN:0] d_reg, m_reg, p_reg;\r
-\r
-always @(posedge clk)\r
-begin\r
- if (rst)\r
- begin\r
- a_reg <= 0;\r
- b_reg <= 0;\r
- c_reg <= 0;\r
- d_reg <= 0;\r
- add_reg <= 0;\r
- m_reg <= 0;\r
- p_reg <= 0;\r
- end\r
- else if (ce)\r
- begin\r
- a_reg <= a;\r
- b_reg <= b;\r
- c_reg <= c;\r
- d_reg <= d;\r
- if (subadd)\r
- add_reg <= a_reg - b_reg;\r
- else\r
- add_reg <= a_reg + b_reg;\r
- m_reg <= add_reg * c_reg;\r
- p_reg <= m_reg + d_reg;\r
- end\r
-end\r
-\r
-// Output accumulation result\r
-assign dynpreaddmultadd_out = p_reg;\r
-\r
-endmodule // dynpreaddmultadd\r
+++ /dev/null
-read_verilog dynpreaddmultadd.v
-hierarchy -top dynpreaddmultadd
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd dynpreaddmultadd
-
-#Vivado synthesizes 1 DSP48E1.
-select -assert-count 1 t:BUFG
-select -assert-count 75 t:FDRE
-select -assert-count 8 t:LUT1
-select -assert-count 131 t:LUT2
-select -assert-count 19 t:LUT3
-select -assert-count 26 t:LUT4
-select -assert-count 12 t:LUT5
-select -assert-count 142 t:LUT6
-select -assert-count 48 t:MUXCY
-select -assert-count 50 t:MUXF7
-select -assert-count 15 t:MUXF8
-select -assert-count 52 t:XORCY
-
-select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:XORCY %% t:* %D
+++ /dev/null
-// State Machine with single sequential block\r
-//fsm_1.v\r
-module fsm_1(clk,reset,flag,sm_out);\r
-input clk,reset,flag;\r
-output reg sm_out;\r
-\r
-parameter s1 = 3'b000;\r
-parameter s2 = 3'b001;\r
-parameter s3 = 3'b010;\r
-parameter s4 = 3'b011;\r
-parameter s5 = 3'b111;\r
-\r
-reg [2:0] state;\r
-\r
-always@(posedge clk)\r
- begin\r
- if(reset)\r
- begin\r
- state <= s1;\r
- sm_out <= 1'b1;\r
- end\r
- else\r
- begin\r
- case(state)\r
- s1: if(flag) \r
- begin \r
- state <= s2; \r
- sm_out <= 1'b1; \r
- end\r
- else\r
- begin\r
- state <= s3;\r
- sm_out <= 1'b0;\r
- end\r
- s2: begin state <= s4; sm_out <= 1'b0; end\r
- s3: begin state <= s4; sm_out <= 1'b0; end\r
- s4: begin state <= s5; sm_out <= 1'b1; end\r
- s5: begin state <= s1; sm_out <= 1'b1; end\r
- endcase\r
- end\r
- end\r
-endmodule\r
+++ /dev/null
-read_verilog fsm_1.v
-hierarchy -top fsm_1
-proc
-flatten
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-cd fsm_1 # Constrain all select calls below inside the top module
-#Vivado synthesizes 2 LUT5, 2 LUT4, 1 LUT3, 4 FDRE.
-stat
-select -assert-count 1 t:BUFG
-select -assert-count 4 t:FDRE
-select -assert-count 2 t:LUT4
-select -assert-count 2 t:LUT5
-select -assert-count 1 t:LUT6
-
-select -assert-none t:BUFG t:FDRE t:LUT4 t:LUT5 t:LUT6 %% t:* %D
+++ /dev/null
-// Latch with Positive Gate and Asynchronous Reset
-// File: latches.v
-module latches (
- input G,
- input D,
- input CLR,
- output reg Q
- );
-always @ *
-begin
- if(CLR)
- Q = 0;
- else if(G)
- Q = D;
-end
-
-endmodule
+++ /dev/null
-read_verilog latches.v
-proc
-hierarchy -top latches
-flatten
-synth_xilinx
-#Vivado synthesizes 1 BUFG, 8 LDCE.
-select -assert-count 2 t:LUT2
-select -assert-count 1 t:$_DLATCH_P_
-#ERROR: Assertion failed: selection is not empty: t:LUT2 t:$_DLATCH_P_ %% t:* %D
-#select -assert-none t:LUT2 t:$_DLATCH_P_ %% t:* %D
+++ /dev/null
-// Signed 40-bit streaming accumulator with 16-bit inputs\r
-// File: macc.v\r
-//\r
-module macc # (\r
- //Default parameters were changed because of slow test\r
- // parameter SIZEIN = 16, SIZEOUT = 40\r
- // parameter SIZEIN = 12, SIZEOUT = 30\r
- parameter SIZEIN = 8, SIZEOUT = 20\r
- )\r
- (\r
- input clk, ce, sload,\r
- input signed [SIZEIN-1:0] a, b,\r
- output signed [SIZEOUT-1:0] accum_out\r
- );\r
-\r
- // Declare registers for intermediate values\r
-reg signed [SIZEIN-1:0] a_reg, b_reg;\r
-reg sload_reg;\r
-reg signed [2*SIZEIN:0] mult_reg;\r
-reg signed [SIZEOUT-1:0] adder_out, old_result;\r
-\r
-always @(adder_out or sload_reg)\r
-begin\r
- if (sload_reg)\r
- old_result <= 0;\r
- else\r
- // 'sload' is now active (=low) and opens the accumulation loop.\r
- // The accumulator takes the next multiplier output in\r
- // the same cycle.\r
- old_result <= adder_out;\r
-end\r
-\r
-always @(posedge clk)\r
- if (ce)\r
- begin\r
- a_reg <= a;\r
- b_reg <= b;\r
- mult_reg <= a_reg * b_reg;\r
- sload_reg <= sload;\r
- // Store accumulation result into a register\r
- adder_out <= old_result + mult_reg;\r
- end\r
-\r
-// Output accumulation result\r
-assign accum_out = adder_out;\r
-\r
-endmodule // macc\r
+++ /dev/null
-read_verilog macc.v
-hierarchy -top macc
-proc
-flatten
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-
-cd macc
-#Vivado synthesizes 1 DSP48E1, 1 FDRE. (When SIZEIN = 12, SIZEOUT = 30)
-stat
-select -assert-count 1 t:BUFG
-select -assert-count 53 t:FDRE
-select -assert-count 64 t:LUT2
-select -assert-count 10 t:LUT3
-select -assert-count 22 t:LUT4
-select -assert-count 14 t:LUT5
-select -assert-count 123 t:LUT6
-select -assert-count 34 t:MUXCY
-select -assert-count 41 t:MUXF7
-select -assert-count 14 t:MUXF8
-select -assert-count 36 t:XORCY
-
-select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:XORCY %% t:* %D
+++ /dev/null
-// Unsigned 16x24-bit Multiplier\r
-// 1 latency stage on operands\r
-// 3 latency stage after the multiplication\r
-// File: multipliers2.v\r
-//\r
-module mult_unsigned (clk, A, B, RES);\r
-//Default parameters were changed because of slow test\r
-//parameter WIDTHA = 16;\r
-//parameter WIDTHB = 24;\r
-parameter WIDTHA = 8;\r
-parameter WIDTHB = 12;\r
-input clk;\r
-input [WIDTHA-1:0] A;\r
-input [WIDTHB-1:0] B;\r
-output [WIDTHA+WIDTHB-1:0] RES;\r
-\r
-reg [WIDTHA-1:0] rA;\r
-reg [WIDTHB-1:0] rB;\r
-reg [WIDTHA+WIDTHB-1:0] M [3:0];\r
-\r
-integer i;\r
-always @(posedge clk)\r
- begin\r
- rA <= A;\r
- rB <= B;\r
- M[0] <= rA * rB;\r
- for (i = 0; i < 3; i = i+1)\r
- M[i+1] <= M[i];\r
- end\r
-\r
-assign RES = M[3];\r
-\r
-endmodule\r
+++ /dev/null
-read_verilog mult_unsigned.v
-hierarchy -top mult_unsigned
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd mult_unsigned
-
-#Vivado synthesizes 1 DSP48E1, 40 FDRE.
-select -assert-count 1 t:BUFG
-select -assert-count 20 t:FDRE
-select -assert-count 33 t:LUT2
-select -assert-count 1 t:LUT3
-select -assert-count 11 t:LUT4
-select -assert-count 4 t:LUT5
-select -assert-count 139 t:LUT6
-select -assert-count 19 t:MUXCY
-select -assert-count 35 t:MUXF7
-select -assert-count 20 t:SRL16E
-select -assert-count 20 t:XORCY
-select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:SRL16E t:XORCY %% t:* %D
+++ /dev/null
-//\r
-// Pre-adder support in subtract mode for DSP block\r
-// File: presubmult.v\r
-\r
-module presubmult # (//Default parameters were changed because of slow test\r
- // parameter SIZEIN = 16\r
- parameter SIZEIN = 8\r
- )\r
- (\r
- input clk, ce, rst,\r
- input signed [SIZEIN-1:0] a, b, c,\r
- output signed [2*SIZEIN:0] presubmult_out\r
- );\r
-\r
-// Declare registers for intermediate values\r
-reg signed [SIZEIN-1:0] a_reg, b_reg, c_reg;\r
-reg signed [SIZEIN:0] add_reg;\r
-reg signed [2*SIZEIN:0] m_reg, p_reg;\r
-\r
-always @(posedge clk)\r
- if (rst)\r
- begin\r
- a_reg <= 0;\r
- b_reg <= 0;\r
- c_reg <= 0;\r
- add_reg <= 0;\r
- m_reg <= 0;\r
- p_reg <= 0;\r
- end\r
- else if (ce)\r
- begin\r
- a_reg <= a;\r
- b_reg <= b;\r
- c_reg <= c;\r
- add_reg <= a - b;\r
- m_reg <= add_reg * c_reg;\r
- p_reg <= m_reg;\r
- end\r
-\r
-// Output accumulation result\r
-assign presubmult_out = p_reg;\r
-\r
-endmodule // presubmult\r
+++ /dev/null
-read_verilog presubmult.v
-hierarchy -top presubmult
-proc
-flatten
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-
-cd presubmult
-#Vivado synthesizes 1 DSP48E1. (When SIZEIN = 8)
-stat
-select -assert-count 1 t:BUFG
-select -assert-count 51 t:FDRE
-select -assert-count 75 t:LUT2
-select -assert-count 10 t:LUT3
-select -assert-count 24 t:LUT4
-select -assert-count 15 t:LUT5
-select -assert-count 136 t:LUT6
-select -assert-count 24 t:MUXCY
-select -assert-count 46 t:MUXF7
-select -assert-count 14 t:MUXF8
-select -assert-count 26 t:XORCY
-
-select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:XORCY %% t:* %D
+++ /dev/null
-// Simple Dual-Port Block RAM with One Clock\r
-// File: simple_dual_one_clock.v\r
-\r
-module simple_dual_one_clock (clk,ena,enb,wea,addra,addrb,dia,dob);\r
-\r
-input clk,ena,enb,wea;\r
-input [9:0] addra,addrb;\r
-input [15:0] dia;\r
-output [15:0] dob;\r
-reg [15:0] ram [1023:0];\r
-reg [15:0] doa,dob;\r
-\r
-always @(posedge clk) begin \r
- if (ena) begin\r
- if (wea)\r
- ram[addra] <= dia;\r
- end\r
-end\r
-\r
-always @(posedge clk) begin \r
- if (enb)\r
- dob <= ram[addrb];\r
-end\r
-\r
-endmodule
\ No newline at end of file
+++ /dev/null
-read_verilog ram_simple_dual_one_clock.v
-hierarchy -top simple_dual_one_clock
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-design -load postopt
-cd simple_dual_one_clock
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 1 t:BUFG
-select -assert-count 1 t:LUT2
-select -assert-count 1 t:RAMB18E1
-
-select -assert-none t:BUFG t:LUT2 t:RAMB18E1 %% t:* %D
+++ /dev/null
-// Simple Dual-Port Block RAM with Two Clocks\r
-// File: simple_dual_two_clocks.v\r
-\r
-module simple_dual_two_clocks (clka,clkb,ena,enb,wea,addra,addrb,dia,dob);\r
-\r
-input clka,clkb,ena,enb,wea;\r
-input [9:0] addra,addrb;\r
-input [15:0] dia;\r
-output [15:0] dob;\r
-reg [15:0] ram [1023:0];\r
-reg [15:0] dob;\r
-\r
-always @(posedge clka) \r
-begin \r
- if (ena)\r
- begin\r
- if (wea)\r
- ram[addra] <= dia;\r
- end\r
-end\r
-\r
-always @(posedge clkb) \r
-begin\r
- if (enb)\r
- begin\r
- dob <= ram[addrb];\r
- end\r
-end\r
-\r
-endmodule\r
+++ /dev/null
-read_verilog ram_simple_dual_two_clocks.v
-hierarchy -top simple_dual_two_clocks
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-design -load postopt
-cd simple_dual_two_clocks
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 2 t:BUFG
-select -assert-count 1 t:LUT2
-select -assert-count 1 t:RAMB18E1
-
-select -assert-none t:BUFG t:LUT2 t:RAMB18E1 %% t:* %D
+++ /dev/null
-// Dual-Port RAM with Asynchronous Read (Distributed RAM)\r
-// File: rams_dist.v\r
-\r
-module rams_dist (clk, we, a, dpra, di, spo, dpo);\r
-\r
-input clk;\r
-input we;\r
-input [5:0] a;\r
-input [5:0] dpra;\r
-input [15:0] di;\r
-output [15:0] spo;\r
-output [15:0] dpo;\r
-reg [15:0] ram [63:0];\r
-\r
-always @(posedge clk) \r
-begin \r
- if (we)\r
- ram[a] <= di;\r
-end\r
-\r
-assign spo = ram[a];\r
-assign dpo = ram[dpra];\r
-\r
-endmodule\r
+++ /dev/null
-read_verilog rams_dist.v
-hierarchy -top rams_dist
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd rams_dist
-stat
-#Vivado synthesizes 32 RAM64X1D.
-select -assert-count 1 t:BUFG
-select -assert-count 32 t:RAM64X1D
-
-select -assert-none t:BUFG t:RAM64X1D %% t:* %D
+++ /dev/null
-00001110110000011001111011000110
-00101011001011010101001000100011
-01110100010100011000011100001111
-01000001010000100101001110010100
-00001001101001111111101000101011
-00101101001011111110101010100111
-11101111000100111000111101101101
-10001111010010011001000011101111
-00000001100011100011110010011111
-11011111001110101011111001001010
-11100111010100111110110011001010
-11000100001001101100111100101001
-10001011100101011111111111100001
-11110101110110010000010110111010
-01001011000000111001010110101110
-11100001111111001010111010011110
-01101111011010010100001101110001
-01010100011011111000011000100100
-11110000111101101111001100001011
-10101101001111010100100100011100
-01011100001010111111101110101110
-01011101000100100111010010110101
-11110111000100000101011101101101
-11100111110001111010101100001101
-01110100000011101111111000011111
-00010011110101111000111001011101
-01101110001111100011010101101111
-10111100000000010011101011011011
-11000001001101001101111100010000
-00011111110010110110011111010101
-01100100100000011100100101110000
-10001000000100111011001010001111
-11001000100011101001010001100001
-10000000100111010011100111100011
-11011111010010100010101010000111
-10000000110111101000111110111011
-10110011010111101111000110011001
-00010111100001001010110111011100
-10011100101110101111011010110011
-01010011101101010001110110011010
-01111011011100010101000101000001
-10001000000110010110111001101010
-11101000001101010000111001010110
-11100011111100000111110101110101
-01001010000000001111111101101111
-00100011000011001000000010001111
-10011000111010110001001011100100
-11111111111011110101000101000111
-11000011000101000011100110100000
-01101101001011111010100011101001
-10000111101100101001110011010111
-11010110100100101110110010100100
-01001111111001101101011111001011
-11011001001101110110000100110111
-10110110110111100101110011100110
-10011100111001000010111111010110
-00000000001011011111001010110010
-10100110011010000010001000011011
-11001010111111001001110001110101
-00100001100010000111000101001000
-00111100101111110001101101111010
-11000010001010000000010100100001
-11000001000110001101000101001110
-10010011010100010001100100100111
+++ /dev/null
-// Initializing Block RAM from external data file\r
-// Binary data\r
-// File: rams_init_file.v \r
-\r
-module rams_init_file (clk, we, addr, din, dout);\r
-input clk;\r
-input we;\r
-input [5:0] addr;\r
-input [31:0] din;\r
-output [31:0] dout;\r
-\r
-reg [31:0] ram [0:63];\r
-reg [31:0] dout;\r
-\r
-initial begin\r
-$readmemb("rams_init_file.data",ram);\r
-end\r
-\r
-always @(posedge clk)\r
-begin\r
- if (we)\r
- ram[addr] <= din;\r
- dout <= ram[addr];\r
-end endmodule\r
+++ /dev/null
-read_verilog rams_init_file.v
-hierarchy -top rams_init_file
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd rams_init_file
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 1 t:BUFG
-select -assert-count 32 t:FDRE
-select -assert-count 32 t:RAM64X1D
-
-select -assert-none t:BUFG t:FDRE t:RAM64X1D %% t:* %D
+++ /dev/null
-// Block RAM with Optional Output Registers\r
-// File: rams_pipeline\r
-\r
-module rams_pipeline (clk1, clk2, we, en1, en2, addr1, addr2, di, res1, res2);\r
-input clk1;\r
-input clk2;\r
-input we, en1, en2;\r
-input [9:0] addr1;\r
-input [9:0] addr2;\r
-input [15:0] di;\r
-output [15:0] res1;\r
-output [15:0] res2;\r
-reg [15:0] res1;\r
-reg [15:0] res2;\r
-reg [15:0] RAM [1023:0];\r
-reg [15:0] do1;\r
-reg [15:0] do2;\r
-\r
-always @(posedge clk1)\r
-begin\r
- if (we == 1'b1)\r
- RAM[addr1] <= di;\r
- do1 <= RAM[addr1];\r
-end\r
-\r
-always @(posedge clk2)\r
-begin\r
- do2 <= RAM[addr2];\r
-end\r
-\r
-always @(posedge clk1)\r
-begin\r
- if (en1 == 1'b1)\r
- res1 <= do1;\r
-end\r
-\r
-always @(posedge clk2)\r
-begin\r
- if (en2 == 1'b1)\r
- res2 <= do2;\r
-end \r
-endmodule\r
+++ /dev/null
-read_verilog rams_pipeline.v
-hierarchy -top rams_pipeline
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd rams_pipeline
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 2 t:BUFG
-select -assert-count 32 t:FDRE
-select -assert-count 2 t:RAMB18E1
-
-select -assert-none t:BUFG t:FDRE t:RAMB18E1 %% t:* %D
+++ /dev/null
-// Single-Port Block RAM No-Change Mode\r
-// File: rams_sp_nc.v\r
-\r
-module rams_sp_nc (clk, we, en, addr, di, dout);\r
-\r
-input clk; \r
-input we; \r
-input en;\r
-input [9:0] addr; \r
-input [15:0] di; \r
-output [15:0] dout;\r
-\r
-reg [15:0] RAM [1023:0];\r
-reg [15:0] dout;\r
-\r
-always @(posedge clk)\r
-begin\r
- if (en)\r
- begin\r
- if (we)\r
- RAM[addr] <= di;\r
- else\r
- dout <= RAM[addr];\r
- end\r
-end\r
-endmodule\r
+++ /dev/null
-read_verilog rams_sp_nc.v
-hierarchy -top rams_sp_nc
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd rams_sp_nc
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 1 t:BUFG
-select -assert-count 2 t:LUT2
-select -assert-count 1 t:RAMB18E1
-
-select -assert-none t:BUFG t:LUT2 t:RAMB18E1 %% t:* %D
+++ /dev/null
-// Single-Port Block RAM Read-First Mode\r
-// rams_sp_rf.v\r
-module rams_sp_rf (clk, en, we, addr, di, dout);\r
-\r
-input clk; \r
-input we; \r
-input en;\r
-input [9:0] addr; \r
-input [15:0] di; \r
-output [15:0] dout;\r
-\r
-reg [15:0] RAM [1023:0];\r
-reg [15:0] dout;\r
-\r
-always @(posedge clk)\r
-begin\r
- if (en)\r
- begin\r
- if (we)\r
- RAM[addr]<=di;\r
- dout <= RAM[addr];\r
- end\r
-end\r
-\r
-endmodule\r
-\r
+++ /dev/null
-read_verilog rams_sp_rf.v
-hierarchy -top rams_sp_rf
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd rams_sp_rf
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 1 t:BUFG
-select -assert-count 1 t:LUT2
-select -assert-count 1 t:RAMB18E1
-
-select -assert-none t:BUFG t:LUT2 t:RAMB18E1 %% t:* %D
+++ /dev/null
-// Block RAM with Resettable Data Output\r
-// File: rams_sp_rf_rst.v\r
-\r
-module rams_sp_rf_rst (clk, en, we, rst, addr, di, dout);\r
-input clk; \r
-input en; \r
-input we; \r
-input rst;\r
-input [9:0] addr; \r
-input [15:0] di; \r
-output [15:0] dout;\r
-\r
-reg [15:0] ram [1023:0];\r
-reg [15:0] dout;\r
-\r
-always @(posedge clk)\r
-begin\r
- if (en) //optional enable\r
- begin\r
- if (we) //write enable\r
- ram[addr] <= di;\r
- if (rst) //optional reset\r
- dout <= 0;\r
- else\r
- dout <= ram[addr];\r
- end\r
-end\r
-\r
-endmodule\r
+++ /dev/null
-read_verilog rams_sp_rf_rst.v
-hierarchy -top rams_sp_rf_rst
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd rams_sp_rf_rst
-stat
-#Vivado synthesizes 1 RAMB18E1.
-
-select -assert-count 1 t:BUFG
-select -assert-count 16 t:FDRE
-select -assert-count 5 t:LUT2
-select -assert-count 4 t:LUT3
-select -assert-count 13 t:LUT4
-select -assert-count 23 t:LUT5
-select -assert-count 32 t:LUT6
-select -assert-count 128 t:RAM128X1D
-
-select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:RAM128X1D %% t:* %D
+++ /dev/null
-// Initializing Block RAM (Single-Port Block RAM)\r
-// File: rams_sp_rom \r
-module rams_sp_rom (clk, we, addr, di, dout);\r
-input clk;\r
-input we;\r
-input [5:0] addr;\r
-input [19:0] di;\r
-output [19:0] dout;\r
-\r
-reg [19:0] ram [63:0];\r
-reg [19:0] dout;\r
-\r
-initial \r
-begin\r
- ram[63] = 20'h0200A; ram[62] = 20'h00300; ram[61] = 20'h08101;\r
- ram[60] = 20'h04000; ram[59] = 20'h08601; ram[58] = 20'h0233A;\r
- ram[57] = 20'h00300; ram[56] = 20'h08602; ram[55] = 20'h02310;\r
- ram[54] = 20'h0203B; ram[53] = 20'h08300; ram[52] = 20'h04002;\r
- ram[51] = 20'h08201; ram[50] = 20'h00500; ram[49] = 20'h04001;\r
- ram[48] = 20'h02500; ram[47] = 20'h00340; ram[46] = 20'h00241;\r
- ram[45] = 20'h04002; ram[44] = 20'h08300; ram[43] = 20'h08201;\r
- ram[42] = 20'h00500; ram[41] = 20'h08101; ram[40] = 20'h00602;\r
- ram[39] = 20'h04003; ram[38] = 20'h0241E; ram[37] = 20'h00301;\r
- ram[36] = 20'h00102; ram[35] = 20'h02122; ram[34] = 20'h02021;\r
- ram[33] = 20'h00301; ram[32] = 20'h00102; ram[31] = 20'h02222;\r
- ram[30] = 20'h04001; ram[29] = 20'h00342; ram[28] = 20'h0232B; \r
- ram[27] = 20'h00900; ram[26] = 20'h00302; ram[25] = 20'h00102; \r
- ram[24] = 20'h04002; ram[23] = 20'h00900; ram[22] = 20'h08201; \r
- ram[21] = 20'h02023; ram[20] = 20'h00303; ram[19] = 20'h02433; \r
- ram[18] = 20'h00301; ram[17] = 20'h04004; ram[16] = 20'h00301; \r
- ram[15] = 20'h00102; ram[14] = 20'h02137; ram[13] = 20'h02036; \r
- ram[12] = 20'h00301; ram[11] = 20'h00102; ram[10] = 20'h02237; \r
- ram[9] = 20'h04004; ram[8] = 20'h00304; ram[7] = 20'h04040; \r
- ram[6] = 20'h02500; ram[5] = 20'h02500; ram[4] = 20'h02500; \r
- ram[3] = 20'h0030D; ram[2] = 20'h02341; ram[1] = 20'h08201; \r
- ram[0] = 20'h0400D;\r
-end\r
- \r
-always @(posedge clk)\r
-begin\r
- if (we)\r
- ram[addr] <= di;\r
- dout <= ram[addr];\r
-end \r
-\r
-endmodule\r
+++ /dev/null
-read_verilog rams_sp_rom.v
-hierarchy -top rams_sp_rom
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd rams_sp_rom
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 1 t:BUFG
-select -assert-count 20 t:RAM64X1D
-select -assert-count 20 t:FDRE
-
-select -assert-none t:BUFG t:RAM64X1D t:FDRE %% t:* %D
+++ /dev/null
-// ROMs Using Block RAM Resources.\r
-// File: rams_sp_rom_1.v\r
-//\r
-module rams_sp_rom_1 (clk, en, addr, dout);\r
-input clk;\r
-input en;\r
-input [5:0] addr;\r
-output [19:0] dout;\r
-\r
-(*rom_style = "block" *) reg [19:0] data;\r
-\r
-always @(posedge clk) \r
-begin \r
- if (en)\r
- case(addr)\r
- 6'b000000: data <= 20'h0200A; 6'b100000: data <= 20'h02222;\r
- 6'b000001: data <= 20'h00300; 6'b100001: data <= 20'h04001;\r
- 6'b000010: data <= 20'h08101; 6'b100010: data <= 20'h00342;\r
- 6'b000011: data <= 20'h04000; 6'b100011: data <= 20'h0232B;\r
- 6'b000100: data <= 20'h08601; 6'b100100: data <= 20'h00900;\r
- 6'b000101: data <= 20'h0233A; 6'b100101: data <= 20'h00302;\r
- 6'b000110: data <= 20'h00300; 6'b100110: data <= 20'h00102;\r
- 6'b000111: data <= 20'h08602; 6'b100111: data <= 20'h04002;\r
- 6'b001000: data <= 20'h02310; 6'b101000: data <= 20'h00900;\r
- 6'b001001: data <= 20'h0203B; 6'b101001: data <= 20'h08201;\r
- 6'b001010: data <= 20'h08300; 6'b101010: data <= 20'h02023;\r
- 6'b001011: data <= 20'h04002; 6'b101011: data <= 20'h00303;\r
- 6'b001100: data <= 20'h08201; 6'b101100: data <= 20'h02433;\r
- 6'b001101: data <= 20'h00500; 6'b101101: data <= 20'h00301;\r
- 6'b001110: data <= 20'h04001; 6'b101110: data <= 20'h04004;\r
- 6'b001111: data <= 20'h02500; 6'b101111: data <= 20'h00301;\r
- 6'b010000: data <= 20'h00340; 6'b110000: data <= 20'h00102;\r
- 6'b010001: data <= 20'h00241; 6'b110001: data <= 20'h02137;\r
- 6'b010010: data <= 20'h04002; 6'b110010: data <= 20'h02036;\r
- 6'b010011: data <= 20'h08300; 6'b110011: data <= 20'h00301;\r
- 6'b010100: data <= 20'h08201; 6'b110100: data <= 20'h00102;\r
- 6'b010101: data <= 20'h00500; 6'b110101: data <= 20'h02237;\r
- 6'b010110: data <= 20'h08101; 6'b110110: data <= 20'h04004;\r
- 6'b010111: data <= 20'h00602; 6'b110111: data <= 20'h00304;\r
- 6'b011000: data <= 20'h04003; 6'b111000: data <= 20'h04040;\r
- 6'b011001: data <= 20'h0241E; 6'b111001: data <= 20'h02500;\r
- 6'b011010: data <= 20'h00301; 6'b111010: data <= 20'h02500;\r
- 6'b011011: data <= 20'h00102; 6'b111011: data <= 20'h02500;\r
- 6'b011100: data <= 20'h02122; 6'b111100: data <= 20'h0030D;\r
- 6'b011101: data <= 20'h02021; 6'b111101: data <= 20'h02341;\r
- 6'b011110: data <= 20'h00301; 6'b111110: data <= 20'h08201;\r
- 6'b011111: data <= 20'h00102; 6'b111111: data <= 20'h0400D;\r
- endcase\r
-end \r
-\r
-assign dout = data;\r
-\r
-endmodule\r
+++ /dev/null
-read_verilog rams_sp_rom_1.v
-hierarchy -top rams_sp_rom_1
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd rams_sp_rom_1
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 1 t:BUFG
-select -assert-count 14 t:LUT6
-select -assert-count 14 t:FDRE
-
-select -assert-none t:BUFG t:LUT6 t:FDRE %% t:* %D
+++ /dev/null
-// Single-Port Block RAM Write-First Mode (recommended template)\r
-// File: rams_sp_wf.v\r
-module rams_sp_wf (clk, we, en, addr, di, dout);\r
-input clk; \r
-input we; \r
-input en;\r
-input [9:0] addr; \r
-input [15:0] di; \r
-output [15:0] dout;\r
-reg [15:0] RAM [1023:0];\r
-reg [15:0] dout;\r
-\r
-always @(posedge clk)\r
-begin\r
- if (en)\r
- begin\r
- if (we)\r
- begin\r
- RAM[addr] <= di;\r
- dout <= di;\r
- end\r
- else\r
- dout <= RAM[addr];\r
- end\r
-end\r
-endmodule\r
+++ /dev/null
-read_verilog rams_sp_wf.v
-hierarchy -top rams_sp_wf
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd rams_sp_wf
-stat
-#Vivado synthesizes 1 RAMB18E1.
-
-select -assert-count 1 t:BUFG
-select -assert-count 16 t:FDRE
-select -assert-count 44 t:LUT5
-select -assert-count 38 t:LUT6
-select -assert-count 10 t:MUXF7
-select -assert-count 128 t:RAM128X1D
-
-select -assert-none t:BUFG t:LUT2 t:FDRE t:LUT5 t:LUT6 t:MUXF7 t:RAM128X1D %% t:* %D
+++ /dev/null
-// Dual-Port Block RAM with Two Write Ports\r
-// File: rams_tdp_rf_rf.v\r
-\r
-module rams_tdp_rf_rf (clka,clkb,ena,enb,wea,web,addra,addrb,dia,dib,doa,dob);\r
-\r
-input clka,clkb,ena,enb,wea,web;\r
-input [9:0] addra,addrb;\r
-input [15:0] dia,dib;\r
-output [15:0] doa,dob;\r
-reg [15:0] ram [1023:0];\r
-reg [15:0] doa,dob;\r
-\r
-always @(posedge clka)\r
-begin \r
- if (ena)\r
- begin\r
- if (wea)\r
- ram[addra] <= dia;\r
- doa <= ram[addra];\r
- end\r
-end\r
-\r
-always @(posedge clkb) \r
-begin \r
- if (enb)\r
- begin\r
- if (web)\r
- ram[addrb] <= dib;\r
- dob <= ram[addrb];\r
- end\r
-end\r
-\r
-endmodule\r
+++ /dev/null
-read_verilog rams_tdp_rf_rf.v
-hierarchy -top rams_tdp_rf_rf
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd rams_tdp_rf_rf
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 1 t:$mem
-select -assert-count 2 t:LUT2
-
-select -assert-none t:$mem t:LUT2 %% t:* %D
+++ /dev/null
-// 8-bit Register with\r
-// Rising-edge Clock\r
-// Active-high Synchronous Clear\r
-// Active-high Clock Enable\r
-// File: registers_1.v\r
-\r
-module registers_1(d_in,ce,clk,clr,dout);\r
-input [7:0] d_in;\r
-input ce;\r
-input clk;\r
-input clr;\r
-output [7:0] dout;\r
-reg [7:0] d_reg;\r
-\r
-always @ (posedge clk)\r
-begin\r
- if(clr)\r
- d_reg <= 8'b0;\r
- else if(ce)\r
- d_reg <= d_in;\r
-end\r
-\r
-assign dout = d_reg;\r
-endmodule\r
-\r
+++ /dev/null
-read_verilog registers_1.v
-hierarchy -top registers_1
-proc
-flatten
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-cd registers_1 # Constrain all select calls below inside the top module
-#Vivado synthesizes 1 BUFG, 8 FDRE.
-select -assert-count 1 t:BUFG
-select -assert-count 8 t:FDRE
-select -assert-count 9 t:LUT2
-select -assert-none t:BUFG t:FDRE t:LUT2 %% t:* %D
+++ /dev/null
-#!/usr/bin/env bash
-set -e
-{
-echo "all::"
-for x in *.ys; do
- echo "all:: run-$x"
- echo "run-$x:"
- echo " @echo 'Running $x..'"
- echo " @../../yosys -ql ${x%.ys}.log $x"
-done
-for s in *.sh; do
- if [ "$s" != "run-test.sh" ]; then
- echo "all:: run-$s"
- echo "run-$s:"
- echo " @echo 'Running $s..'"
- echo " @bash $s"
- fi
-done
-} > run-test.mk
-exec ${MAKE:-make} -f run-test.mk
+++ /dev/null
-//sfir_shifter.v\r
-(* dont_touch = "yes" *)\r
-module sfir_shifter #(parameter dsize = 16, nbtap = 4)\r
- (input clk,input [dsize-1:0] datain, output [dsize-1:0] dataout);\r
-\r
- (* srl_style = "srl_register" *) reg [dsize-1:0] tmp [0:2*nbtap-1];\r
- integer i;\r
-\r
- always @(posedge clk)\r
- begin\r
- tmp[0] <= datain;\r
- for (i=0; i<=2*nbtap-2; i=i+1)\r
- tmp[i+1] <= tmp[i];\r
- end\r
-\r
- assign dataout = tmp[2*nbtap-1];\r
-\r
-endmodule\r
-// sfir_shifter\r
+++ /dev/null
-read_verilog sfir_shifter.v
-hierarchy -top sfir_shifter
-proc
-flatten
-#ERROR: Found 32 unproven $equiv cells in 'equiv_status -assert'.
-#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-
-cd sfir_shifter
-#Vivado synthesizes 32 FDRE, 16 SRL16E.
-stat
-select -assert-count 1 t:BUFG
-select -assert-count 16 t:SRL16E
-
-select -assert-none t:BUFG t:SRL16E %% t:* %D
+++ /dev/null
-// 8-bit Shift Register\r
-// Rising edge clock\r
-// Active high clock enable\r
-// Concatenation-based template\r
-// File: shift_registers_0.v\r
-\r
-module shift_registers_0 (clk, clken, SI, SO);\r
-parameter WIDTH = 32; \r
-input clk, clken, SI; \r
-output SO;\r
-\r
-reg [WIDTH-1:0] shreg;\r
-\r
-always @(posedge clk)\r
- begin\r
- if (clken)\r
- shreg = {shreg[WIDTH-2:0], SI};\r
- end\r
-\r
-assign SO = shreg[WIDTH-1];\r
-\r
-endmodule\r
+++ /dev/null
-read_verilog shift_registers_0.v
-hierarchy -top shift_registers_0
-proc
-flatten
-#ERROR: Found 2 unproven $equiv cells in 'equiv_status -assert'.
-#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-cd shift_registers_0 # Constrain all select calls below inside the top module
-#Vivado synthesizes 1 BUFG, 2 FDRE, 3 SRLC32E.
-select -assert-count 1 t:BUFG
-select -assert-count 1 t:SRLC32E
-select -assert-none t:BUFG t:SRLC32E %% t:* %D
+++ /dev/null
-// 32-bit Shift Register\r
-// Rising edge clock\r
-// Active high clock enable\r
-// For-loop based template\r
-// File: shift_registers_1.v\r
-\r
-module shift_registers_1 (clk, clken, SI, SO);\r
-parameter WIDTH = 32; \r
-input clk, clken, SI; \r
-output SO;\r
-reg [WIDTH-1:0] shreg;\r
-\r
-integer i;\r
-always @(posedge clk)\r
-begin\r
- if (clken)\r
- begin\r
- for (i = 0; i < WIDTH-1; i = i+1)\r
- shreg[i+1] <= shreg[i];\r
- shreg[0] <= SI; \r
- end\r
-end\r
-assign SO = shreg[WIDTH-1];\r
-endmodule\r
+++ /dev/null
-read_verilog shift_registers_1.v
-hierarchy -top shift_registers_1
-proc
-flatten
-#ERROR: Found 2 unproven $equiv cells in 'equiv_status -assert'.
-#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-cd shift_registers_1 # Constrain all select calls below inside the top module
-#Vivado synthesizes 1 BUFG, 2 FDRE, 3 SRLC32E.
-select -assert-count 1 t:BUFG
-select -assert-count 1 t:SRLC32E
-select -assert-none t:BUFG t:SRLC32E %% t:* %D
+++ /dev/null
-// This module performs subtraction of two inputs, squaring on the diff\r
-// and then accumulation\r
-// This can be implemented in 1 DSP Block (Ultrascale architecture)\r
-// File : squarediffmacc.v\r
-module squarediffmacc # (\r
- //Default parameters were changed because of slow test\r
- //parameter SIZEIN = 16,\r
- //SIZEOUT = 40\r
- parameter SIZEIN = 8,\r
- SIZEOUT = 20\r
- )\r
- (\r
- input clk,\r
- input ce,\r
- input sload,\r
- input signed [SIZEIN-1:0] a,\r
- input signed [SIZEIN-1:0] b,\r
- output signed [SIZEOUT+1:0] accum_out\r
- );\r
-\r
-// Declare registers for intermediate values\r
-reg signed [SIZEIN-1:0] a_reg, b_reg;\r
-reg signed [SIZEIN:0] diff_reg;\r
-reg sload_reg;\r
-reg signed [2*SIZEIN+1:0] m_reg;\r
-reg signed [SIZEOUT-1:0] adder_out, old_result;\r
-\r
- always @(sload_reg or adder_out)\r
- if (sload_reg)\r
- old_result <= 0;\r
- else\r
- // 'sload' is now and opens the accumulation loop.\r
- // The accumulator takes the next multiplier output\r
- // in the same cycle.\r
- old_result <= adder_out;\r
-\r
- always @(posedge clk)\r
- if (ce)\r
- begin\r
- a_reg <= a;\r
- b_reg <= b;\r
- diff_reg <= a_reg - b_reg;\r
- m_reg <= diff_reg * diff_reg;\r
- sload_reg <= sload;\r
- // Store accumulation result into a register\r
- adder_out <= old_result + m_reg;\r
- end\r
-\r
- // Output accumulation result\r
- assign accum_out = adder_out;\r
-\r
-endmodule // squarediffmacc\r
+++ /dev/null
-read_verilog squarediffmacc.v
-hierarchy -top squarediffmacc
-proc
-flatten
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-
-cd squarediffmacc
-#Vivado synthesizes 1 DSP48E1, 33 FDRE, 16 LUT.
-stat
-select -assert-count 1 t:BUFG
-select -assert-count 64 t:FDRE
-select -assert-count 78 t:LUT2
-select -assert-count 7 t:LUT3
-select -assert-count 11 t:LUT4
-select -assert-count 8 t:LUT5
-select -assert-count 125 t:LUT6
-select -assert-count 44 t:MUXCY
-select -assert-count 50 t:MUXF7
-select -assert-count 17 t:MUXF8
-select -assert-count 47 t:XORCY
-
-select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:XORCY %% t:* %D
+++ /dev/null
-// Squarer support for DSP block (DSP48E2) with \r
-// pre-adder configured\r
-// as subtractor\r
-// File: squarediffmult.v\r
-\r
-module squarediffmult # (parameter SIZEIN = 16)\r
- (\r
- input clk, ce, rst,\r
- input signed [SIZEIN-1:0] a, b,\r
- output signed [2*SIZEIN+1:0] square_out\r
- );\r
-\r
- // Declare registers for intermediate values\r
-reg signed [SIZEIN-1:0] a_reg, b_reg;\r
-reg signed [SIZEIN:0] diff_reg;\r
-reg signed [2*SIZEIN+1:0] m_reg, p_reg;\r
-\r
-always @(posedge clk)\r
-begin\r
- if (rst)\r
- begin\r
- a_reg <= 0;\r
- b_reg <= 0;\r
- diff_reg <= 0; \r
- m_reg <= 0;\r
- p_reg <= 0;\r
- end\r
- else\r
- if (ce)\r
- begin\r
- a_reg <= a;\r
- b_reg <= b;\r
- diff_reg <= a_reg - b_reg;\r
- m_reg <= diff_reg * diff_reg;\r
- p_reg <= m_reg; \r
- end\r
-end\r
-\r
-// Output result\r
-assign square_out = p_reg;\r
- \r
-endmodule // squarediffmult\r
+++ /dev/null
-read_verilog squarediffmult.v
-hierarchy -top squarediffmult
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd squarediffmult
-stat
-#Vivado synthesizes 16 FDRE, 1 DSP48E1.
-select -assert-count 1 t:BUFG
-select -assert-count 117 t:FDRE
-select -assert-count 223 t:LUT2
-select -assert-count 50 t:LUT3
-select -assert-count 38 t:LUT4
-select -assert-count 56 t:LUT5
-select -assert-count 372 t:LUT6
-select -assert-count 49 t:MUXCY
-select -assert-count 99 t:MUXF7
-select -assert-count 26 t:MUXF8
-select -assert-count 51 t:XORCY
-
-select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:XORCY %% t:* %D
+++ /dev/null
-// Multiplexer using case statement \r
-module mux4 (sel, a, b, c, d, outmux);\r
-input [1:0] sel;\r
-input [1:0] a, b, c, d;\r
-output [1:0] outmux;\r
-reg [1:0] outmux;\r
-\r
-always @ *\r
- begin \r
- case(sel)\r
- 2'b00 : outmux = a;\r
- 2'b01 : outmux = b;\r
- 2'b10 : outmux = c;\r
- 2'b11 : outmux = d;\r
- endcase\r
- end \r
-endmodule\r
-\r
+++ /dev/null
-read_verilog top_mux.v
-hierarchy -top mux4
-proc
-flatten
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-
-cd mux4
-#Vivado synthesizes 2 LUT.
-stat
-select -assert-count 2 t:LUT6
-
-select -assert-none t:LUT6 %% t:* %D
+++ /dev/null
-// Tristate Description Using Combinatorial Always Block\r
-// File: tristates_1.v\r
-//\r
-module tristates_1 (T, I, O);\r
-input T, I;\r
-output O;\r
-reg O;\r
-\r
-always @(T or I)\r
-begin\r
- if (~T)\r
- O = I;\r
- else\r
- O = 1'bZ;\r
-end\r
-\r
-endmodule\r
+++ /dev/null
-read_verilog tristates_1.v
-hierarchy -top tristates_1
-proc
-tribuf
-flatten
-synth
-equiv_opt -assert -map +/xilinx/cells_sim.v -map +/simcells.v synth_xilinx # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-cd tristates_1 # Constrain all select calls below inside the top module
-#Vivado synthesizes 3 IBUF, 1 OBUFT.
-select -assert-count 1 t:LUT1
-select -assert-count 1 t:$_TBUF_
-select -assert-none t:LUT1 t:$_TBUF_ %% t:* %D
+++ /dev/null
-// Tristate Description Using Concurrent Assignment\r
-// File: tristates_2.v\r
-//\r
-module tristates_2 (T, I, O);\r
-input T, I;\r
-output O;\r
-\r
-assign O = (~T) ? I: 1'bZ;\r
-\r
-endmodule\r
+++ /dev/null
-read_verilog tristates_2.v
-hierarchy -top tristates_2
-proc
-tribuf
-flatten
-synth
-equiv_opt -assert -map +/xilinx/cells_sim.v -map +/simcells.v synth_xilinx # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-cd tristates_2 # Constrain all select calls below inside the top module
-#Vivado synthesizes 3 IBUF, 1 OBUFT.
-select -assert-count 1 t:LUT1
-select -assert-count 1 t:$_TBUF_
-select -assert-none t:LUT1 t:$_TBUF_ %% t:* %D
+++ /dev/null
-// Xilinx UltraRAM Single Port No Change Mode. This code implements\r
-// a parameterizable UltraRAM block in No Change mode. The behavior of this RAM is\r
-// when data is written, the output of RAM is unchanged. Only when write is\r
-// inactive data corresponding to the address is presented on the output port.\r
-//\r
-module xilinx_ultraram_single_port_no_change #(\r
-//Default parameters were changed because of slow test\r
- //parameter AWIDTH = 12, // Address Width\r
- //parameter DWIDTH = 72, // Data Width\r
- //parameter NBPIPE = 3 // Number of pipeline Registers\r
- parameter AWIDTH = 8, // Address Width\r
- parameter DWIDTH = 8, // Data Width\r
- parameter NBPIPE = 3 // Number of pipeline Registers\r
- ) (\r
- input clk, // Clock\r
- input rst, // Reset\r
- input we, // Write Enable\r
- input regce, // Output Register Enable\r
- input mem_en, // Memory Enable\r
- input [DWIDTH-1:0] din, // Data Input\r
- input [AWIDTH-1:0] addr, // Address Input\r
- output reg [DWIDTH-1:0] dout // Data Output\r
- );\r
-\r
-(* ram_style = "ultra" *)\r
-reg [DWIDTH-1:0] mem[(1<<AWIDTH)-1:0]; // Memory Declaration\r
-reg [DWIDTH-1:0] memreg;\r
-reg [DWIDTH-1:0] mem_pipe_reg[NBPIPE-1:0]; // Pipelines for memory\r
-reg mem_en_pipe_reg[NBPIPE:0]; // Pipelines for memory enable\r
-\r
-integer i;\r
-\r
-// RAM : Read has one latency, Write has one latency as well.\r
-always @ (posedge clk)\r
-begin\r
- if(mem_en)\r
- begin\r
- if(we)\r
- mem[addr] <= din;\r
- else\r
- memreg <= mem[addr];\r
- end\r
-end\r
-// The enable of the RAM goes through a pipeline to produce a\r
-// series of pipelined enable signals required to control the data\r
-// pipeline.\r
-always @ (posedge clk)\r
-begin\r
-mem_en_pipe_reg[0] <= mem_en;\r
- for (i=0; i<NBPIPE; i=i+1)\r
- mem_en_pipe_reg[i+1] <= mem_en_pipe_reg[i];\r
-end\r
-\r
-// RAM output data goes through a pipeline.\r
-always @ (posedge clk)\r
-begin\r
- if (mem_en_pipe_reg[0])\r
- mem_pipe_reg[0] <= memreg;\r
-end\r
-\r
-always @ (posedge clk)\r
-begin\r
- for (i = 0; i < NBPIPE-1; i = i+1)\r
- if (mem_en_pipe_reg[i+1])\r
- mem_pipe_reg[i+1] <= mem_pipe_reg[i];\r
-end\r
-\r
-// Final output register gives user the option to add a reset and\r
-// an additional enable signal just for the data ouptut\r
-always @ (posedge clk)\r
-begin\r
- if (rst)\r
- dout <= 0;\r
- else if (mem_en_pipe_reg[NBPIPE] && regce)\r
- dout <= mem_pipe_reg[NBPIPE-1];\r
-end\r
-endmodule\r
-\r
+++ /dev/null
-read_verilog xilinx_ultraram_single_port_no_change.v
-hierarchy -top xilinx_ultraram_single_port_no_change
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd xilinx_ultraram_single_port_no_change
-stat
-#Vivado synthesizes 1 RAMB36E1, 28 FDRE.
-select -assert-count 1 t:BUFG
-select -assert-count 53 t:FDRE
-select -assert-count 1 t:LUT1
-select -assert-count 9 t:LUT2
-select -assert-count 11 t:LUT3
-select -assert-count 16 t:RAM128X1D
-
-select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT2 t:LUT3 t:RAM128X1D %% t:* %D
+++ /dev/null
-// Xilinx UltraRAM Single Port Read First Mode. This code implements\r
-// a parameterizable UltraRAM block in read first mode. The behavior of this RAM is\r
-// when data is written, the old memory contents at the write address are\r
-// presented on the output port.\r
-//\r
-module xilinx_ultraram_single_port_read_first #(\r
-\r
-//Default parameters were changed because of slow test\r
- //parameter AWIDTH = 12, // Address Width\r
- //parameter DWIDTH = 72, // Data Width\r
- //parameter NBPIPE = 3 // Number of pipeline Registers\r
- parameter AWIDTH = 8, // Address Width\r
- parameter DWIDTH = 8, // Data Width\r
- parameter NBPIPE = 3 // Number of pipeline Registers\r
- ) (\r
- input clk, // Clock\r
- input rst, // Reset\r
- input we, // Write Enable\r
- input regce, // Output Register Enable\r
- input mem_en, // Memory Enable\r
- input [DWIDTH-1:0] din, // Data Input\r
- input [AWIDTH-1:0] addr, // Address Input\r
- output reg [DWIDTH-1:0] dout // Data Output\r
- );\r
-\r
-(* ram_style = "ultra" *)\r
-reg [DWIDTH-1:0] mem[(1<<AWIDTH)-1:0]; // Memory Declaration\r
-reg [DWIDTH-1:0] memreg;\r
-reg [DWIDTH-1:0] mem_pipe_reg[NBPIPE-1:0]; // Pipelines for memory\r
-reg mem_en_pipe_reg[NBPIPE:0]; // Pipelines for memory enable\r
-\r
-integer i;\r
-\r
-// RAM : Both READ and WRITE have a latency of one\r
-always @ (posedge clk)\r
-begin\r
- if(mem_en)\r
- begin\r
- if(we)\r
- mem[addr] <= din;\r
- memreg <= mem[addr];\r
- end\r
-end\r
-\r
-// The enable of the RAM goes through a pipeline to produce a\r
-// series of pipelined enable signals required to control the data\r
-// pipeline.\r
-always @ (posedge clk)\r
-begin\r
- mem_en_pipe_reg[0] <= mem_en;\r
- for (i=0; i<NBPIPE; i=i+1)\r
- mem_en_pipe_reg[i+1] <= mem_en_pipe_reg[i];\r
-end\r
-\r
-// RAM output data goes through a pipeline.\r
-always @ (posedge clk)\r
-begin\r
- if (mem_en_pipe_reg[0])\r
- mem_pipe_reg[0] <= memreg;\r
-end\r
-\r
-always @ (posedge clk)\r
-begin\r
- for (i = 0; i < NBPIPE-1; i = i+1)\r
- if (mem_en_pipe_reg[i+1])\r
- mem_pipe_reg[i+1] <= mem_pipe_reg[i];\r
-end\r
-\r
-// Final output register gives user the option to add a reset and\r
-// an additional enable signal just for the data ouptut\r
-always @ (posedge clk)\r
-begin\r
- if (rst)\r
- dout <= 0;\r
- else if (mem_en_pipe_reg[NBPIPE] && regce)\r
- dout <= mem_pipe_reg[NBPIPE-1];\r
-end\r
-endmodule\r
+++ /dev/null
-read_verilog xilinx_ultraram_single_port_read_first.v
-hierarchy -top xilinx_ultraram_single_port_read_first
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd xilinx_ultraram_single_port_read_first
-#Vivado synthesizes 1 RAMB18E1, 28 FDRE.
-select -assert-count 1 t:BUFG
-select -assert-count 53 t:FDRE
-select -assert-count 1 t:LUT1
-select -assert-count 8 t:LUT2
-select -assert-count 11 t:LUT3
-select -assert-count 16 t:RAM128X1D
-
-select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT2 t:LUT3 t:RAM128X1D %% t:* %D
+++ /dev/null
-// Xilinx UltraRAM Single Port Write First Mode. This code implements\r
-// a parameterizable UltraRAM block in write first mode. The behavior of this RAM is\r
-// when data is written, the new memory contents at the write address are\r
-// presented on the output port.\r
-//\r
-module xilinx_ultraram_single_port_write_first #(\r
-\r
-//Default parameters were changed because of slow test\r
- //parameter AWIDTH = 12, // Address Width\r
- //parameter DWIDTH = 72, // Data Width\r
- //parameter NBPIPE = 3 // Number of pipeline Registers\r
- parameter AWIDTH = 8, // Address Width\r
- parameter DWIDTH = 8, // Data Width\r
- parameter NBPIPE = 3 // Number of pipeline Registers\r
- ) (\r
- input clk, // Clock\r
- input rst, // Reset\r
- input we, // Write Enable\r
- input regce, // Output Register Enable\r
- input mem_en, // Memory Enable\r
- input [DWIDTH-1:0] din, // Data Input\r
- input [AWIDTH-1:0] addr, // Address Input\r
- output reg [DWIDTH-1:0] dout // Data Output\r
- );\r
-\r
-(* ram_style = "ultra" *)\r
-reg [DWIDTH-1:0] mem[(1<<AWIDTH)-1:0]; // Memory Declaration\r
-reg [DWIDTH-1:0] memreg;\r
-reg [DWIDTH-1:0] mem_pipe_reg[NBPIPE-1:0]; // Pipelines for memory\r
-reg mem_en_pipe_reg[NBPIPE:0]; // Pipelines for memory enable\r
-\r
-integer i;\r
-\r
-// RAM : Both READ and WRITE have a latency of one\r
-always @ (posedge clk)\r
-begin\r
- if(mem_en)\r
- begin\r
- if(we)\r
- begin\r
- mem[addr] <= din;\r
- memreg <= din;\r
- end\r
- else\r
- memreg <= mem[addr];\r
- end\r
-end\r
-\r
-// The enable of the RAM goes through a pipeline to produce a\r
-// series of pipelined enable signals required to control the data\r
-// pipeline.\r
-always @ (posedge clk)\r
-begin\r
- mem_en_pipe_reg[0] <= mem_en;\r
- for (i=0; i<NBPIPE; i=i+1)\r
- mem_en_pipe_reg[i+1] <= mem_en_pipe_reg[i];\r
-end\r
-\r
-// RAM output data goes through a pipeline.\r
-always @ (posedge clk)\r
-begin\r
- if (mem_en_pipe_reg[0])\r
- mem_pipe_reg[0] <= memreg;\r
-end\r
-\r
-always @ (posedge clk)\r
-begin\r
- for (i = 0; i < NBPIPE-1; i = i+1)\r
- if (mem_en_pipe_reg[i+1])\r
- mem_pipe_reg[i+1] <= mem_pipe_reg[i];\r
-end\r
-\r
-// Final output register gives user the option to add a reset and\r
-// an additional enable signal just for the data ouptut\r
-always @ (posedge clk)\r
-begin\r
- if (rst)\r
- dout <= 0;\r
- else if (mem_en_pipe_reg[NBPIPE] && regce)\r
- dout <= mem_pipe_reg[NBPIPE-1];\r
-end\r
-endmodule\r
+++ /dev/null
-read_verilog xilinx_ultraram_single_port_write_first.v
-hierarchy -top xilinx_ultraram_single_port_write_first
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-memory
-opt -full
-
-# TODO
-#equiv_opt -run prove: -assert null
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
-
-design -load postopt
-cd xilinx_ultraram_single_port_write_first
-#Vivado synthesizes 1 RAMB18E1, 28 FDRE.
-select -assert-count 1 t:BUFG
-select -assert-count 44 t:FDRE
-select -assert-count 8 t:LUT5
-select -assert-count 8 t:LUT2
-select -assert-count 3 t:LUT3
-select -assert-count 16 t:RAM128X1D
-
-select -assert-none t:BUFG t:FDRE t:LUT5 t:LUT2 t:LUT3 t:RAM128X1D %% t:* %D
projects / yosys.git / commitdiff