behavior can be expressed in terms of logical functions and sequential elements can be abstracted by the tool: any analog technology of implementation is well understood by TLL, including dynamic logics, CVSL... A non-exhaustive list of abstractable blocks includes processors, static memories, FPGAs, cache memories etc.
[...]
.SUBCKT MY_FLOP CK S1 S2 I1 I2 Q
*.pininfo CK:i S1:i S2:i I1:i I2:i Q:o
MP0 N23 CK VDD VDD P w=1.2u l=33.9u
MN0 N23 CK GND GND N w=1.2u l=22.1u
MP1 N24 N23 VDD VDD P w=1.2u l=33.9u
MN2 N24 N23 GND GND N w=1.2u l=22.1u
MP2 Q N25 VDD VDD P w=1.2u l=33.9u
MN3 Q N25 GND GND N w=1.2u l=22.1u
MP3 N26 N24 N27 VDD P w=1.2u l=33.9u
[...]
TLL abstraction produces:
[...]
always @(S1 or S2)
begin
if ((S1 ^ S2) != 1'b1) begin
$display("Constraint violation in MY_FLOP");
end
end
//synopsys translate_on
assign Q = N31;
/*--- Instantiations ---*/
tll_flop ff_1(.rst_1(gnd), .set_2(gnd), .rst_3(gnd), .d(N34), .clk(CK), .q(N31), .qn());
tll_mux_2b mux_N34 (.din1(I2), .din2(I1), .ctrl(S1), .dout(N34));
[...]
What TLL does not do
Official TLL 3.x series do not analyse delays, but up-coming TLL 4 will
One can specify that a signal is a precharge, and the tool will proceed according to the principle of remanence to correctly abstract the signal. However the tool will not confirm that the clock and the circuit are compatible with this remanence or even for example that the precharge transistor is powerful enough to precharge correctly according to the physical characteristics of the circuit etc. It analyses the current flow based on the transistor conductance as precisely as Spice, but only considers the result in the stable phase. It does not have any knowledge of the operating frequencies or the length of the wires...
No analysis of consumption
No study of parasitic effects or other problems related to placement and routing
Practical use
Is TLL automatic ?
Many algorithms and operations are automatic. Generally speaking, TLL will do the right thing by default. TLL’s configuration files are straightforward, although certain configuration techniques can allow the speed of analysis and the quality of the produced model to be drastically improved: a sound knowledge of transistor theory is essential in order to get the best performance from the tool.
Modes of operation
TLL can function in batch mode or via a graphical user interface. The latter allows the visualization of transistor or RTL circuits, as well as offering debugging tools, control of the abstraction process and the customisation of the majority of the configuration options of the tool.
Supported platforms
- Sparc Solaris 7,8 et 9
- i386 Linux RedHat 7.2 and above
Performance
TLL is very fast, particularly considering the 100% formal nature of the analysis.
Some performances figures
- Cache memory (78M transistors) abstracted in less than twenty minutes, using 700Mb RAM.
- Library of 1500 standard cells: 8s.
- Full processor: 230 million transistors, abstracted in a few hours
References
“TLL allowed us to exhaustively verify a whole library in less than one hour. We’ve been able to find functional bugs that had not been found previously.”
Remy Chevalier - Functional Verification Engineer - ST Microelectronics
“We needed a flow that [...]. The abstraction was made possible thanks to TLL flexibility and ease-of-use. After that, the equivalence checking was also straightforward thanks to the quality of the abstracted model generated by TLL.”
Jean-Marc Château - CMG Design Manager - ST Microelectronics
“With TLL we were able to functionally compare the HDL models for the abstracted full-custom designs against our reference models using an equivalence checker. TLL generates high quality HDL code that also enables speed up of dynamic verification by orders of magnitude compared to transistor level simulation.”
Borhan Roohipour - Sr. Member of Technical Staff - AMD
«[...] First of all thanks for all your efforts in providing us with proper TLL fixes and patches to enable us to deploy TLL as the abstraction engine for K8 full custom macro verification flow. TLL is now officially part of our production flow [...] »
Borhan Roohipour - Sr. Member of Technical Staff - AMD
"AMD's Macro Functional Verification team in Sunnyvale, CA deployed TLL to abstract full-custom macro designs, enabling the use of equivalence checking to speed up the verification process. AMD's Macro Functional Verification team specializes in the verification of the most complex full-custom macro designs, where full-custom design of IP blocks is often the best way to achieve optimal performance for a given functionality. Mostly used in systems-on-a-chip to be produced at a very high volume, full-custom design is extended for AMD microprocessors to the entire chip, in order to attain best-in-class performance for every new generation CPU. However, due to the large amount of information inherited from working at a low level of abstraction, the design and verification processes are very complex and extremely time consuming."
"With TLL we were able to create high-level abstracted models of our AMD Athlon™ 64 and AMD Opteron™ processor full-custom macro designs," says Borhan Roohipour, senior member of technical staff, Macro Functional Verification for AMD's California Microprocessor Division.
"Thanks to TLL's accurate latch, flip-flop and ram recognition engine, we have been able to functionally compare the HDL models for the abstracted full-custom designs against our reference models using an equivalence checker. TLL generates high-quality HDL code that also enables significant speed up of dynamic verification. In addition, the tool's advanced hierarchical manipulation capability and user-friendly GUI makes it very flexible to insert in our flow."
Link to article
Download TLL overview
TLL and validation flows