Solid Oak Technologies logo

Timing Diagrams to Assertions

capturing design intent

The CoverAll™ TD2Assert™ module converts timing diagrams into sequences and assertions.

 
Features

Simple to construct Timing Diagrams with included Shapes Stencil

Converts timing diagram into clock-by-clock assertion sequences

Automatically extracts assertions from relationships annotated on the diagram

Runs as a Microsoft Office Visio VSL Add-on

Supports the Verilog 2001 and System Verilog HDL languages

Generates PSL and SVA Assertions

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 Timing Diagram  
   
timing diagram

1. Architect or Designer draws Timing Diagram.

2. Designer creates corresponding Flow Diagrams (FC2Assert).

3. CoverAll extracts RTL (RTLComposer), Assertions, Path Covers and Sequences from Diagram(s).

 

Download the Source file: cnt.vsd

 

//
// Timing Diagram Sequence for i2c_sta_wr
//
sequence td2a_sva_i2c_sta_wr;
@(posedge wb_clk_i)
(
	((wb_adr_i ==? 3'b100) && (wb_dat_i ==? 8'b1001xxxx) && wb_we_i && wb_stb_i && wb_cyc_i && core_en && ~(sta | sto) && ~(rd | wr) && ~tip && ~done && ~irq_flag) ##1
	(core_en && (sta | sto) && (rd | wr) && ~tip && ~done && ~irq_flag) ##1
	(core_en && (sta | sto) && (rd | wr) && tip && ~done && ~irq_flag) ##[1:10000]
	(core_en && (sta | sto) && (rd | wr) && tip && done && ~irq_flag) ##1
	(core_en && ~(sta | sto) && ~(rd | wr) && tip && ~done && irq_flag) ##1
	(core_en && ~(sta | sto) && ~(rd | wr) && ~tip && ~done && irq_flag) ##[1:100]
	((wb_adr_i ==? 3'b100) && (wb_dat_i ==? 8'bxxxxxxx1) && wb_we_i && wb_stb_i && wb_cyc_i && irq_flag) ##1
	(~irq_flag)
);
endsequence
TD2A_SVA_I2C_STA_WR : cover property (td2a_sva_i2c_sta_wr);
//
// Timing Diagram Assertion #1
//
property td2a_sva_td1_td_assert1;
@(posedge wb_clk_i)
((wb_stb_i) |-> ##[0:2] (wb_ack_o));
endproperty
TD2A_SVA_TD1_TD_ASSERT1 : assert property(td2a_sva_td1_td_assert1);
//
// Timing Diagram Assertion #2
//
property td2a_sva_td1_td_assert2;
@(posedge wb_clk_i)
(((rd | wr) && (sta | sto)) |=> (tip));
endproperty
TD2A_SVA_TD1_TD_ASSERT2 : assert property(td2a_sva_td1_td_assert2);
//
// Timing Diagram Assertion #3
//
property td2a_sva_td1_td_assert3;
@(posedge wb_clk_i)
((done) |=> ~(rd | wr));
endproperty
TD2A_SVA_TD1_TD_ASSERT3 : assert property(td2a_sva_td1_td_assert3);
//
// Timing Diagram Assertion #4
//
property td2a_sva_td1_td_assert4;
@(posedge wb_clk_i)
((~(rd | wr) && ~(sta | sto)) |=> ~(tip));
endproperty
TD2A_SVA_TD1_TD_ASSERT4 : assert property(td2a_sva_td1_td_assert4);
//
// Timing Diagram Assertion #5
//
property td2a_sva_td1_td_assert5;
@(posedge wb_clk_i)
((done) |=> ~(sta | sto));
endproperty
TD2A_SVA_TD1_TD_ASSERT5 : assert property(td2a_sva_td1_td_assert5);
//
// Timing Diagram Assertion #6
//
property td2a_sva_td1_td_assert6;
@(posedge wb_clk_i)
((done) |=> (irq_flag));
endproperty
TD2A_SVA_TD1_TD_ASSERT6 : assert property(td2a_sva_td1_td_assert6);
//
// Timing Diagram Assertion #7
//
property td2a_sva_td1_td_assert7;
@(posedge wb_clk_i)
(((wb_adr_i ==? 3'b100) && (wb_dat_i ==? 8'bxxxxxxx1) && wb_we_i && wb_stb_i && wb_cyc_i) |=> ##2 ~(irq_flag));
endproperty
TD2A_SVA_TD1_TD_ASSERT7 : assert property(td2a_sva_td1_td_assert7);
//
// Timing Diagram Sequence for i2c_sta_wr
//
sequence td2a_psl_i2c_sta_wr = {
	{(wb_adr_i ==? 3'b100) && (wb_dat_i ==? 8'b1001xxxx) && wb_we_i && wb_stb_i && wb_cyc_i && core_en && ~(sta | sto) && ~(rd | wr) && ~tip && ~done && ~irq_flag};
	{core_en && (sta | sto) && (rd | wr) && ~tip && ~done && ~irq_flag};
	{core_en && (sta | sto) && (rd | wr) && tip && ~done && ~irq_flag};[*1:10000];
	{core_en && (sta | sto) && (rd | wr) && tip && done && ~irq_flag};
	{core_en && ~(sta | sto) && ~(rd | wr) && tip && ~done && irq_flag};
	{core_en && ~(sta | sto) && ~(rd | wr) && ~tip && ~done && irq_flag};[*1:100];
	{(wb_adr_i ==? 3'b100) && (wb_dat_i ==? 8'bxxxxxxx1) && wb_we_i && wb_stb_i && wb_cyc_i && irq_flag};
	{~irq_flag}
} @(posedge wb_clk_i);
TD2A_PSL_I2C_STA_WR : cover {td2a_psl_i2c_sta_wr};
//
// Timing Diagram Assertion #1
//
property td2a_psl_td1_td_assert1 = always ((wb_stb_i) -> {[*0:2];(wb_ack_o)})
	@(posedge wb_clk_i);
TD2A_PSL_TD1_TD_ASSERT1 : assert (td2a_psl_td1_td_assert1);
//
// Timing Diagram Assertion #2
//
property td2a_psl_td1_td_assert2 = always ({((rd | wr) && (sta | sto))} |=> {(tip)})
	@(posedge wb_clk_i);
TD2A_PSL_TD1_TD_ASSERT2 : assert (td2a_psl_td1_td_assert2);
//
// Timing Diagram Assertion #3
//
property td2a_psl_td1_td_assert3 = always ({(done)} |=> {~(rd | wr)})
	@(posedge wb_clk_i);
TD2A_PSL_TD1_TD_ASSERT3 : assert (td2a_psl_td1_td_assert3);
//
// Timing Diagram Assertion #4
//
property td2a_psl_td1_td_assert4 = always ({(~(rd | wr) && ~(sta | sto))} |=> {~(tip)})
	@(posedge wb_clk_i);
TD2A_PSL_TD1_TD_ASSERT4 : assert (td2a_psl_td1_td_assert4);
//
// Timing Diagram Assertion #5
//
property td2a_psl_td1_td_assert5 = always ({(done)} |=> {~(sta | sto)})
	@(posedge wb_clk_i);
TD2A_PSL_TD1_TD_ASSERT5 : assert (td2a_psl_td1_td_assert5);
//
// Timing Diagram Assertion #6
//
property td2a_psl_td1_td_assert6 = always ({(done)} |=> {(irq_flag)})
	@(posedge wb_clk_i);
TD2A_PSL_TD1_TD_ASSERT6 : assert (td2a_psl_td1_td_assert6);
//
// Timing Diagram Assertion #7
//
property td2a_psl_td1_td_assert7 = always ({((wb_adr_i ==? 3'b100) && (wb_dat_i ==? 8'bxxxxxxx1) && wb_we_i && wb_stb_i && wb_cyc_i)} |=> {[*2];~(irq_flag)})
	@(posedge wb_clk_i);
TD2A_PSL_TD1_TD_ASSERT7 : assert (td2a_psl_td1_td_assert7);
 

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