| Line 52... |
Line 52... |
// Modes
|
// Modes
|
`define QSPI_MOD_SPI 2'b00
|
`define QSPI_MOD_SPI 2'b00
|
`define QSPI_MOD_QOUT 2'b10
|
`define QSPI_MOD_QOUT 2'b10
|
`define QSPI_MOD_QIN 2'b11
|
`define QSPI_MOD_QIN 2'b11
|
|
|
|
// Which level of formal proofs will we be doing? As a component, or a
|
|
// top-level?
|
|
`ifdef LLQSPI_TOP
|
|
`define ASSUME assume
|
|
`else
|
|
`define ASSUME assert
|
|
`endif
|
|
//
|
module llqspi(i_clk,
|
module llqspi(i_clk,
|
// Module interface
|
// Module interface
|
i_wr, i_hold, i_word, i_len, i_spd, i_dir,
|
i_wr, i_hold, i_word, i_len, i_spd, i_dir,
|
o_word, o_valid, o_busy,
|
o_word, o_valid, o_busy,
|
// QSPI interface
|
// QSPI interface
|
| Line 76... |
Line 84... |
// Interface with the QSPI lines
|
// Interface with the QSPI lines
|
output reg o_sck;
|
output reg o_sck;
|
output reg o_cs_n;
|
output reg o_cs_n;
|
output reg [1:0] o_mod;
|
output reg [1:0] o_mod;
|
output reg [3:0] o_dat;
|
output reg [3:0] o_dat;
|
input [3:0] i_dat;
|
input wire [3:0] i_dat;
|
|
|
// output wire [22:0] o_dbg;
|
// output wire [22:0] o_dbg;
|
// assign o_dbg = { state, spi_len,
|
// assign o_dbg = { state, spi_len,
|
// o_busy, o_valid, o_cs_n, o_sck, o_mod, o_dat, i_dat };
|
// o_busy, o_valid, o_cs_n, o_sck, o_mod, o_dat, i_dat };
|
|
|
| Line 192... |
Line 200... |
initial o_dat = 4'hd;
|
initial o_dat = 4'hd;
|
initial o_valid = 1'b0;
|
initial o_valid = 1'b0;
|
initial o_busy = 1'b0;
|
initial o_busy = 1'b0;
|
initial r_input = 31'h000;
|
initial r_input = 31'h000;
|
initial o_mod = `QSPI_MOD_SPI;
|
initial o_mod = `QSPI_MOD_SPI;
|
|
initial o_word = 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((state == `QSPI_IDLE)&&(o_sck))
|
if ((state == `QSPI_IDLE)&&(o_sck))
|
begin
|
begin
|
o_cs_n <= 1'b1;
|
o_cs_n <= 1'b1;
|
o_valid <= 1'b0;
|
o_valid <= 1'b0;
|
o_busy <= 1'b0;
|
o_busy <= 1'b0;
|
o_mod <= `QSPI_MOD_SPI;
|
o_mod <= `QSPI_MOD_SPI;
|
r_word <= i_word;
|
r_word <= i_word;
|
r_spd <= i_spd;
|
r_spd <= i_spd;
|
r_dir <= i_dir;
|
r_dir <= i_dir;
|
if (i_wr)
|
if ((i_wr)&&(!o_busy))
|
begin
|
begin
|
state <= `QSPI_START;
|
state <= `QSPI_START;
|
spi_len<= { 1'b0, i_len, 3'b000 } + 6'h8;
|
spi_len<= { 1'b0, i_len, 3'b000 } + 6'h8;
|
o_cs_n <= 1'b0;
|
o_cs_n <= 1'b0;
|
// o_sck <= 1'b1;
|
// o_sck <= 1'b1;
|
| Line 230... |
Line 239... |
o_valid <= 1'b0;
|
o_valid <= 1'b0;
|
if (r_spd)
|
if (r_spd)
|
o_dat <= r_word[31:28];
|
o_dat <= r_word[31:28];
|
else
|
else
|
o_dat <= { 3'b110, r_word[31] };
|
o_dat <= { 3'b110, r_word[31] };
|
end else if (~o_sck)
|
end else if (!o_sck)
|
begin
|
begin
|
o_sck <= 1'b1;
|
o_sck <= 1'b1;
|
o_busy <= ((state != `QSPI_READY)||(~i_wr));
|
o_busy <= ((state != `QSPI_READY)||(!i_wr));
|
o_valid <= 1'b0;
|
o_valid <= 1'b0;
|
end else if (state == `QSPI_BITS)
|
end else if (state == `QSPI_BITS)
|
begin
|
begin
|
// Should enter into here with at least a spi_len
|
// Should enter into here with at least a spi_len
|
// of one, perhaps more
|
// of one, perhaps more
|
| Line 257... |
Line 266... |
if (spi_len == 6'h1)
|
if (spi_len == 6'h1)
|
state <= `QSPI_READY;
|
state <= `QSPI_READY;
|
end
|
end
|
|
|
o_valid <= 1'b0;
|
o_valid <= 1'b0;
|
if (~o_mod[1])
|
if (!o_mod[1])
|
r_input <= { r_input[29:0], i_miso };
|
r_input <= { r_input[29:0], i_miso };
|
else if (o_mod[1])
|
else if (o_mod[1])
|
r_input <= { r_input[26:0], i_dat };
|
r_input <= { r_input[26:0], i_dat };
|
end else if (state == `QSPI_READY)
|
end else if (state == `QSPI_READY)
|
begin
|
begin
|
| Line 281... |
Line 290... |
spi_len<= { 1'b0, i_len, 3'b000 } + 6'h8 - 6'h4;
|
spi_len<= { 1'b0, i_len, 3'b000 } + 6'h8 - 6'h4;
|
end else begin
|
end else begin
|
r_word <= { i_word[30:0], 1'b0 };
|
r_word <= { i_word[30:0], 1'b0 };
|
spi_len<= { 1'b0, i_len, 3'b000 } + 6'h8 - 6'h1;
|
spi_len<= { 1'b0, i_len, 3'b000 } + 6'h8 - 6'h1;
|
end
|
end
|
if((~o_busy)&&(i_wr))// Acknowledge a new request
|
if((!o_busy)&&(i_wr))// Acknowledge a new request
|
begin
|
begin
|
state <= `QSPI_BITS;
|
state <= `QSPI_BITS;
|
o_busy <= 1'b1;
|
o_busy <= 1'b1;
|
o_sck <= 1'b0;
|
o_sck <= 1'b0;
|
|
|
| Line 298... |
Line 307... |
o_dat <= { 3'b110, i_word[31] };
|
o_dat <= { 3'b110, i_word[31] };
|
|
|
end else begin
|
end else begin
|
o_sck <= 1'b1;
|
o_sck <= 1'b1;
|
state <= (i_hold)?`QSPI_HOLDING : `QSPI_STOP;
|
state <= (i_hold)?`QSPI_HOLDING : `QSPI_STOP;
|
o_busy <= (~i_hold);
|
o_busy <= (!i_hold);
|
end
|
end
|
|
|
// Read a bit upon any transition
|
// Read a bit upon any transition
|
o_valid <= 1'b1;
|
o_valid <= 1'b1;
|
if (~o_mod[1])
|
if (!o_mod[1])
|
begin
|
begin
|
r_input <= { r_input[29:0], i_miso };
|
r_input <= { r_input[29:0], i_miso };
|
o_word <= { r_input[30:0], i_miso };
|
o_word <= { r_input[30:0], i_miso };
|
end else if (o_mod[1])
|
end else if (o_mod[1])
|
begin
|
begin
|
| Line 325... |
Line 334... |
// commends in wbqspiflash for more details.
|
// commends in wbqspiflash for more details.
|
//
|
//
|
o_valid <= 1'b0;
|
o_valid <= 1'b0;
|
o_cs_n <= 1'b0;
|
o_cs_n <= 1'b0;
|
o_busy <= 1'b0;
|
o_busy <= 1'b0;
|
if((~o_busy)&&(i_wr))// Acknowledge a new request
|
r_spd <= i_spd;
|
|
r_dir <= i_dir;
|
|
if (i_spd)
|
|
begin
|
|
r_word <= { i_word[27:0], 4'h0 };
|
|
spi_len<= { 1'b0, i_len, 3'b100 };
|
|
end else begin
|
|
r_word <= { i_word[30:0], 1'b0 };
|
|
spi_len<= { 1'b0, i_len, 3'b111 };
|
|
end
|
|
if((!o_busy)&&(i_wr))// Acknowledge a new request
|
begin
|
begin
|
state <= `QSPI_BITS;
|
state <= `QSPI_BITS;
|
o_busy <= 1'b1;
|
o_busy <= 1'b1;
|
o_sck <= 1'b0;
|
o_sck <= 1'b0;
|
|
|
// Read the new request off the bus
|
// Read the new request off the bus
|
r_spd <= i_spd;
|
|
r_dir <= i_dir;
|
|
// Set up the first bits on the bus
|
// Set up the first bits on the bus
|
o_mod<=(i_spd)?{ 1'b1, i_dir } : `QSPI_MOD_SPI;
|
o_mod<=(i_spd)?{ 1'b1, i_dir } : `QSPI_MOD_SPI;
|
if (i_spd)
|
if (i_spd)
|
begin
|
|
o_dat <= i_word[31:28];
|
o_dat <= i_word[31:28];
|
r_word <= { i_word[27:0], 4'h0 };
|
else
|
spi_len<= { 1'b0, i_len, 3'b100 };
|
|
end else begin
|
|
o_dat <= { 3'b110, i_word[31] };
|
o_dat <= { 3'b110, i_word[31] };
|
r_word <= { i_word[30:0], 1'b0 };
|
|
spi_len<= { 1'b0, i_len, 3'b111 };
|
|
end
|
|
end else begin
|
end else begin
|
o_sck <= 1'b1;
|
o_sck <= 1'b1;
|
state <= (i_hold)?`QSPI_HOLDING : `QSPI_STOP;
|
state <= (i_hold)?`QSPI_HOLDING : `QSPI_STOP;
|
o_busy <= (~i_hold);
|
o_busy <= (!i_hold);
|
end
|
end
|
end else if (state == `QSPI_STOP)
|
end else if (state == `QSPI_STOP)
|
begin
|
begin
|
o_sck <= 1'b1; // Stop the clock
|
o_sck <= 1'b1; // Stop the clock
|
o_valid <= 1'b0; // Output may have just been valid, but no more
|
o_valid <= 1'b0; // Output may have just been valid, but no more
|
| Line 378... |
Line 389... |
o_sck <= 1'b1;
|
o_sck <= 1'b1;
|
o_mod <= `QSPI_MOD_SPI;
|
o_mod <= `QSPI_MOD_SPI;
|
o_dat <= 4'hd;
|
o_dat <= 4'hd;
|
end
|
end
|
|
|
endmodule
|
`ifdef FORMAL
|
|
reg prev_i_clk, past_valid;
|
|
|
|
initial `ASSUME(i_clk == 1'b0);
|
|
initial prev_i_clk = 1;
|
|
always @($global_clock)
|
|
begin
|
|
prev_i_clk <= i_clk;
|
|
`ASSUME(i_clk != prev_i_clk);
|
|
end
|
|
|
|
reg past_valid;
|
|
initial past_valid = 1'b0;
|
|
always @(posedge i_clk)
|
|
past_valid <= 1'b1;
|
|
|
|
/*
|
|
always @(*)
|
|
if (!$stable(i_spd))
|
|
assert($rose(i_clk));
|
|
*/
|
|
|
|
always @(posedge i_clk) begin
|
|
if ((past_valid)&&($past(i_wr))&&($past(o_busy)))
|
|
begin
|
|
// any time i_wr and o_busy are true, nothing changes
|
|
// of spd, len, word or dir
|
|
`ASSUME(i_wr);
|
|
`ASSUME(i_spd == $past(i_spd));
|
|
`ASSUME(i_len == $past(i_len));
|
|
`ASSUME(i_word == $past(i_word));
|
|
`ASSUME(i_dir == $past(i_dir));
|
|
`ASSUME(i_hold == $past(i_hold));
|
|
end
|
|
if ((past_valid)&&($past(i_wr))&&($past(o_busy))&&($past(state == `QSPI_IDLE)))
|
|
assert($past(state)==state);
|
|
if (i_hold == $past(i_hold))
|
|
assert($stable(i_hold));
|
|
end
|
|
|
|
always @(*) begin
|
|
if (o_mod == `QSPI_MOD_QOUT)
|
|
`ASSUME(i_dat == o_dat);
|
|
if (o_mod == `QSPI_MOD_SPI)
|
|
`ASSUME(i_dat[3:2] == 2'b11);
|
|
if (o_mod == `QSPI_MOD_SPI)
|
|
`ASSUME(i_dat[0] == o_dat[0]);
|
|
end
|
|
|
|
initial `ASSUME(i_wr == 1'b0);
|
|
initial `ASSUME(i_word == 0);
|
|
|
|
always @($global_clock)
|
|
if (!$rose(i_clk))
|
|
begin
|
|
`ASSUME($stable(i_wr));
|
|
//
|
|
`ASSUME($stable(i_len));
|
|
`ASSUME($stable(i_dir));
|
|
`ASSUME($stable(i_spd));
|
|
`ASSUME($stable(i_word));
|
|
//
|
|
`ASSUME($stable(i_hold));
|
|
end
|
|
|
|
always @($global_clock)
|
|
if (!$fell(o_sck))
|
|
assume($stable(i_dat));
|
|
|
|
// This is ... not as believable. There might be a delay here.
|
|
// For now, we'll just assume (not necessarily true) that the
|
|
// output
|
|
always @(posedge i_clk)
|
|
if (past_valid)
|
|
`ASSUME( (i_dat == $past(i_dat)) || (o_sck != $past(o_sck)) );
|
|
|
|
reg f_last_sck;
|
|
always @(posedge i_clk)
|
|
f_last_sck <= o_sck;
|
|
|
|
reg [31:0] f_shiftreg, f_goal;
|
|
initial f_shiftreg = 0;
|
|
initial f_goal = 0;
|
|
always @(posedge i_clk)
|
|
if ((o_sck)&&(!f_last_sck))
|
|
begin
|
|
if (o_mod == `QSPI_MOD_QOUT)
|
|
f_shiftreg <= { f_shiftreg[28:0], o_dat };
|
|
else if (o_mod == `QSPI_MOD_SPI)
|
|
f_shiftreg <= { f_shiftreg[30:0], o_dat[0] };
|
|
end
|
|
|
|
reg [5:0] f_nsent, f_vsent;
|
|
reg [2:0] f_nbits_r;
|
|
wire [5:0] f_nbits;
|
|
always @(posedge i_clk)
|
|
if ((i_wr)&&(!o_busy))
|
|
begin
|
|
f_goal <= i_word;
|
|
f_nbits_r <= { 1'b0, i_len } + 3'h1;
|
|
end
|
|
assign f_nbits = { f_nbits_r, 3'b000 };
|
|
always @(posedge i_clk)
|
|
if ((!o_sck)||(!o_cs_n))
|
|
assert(f_nbits != 0);
|
|
|
|
always @(posedge i_clk)
|
|
if (o_cs_n)
|
|
f_nsent <= 0;
|
|
else if ((!o_busy)&&(i_wr))
|
|
f_nsent <= 0;
|
|
else if ((!f_last_sck)&&(o_sck))
|
|
begin
|
|
if (o_mod == `QSPI_MOD_SPI)
|
|
f_nsent <= f_nsent + 6'h1;
|
|
else
|
|
f_nsent <= f_nsent + 6'h4;
|
|
end
|
|
always @(posedge i_clk)
|
|
if (o_cs_n)
|
|
f_vsent <= 0;
|
|
else
|
|
f_vsent <= f_nsent;
|
|
always @(posedge i_clk)
|
|
if ((!o_cs_n)&&(state == `QSPI_BITS)&&(!o_sck))
|
|
begin
|
|
if (o_mod != `QSPI_MOD_SPI)
|
|
assert(f_nsent + spi_len + 6'h4 == f_nbits);
|
|
else
|
|
assert(f_nsent + spi_len + 6'h1 == f_nbits);
|
|
end
|
|
|
|
always @(posedge i_clk)
|
|
assert((o_busy)||(f_goal[(f_nbits-1):0] == f_shiftreg[(f_nbits-1):0]));
|
|
|
|
always @(posedge i_clk) begin
|
|
// We are only ever in one of three speed modes, fourth mode
|
|
// isn't allowed
|
|
assert( (o_mod == `QSPI_MOD_SPI)
|
|
||(o_mod == `QSPI_MOD_QIN)
|
|
||(o_mod == `QSPI_MOD_QOUT));
|
|
|
|
if ((past_valid)&&($past(i_wr))&&(!$past(o_busy)))
|
|
begin
|
|
// Any accepted request leaves us in an active state
|
|
assert(!o_cs_n);
|
|
|
|
// Any accepted request allows us to set our speed
|
|
assert(r_spd == $past(i_spd));
|
|
end
|
|
|
|
// We're either busy, or idle with the clock high
|
|
// or pausing (upon a request) mid-transaction
|
|
assert((o_busy)
|
|
||((state == `QSPI_IDLE)&&(o_sck)&&(o_cs_n))
|
|
||((state == `QSPI_READY)&&(o_sck)&&(!o_cs_n))
|
|
||((state == `QSPI_HOLDING)&&(o_sck)&&(!o_cs_n))
|
|
);
|
|
|
|
// Anytime CS is idle, SCK is high
|
|
if (o_cs_n)
|
|
assert(o_sck);
|
|
|
|
|
|
// What can we assert about i_hold?
|
|
|
|
// When i_hold is asserted before a transaction completes,
|
|
// the transaction will "hold" and wait for a next input.
|
|
// i.e. the clock will stop
|
|
|
|
// First assert that o_busy will be deasserted any time the
|
|
// currently requested word has been sent
|
|
//
|
|
//if ((($past(i_wr))||(i_hold))
|
|
// &&(f_nsent == f_nbits)&&(!o_sck)&&(!o_cs_n))
|
|
// assert(!o_busy);
|
|
|
|
|
|
// First, assert of i_hold that !o_busy will be set.
|
|
if ((past_valid)&&($past(i_hold))&&(f_nsent == f_nbits)&&(!o_cs_n))
|
|
begin
|
|
assert((!o_busy)||(o_sck));
|
|
end
|
|
if ((past_valid)&&($past(i_hold))&&(!$past(i_wr))
|
|
&&(!$past(o_busy))&&(!$past(o_cs_n)))
|
|
begin
|
|
assert(!o_cs_n);
|
|
assert($past(o_sck)==o_sck);
|
|
end
|
|
|
|
// DATA only changes on the falling edge of SCK
|
|
if ((past_valid)&&(o_sck))
|
|
assert(o_dat==$past(o_dat));
|
|
|
|
// Valid is only ever true for one clock
|
|
if ((past_valid)&&(o_valid))
|
|
assert(!$past(o_valid));
|
|
|
|
// Valid is only ever true after receiving a full number of bits
|
|
if ((past_valid)&&(o_valid))
|
|
begin
|
|
if ((!$past(i_wr))||($past(o_busy)))
|
|
assert(f_nsent == f_nbits);
|
|
end
|
|
|
|
// In SPI mode, the top bits of o_dat are always 3'b110
|
|
//
|
|
// This should be true, but there's a problem holding this
|
|
// true
|
|
// assert( (o_mod != `QSPI_MOD_SPI)||(o_dat[3:1] == 3'b110) );
|
|
|
|
// Either valid is true (this clock), or our output word is
|
|
// identical to what it was on the last clock
|
|
if (past_valid)
|
|
assert((o_valid) || (o_word == $past(o_word)));
|
|
end
|
|
`endif
|
|
|
|
endmodule
|
|
|
No newline at end of file
|
No newline at end of file
|
