Solid Oak Technologies logo
Flow Charts to Assertions
Capture Design Intent

The CoverAll™ FC2Assert™ module converts functional flow diagrams into assertions, path covers and FSM sequences. Coverall can provide data in SVA or PSL languages or OVL libraries for simulation and/or formal verification.

 
Features

Simple to Construct Flow Diagrams with included Shapes Stencil

Runs as a Microsoft Office Visio Add-on

Supports the Verilog 2001 and System Verilog HDL languages

Generates PSL, SVA and OVL Assertions

Automatically extracts Assertions and Path Covers for logic depicted in diagram

Extensive FSM Support

Great for documentation of designs: Visio objects import directly into word processors such as Microsoft's Word and Adobe's FrameMaker.

Windows or Enterprise (Linux) versions

 
 
CoverAll™
FC2Assert
TD2Assert
RTLComposer
Ver2FC
Wave2TD
Example Flow Chart  
 
Structural Flow Chart

Process

1. Architect or Designer draws Flow Diagram.

2. FC2Assert extracts Assertions and Cover Paths from Diagram.

3. RTLComposer extracts RTL, generates Testbench and Formal Verification scripts.

This simple diagram depicts two registers: cnt and clk_en.

The registers are clocked on the positive edge of signal clk and are asynchronously reset by active low signal nReset.

Active high synchronous reset signal rst is indicated by the arrow from the oblong block to the first rectangle.

RTL, assertions and functional coverage properties are all generated from a single source!

Download the Source file: cnt.vsd

module cnt (
        clk,
        nReset,
        rst,
        ena,
        slave_wait,
        clk_cnt,
        cnt,
        clk_en);

input		clk;
input		nReset;
input		rst;
input		ena;
input		slave_wait;
input	[15:0]	clk_cnt;

output	[15:0]	cnt;
output		clk_en;

