diff --git a/.gitignore b/.gitignore index d163863..3c0160d 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ -build/ \ No newline at end of file +build/ +out/ diff --git a/.gitmodules b/.gitmodules index 9552b04..9f09b32 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,6 +1,6 @@ [submodule "fusesoc_libraries/serv"] path = fusesoc_libraries/serv - url = https://github.com/Jojojoppe/serv/tree/xilinx_ise + url = git@github.com:Jojojoppe/serv.git [submodule "fusesoc_libraries/fusesoc-cores"] path = fusesoc_libraries/fusesoc-cores url = https://github.com/fusesoc/fusesoc-cores diff --git a/cores/wb/check_formal.sh b/check_formal.sh similarity index 97% rename from cores/wb/check_formal.sh rename to check_formal.sh index 4df22a7..9155dd7 100755 --- a/cores/wb/check_formal.sh +++ b/check_formal.sh @@ -9,6 +9,10 @@ joppeb:wb:jtag_wb_bridge joppeb:wb:wb_timer " +if [ -n "$1" ]; then + CORES="$1" +fi + # Add or remove formal tasks here. TASKS=" bmc diff --git a/cores/system/mcu/rtl/mcu_peripherals.v b/cores/system/mcu/rtl/mcu_peripherals.v index 771445e..d5ea5b9 100644 --- a/cores/system/mcu/rtl/mcu_peripherals.v +++ b/cores/system/mcu/rtl/mcu_peripherals.v @@ -44,7 +44,9 @@ module mcu_peripherals ( wire [31:0] gpio_wbs_dat_r; wire gpio_wbs_ack; + wire [31:0] timer_wbs_adr = wbs_adr[1*32 +: 32]; wire [31:0] timer_wbs_dat_w = wbs_dat_w[1*32 +: 32]; + wire [3:0] timer_wbs_sel = wbs_sel[1*4 +: 4]; wire timer_wbs_we = wbs_we[1]; wire timer_wbs_cyc = wbs_cyc[1]; wire timer_wbs_stb = wbs_stb[1]; @@ -108,12 +110,16 @@ module mcu_peripherals ( assign wbs_dat_r[0*32 +: 32] = gpio_wbs_dat_r; assign wbs_ack[0] = gpio_wbs_ack; - wb_countdown_timer timer ( + wb_countdown_timer #( + .address(TIMER_BASE_ADDR) + ) timer ( .i_clk(i_clk), .i_rst(i_rst), .o_irq(o_timer_irq), + .i_wb_adr(timer_wbs_adr), .i_wb_dat(timer_wbs_dat_w), .o_wb_dat(timer_wbs_dat_r), + .i_wb_sel(timer_wbs_sel), .i_wb_we(timer_wbs_we), .i_wb_cyc(timer_wbs_cyc), .i_wb_stb(timer_wbs_stb), diff --git a/cores/system/test/rtl/toplevel.v b/cores/system/test/rtl/toplevel.v index 093a97d..e14c9f8 100644 --- a/cores/system/test/rtl/toplevel.v +++ b/cores/system/test/rtl/toplevel.v @@ -1,7 +1,8 @@ `timescale 1ns/1ps module toplevel #( - parameter sim = 0 + parameter sim = 0, + parameter memfile = "sweep.hex" )( input wire aclk, input wire aresetn, @@ -57,7 +58,7 @@ module toplevel #( wire test; mcu #( - .memfile("../sw/sweep/sweep.hex"), + .memfile(memfile), .sim(sim), .jtag(1) ) mcu ( diff --git a/cores/system/test/sw/sweep/sweep.c b/cores/system/test/sw/sweep/sweep.c index 038db42..447ba27 100644 --- a/cores/system/test/sw/sweep/sweep.c +++ b/cores/system/test/sw/sweep/sweep.c @@ -6,7 +6,9 @@ static volatile uint32_t * const LEDS = (volatile uint32_t *)(GPIO_BASE+4) static volatile uint32_t * const LEDGR = (volatile uint32_t *)(GPIO_BASE+8); #define TIMER_BASE 0x40010000u -static volatile uint32_t * const TIMER = (volatile uint32_t *)(TIMER_BASE+0); +static volatile uint32_t * const TIMER_CNT = (volatile uint32_t *)(TIMER_BASE+0); +static volatile uint32_t * const TIMER_LD = (volatile uint32_t *)(TIMER_BASE+4); +static volatile uint32_t * const TIMER_ACK = (volatile uint32_t *)(TIMER_BASE+8); #define MSTATUS_MIE (1u << 3) #define MIE_MTIE (1u << 7) @@ -25,21 +27,21 @@ static inline void irq_init() { } void timer_isr(){ - static int set = 0; - *TIMER = 1840000*8; + *TIMER_ACK = 1; *LEDGR = ~(*LEDGR); } void main(){ irq_init(); - *LEDGR = 3; - *TIMER = 1840000*2; + *LEDGR = 1; + *TIMER_LD = 2 * 15000000/1000; for(;;){ - for(int i=1000; i<10000; i++){ + for(int i=1000; i<10000; i+=10){ *R_FREQ = i; - for(int j=0; j<80; j++) asm volatile("nop"); + *LEDS = i>>4; + // for(int j=0; j<80; j++) asm volatile("nop"); } } } \ No newline at end of file diff --git a/cores/system/test/tb/tb_toplevel.v b/cores/system/test/tb/tb_toplevel.v new file mode 100644 index 0000000..0be568b --- /dev/null +++ b/cores/system/test/tb/tb_toplevel.v @@ -0,0 +1,37 @@ +`timescale 1ns/1ps + +module tb_toplevel; + reg aclk; + reg aresetn; + wire led_green; + wire led_red; + wire [5:0] r2r; + wire [7:0] LED; + + toplevel #( + .sim(1) + ) dut ( + .aclk(aclk), + .aresetn(aresetn), + .led_green(led_green), + .led_red(led_red), + .r2r(r2r), + .LED(LED) + ); + + initial aclk = 1'b0; + always #33.33 aclk = ~aclk; + + initial begin + $dumpfile("toplevel.vcd"); + $dumpvars(1, tb_toplevel); + + aresetn = 1'b0; + #100; + aresetn = 1'b1; + + #10_000_000; + + $finish; + end +endmodule diff --git a/cores/system/test/test.core b/cores/system/test/test.core index 0702eae..31c1f11 100644 --- a/cores/system/test/test.core +++ b/cores/system/test/test.core @@ -13,10 +13,14 @@ filesets: files: - rtl/toplevel.v file_type: verilogSource + tb: + files: + - tb/tb_toplevel.v + file_type: verilogSource sw: files: - - sw/sweep/sweep.hex + - sw/sweep/sweep.hex : {copyto : sweep.hex} file_type: user mimas: @@ -29,6 +33,13 @@ targets: filesets: - rtl toplevel: toplevel + sim: + default_tool: icarus + filesets: + - rtl + - sw + - tb + toplevel: tb_toplevel mimas: filesets: diff --git a/cores/wb/formal_checker/formal/formal_wb_master_checker.v b/cores/wb/formal_checker/formal/formal_wb_master_checker.v index 68dc7c6..13f4ae9 100644 --- a/cores/wb/formal_checker/formal/formal_wb_master_checker.v +++ b/cores/wb/formal_checker/formal/formal_wb_master_checker.v @@ -22,14 +22,14 @@ module formal_wb_master_checker ( // A1: Slave ACK must correspond to either a same-cycle or previous-cycle request if(o_wb_ack) - assume( + A1: assume( (i_wb_cyc && i_wb_stb) || (f_past_valid && $past(i_wb_cyc && i_wb_stb)) ); // A2: Slave must not ACK outside an active cycle if(!i_wb_cyc) - assume(!o_wb_ack); + A2: assume(!o_wb_ack); // A3: Once STB has been low for a full cycle, slave ACK must be low if( @@ -37,19 +37,19 @@ module formal_wb_master_checker ( !$past(i_wb_stb) && !i_wb_stb ) - assume(!o_wb_ack); + A3: assume(!o_wb_ack); // R1: Reset must leave the master initialized on the following cycle if(f_past_valid && $past(i_rst || i_wb_rst)) begin - assert(!i_wb_cyc); - assert(!i_wb_stb); + R1: assert(!i_wb_cyc); + R2: assert(!i_wb_stb); end - // R2: STB never high without CYC + // R3: STB never high without CYC if(i_wb_stb) - assert(i_wb_cyc); + R3: assert(i_wb_cyc); - // R3: Once a request starts, hold it stable until the slave responds + // R4-R9: Once a request starts, hold it stable until the slave responds if( f_past_valid && !$past(i_rst || i_wb_rst) && @@ -57,40 +57,40 @@ module formal_wb_master_checker ( !o_wb_ack && !(i_rst || i_wb_rst) ) begin - assert(i_wb_cyc); - assert(i_wb_stb); - assert(i_wb_adr == $past(i_wb_adr)); - assert(i_wb_dat == $past(i_wb_dat)); - assert(i_wb_sel == $past(i_wb_sel)); - assert(i_wb_we == $past(i_wb_we)); + R4: assert(i_wb_cyc); + R5: assert(i_wb_stb); + R6: assert(i_wb_adr == $past(i_wb_adr)); + R7: assert(i_wb_dat == $past(i_wb_dat)); + R8: assert(i_wb_sel == $past(i_wb_sel)); + R9: assert(i_wb_we == $past(i_wb_we)); end - // R4: Once CYC is low, STB must also be low + // R10: Once CYC is low, STB must also be low if(!i_wb_cyc) - assert(!i_wb_stb); + R10: assert(!i_wb_stb); - // C0: We eventually initiate a request - cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb); + // C1: We eventually initiate a request + C1: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb); - // C1: We eventually get an ACK during an active request - cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && o_wb_ack); + // C2: We eventually get an ACK during an active request + C2: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && o_wb_ack); - // C2: A delayed ACK occurs for a request issued in a previous cycle. + // C3: A delayed ACK occurs for a request issued in a previous cycle. // This does not require the request to drop in the ACK cycle. - cover(f_past_valid && !i_rst && !i_wb_rst && + C3: cover(f_past_valid && !i_rst && !i_wb_rst && $past(i_wb_cyc && i_wb_stb) && o_wb_ack); // C4: A “wait state” happens: request asserted, no ACK for at least 1 cycle - cover(f_past_valid && !i_rst && !i_wb_rst && + C4: cover(f_past_valid && !i_rst && !i_wb_rst && $past(i_wb_cyc && i_wb_stb && !o_wb_ack) && (i_wb_cyc && i_wb_stb && !o_wb_ack)); - // C5: Read and write both occur (even if only once each) - cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && !i_wb_we); - cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && i_wb_we); + // C5-C6: Read and write both occur (even if only once each) + C5: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && !i_wb_we); + C6: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && i_wb_we); - // C6: A transfer completes and the master drops CYC sometime after - cover(f_past_valid && !i_rst && !i_wb_rst && + // C7: A transfer completes and the master drops CYC sometime after + C7: cover(f_past_valid && !i_rst && !i_wb_rst && $past(i_wb_cyc && i_wb_stb && o_wb_ack) && !i_wb_cyc); end diff --git a/cores/wb/formal_checker/formal/formal_wb_slave_checker.v b/cores/wb/formal_checker/formal/formal_wb_slave_checker.v index 866e730..b1217fb 100644 --- a/cores/wb/formal_checker/formal/formal_wb_slave_checker.v +++ b/cores/wb/formal_checker/formal/formal_wb_slave_checker.v @@ -1,7 +1,8 @@ `timescale 1ns/1ps module formal_wb_slave_checker #( - parameter combinatorial_ack = 0 + parameter combinatorial_ack = 0, + parameter expect_wait_state = 0 ) ( input wire i_clk, input wire i_rst, @@ -24,38 +25,38 @@ module formal_wb_slave_checker #( // A1: Reset forces cyc=0, stb=0 if (i_rst) begin - assume(!i_wb_cyc); - assume(!i_wb_stb); + A1: assume(!i_wb_cyc); + A2: assume(!i_wb_stb); end - // A2: std->cyc, stb never high without cyc + // A3: std->cyc, stb never high without cyc if(i_wb_stb) - assume(i_wb_cyc); + A3: assume(i_wb_cyc); - // A3: once a request starts, hold it stable until the slave responds + // A4-A9: once a request starts, hold it stable until the slave responds if(f_past_valid && $past(i_wb_cyc && i_wb_stb && !o_wb_ack)) begin - assume(i_wb_cyc); - assume(i_wb_stb); - assume(i_wb_adr == $past(i_wb_adr)); - assume(i_wb_dat == $past(i_wb_dat)); - assume(i_wb_sel == $past(i_wb_sel)); - assume(i_wb_we == $past(i_wb_we)); + A4: assume(i_wb_cyc); + A5: assume(i_wb_stb); + A6: assume(i_wb_adr == $past(i_wb_adr)); + A7: assume(i_wb_dat == $past(i_wb_dat)); + A8: assume(i_wb_sel == $past(i_wb_sel)); + A9: assume(i_wb_we == $past(i_wb_we)); end // R1: ACK must correspond to either a same-cycle or previous-cycle request if(o_wb_ack) - assert( + R1: assert( (i_wb_cyc && i_wb_stb) || (f_past_valid && $past(i_wb_cyc && i_wb_stb)) ); // R2: !CYC->!ACK : no ghost acks if(!i_wb_cyc) - assert(!o_wb_ack); + R2: assert(!o_wb_ack); // R3: Reset must leave the slave initialized on the following cycle if(f_past_valid && $past(i_rst || i_wb_rst)) - assert(!o_wb_ack); + R3: assert(!o_wb_ack); // R4: once STB has been dropped for a full cycle, ACK must be low if( @@ -63,34 +64,35 @@ module formal_wb_slave_checker #( !$past(i_wb_stb) && !i_wb_stb ) - assert(!o_wb_ack); + R4: assert(!o_wb_ack); - // C0: A request occurs at all - cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb); + // C1: A request occurs at all + C1: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb); - // C1: A request with write and with read occur - cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && i_wb_we); - cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && !i_wb_we); + // C2-C3: A request with write and with read occur + C2: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && i_wb_we); + C3: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && !i_wb_we); - // C2: ACK happens during a request (basic progress) - cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && o_wb_ack); + // C4: ACK happens during a request (basic progress) + C4: cover(f_past_valid && !i_rst && !i_wb_rst && i_wb_cyc && i_wb_stb && o_wb_ack); - // C3: Exercise the expected ACK timing style for this slave. + // C5-C7: Exercise the expected ACK timing style for this slave. if (combinatorial_ack) begin - cover(f_past_valid && !i_rst && !i_wb_rst && + C5: cover(f_past_valid && !i_rst && !i_wb_rst && (i_wb_cyc && i_wb_stb) && o_wb_ack); end else begin - cover(f_past_valid && !i_rst && !i_wb_rst && + C6: cover(f_past_valid && !i_rst && !i_wb_rst && $past(i_wb_cyc && i_wb_stb) && o_wb_ack); - // C4: Wait-state behavior for registered/non-zero-wait slaves. - cover(f_past_valid && !i_rst && !i_wb_rst && - $past(i_wb_cyc && i_wb_stb && !o_wb_ack) && - (i_wb_cyc && i_wb_stb && !o_wb_ack)); + // C7: Optional wait-state behavior for slaves that intentionally stall. + if (expect_wait_state) + C7: cover(f_past_valid && !i_rst && !i_wb_rst && + $past(i_wb_cyc && i_wb_stb && !o_wb_ack) && + (i_wb_cyc && i_wb_stb && !o_wb_ack)); end - // C5: Master ends a cycle (CYC drops) after at least one request - cover(f_past_valid && !i_rst && !i_wb_rst && + // C8: Master ends a cycle (CYC drops) after at least one request + C8: cover(f_past_valid && !i_rst && !i_wb_rst && $past(i_wb_cyc && i_wb_stb) && !i_wb_cyc); end diff --git a/cores/wb/wb_gpio/formal/wb_gpio/config.sby b/cores/wb/wb_gpio/formal/wb_gpio/config.sby deleted file mode 100644 index 0fbf6d2..0000000 --- a/cores/wb/wb_gpio/formal/wb_gpio/config.sby +++ /dev/null @@ -1,13 +0,0 @@ -[options] -mode prove -depth 8 - -[engines] -smtbmc z3 parallel.enable=true parallel.threads.max=8 - -[script] -{{"-formal"|gen_reads}} -prep -top {{top_level}} - -[files] -{{files}} diff --git a/cores/wb/wb_gpio/formal/wb_gpio/logfile.txt b/cores/wb/wb_gpio/formal/wb_gpio/logfile.txt deleted file mode 100644 index 5bc85e5..0000000 --- a/cores/wb/wb_gpio/formal/wb_gpio/logfile.txt +++ /dev/null @@ -1,2 +0,0 @@ -SBY 17:32:33 [cores/wb/wb_gpio/formal/wb_gpio] Removing directory '/data/joppe/projects/fusesoc_test/cores/wb/wb_gpio/formal/wb_gpio'. -SBY 17:32:33 [cores/wb/wb_gpio/formal/wb_gpio] Copy '/data/joppe/projects/fusesoc_test/{{files}}' to '/data/joppe/projects/fusesoc_test/cores/wb/wb_gpio/formal/wb_gpio/src/{{files}}'. diff --git a/cores/wb/wb_timer/formal/formal_wb_timer.v b/cores/wb/wb_timer/formal/formal_wb_timer.v index 848c8e3..ee82a09 100644 --- a/cores/wb/wb_timer/formal/formal_wb_timer.v +++ b/cores/wb/wb_timer/formal/formal_wb_timer.v @@ -1,9 +1,6 @@ `timescale 1ns/1ps -module formal_wb_timer #( - parameter WIDTH = 8, - parameter DIVIDER = 0 -); +module formal_wb_timer; (* gclk *) reg i_clk; (* anyseq *) reg i_rst; (* anyseq *) reg [31:0] i_wb_adr; @@ -20,15 +17,14 @@ module formal_wb_timer #( assign i_wb_rst = 1'b0; - wb_countdown_timer #( - .WIDTH(WIDTH), - .DIVIDER(DIVIDER) - ) dut ( + wb_countdown_timer dut ( .i_clk(i_clk), .i_rst(i_rst), .o_irq(o_irq), + .i_wb_adr(i_wb_adr), .i_wb_dat(i_wb_dat), .o_wb_dat(o_wb_dat), + .i_wb_sel(i_wb_sel), .i_wb_we(i_wb_we), .i_wb_cyc(i_wb_cyc), .i_wb_stb(i_wb_stb), @@ -36,7 +32,7 @@ module formal_wb_timer #( ); formal_wb_slave_checker #( - .combinatorial_ack(1) + .combinatorial_ack(0) ) wb_checker ( .i_clk(i_clk), .i_rst(i_rst), diff --git a/cores/wb/wb_timer/formal/wb_timer.sby b/cores/wb/wb_timer/formal/wb_timer.sby index be55a8b..f6d6f5b 100644 --- a/cores/wb/wb_timer/formal/wb_timer.sby +++ b/cores/wb/wb_timer/formal/wb_timer.sby @@ -13,7 +13,7 @@ prove: mode prove [engines] bmc: smtbmc yices cover: smtbmc yices -prove: abc pdr +prove: smtbmc yices [script] {{"-formal"|gen_reads}} diff --git a/cores/wb/wb_timer/rtl/wb_timer.v b/cores/wb/wb_timer/rtl/wb_timer.v index ac14586..0370c3a 100644 --- a/cores/wb/wb_timer/rtl/wb_timer.v +++ b/cores/wb/wb_timer/rtl/wb_timer.v @@ -1,74 +1,100 @@ `timescale 1ns/1ps module wb_countdown_timer #( - parameter WIDTH = 32, // counter width (<=32 makes bus mapping easy) - parameter DIVIDER = 0 // optional prescaler: tick every 2^DIVIDER cycles + parameter address = 32'h00000000 // Base address of peripheral )( input wire i_clk, input wire i_rst, - output reg o_irq, + output wire o_irq, + input wire [31:0] i_wb_adr, input wire [31:0] i_wb_dat, output reg [31:0] o_wb_dat, + input wire [3:0] i_wb_sel, input wire i_wb_we, input wire i_wb_cyc, input wire i_wb_stb, output wire o_wb_ack ); - // One-cycle acknowledge on any valid WB access - // (classic, zero-wait-state peripheral) - assign o_wb_ack = i_wb_cyc & i_wb_stb; + // Registers + reg [31:0] counter; // The actual counter. Generates an interrupt when it reaches 0 + reg [31:0] preload; // The value with which the counter gets loaded after it reaches 0. 0 to keep the timer off - // Internal countdown and prescaler - reg [WIDTH-1:0] counter; - reg [DIVIDER:0] presc; // enough bits to count up to 2^DIVIDER-1 - wire tick = (DIVIDER == 0) ? 1'b1 : (presc[DIVIDER] == 1'b1); + reg wb_ack = 0; + reg irq_fired = 0; + reg counter_started = 0; + reg counter_running = 0; + reg prev_counter_running = 0; + assign o_wb_ack = wb_ack; - // Readback: expose the current counter value - always @(*) begin - o_wb_dat = 32'd0; - o_wb_dat[WIDTH-1:0] = counter; - end + assign o_irq = irq_fired; - // Main logic always @(posedge i_clk) begin - if (i_rst) begin - counter <= {WIDTH{1'b0}}; - presc <= { (DIVIDER+1){1'b0} }; - o_irq <= 1'b0; + if(i_rst) begin + counter <= 0; + preload <= 0; + wb_ack <= 0; + o_wb_dat <= 0; + irq_fired <= 0; + counter_started <= 0; + counter_running <= 0; + prev_counter_running <= 0; end else begin - // Default prescaler behavior - if (DIVIDER != 0) begin - if (counter != 0 && !o_irq) - presc <= presc + 1'b1; - else - presc <= { (DIVIDER+1){1'b0} }; - end - // Wishbone write: load counter and clear IRQ - if (o_wb_ack && i_wb_we) begin - counter <= i_wb_dat[WIDTH-1:0]; - o_irq <= 1'b0; + prev_counter_running <= counter_running; + counter_running <= counter>0; - // reset prescaler on (re)start or stop - presc <= { (DIVIDER+1){1'b0} }; + if(!irq_fired && prev_counter_running && !counter_running) + irq_fired <= 1'b1; + if(counter>0 && counter_started) + counter <= counter - 1; - end else begin - // Countdown when running (counter>0), not already IRQ'd - if (!o_irq && counter != 0) begin - if (tick) begin - if (counter == 1) begin - counter <= {WIDTH{1'b0}}; - o_irq <= 1'b1; // sticky until next write - presc <= { (DIVIDER+1){1'b0} }; - end else begin - counter <= counter - 1'b1; - end - end + if(counter == 0 && preload>0 && counter_started) + counter <= preload; + + if(counter == 0 && preload == 0) + counter_started <= 1'b0; + + // Ack generation + wb_ack <= i_wb_cyc & i_wb_stb & !wb_ack; + + // Read cycle + if(i_wb_cyc && i_wb_stb && !i_wb_we) begin + if(i_wb_adr[3:0] == 4'b0000) begin + if(i_wb_sel[0]) o_wb_dat[7:0] <= counter[7:0]; + if(i_wb_sel[1]) o_wb_dat[15:8] <= counter[15:8]; + if(i_wb_sel[2]) o_wb_dat[23:16] <= counter[23:16]; + if(i_wb_sel[3]) o_wb_dat[31:24] <= counter[31:24]; + end else if(i_wb_adr[3:0] == 4'b0100) begin + if(i_wb_sel[0]) o_wb_dat[7:0] <= preload[7:0]; + if(i_wb_sel[1]) o_wb_dat[15:8] <= preload[15:8]; + if(i_wb_sel[2]) o_wb_dat[23:16] <= preload[23:16]; + if(i_wb_sel[3]) o_wb_dat[31:24] <= preload[31:24]; end end + + // write cycle + if(i_wb_cyc && i_wb_stb && i_wb_we) begin + if(i_wb_adr[3:0] == 4'b0000) begin + if(i_wb_sel[0]) counter[7:0] <= i_wb_dat[7:0]; + if(i_wb_sel[1]) counter[15:8] <= i_wb_dat[15:8]; + if(i_wb_sel[2]) counter[23:16] <= i_wb_dat[23:16]; + if(i_wb_sel[3]) counter[31:24] <= i_wb_dat[31:24]; + counter_started <= 1'b1; + end else if(i_wb_adr[3:0] == 4'b0100) begin + if(i_wb_sel[0]) preload[7:0] <= i_wb_dat[7:0]; + if(i_wb_sel[1]) preload[15:8] <= i_wb_dat[15:8]; + if(i_wb_sel[2]) preload[23:16] <= i_wb_dat[23:16]; + if(i_wb_sel[3]) preload[31:24] <= i_wb_dat[31:24]; + counter_started <= 1'b1; + end else if(i_wb_adr[3:0] == 4'b1000) begin + // Any write to BASE+8 will ack the IRQ + irq_fired <= 1'b0; + end + end + end end -endmodule \ No newline at end of file +endmodule diff --git a/cores/wb/wb_timer/tb/tb_wb_timer.v b/cores/wb/wb_timer/tb/tb_wb_timer.v new file mode 100644 index 0000000..0c38307 --- /dev/null +++ b/cores/wb/wb_timer/tb/tb_wb_timer.v @@ -0,0 +1,143 @@ +`timescale 1ns/1ps + +module tb_wb_timer; + localparam ADDR_COUNTER = 32'h0000_0000; + localparam ADDR_PRELOAD = 32'h0000_0004; + localparam ADDR_ACK = 32'h0000_0008; + + reg i_clk; + reg i_rst; + reg [31:0] i_wb_adr; + reg [31:0] i_wb_dat; + reg [3:0] i_wb_sel; + reg i_wb_we; + reg i_wb_stb; + reg i_wb_cyc; + wire [31:0] o_wb_dat; + wire o_wb_ack; + wire o_irq; + + reg [31:0] read_data; + integer cycle; + + wb_countdown_timer dut ( + .i_clk(i_clk), + .i_rst(i_rst), + .o_irq(o_irq), + .i_wb_adr(i_wb_adr), + .i_wb_dat(i_wb_dat), + .o_wb_dat(o_wb_dat), + .i_wb_sel(i_wb_sel), + .i_wb_we(i_wb_we), + .i_wb_cyc(i_wb_cyc), + .i_wb_stb(i_wb_stb), + .o_wb_ack(o_wb_ack) + ); + + initial i_clk = 1'b0; + always #5 i_clk = ~i_clk; + + task automatic wb_write; + input [31:0] addr; + input [31:0] data; + input [3:0] sel; + begin + @(negedge i_clk); + i_wb_adr <= addr; + i_wb_dat <= data; + i_wb_sel <= sel; + i_wb_we <= 1'b1; + i_wb_stb <= 1'b1; + i_wb_cyc <= 1'b1; + + while (!o_wb_ack) + @(posedge i_clk); + + @(negedge i_clk); + i_wb_we <= 1'b0; + i_wb_stb <= 1'b0; + i_wb_cyc <= 1'b0; + i_wb_sel <= 4'b0000; + i_wb_dat <= 32'h0000_0000; + end + endtask + + task automatic wb_read; + input [31:0] addr; + output [31:0] data; + begin + @(negedge i_clk); + i_wb_adr <= addr; + i_wb_dat <= 32'h0000_0000; + i_wb_sel <= 4'b1111; + i_wb_we <= 1'b0; + i_wb_stb <= 1'b1; + i_wb_cyc <= 1'b1; + + while (!o_wb_ack) + @(posedge i_clk); + + #1; + data = o_wb_dat; + + @(negedge i_clk); + i_wb_stb <= 1'b0; + i_wb_cyc <= 1'b0; + i_wb_sel <= 4'b0000; + end + endtask + + initial begin + $dumpfile("wb_timer.vcd"); + $dumpvars(0, tb_wb_timer); + + i_rst = 1'b1; + i_wb_adr = 32'h0000_0000; + i_wb_dat = 32'h0000_0000; + i_wb_sel = 4'b0000; + i_wb_we = 1'b0; + i_wb_stb = 1'b0; + i_wb_cyc = 1'b0; + + repeat (2) @(posedge i_clk); + i_rst = 1'b0; + + wb_write(ADDR_COUNTER, 5, 4'b1111); + wb_write(ADDR_PRELOAD, 0, 4'b1111); + + for (cycle = 0; cycle < 40; cycle = cycle + 1) begin + @(posedge i_clk); + if(o_irq) + wb_write(ADDR_ACK, 32'h0000_ffff, 4'b1111); + end + + for (cycle = 0; cycle < 8; cycle = cycle + 1) + @(posedge i_clk); + + wb_write(ADDR_PRELOAD, 8, 4'b1111); + + for (cycle = 0; cycle < 21; cycle = cycle + 1) begin + @(posedge i_clk); + if(o_irq) + wb_write(ADDR_ACK, 32'h0000_ffff, 4'b1111); + end + + wb_write(ADDR_PRELOAD, 6, 4'b1111); + + for (cycle = 0; cycle < 21; cycle = cycle + 1) begin + @(posedge i_clk); + if(o_irq) + wb_write(ADDR_ACK, 32'h0000_ffff, 4'b1111); + end + + wb_write(ADDR_PRELOAD, 0, 4'b1111); + + for (cycle = 0; cycle < 10; cycle = cycle + 1) begin + @(posedge i_clk); + if(o_irq) + wb_write(ADDR_ACK, 32'h0000_ffff, 4'b1111); + end + + $finish; + end +endmodule diff --git a/cores/wb/wb_timer/wb_timer.core b/cores/wb/wb_timer/wb_timer.core index 47503f9..91a294b 100644 --- a/cores/wb/wb_timer/wb_timer.core +++ b/cores/wb/wb_timer/wb_timer.core @@ -8,6 +8,10 @@ filesets: files: - rtl/wb_timer.v file_type: verilogSource + tb: + files: + - tb/tb_wb_timer.v + file_type: verilogSource formal_rtl: depend: - joppeb:wb:formal_checker @@ -25,8 +29,13 @@ targets: - rtl toplevel: wb_countdown_timer parameters: - - WIDTH - - DIVIDER + - address + sim: + default_tool: icarus + filesets: + - rtl + - tb + toplevel: tb_wb_timer formal: default_tool: symbiyosys filesets: @@ -35,15 +44,10 @@ targets: - formal_cfg toplevel: formal_wb_timer parameters: - - WIDTH - - DIVIDER + - address parameters: - WIDTH: + address: datatype: int - description: Counter width in bits - paramtype: vlogparam - DIVIDER: - datatype: int - description: Prescaler divider as a power of two exponent + description: Base address of register set paramtype: vlogparam diff --git a/fusesoc_libraries/serv b/fusesoc_libraries/serv index 4999793..74a7f73 160000 --- a/fusesoc_libraries/serv +++ b/fusesoc_libraries/serv @@ -1 +1 @@ -Subproject commit 4999793a48485e2104155048859dc8506b719a50 +Subproject commit 74a7f73d3198f17bebf5754cb94e72dc30b0103e diff --git a/xilinx_fusesoc.sh b/xilinx_fusesoc.sh new file mode 100755 index 0000000..0e9bfd4 --- /dev/null +++ b/xilinx_fusesoc.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +set -e + +. /opt/Xilinx/14.7/ISE_DS/settings64.sh /opt/Xilinx/14.7/ISE_DS + +echo fusesoc "$@" +exec fusesoc "$@"