From 1deb6e9789e2da7e414ad72e514cda475a9a2c89 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Fri, 28 Dec 2018 13:57:23 +0100 Subject: [PATCH] Add vai_reg to README; using SVA default clocking --- README.md | 6 ++++- vai_reg/properties.sv | 56 +++++++++++++++++++++++-------------------- 2 files changed, 35 insertions(+), 27 deletions(-) diff --git a/README.md b/README.md index 0d69da4..8456a0b 100644 --- a/README.md +++ b/README.md @@ -1,10 +1,11 @@ The original repository is located on my own git-server at [https://git.goodcleanfun.de/tmeissner/formal_verification](https://git.goodcleanfun.de/tmeissner/formal_verification) + It is mirrored to github with every push, so both should be in sync. # formal_verification -Tests and examples of using formal verification to check correctness of digital hardware designs. All tests are done with SymbiYosys, a front-end for formal verification flows based on [Yosys](https://github.com/YosysHQ). Some examples use the VHDL/SystemVerilog parser plugin by Verific which isn't free SW and not included in the free Yosys version. See on the [Symbiotic EDA website](https://www.symbioticeda.com) for more information. +Tests and examples of using formal verification to check correctness of digital hardware designs. All tests are done with SymbiYosys, a front-end for formal verification flows based on [Yosys](https://github.com/YosysHQ). Some examples use the VHDL/SystemVerilog parser plugin by Verific which isn't free SW and not included in the free Yosys version. See on the [Symbiotic EDA website](https://www.symbioticeda.com) for more information. ### alu A simple ALU design in VHDL, together with a formal testbench written in SystemVerilog. The testbench contains various simple SVA properties used by assert & cover directives which are proved with the SymbiYosys tool. @@ -15,3 +16,6 @@ A simple counter design in VHDL, together with a formal testbench written in Sys ### dlatch A simple test design which generates the `Unsupported cell type $dlatchsr` error using with Verific plugin. + +### vai_reg +A simple register file with VAI (valid-accept-interface) which serves as test design to try formal verification of FSMs. \ No newline at end of file diff --git a/vai_reg/properties.sv b/vai_reg/properties.sv index 822c78e..79d610f 100644 --- a/vai_reg/properties.sv +++ b/vai_reg/properties.sv @@ -33,20 +33,24 @@ module properties ( always @(posedge Clk_i) init_state = 0; + default clocking + @(posedge Clk_i); + endclocking + // Constraints - assume property (@(posedge Clk_i) + assume property ( DinValid_i && !DinAccept_o |=> $stable(Din_i) ); - assume property (@(posedge Clk_i) + assume property ( DinValid_i && !DinAccept_o |=> $stable(DinStart_i) ); - assume property (@(posedge Clk_i) + assume property ( DinValid_i && !DinAccept_o |=> $stable(DinStop_i) ); @@ -54,31 +58,31 @@ module properties ( // Asserts - assert property (@(posedge Clk_i) + assert property ( s_fsm_state >= 0 && s_fsm_state <= 6 ); - assert property (@(posedge Clk_i) + assert property ( DoutStart_o |-> DoutValid_o ); - assert property (@(posedge Clk_i) + assert property ( DoutStart_o && DoutAccept_i |=> !DoutStart_o ); - assert property (@(posedge Clk_i) + assert property ( DoutStop_o |-> DoutValid_o ); - assert property (@(posedge Clk_i) + assert property ( DoutStop_o && DoutAccept_i |=> !DoutStop_o ); - assert property (@(posedge Clk_i) + assert property ( s_fsm_state == 1 && DinValid_i && DinStart_i && DinAccept_o |=> s_header == $past(Din_i) ); @@ -86,77 +90,77 @@ module properties ( // State changes - assert property (@(posedge Clk_i) disable iff (!Reset_n_i) + assert property (disable iff (!Reset_n_i) s_fsm_state == 0 |=> s_fsm_state == 1 ); - assert property (@(posedge Clk_i) disable iff (!Reset_n_i) + assert property (disable iff (!Reset_n_i) s_fsm_state == 1 && DinValid_i && DinStart_i && DinStop_i && Din_i[3:0] == `READ |=> s_fsm_state == 2 ); - assert property (@(posedge Clk_i) disable iff (!Reset_n_i) + assert property (disable iff (!Reset_n_i) s_fsm_state == 1 && DinValid_i && DinStart_i && !DinStop_i && Din_i[3:0] == `WRITE |=> s_fsm_state == 3 ); - assert property (@(posedge Clk_i) disable iff (!Reset_n_i) + assert property (disable iff (!Reset_n_i) s_fsm_state == 2 |=> s_fsm_state == 4 ); - assert property (@(posedge Clk_i) disable iff (!Reset_n_i) + assert property (disable iff (!Reset_n_i) s_fsm_state == 4 && DoutValid_o && DoutAccept_i && s_header[3:0] == `READ |=> s_fsm_state == 5 ); - assert property (@(posedge Clk_i) disable iff (!Reset_n_i) + assert property (disable iff (!Reset_n_i) s_fsm_state == 4 && DoutValid_o && DoutAccept_i && s_header[3:0] != `READ |=> s_fsm_state == 6 ); - assert property (@(posedge Clk_i) disable iff (!Reset_n_i) + assert property (disable iff (!Reset_n_i) s_fsm_state == 6 && DoutValid_o && DoutAccept_i |=> s_fsm_state == 0 ); // Protocol checks - assert property (@(posedge Clk_i) + assert property ( s_fsm_state > 1 |-> - s_header[3:0] == `READ || s_header[3:0] == `WRITE + s_header[3:0] inside {`READ, `WRITE} ); - assert property (@(posedge Clk_i) + assert property ( DoutStart_o && DoutValid_o |-> Dout_o[3:0] == s_header[3:0] ); - assert property (@(posedge Clk_i) + assert property ( DoutValid_o && !DoutAccept_i |=> $stable(Dout_o) ); - assert property (@(posedge Clk_i) + assert property ( DoutValid_o && !DoutAccept_i |=> $stable(DoutStart_o) ); - assert property (@(posedge Clk_i) + assert property ( DoutValid_o && !DoutAccept_i |=> $stable(DoutStop_o) ); - assert property (@(posedge Clk_i) + assert property ( DoutValid_o |-> !(DoutStart_o && DoutStop_o) ); - assert property (@(posedge Clk_i) + assert property ( DoutStart_o |-> s_fsm_state == 4 ); - assert property (@(posedge Clk_i) + assert property ( DoutStop_o |-> s_fsm_state == 6 ); - assert property (@(posedge Clk_i) + assert property ( DoutValid_o |-> s_fsm_state >= 4 && s_fsm_state <= 6 );