luke
/
manta
mirror of https://github.com/fischermoseley/manta.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

add bridge_rx formal to makefile

This commit is contained in:
Fischer Moseley 2023-07-17 07:41:29 -07:00
parent adf355c633
commit 2b483b1beb
2 changed files with 16 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Makefile
View File

@ -95,6 +95,7 @@ lut_mem_tb:
# Formal Verification
formal:
sby -f test/formal_verification/uart_rx.sby
sby -f test/formal_verification/bridge_rx.sby
# Build Examples
nexys_a7: nexys_a7_video_sprite_uart nexys_a7_io_core nexys_a7_ps2_logic_analyzer nexys_a7_lut_mem

41
src/manta/uart_iface/bridge_rx.v
View File

@ -121,38 +121,27 @@ module bridge_rx (
`ifdef FORMAL
always @(posedge clk) begin
// covers
// find_any_write_transaction: cover(rw_o == 1);
// find_any_read_transaction: cover(rw_o == 0);
find_any_write_transaction: cover(rw_o == 1);
find_any_read_transaction: cover(rw_o == 0);
// find_specific_write_transaction:
// cover(data_o == 16'h1234 && addr_o == 16'h5678 && rw_o == 1 && valid_o == 1);
find_specific_write_transaction:
cover(data_o == 16'h1234 && addr_o == 16'h5678 && rw_o == 1 && valid_o == 1);
// find_specific_read_transaction:
// cover(addr_o == 16'h1234 && rw_o == 0 && valid_o == 1);
find_specific_read_transaction:
cover(addr_o == 16'h1234 && rw_o == 0 && valid_o == 1);
// find_spacey_write_transaction:
// cover((rw_o == 1) && ($past(valid_i, 3) == 0));
// // asserts
// no_back_to_back_transactions:
// assert( ~(valid_o && $past(valid_o)) );
// no_invalid_states:
// assert(state == IDLE || state == READ || state == WRITE);
// byte_counter_only_increases:
// assert(byte_num == $past(byte_num) || byte_num == $past(byte_num) + 1 || byte_num == 0);
// only_r_triggers_reads:
// assert property ( (state == READ) |=> ($past(valid_i) ) );
// state transitions
enter_read:
assert( ($past(state) == IDLE && state == READ) )
find_spacey_write_transaction:
cover((rw_o == 1) && ($past(valid_i, 3) == 0));
// asserts
no_back_to_back_transactions:
assert( ~(valid_o && $past(valid_o)) );
no_invalid_states:
assert(state == IDLE || state == READ || state == WRITE);
byte_counter_only_increases:
assert(byte_num == $past(byte_num) || byte_num == $past(byte_num) + 1 || byte_num == 0);
end
`endif // FORMAL
endmodule