diff options
author | Clifford Wolf <clifford@clifford.at> | 2015-08-15 11:28:35 +0200 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2015-08-15 11:28:35 +0200 |
commit | f227332a9890f44ec9db5c60578f4d38d6ec2d80 (patch) | |
tree | fa87d355c6d2167df7404081f9af12716e645949 /scripts/smt2-bmc/main.v | |
parent | ec0891326aee1334bce4bb096e7521a3907d4bdc (diff) | |
download | picorv32-f227332a9890f44ec9db5c60578f4d38d6ec2d80.tar.gz picorv32-f227332a9890f44ec9db5c60578f4d38d6ec2d80.zip |
Added scripts/smt2-bmc/sync.*
Diffstat (limited to 'scripts/smt2-bmc/main.v')
-rw-r--r-- | scripts/smt2-bmc/main.v | 64 |
1 files changed, 64 insertions, 0 deletions
diff --git a/scripts/smt2-bmc/main.v b/scripts/smt2-bmc/main.v new file mode 100644 index 0000000..db854bc --- /dev/null +++ b/scripts/smt2-bmc/main.v @@ -0,0 +1,64 @@ +`timescale 1 ns / 1 ps + +module main (input clk, resetn, domem, output trap); + parameter integer MEMORY_WORDS = 2**30; + + // timing parameters (vary for async test) + parameter [0:0] ENABLE_REGS_DUALPORT = 1; + parameter [0:0] TWO_STAGE_SHIFT = 1; + parameter [0:0] TWO_CYCLE_COMPARE = 0; + parameter [0:0] TWO_CYCLE_ALU = 0; + + // isa parameters (vary for sync test) + parameter [0:0] ENABLE_COUNTERS = 0; + parameter [0:0] CATCH_MISALIGN = 1; + parameter [0:0] CATCH_ILLINSN = 1; + parameter [0:0] ENABLE_MUL = 0; + parameter [0:0] ENABLE_IRQ = 0; + + (* keep *) wire mem_valid; + (* keep *) wire mem_ready; + (* keep *) wire [31:0] mem_addr; + (* keep *) wire [31:0] mem_wdata; + (* keep *) wire [ 3:0] mem_wstrb; + (* keep *) wire [31:0] mem_rdata; + + picorv32 #( + // timing parameters + .ENABLE_REGS_DUALPORT(ENABLE_REGS_DUALPORT), + .TWO_STAGE_SHIFT (TWO_STAGE_SHIFT ), + .TWO_CYCLE_COMPARE (TWO_CYCLE_COMPARE ), + .TWO_CYCLE_ALU (TWO_CYCLE_ALU ), + + // isa parameters + .ENABLE_COUNTERS(ENABLE_COUNTERS), + .CATCH_MISALIGN (CATCH_MISALIGN ), + .CATCH_ILLINSN (CATCH_ILLINSN ), + .ENABLE_MUL (ENABLE_MUL ), + .ENABLE_IRQ (ENABLE_IRQ ) + ) cpu ( + .clk (clk ), + .resetn (resetn ), + .trap (trap ), + .mem_valid(mem_valid), + .mem_ready(mem_ready), + .mem_addr (mem_addr ), + .mem_wdata(mem_wdata), + .mem_wstrb(mem_wstrb), + .mem_rdata(mem_rdata) + ); + + reg [31:0] memory [0:MEMORY_WORDS-1]; + + assign mem_ready = domem && resetn && mem_valid; + assign mem_rdata = memory[mem_addr >> 2]; + + always @(posedge clk) begin + if (mem_ready && mem_valid) begin + if (mem_wstrb[0]) memory[mem_addr >> 2][ 7: 0] <= mem_wdata[ 7: 0]; + if (mem_wstrb[1]) memory[mem_addr >> 2][15: 8] <= mem_wdata[15: 8]; + if (mem_wstrb[2]) memory[mem_addr >> 2][23:16] <= mem_wdata[23:16]; + if (mem_wstrb[3]) memory[mem_addr >> 2][31:24] <= mem_wdata[31:24]; + end + end +endmodule |