diff --git a/Makefile b/Makefile index 2bca3a8..ecf7648 100644 --- a/Makefile +++ b/Makefile @@ -63,7 +63,6 @@ $(ICESTICK_EXAMPLES): # Formal Verification formal: - sby -f test/formal_verification/uart_rx.sby sby -f test/formal_verification/bridge_rx.sby # Functional Simulation diff --git a/test/formal_verification/uart_rx.sby b/test/formal_verification/uart_rx.sby deleted file mode 100644 index 6b05f3c..0000000 --- a/test/formal_verification/uart_rx.sby +++ /dev/null @@ -1,29 +0,0 @@ -[tasks] -basic bmc -nofullskip prove -cover -noverific cover -basic cover : default - -[options] -cover: -mode cover --- -prove: -mode prove --- -bmc: -mode bmc --- - -[engines] -smtbmc boolector - -[script] -nofullskip: read -define NO_FULL_SKIP=1 -noverific: read -noverific -read -formal uart_rx.v -prep -top uart_rx - -[files] -src/manta/uart_iface/uart_rx.v \ No newline at end of file