mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-03 21:09:12 +00:00
Code Activity

Merge pull request #2078 from YosysHQ/eddie/xilinx_sim_tidy

Browse source 
xilinx: tidy up cells_sim.v a little
This commit is contained in:
Eddie Hung 2020-05-25 14:21:10 -07:00 • committed by GitHub
commit a7f2ef6d34
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 15 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

12
tests/arch/xilinx/macc.v
View file

@ -10,10 +10,10 @@ module macc # (parameter SIZEIN = 16, SIZEOUT = 40) (
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;
reg signed [SIZEIN-1:0] a_reg = 0, b_reg = 0;
reg sload_reg = 0;
reg signed [2*SIZEIN-1:0] mult_reg = 0;
reg signed [SIZEOUT-1:0] adder_out = 0, old_result;
always @* /*(adder_out or sload_reg)*/ begin // Modification necessary to fix sim/synth mismatch
if (sload_reg)
old_result <= 0;
@ -50,10 +50,10 @@ module macc2 # (parameter SIZEIN = 16, SIZEOUT = 40) (
output overflow
);
// Declare registers for intermediate values
reg signed [SIZEIN-1:0] a_reg, b_reg, a_reg2, b_reg2;
reg signed [SIZEIN-1:0] a_reg = 0, b_reg = 0, a_reg2 = 0, b_reg2 = 0;
reg signed [2*SIZEIN-1:0] mult_reg = 0;
reg signed [SIZEOUT:0] adder_out = 0;
reg overflow_reg;
reg overflow_reg = 0;
always @(posedge clk) begin
//if (ce)
begin

4
tests/arch/xilinx/macc.ys
View file

@ -6,7 +6,7 @@ proc
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter
sat -verify -prove-asserts -seq 3 -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
@ -20,7 +20,7 @@ proc
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter
sat -verify -prove-asserts -seq 4 -show-inputs -show-outputs miter
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd macc2 # Constrain all select calls below inside the top module