diff options
Diffstat (limited to 'tests')
65 files changed, 2450 insertions, 10 deletions
diff --git a/tests/arch/anlogic/blockram.ys b/tests/arch/anlogic/blockram.ys new file mode 100644 index 000000000..da23409ba --- /dev/null +++ b/tests/arch/anlogic/blockram.ys @@ -0,0 +1,13 @@ +read_verilog ../common/blockram.v +hierarchy -top sync_ram_sp +proc +memory -nomap +equiv_opt -run :prove -map +/anlogic/cells_sim.v synth_anlogic +memory +opt -full + +design -load postopt +cd sync_ram_sp + +select -assert-count 1 t:EG_PHY_BRAM +select -assert-none t:EG_PHY_BRAM %% t:* %D diff --git a/tests/arch/anlogic/lutram.ys b/tests/arch/anlogic/lutram.ys index 6dbdbdac3..fe6135c73 100644 --- a/tests/arch/anlogic/lutram.ys +++ b/tests/arch/anlogic/lutram.ys @@ -2,7 +2,7 @@ read_verilog ../common/lutram.v hierarchy -top lutram_1w1r proc memory -nomap -equiv_opt -run :prove -map +/anlogic/cells_sim.v synth_anlogic +equiv_opt -run :prove -map +/anlogic/cells_sim.v synth_anlogic -nobram memory opt -full diff --git a/tests/arch/gowin/lutram.ys b/tests/arch/gowin/lutram.ys index 56f69e7c5..d668783a2 100644 --- a/tests/arch/gowin/lutram.ys +++ b/tests/arch/gowin/lutram.ys @@ -7,12 +7,11 @@ memory opt -full miter -equiv -flatten -make_assert -make_outputs gold gate miter -#ERROR: Called with -verify and proof did fail! -#sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter +sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter sat -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter design -load postopt cd lutram_1w1r -select -assert-count 8 t:RAM16S4 +select -assert-count 8 t:RAM16SDP4 # other logic present that is not simple #select -assert-none t:RAM16S4 %% t:* %D diff --git a/tests/arch/intel_alm/blockram.ys b/tests/arch/intel_alm/blockram.ys index c157c3165..3b61b9339 100644 --- a/tests/arch/intel_alm/blockram.ys +++ b/tests/arch/intel_alm/blockram.ys @@ -2,5 +2,6 @@ read_verilog ../common/blockram.v chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 10 sync_ram_sdp synth_intel_alm -family cyclonev -noiopad -noclkbuf cd sync_ram_sdp +select -assert-count 1 t:MISTRAL_NOT select -assert-count 1 t:MISTRAL_M10K -select -assert-none t:MISTRAL_M10K %% t:* %D +select -assert-none t:MISTRAL_NOT t:MISTRAL_M10K %% t:* %D diff --git a/tests/opt/opt_reduce_bmux.ys b/tests/opt/opt_reduce_bmux.ys new file mode 100644 index 000000000..55e0b6d4b --- /dev/null +++ b/tests/opt/opt_reduce_bmux.ys @@ -0,0 +1,117 @@ +read_ilang << EOT + +module \top + wire width 12 input 0 \A + wire width 2 input 1 \S + wire width 6 output 2 \Y + + cell $bmux $0 + parameter \WIDTH 6 + parameter \S_WIDTH 2 + connect \A { \A [11:10] \A [3:2] \A [10:9] \A [7] \A [7] \A [8] \A [2] \A [7:6] \A [5] \A [5] \A [3:2] \A [5:4] \A [1] \A [1] \A [3:0] } + connect \S \S + connect \Y \Y + end +end + +EOT + +equiv_opt -assert opt_reduce -fine +opt_reduce -fine +select -assert-count 1 t:$bmux r:WIDTH=4 %i + +design -reset + +read_ilang << EOT + +module \top + wire width 6 input 0 \A + wire width 2 input 1 \S + wire width 6 output 2 \Y + + cell $bmux $0 + parameter \WIDTH 6 + parameter \S_WIDTH 2 + connect \A { \A [5:0] \A [5:0] \A [5:0] \A [5:0] } + connect \S \S + connect \Y \Y + end +end + +EOT + +equiv_opt -assert opt_reduce -fine +opt_reduce -fine +select -assert-count 0 t:$bmux + +design -reset + +read_ilang << EOT + +module \top + wire width 160 input 0 \A + wire width 2 input 1 \S + wire width 5 output 2 \Y + + cell $bmux $0 + parameter \WIDTH 5 + parameter \S_WIDTH 5 + connect \A \A + connect \S { \S [1] 1'1 \S [0] \S [1] 1'0 } + connect \Y \Y + end +end + +EOT + +equiv_opt -assert opt_reduce -fine +opt_reduce -fine +select -assert-count 1 t:$bmux r:S_WIDTH=2 %i + +design -reset + +read_ilang << EOT + +module \top + wire width 10 input 0 \A + wire input 1 \S + wire width 5 output 2 \Y + + cell $bmux $0 + parameter \WIDTH 5 + parameter \S_WIDTH 1 + connect \A \A + connect \S \S + connect \Y \Y + end +end + +EOT + +equiv_opt -assert opt_reduce -fine +opt_reduce -fine +select -assert-count 0 t:$bmux +select -assert-count 1 t:$mux + +design -reset + +read_ilang << EOT + +module \top + wire width 5 input 0 \A + wire width 5 output 1 \Y + + cell $bmux $0 + parameter \WIDTH 5 + parameter \S_WIDTH 0 + connect \A \A + connect \S { } + connect \Y \Y + end +end + +EOT + +equiv_opt -assert opt_reduce -fine +opt_reduce -fine +select -assert-count 0 t:$bmux diff --git a/tests/opt/opt_reduce_demux.ys b/tests/opt/opt_reduce_demux.ys new file mode 100644 index 000000000..3c5bd7d43 --- /dev/null +++ b/tests/opt/opt_reduce_demux.ys @@ -0,0 +1,91 @@ +read_ilang << EOT + +module \top + wire width 4 input 0 \A + wire width 2 input 1 \S + wire width 24 output 2 \Y + + cell $demux $0 + parameter \WIDTH 6 + parameter \S_WIDTH 2 + connect \A { \A [3] \A [1] 1'0 \A [2:0] } + connect \S \S + connect \Y \Y + end +end + +EOT + +equiv_opt -assert opt_reduce -fine +opt_reduce -fine +select -assert-count 1 t:$demux r:WIDTH=4 %i + +design -reset + +read_ilang << EOT + +module \top + wire width 2 input 1 \S + wire width 24 output 2 \Y + + cell $demux $0 + parameter \WIDTH 6 + parameter \S_WIDTH 2 + connect \A 6'000000 + connect \S \S + connect \Y \Y + end +end + +EOT + +equiv_opt -assert opt_reduce -fine +opt_reduce -fine +select -assert-count 0 t:$demux + +design -reset + +read_ilang << EOT + +module \top + wire width 5 input 0 \A + wire width 2 input 1 \S + wire width 160 output 2 \Y + + cell $demux $0 + parameter \WIDTH 5 + parameter \S_WIDTH 5 + connect \A \A + connect \S { \S [0] \S [1] 1'1 \S [0] 1'0 } + connect \Y \Y + end +end + +EOT + +equiv_opt -assert opt_reduce -fine +opt_reduce -fine +select -assert-count 1 t:$demux r:S_WIDTH=2 %i + +design -reset + +read_ilang << EOT + +module \top + wire width 5 input 0 \A + wire width 20 output 2 \Y + + cell $demux $0 + parameter \WIDTH 5 + parameter \S_WIDTH 2 + connect \A \A + connect \S { 2'10 } + connect \Y \Y + end +end + +EOT + +equiv_opt -assert opt_reduce -fine +opt_reduce -fine +select -assert-count 0 t:$demux diff --git a/tests/sat/.gitignore b/tests/sat/.gitignore index 8355de9dc..664425d73 100644 --- a/tests/sat/.gitignore +++ b/tests/sat/.gitignore @@ -1,2 +1,4 @@ *.log run-test.mk +*.vcd +*.fst diff --git a/tests/sat/alu.v b/tests/sat/alu.v new file mode 100644 index 000000000..9826fe05d --- /dev/null +++ b/tests/sat/alu.v @@ -0,0 +1,79 @@ +module alu( + input clk, + input [7:0] A, + input [7:0] B, + input [3:0] operation, + output reg [7:0] result, + output reg CF, + output reg ZF, + output reg SF +); + + localparam ALU_OP_ADD /* verilator public_flat */ = 4'b0000; + localparam ALU_OP_SUB /* verilator public_flat */ = 4'b0001; + localparam ALU_OP_ADC /* verilator public_flat */ = 4'b0010; + localparam ALU_OP_SBC /* verilator public_flat */ = 4'b0011; + + localparam ALU_OP_AND /* verilator public_flat */ = 4'b0100; + localparam ALU_OP_OR /* verilator public_flat */ = 4'b0101; + localparam ALU_OP_NOT /* verilator public_flat */ = 4'b0110; + localparam ALU_OP_XOR /* verilator public_flat */ = 4'b0111; + + localparam ALU_OP_SHL /* verilator public_flat */ = 4'b1000; + localparam ALU_OP_SHR /* verilator public_flat */ = 4'b1001; + localparam ALU_OP_SAL /* verilator public_flat */ = 4'b1010; + localparam ALU_OP_SAR /* verilator public_flat */ = 4'b1011; + + localparam ALU_OP_ROL /* verilator public_flat */ = 4'b1100; + localparam ALU_OP_ROR /* verilator public_flat */ = 4'b1101; + localparam ALU_OP_RCL /* verilator public_flat */ = 4'b1110; + localparam ALU_OP_RCR /* verilator public_flat */ = 4'b1111; + + reg [8:0] tmp; + + always @(posedge clk) + begin + case (operation) + ALU_OP_ADD : + tmp = A + B; + ALU_OP_SUB : + tmp = A - B; + ALU_OP_ADC : + tmp = A + B + { 7'b0000000, CF }; + ALU_OP_SBC : + tmp = A - B - { 7'b0000000, CF }; + ALU_OP_AND : + tmp = {1'b0, A & B }; + ALU_OP_OR : + tmp = {1'b0, A | B }; + ALU_OP_NOT : + tmp = {1'b0, ~B }; + ALU_OP_XOR : + tmp = {1'b0, A ^ B}; + ALU_OP_SHL : + tmp = { A[7], A[6:0], 1'b0}; + ALU_OP_SHR : + tmp = { A[0], 1'b0, A[7:1]}; + ALU_OP_SAL : + // Same as SHL + tmp = { A[7], A[6:0], 1'b0}; + ALU_OP_SAR : + tmp = { A[0], A[7], A[7:1]}; + ALU_OP_ROL : + tmp = { A[7], A[6:0], A[7]}; + ALU_OP_ROR : + tmp = { A[0], A[0], A[7:1]}; + ALU_OP_RCL : + tmp = { A[7], A[6:0], CF}; + ALU_OP_RCR : + tmp = { A[0], CF, A[7:1]}; + endcase + + CF <= tmp[8]; + ZF <= tmp[7:0] == 0; + SF <= tmp[7]; + + result <= tmp[7:0]; + end +endmodule + diff --git a/tests/sat/grom.ys b/tests/sat/grom.ys new file mode 100644 index 000000000..da0f3b620 --- /dev/null +++ b/tests/sat/grom.ys @@ -0,0 +1,9 @@ +read_verilog grom_computer.v grom_cpu.v alu.v ram_memory.v; +prep -top grom_computer; +sim -clock clk -reset reset -fst grom.fst -vcd grom.vcd -n 80 + +sim -clock clk -r grom.fst -scope grom_computer -start 25ns -stop 100ns -sim-cmp + +sim -clock clk -r grom.fst -scope grom_computer -stop 100ns -sim-gold + +sim -clock clk -r grom.fst -scope grom_computer -n 10 -sim-gate diff --git a/tests/sat/grom_computer.v b/tests/sat/grom_computer.v new file mode 100644 index 000000000..63a5c8ff8 --- /dev/null +++ b/tests/sat/grom_computer.v @@ -0,0 +1,31 @@ +module grom_computer + (input clk, // Main Clock + input reset, // reset + output hlt, + output reg[7:0] display_out + ); + + wire [11:0] addr; + wire [7:0] memory_out; + wire [7:0] memory_in; + wire mem_enable; + wire we; + wire ioreq; + + grom_cpu cpu(.clk(clk),.reset(reset),.addr(addr),.data_in(memory_out),.data_out(memory_in),.we(we),.ioreq(ioreq),.hlt(hlt)); + + assign mem_enable = we & ~ioreq; + + ram_memory memory(.clk(clk),.addr(addr),.data_in(memory_in),.we(mem_enable),.data_out(memory_out)); + + always @(posedge clk) + begin + if(ioreq==1 && we==1) + begin + display_out <= memory_in; + `ifdef DISASSEMBLY + $display("Display output : %h", memory_in); + `endif + end + end +endmodule diff --git a/tests/sat/grom_cpu.v b/tests/sat/grom_cpu.v new file mode 100644 index 000000000..914c0f56c --- /dev/null +++ b/tests/sat/grom_cpu.v @@ -0,0 +1,747 @@ +module grom_cpu( + input clk, + input reset, + output reg [11:0] addr, + input [7:0] data_in, + output reg [7:0] data_out, + output reg we, + output reg ioreq, + output reg hlt +); + + reg[11:0] PC /* verilator public_flat */; // Program counter + reg[7:0] IR /* verilator public_flat */; // Instruction register + reg[7:0] VALUE /* verilator public_flat */; // Temp reg for storing 2nd operand + reg[3:0] CS /* verilator public_flat */; // Code segment regiser + reg[3:0] DS /* verilator public_flat */; // Data segment regiser + reg[11:0] SP /* verilator public_flat */; // Stack pointer regiser + reg[7:0] R[0:3] /* verilator public_flat */; // General purpose registers + reg[11:0] FUTURE_PC /* verilator public_flat */; // PC to jump to + + localparam STATE_RESET /*verilator public_flat*/ = 5'b00000; + localparam STATE_FETCH_PREP /*verilator public_flat*/ = 5'b00001; + localparam STATE_FETCH_WAIT /*verilator public_flat*/ = 5'b00010; + localparam STATE_FETCH /*verilator public_flat*/ = 5'b00011; + localparam STATE_EXECUTE /*verilator public_flat*/ = 5'b00100; + localparam STATE_FETCH_VALUE_PREP /*verilator public_flat*/ = 5'b00101; + localparam STATE_FETCH_VALUE /*verilator public_flat*/ = 5'b00110; + localparam STATE_EXECUTE_DBL /*verilator public_flat*/ = 5'b00111; + localparam STATE_LOAD_VALUE /*verilator public_flat*/ = 5'b01000; + localparam STATE_LOAD_VALUE_WAIT /*verilator public_flat*/ = 5'b01001; + localparam STATE_ALU_RESULT_WAIT /*verilator public_flat*/ = 5'b01010; + localparam STATE_ALU_RESULT /*verilator public_flat*/ = 5'b01011; + localparam STATE_PUSH_PC_LOW /*verilator public_flat*/ = 5'b01100; + localparam STATE_JUMP /*verilator public_flat*/ = 5'b01101; + localparam STATE_RET_VALUE_WAIT /*verilator public_flat*/ = 5'b01110; + localparam STATE_RET_VALUE /*verilator public_flat*/ = 5'b01111; + localparam STATE_RET_VALUE_WAIT2 /*verilator public_flat*/ = 5'b10000; + localparam STATE_RET_VALUE2 /*verilator public_flat*/ = 5'b10001; + + reg [4:0] state /* verilator public_flat */ = STATE_RESET; + + reg [7:0] alu_a /* verilator public_flat */; + reg [7:0] alu_b /* verilator public_flat */; + reg [3:0] alu_op /* verilator public_flat */; + + reg [1:0] RESULT_REG /* verilator public_flat */; + + wire [7:0] alu_res /* verilator public_flat */; + wire alu_CF /* verilator public_flat */; + wire alu_ZF /* verilator public_flat */; + wire alu_SF /* verilator public_flat */; + reg jump; + + alu alu(.clk(clk),.A(alu_a),.B(alu_b),.operation(alu_op),.result(alu_res),.CF(alu_CF),.ZF(alu_ZF),.SF(alu_SF)); + + always @(posedge clk) + begin + if (reset) + begin + state <= STATE_RESET; + hlt <= 0; + end + else + begin + case (state) + STATE_RESET : + begin + PC <= 12'h000; + state <= STATE_FETCH_PREP; + CS <= 4'h0; + DS <= 4'h0; + R[0] <= 8'h00; + R[1] <= 8'h00; + R[2] <= 8'h00; + R[3] <= 8'h00; + SP <= 12'hfff; + end + + STATE_FETCH_PREP : + begin + addr <= PC; + we <= 0; + ioreq <= 0; + + state <= STATE_FETCH_WAIT; + end + + STATE_FETCH_WAIT : + begin + // Sync with memory due to CLK + state <= (hlt) ? STATE_FETCH_PREP : STATE_FETCH; + end + + STATE_FETCH : + begin + IR <= data_in; + PC <= PC + 1; + + state <= STATE_EXECUTE; + end + STATE_EXECUTE : + begin + `ifdef DISASSEMBLY + $display(" PC %h R0 %h R1 %h R2 %h R3 %h CS %h DS %h SP %h ALU [%d %d %d]", PC, R[0], R[1], R[2], R[3], CS, DS, SP, alu_CF,alu_SF,alu_ZF); + `endif + if (IR[7]) + begin + addr <= PC; + state <= STATE_FETCH_VALUE_PREP; + PC <= PC + 1; + end + else + begin + case(IR[6:4]) + 3'b000 : + begin + `ifdef DISASSEMBLY + $display("MOV R%d,R%d",IR[3:2],IR[1:0]); + `endif + R[IR[3:2]] <= R[IR[1:0]]; + state <= STATE_FETCH_PREP; + end + 3'b001 : + begin + alu_a <= R[0]; // first input R0 + alu_b <= R[IR[1:0]]; + RESULT_REG <= 0; // result in R0 + alu_op <= { 2'b00, IR[3:2] }; + + state <= STATE_ALU_RESULT_WAIT; + + `ifdef DISASSEMBLY + case(IR[3:2]) + 2'b00 : begin + $display("ADD R%d",IR[1:0]); + end + 2'b01 : begin + $display("SUB R%d",IR[1:0]); + end + 2'b10 : begin + $display("ADC R%d",IR[1:0]); + end + 2'b11 : begin + $display("SBC R%d",IR[1:0]); + end + endcase + `endif + end + 3'b010 : + begin + alu_a <= R[0]; // first input R0 + alu_b <= R[IR[1:0]]; + RESULT_REG <= 0; // result in R0 + alu_op <= { 2'b01, IR[3:2] }; + state <= STATE_ALU_RESULT_WAIT; + `ifdef DISASSEMBLY + case(IR[3:2]) + 2'b00 : begin + $display("AND R%d",IR[1:0]); + end + 2'b01 : begin + $display("OR R%d",IR[1:0]); + end + 2'b10 : begin + $display("NOT R%d",IR[1:0]); + end + 2'b11 : begin + $display("XOR R%d",IR[1:0]); + end + endcase + `endif + end + 3'b011 : + begin + RESULT_REG <= IR[1:0]; // result in REG + // CMP and TEST are not storing result + state <= IR[3] ? STATE_FETCH_PREP : STATE_ALU_RESULT_WAIT; + // CMP and TEST are having first input R0, for INC and DEC is REG + alu_a <= IR[3] ? R[0] : R[IR[1:0]]; + // CMP and TEST are having second input REG, for INC and DEC is 1 + alu_b <= IR[3] ? R[IR[1:0]] : 8'b00000001; + + case(IR[3:2]) + 2'b00 : begin + `ifdef DISASSEMBLY + $display("INC R%d",IR[1:0]); + `endif + alu_op <= 4'b0000; // ALU_OP_ADD + end + 2'b01 : begin + `ifdef DISASSEMBLY + $display("DEC R%d",IR[1:0]); + `endif + alu_op <= 4'b0001; // ALU_OP_SUB + end + 2'b10 : begin + `ifdef DISASSEMBLY + $display("CMP R%d",IR[1:0]); + `endif + alu_op <= 4'b0001; // ALU_OP_SUB + end + 2'b11 : begin + `ifdef DISASSEMBLY + $display("TST R%d",IR[1:0]); + `endif + alu_op <= 4'b0100; // ALU_OP_AND + end + endcase + end + 3'b100 : + begin + if (IR[3]==0) + begin + alu_a <= R[0]; // first input R0 + // no 2nd input + RESULT_REG <= 0; // result in R0 + alu_op <= { 1'b1, IR[2:0] }; + `ifdef DISASSEMBLY + case(IR[2:0]) + 3'b000 : begin + $display("SHL"); + end + 3'b001 : begin + $display("SHR"); + end + 3'b010 : begin + $display("SAL"); + end + 3'b011 : begin + $display("SAR"); + end + 3'b100 : begin + $display("ROL"); + end + 3'b101 : begin + $display("ROR"); + end + 3'b110 : begin + $display("RCL"); + end + 3'b111 : begin + $display("RCR"); + end + endcase + `endif + state <= STATE_ALU_RESULT_WAIT; + end + else + begin + if (IR[2]==0) + begin + `ifdef DISASSEMBLY + $display("PUSH R%d",IR[1:0]); + `endif + addr <= SP; + we <= 1; + ioreq <= 0; + data_out <= R[IR[1:0]]; + SP <= SP - 1; + state <= STATE_FETCH_PREP; + end + else + begin + `ifdef DISASSEMBLY + $display("POP R%d",IR[1:0]); + `endif + addr <= SP + 1; + we <= 0; + ioreq <= 0; + RESULT_REG <= IR[1:0]; + SP <= SP + 1; + state <= STATE_LOAD_VALUE_WAIT; + end + end + end + 3'b101 : + begin + `ifdef DISASSEMBLY + $display("LOAD R%d,[R%d]", IR[3:2], IR[1:0]); + `endif + addr <= { DS, R[IR[1:0]] }; + we <= 0; + ioreq <= 0; + RESULT_REG <= IR[3:2]; + + state <= STATE_LOAD_VALUE_WAIT; + end + 3'b110 : + begin + `ifdef DISASSEMBLY + $display("STORE [R%d],R%d", IR[3:2], IR[1:0]); + `endif + addr <= { DS, R[IR[3:2]] }; + we <= 1; + ioreq <= 0; + data_out <= R[IR[1:0]]; + + state <= STATE_FETCH_PREP; + end + 3'b111 : + begin + // Special instuctions + case(IR[3:2]) + 2'b00 : begin + CS <= R[IR[1:0]][3:0]; + state <= STATE_FETCH_PREP; + `ifdef DISASSEMBLY + $display("MOV CS,R%d",IR[1:0]); + `endif + end + 2'b01 : begin + DS <= R[IR[1:0]][3:0]; + state <= STATE_FETCH_PREP; + `ifdef DISASSEMBLY + $display("MOV DS,R%d",IR[1:0]); + `endif + end + 2'b10 : begin + case(IR[1:0]) + 2'b00 : begin + `ifdef DISASSEMBLY + $display("PUSH CS"); + `endif + addr <= SP; + we <= 1; + ioreq <= 0; + data_out <= { 4'b0000, CS}; + SP <= SP - 1; + state <= STATE_FETCH_PREP; + end + 2'b01 : begin + `ifdef DISASSEMBLY + $display("PUSH DS"); + `endif + addr <= SP; + we <= 1; + ioreq <= 0; + data_out <= { 4'b0000, DS}; + SP <= SP - 1; + state <= STATE_FETCH_PREP; + end + 2'b10 : begin + `ifdef DISASSEMBLY + $display("Unused opcode"); + `endif + end + 2'b11 : begin + `ifdef DISASSEMBLY + $display("Unused opcode"); + `endif + end + endcase + state <= STATE_FETCH_PREP; + end + 2'b11 : begin + case(IR[1:0]) + 2'b00 : begin + `ifdef DISASSEMBLY + $display("Unused opcode"); + `endif + state <= STATE_FETCH_PREP; + end + 2'b01 : begin + `ifdef DISASSEMBLY + $display("Unused opcode"); + `endif + state <= STATE_FETCH_PREP; + end + 2'b10 : begin + `ifdef DISASSEMBLY + $display("RET"); + `endif + addr <= SP + 1; + we <= 0; + ioreq <= 0; + SP <= SP + 1; + state <= STATE_RET_VALUE_WAIT; + end + 2'b11 : begin + hlt <= 1; + `ifdef DISASSEMBLY + $display("HALT"); + `endif + state <= STATE_FETCH_PREP; + end + endcase + end + endcase + end + endcase + end + end + STATE_FETCH_VALUE_PREP : + begin + // Sync with memory due to CLK + state <= STATE_FETCH_VALUE; + end + STATE_FETCH_VALUE : + begin + VALUE <= data_in; + state <= STATE_EXECUTE_DBL; + end + STATE_EXECUTE_DBL : + begin + case(IR[6:4]) + 3'b000 : + begin + if (IR[3]==0) + begin + case(IR[2:0]) + 3'b000 : + begin + `ifdef DISASSEMBLY + $display("JMP %h ",{ CS, VALUE[7:0] }); + `endif + jump = 1; + end + 3'b001 : + begin + `ifdef DISASSEMBLY + $display("JC %h ",{CS, VALUE[7:0] }); + `endif + jump = (alu_CF==1); + end + 3'b010 : + begin + `ifdef DISASSEMBLY + $display("JNC %h ",{CS, VALUE[7:0] }); + `endif + jump = (alu_CF==0); + end + 3'b011 : + begin + `ifdef DISASSEMBLY + $display("JM %h ",{CS, VALUE[7:0] }); + `endif + jump = (alu_SF==1); + end + 3'b100 : + begin + `ifdef DISASSEMBLY + $display("JP %h ",{CS, VALUE[7:0] }); + `endif + jump = (alu_SF==0); + end + 3'b101 : + begin + `ifdef DISASSEMBLY + $display("JZ %h ",{CS, VALUE[7:0] }); + `endif + jump = (alu_ZF==1); + end + 3'b110 : + begin + `ifdef DISASSEMBLY + $display("JNZ %h ",{CS, VALUE[7:0] }); + `endif + jump = (alu_ZF==0); + end + 3'b111 : + begin + `ifdef DISASSEMBLY + $display("Unused opcode %h",IR); + `endif + jump = 0; + end + endcase + + if (jump) + begin + PC <= { CS, VALUE[7:0] }; + addr <= { CS, VALUE[7:0] }; + we <= 0; + ioreq <= 0; + end + state <= STATE_FETCH_PREP; + end + else + begin + case(IR[2:0]) + 3'b000 : + begin + `ifdef DISASSEMBLY + $display("JR %h ", PC + {VALUE[7],VALUE[7],VALUE[7],VALUE[7],VALUE[7:0]} ); + `endif + jump = 1; + end + 3'b001 : + begin + `ifdef DISASSEMBLY + $display("JRC %h ",{CS, VALUE[7:0] }); + `endif + jump = (alu_CF==1); + end + 3'b010 : + begin + `ifdef DISASSEMBLY + $display("JRNC %h ",{CS, VALUE[7:0] }); + `endif + jump = (alu_CF==0); + end + 3'b011 : + begin + `ifdef DISASSEMBLY + $display("JRM %h ",{CS, VALUE[7:0] }); + `endif + jump = (alu_SF==1); + end + 3'b100 : + begin + `ifdef DISASSEMBLY + $display("JRP %h ",{CS, VALUE[7:0] }); + `endif + jump = (alu_SF==0); + end + 3'b101 : + begin + `ifdef DISASSEMBLY + $display("JRZ %h ",{CS, VALUE[7:0] }); + `endif + jump = (alu_ZF==1); + end + 3'b110 : + begin + `ifdef DISASSEMBLY + $display("JRNZ %h ",{CS, VALUE[7:0] }); + `endif + jump = (alu_ZF==0); + end + 3'b111 : + begin + `ifdef DISASSEMBLY + $display("Unused opcode %h",IR); + `endif + jump = 0; + end + endcase + if (jump) + begin + PC <= PC + {VALUE[7],VALUE[7],VALUE[7],VALUE[7],VALUE[7:0]}; + addr <= PC + {VALUE[7],VALUE[7],VALUE[7],VALUE[7],VALUE[7:0]}; + we <= 0; + ioreq <= 0; + end + state <= STATE_FETCH_PREP; + end + end + 3'b001 : + begin + `ifdef DISASSEMBLY + $display("JUMP %h ",{ IR[3:0], VALUE[7:0] }); + `endif + PC <= { IR[3:0], VALUE[7:0] }; + addr <= { IR[3:0], VALUE[7:0] }; + we <= 0; + ioreq <= 0; + state <= STATE_FETCH_PREP; + end + 3'b010 : + begin + `ifdef DISASSEMBLY + $display("CALL %h ",{ IR[3:0], VALUE[7:0] }); + `endif + FUTURE_PC <= { IR[3:0], VALUE[7:0] }; + addr <= SP; + we <= 1; + ioreq <= 0; + data_out <= { 4'b0000, PC[11:8]}; + SP <= SP - 1; + state <= STATE_PUSH_PC_LOW; + end + 3'b011 : + begin + `ifdef DISASSEMBLY + $display("MOV SP,%h ",{ IR[3:0], VALUE[7:0] }); + `endif + SP <= { IR[3:0], VALUE[7:0] }; + state <= STATE_FETCH_PREP; + end + 3'b100 : + begin + `ifdef DISASSEMBLY + $display("IN R%d,[0x%h]",IR[1:0], VALUE); + `endif + ioreq <= 1; + we <= 0; + addr <= { 4'b0000, VALUE }; + RESULT_REG <= IR[1:0]; + state <= STATE_LOAD_VALUE_WAIT; + end + 3'b101 : + begin + `ifdef DISASSEMBLY + $display("OUT [0x%h],R%d",VALUE,IR[1:0]); + `endif + ioreq <= 1; + we <= 1; + addr <= { 4'b0000, VALUE }; + data_out <= R[IR[1:0]]; + state <= STATE_FETCH_PREP; + end + 3'b110 : + begin + // Special instuctions + case(IR[1:0]) + 2'b00 : begin + `ifdef DISASSEMBLY + $display("MOV CS,0x%h",VALUE); + `endif + CS <= VALUE[3:0]; + state <= STATE_FETCH_PREP; + end + 2'b01 : begin + `ifdef DISASSEMBLY + $display("MOV DS,0x%h",VALUE); + `endif + DS <= VALUE[3:0]; + state <= STATE_FETCH_PREP; + end + 2'b10 : begin + `ifdef DISASSEMBLY + $display("Unused opcode %h",IR); + `endif + state <= STATE_FETCH_PREP; + end + 2'b11 : begin + `ifdef DISASSEMBLY + $display("Unused opcode %h",IR); + `endif + state <= STATE_FETCH_PREP; + end + endcase + end + 3'b111 : + begin + case(IR[3:2]) + 2'b00 : begin + `ifdef DISASSEMBLY + $display("MOV R%d,0x%h",IR[1:0],VALUE); + `endif + R[IR[1:0]] <= VALUE; + state <= STATE_FETCH_PREP; + end + 2'b01 : begin + `ifdef DISASSEMBLY + $display("LOAD R%d,[0x%h]",IR[1:0], {DS, VALUE}); + `endif + addr <= { DS, VALUE }; + we <= 0; + ioreq <= 0; + RESULT_REG <= IR[1:0]; + + state <= STATE_LOAD_VALUE_WAIT; + end + 2'b10 : begin + `ifdef DISASSEMBLY + $display("STORE [0x%h],R%d", {DS, VALUE}, IR[1:0]); + `endif + addr <= { DS, VALUE }; + we <= 1; + ioreq <= 0; + data_out <= R[IR[1:0]]; + + state <= STATE_FETCH_PREP; + end + 2'b11 : begin + `ifdef DISASSEMBLY + $display("Unused opcode %h",IR); + `endif + state <= STATE_FETCH_PREP; + end + endcase + end + endcase + end + STATE_LOAD_VALUE_WAIT : + begin + // Sync with memory due to CLK + state <= STATE_LOAD_VALUE; + end + STATE_LOAD_VALUE : + begin + R[RESULT_REG] <= data_in; + we <= 0; + state <= STATE_FETCH_PREP; + end + STATE_ALU_RESULT_WAIT : + begin + state <= STATE_ALU_RESULT; + end + STATE_ALU_RESULT : + begin + R[RESULT_REG] <= alu_res; + state <= STATE_FETCH_PREP; + end + STATE_PUSH_PC_LOW : + begin + addr <= SP; + we <= 1; + ioreq <= 0; + data_out <= PC[7:0]; + SP <= SP - 1; + state <= STATE_JUMP; + end + STATE_JUMP : + begin + `ifdef DISASSEMBLY + $display("Jumping to %h",FUTURE_PC); + `endif + PC <= FUTURE_PC; + state <= STATE_FETCH_PREP; + end + STATE_RET_VALUE_WAIT : + begin + // Sync with memory due to CLK + state <= STATE_RET_VALUE; + end + STATE_RET_VALUE : + begin + FUTURE_PC <= { 4'b0000, data_in }; + we <= 0; + state <= STATE_RET_VALUE_WAIT2; + + addr <= SP + 1; + we <= 0; + ioreq <= 0; + SP <= SP + 1; + end + STATE_RET_VALUE_WAIT2 : + begin + // Sync with memory due to CLK + state <= STATE_RET_VALUE2; + end + STATE_RET_VALUE2 : + begin + FUTURE_PC <= FUTURE_PC | ({ 4'b0000, data_in } << 8); + we <= 0; + state <= STATE_JUMP; + end + default : + begin + state <= STATE_FETCH_PREP; + end + endcase + end + end +endmodule diff --git a/tests/sat/ram_memory.v b/tests/sat/ram_memory.v new file mode 100644 index 000000000..0d91514b2 --- /dev/null +++ b/tests/sat/ram_memory.v @@ -0,0 +1,39 @@ +module ram_memory( + input clk, + input [11:0] addr, + input [7:0] data_in, + input we, + output reg [7:0] data_out +); + + reg [7:0] store[0:4095] /* verilator public_flat */; + + initial + begin + store[0] <= 8'b11100001; // MOV DS,2 + store[1] <= 8'b00000010; // + store[2] <= 8'b01010100; // LOAD R1,[R0] + store[3] <= 8'b00110001; // INC R1 + store[4] <= 8'b00110001; // INC R1 + store[5] <= 8'b01100001; // STORE [R0],R1 + store[6] <= 8'b11010001; // OUT [0],R1 + store[7] <= 8'b00000000; // + store[8] <= 8'b00110001; // INC R1 + store[9] <= 8'b10100001; // CALL 0x100 + store[10] <= 8'b00000000; // + store[11] <= 8'b01111111; // HLT + + + store[256] <= 8'b11010001; // OUT [0],R1 + store[257] <= 8'b00000000; // + store[258] <= 8'b01111110; // RET + + store[512] <= 8'b00000000; + end + + always @(posedge clk) + if (we) + store[addr] <= data_in; + else + data_out <= store[addr]; +endmodule diff --git a/tests/sat/sim_counter.ys b/tests/sat/sim_counter.ys new file mode 100644 index 000000000..a0ff41b6e --- /dev/null +++ b/tests/sat/sim_counter.ys @@ -0,0 +1,48 @@ +# Create stimulus file +read_verilog <<EOT +module top (clk, reset, cnt); + +input clk; +input reset; +output [7:0] cnt; + +reg [7:0] cnt; + +endmodule +EOT +prep -top top; +sim -clock clk -reset reset -fst stimulus.fst -n 10 +design -reset + +# Counter implementation +read_verilog <<EOT +module top (clk, reset, cnt); + +input clk; +input reset; +output [7:0] cnt; + +reg [7:0] cnt; + +always @(posedge clk) + if (!reset) + cnt = cnt + 1; + else + cnt = 0; + +endmodule +EOT +prep -top top; + +# Simulate with stimulus +sim -clock clk -scope top -r stimulus.fst + +# Stimulus does not have counter values +# x in FST can match any value in simulation +sim -clock clk -scope top -r stimulus.fst -sim-gate + +# Stimulus does not have counter values +# x in simulation can match any value in FST +# so we expect error +logger -expect error "Signal difference" 1 +sim -clock clk -scope top -r stimulus.fst -sim-gold diff --git a/tests/sim/.gitignore b/tests/sim/.gitignore new file mode 100644 index 000000000..2c96b65f8 --- /dev/null +++ b/tests/sim/.gitignore @@ -0,0 +1,6 @@ +*.log +/run-test.mk ++*_synth.v ++*_testbench +*.out +*.fst diff --git a/tests/sim/adff.v b/tests/sim/adff.v new file mode 100644 index 000000000..8c8fb0acf --- /dev/null +++ b/tests/sim/adff.v @@ -0,0 +1,7 @@ +module adff( input d, clk, rst, output reg q ); + always @( posedge clk, posedge rst ) + if (rst) + q <= 0; + else + q <= d; +endmodule diff --git a/tests/sim/adffe.v b/tests/sim/adffe.v new file mode 100644 index 000000000..55c7d8d4e --- /dev/null +++ b/tests/sim/adffe.v @@ -0,0 +1,8 @@ +module adffe( input d, clk, rst, en, output reg q ); + always @( posedge clk, posedge rst ) + if (rst) + q <= 0; + else + if (en) + q <= d; +endmodule diff --git a/tests/sim/adlatch.v b/tests/sim/adlatch.v new file mode 100644 index 000000000..5e8f48e49 --- /dev/null +++ b/tests/sim/adlatch.v @@ -0,0 +1,8 @@ +module adlatch( input d, rst, en, output reg q ); + always @* begin + if (rst) + q = 0; + else if (en) + q = d; + end +endmodule diff --git a/tests/sim/aldff.v b/tests/sim/aldff.v new file mode 100644 index 000000000..eeb0f0673 --- /dev/null +++ b/tests/sim/aldff.v @@ -0,0 +1,7 @@ +module aldff( input [0:3] d, input [0:3] ad, input clk, aload, output reg [0:3] q ); + always @( posedge clk, posedge aload) + if (aload) + q <= ad; + else + q <= d; +endmodule diff --git a/tests/sim/aldffe.v b/tests/sim/aldffe.v new file mode 100644 index 000000000..79c65afc4 --- /dev/null +++ b/tests/sim/aldffe.v @@ -0,0 +1,8 @@ +module aldffe( input [0:3] d, input [0:3] ad, input clk, aload, en, output reg [0:3] q ); + always @( posedge clk, posedge aload) + if (aload) + q <= ad; + else + if (en) + q <= d; +endmodule diff --git a/tests/sim/dff.v b/tests/sim/dff.v new file mode 100644 index 000000000..ce792b59a --- /dev/null +++ b/tests/sim/dff.v @@ -0,0 +1,4 @@ +module dff( input d, clk, output reg q ); + always @( posedge clk ) + q <= d; +endmodule diff --git a/tests/sim/dffe.v b/tests/sim/dffe.v new file mode 100644 index 000000000..853fcf66a --- /dev/null +++ b/tests/sim/dffe.v @@ -0,0 +1,5 @@ +module dffe( input clk, en, d, output reg q ); + always @( posedge clk ) + if ( en ) + q <= d; +endmodule diff --git a/tests/sim/dffsr.v b/tests/sim/dffsr.v new file mode 100644 index 000000000..2158708f1 --- /dev/null +++ b/tests/sim/dffsr.v @@ -0,0 +1,9 @@ +module dffsr( input clk, d, clr, set, output reg q ); + always @( posedge clk, posedge set, posedge clr) + if ( clr ) + q <= 0; + else if (set) + q <= 1; + else + q <= d; +endmodule diff --git a/tests/sim/dlatch.v b/tests/sim/dlatch.v new file mode 100644 index 000000000..315b43216 --- /dev/null +++ b/tests/sim/dlatch.v @@ -0,0 +1,6 @@ +module dlatch( input d, en, output reg q ); + always @* begin + if ( en ) + q = d; + end +endmodule diff --git a/tests/sim/dlatchsr.v b/tests/sim/dlatchsr.v new file mode 100644 index 000000000..1d13ac2ad --- /dev/null +++ b/tests/sim/dlatchsr.v @@ -0,0 +1,11 @@ +module dlatchsr( input d, set, clr, en, output reg q ); + always @* begin + if ( clr ) + q = 0; + else if (set) + q = 1; + else + if (en) + q = d; + end +endmodule diff --git a/tests/sim/run-test.sh b/tests/sim/run-test.sh new file mode 100755 index 000000000..d34d1f3c9 --- /dev/null +++ b/tests/sim/run-test.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash +set -eu +source ../gen-tests-makefile.sh +echo "Generate FST for sim models" +find tb/* -name tb*.v | while read name; do + test_name=$(basename -s .v $name) + echo "Test $test_name" + verilog_name=${test_name:3}.v + iverilog -o tb/$test_name.out $name $verilog_name + ./tb/$test_name.out -fst +done +run_tests --yosys-scripts --bash --yosys-args "-w 'Yosys has only limited support for tri-state logic at the moment.'" diff --git a/tests/sim/sdff.v b/tests/sim/sdff.v new file mode 100644 index 000000000..6b25516e1 --- /dev/null +++ b/tests/sim/sdff.v @@ -0,0 +1,7 @@ +module sdff( input d, clk, rst, output reg q ); + always @( posedge clk) + if (rst) + q <= 0; + else + q <= d; +endmodule diff --git a/tests/sim/sdffce.v b/tests/sim/sdffce.v new file mode 100644 index 000000000..7d27d5741 --- /dev/null +++ b/tests/sim/sdffce.v @@ -0,0 +1,8 @@ +module sdffce( input d, clk, rst, en, output reg q ); + always @( posedge clk) + if(en) + if (rst) + q <= 0; + else + q <= d; +endmodule diff --git a/tests/sim/sdffe.v b/tests/sim/sdffe.v new file mode 100644 index 000000000..0a96693e1 --- /dev/null +++ b/tests/sim/sdffe.v @@ -0,0 +1,8 @@ +module sdffe( input d, clk, rst, en, output reg q ); + always @( posedge clk) + if (rst) + q <= 0; + else + if (en) + q <= d; +endmodule diff --git a/tests/sim/sim_adff.ys b/tests/sim/sim_adff.ys new file mode 100644 index 000000000..6efd804a9 --- /dev/null +++ b/tests/sim/sim_adff.ys @@ -0,0 +1,6 @@ +read_verilog adff.v +proc +opt_dff +stat +select -assert-count 1 t:$adff +sim -clock clk -r tb_adff.fst -scope tb_adff.uut -sim-cmp adff diff --git a/tests/sim/sim_adffe.ys b/tests/sim/sim_adffe.ys new file mode 100644 index 000000000..47a51ebce --- /dev/null +++ b/tests/sim/sim_adffe.ys @@ -0,0 +1,6 @@ +read_verilog adffe.v +proc +opt_dff +stat +select -assert-count 1 t:$adffe +sim -clock clk -r tb_adffe.fst -scope tb_adffe.uut -sim-cmp adffe diff --git a/tests/sim/sim_adlatch.ys b/tests/sim/sim_adlatch.ys new file mode 100644 index 000000000..eece7dc0d --- /dev/null +++ b/tests/sim/sim_adlatch.ys @@ -0,0 +1,10 @@ +read_verilog -icells <<EOT +module adlatch(input d, rst, en, output reg q); +$adlatch #(.EN_POLARITY(1'b1), .ARST_POLARITY(1'b1), .ARST_VALUE(1'b0), .WIDTH(1)) uut (.EN(en), .ARST(rst), .D(d), .Q(q)); +endmodule +EOT +proc +opt_dff +stat +select -assert-count 1 t:$adlatch +sim -r tb_adlatch.fst -scope tb_adlatch.uut -sim-cmp adlatch diff --git a/tests/sim/sim_aldff.ys b/tests/sim/sim_aldff.ys new file mode 100644 index 000000000..9c8b3bdfc --- /dev/null +++ b/tests/sim/sim_aldff.ys @@ -0,0 +1,6 @@ +read_verilog aldff.v +proc +opt_dff +stat +select -assert-count 1 t:$aldff +sim -clock clk -r tb_aldff.fst -scope tb_aldff.uut -sim-cmp aldff diff --git a/tests/sim/sim_aldffe.ys b/tests/sim/sim_aldffe.ys new file mode 100644 index 000000000..b191cf877 --- /dev/null +++ b/tests/sim/sim_aldffe.ys @@ -0,0 +1,6 @@ +read_verilog aldffe.v +proc +opt_dff +stat +select -assert-count 1 t:$aldffe +sim -clock clk -r tb_aldffe.fst -scope tb_aldffe.uut -sim-cmp aldffe diff --git a/tests/sim/sim_dff.ys b/tests/sim/sim_dff.ys new file mode 100644 index 000000000..12f402443 --- /dev/null +++ b/tests/sim/sim_dff.ys @@ -0,0 +1,6 @@ +read_verilog dff.v +proc +opt_dff +stat +select -assert-count 1 t:$dff +sim -clock clk -r tb_dff.fst -scope tb_dff.uut -sim-cmp dff diff --git a/tests/sim/sim_dffe.ys b/tests/sim/sim_dffe.ys new file mode 100644 index 000000000..f9b9e4767 --- /dev/null +++ b/tests/sim/sim_dffe.ys @@ -0,0 +1,6 @@ +read_verilog dffe.v +proc +opt_dff +stat +select -assert-count 1 t:$dffe +sim -clock clk -r tb_dffe.fst -scope tb_dffe.uut -sim-cmp dffe diff --git a/tests/sim/sim_dffsr.ys b/tests/sim/sim_dffsr.ys new file mode 100644 index 000000000..e99ee860d --- /dev/null +++ b/tests/sim/sim_dffsr.ys @@ -0,0 +1,6 @@ +read_verilog dffsr.v +proc +opt_dff +stat +select -assert-count 1 t:$dffsr +sim -clock clk -r tb_dffsr.fst -scope tb_dffsr.uut -sim-cmp dffsr diff --git a/tests/sim/sim_dlatch.ys b/tests/sim/sim_dlatch.ys new file mode 100644 index 000000000..79e4601e3 --- /dev/null +++ b/tests/sim/sim_dlatch.ys @@ -0,0 +1,6 @@ +read_verilog dlatch.v +proc +opt_dff +stat +select -assert-count 1 t:$dlatch +sim -r tb_dlatch.fst -scope tb_dlatch.uut -sim-cmp dlatch diff --git a/tests/sim/sim_dlatchsr.ys b/tests/sim/sim_dlatchsr.ys new file mode 100644 index 000000000..c83051c8b --- /dev/null +++ b/tests/sim/sim_dlatchsr.ys @@ -0,0 +1,10 @@ +read_verilog -icells <<EOT +module dlatchsr(input d, set, clr, en, output reg q); +$dlatchsr #(.EN_POLARITY(1'b1), .CLR_POLARITY(1'b1), .SET_POLARITY(1'b1), .WIDTH(1)) uut (.EN(en), .SET(set), .CLR(clr), .D(d), .Q(q)); +endmodule +EOT +proc +opt_dff +stat +select -assert-count 1 t:$dlatchsr +sim -r tb_dlatchsr.fst -scope tb_dlatchsr.uut -sim-cmp dlatchsr diff --git a/tests/sim/sim_sdff.ys b/tests/sim/sim_sdff.ys new file mode 100644 index 000000000..a812c5d80 --- /dev/null +++ b/tests/sim/sim_sdff.ys @@ -0,0 +1,6 @@ +read_verilog sdff.v +proc +opt_dff +stat +select -assert-count 1 t:$sdff +sim -clock clk -r tb_sdff.fst -scope tb_sdff.uut -sim-cmp sdff diff --git a/tests/sim/sim_sdffce.ys b/tests/sim/sim_sdffce.ys new file mode 100644 index 000000000..b28acb83d --- /dev/null +++ b/tests/sim/sim_sdffce.ys @@ -0,0 +1,6 @@ +read_verilog sdffce.v +proc +opt_dff +stat +select -assert-count 1 t:$sdffce +sim -clock clk -r tb_sdffce.fst -scope tb_sdffce.uut -sim-cmp sdffce diff --git a/tests/sim/sim_sdffe.ys b/tests/sim/sim_sdffe.ys new file mode 100644 index 000000000..044f78eb3 --- /dev/null +++ b/tests/sim/sim_sdffe.ys @@ -0,0 +1,6 @@ +read_verilog sdffe.v +proc +opt_dff +stat +select -assert-count 1 t:$sdffe +sim -clock clk -r tb_sdffe.fst -scope tb_sdffe.uut -sim-cmp sdffe diff --git a/tests/sim/tb/tb_adff.v b/tests/sim/tb/tb_adff.v new file mode 100755 index 000000000..f1bc3547e --- /dev/null +++ b/tests/sim/tb/tb_adff.v @@ -0,0 +1,40 @@ +`timescale 1ns/1ns +module tb_adff(); + reg clk = 0; + reg rst = 0; + reg d = 0; + wire q; + + adff uut(.clk(clk),.d(d),.rst(rst),.q(q)); + + always + #(5) clk <= !clk; + + initial + begin + $dumpfile("tb_adff"); + $dumpvars(0,tb_adff); + #10 + d = 1; + #10 + d = 0; + #10 + rst = 1; + #10 + d = 1; + #10 + d = 0; + #10 + rst = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + $finish; + end +endmodule diff --git a/tests/sim/tb/tb_adffe.v b/tests/sim/tb/tb_adffe.v new file mode 100755 index 000000000..bb23f963d --- /dev/null +++ b/tests/sim/tb/tb_adffe.v @@ -0,0 +1,58 @@ +`timescale 1ns/1ns +module tb_adffe(); + reg clk = 0; + reg rst = 0; + reg d = 0; + reg en = 0; + wire q; + + adffe uut(.clk(clk),.d(d),.rst(rst),.en(en),.q(q)); + + always + #(5) clk <= !clk; + + initial + begin + $dumpfile("tb_adffe"); + $dumpvars(0,tb_adffe); + #10 + d = 1; + #10 + d = 0; + #10 + rst = 1; + #10 + d = 1; + #10 + d = 0; + #10 + rst = 0; + #10 + d = 1; + #10 + d = 0; + #10 + en = 1; + rst = 1; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + rst = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + $finish; + end +endmodule diff --git a/tests/sim/tb/tb_adlatch.v b/tests/sim/tb/tb_adlatch.v new file mode 100755 index 000000000..59dd498d2 --- /dev/null +++ b/tests/sim/tb/tb_adlatch.v @@ -0,0 +1,70 @@ +`timescale 1ns/1ns +module tb_adlatch(); + reg clk = 0; + reg rst = 0; + reg en = 0; + reg d = 0; + wire q; + + adlatch uut(.d(d),.rst(rst),.en(en),.q(q)); + + always + #(5) clk <= !clk; + + initial + begin + $dumpfile("tb_adlatch"); + $dumpvars(0,tb_adlatch); + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + rst = 1; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + rst = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + en = 1; + rst = 1; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + rst = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + $finish; + end +endmodule diff --git a/tests/sim/tb/tb_aldff.v b/tests/sim/tb/tb_aldff.v new file mode 100755 index 000000000..0591c8b3c --- /dev/null +++ b/tests/sim/tb/tb_aldff.v @@ -0,0 +1,73 @@ +`timescale 1ns/1ns +module tb_aldff(); + reg clk = 0; + reg aload = 0; + reg [0:3] d = 4'b0000; + reg [0:3] ad = 4'b1010; + wire [0:3] q; + + aldff uut(.clk(clk),.d(d),.ad(ad),.aload(aload),.q(q)); + + always + #(5) clk <= !clk; + + initial + begin + $dumpfile("tb_aldff"); + $dumpvars(0,tb_aldff); + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + aload = 1; + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + aload = 0; + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + aload = 1; + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + aload = 0; + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + $finish; + end +endmodule diff --git a/tests/sim/tb/tb_aldffe.v b/tests/sim/tb/tb_aldffe.v new file mode 100755 index 000000000..c3cb57f4e --- /dev/null +++ b/tests/sim/tb/tb_aldffe.v @@ -0,0 +1,75 @@ +`timescale 1ns/1ns +module tb_aldffe(); + reg clk = 0; + reg aload = 0; + reg [0:3] d = 4'b0000; + reg [0:3] ad = 4'b1010; + reg en = 0; + wire [0:3] q; + + aldffe uut(.clk(clk),.d(d),.ad(ad),.aload(aload),.en(en),.q(q)); + + always + #(5) clk <= !clk; + + initial + begin + $dumpfile("tb_aldffe"); + $dumpvars(0,tb_aldffe); + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + aload = 1; + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + aload = 0; + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + en = 1; + aload = 1; + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + aload = 0; + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + d = 4'b1100; + #10 + d = 4'b0011; + #10 + $finish; + end +endmodule diff --git a/tests/sim/tb/tb_dff.v b/tests/sim/tb/tb_dff.v new file mode 100755 index 000000000..aa41d1c6c --- /dev/null +++ b/tests/sim/tb/tb_dff.v @@ -0,0 +1,47 @@ +`timescale 1ns/1ns +module tb_dff(); + reg clk = 0; + reg d = 0; + wire q; + + dff uut(.clk(clk),.d(d),.q(q)); + + always + #(5) clk <= !clk; + + initial + begin + $dumpfile("tb_dff"); + $dumpvars(0,tb_dff); + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + $finish; + end +endmodule diff --git a/tests/sim/tb/tb_dffe.v b/tests/sim/tb/tb_dffe.v new file mode 100755 index 000000000..4e262b928 --- /dev/null +++ b/tests/sim/tb/tb_dffe.v @@ -0,0 +1,42 @@ +`timescale 1ns/1ns +module tb_dffe(); + reg clk = 0; + reg en = 0; + reg d = 0; + wire q; + + dffe uut(.clk(clk),.d(d),.en(en),.q(q)); + + always + #(5) clk <= !clk; + + initial + begin + $dumpfile("tb_dffe"); + $dumpvars(0,tb_dffe); + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + en = 1; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + $finish; + end +endmodule diff --git a/tests/sim/tb/tb_dffsr.v b/tests/sim/tb/tb_dffsr.v new file mode 100755 index 000000000..6ecb85d67 --- /dev/null +++ b/tests/sim/tb/tb_dffsr.v @@ -0,0 +1,69 @@ +`timescale 1ns/1ns +module tb_dffsr(); + reg clk = 0; + reg d = 0; + reg set = 0; + reg clr = 0; + wire q; + + dffsr uut(.d(d),.clk(clk),.set(set),.clr(clr),.q(q)); + + always + #(5) clk <= !clk; + + initial + begin + $dumpfile("tb_dffsr"); + $dumpvars(0,tb_dffsr); + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + clr = 1; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + clr = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + set = 1; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + set = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + $finish; + end +endmodule diff --git a/tests/sim/tb/tb_dlatch.v b/tests/sim/tb/tb_dlatch.v new file mode 100755 index 000000000..aea6cb0a3 --- /dev/null +++ b/tests/sim/tb/tb_dlatch.v @@ -0,0 +1,50 @@ +`timescale 1ns/1ns +module tb_dlatch(); + reg clk = 0; + reg en = 0; + reg d = 0; + wire q; + + dlatch uut(.d(d),.en(en),.q(q)); + + always + #(5) clk <= !clk; + + initial + begin + $dumpfile("tb_dlatch"); + $dumpvars(0,tb_dlatch); + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + en = 1; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + $finish; + end +endmodule diff --git a/tests/sim/tb/tb_dlatchsr.v b/tests/sim/tb/tb_dlatchsr.v new file mode 100755 index 000000000..0105d3288 --- /dev/null +++ b/tests/sim/tb/tb_dlatchsr.v @@ -0,0 +1,65 @@ +`timescale 1ns/1ns +module tb_dlatchsr(); + reg d = 0; + reg set = 0; + reg clr = 0; + wire q; + + dlatchsr uut(.d(d),.set(set),.clr(clr),.q(q)); + + initial + begin + $dumpfile("tb_dlatchsr"); + $dumpvars(0,tb_dlatchsr); + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + clr = 1; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + clr = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + set = 1; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + set = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + $finish; + end +endmodule diff --git a/tests/sim/tb/tb_sdff.v b/tests/sim/tb/tb_sdff.v new file mode 100755 index 000000000..f8e2a1c9d --- /dev/null +++ b/tests/sim/tb/tb_sdff.v @@ -0,0 +1,48 @@ +`timescale 1ns/1ns +module tb_sdff(); + reg clk = 0; + reg rst = 0; + reg d = 0; + wire q; + + sdff uut(.clk(clk),.d(d),.rst(rst),.q(q)); + + always + #(5) clk <= !clk; + + initial + begin + $dumpfile("tb_sdff"); + $dumpvars(0,tb_sdff); + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + rst = 1; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + rst = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + $finish; + end +endmodule diff --git a/tests/sim/tb/tb_sdffce.v b/tests/sim/tb/tb_sdffce.v new file mode 100755 index 000000000..1c9952806 --- /dev/null +++ b/tests/sim/tb/tb_sdffce.v @@ -0,0 +1,79 @@ +`timescale 1ns/1ns +module tb_sdffce(); + reg clk = 0; + reg rst = 0; + reg d = 0; + reg en = 0; + wire q; + + sdffce uut(.clk(clk),.d(d),.rst(rst),.en(en),.q(q)); + + always + #(5) clk <= !clk; + + initial + begin + $dumpfile("tb_sdffce"); + $dumpvars(0,tb_sdffce); + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + rst = 1; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + rst = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + en = 1; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + rst = 1; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + rst = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + $finish; + end +endmodule diff --git a/tests/sim/tb/tb_sdffe.v b/tests/sim/tb/tb_sdffe.v new file mode 100755 index 000000000..36072f93d --- /dev/null +++ b/tests/sim/tb/tb_sdffe.v @@ -0,0 +1,70 @@ +`timescale 1ns/1ns +module tb_sdffe(); + reg clk = 0; + reg rst = 0; + reg d = 0; + reg en = 0; + wire q; + + sdffe uut(.clk(clk),.d(d),.rst(rst),.en(en),.q(q)); + + always + #(5) clk <= !clk; + + initial + begin + $dumpfile("tb_sdffe"); + $dumpvars(0,tb_sdffe); + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + rst = 1; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + rst = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + en = 1; + rst = 1; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + rst = 0; + #10 + d = 1; + #10 + d = 0; + #10 + d = 1; + #10 + d = 0; + #10 + $finish; + end +endmodule diff --git a/tests/various/.gitignore b/tests/various/.gitignore index 2bb6c7179..c6373468a 100644 --- a/tests/various/.gitignore +++ b/tests/various/.gitignore @@ -5,3 +5,4 @@ /run-test.mk /plugin.so /plugin.so.dSYM +/temp diff --git a/tests/various/json_escape_chars.ys b/tests/various/json_escape_chars.ys new file mode 100644 index 000000000..f118357c0 --- /dev/null +++ b/tests/various/json_escape_chars.ys @@ -0,0 +1,14 @@ +! mkdir -p temp +read_verilog <<EOT +(* src = "\042 \057 \134 \010 \014 \012 \015 \011 \025 \033" *) +module foo; +endmodule +EOT +write_json temp/test_escapes.json +design -reset +read_json temp/test_escapes.json +write_json temp/test_escapes.json +design -reset +read_json temp/test_escapes.json +write_rtlil temp/test_escapes.json.il +! grep -F 'attribute \src "\" / \\ \010 \014 \n \015 \t \025 \033"' temp/test_escapes.json.il diff --git a/tests/various/param_struct.ys b/tests/various/param_struct.ys index 6d7a7c6ad..b8de67968 100644 --- a/tests/various/param_struct.ys +++ b/tests/various/param_struct.ys @@ -41,8 +41,7 @@ always_comb begin assert(j == 1'b1); assert(k == 1'b0); assert(l == 3'b111); -// TODO: support access to whole sub-structs and unions -// assert(m == 2'b10); + assert(m == 2'b10); assert(u == 5'b11001); end endmodule diff --git a/tests/various/struct_access.sv b/tests/various/struct_access.sv new file mode 100644 index 000000000..d41a7114f --- /dev/null +++ b/tests/various/struct_access.sv @@ -0,0 +1,43 @@ +module dut(); +typedef struct packed { + logic a; + logic b; +} sub_sub_struct_t; + +typedef struct packed { + sub_sub_struct_t c; +} sub_struct_t; + +typedef struct packed { + sub_struct_t d; + sub_struct_t e; +} struct_t; + +parameter struct_t P = 4'b1100; + +localparam sub_struct_t f = P.d; +localparam sub_struct_t g = P.e; +localparam sub_sub_struct_t h = f.c; +localparam logic i = P.d.c.a; +localparam logic j = P.d.c.b; +localparam x = P.e; +localparam y = x.c; +localparam z = y.a; +localparam q = P.d; +localparam n = q.c.a; + +always_comb begin + assert(P == 4'b1100); + assert(f == 2'b11); + assert(g == 2'b00); + assert(h == 2'b11); + assert(i == 1'b1); + assert(j == 1'b1); + assert(x == 2'b00); + assert(y == 2'b00); + assert(x.c == 2'b00); + assert(y.b == 1'b0); + assert(n == 1'b1); + assert(z == 1'b0); +end +endmodule diff --git a/tests/various/struct_access.ys b/tests/various/struct_access.ys new file mode 100644 index 000000000..2282edd92 --- /dev/null +++ b/tests/various/struct_access.ys @@ -0,0 +1,5 @@ +read_verilog -sv struct_access.sv +hierarchy +proc +opt +sat -verify -seq 1 -prove-asserts -show-all diff --git a/tests/verilog/delay_time_scale.ys b/tests/verilog/delay_time_scale.ys new file mode 100644 index 000000000..f45ba7b26 --- /dev/null +++ b/tests/verilog/delay_time_scale.ys @@ -0,0 +1,25 @@ +logger -expect-no-warnings +read_verilog -sv <<EOT +module top; +wand x; +`define TEST(time_scale) if (1) assign #time_scale x = 1; + +`TEST(1s) +`TEST(1ms) +`TEST(1us) +`TEST(1ns) +`TEST(1ps) +`TEST(1fs) + +`TEST((1s)) +`TEST(( 1s)) +`TEST((1s )) +`TEST(( 1s )) + +`TEST(1.0s) +`TEST(1.1s) +`TEST(1.0e-1s) +`TEST(1e-1s) + +endmodule +EOT diff --git a/tests/verilog/dynamic_range_lhs.sh b/tests/verilog/dynamic_range_lhs.sh new file mode 100755 index 000000000..618204aed --- /dev/null +++ b/tests/verilog/dynamic_range_lhs.sh @@ -0,0 +1,32 @@ +#!/bin/bash + +run() { + alt=$1 + span=$2 + left=$3 + right=$4 + echo "a=$alt s=$span l=$left r=$right" + + ../../yosys -q \ + -DALT=$alt \ + -DSPAN=$span \ + -DLEFT=$left \ + -DRIGHT=$right \ + -p "read_verilog dynamic_range_lhs.v" \ + -p "proc" \ + -p "equiv_make gold gate equiv" \ + -p "equiv_simple" \ + -p "equiv_status -assert" +} + +trap 'echo "ERROR in dynamic_range_lhs.sh span=$span left=$left right=$right" >&2; exit 1' ERR + +for alt in `seq 0 1`; do +for span in `seq 1 4`; do +for left in `seq -4 4`; do +for right in `seq $(expr $left + -3) $(expr $left + 3)`; do + run $alt $span $left $right +done +done +done +done diff --git a/tests/verilog/dynamic_range_lhs.v b/tests/verilog/dynamic_range_lhs.v new file mode 100644 index 000000000..ae291374d --- /dev/null +++ b/tests/verilog/dynamic_range_lhs.v @@ -0,0 +1,76 @@ +module gate( + output reg [`LEFT:`RIGHT] out_u, out_s, + (* nowrshmsk = `ALT *) + input wire data, + input wire [1:0] sel1, sel2 +); +always @* begin + out_u = 0; + out_s = 0; + case (`SPAN) + 1: begin + out_u[sel1*sel2] = data; + out_s[$signed(sel1*sel2)] = data; + end + 2: begin + out_u[sel1*sel2+:2] = {data, data}; + out_s[$signed(sel1*sel2)+:2] = {data, data}; + end + 3: begin + out_u[sel1*sel2+:3] = {data, data, data}; + out_s[$signed(sel1*sel2)+:3] = {data, data, data}; + end + 4: begin + out_u[sel1*sel2+:4] = {data, data, data, data}; + out_s[$signed(sel1*sel2)+:4] = {data, data, data, data}; + end + endcase +end +endmodule + +module gold( + output reg [`LEFT:`RIGHT] out_u, out_s, + input wire data, + input wire [1:0] sel1, sel2 +); +task set; + input integer a, b; + localparam LOW = `LEFT > `RIGHT ? `RIGHT : `LEFT; + localparam HIGH = `LEFT > `RIGHT ? `LEFT : `RIGHT; + if (LOW <= a && a <= HIGH) + out_u[a] = data; + if (LOW <= b && b <= HIGH) + out_s[b] = data; +endtask +always @* begin + out_u = 0; + out_s = 0; + case (sel1*sel2) + 2'b00: set(0, 0); + 2'b01: set(1, 1); + 2'b10: set(2, -2); + 2'b11: set(3, -1); + endcase + if (`SPAN >= 2) + case (sel1*sel2) + 2'b00: set(1, 1); + 2'b01: set(2, 2); + 2'b10: set(3, -1); + 2'b11: set(4, 0); + endcase + if (`SPAN >= 3) + case (sel1*sel2) + 2'b00: set(2, 2); + 2'b01: set(3, 3); + 2'b10: set(4, 0); + 2'b11: set(5, 1); + endcase + if (`SPAN >= 4) + case (sel1*sel2) + 2'b00: set(3, 3); + 2'b01: set(4, 4); + 2'b10: set(5, 1); + 2'b11: set(6, 2); + endcase +end +endmodule diff --git a/tests/verilog/func_upto.sv b/tests/verilog/func_upto.sv new file mode 100644 index 000000000..547e5d325 --- /dev/null +++ b/tests/verilog/func_upto.sv @@ -0,0 +1,77 @@ +`default_nettype none + +module evil; + parameter HI = 3; + parameter LO = 0; + parameter SPAN = 1; + parameter [HI:LO] A_VAL = 4'b0110; + parameter [HI:LO] B_VAL = 4'b1100; + parameter [2:0] SWAPS = 0; + + localparam D_LEFT = !(SWAPS[0]) ? HI : LO; + localparam D_RIGHT = (SWAPS[0]) ? HI : LO; + localparam E_LEFT = !(SWAPS[1]) ? HI : LO; + localparam E_RIGHT = (SWAPS[1]) ? HI : LO; + localparam F_LEFT = !(SWAPS[2]) ? HI : LO; + localparam F_RIGHT = (SWAPS[2]) ? HI : LO; + + localparam [HI:LO] A_CONST = A_VAL; + localparam [HI:LO] B_CONST = B_VAL; + localparam [HI:LO] C_CONST = F(A_CONST, B_CONST); + + reg [HI:LO] C_WIRE, C_FUNC; + always @* begin + assert (C_CONST == C_WIRE); + assert (C_CONST == C_FUNC); + end + + initial begin : blk + reg [HI:LO] A_WIRE; + reg [HI:LO] B_WIRE; + reg [D_LEFT:D_RIGHT] D; + reg [E_LEFT:E_RIGHT] E; + reg [F_LEFT:F_RIGHT] F_WIRE; + reg [31:0] i; + A_WIRE = A_VAL; + B_WIRE = B_VAL; + D = A_WIRE; + E = B_WIRE; + F_WIRE = 0; + for (i = LO; i + SPAN < HI; i = i + SPAN) + if (SPAN == 1) + F_WIRE[i] = D[i] && E[i]; + else + F_WIRE[i+:SPAN] = D[i+:SPAN] && E[i+:SPAN]; + C_WIRE = F_WIRE; + C_FUNC = F(A_WIRE, B_WIRE); + end + + function automatic [F_LEFT:F_RIGHT] F( + input [D_LEFT:D_RIGHT] D, + input [E_LEFT:E_RIGHT] E); + reg [31:0] i; + F = 0; + for (i = LO; i + SPAN < HI; i = i + SPAN) + if (SPAN == 1) + F[i] = D[i] && E[i]; + else + F[i+:SPAN] = D[i+:SPAN] && E[i+:SPAN]; + endfunction +endmodule + +module top; + for (genvar hi = 0; hi < 3; hi++) + for (genvar lo = 0; lo <= hi; lo++) + for (genvar span = 1; span <= hi - lo + 1; span++) + for (genvar a_val = 0; a_val < 2 ** (hi - lo + 1); a_val++) + for (genvar b_val = 0; b_val < 2 ** (hi - lo + 1); b_val++) + for (genvar swaps = 0; swaps < 2 ** 3; swaps++) + evil #( + .HI(hi), + .LO(lo), + .SPAN(span), + .A_VAL(a_val), + .B_VAL(b_val), + .SWAPS(swaps) + ) e(); +endmodule diff --git a/tests/verilog/func_upto.ys b/tests/verilog/func_upto.ys new file mode 100644 index 000000000..7a8c53506 --- /dev/null +++ b/tests/verilog/func_upto.ys @@ -0,0 +1,7 @@ +read_verilog -sv func_upto.sv +hierarchy -top top +proc +flatten +opt -full +select -module top +sat -verify -seq 1 -prove-asserts -enable_undef diff --git a/tests/verilog/struct_access.sv b/tests/verilog/struct_access.sv index f13b8dd51..bc91e3f01 100644 --- a/tests/verilog/struct_access.sv +++ b/tests/verilog/struct_access.sv @@ -77,9 +77,8 @@ module top; `CHECK(s.y.a, 1, 0) `CHECK(s.y.b, 1, 1) - // TODO(zachjs): support access to whole sub-structs and unions - // `CHECK(s.x, 2, 0) - // `CHECK(s.y, 2, 1) + `CHECK(s.x, 2, 0) + `CHECK(s.y, 2, 1) assert (fail === 0); end |