diff --git a/ckt_examples/simple_examples/validready.fl b/ckt_examples/simple_examples/validready.fl new file mode 100644 index 00000000..64360981 --- /dev/null +++ b/ckt_examples/simple_examples/validready.fl @@ -0,0 +1,135 @@ +// +// The example creates a buffer for a stream of bits that support valid-ready handshaking. +// Currently it doesn't prove anything useful, but what I'd like to prove is: +// `i_sent_data` is the sequence of values of `i_data` where both `i_valid` and `i_ready` are high. +// `o_sent_data` is the sequence of values of `o_data` where both `o_valid` and `o_ready` are high. +// I want to prove that `o_sent_data == i_sent_data + buffered_dat` where buffered_data is a sequence of max length 1. +// +// Hopefully I'll get the hang of VossII enough to be able to prove these properties. +// +// The proof should look something like: +// +// Let S[x], I[x], O[x] be state, inputs and outputs at time x. +// Assume reset[0] = 0 +// Assume reset[x] = 1 for x > 0 +// Define i_sent_data[1] = [] +// Define o_sent_data[1] = [] +// Assert buffered_data[1] = [] (buffered_data[x] is a function of S[x]) +// Define i_sent_data[x] = i_sent_data[x-1] + (if i_valid[x-1]&i_ready[x-1] then [i_data[x-1]] else []) +// Define o_sent_data[x] = o_sent_data[x-1] + (if o_valid[x-1]&o_ready[x-1] then [o_data[x-1]] else []) +// Assert (i_sent_data[x] == o_sent_data[x] + buffered_data[x]) ==> (i_sent_data[x+1] == o_sent_data[x+1] + buffered_data[x+1]) +// +// It feels like what I need to prove with STE is straightforward and only needs to step one cycle. +// 1) Show that one cycle after a reset that buffered_data is []. +// 2) Show that additional_o_data + new_buffered_data = additional_i_data + old_buffered_data +// additional_o_data is a function of the O[x].o_valid O[x].o_data and I[x].o_ready +// additional_i_data is a function of the I[x].i_valid I[x].i_data and O[x].i_ready +// new_buffered_data is a function of S[x+1] and old_buffered_data is a function of S[x]. +// +// What I'm not sure of is: +// 1) How do I actually use the STE to prove the above two points. If a could extract from the fsm functions for +// (I, S) -> O and (I, S) -> S, then I could do this manually as described in the fl tutorial, but presumably there are +// better ways. +// 2) I'm not sure how to prove the recursion in fl, and how I should define the things I want to prove so that I can use them +// when I compose larger circuits whose proofs need these properties. + +// The below expression doesn't work. I think the length of the list can't be variable. +// Maybe I need to use normal booleans for this function. Do they even exist in fl? +// let {buffered_data::bool->bool->bool list} {o_valid::bool} {o_data::bool} = o_valid => [o_data] | [] ; +// let {additional_data::bool->bool->bool->bool list} {valid::bool} {ready::bool} {data::bool} = valid AND ready => [data] | []; + +// I'm not sure how to connect this up to the hardware model that I've made. +// Probably something like this? +// let buffered_data_correct i_valid i_ready i_data o_valid o_ready o_data i_valid_n i_ready_n i_data_n o_valid_n o_ready_n o_data_n = +// ((additional_data o_valid o_ready o_data) @ (buffered_data o_valid_n o_data_n) == (additional_data i_valid i_ready i_data) @ (buffered_data o_valid o_data)); + +load "ste.fl"; + +let valid_ready_buffer = + bit_input clk reset i_valid i_ready i_data. + bit_output o_valid o_ready o_data. + bit_internal en_data. + CELL "valid_ready_buffer" [ + i_ready <- o_ready '|' '~' o_valid, + always_ff (posedge clk) [ + o_valid <== (IF reset THEN '0 ELSE (IF i_ready THEN i_valid ELSE o_valid)), + o_data <== (IF i_ready '&' i_valid THEN i_data ELSE o_data) + ] + ]; +print "valid_ready_buffer is "; +valid_ready_buffer; + +let p = valid_ready_buffer 'clk 'reset 'i_valid 'i_ready 'i_data 'o_valid 'o_ready 'o_data; + +let ckt = pexlif2fsm p; + +let vis = STE_debug ckt; + +// 1) Show that one cycle after a reset that buffered_data is []. + +let ant = + "clk" is_clock (10/2) and + "reset" is "1" in_cycle 0; + +let cons = + "o_valid" is "0" in_cycle 1; + +let ste = STE "-e" vis [] ant cons []; +let ok = get_ste_result ste "strong"; +"Result is:"; +ok; + +// 2) Show that additional_o_data + new_buffered_data = additional_i_data + old_buffered_data +// additional_o_data is a function of the O[x].o_valid O[x].o_data and I[x].o_ready +// additional_i_data is a function of the I[x].i_valid I[x].i_data and O[x].i_ready +// new_buffered_data is a function of S[x+1] and old_buffered_data is a function of S[x]. + +// new i_data cycle 0 +// buffer_data cycle 0 +// new o_data cycle 0 + +let i_valid_1 = variable "i_valid_1"; +let i_valid_2 = variable "i_valid_2"; +let i_ready_1 = variable "i_ready_1"; +let i_ready_2 = variable "i_ready_2"; +let i_data_1 = variable "i_data_1"; +let i_data_2 = variable "i_data_2"; + +let o_valid_1 = variable "o_valid_1"; +let o_valid_2 = variable "o_valid_2"; +let o_ready_1 = variable "o_ready_1"; +let o_ready_2 = variable "o_ready_2"; +let o_data_1 = variable "o_data_1"; +let o_data_2 = variable "o_data_2"; + +let ant = + "clk" is_clock (10/2) and + "reset" is "0" in_cycle 0 and + "i_valid" is i_valid_1 in_cycle 1 and + "i_ready" is i_ready_1 in_cycle 1 and + "i_data" is i_data_1 in_cycle 1 and + "o_valid" is o_valid_1 in_cycle 1 and + "o_ready" is o_ready_1 in_cycle 1 and + "o_data" is o_data_1 in_cycle 1 and + "o_valid" is o_valid_2 in_cycle 2 and + "o_data" is o_data_2 in_cycle 2 + ; + +let cons = []; + +let ste = STE "-e" vis [] ant cons []; +let constraint = get_ste_result ste "strong"; + +// The below doesn't work because of the problem with `bool list`. + +//let additional_i_data = additional_data i_ready_1 i_valid_1 i_data_1; +//let additional_o_data = additional_data o_ready_1 o_valid_1 o_data_1; +// +//let init_buffered_data = buffered_data o_valid_1 o_data_1; +//let final_buffered_data = buffered_data o_valid_2 o_data_2; +// +//let correct = (init_buffered_data @ additional_i_data = additional_o_data @ final_buffered_data); + +"Result is:"; +ok; +//correct;