diff options
| author | Miodrag Milanovic <mmicko@gmail.com> | 2023-02-23 14:58:02 +0100 |
|---|---|---|
| committer | Miodrag Milanovic <mmicko@gmail.com> | 2023-02-27 09:24:04 +0100 |
| commit | 53a4f0fb56f298880c9b91dfa8c2e69a383cd5bc (patch) | |
| tree | 44ee5c89586f8f6e0c9a4a6a8bb6af913ac2fd5f /tests/verific | |
| parent | a30894e5facf9d0f3e814a4c00e376000d3eed6c (diff) | |
| download | yosys-53a4f0fb56f298880c9b91dfa8c2e69a383cd5bc.tar.gz yosys-53a4f0fb56f298880c9b91dfa8c2e69a383cd5bc.tar.bz2 yosys-53a4f0fb56f298880c9b91dfa8c2e69a383cd5bc.zip | |
Add test example
Diffstat (limited to 'tests/verific')
| -rw-r--r-- | tests/verific/.gitignore | 3 | ||||
| -rw-r--r-- | tests/verific/case.sv | 28 | ||||
| -rw-r--r-- | tests/verific/case.ys | 16 | ||||
| -rwxr-xr-x | tests/verific/run-test.sh | 4 |
4 files changed, 51 insertions, 0 deletions
diff --git a/tests/verific/.gitignore b/tests/verific/.gitignore new file mode 100644 index 000000000..b48f808a1 --- /dev/null +++ b/tests/verific/.gitignore @@ -0,0 +1,3 @@ +/*.log +/*.out +/run-test.mk diff --git a/tests/verific/case.sv b/tests/verific/case.sv new file mode 100644 index 000000000..ed8529b91 --- /dev/null +++ b/tests/verific/case.sv @@ -0,0 +1,28 @@ +module top ( + input clk, + input [5:0] currentstate, + output reg [1:0] o + ); + always @ (posedge clk) + begin + case (currentstate) + 5'd1,5'd2, 5'd3: + begin + o <= 2'b01; + end + 5'd4: + begin + o <= 2'b10; + end + 5'd5,5'd6,5'd7: + begin + o <= 2'b11; + end + default : + begin + o <= 2'b00; + end + endcase + end +endmodule + diff --git a/tests/verific/case.ys b/tests/verific/case.ys new file mode 100644 index 000000000..a181b39cf --- /dev/null +++ b/tests/verific/case.ys @@ -0,0 +1,16 @@ +verific -cfg db_abstract_case_statement_synthesis 0 +read -sv case.sv +verific -import top +prep +rename top gold + +verific -cfg db_abstract_case_statement_synthesis 1 +read -sv case.sv +verific -import top +prep +rename top gate + +miter -equiv -flatten -make_assert gold gate miter +prep -top miter +clk2fflogic +sat -set-init-zero -tempinduct -prove-asserts -verify diff --git a/tests/verific/run-test.sh b/tests/verific/run-test.sh new file mode 100755 index 000000000..2f91cf0fd --- /dev/null +++ b/tests/verific/run-test.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash +set -eu +source ../gen-tests-makefile.sh +run_tests --yosys-scripts --bash |