Constraint Verification
Formal verification of SDC constraints
• Flags constraint/design issues that are not caught by other tools
• Eliminates the need for gate-level sims and the risk of silicon failure from bad constraints
• Assertions generated for timing exceptions that fail formal proof
• Use of RTL simulation to verify generated assertions is recommended– reduces review effort
• RTL input is recommended– RTL is not synthesized by the tool, allowing compact assertions to be generated
for simulation
• Refocus maps gate-level signoff constraints to RTL
Constraint Verification Capabilities
Generated
Clock
• Waveform Glitch
Verification Are timing
Constraint • Alignment endpoints
Mapping Verification glitch safe? CDC
Formal Timing RDC
Constraint Exception
Lint • FP
Verification
• MCP
Verification
Constraint Mapping
Application of Constraints to RTL
Tcl is converted to SDC
Loops are unrolled, filters evaluated, wildcards expanded
Netlist names are mapped to RTL
LEC Mapping file can optionally be provided (normally not required)
Syntax issues are flagged
Incorrect object references are flagged
set_multicycle_path –setup 2 –from [get_pins u_arbiter_ready_reg_3]
set_false_path –through [get_pins genloop*u_adder/sum]
set_multicycle_path –setup 2 –from u_arbiter/ready_reg[3]
set_false_path –through {genloop[0].u_adder/sum
genloop[1].u_adder/sum genloop[2].u_adder/sum
genloop[3].u_adder/sum}
Back
Formal Constraint Lint
Clock Definitions • Unclocked registers, missing clock definitions
• Missing generated clocks
Generated Clock • Incorrect edge specification
Definitions • No combinational path from master to generated clock
• Clock reconvergence
Clock Propagation • False paths in clock propagation network
Clock Crossing • Missing/incorrect clock groups, clock-to-clock false paths
Case Analysis • Conflicting case analysis
• Setup MCPs with missing hold MCP
Exception Issues • Overlapping timing exceptions
• Timing exceptions that apply to large numbers of paths
Input/Output Delays • Missing I/O constraints
Back
No Combinational Path from Master to Generated
Clock
Unintended path
Intended path
create_clock –name clk {clk} –period 10
create_generated_clock –name genclk1 –source clk –master_clock clk {U1/O}
create_generated_clock –name genclk2 –source clk –master_clock clk {U2/Q}
Back
False Paths in Clock Propagation Network
create_clock –period 10 CLKA
create_clock –period 10 CLKB
create_clock –period 15 TCLK
Back
Incorrect Logically Exclusive Clock Group
set_clock_group –logically_exclusive –group clk –group genclk
Back
Conflicting Case Analysis
set_case_analysis 0 U1/S
set_case_analysis 0 U2/S
Back
Generated Clock Waveform Verification
create_clock clk –period 10
create_generated_clock –source clk –edges {1 3 7} genclk
1 2 3 4 5 6 7 8 9
clk
specified
genclk
actual
genclk Back
Generated Clock Alignment Verification
mclk
mclkby2
mclkby4
4 cycles
mclkby8 of mclk
2 cycles
of mclk
Back
False-Path Verification
All paths constrained by a false-path are verified
Clock-to-Clock FPs are verified as part of constraint lint
Only paths between synchronous clocks are verified
Path passes verification if any of the following is true:
Startpoint is static
Endpoint is synchronizer cell
Condition required to propagate a transition from startpoint to
endpoint can never be true
Assertion generated for FP that fails formal verification
FPs that are specified for “timing don’t care” reasons should
not be verified
Back
False-Path Supported by Design Logic
set_false_path –from FF1_reg –to CLKB
set_false_path –from FF2_reg –to CLKA
Back
False-Path Assertion
module u_top_fp15_1 (input bit clk, input logic from_reg, input logic
to_reg, input bit v1);
wire path_propagation_condition = ( !v1 );
property e_fp15_1;
@(posedge clk) `FT_DISABLE (`FT_TRANSITIONS_AND_NOT_UNKNOWN(from_reg))
|=> (`FT_PPC_IS_FALSE_IN_PREV_CYCLE(path_propagation_condition)
|| (!(`FT_TRANSITIONS_AND_NOT_UNKNOWN(to_reg))));
endproperty
fp15_1: assert property(e_fp15_1) $display("top_fp15_1 checked"); else
$error("top_fp15_1 failed");
endmodule
bind top u_top_fp15_1 sva_u_top_fp15_1(.clk(clk1), .from_reg(r1),
.to_reg(r2),
.v1(i_mux.INT_TXBYTECLK_PORT_GEN[0].\ctech_lib_clk_mux_2to1_txbyteclkhs_int
[txport].s));
Back
Multi-Cycle Path Verification
All paths constrained by a multi-cycle path are verified
Only paths between synchronous clocks are verified
Path passes verification if any of the following is true:
Startpoint is static
Endpoint is allowed to go metastable and startpoint value is held
stable for multiple cycles
Condition required to propagate a transition from startpoint to
endpoint is not true when the startpoint transitions
Assertion generated for MCP that fails formal verification
MCPs that are specified for “timing don’t care” reasons
should not be verified
Back
Multi-Cycle Path Supported by Design Logic
set_multicycle_path –setup 2 –from FF1 –to FF2
set_multicycle_path –hold 1 –from FF1 –to FF2
Back
Multi-Cycle Path Assertion
module u_top_mcp9_4 (input bit clk, input logic from_reg, input logic
to_reg_1, input logic to_reg_2, input bit [1:0] v60, input bit [3:0] v62,
input bit [1:0] v66);
wire path_propagation_condition_1 =
( (v60[1:0] == 2'b11) && (v62[3:0] == 4'b0011) );
wire path_propagation_condition_2 =
( (v62[3:0] == 4'b0011) && (v66[1:0] == 2'b00) );
property e_mcp9_4_1;
@(posedge clk) `FT_DISABLE
(`FT_TRANSITIONS_AND_NOT_UNKNOWN(from_reg)) |=> (
((`FT_PPC_IS_FALSE_IN_PREV_CYCLE(path_propagation_condition_2) ||
(!(`FT_TRANSITIONS_AND_NOT_UNKNOWN(to_reg_2)))) &&
(`FT_PPC_IS_FALSE_IN_PREV_CYCLE(path_propagation_condition_1) ||
(!(`FT_TRANSITIONS_AND_NOT_UNKNOWN(to_reg_1))))));
endproperty
mcp9_4_1: assert property(e_mcp9_4_1) $display("top_mcp9_4 checked"); else
$error("top_mcp9_4 failed");
endmodule
bind top u_top_mcp9_4 sva_u_top_mcp9_4(.clk(clk), .from_reg(sp1),
.to_reg_1(q1), .to_reg_2(q2), .v60(dis1), .v62(counter), .v66(dis2)); Back
Glitch Verification
@(posedge clk)
(($rose(poken10_1p8) && `FT_IS_LO(pok10_1p8) && $fell(pok10_out_1p8)) ||
($fell(poken10_1p8) && `FT_IS_LO(pok10_1p8) && $rose(pok10_out_1p8)))
|->
(!(`FT_IS_HI(reset_tamper_extended.q) && `FT_IS_LO(U240.y) &&
`FT_IS_LO(U34.y) && `FT_IS_HI(U244.y) && `FT_IS_HI(u245.y) )); Back
Back
RDC Verification
Path through async reset to capture flop must be false
Formal verification, with assertions generated for formal failures
Back
Formal CDC Verification
Formal proof that async. clock crossings are correctly synchronized
Verification that either handshake mechanism is in place for correct data
transfer or path ends at synchronizer cell
No need to specify or recognize CDC structures
Back
