riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Update macc test

This commit is contained in:
Eddie Hung 2019-09-06 23:19:03 -07:00
parent 74a5c802f7
commit e68507a716
2 changed files with 42 additions and 42 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

66
tests/xilinx/macc.v
View File

@ -1,37 +1,41 @@
// Signed 40-bit streaming accumulator with 16-bit inputs
// File: HDL_Coding_Techniques/multipliers/multipliers4.v
//
module macc # (parameter SIZEIN = /*16*/7, SIZEOUT = 40)
(input clk, ce, sload,
input signed [SIZEIN-1:0] a, b,
output signed [SIZEOUT-1:0] accum_out);
// Declare registers for intermediate values
reg signed [SIZEIN-1:0] a_reg, b_reg;
reg sload_reg;
reg signed [2*SIZEIN:0] mult_reg;
reg signed [SIZEOUT-1:0] adder_out, old_result;
always @(adder_out or sload_reg) begin
//if (sload_reg)
//old_result <= 0;
//else
// 'sload' is now active (=low) and opens the accumulation loop.
// The accumulator takes the next multiplier output in
// the same cycle.
old_result <= adder_out;
a_reg <= a;
b_reg <= b;
end
// Source:
// https://www.xilinx.com/support/documentation/sw_manuals/xilinx2014_2/ug901-vivado-synthesis.pdf p.90
//
module macc # (parameter SIZEIN = 16, SIZEOUT = 40) (
input clk, ce, sload,
input signed [SIZEIN-1:0] a, b,
output signed [SIZEOUT-1:0] accum_out
);
// Declare registers for intermediate values
reg signed [SIZEIN-1:0] a_reg, b_reg;
reg sload_reg;
reg signed [2*SIZEIN-1:0] mult_reg;
reg signed [SIZEOUT-1:0] adder_out, old_result;
always @* /*(adder_out or sload_reg)*/ begin // Modification necessary to fix sim/synth mismatch
if (sload_reg)
old_result <= 0;
else
// 'sload' is now active (=low) and opens the accumulation loop.
// The accumulator takes the next multiplier output in
// the same cycle.
old_result <= adder_out;
end
always @(posedge clk)
//if (ce)
begin
mult_reg <= a_reg * b_reg;
sload_reg <= sload;
// Store accumulation result into a register
adder_out <= old_result + mult_reg;
end
always @(posedge clk)
if (ce)
begin
a_reg <= a;
b_reg <= b;
mult_reg <= a_reg * b_reg;
sload_reg <= sload;
// Store accumulation result into a register
adder_out <= old_result + mult_reg;
end
// Output accumulation result
assign accum_out = adder_out;
// Output accumulation result
assign accum_out = adder_out;
endmodule // macc
endmodule

18
tests/xilinx/macc.ys
View File

@ -1,17 +1,13 @@
read_verilog macc.v
proc
hierarchy -top macc
equiv_opt -run :restore -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
#equiv_miter -trigger miter equiv
#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
#equiv_opt -assert -run :prove -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
#miter -equiv -flatten -make_assert -make_outputs gold gate miter
#sat -set-init-zero -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter
hierarchy -auto-top
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd macc # Constrain all select calls below inside the top module
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-count 1 t:DSP48E1
select -assert-none t:BUFG t:DSP48E1 %% t:* %D
select -assert-none t:BUFG t:FDRE t:DSP48E1 %% t:* %D