mirror of
https://github.com/YosysHQ/yosys
synced 2026-06-29 03:58:50 +00:00
End of file fix
This commit is contained in:
parent
3ac58b3ac1
commit
48a3dcc02a
304 changed files with 64 additions and 321 deletions
|
|
@ -47,4 +47,3 @@ chparam -set SIZEA 768
|
|||
chparam -set WIDTHB 24 -set SIZEB 128 -set ADDRWIDTHB 7 asym_ram_sdp_read_wider
|
||||
synth_analogdevices -top asym_ram_sdp_read_wider -noiopad
|
||||
select -assert-count 2 t:RBRAM2
|
||||
|
||||
|
|
|
|||
|
|
@ -38,4 +38,3 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p
|
|||
cd dffe # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:FFRE
|
||||
select -assert-none t:FFRE %% t:* %D
|
||||
|
||||
|
|
|
|||
|
|
@ -39,4 +39,3 @@ techmap -autoproc -wb -map +/analogdevices/cells_sim.v
|
|||
opt -full -fine
|
||||
select -assert-count 0 t:* t:$assert %d
|
||||
sat -verify -prove-asserts
|
||||
|
||||
|
|
|
|||
|
|
@ -325,4 +325,3 @@ module double_sync_ram_tdp #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=10)
|
|||
);
|
||||
|
||||
endmodule // double_sync_ram_tdp
|
||||
|
||||
|
|
|
|||
|
|
@ -85,4 +85,3 @@ module distributed_ram_manual_syn #(parameter DATA_WIDTH=8, ADDRESS_WIDTH=4)
|
|||
|
||||
assign data_out = data_out_r;
|
||||
endmodule // distributed_ram
|
||||
|
||||
|
|
|
|||
|
|
@ -9,4 +9,3 @@ select -assert-max 26 t:LUT4
|
|||
select -assert-count 10 t:PFUMX
|
||||
select -assert-count 6 t:L6MUX21
|
||||
select -assert-none t:LUT4 t:PFUMX t:L6MUX21 %% t:* %D
|
||||
|
||||
|
|
|
|||
|
|
@ -16,4 +16,4 @@ equiv_opt -assert -map +/ecp5/cells_sim.v synth_ecp5 # equivalency check
|
|||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd dffe # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:TRELLIS_FF
|
||||
select -assert-none t:TRELLIS_FF %% t:* %D
|
||||
select -assert-none t:TRELLIS_FF %% t:* %D
|
||||
|
|
|
|||
|
|
@ -7,4 +7,3 @@ cd top # Constrain all select calls below inside the top module
|
|||
select -assert-count 10 t:EFX_ADD
|
||||
select -assert-count 4 t:EFX_LUT4
|
||||
select -assert-none t:EFX_ADD t:EFX_LUT4 %% t:* %D
|
||||
|
||||
|
|
|
|||
|
|
@ -10,4 +10,3 @@ select -assert-count 8 t:IBUF
|
|||
select -assert-count 1 t:GND
|
||||
select -assert-count 1 t:VCC
|
||||
select -assert-none t:ALU t:OBUF t:IBUF t:GND t:VCC %% t:* %D
|
||||
|
||||
|
|
|
|||
|
|
@ -5,5 +5,3 @@ equiv_opt -assert -map +/gowin/cells_sim.v synth_gowin # equivalency check
|
|||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd top # Constrain all select calls below inside the top module
|
||||
select -assert-count 5 t:ALU
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -11,4 +11,4 @@ cd tristate # Constrain all select calls below inside the top module
|
|||
select -assert-count 1 t:TBUF
|
||||
select -assert-count 1 t:LUT1
|
||||
select -assert-count 2 t:IBUF
|
||||
select -assert-none t:TBUF t:IBUF t:LUT1 %% t:* %D
|
||||
select -assert-none t:TBUF t:IBUF t:LUT1 %% t:* %D
|
||||
|
|
|
|||
|
|
@ -6,4 +6,3 @@ cd top # Constrain all select calls below inside the top module
|
|||
select -assert-count 10 t:SB_LUT4
|
||||
select -assert-count 6 t:SB_CARRY
|
||||
select -assert-none t:SB_LUT4 t:SB_CARRY %% t:* %D
|
||||
|
||||
|
|
|
|||
|
|
@ -16,4 +16,4 @@ equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check
|
|||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd dffe # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:SB_DFFE
|
||||
select -assert-none t:SB_DFFE %% t:* %D
|
||||
select -assert-none t:SB_DFFE %% t:* %D
|
||||
|
|
|
|||
|
|
@ -6,4 +6,3 @@ cd top # Constrain all select calls below inside the top module
|
|||
stat
|
||||
select -assert-count 9 t:MISTRAL_ALUT_ARITH
|
||||
select -assert-none t:MISTRAL_ALUT_ARITH %% t:* %D
|
||||
|
||||
|
|
|
|||
|
|
@ -45,4 +45,3 @@ select -assert-count 1 t:MISTRAL_FF
|
|||
select -assert-count 2 t:MISTRAL_NOT
|
||||
|
||||
select -assert-none t:MISTRAL_FF t:MISTRAL_NOT %% t:* %D
|
||||
|
||||
|
|
|
|||
|
|
@ -5,4 +5,3 @@ cd sync_ram_sdp
|
|||
select -assert-count 1 t:MISTRAL_NOT
|
||||
select -assert-count 1 t:MISTRAL_M10K
|
||||
select -assert-none t:MISTRAL_NOT t:MISTRAL_M10K %% t:* %D
|
||||
|
||||
|
|
|
|||
|
|
@ -10,4 +10,3 @@ select -assert-count 2 t:MISTRAL_NOT
|
|||
select -assert-count 8 t:MISTRAL_ALUT_ARITH
|
||||
select -assert-count 8 t:MISTRAL_FF
|
||||
select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT_ARITH t:MISTRAL_FF %% t:* %D
|
||||
|
||||
|
|
|
|||
|
|
@ -18,4 +18,3 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p
|
|||
cd dffe # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:MISTRAL_FF
|
||||
select -assert-none t:MISTRAL_FF %% t:* %D
|
||||
|
||||
|
|
|
|||
|
|
@ -19,4 +19,3 @@ select -assert-max 2 t:MISTRAL_ALUT4 # Clang returns 0, GCC returns 1
|
|||
select -assert-max 6 t:MISTRAL_ALUT5 # Clang returns 5, GCC returns 4
|
||||
select -assert-max 2 t:MISTRAL_ALUT6 # Clang returns 1, GCC returns 2
|
||||
select -assert-none t:MISTRAL_FF t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_ALUT4 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D
|
||||
|
||||
|
|
|
|||
|
|
@ -9,4 +9,3 @@ select -assert-count 1 t:MISTRAL_NOT
|
|||
select -assert-count 6 t:MISTRAL_ALUT2
|
||||
select -assert-count 2 t:MISTRAL_ALUT4
|
||||
select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT4 %% t:* %D
|
||||
|
||||
|
|
|
|||
|
|
@ -37,4 +37,3 @@ select -assert-count 2 t:MISTRAL_ALUT2
|
|||
select -assert-count 8 t:MISTRAL_ALUT3
|
||||
select -assert-count 8 t:MISTRAL_FF
|
||||
select -assert-none t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_FF t:MISTRAL_MLAB %% t:* %D
|
||||
|
||||
|
|
|
|||
|
|
@ -32,4 +32,3 @@ cd top # Constrain all select calls below inside the top module
|
|||
|
||||
select -assert-count 1 t:MISTRAL_MUL27X27
|
||||
select -assert-none t:MISTRAL_MUL27X27 %% t:* %D
|
||||
|
||||
|
|
|
|||
|
|
@ -42,4 +42,3 @@ select -assert-max 1 t:MISTRAL_ALUT3
|
|||
select -assert-max 2 t:MISTRAL_ALUT5
|
||||
select -assert-max 5 t:MISTRAL_ALUT6
|
||||
select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D
|
||||
|
||||
|
|
|
|||
|
|
@ -7,4 +7,3 @@ design -load postopt # load the post-opt design (otherwise equiv_opt loads the p
|
|||
cd top # Constrain all select calls below inside the top module
|
||||
select -assert-count 8 t:MISTRAL_FF
|
||||
select -assert-none t:MISTRAL_FF %% t:* %D
|
||||
|
||||
|
|
|
|||
|
|
@ -10,4 +10,3 @@ cd tristate # Constrain all select calls below inside the top module
|
|||
#Internal cell type used. Need support it.
|
||||
select -assert-count 1 t:$_TBUF_
|
||||
select -assert-none t:$_TBUF_ %% t:* %D
|
||||
|
||||
|
|
|
|||
1
tests/arch/microchip/.gitignore
vendored
1
tests/arch/microchip/.gitignore
vendored
|
|
@ -1,2 +1 @@
|
|||
*.vm
|
||||
|
||||
|
|
|
|||
|
|
@ -73,4 +73,4 @@ synth_microchip -top dffs -family polarfire -noiopad
|
|||
select -assert-count 1 t:SLE
|
||||
select -assert-count 1 t:CLKBUF
|
||||
select -assert-count 1 t:CFG1
|
||||
select -assert-none t:SLE t:CLKBUF t:CFG1 %% t:* %D
|
||||
select -assert-none t:SLE t:CLKBUF t:CFG1 %% t:* %D
|
||||
|
|
|
|||
|
|
@ -39,4 +39,4 @@ synth_microchip -top dff_opt -family polarfire -noiopad
|
|||
select -assert-count 1 t:SLE
|
||||
select -assert-count 1 t:CFG4
|
||||
select -assert-count 1 t:CLKBUF
|
||||
select -assert-none t:SLE t:CFG4 t:CLKBUF %% t:* %D
|
||||
select -assert-none t:SLE t:CFG4 t:CLKBUF %% t:* %D
|
||||
|
|
|
|||
|
|
@ -47,4 +47,4 @@ hierarchy -top sync_ram_sdp
|
|||
chparam -set DATA_WIDTH 32 -set ADDRESS_WIDTH 8
|
||||
synth_microchip -top sync_ram_sdp -family polarfire -noiopad
|
||||
select -assert-count 1 t:RAM1K20
|
||||
select -assert-none t:RAM1K20 %% t:* %D
|
||||
select -assert-none t:RAM1K20 %% t:* %D
|
||||
|
|
|
|||
|
|
@ -61,4 +61,4 @@ chparam -set DATA_WIDTH 2 -set ADDRESS_WIDTH 10
|
|||
synth_microchip -top sync_ram_tdp -family polarfire -noiopad
|
||||
select -assert-count 1 t:RAM1K20
|
||||
select -assert-count 2 t:CFG1
|
||||
select -assert-none t:RAM1K20 t:CFG1 %% t:* %D
|
||||
select -assert-none t:RAM1K20 t:CFG1 %% t:* %D
|
||||
|
|
|
|||
|
|
@ -25,4 +25,3 @@ EOT
|
|||
synth_microchip -top reduce -family polarfire -noiopad
|
||||
select -assert-count 1 t:XOR8
|
||||
select -assert-none t:XOR8 %% t:* %D
|
||||
|
||||
|
|
|
|||
|
|
@ -19,4 +19,4 @@ hierarchy -top sync_ram_sp
|
|||
chparam -set DATA_WIDTH 20 -set ADDRESS_WIDTH 10
|
||||
synth_microchip -top sync_ram_sp -family polarfire -noiopad
|
||||
select -assert-count 1 t:RAM1K20
|
||||
select -assert-none t:RAM1K20 %% t:* %D
|
||||
select -assert-none t:RAM1K20 %% t:* %D
|
||||
|
|
|
|||
|
|
@ -38,4 +38,4 @@ equiv_opt -assert -map +/microchip/cells_sim.v synth_microchip -top mux4 -family
|
|||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd mux4 # Constrain all select calls below inside the top module
|
||||
select -assert-count 3 t:CFG3
|
||||
select -assert-none t:CFG3 %% t:* %D
|
||||
select -assert-none t:CFG3 %% t:* %D
|
||||
|
|
|
|||
|
|
@ -47,4 +47,3 @@ chparam -set SIZEA 768
|
|||
chparam -set WIDTHB 24 -set SIZEB 128 -set ADDRWIDTHB 7 asym_ram_sdp_read_wider
|
||||
synth_xilinx -top asym_ram_sdp_read_wider -noiopad
|
||||
select -assert-count 1 t:RAMB18E1
|
||||
|
||||
|
|
|
|||
|
|
@ -69,4 +69,4 @@ module asym_ram_sdp_read_wider (clkA, clkB, enaA, weA, enaB, addrA, addrB, diA,
|
|||
end
|
||||
end
|
||||
assign doB = readB;
|
||||
endmodule
|
||||
endmodule
|
||||
|
|
|
|||
|
|
@ -68,4 +68,4 @@ module asym_ram_sdp_write_wider (clkA, clkB, weA, enaA, enaB, addrA, addrB, diA,
|
|||
end
|
||||
end
|
||||
end
|
||||
endmodule
|
||||
endmodule
|
||||
|
|
|
|||
|
|
@ -42,4 +42,3 @@ cd dffe # Constrain all select calls below inside the top module
|
|||
select -assert-count 1 t:BUFG
|
||||
select -assert-count 1 t:FDRE
|
||||
select -assert-none t:BUFG t:FDRE %% t:* %D
|
||||
|
||||
|
|
|
|||
|
|
@ -87,4 +87,3 @@ select -assert-none t:DSP48A1 t:BUFG t:FDRE %% t:* %D
|
|||
# Very crude method of checking that DSP48E1.PCOUT -> DSP48E1.PCIN
|
||||
# (see above for explanation)
|
||||
select -assert-count 1 t:DSP48A1 %co:+[PCOUT] t:DSP48A1 %d %co:+[PCIN] w:* %d t:DSP48A1 %i
|
||||
|
||||
|
|
|
|||
|
|
@ -104,4 +104,4 @@ equiv_opt -assert arith_tree
|
|||
design -load postopt
|
||||
select -assert-min 1 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
design -reset
|
||||
|
|
|
|||
|
|
@ -67,4 +67,3 @@ select -assert-none t:$add
|
|||
select -assert-min 1 t:$_AND_
|
||||
select -assert-min 1 t:$_XOR_
|
||||
design -reset
|
||||
|
||||
|
|
|
|||
|
|
@ -26,4 +26,3 @@ end
|
|||
|
||||
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -98,4 +98,3 @@ if (count_compare != count) begin
|
|||
end
|
||||
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -324,4 +324,3 @@ def create_tests():
|
|||
)
|
||||
|
||||
gen_tests_makefile.generate_custom(create_tests)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,3 @@
|
|||
module a;
|
||||
integer [31:0]w;
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -4,4 +4,3 @@ task to (
|
|||
);
|
||||
endtask
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -4,4 +4,3 @@ task to (
|
|||
);
|
||||
endtask
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,3 @@
|
|||
module a;
|
||||
wire [3]x;
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,3 @@
|
|||
module a;
|
||||
input x[2:0];
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -3,4 +3,3 @@ initial
|
|||
begin : label1
|
||||
end: label2
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -3,4 +3,3 @@ wire [5:0]x;
|
|||
wire [3:0]y;
|
||||
assign y = (4)55;
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -3,4 +3,3 @@ wire [5:0]x;
|
|||
wire [3:0]y;
|
||||
assign y = x 55;
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -1,3 +1,2 @@
|
|||
module a(input wire x = 1'b0);
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,3 @@
|
|||
module a #(p = 0)
|
||||
();
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -378,4 +378,4 @@ def generate_test_cases(per_cell, rnd):
|
|||
names.append(f'{cell.name}-{name}' if name != '' else cell.name)
|
||||
if per_cell is not None and len(seen_names) >= per_cell:
|
||||
break
|
||||
return (names, tests)
|
||||
return (names, tests)
|
||||
|
|
|
|||
|
|
@ -185,4 +185,4 @@ def simulate_smt(smt_file_path, vcd_path, num_steps, rnd):
|
|||
try:
|
||||
simulate_smt_with_smtio(smt_file_path, vcd_path, smt_io, num_steps, rnd)
|
||||
finally:
|
||||
smt_io.p_close()
|
||||
smt_io.p_close()
|
||||
|
|
|
|||
|
|
@ -1,4 +1,3 @@
|
|||
|
||||
These test cases are copied from the hana project:
|
||||
https://sourceforge.net/projects/sim-sim/
|
||||
|
||||
|
|
|
|||
|
|
@ -1136,4 +1136,3 @@ module INC64 #(parameter SIZE = 64) (input [SIZE-1:0] in, output [SIZE:0] out);
|
|||
assign out = in + 1;
|
||||
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -216,4 +216,3 @@ always @(in or enable)
|
|||
endcase
|
||||
end
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -62,4 +62,3 @@ VCC synth_VCC_1(.out(
|
|||
synth_net_4));
|
||||
VCC synth_VCC_2(.out(synth_net_10));
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -334,4 +334,4 @@ library (ls05_stdcells) {
|
|||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -3,4 +3,3 @@ library("foobar") {
|
|||
bar : baz[0] ;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -11,4 +11,4 @@ library(dummy) {
|
|||
function : "A" ;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -54,4 +54,4 @@ library (retention) {
|
|||
direction : input;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -68,5 +68,3 @@ library(supergate) {
|
|||
}
|
||||
|
||||
} /* end */
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -1588,4 +1588,3 @@ extra = [
|
|||
"endif",
|
||||
]
|
||||
gen_tests_makefile.generate_custom(create_tests, extra)
|
||||
|
||||
|
|
|
|||
|
|
@ -25,4 +25,3 @@ ram distributed \RAM_LUT {
|
|||
clock anyedge;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -26,4 +26,3 @@ always @(posedge PORT_A_CLK) begin
|
|||
end
|
||||
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -81,4 +81,3 @@ always @(posedge i_clk)
|
|||
end
|
||||
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -24,4 +24,3 @@ always @(posedge clk, posedge reset) begin
|
|||
end
|
||||
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -24,4 +24,3 @@ always @(posedge clk) begin
|
|||
end
|
||||
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -43,4 +43,3 @@ always @(posedge clk) begin
|
|||
end
|
||||
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -29,4 +29,3 @@ always @(posedge clk) begin
|
|||
end
|
||||
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -37,4 +37,3 @@ always @(posedge clk) begin
|
|||
end
|
||||
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -47,4 +47,3 @@ select -assert-count 6 t:$_DFFE_??_
|
|||
select -assert-count 4 t:$_DLATCH_?_
|
||||
select -assert-count 4 t:$_SR_??_
|
||||
select -assert-none t:$_AND_ t:$_DFFE_??_ t:$_DLATCH_?_ t:$_SR_??_ %% %n t:* %i
|
||||
|
||||
|
|
|
|||
|
|
@ -110,4 +110,3 @@ select -assert-count 2 t:$_DFF_P_
|
|||
select -assert-count 4 t:$_DFFE_PP_
|
||||
|
||||
design -reset
|
||||
|
||||
|
|
|
|||
|
|
@ -374,4 +374,4 @@ EOF
|
|||
|
||||
scratchpad -set opt.did_something false
|
||||
opt_expr
|
||||
scratchpad -assert opt.did_something false
|
||||
scratchpad -assert opt.did_something false
|
||||
|
|
|
|||
|
|
@ -287,4 +287,3 @@ select -assert-none t:$_MUX16_
|
|||
select -assert-count 1 o:out %ci*
|
||||
|
||||
##########
|
||||
|
||||
|
|
|
|||
|
|
@ -13,4 +13,3 @@ chformal -lower
|
|||
clean
|
||||
opt_merge
|
||||
select -assert-count 2 t:$cover
|
||||
|
||||
|
|
|
|||
|
|
@ -17,4 +17,3 @@ EOT
|
|||
proc
|
||||
alumacc
|
||||
equiv_opt -assert opt_share
|
||||
|
||||
|
|
|
|||
|
|
@ -25,4 +25,3 @@ module = d.module(r"\spm")
|
|||
for conn_from, conn_to in module.connections_:
|
||||
for bit_from, bit_to in zip(conn_from, conn_to):
|
||||
print(f"assign {_dump_sigbit(bit_from)} = {_dump_sigbit(bit_to)};")
|
||||
|
||||
|
|
|
|||
2
tests/rtlil/.gitignore
vendored
2
tests/rtlil/.gitignore
vendored
|
|
@ -1 +1 @@
|
|||
/temp
|
||||
/temp
|
||||
|
|
|
|||
|
|
@ -76,4 +76,3 @@ module alu(
|
|||
result <= tmp[7:0];
|
||||
end
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -84,4 +84,3 @@ module test_005(clk, a, a_old, b);
|
|||
assert(a_old != b);
|
||||
end
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -12,4 +12,3 @@ sat -falsify -prove-asserts -seq 2 test_002
|
|||
sat -falsify -prove-asserts -seq 2 test_003
|
||||
sat -falsify -prove-asserts -seq 2 test_004
|
||||
sat -verify -prove-asserts -seq 2 test_005
|
||||
|
||||
|
|
|
|||
|
|
@ -35,4 +35,3 @@ module counter2(clk, rst, ping);
|
|||
|
||||
assign ping = &count;
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -7,4 +7,3 @@ miter -equiv -make_assert -make_outputs counter1 counter2 miter
|
|||
|
||||
cd miter; flatten; opt
|
||||
sat -verify -prove-asserts -tempinduct -set-at 1 in_rst 1 -seq 1 -show-inputs -show-outputs
|
||||
|
||||
|
|
|
|||
|
|
@ -32,4 +32,3 @@ module counter2(clk, rst, ping);
|
|||
|
||||
assign ping = &count;
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -7,4 +7,3 @@ miter -equiv -make_assert -make_outputs counter1 counter2 miter
|
|||
|
||||
cd miter; flatten; opt
|
||||
sat -verify -prove-asserts -tempinduct -set-at 1 in_rst 1 -seq 1 -show-inputs -show-outputs
|
||||
|
||||
|
|
|
|||
|
|
@ -30,4 +30,3 @@ always @(posedge clk, negedge rst_n)
|
|||
else
|
||||
y <= a != 0;
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -12,4 +12,3 @@ flatten miter34; opt miter34
|
|||
|
||||
sat -verify -prove trigger 0 miter12
|
||||
sat -verify -prove trigger 0 miter34
|
||||
|
||||
|
|
|
|||
|
|
@ -52,4 +52,3 @@ module test_3(
|
|||
if (9 <= s && s < 12) y3 <= b / a;
|
||||
end
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -59,4 +59,3 @@ module alu(
|
|||
result <= tmp[7:0];
|
||||
end
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -1,2 +1,2 @@
|
|||
puts "This should print something:"
|
||||
puts [get_ports {A[0]}]
|
||||
puts [get_ports {A[0]}]
|
||||
|
|
|
|||
|
|
@ -1,2 +1,2 @@
|
|||
read_verilog simple_assign.v
|
||||
sim -r simple_assign.vcd -scope simple_assign
|
||||
sim -r simple_assign.vcd -scope simple_assign
|
||||
|
|
|
|||
|
|
@ -10,4 +10,4 @@ b1 n1
|
|||
b1 n2
|
||||
#10
|
||||
b0 n1
|
||||
b0 n2
|
||||
b0 n2
|
||||
|
|
|
|||
|
|
@ -1,3 +1,3 @@
|
|||
read_rtlil vector_assign.il
|
||||
sim -r var_reference_without_whitespace.vcd -scope tb.uut
|
||||
sim -r var_reference_with_whitespace.vcd -scope tb.uut
|
||||
sim -r var_reference_with_whitespace.vcd -scope tb.uut
|
||||
|
|
|
|||
|
|
@ -21,4 +21,3 @@ always @(posedge clk) begin
|
|||
end
|
||||
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -12,4 +12,3 @@ module aoi12(a, b, c, y);
|
|||
output y;
|
||||
assign y = ~((a & b) | c);
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -18,4 +18,3 @@ module attrib01_foo(clk, rst, inp, out);
|
|||
|
||||
attrib01_bar bar_instance (clk, rst, inp, out);
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
|
|
@ -22,4 +22,3 @@ module attrib02_foo(clk, rst, inp, out);
|
|||
|
||||
attrib02_bar bar_instance (clk, rst, inp, out);
|
||||
endmodule
|
||||
|
||||
|
|
|
|||
Some files were not shown because too many files have changed in this diff Show more
Loading…
Add table
Add a link
Reference in a new issue