+cd tests/arch && bash run-test.sh
+cd tests/ice40 && bash run-test.sh $(SEEDOPT)
+cd tests/rpc && bash run-test.sh
+ +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
+
+#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
+#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
+
+#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