reg	[15:0]	cnt;
reg		clk_en;

     always_ff@(posedge clk or negedge nReset) begin
         if(!nReset) begin
             cnt[15:0]<=16'h0;
             clk_en<=1'b1;
         end
         else begin
             if(rst) begin
                 cnt[15:0]<=16'h0;
                 clk_en<=1'b1;
             end
             else begin
                 if(ena) begin
                     if(cnt==16'h00) begin
                         cnt<=clk_cnt;
                         clk_en<=1'b1;
                     end
                     else begin
                         if(slave_wait) begin
                             cnt<=cnt;
                             clk_en<=1'b0;
                         end
                         else begin
                             cnt<=cnt-16'h1;
                             clk_en<=1'b0;
                         end
                     end
                 end
                 else begin
                     cnt<=clk_cnt;
                     clk_en<=1'b1;
                 end
             end
         end
     end
endmodule
//
// async reset property for signal clk_en
//
property fc2a_sva_clk_en_arst;
@(posedge clk)
(!nReset |-> clk_en == 1'b1);
endproperty
FC2A_SVA_CLK_EN_ARST : assert property(fc2a_sva_clk_en_arst);
//
// sync reset property for signal clk_en
//
property fc2a_sva_clk_en_srst;
@(posedge clk)
disable iff(!nReset)
(rst |=> clk_en === 1'b1);
endproperty
FC2A_SVA_CLK_EN_SRST : assert property(fc2a_sva_clk_en_srst);
//
// property #1 for signal clk_en
//
property fc2a_sva_clk_en_prop1;
@(posedge clk)
disable iff((!nReset) | (rst))
((~(slave_wait) & ~(cnt==16'h00) & (ena)) |=> clk_en === 1'b0);
endproperty
FC2A_SVA_CLK_EN_PROP1 : assert property(fc2a_sva_clk_en_prop1);
//
// property #2 for signal clk_en
//
property fc2a_sva_clk_en_prop2;
@(posedge clk)
disable iff((!nReset) | (rst))
(((slave_wait) & ~(cnt==16'h00) & (ena)) |=> clk_en === 1'b0);
endproperty
FC2A_SVA_CLK_EN_PROP2 : assert property(fc2a_sva_clk_en_prop2);
//
// property #3 for signal clk_en
//
property fc2a_sva_clk_en_prop3;
@(posedge clk)
disable iff((!nReset) | (rst))
((~(ena)) |=> clk_en === 1'b1);
endproperty
FC2A_SVA_CLK_EN_PROP3 : assert property(fc2a_sva_clk_en_prop3);
//
// property #4 for signal clk_en
//
property fc2a_sva_clk_en_prop4;
@(posedge clk)
disable iff((!nReset) | (rst))
(((cnt==16'h00) & (ena)) |=> clk_en === 1'b1);
endproperty
FC2A_SVA_CLK_EN_PROP4 : assert property(fc2a_sva_clk_en_prop4);
//
// property #1 for signal cnt
//
property fc2a_sva_cnt_prop1;
@(posedge clk)
disable iff((!nReset) | (rst))
((~(slave_wait) & ~(cnt==16'h00) & (ena)) |=> cnt === $past(cnt)-16'h1);
endproperty
FC2A_SVA_CNT_PROP1 : assert property(fc2a_sva_cnt_prop1);
//
// property #2 for signal cnt
//
property fc2a_sva_cnt_prop2;
@(posedge clk)
disable iff((!nReset) | (rst))
(((slave_wait) & ~(cnt==16'h00) & (ena)) |=> cnt === $past(cnt));
endproperty
FC2A_SVA_CNT_PROP2 : assert property(fc2a_sva_cnt_prop2);
//
// property #3 for signal cnt
//
property fc2a_sva_cnt_prop3;
@(posedge clk)
disable iff((!nReset) | (rst))
((~(ena)) |=> cnt === $past(clk_cnt));
endproperty
FC2A_SVA_CNT_PROP3 : assert property(fc2a_sva_cnt_prop3);
//
// property #4 for signal cnt
//
property fc2a_sva_cnt_prop4;
@(posedge clk)
disable iff((!nReset) | (rst))
(((cnt==16'h00) & (ena)) |=> cnt === $past(clk_cnt));
endproperty
FC2A_SVA_CNT_PROP4 : assert property(fc2a_sva_cnt_prop4);
//
// async reset property for signal cnt[15:0]
//
property fc2a_sva_cnt_15_to_0_arst;
@(posedge clk)
(!nReset |-> cnt[15:0] == 16'h0);
endproperty
FC2A_SVA_CNT_15_TO_0_ARST : assert property(fc2a_sva_cnt_15_to_0_arst);
//
// sync reset property for signal cnt[15:0]
//
property fc2a_sva_cnt_15_to_0_srst;
@(posedge clk)
disable iff(!nReset)
(rst |=> cnt[15:0] === 16'h0);
endproperty
FC2A_SVA_CNT_15_TO_0_SRST : assert property(fc2a_sva_cnt_15_to_0_srst);
//
// Path properties for flow 0
//
FC2A_SVA_PATH_CNT1_0_1 : cover property (@(posedge clk) (~(slave_wait) & ~(cnt==16'h00) & (ena)));
FC2A_SVA_PATH_CNT1_0_2 : cover property (@(posedge clk) ((slave_wait) & ~(cnt==16'h00) & (ena)));
FC2A_SVA_PATH_CNT1_0_3 : cover property (@(posedge clk) (~(ena)));
FC2A_SVA_PATH_CNT1_0_4 : cover property (@(posedge clk) ((cnt==16'h00) & (ena)));
//
// async reset property for signal clk_en
//
property fc2a_psl_clk_en_arst = always(!nReset -> clk_en == 1'b1)
	@(posedge clk);
FC2A_PSL_CLK_EN_ARST : assert fc2a_psl_clk_en_arst;
//
// sync reset property for signal clk_en
//
property fc2a_psl_clk_en_srst = always({rst} |=> {clk_en === 1'b1})
	@(posedge clk) abort (!nReset);
FC2A_PSL_CLK_EN_SRST : assert fc2a_psl_clk_en_srst;
//
// property #1 for signal clk_en
//
property fc2a_psl_clk_en_prop1 = always({(~(slave_wait) & ~(cnt==16'h00) & (ena))} |=> {clk_en === 1'b0})
	@(posedge clk)abort ((!nReset) | (rst));
FC2A_PSL_CLK_EN_PROP1 : assert fc2a_psl_clk_en_prop1;
//
// property #2 for signal clk_en
//
property fc2a_psl_clk_en_prop2 = always({((slave_wait) & ~(cnt==16'h00) & (ena))} |=> {clk_en === 1'b0})
	@(posedge clk)abort ((!nReset) | (rst));
FC2A_PSL_CLK_EN_PROP2 : assert fc2a_psl_clk_en_prop2;
//
// property #3 for signal clk_en
//
property fc2a_psl_clk_en_prop3 = always({(~(ena))} |=> {clk_en === 1'b1})
	@(posedge clk)abort ((!nReset) | (rst));
FC2A_PSL_CLK_EN_PROP3 : assert fc2a_psl_clk_en_prop3;
//
// property #4 for signal clk_en
//
property fc2a_psl_clk_en_prop4 = always({((cnt==16'h00) & (ena))} |=> {clk_en === 1'b1})
	@(posedge clk)abort ((!nReset) | (rst));
FC2A_PSL_CLK_EN_PROP4 : assert fc2a_psl_clk_en_prop4;
//
// property #1 for signal cnt
//
property fc2a_psl_cnt_prop1 = always({(~(slave_wait) & ~(cnt==16'h00) & (ena))} |=> {cnt === prev(cnt)-16'h1})
	@(posedge clk)abort ((!nReset) | (rst));
FC2A_PSL_CNT_PROP1 : assert fc2a_psl_cnt_prop1;
//
// property #2 for signal cnt
//
property fc2a_psl_cnt_prop2 = always({((slave_wait) & ~(cnt==16'h00) & (ena))} |=> {cnt === prev(cnt)})
	@(posedge clk)abort ((!nReset) | (rst));
FC2A_PSL_CNT_PROP2 : assert fc2a_psl_cnt_prop2;
//
// property #3 for signal cnt
//
property fc2a_psl_cnt_prop3 = always({(~(ena))} |=> {cnt === prev(clk_cnt)})
	@(posedge clk)abort ((!nReset) | (rst));
FC2A_PSL_CNT_PROP3 : assert fc2a_psl_cnt_prop3;
//
// property #4 for signal cnt
//
property fc2a_psl_cnt_prop4 = always({((cnt==16'h00) & (ena))} |=> {cnt === prev(clk_cnt)})
	@(posedge clk)abort ((!nReset) | (rst));
FC2A_PSL_CNT_PROP4 : assert fc2a_psl_cnt_prop4;
//
// async reset property for signal cnt[15:0]
//
property fc2a_psl_cnt_15_to_0_arst = always(!nReset -> cnt[15:0] == 16'h0)
	@(posedge clk);
FC2A_PSL_CNT_15_TO_0_ARST : assert fc2a_psl_cnt_15_to_0_arst;
//
// sync reset property for signal cnt[15:0]
//
property fc2a_psl_cnt_15_to_0_srst = always({rst} |=> {cnt[15:0] === 16'h0})
	@(posedge clk) abort (!nReset);
FC2A_PSL_CNT_15_TO_0_SRST : assert fc2a_psl_cnt_15_to_0_srst;
//
// Path properties for flow 0
//
FC2A_PSL_PATH_CNT1_0_1 : cover {~(slave_wait) & ~(cnt==16'h00) & (ena)} @(posedge clk);
FC2A_PSL_PATH_CNT1_0_2 : cover {(slave_wait) & ~(cnt==16'h00) & (ena)} @(posedge clk);
FC2A_PSL_PATH_CNT1_0_3 : cover {~(ena)} @(posedge clk);
FC2A_PSL_PATH_CNT1_0_4 : cover {(cnt==16'h00) & (ena)} @(posedge clk);
// standard defines
`define OVL_XCHECK_OFF
`define OVL_MAX_REPORT_COVER_POINT 1
`include "std_ovl_defines.h"
//
// async reset property for signal clk_en
//
assert_implication #(`OVL_ERROR, `OVL_ASSERT, "fc2a_ovl_v1_clk_en_arst") fc2a_ovl_v1_clk_en_arst (clk, 1'b1, !nReset, clk_en == 1'b1);
//
// sync reset property for signal clk_en
//
assert_next #(`OVL_ERROR, 1, 1, 0, `OVL_ASSERT, "fc2a_ovl_v1_clk_en_srst") fc2a_ovl_v1_clk_en_srst (clk, ~(!nReset), rst, clk_en == 1'b1);
//
// property #1 for signal clk_en
//
assert_next #(`OVL_ERROR, 1, 1, 0, `OVL_ASSERT, "fc2a_ovl_v1_clk_en_prop1") fc2a_ovl_v1_clk_en_prop1 (clk, ~((!nReset) | (rst)), (~(slave_wait) & ~(cnt==16'h00) & (ena)), clk_en === 1'b0);
//
// property #2 for signal clk_en
//
assert_next #(`OVL_ERROR, 1, 1, 0, `OVL_ASSERT, "fc2a_ovl_v1_clk_en_prop2") fc2a_ovl_v1_clk_en_prop2 (clk, ~((!nReset) | (rst)), ((slave_wait) & ~(cnt==16'h00) & (ena)), clk_en === 1'b0);
//
// property #3 for signal clk_en
//
assert_next #(`OVL_ERROR, 1, 1, 0, `OVL_ASSERT, "fc2a_ovl_v1_clk_en_prop3") fc2a_ovl_v1_clk_en_prop3 (clk, ~((!nReset) | (rst)), (~(ena)), clk_en === 1'b1);
//
// property #4 for signal clk_en
//
assert_next #(`OVL_ERROR, 1, 1, 0, `OVL_ASSERT, "fc2a_ovl_v1_clk_en_prop4") fc2a_ovl_v1_clk_en_prop4 (clk, ~((!nReset) | (rst)), ((cnt==16'h00) & (ena)), clk_en === 1'b1);
//
// property #1 for signal cnt
//
assert_reg_loaded #(`OVL_ERROR, 0, 0, 1, 2, `OVL_ASSERT, "fc2a_ovl_v1_cnt_prop1") fc2a_ovl_v1_cnt_prop1 (clk, ~((!nReset) | (rst)), (~(slave_wait) & ~(cnt==16'h00) & (ena)), 1'b0, cnt-16'h1, cnt);
//
// property #2 for signal cnt
//
assert_reg_loaded #(`OVL_ERROR, 0, 0, 1, 2, `OVL_ASSERT, "fc2a_ovl_v1_cnt_prop2") fc2a_ovl_v1_cnt_prop2 (clk, ~((!nReset) | (rst)), ((slave_wait) & ~(cnt==16'h00) & (ena)), 1'b0, cnt, cnt);
//
// property #3 for signal cnt
//
assert_reg_loaded #(`OVL_ERROR, 0, 0, 1, 2, `OVL_ASSERT, "fc2a_ovl_v1_cnt_prop3") fc2a_ovl_v1_cnt_prop3 (clk, ~((!nReset) | (rst)), (~(ena)), 1'b0, clk_cnt, cnt);
//
// property #4 for signal cnt
//
assert_reg_loaded #(`OVL_ERROR, 0, 0, 1, 2, `OVL_ASSERT, "fc2a_ovl_v1_cnt_prop4") fc2a_ovl_v1_cnt_prop4 (clk, ~((!nReset) | (rst)), ((cnt==16'h00) & (ena)), 1'b0, clk_cnt, cnt);
//
// async reset property for signal cnt[15:0]
//
assert_implication #(`OVL_ERROR, `OVL_ASSERT, "fc2a_ovl_v1_cnt_15_to_0_arst") fc2a_ovl_v1_cnt_15_to_0_arst (clk, 1'b1, !nReset, cnt[15:0] == 16'h0);
//
// sync reset property for signal cnt[15:0]
//
assert_next #(`OVL_ERROR, 1, 1, 0, `OVL_ASSERT, "fc2a_ovl_v1_cnt_15_to_0_srst") fc2a_ovl_v1_cnt_15_to_0_srst (clk, ~(!nReset), rst, cnt[15:0] == 16'h0);
//
// Path properties for flow 0
//
assert_implication #(`OVL_ERROR, `OVL_ASSERT, "fc2a_ovl_v1_path_cnt1_0_1") fc2a_ovl_v1_path_cnt1_0_1(clk, ~((!nReset) | (rst)), ~(slave_wait) & ~(cnt==16'h00) & (ena), ~(slave_wait) & ~(cnt==16'h00) & (ena) === 1'b1);
assert_implication #(`OVL_ERROR, `OVL_ASSERT, "fc2a_ovl_v1_path_cnt1_0_2") fc2a_ovl_v1_path_cnt1_0_2(clk, ~((!nReset) | (rst)), (slave_wait) & ~(cnt==16'h00) & (ena), (slave_wait) & ~(cnt==16'h00) & (ena) === 1'b1);
assert_implication #(`OVL_ERROR, `OVL_ASSERT, "fc2a_ovl_v1_path_cnt1_0_3") fc2a_ovl_v1_path_cnt1_0_3(clk, ~((!nReset) | (rst)), ~(ena), ~(ena) === 1'b1);
assert_implication #(`OVL_ERROR, `OVL_ASSERT, "fc2a_ovl_v1_path_cnt1_0_4") fc2a_ovl_v1_path_cnt1_0_4(clk, ~((!nReset) | (rst)), (cnt==16'h00) & (ena), (cnt==16'h00) & (ena) === 1'b1);
// standard defines
`define OVL_XCHECK_OFF
`define OVL_MAX_REPORT_COVER_POINT 1
`include "std_ovl_defines.h"
//
// async reset property for signal clk_en
//
ovl_implication #(`OVL_ERROR, `OVL_ASSERT, "fc2a_ovl_v2_clk_en_arst") fc2a_ovl_v2_clk_en_arst (clk, 1'b1, !nReset, 1'b1, clk_en == 1'b1, );
//
// sync reset property for signal clk_en
//
ovl_next #(`OVL_ERROR, 1, 1, 0, `OVL_ASSERT, "fc2a_ovl_v2_clk_en_srst") fc2a_ovl_v2_clk_en_srst (clk, ~(!nReset), 1'b1, rst, clk_en == 1'b1, );
//
// property #1 for signal clk_en
//
ovl_next #(`OVL_ERROR, 1, 1, 0, `OVL_ASSERT, "fc2a_ovl_v2_clk_en_prop1") fc2a_ovl_v2_clk_en_prop1 (clk, ~((!nReset) | (rst)), 1'b1, (~(slave_wait) & ~(cnt==16'h00) & (ena)), clk_en === 1'b0, );
//
// property #2 for signal clk_en
//
ovl_next #(`OVL_ERROR, 1, 1, 0, `OVL_ASSERT, "fc2a_ovl_v2_clk_en_prop2") fc2a_ovl_v2_clk_en_prop2 (clk, ~((!nReset) | (rst)), 1'b1, ((slave_wait) & ~(cnt==16'h00) & (ena)), clk_en === 1'b0, );
//
// property #3 for signal clk_en
//
ovl_next #(`OVL_ERROR, 1, 1, 0, `OVL_ASSERT, "fc2a_ovl_v2_clk_en_prop3") fc2a_ovl_v2_clk_en_prop3 (clk, ~((!nReset) | (rst)), 1'b1, (~(ena)), clk_en === 1'b1, );
//
// property #4 for signal clk_en
//
ovl_next #(`OVL_ERROR, 1, 1, 0, `OVL_ASSERT, "fc2a_ovl_v2_clk_en_prop4") fc2a_ovl_v2_clk_en_prop4 (clk, ~((!nReset) | (rst)), 1'b1, ((cnt==16'h00) & (ena)), clk_en === 1'b1, );
//
// property #1 for signal cnt
//
ovl_reg_loaded #(`OVL_ERROR, 1, 1, 2, `OVL_ASSERT, "fc2a_ovl_v2_cnt_prop1") fc2a_ovl_v2_cnt_prop1 (clk, ~((!nReset) | (rst)), 1'b1, (~(slave_wait) & ~(cnt==16'h00) & (ena)), 1'b0, cnt-16'h1, cnt, );
//
// property #2 for signal cnt
//
ovl_reg_loaded #(`OVL_ERROR, 1, 1, 2, `OVL_ASSERT, "fc2a_ovl_v2_cnt_prop2") fc2a_ovl_v2_cnt_prop2 (clk, ~((!nReset) | (rst)), 1'b1, ((slave_wait) & ~(cnt==16'h00) & (ena)), 1'b0, cnt, cnt, );
//
// property #3 for signal cnt
//
ovl_reg_loaded #(`OVL_ERROR, 1, 1, 2, `OVL_ASSERT, "fc2a_ovl_v2_cnt_prop3") fc2a_ovl_v2_cnt_prop3 (clk, ~((!nReset) | (rst)), 1'b1, (~(ena)), 1'b0, clk_cnt, cnt, );
//
// property #4 for signal cnt
//
ovl_reg_loaded #(`OVL_ERROR, 1, 1, 2, `OVL_ASSERT, "fc2a_ovl_v2_cnt_prop4") fc2a_ovl_v2_cnt_prop4 (clk, ~((!nReset) | (rst)), 1'b1, ((cnt==16'h00) & (ena)), 1'b0, clk_cnt, cnt, );
//
// async reset property for signal cnt[15:0]
//
ovl_implication #(`OVL_ERROR, `OVL_ASSERT, "fc2a_ovl_v2_cnt_15_to_0_arst") fc2a_ovl_v2_cnt_15_to_0_arst (clk, 1'b1, !nReset, 1'b1, cnt[15:0] == 16'h0, );
//
// sync reset property for signal cnt[15:0]
//
ovl_next #(`OVL_ERROR, 1, 1, 0, `OVL_ASSERT, "fc2a_ovl_v2_cnt_15_to_0_srst") fc2a_ovl_v2_cnt_15_to_0_srst (clk, ~(!nReset), 1'b1, rst, cnt[15:0] == 16'h0, );
//
// Path properties for flow 0
//
ovl_implication #(`OVL_ERROR, `OVL_ASSERT, "fc2a_ovl_v2_path_cnt1_0_1") fc2a_ovl_v2_path_cnt1_0_1(clk, ~((!nReset) | (rst)), 1'b1, ~(slave_wait) & ~(cnt==16'h00) & (ena), ~(slave_wait) & ~(cnt==16'h00) & (ena) === 1'b1, );
ovl_implication #(`OVL_ERROR, `OVL_ASSERT, "fc2a_ovl_v2_path_cnt1_0_2") fc2a_ovl_v2_path_cnt1_0_2(clk, ~((!nReset) | (rst)), 1'b1, (slave_wait) & ~(cnt==16'h00) & (ena), (slave_wait) & ~(cnt==16'h00) & (ena) === 1'b1, );
ovl_implication #(`OVL_ERROR, `OVL_ASSERT, "fc2a_ovl_v2_path_cnt1_0_3") fc2a_ovl_v2_path_cnt1_0_3(clk, ~((!nReset) | (rst)), 1'b1, ~(ena), ~(ena) === 1'b1, );
ovl_implication #(`OVL_ERROR, `OVL_ASSERT, "fc2a_ovl_v2_path_cnt1_0_4") fc2a_ovl_v2_path_cnt1_0_4(clk, ~((!nReset) | (rst)), 1'b1, (cnt==16'h00) & (ena), (cnt==16'h00) & (ena) === 1'b1, );

Copyright © 2012 Solid Oak Technologies, LLC. All Rights Reserved
Privacy Policy | Terms of Use