# Using LLMs to Facilitate Formal Verification of RTL

Marcelo Orenes-Vera, Margaret Martonosi and David Wentzlaff  Department of
Computer Science and Electrical Engineering, Princeton University
Princeton, New Jersey, USA
Email: {movera, mrm<EMAIL_ADDRESS>
###### Abstract

Formal property verification (FPV) has existed for decades and has been shown
to be effective at finding intricate RTL bugs. However, formal properties,
such as those written as SystemVerilog Assertions (SVA), are time-consuming
and error-prone to write, even for experienced users. Prior work has attempted
to lighten this burden by raising the abstraction level so that SVA is
generated from high-level specifications. However, this does not eliminate the
manual effort of reasoning and writing about the detailed hardware behavior.
Motivated by the increased need for FPV in the era of heterogeneous hardware
and the advances in large language models (LLMs), we set out to explore
whether LLMs can capture RTL behavior and generate correct SVA properties.
First, we design an FPV-based evaluation framework that measures the
correctness and completeness of SVA. Then, we evaluate GPT4 iteratively to
craft the set of syntax and semantic rules needed to prompt it toward creating
better SVA. We extend the open-source AutoSVA framework by integrating our
improved GPT4-based flow to generate safety properties, in addition to
facilitating their existing flow for liveness properties. Lastly, our use
cases evaluate (1) the FPV coverage of GPT4-generated SVA on complex open-
source RTL and (2) using generated SVA to prompt GPT4 to create RTL from
scratch. Through these experiments, we find that GPT4 can generate correct SVA
even for flawed RTL—without mirroring design errors. Particularly, it
generated SVA that exposed a bug in the RISC-V CVA6 core that eluded the prior
work’s evaluation.

##  I Introduction and Background

The Cambrian explosion in the diversity of hardware caused by the end of
Moore’s law has exacerbated the challenges associated with RTL design
verification (DV) [12]. Formal property verification (FPV) utilizing industry-
standard SystemVerilog Assertions (SVA) [6] is becoming increasingly important
to provide exhaustive DV in the face of growing hardware complexity and
variety. SVA can express temporal relations over RTL signals, which fall into
two major classes: safety and liveness properties. Safety specifies that
“nothing bad will happen”, e.g., FSM transitions, while liveness specifies
that “something good will happen”, e.g., a request should eventually get a
response. FPV tools [3, 15] use solver engines based on formal methods to
search for counterexamples (CEXs) exhaustively. While FPV is very effective
for DV, engineers often feel discouraged from using it because of the steep
learning curve and additional effort to write assertions [13].

Prior work has tried to ease the use of FPV by automating parts of the
process: AutoSVA [11] generates end-to-end liveness properties from an
annotated RTL module interface; ILA [5] generates a model of the design from a
functional specification and compares it against its RTL implementation; and
RTLCheck [8] verifies the RTL of CPU pipelines for memory consistency by
synthesizing SVA from axiomatic specifications. While these are effective
tools, they either verify subsets of RTL designs or require significant effort
to write structured specifications. With the recent advances in LLMs, a
question arises: Can LLMs help accelerate RTL design and verification? And if
so, how should we integrate them into modern RTL development? In the last few
months, researchers have explored using LLMs to generate temporal logic
specifications and assertions from natural language [4, 7], as well as filling
gaps in incomplete RTL [14]. We take a more holistic approach and explore
whether LLMs can generate correct SVA for a given design without any
specification beyond the RTL—even when the RTL contains bugs. Our motivation
for that is that specifications are not always available or precise enough.
Often, implementation details are not fleshed out until the RTL is written.
This is especially true in academic and open-source hardware, where the RTL is
in continuous development [10]. Moreover, generating SVA solely from RTL would
enable formally verifying RTL that has been generated by LLMs [14].

Figure 1:  FPV-based evaluation framework. The FPV tool returns whether the
assertions generated by the LLM are correct or not—for a given RTL. Hinted by
the errors or CEXs of the FPV report, the engineer manually writes or refines
the rules that guide the LLM toward generating better SVA. The rule set and
the RTL are combined into a prompt in order to generate a new iteration of SVA
properties. The green boxes are automated steps; the blue ones are manual.

Our approach: Starting with an empty FPV testbench (FT) for an RTL module, we
aim to generate SVA that reasons about the correctness of the design without
needing to manually provide details about functionality or the properties to
be generated. We utilize GPT4 [9] for this holistic task because early
experiments with smaller LLMs were not promising. However, even state-of-the-
art GPT4 generates syntactically and semantically wrong SVA by default. Thus,
we first had to teach GPT4 how to generate correct SVA by iteratively refining
the prompt with rules (Fig. 1). We then build on top of AutoSVA [11] to
include our improved GPT4-based flow for safety properties in addition to
facilitating the existing liveness flow (Fig. 2). We make our extended
framework available—anonymized for now—as AutoSVA2[2]. Our use cases evaluate
(1) the FPV coverage of AutoSVA2 on complex RTL, and (2) using generated SVA
to prompt GPT4 to create RTL from scratch, for which AutoSVA2 can output more
SVA (Fig. 3).

Our technical contributions are:

  * •

An iterative methodology based on FPV to find the rules required to teach an
LLM how to generate syntactically and semantically correct SVA from a given
RTL module.

  * •

Evaluating GPT4 and crafting the rules that improve its SVA output, and
extending the AutoSVA framework with this improved GPT4-based SVA generation
flow.

  * •

Characterizing robustness and coverage of AutoSVA2.

  * •

An AutoSVA2-driven RTL generation and verification methodology; iteratively
improves LLM-generated RTL by prompting human-refined generated SVA (Fig. 3).

Our experiments found that:

  * •

GPT4’s creativity allows it to generate correct SVA from buggy RTL, i.e., it
is not compelled to generate SVA solely based on the RTL we have provided.

  * •

GPT4 is not significantly sensitive to the names of the RTL module and
variables in order to generate SVA.

  * •

For the same RTL modules, AutoSVA2-generated properties improved coverage of
RTL behavior by up to $6\times$ over AutoSVA-generated ones.[1].

  * •

Within an hour of engineering effort, our AutoSVA2 evaluation exposed a bug in
the RISC-V CVA6 Ariane core[10] that eluded AutoSVA’s prior evaluation[11].

  * •

GPT4 generates better RTL when we include SVA in the prompt; its creativity
allows it to generate correct RTL even if the SVA was not entirely correct.

The rest of the paper is organized as follows: Sec. II shows our iterative
approach to find flaws in the LLM-generated SVA and test rules to steer it
toward generating better SVA. Sec. III introduces AutoSVA2, our extended
framework that integrates a GPT4-based flow on top of AutoSVA to create more
complete FTs with less effort. Sec. IV and V present our two uses cases.

##  II Iteratively Teaching SVA to LLMs

Our early experiments with GPT4 showed us that it could generate several SVA
properties solely from RTL, but they contained syntactic and semantic errors.
However, we found that we could nudge GPT4 towards generating better SVA by
giving it rules to follow. Sec. II-A describes the methodology we used to
iteratively construct the set of rules that are needed in the prompt for GPT4
to generate useful assertions. Sec. II-B describes the issues we encountered
and the rules we added to the prompt to overcome them.

###  II-A Rule-refinement Methodology

Fig. 1 depicts the evaluation framework we use to iteratively refine the set
of rules to be included in the prompt of an LLM. Although all our experiments
with this framework have been done on GPT4 (Table I), we argue that it can be
used to assess the output quality of any LLM.

This methodology requires having an FT. We can create one quickly by executing
the AutoSVA [1] script indicating the target RTL module. (The generated FT has
property and tool-binding files but no assertions.) In theory, one could use
any RTL module as input to the LLM, but note that the engineer should be able
to easily determine the issues with the SVA. Ideally, the RTL module used
should be entirely correct, so that the CEXs generated by the FPV engine are
due to wrong assertions. Recall that the goal of this methodology is not to
provide a complete FT for this RTL module but rather to refine the rules for
the LLM to generate better SVA. For our experiments with GPT4 (detailed in
Sec. II-B), we used the FIFO module from the AutoSVA repository [1].

###  II-B Experiments with GPT4

We apply the above methodology to GPT4 to test its generated SVA and assess
whether our hand-written rules improve it. Particularly, we used the 8K-token
version offered via OpenAI’s chat interface [9]. We use a clean-slate context
for each iteration to avoid polluting the new SVA with previous issues.

Reproducibility is challenging with LLMs because of their creativity—a key
attribute of our interest in LLMs for SVA generation. Our best effort towards
reproducibility is to be fully transparent with our experiments. To do that,
we made a separate commit for each iteration on our anonymized repository[2]
starting from a fork of AutoSVA [1]. This repository includes prompt,
response, and FT for each iteration and a booklog with our observations for
all the experiments described in this paper.

Engineering effort: It took 23 iterations and $\sim$8 hours111 The engineering
time can be observed from the commit timestamps[2] to create the rules for
GPT4 to output a complete and correct set of assertions for the FIFO module.
Correctness was shown by full proof, and completeness was shown from statement
and toggle coverage. We obtained assertion validity and coverage using
JasperGold (JG) [3]. JG took just a few seconds to compile and test the
assertions on our server. GPT4 generated each set of SVA in under a minute.
Most of the time was spent auditing the assertions and carefully writing and
refining the rules.

LLM cost: We already had a monthly subscription to this model, so these
experiments did not incur extra costs. However, note that when used via the
API, queries to this model currently cost 0.03 USD per 1000 tokens, which
again incentivizes using a small RTL module for this task.

TABLE I: Status for compilation and SVA correctness (# of properties generated and failing) for each iteration test (T). T | Compile | #Prop | #Fail | Main issues
---|---|---|---|---
1 | ✗ | 4 | $-$ | IN: Undeclared var (no module prefix)
2 | ✗ | 6 | $-$ | SY: Wrong keyword for assertion
3 | ✗ | 8 | $-$ |  SY: Using foreach as an assertion loop
4 | ✗ | 4 | $-$ |  IN: Undeclared buffer_head_r
5 | ✗ | 9 | $-$ | SY: Error in include and assert naming
6 | ✗ | 6 | $-$ | SY: Duplicated assertion name
7 | ✓ | 6 | 4 |  WT: Wrong time semantics $|->$
8 | ✗ | 6 | 3 | IN: Undeclared var (no module prefix)
9 | ✗ | 5 | $-$ | IN: Module prefix; ignored prev. rules
10 | ✓ | 9 | 5 |  WT: Wrong time semantics $|=>$
11 | ✓ | 7 | 1 | WT: Missing $past in postcondition
12 | ✓ | 10 | 7 | WT: Too much $past usage
13 | ✗ | 9 | $-$ |  SY: Forgot foreach rule from T3
14 | ✓ | 12 | 4 | WS: Incr. without wrap; wrong signal
15 | ✓ | 8 | 2 | WT: Missing $past in postcondition
16 | ✓ | 9 | 4 | WT/WS: Wrong bitwise manipulation
17 | ✓ | 8 | 3 |  WT: Wrong time semantics $|=>$
18 | ✗ | 10 | 0 | SY: Array-named assertions as_name[i]
19 | ✗ | 12 | 2 | SY/WS: Empty precond.;wrong bitwise
20 | ✗ | 10 | $-$ | SY: Wrong width in constant usage
21 | ✓ | 7 | 1 | WT: Missing $past for register
22 | ✓ | 9 | 1 | WT: Incorrect $past in precondition
23 | ✓ | 8 | 0 | Full Proof
24 | ✓ | 8 | 1 |  Assuming wrong behavior about out_rdy

Table I shows, for each iteration test (T), whether the FPV tool successfully
compiled the property file, the number of assertions generated and failing,
and the main issues found.222The booklog contains details of the issues
observed at each iteration [2]

We group the issues into four categories: not compiling due to wrongly
referencing internal signals (IN) or wrong syntax (SY); and compiling but
using wrong timing (WT) or wrong semantics (WS). For tests where JG could not
successfully compile the FT (✗), we did not attempt to fix it to check how
many assertions failed ($-$), except on a few iterations when the compilation
error was minor (✗).

Internal Signals (IN): Since our first iteration, we observed that GPT4 would
not properly reference internal signals (not declared in the module
interface). It took several iterations to refine the rules for GPT4 to use
hierarchical referencing by prefixing the module name before the internal
signal. These rules are shown in lines 4-5 of 2.

Syntax (SY): We found errors related to using incorrect keywords, e.g.,
always@(<condition>) instead of assert, and wrong module include and property
names. GPT4 also kept using foreach wrongly to create loops of assertions. Our
rules to fix syntax issues are described in lines 1-3.

Wrong Timing (WT): One of the hardest issues to fix was the concept of time in
SVA; e.g., GPT4 kept using same-cycle implications ($|->$) for reasoning about
the updated value of registers (flip-flops). Timing becomes especially
problematic when updating registers within an array because the index selector
may also be a register. In this case, the postcondition should reason about
the updated value of the register array but the old value of the index. We
show an example of this from T16 in 1; the assertion should have used $past
for buffer_head_r. Our rules to overcome that (lines 9-16) include teaching
the concept of registers and combinational logic, same- and next-cycle
assertions, and when to use $past.

Wrong Semantics (WS): Beyond timing, we found other wrong semantics in counter
increment logic, $countones and bitwise operators. 1 shows an example of this,
where the comment generated by GPT4 is correct, but the assertion is wrongly
using !& instead of !| to check that all buffer slots are invalid. We fixed
them by adding rules to teach GPT4 about the correct behavior of these
operators (lines 6-8).

⬇

// Check that if there’s an in handshake (in_hsk), the buffer corresponding to
the head of the FIFO should be updated with data on the next cycle.

as__in_hsk_data_update: assert property (fifo.in_hsk |=>
fifo.buffer_data_r[fifo.buffer_head_r]==$past(in_data));

// Check that out_val should be low if all slots are invalid

as__out_val_low_if_all_buffer_invalid: assert property

((!&fifo.buffer_val_r) |-> fifo.out_val == 0’b0);

Listing 1:  Semantically wrong assertions from iteration test 16.

⬇

1DO NOT declare properties; DECLARE assertions named as__<NAME>: assert
property (<EXPRESSION>).

2DO NOT use [] at the end of assertion NAME. Do not add @(posedge clk) to
EXPRESSION.

3DO NOT use foreach loops in assertions, use generate for.

4Internal signals are those NOT present in the interface. Internal signals are
declared within the module.

5Referencing internal signals in the property file ALWAYS requires prepending
the name of the module before the signal name, e.g., name.<internal_signal>.

6&bitarray means that ALL the bits are ONES.

7!(&bitarray) means it’s NOT TRUE that ALL the bits are ONES, i.e., SOME of
the bits are ZEROS.

8!(|bitarray) means that NONE of the bits are ONES, i.e., ALL the bits are
ZEROS.

9Signals ending in _reg are registers: the assigned value changes in the next
cycle.

10Signals NOT ending in _reg are wires: the assigned value changes in the same
cycle.

11USE a same-cycle assertion (|->) to reason about behavior occurring in the
same cycle.

12USE a next-cycle assertion (|=>) to reason about behavior occurring in the
next cycle, for example, the updated value of a _reg.

13DO NOT USE $past() in preconditions, ONLY in postconditions

14DO NOT USE $past() on postcondition of same-cycle assertion

15On the postcondition of next-cycle assertions (|=>), USE $past() to refer to
the value of wires or a _reg on the cycle of the precondition.

16On the postcondition of next-cycle assertions (|=>), DO NOT USE $past() to
refer to the updated value of _reg.

Listing 2:  Some of the rules we crafted to refine GPT4’s SVA
generation—written in plain (imperative) English based on our knowledge of
SVA.

###  II-C Assertion Quality and Determinism

It took 7 iterations to get the first correct syntax and 18 iterations for all
assertions to pass, but we only first achieved correct syntax and full proof
at T23.

Creativity: We made an extra iteration to check for output determinism given
the same input. Of the eight assertions of T24, only two were the same as T23,
and the rest were slight variations to test similar behavior. 3 shows two of
the variations that check data integrity.

⬇

// T23: If FIFO is not empty and output handshake is true, the data at
’buffer_tail_reg’ index should be sent out in the same cycle

for (genvar i=0; i<INFLIGHT; i=i+1) begin: check_data_on_wr

as__data_correctly_written: assert property (fifo.in_hsk &&
!(|fifo.buffer_val_reg) && (fifo.buffer_head_reg == i) |=>
fifo.buffer_data_reg[i] == $past(fifo.in_data));

end

// T24: When add_buffer flag is set, the next value of buffer_data_reg at that
index should be in_data.

for (genvar i=0; i<INFLIGHT; i=i+1) begin: check_buffer_data

as__buffer_data_set: assert property (fifo.add_buffer[i] |=>
fifo.buffer_data_reg[i] == $past(fifo.in_data));

end

Listing 3:  Assertions from T23 and 24 to check data integrity. The first one
has a larger scope, since it uses more primary signals while the second one
uses an intermidiate signal from the design (add_buffer).

Asserting unknown behaviors: T24 had a failing assertion that checked that if
the FIFO consumer is not ready to read (out_rdy low), it must be because the
FIFO is empty. Since out_rdy is an input to the FIFO, the FPV can set it to
any value at any given time, and thus the assertion fails. However, we found
it interesting that GPT4 tried to assert the behavior of a signal that was not
driven inside the RTL.

RTL coverage: With the refinement of rules, GPT4 was encouraged to use more
features, and with that, it generated more assertions. We also attribute that
increase in assertion count to the better utilization of the context size.
After T9, we instructed GPT4 to output only assertions and comments, but not
module interfaces or further explanations, to save tokens in favor of
producing better SVA. (Sec. III elaborates more on how to use the context
efficiently.) Via JG’s coverage tool, we found that the SVA from T23 and T24
achieved full coverage of the FIFO module. Although a FIFO is not a complex
module, note that the SVA was generated from scratch solely based on the RTL
code and the generic set of rules from 2. Sec. IV evaluates more complex RTL
modules and shows how generating multiple batches of SVA increases coverage.

Robustness: We made two more tests to check the robustness of GPT4 with
respect to signal names. For T25, we replaced fifo with modul throughout the
entire RTL module, including the module name, to discern whether prior
knowledge about FIFO behavior enhanced GPT4’s output. GPT4 generated a set of
assertions with similar quality as T24. For T26, we replaced modul with
multiplier to investigate whether prior knowledge about multipliers would
worsen GPT4’s output for the same RTL behavior. Again, we found no significant
impact. We also observe no sign of GPT4 internally learning from prompting the
rules repeatedly since removing the rule set results in a similar SVA as in
T1.

Rule set completeness: The fact that our set of rules was good enough for our
FIFO module does not mean it is sufficient for every module. Several of the
SVA features not encountered during our rule-refinement experiments could
still cause trouble for GPT4. For example, $countones only appeared at
T25—wrongly used—so we needed to add an extra rule. This is to say, as more
RTL modules are tested with GPT4, rules may need to be appended. Moreover,
particular strategies could be used to nudge GPT4 to generate assertions in a
particular way, e.g., to write assertions about FSMs transitions (tested in
Sec. IV-A).

##  III AutoSVA2: Extending AutoSVA with GPT4

The above experiments show that SVA generated by GPT4 is useful, not because
it’s perfect (which is not), but because GPT4 generates SVA that checks
behaviors beyond what is written in the RTL—often spanning multiple assignment
steps.

We decided to integrate our new SVA generation flow into AutoSVA because: (1)
AutoSVA already generates the FT scaffolding we need to run SVA properties on
FPV tools like JasperGold (JG) [3] and YosysHQ’s SBY [15]. (2) properties
generated with AutoSVA and GPT4 can be complementary (Sec. IV-B); (3) AutoSVA
is open-source and continues being extended for new features, e.g., hardware
security [12].

Fig. 2 depicts how AutoSVA2—by combining our new flow (green arrows) with the
existing one from AutoSVA—creates a more complete FT We also added an extra
flow (blue arrows) to lighten the effort of adding annotations to the RTL
module interface. The engineer audits the generated annotations and SVA and
corrects them if necessary.

Interface-annotation flow: We crafted another set of rules333Included in our
anonymized GitHub repository[2] to teach GPT4 how to generate the annotations
about module transactions that the AutoSVA paper [11] introduced in order to
generate end-to-end liveness properties. As depicted in Fig. 2, AutoSVA2 takes
the RTL module as input and appends these rules to compose a prompt for GPT4.
We found this flow to capture transactions correctly on RTL components with
clear interfaces like the FIFO, with valid syntax and semantics. However, for
more complex modules with several interfaces like those evaluated in Sec. IV,
it grouped together interfaces and signals that are not part of the same
transaction, e.g., the memory request interface and the response into the TLB.
We argue that even when the annotations are incorrect, it is still easier for
an engineer to correct them than starting from scratch.

Figure 2:  Overview of AutoSVA2. Our additions to the original AutoSVA flow
are shown with thick boxes and arrows; the original flow is shown with thin
boxes and arrows. The green boxes indicate automatically generated artifacts.
The green arrows indicate the SVA generation flow and the blue arrows the
annotation generation flow. The engineer in the loop revises both the
annotations and the generated SVA.

Completeness of the FT: The engineer may want to generate multiple batches of
SVA, as we found that to increase completeness (Sec. IV-B) and having
redundant assertions is not problematic for FPV tools—they can reuse the same
state space exploration to prove multiple properties. On the contrary, the
annotation flow is only triggered once when the FT is first created. The
coverage metrics reported by FPV tools like JG can guide the engineer on which
interface signals may be missing annotations and which other internal signals
miss assertions. Future work could extract from the FPV report the RTL lines
that are not being covered and use that to generate a more targeted
prompt—until the SVA covers the entire design.

Completeness vs Correctness: Having SVA with full RTL coverage does not imply
that the assertions or the RTL are correct. (a) assertions producing CEXs
still contribute to coverage, and (b) assertions may have the same bug as the
RTL. Our goal with AutoSVA2 is that the generated assertions have as much
coverage as possible so that the engineer does not need to come up with new
properties but rather focus on auditing the existing one to ensure it matches
the hardware specification. Note that the engineer must audit all assertions,
not only those producing CEXs, as they may be proving the wrong thing.
Throughout our experiments, we found GPT4’s creativity valuable for SVA
generation: the fact that it generates similar properties with slight
variations makes it prone to create buggy SVA for correct RTL but also to
create correct SVA for buggy RTL.

Filtering comments from RTL design: It may seem counterintuitive at first, but
we found that removing comments from the RTL design improves the quality of
the generated SVA for larger RTL modules (e.g., those tested Sec. IV). The
GPT4 model we use has a context of 8K tokens for input and output combined;
when the prompt gets close to that limit, the model start forgetting part of
the input in order to generate the output.

Larger context sizes vs Modularity: If the module contains too many tokens
even when comments are removed ($>$500 lines), we see two options to move
forward: (1) use a model with a larger context size, e.g., GPT4-32K, or (2)
break down the RTL into smaller modules. We advocate for the latter, not only
because the 32K version currently costs twice as much as the 8K one per token
via the API but because it is good coding practice to create submodules for
self-contained functionality.

##  IV Use case 1: Testing AutoSVA2 on Complex RTL

We applied our new SVA flow with the page-table walker (PTW) and translation
look-aside buffer (TLB) of the 64-bit RISC-V CVA6 Ariane core. We chose these
modules for their complexity and because they were also evaluated in the
original AutoSVA paper [11], so we can compare the results.

Goals: With these experiments, we are not aiming to return fully verified
RTL—auditing the CEXs would require a functional specification or more
knowledge about the design. Instead, we aim to test our GPT4-based SVA
generation flow on complex RTL modules and compare the coverage of the new
properties over the existing ones from AutoSVA.

###  IV-A Building the PTW FT and exposing an RTL Bug

Because CVA6 is widely used in the open-hardware community to build chips, it
keeps being actively developed. We found that the PTW code evaluated by
AutoSVA has changed since then. Tracking the bug fixes in the OpenHW Group’s
CVA6 repo, we found that the PTW had a bug that was fixed
recently.444https://github.com/openhwgroup/cva6/pull/1184 This bug was not
uncovered by the assertions generated in AutoSVA’s evaluation [11]. Thus, we
set out to evaluate whether AutoSVA2 could find this bug.

We started by rebuilding the PTW FT from the AutoSVA repository [1]. Within a
few minutes1 we had generated the first batch555We call batch to the output
from prompting GPT4 into generating SVA. of 12 assertions. We generated two
more batches for a total of 36 assertions. After spending half an hour
auditing the assertions and the RTL, we found one failing assertion that, if
refined properly, could uncover the bug.

We kept generating more assertions to find whether GPT4 could generate the
correct assertions that would fail because of the RTL bug; it did after six
batches—totaling 80 assertions.3

⬇

// When in WAIT_RVALID, should remain as it was in the previous cycle if not
ptw.data_rvalid_q

asgpt__wait_rvalid_tag_valid_stable: assert property (

(ptw.state_q == WAIT_RVALID) && !ptw.data_rvalid_q |=> ptw.state_q ==
WAIT_RVALID);

Listing 4:  Assertion uncovering the PTW bug.

4 shows the failing assertion, which actually checks the correct transition
for the PTW’s FSM according to the bugfix commit.4 Once we then applied the
fix,4 the assertion proved in a few seconds of FPV tool runtime.

Assertion generation strategy: The literature on formal verification describes
different strategies to write assertions [13]. For FSMs, that strategy can be
creating assertions for each state transition. We appended this to the prompt
to instruct GPT4 to assert when FSMs change or retain states. Other strategies
could potentially be added to nudge GPT4 in a certain direction, e.g., to
generate assertions for output signals based on intermediate signals and
continue backward toward the inputs.

###  IV-B RTL Coverage of Automatically Generated SVA

We evaluated statement and toggle coverage for PTW and TLB with different sets
of assertions: the assertions from the AutoSVA evaluation [1]; one, three, and
six batches of GPT4-generated assertions; and all assertions combined.

Multi-batch improvements: We studied coverage improvement, starting with the
existing AutoSVA assertions and adding batches of AutoSVA2 outputs. For PTW,
we obtained a 1.05$\times$, 1.23$\times$, and 1.25$\times$ increase in
statement coverage with one, three, and six batches, respectively, over
AutoSVA assertions alone; and 1.24$\times$, 1.57$\times$, and 1.57$\times$
increase in toggle coverage. For TLB, the improvements are much larger:
2$\times$, 6$\times$, and 6$\times$ increase in statement coverage; and
2.12$\times$, 3.67$\times$, and 3.74$\times$ increase in toggle coverage.
These results show that (a) AutoSVA2 improves coverage significantly over
AutoSVA and (b) it is worth generating multiple batches, although we observed
little to no improvements after three batches.

Complementary assertions: The assertions generated by GPT4 and AutoSVA are
sometimes complementary, covering different parts of the design. Although for
the TLB we observed that having the AutoSVA assertions did not affect the
final coverage, for PTW, the combination of AutoSVA and GPT4 assertions had
1.59$\times$ and 1.34$\times$ more statement and toggle coverage,
respectively, over the GPT4 batches alone. This makes sense because AutoSVA
generates end-to-end properties for interface transactions, while GPT4 mostly
generates assertions for internal behavior. It is hard for GPT4 to generate
end-to-end properties because they are not directly observable from the RTL.
Even for cases like the TLB where the coverage is overlapped, it is often
easier for FPV tools to prove end-to-end assertions out of smaller assertions
[13].

##  V Use case 2: AutoSVA2 guiding RTL generation

Figure 3:  Methodology for iteratively building RTL and FT. The blue arrows
show the RTL generation flow; green arrows, the SVA flow; black arrows, the
assertion debugging flow with the human in the loop. The green boxes indicate
they are automatically generated, and the blue box, manually written.

LLMs have been previously used to generate RTL in partially incomplete modules
[14]. For the holistic task of generating RTL from scratch, we set out to
evaluate whether prompting GPT4 with SVA can help it generate better RTL.

Fig. 3 depicts the flow we devise to generate RTL from SVA (blue arrows) in
addition to the AutoSVA2 flow for generating SVA from RTL (green arrows): ①
Start with a high-level specification in English; ② The LLM generates a first
version of the RTL based on the specification, the module interface, and an
order to generate synthesizable Verilog; ③ AutoSVA2 generates an FT based on
the RTL; ④ JasperGold evaluates the FT; ⑤ The engineer audits and fixes the
SVA; ⑥ The LLM generates a new version of the RTL after appending the SVA to
the previous prompt. Steps ③ to ⑥ are then repeated until convergence: either
(a) full proof and coverage of the FT or (b) a plateau in the improvements of
the RTL and SVA.

Our experiment: We used this flow to generate a FIFO queue starting with a
specification of $\sim$50 words3). We achieved convergence by full proof after
two RTL iterations. We discuss here our observations from this experiment.

SVA from the first RTL: From the FPV report and the SVA, we observed that 5
out of 11 assertions failed due to SVA issues; we made minor fixes in three of
them (similar to T22 from Table I), a partial rewrite in another one, and
directly removed one that was not salvageable. Interestingly, we found a valid
assertion that failed due to a wrong RTL implementation and an assertion that
failed due to issues in both RTL and SVA regarding the empty/full flags of the
FIFO.3 We fixed that assertion but not the RTL since (as shown in Fig. 3) we
do not prompt the old RTL to GPT4 to generate the next RTL version.

RTL from the refined SVA: We found the RTL generated from the refined SVA to
be much better than the first version; not only did it not have the bug, but
the RTL was also more readable. The assertions for the full/empty flags were
still failing; we found via the CEXs that the write pointer was missing the
bit selection (to ignore the carry bit) while comparing it with the read
pointer. After fixing this on the RTL, the assertion kept failing. We observed
that we had wrongly specified the empty/full flags on the manually-revised
assertion from the previous step. Once we fixed that all assertions proved.

Takeaways: From this use case, we conclude that (a) this iterative methodology
is an efficient and effective way to bring up RTL and FTs from scratch, by
having the verification engineer in the loop reviewing and fixing the SVA; (b)
that errors in the RTL do not preclude GPT4 from generating correct SVA; (c)
that even if the engineer erroneously modifies the SVA, GPT4 can still
generate correct RTL.

##  VI Discussion and Conclusion

While FPV techniques have been around for decades and are acknowledged as the
most exhaustive method for DV, they are also exhausting for engineers to
apply. Prior work lightens this burden by raising the level of abstraction and
generating SVA from high-level specifications [5, 11]. However, this does not
eliminate the effort of writing specifications because, in the end, someone
must reason about the detailed behavior of the hardware. In this paper, we
evaluated whether LLMs can be the ones to reason about the hardware behavior
and generate, in our case, a low-level specification in SVA.

We found that GPT4—with careful guidance—can do that; it does not merely
translate Verilog into SVA but rather seems to capture some of the design
intent. Integrated into the AutoSVA framework, GPT4 enables the automatic
generation of FTs for RTL modules, whose completeness and correctness depend
on the complexity of the design. For small hardware components like the queue
we evaluated, it requires very little human intervention to get a complete FT.

We argue that AutoSVA2 has the potential to expand the adoption of FPV—much
needed in this era of heterogeneous hardware. Moreover, producing FTs
exclusively from RTL could pave the way for safer LLM-assisted RTL design
approaches [14]. We also believe that with a curated dataset of SVA properties
and their RTL, there is potential for fine-tuning LLMs to be more accurate or
cost-effective (with smaller models). Perhaps AutoSVA2 can be a starting point
for generating such a dataset from open-source RTL; AutoSVA2 can assist you in
generating FTs for existing RTL modules and developing new ones from scratch.
To conclude, we want to encourage the community to keep advancing and
streamlining RTL design and verification methodologies that leverage the power
of FPV. Our open-source artifacts [2] include (in addition to our experiments’
outputs): our rule set to guide GPT4 at generating SVA (SVA_GEN.v) and AutoSVA
annotations (AUTOSVA_GEN.v); our template to prompt GPT4 to generate RTL
(RTL_GEN.v); and the script that puts everything together (autosva2.py).

## References

  * [1] “AutoSVA,” github.com/PrincetonUniversity/AutoSVA.
  * [2] Anonymous, “AutoSVA2,” 2023, https://github.com/gpt4rtl/AutoSVA2.
  * [3] Cadence Design Systems Inc., “Jaspergold apps user’s guide,” 2015.
  * [4] M. Cosler, C. Hahn, D. Mendoza, F. Schmitt, and C. Trippel, “nl2spec: Interactively translating unstructured natural language to temporal logics with large language models,” _arXiv preprint arXiv:2303.04864_ , 2023.
  * [5] B.-Y. Huang, H. Zhang, P. Subramanyan, Y. Vizel, A. Gupta, and S. Malik, “Instruction-level abstraction (ILA): A uniform specification for system-on-chip verification,” _ACM Transactions on Design Automation of Electronic Systems (TODAES)_ , vol. 24, no. 1, pp. 1–24, 2018.
  * [6] _IEEE Standard for SystemVerilog–Unified Hardware Design, Specification, and Verification Language_ , IEEE 1800-2012 Std., 2013.
  * [7] R. Kande, H. Pearce, B. Tan, B. Dolan-Gavitt, S. Thakur, R. Karri, and J. Rajendran, “LLM-assisted generation of hardware assertions,” _arXiv preprint arXiv:2306.14027_ , 2023.
  * [8] Y. A. Manerkar, D. Lustig, M. Martonosi, and M. Pellauer, “RTLCheck: Verifying the memory consistency of RTL designs,” in _2017 50th Annual IEEE/ACM MICRO_ , 2017, pp. 463–476.
  * [9] OpenAI, “GPT4,” https://openai.com/gpt-4.
  * [10] OpenHW Group, “CVA6,” https://github.com/openhwgroup/cva6.
  * [11] M. Orenes-Vera, A. Manocha, D. Wentzlaff, and M. Martonosi, “AutoSVA: Democratizing Formal Verification of RTL Module Interactions,” in _ACM/IEEE Design Automation Conference (DAC)_ , 2021, pp. 535–540.
  * [12] M. Orenes-Vera, H. Yun, N. Wistoff, G. Heiser, L. Benini, D. Wentzlaff, and M. Martonosi, “AutoCC: Automatic discovery of covert channels in time-shared hardware,” in _56th IEEE/ACM MICRO_ , 2023.
  * [13] E. Seligman, T. Schubert, and M. A. K. Kumar, _Formal verification: an essential toolkit for modern VLSI design_. Morgan Kaufmann, 2015.
  * [14] S. Thakur, B. Ahmad, Z. Fan, H. Pearce, B. Tan, R. Karri, B. Dolan-Gavitt, and S. Garg, “Benchmarking large language models for automated verilog rtl code generation,” in _DATE_. IEEE, 2023, pp. 1–6.
  * [15] C. Wolf, “SymbiYosys,” https://github.com/YosysHQ/SymbiYosys.


# Entanglement and nonlocality of one- and two-mode combination squeezed
state††thanks: Work supported by a grant from the Key Programs Foundation of
Ministry of Education of China (No. 210115) and the Research Foundation of the
Education Department of Jiangxi Province of China (No. GJJ10097).

Li-yun Hu1, Xue-xiang Xu1,2, Qin Guo1, and Hong-yi Fan2
1College of Physics & Communication Electronics, Jiangxi Normal University,
Nanchang 330022, China
2Department of Physics, Shanghai Jiao Tong University, Shanghai 200030, China
Corresponding author. E-mail<EMAIL_ADDRESS>
###### Abstract

We investigate the entanglement and nonlocality properties of one- and two-
mode combination squeezed vacuum state (OTCSS, with two-parameter $\lambda$
and $\gamma$) by analyzing the logarithmic negativity and the Bell’s
inequality. It is found that this state exhibits larger entanglement than that
of the usual two-mode squeezed vacuum state (TSVS), and that in a certain
regime of $\lambda$, the violation of Bell’s inequality becomes more obvious,
which indicates that the nonlocality of OTCSS can be stronger than that of
TSVS. As an application of OTCSS, the quantum teleportaion is examined, which
shows that there is a region spanned by $\lambda$ and $\gamma$in which the
fidelity of OTCSS channel is larger than that of TSVS.

Keywords: Entanglement, nonlocality, IWOP technique, teleportation

PACS number(s): 42.50.Dv, 03.65.Wj, 03.67.Mn

##  1 Introduction

Entanglement between quantum systems plays a key role in quantum information
processing, such as quantum teleportation, dense coding, and quantum cloning.
In recent years, various entangled states have brought considerable attention
and interests of physicists because of their potential uses in quantum
communication [1, 2]. For instance, the two-mode squeezed state is a typical
entangled state of continuous variable and exhibits quantum entanglement
between the idle-mode and the signal-mode in a frequency domain manifestly.
Theoretically, the two-mode squeezed state is constructed by the two-mode
squeezing operator
$S=\exp[\lambda(a_{1}a_{2}-a_{1}^{\dagger}a_{2}^{\dagger})]$ [3, 4, 5] acting
on the two-mode vacuum state $\left|00\right\rangle$,

$S\left|00\right\rangle=\text{sech}\lambda\exp\left[-a_{1}^{{}^{\dagger}}a_{2}^{{}^{\dagger}}\tanh\lambda\right]\left|00\right\rangle,$
(1)

where $\lambda$ is a squeezing parameter, the disentangling of $S$ can be
obtained by using SU(1,1) Lie algebra,
$[a_{1}a_{2},a_{1}^{\dagger}a_{2}^{\dagger}]=a_{1}^{\dagger}a_{1}+a_{2}^{\dagger}a_{2}+1,$
or by using the entangled state representation $\left|\eta\right\rangle$ [6,
7, 8], which was constructed according to the idea of Einstein, Podolsky and
Rosen in their argument that quantum mechanics is incomplete [9].

Using the relation between Bosonic operators and the coordinate $Q_{i},$
momentum $P_{i},$ $Q_{i}=(a_{i}+a_{i}^{\dagger})/\sqrt{2},\
P_{i}=(a_{i}-a_{i}^{\dagger})/(\sqrt{2}\mathtt{i}),$ and introducing the two-
mode quadrature operators of light field, $x_{1}=(Q_{1}+Q_{2})/2,$
$x_{2}=(P_{1}+P_{2})/2,$ the variances of $x_{1}$ and $x_{2}$ in the state
$S\left|00\right\rangle$ are in the standard form

$\left\langle
00\right|S^{\dagger}x_{2}^{2}S\left|00\right\rangle=\frac{1}{4}e^{-2\lambda},\text{
}\left\langle
00\right|S^{\dagger}x_{1}^{2}S\left|00\right\rangle=\frac{1}{4}e^{2\lambda},$
(2)

thus we get the standard squeezing for the two quadrature:
$x_{1}\rightarrow\frac{1}{2}e^{\lambda}x_{1},$
$x_{2}\rightarrow\frac{1}{2}e^{-\lambda}x_{2}$. On the other hand, the two-
mode squeezing operator can also be recast into the form
$S=\exp\left[\mathtt{i}\lambda\left(Q_{1}P_{2}+Q_{2}P_{1}\right)\right].$ Then
some interesting questions naturally rise: what is the property of the
following operator

$V=\exp\left[-\mathtt{i}\left(\lambda_{1}Q_{1}P_{2}+\lambda_{2}Q_{2}P_{1}\right)\right],$
(3)

with two parameters $\lambda_{1}=\lambda e^{\gamma},\lambda_{2}=\lambda
e^{-\gamma},\lambda>0$? What is the normally ordered expansion of $V$ and what
is the state $V\left|00\right\rangle$? What are the entanglement and
nonlocality properties of $V\left|00\right\rangle?$ When $\gamma=0,$ Eq.(3)
just reduces to the usual two-mode squeezing operator $S$. Thus we can
consider $V$ as a generalized two-mode squeezing operator and
$V\left|00\right\rangle$ as one- and two-mode combination squeezed vacuum
state (OTCSS).

In this paper, we investigate entanglement properties and quantum nonlocality
of $V\left|00\right\rangle$ in terms of logarithmic negativity and the Bell’s
inequality, respectively. Subsequently, we consider its application in the
field of quantum teleportation by using the characteristic-function formula.
It is shown that this state exhibits larger entanglement than that of the
usual two-mode squeezed vacuum state (TSVS); and in a certain smaller regime
of $\lambda$, that the nonlocality of this state can be stronger than that of
TSVS due to the presence of $\gamma.$ In addition, application to quantum
teleportation with OTCSS is also considered, which shows that there is a
region spanned by $\lambda$ and $\gamma$ in which the fidelity of OTCSS
channel is larger than that of TSVS.

Our paper is arranged as follows. In section 2, we derive the normal ordering
form of one- and two-mode combination squeezing operator by using the
technique of integration within an ordered product (IWOP) of operators. In
section 3, using the Weyl ordering form of single-mode Wigner operator and the
order-invariance of Weyl ordered operators under similar transformations, we
derive analytically the Wigner function of $V\left|00\right\rangle$. Sections
4 and 5 are devoted to investigating the entanglement properties and the
nonlocal properties OTCSS by using the Bell’s inequality and the logarithmic
negativity, respectively. An application to quantum teleportation with OTCSS
is involved in section 6. We end with the main conclusions of our work.

##  2 The normal ordering form of $V$ and fluctuations in
$V\left|00\right\rangle$

In order to know $V\left|00\right\rangle,$ we need to derive the normal
ordering form of the unitary operator $V$ by virtue of the IWOP technique [10,
11, 12]. Using the Baker-Hausdorff formula,

$e^{A}Be^{-A}=B+\left[A,B\right]+\frac{1}{2!}\left[A,\left[A,B\right]\right]+\frac{1}{3!}\left[A,\left[A,\left[A,B\right]\right]\right]+\cdots,$
(4)

and noticing that

$\displaystyle
i\left[\lambda_{1}Q_{1}P_{2}+\lambda_{2}Q_{2}P_{1},Q_{1}\right]$
$\displaystyle=\lambda_{2}Q_{2},\text{ }$ (5) $\displaystyle
i\left[\lambda_{1}Q_{1}P_{2}+\lambda_{2}Q_{2}P_{1},Q_{2}\right]$
$\displaystyle=\lambda_{1}Q_{1},$ (6) $\displaystyle
i\left[\lambda_{1}Q_{1}P_{2}+\lambda_{2}Q_{2}P_{1},P_{1}\right]$
$\displaystyle=-\lambda_{1}P_{2},$ (7) $\displaystyle
i\left[\lambda_{1}Q_{1}P_{2}+\lambda_{2}Q_{2}P_{1},P_{2}\right]$
$\displaystyle=-\lambda_{2}P_{1},$ (8)

we have

$\displaystyle V^{-1}Q_{1}V$
$\displaystyle=Q_{1}\cosh\lambda+Q_{2}e^{-\gamma}\sinh\lambda,$ (9)
$\displaystyle V^{-1}Q_{2}V$
$\displaystyle=Q_{2}\cosh\lambda+Q_{1}e^{\gamma}\sinh\lambda,$ (10)
$\displaystyle V^{-1}P_{1}V$ $\displaystyle=P_{1}\cosh\lambda-
P_{2}e^{\gamma}\sinh\lambda,$ (11) $\displaystyle V^{-1}P_{2}V$
$\displaystyle=P_{2}\cosh\lambda-P_{1}e^{-\gamma}\sinh\lambda.$ (12)

Thus, in order to keep the eigenvalues invariant under the $V$ transformation,
i..e.,

$V^{-1}Q_{k}V\left|q_{1}q_{2}\right\rangle^{\prime}=q_{k}\left|q_{1}q_{2}\right\rangle^{\prime},(k=1,2),$
(13)

the base vector must be changed to

$\left|q_{1}q_{2}\right\rangle^{\prime}=V^{-1}\left|q_{1}q_{2}\right\rangle=\left|\Lambda^{-1}\left(\begin{array}[c]{c}q_{1}\\\
q_{2}\end{array}\right)\right\rangle,\Lambda=\left(\begin{array}[c]{cc}\cosh\lambda&e^{-\gamma}\sinh\lambda\\\
e^{\gamma}\sinh\lambda&\cosh\lambda\end{array}\right),$ (14)

where
$\left|q_{1}q_{2}\right\rangle=\left|q_{1}\right\rangle\otimes\left|q_{2}\right\rangle$,
and $\left|q_{k}\right\rangle$ is the coordinate eigenstate,

$\left|q_{k}\right\rangle=\pi^{-1/4}\exp[-\frac{1}{2}q^{2}+\sqrt{2}qa^{{\dagger}}-\frac{1}{2}a^{{\dagger}2}]\left|0\right\rangle.$
(15)

Using the completeness raltion
$\int_{-\infty}^{\infty}dq_{1}dq_{2}\left|q_{1},q_{2}\right\rangle\left\langle
q_{1},q_{2}\right|=1$, we have

$V^{-1}=\int_{-\infty}^{\infty}dq_{1}dq_{2}\left|\Lambda^{-1}\left(\begin{array}[c]{c}q_{1}\\\
q_{2}\end{array}\right)\right\rangle\left\langle q_{1},q_{2}\right|,$ (16)

which leads to

$V=\int_{-\infty}^{\infty}dq_{1}dq_{2}\left|\Lambda\left(\begin{array}[c]{c}q_{1}\\\
q_{2}\end{array}\right)\right\rangle\left\langle q_{1},q_{2}\right|.$ (17)

Actually, one can check (17) by $V^{-1}V=VV^{-1}=1.$ Further using the vacuum
projector $\left|00\right\rangle\left\langle
00\right|=\colon\exp[-a^{{\dagger}}a-b^{{\dagger}}b]\colon(\colon\colon$
denoting normal ordering$)$, as well as the IWOP technique, we can put $V$
into the normal ordering form [13],

$\displaystyle V$
$\displaystyle=\frac{2}{\sqrt{L}}\exp\left\\{\frac{1}{L}\left[\left(b^{{\dagger}2}-a^{{\dagger}2}\right)\sinh^{2}\lambda\sinh
2\gamma+2a^{{\dagger}}b^{{\dagger}}\sinh 2\lambda\cosh\gamma\right]\right\\}$
$\displaystyle\colon\exp\left\\{\frac{4}{L}\left[\left(a^{{\dagger}}a+b^{{\dagger}}b\right)\cosh\lambda+\left(b^{{\dagger}}a-a^{{\dagger}}b\right)\sinh\lambda\sinh\gamma\right]-a^{{\dagger}}a-b^{{\dagger}}b\right\\}\colon$
$\displaystyle\exp\left\\{\frac{1}{L}\left[\left(b^{2}-a^{2}\right)\sinh^{2}\lambda\sinh
2\gamma-2a^{{\dagger}}b^{{\dagger}}\sinh 2\lambda\cosh\gamma\right]\right\\},$
(18)

where $L=4\left(1+\sinh^{2}\gamma\tanh^{2}\lambda\right)\cosh^{2}\lambda.$ Eq.
(18) is just the normal ordering form of $V$. It is obviously to see that when
$\gamma=0$, Eq.(18) just reduces to the usual two-mode squeezing operator.
Operating $V$ on the two-mode vacuum state $\left|00\right\rangle$, we obtain
the squeezed vacuum state,

$V\left|00\right\rangle=\frac{2}{\sqrt{L}}\exp\left\\{\frac{1}{L}\left[\left(b^{{\dagger}2}-a^{{\dagger}2}\right)\sinh^{2}\lambda\sinh
2\gamma+2a^{{\dagger}}b^{{\dagger}}\sinh
2\lambda\cosh\gamma\right]\right\\}\left|00\right\rangle.$ (19)

On the other hand, by using the transformations Eqs.(9)-(12), one can derive
the variances of $x_{1}$ and $x_{2}$ in the state $V\left|00\right\rangle$
[13]

$\displaystyle\left\langle\left(\Delta x_{1}\right)^{2}\right\rangle$
$\displaystyle=\frac{1}{4}\left(\cosh
2\lambda+2\sinh^{2}\lambda\sinh^{2}\gamma+\sinh 2\lambda\cosh\gamma\right),$
(20) $\displaystyle\left\langle\left(\Delta x_{2}\right)^{2}\right\rangle$
$\displaystyle=\frac{1}{4}\left(\cosh
2\lambda+2\sinh^{2}\lambda\sinh^{2}\gamma-\sinh 2\lambda\cosh\gamma\right),$
(21)

which indicate that the variances are not only dependent on parameter
$\lambda$, but also on parameter $\gamma.$ When $\gamma=0,$ Eqs.(20) and (21)
reduce to $\left\langle\left(\Delta
x_{1}\right)^{2}\right\rangle=\frac{1}{4}e^{2\lambda},$ and
$\left\langle\left(\Delta
x_{2}\right)^{2}\right\rangle=\frac{1}{4}e^{-2\lambda},$ corresponding to the
usual TSVS. In particular, by modulating the two parameters ($\lambda$ and
$\gamma$), we can realize that

$\left\langle\left(\Delta
x_{1}\right)^{2}\right\rangle>\frac{1}{4}e^{2\lambda},\left\langle\left(\Delta
x_{2}\right)^{2}\right\rangle<\frac{1}{4}e^{-2\lambda},$ (22)

whose condition is given by

$0<\tanh\lambda<\frac{1}{1+\cosh\gamma},\lambda>0,$ (23)

which mean that the OTCSS may exhibit stronger squeezing in one quadrature
than that of the TSVS while exhibiting weaker squeezing in another quadrature
when the condition (23) satisfied. Then, can the OTCSS exhibits stronger
nonlocality or more observable violation of Bell’s inequality? In the
following, we pay our attention to these two aspects.

##  3 Wigner function of $V\left|00\right\rangle$

Wigner distribution functions [14, 15, 16] of quantum states are widely
studied in quantum statistics and quantum optics. Now we derive the expression
of the Wigner function of $V\left|00\right\rangle.$ Here we take a new method
to do it. Recalling that in Ref.[17, 18, 19] we have introduced the Weyl
ordering form of single-mode Wigner operator
$\Delta_{1}\left(q_{1},p_{1}\right)$,

$\Delta_{1}\left(q_{1},p_{1}\right)=\genfrac{}{}{0.0pt}{}{:}{:}\delta\left(q_{1}-Q_{1}\right)\delta\left(p_{1}-P_{1}\right)\genfrac{}{}{0.0pt}{}{:}{:},$
(24)

its normal ordering form is

$\Delta_{1}\left(q_{1},p_{1}\right)=\frac{1}{\pi}\colon\exp\left[-\left(q_{1}-Q_{1}\right)^{2}-\left(p_{1}-P_{1}\right)^{2}\right]\colon,$
(25)

where the symbols $\colon\colon$ and
$\genfrac{}{}{0.0pt}{}{:}{:}\genfrac{}{}{0.0pt}{}{:}{:}$ denote the normal
ordering and the Weyl ordering, respectively. Note that the order of Bose
operators $a_{1}$ and $a_{1}^{\dagger}$ within a normally ordered product and
a Weyl ordered product can be permuted. That is to say, even though
$[a_{1},a_{1}^{\dagger}]=1$, we can have $\colon
a_{1}a_{1}^{\dagger}\colon=\colon a_{1}^{\dagger}a_{1}\colon$
and$\genfrac{}{}{0.0pt}{}{:}{:}a_{1}a_{1}^{\dagger}\genfrac{}{}{0.0pt}{}{:}{:}=\genfrac{}{}{0.0pt}{}{:}{:}a_{1}^{\dagger}a_{1}\genfrac{}{}{0.0pt}{}{:}{:}.$

For one- and two-mode combination squeezed vacuum state
$V\left|00\right\rangle$, its Wigner function is given by

$W\left(q_{1},p_{1};q_{2},p_{2}\right)=\mathtt{tr}\left[V\left|00\right\rangle\left\langle
00\right|V^{-1}\Delta_{1}\left(q_{1},p_{1}\right)\Delta_{2}\left(q_{2},p_{2}\right)\right]=\left\langle
00\right|U\left|00\right\rangle,$ (26)

where
$U=V^{-1}\Delta_{1}\left(q_{1},p_{1}\right)\Delta_{2}\left(q_{2},p_{2}\right)V.$
Further using Eq.(24), noticing that the Weyl ordering has a remarkable
property, i.e., the order-invariance of Weyl ordered operators under similar
transformations [17, 18, 19], which means

$V^{-1}\genfrac{}{}{0.0pt}{}{:}{:}\left(\circ\circ\circ\right)\genfrac{}{}{0.0pt}{}{:}{:}V=\genfrac{}{}{0.0pt}{}{:}{:}V^{-1}\left(\circ\circ\circ\right)V\genfrac{}{}{0.0pt}{}{:}{:},$
(27)

as if the “fence” $\genfrac{}{}{0.0pt}{}{:}{:}\genfrac{}{}{0.0pt}{}{:}{:}$did
not exist, thus $U$ can be cast into the following form (see appendix A),

$\displaystyle U$
$\displaystyle=V^{-1}\genfrac{}{}{0.0pt}{}{:}{:}\delta\left(q_{1}-Q_{1}\right)\delta\left(p_{1}-P_{1}\right)\delta\left(q_{2}-Q_{2}\right)\delta\left(p_{2}-P_{2}\right)\genfrac{}{}{0.0pt}{}{:}{:}V$
$\displaystyle=\Delta_{1}\left(q_{1}\cosh\lambda-
q_{2}e^{-\gamma}\sinh\lambda,p_{1}\cosh\lambda+p_{2}e^{\gamma}\sinh\lambda\right)$
$\displaystyle\times\Delta_{2}\left(q_{2}\cosh\lambda-
q_{1}e^{\gamma}\sinh\lambda,p_{2}\cosh\lambda+p_{1}e^{-\gamma}\sinh\lambda\right).$
(28)

So the Wigner function of $V\left|00\right\rangle$ is given by

$W\left(q_{1},p_{1};q_{2},p_{2}\right)=\frac{1}{\pi^{2}}\exp\left\\{-m_{1}\left(q_{1}^{2}+p_{2}^{2}\right)\allowbreak-
m_{2}\left(p_{1}^{2}+q_{2}^{2}\right)+2\left(q_{1}q_{2}\allowbreak-
p_{1}p_{2}\right)m_{3}\right\\},$ (29)

where

$m_{1}=\cosh^{2}\lambda+e^{2\gamma}\sinh^{2}\lambda,\text{
}m_{2}=\cosh^{2}\lambda+e^{-2\gamma}\allowbreak\sinh^{2}\lambda,\text{
}m_{3}=\cosh\gamma\sinh 2\lambda.$

In particular, when $\gamma=0$, Eq.(29) becomes

$\displaystyle W\left(q_{1},p_{1};q_{2},p_{2}\right)$
$\displaystyle=\frac{1}{\pi^{2}}\exp\left\\{-\left(p_{1}^{2}+p_{2}^{2}+q_{1}^{2}+q_{2}^{2}\right)\cosh
2\lambda\allowbreak\right.$
$\displaystyle\left.+2\left(q_{1}q_{2}-p_{1}p_{2}\right)\sinh
2\lambda\right\\},$ (30)

which is just the Wigner function of the usual TSVS.

##  4 Entanglement properties of $V\left|00\right\rangle$

In this section, we consider the entanglement properties of
$V\left|00\right\rangle$. It is well known that a two-mode Gaussian state can
be completely characterized by its first and second statistical moments and
the covariance matrix of elements $\sigma$. In general, the first statistical
moments can be adjusted by local displacements without affecting entanglement,
thus they they will can be set to be zero without loss of generality and the
behavior of the covariance matrix $\sigma$ is all important for the study of
entanglement. There are several quantitative measurements of quantum
entanglement proposed [20, 21, 22]. For a two-mode Gaussian state, the
entanglement is best characterized by the logarithmic negativity
$E_{\mathcal{N}}$, a quantity evaluated in terms of the symplectic eigenvalues
of $\sigma$ [23, 24].

In order to evaluate the entanglement of $V\left|00\right\rangle,$ we reform
Eq.(29) as follows in terms of phase space quadrature variables,

$W\left(q_{1},p_{1};q_{2},p_{2}\right)=\frac{1}{\pi^{2}}\exp\left[-\frac{1}{2}\left(\begin{array}[c]{cccc}q_{1}&p_{1}&q_{2}&p_{2}\end{array}\right)\sigma^{-1}\left(\begin{array}[c]{cccc}q_{1}&p_{1}&q_{2}&p_{2}\end{array}\right)^{T}\right],$
(31)

where the covariance matrix $\sigma$ of this OTCSS is [25]

$\sigma=\left(\begin{array}[c]{cc}u&w\\\ w^{T}&v\end{array}\right),\text{
}u=\frac{1}{2}\left(\begin{array}[c]{cc}m_{2}&0\\\
0&m_{1}\end{array}\right),v=\frac{1}{2}\left(\begin{array}[c]{cc}m_{1}&0\\\
0&m_{2}\end{array}\right),w=\frac{1}{2}\left(\begin{array}[c]{cc}m_{3}&0\\\
0&-m_{3}\end{array}\right).$ (32)

In particular, when $\gamma=0$, $m_{1}=m_{2}=\cosh 2\lambda,$ $m_{3}=\sinh
2\lambda$, Eq.(32) just reduces to the so-called standard form of covariance
matrix for TSVS [24].

The condition for entanglement of a Gaussian state is derived from the
partially transposed density matrix (PPT criterion) [24], according to the
smallest symplectic eigenvalue $\tilde{n}_{s}$ of the partially transposed
state, $\tilde{n}_{s}<\frac{1}{2},$ i.e., $\tilde{n}_{s}\geqslant\frac{1}{2}$
means the a two-mode Gaussian state is separable, where $\tilde{n}_{s}$ is
defined as

$\tilde{n}_{s}=\min\left[\tilde{n}_{+},\tilde{n}_{-}\right],$ (33)

and $\tilde{n}_{\pm}\ $is given by [26]

$\tilde{n}_{\pm}=\sqrt{\frac{\tilde{\Delta}\left(\sigma\right)\pm(\tilde{\Delta}\left(\sigma\right)^{2}-4\det\sigma)^{1/2}}{2}},$
(34)

where
$\tilde{\Delta}\left(\sigma\right)=\Delta\left(\tilde{\sigma}\right)=\det
u+\det v-2\det w.$

Using Eqs.(32)-(34), the corresponding sympletic eigenvalues $\tilde{n}_{\pm}$
are then given by

$\tilde{n}_{\pm}=\frac{1}{2}\left(\sqrt{m_{1}m_{2}}\pm m_{3}\right).$ (35)

One the other hand, the corresponding quantification of entanglement is given
by the logarithmic negativity $E_{\mathcal{N}}$ defined as [20, 26, 27],

$E_{\mathcal{N}}=\max\left[0,-\ln 2\tilde{n}_{s}\right].$ (36)

From Eqs.(32), (35) and (36), one can clearly see that the logarithmic
negativity $E_{\mathcal{N}}$ is dependent on $\lambda$ and $\gamma.$ In figure
1, we plot the logarithmic negativity $E_{\mathcal{N}}$ as a function of
parameters $\lambda$ and $\gamma$. From Fig.1, we clearly see a new feature,
i.e., in presence of parameter $\gamma$, the logarithmic negativity becomes
larger than that of tha usual squeezed state ($\gamma=0$).

Figure 1: (Color online) The logarithmic negativity $E_{\mathcal{N}}$as a
function of parameters $\lambda$and $\gamma$.

##  5 Violations of Bell’s inequality for $V\left|00\right\rangle$

We now turn our attention to the nonlocal properties of
$V\left|00\right\rangle$ in terms of the Bell’s inequality. For a two-mode
continuous variable system, the Bell’s inequality is given, using correlations
between parity measurement, by

$\left|\mathcal{B}\right|\equiv\left|\left\langle\hat{\Pi}^{ab}\left(\alpha^{\prime},\beta^{\prime}\right)+\hat{\Pi}^{ab}\left(\alpha,\beta^{\prime}\right)+\hat{\Pi}^{ab}\left(\alpha^{\prime},\beta\right)-\hat{\Pi}^{ab}\left(\alpha,\beta\right)\right\rangle\right|\leqslant
2,$ (37)

where $B$ is the Bell function, and the superscripts $a$ and $b$ denote the
modes and $\hat{\Pi}^{ab}\left(\alpha,\beta\right)$ is the displaced parity
operator (Wigner operator)[28] defined as

$\displaystyle\hat{\Pi}^{ab}\left(\alpha,\beta\right)$
$\displaystyle\equiv\hat{\Pi}^{a}\left(\alpha\right)\hat{\Pi}^{b}\left(\beta\right)=D\left(\alpha\right)D\left(\beta\right)(-1)^{a^{{\dagger}}a+b^{{\dagger}}b}D^{{\dagger}}\left(\beta\right)D^{{\dagger}}\left(\alpha\right)$
$\displaystyle=\pi^{2}\Delta_{a}\left(\alpha\right)\Delta_{b}\left(\beta\right),$
(38)

where $\alpha=(q_{1}+ip_{1})/\sqrt{2},\beta=(q_{2}+ip_{2})/\sqrt{2}.$ The
expectation value of this displaced parity operator is just proportional to
the two-mode Wigner function, i.e.,

$\Pi\left(\alpha,\beta\right)=\mathtt{tr}\left[\rho\hat{\Pi}^{ab}\left(\alpha,\beta\right)\right]=\pi^{2}W\left(\alpha,\beta\right),$
(39)

which shows that the connection between this displaced parity operator and
Wigner function provides an equivalent definition [29].

The Bell function is measured for any of four combinations of
$\alpha=0,\sqrt{J}e^{i\varphi}$ and $\beta=0,\sqrt{J}e^{i\theta}$, where
$J(=\left|\alpha\right|^{2}=\left|\beta\right|^{2})$ is a positive constant
characterizing the magnitude of the displacement. From these quantities we
construct the combination [30]

$\mathcal{B}\equiv\pi^{2}\left[W\left(0,0\right)+W\left(\sqrt{J}e^{i\varphi},0\right)+W\left(0,\sqrt{J}e^{i\theta}\right)-W\left(\sqrt{J}e^{i\varphi},\sqrt{J}e^{i\theta}\right)\right].$
(40)

In particular, when $\varphi=0$, $\theta=\pi,$ Eq.(40) just reduces to Eq.(7)
in Ref.[28]. Then we can test Bell’s inequality
$-2\leqslant\mathcal{B}\leqslant 2$ by means of the two-mode Wigner function
measurement. Recently, a generalized quasiprobability function is proposed to
test quantum nonlocality [31], which includes two-type of Bell-inequality by
using the Wigner function [32] and the $Q-$function [30] as its limiting
cases.

By noticing that
$\alpha=(q_{1}+ip_{1})/\sqrt{2},\beta=(q_{2}+ip_{2})/\sqrt{2}$, and
$\left(\begin{array}[c]{cccc}q_{1}&p_{1}&q_{2}&p_{2}\end{array}\right)N^{-1}=\left(\begin{array}[c]{cccc}\alpha^{\ast}&\alpha&\beta^{\ast}&\beta\end{array}\right),N=\frac{1}{\sqrt{2}}\left(\begin{array}[c]{cccc}1&i&0&0\\\
1&-i&0&0\\\ 0&0&1&i\\\ 0&0&1&-i\end{array}\right),$ we can put Eq.(31) into
another form

$W\left(\alpha;\beta\right)=\frac{1}{\pi^{2}}\exp\left[-\frac{1}{2}\left(\begin{array}[c]{cccc}\alpha^{\ast}&\alpha&\beta^{\ast}&\beta\end{array}\right)M\left(\begin{array}[c]{cccc}\alpha^{\ast}&\alpha&\beta^{\ast}&\beta\end{array}\right)^{T}\right],$
(41)

where $\bar{M}$ is a $4\times 4$ Hermitian matrix

$M=\left(\begin{array}[c]{cccc}m_{1}-m_{2}&m_{1}+m_{2}&-2m_{3}&0\\\
m_{1}+m_{2}&m_{1}-m_{2}&0&-2m_{3}\\\ -2m_{3}&0&m_{2}-m_{1}&m_{1}+m_{2}\\\
0&-2m_{3}&m_{1}+m_{2}&m_{2}-m_{1}\end{array}\right).$ (42)

Substituting Eq.(41) into Eq.(40) we have

$\displaystyle\mathcal{B}$
$\displaystyle=1+\exp\left[-2J\cosh^{2}\lambda-2J\left(e^{2\gamma}\cos^{2}\varphi+e^{-2\gamma}\sin^{2}\varphi\allowbreak\right)\sinh^{2}\lambda\right]$
$\displaystyle\text{ \ \ \ \
}+\exp\left[-2J\cosh^{2}\lambda-2J\left(e^{2\gamma}\sin^{2}\theta+e^{-2\gamma}\cos^{2}\theta\allowbreak\right)\sinh^{2}\lambda\right]$
$\displaystyle\text{ \ \ \ \
}-\exp\left\\{-4J\cosh^{2}\lambda-2J\left(\cos^{2}\varphi+\sin^{2}\theta\right)e^{2\gamma}\sinh^{2}\lambda\right.$
$\displaystyle\ \ \ \ \ \ \
\left.-2J\left(\sin^{2}\varphi+\cos^{2}\theta\right)e^{-2\gamma}\allowbreak\sinh^{2}\lambda+4J\cos\left(\theta+\varphi\right)\cosh\gamma\sinh
2\lambda\right\\},$ (43)

Thus we can say that $V\left|00\right\rangle$ is quantum mechanically nonlocal
as $\left|\mathcal{B}\right|>2,$ and the nonlocality is stronger with the
increase of $\left|\mathcal{B}\right|$. From Eq.(43) one can see that the
degree of nonlocality not only depends on the coherent amplitude $J$, on the
phases $\theta$ and $\varphi$, but also on the parameter $\gamma$. In
particular, when $\varphi=0$, $\theta=\pi,$ Eq.(43) just reduces to

$\displaystyle\mathcal{B}$
$\displaystyle=1+\exp\left[-2J\left(\cosh^{2}\lambda+e^{2\gamma}\sinh^{2}\lambda\right)\right]$
$\displaystyle\text{ \ \ \ \
}+\exp\left[-2J\left(\cosh^{2}\lambda+e^{-2\gamma}\sinh^{2}\lambda\right)\right]$
$\displaystyle\text{ \ \ \ \ }-\exp\left[-4J\left(\cosh^{2}\lambda+\cosh
2\gamma\sinh^{2}\lambda\right)-4J\allowbreak\cosh\gamma\sinh 2\lambda\right],$
(44)

which further becomes Eq.(7) in Ref.[28] with $\gamma=0$.

Figure 2: (Color online) Plot of the Bell function $\mathcal{B}$as a function
of parameters $\lambda$and $J$, for $\gamma=0,\theta=\pi,\varphi=0$. Only
values exceeding the bound imposed by local theories are shown.

In figure 2, we plot Bell function in the space spanned by parameters $J$ and
$\lambda$ with $\gamma=0$ (corresponding to the usual squeezed vacuum state).
From Fig. 2, one can clearly see that the result (43) violates the upper bound
imposed by local theories. With the increase of $\lambda$, the violation of
Bell’s inequality becomes more observable for smaller $J$.

Figure 3: (Color online) Plot of the Bell function $\mathcal{B}$as a function
of parameters $\lambda$ and $\gamma,$for given
$\left|\alpha\right|=\left|\beta\right|=0.05$and $\theta=\pi,\varphi=0.$Only
values exceeding the bound imposed by local theories are shown. Figure 4:
(Color online) Plot of the Bell function $\mathcal{B}$as a function of
parameters $J$ and $\gamma$,for given $\theta=\pi,\varphi=0,$and
$\lambda=0.1$. Only values exceeding the bound imposed by local theories are
shown.

As depicted in Fig. 3, the Bell function also violates the upper bound in the
space spanned by parameters $\gamma$ and $\lambda$ with given $\alpha,\beta$
values. From Fig.3, one can see that for a given small $\gamma,$ the violation
of Bell’s inequality becomes more observable with the increase of $\lambda$;
while for a large $\gamma$, the Bell function is not always monotone for an
increasing $\lambda$; In a certain smaller regime of $\lambda$, it is found
that the violation of Bell’s inequality becomes more observable with
increasing $\gamma$, which indicates that the nonlocality of
$V\left|00\right\rangle$ is enhanced due to the presence of $\gamma$ (also see
Fig.4). In addition, for a certain larger regime of $\lambda$, the maximum
value of $\mathcal{B}$ becomes smaller with the increase of $\gamma$.

On the other hand, from the expression we see that the degree of nonlocality
depends on the coherent amplitude $J$, and on the squeezed parameters
$\lambda$ and $\gamma$, and on the phases $\varphi$, $\theta$. We have plotted
the Bell function $\mathcal{B}$ as a function of the phases $\varphi$,
$\theta$ and with fixed $J=0.01$ and several different $\lambda,\gamma$, as
shown in Fig. 5. One can clearly see from Fig. 5 that $\mathcal{B}$ is always
greater than zero and for a smaller $\lambda$, the variable $\mathcal{B}$
reaches its maxmum value for $\varphi=0,\theta=\pi$ or $\varphi=\pi,\theta=0$
(see Fig.5(a),(b)); while for a larger $\lambda$, the phases $\varphi$,
$\theta$ corresponding to the maxmum value of $\mathcal{B}$ are different from
those above and vary as $\gamma$ parameter.

Figure 5: (Color online) Plot of the Bell function $\mathcal{B}$ as a function
of parameters $\theta$ and $\varphi$,for given $J=0.01,$and (a) $\lambda=0.5$,
$\gamma=1;$(b) $\lambda=0.5$, $\gamma=2;$(c) $\lambda=1$, $\gamma=1;$(a)
$\lambda=1$, $\gamma=2.$

##  6 Application to quantum teleportation with $V\left|00\right\rangle$

In quantum teleportation (QT), an unknown state is transmitted from a sender
(Alice) to a receiver (Bob) via a quantum channel with the aid of some
classical information. This process may be regarded as sending and extracting
quantum information via the quantum channel. QT was firstly proposed by
Barnnett et al in the discrete variable regime [33] followed by experimental
demonstration [34, 35]. For the continuous variables (CVs) case, the
theoretical analysis of teleportation was firstly made by Vaidman [36]. The
role of teleportation in the CV quantum information is analyzed in the review
Ref.[37].

Recently, a CV teleportation protocol has been given in terms of the
characteristic functions (CFs) of the quantum states involved (input, source
and teleported (output) states) [38]. By using the Weyl expansion of density
operator, it is shown that the CF $\chi_{out}\left(\beta\right)$ of the output
state has a remarkably factorized form

$\chi_{out}\left(\beta\right)=\chi_{in}\left(\beta\right)\chi_{E}\left(\beta^{\ast},\beta\right),$
(45)

where $\chi_{in}\left(\beta\right)$ and
$\chi_{E}\left(\beta^{\ast},\beta\right)$ are the CFs of the input state and
the entangled source, respectively,
$\chi_{in}\left(\alpha_{1}\right)=$tr$\left[D_{1}\left(\alpha_{1}\right)\rho\right]$
and
$\chi_{E}\left(\alpha_{1},\alpha_{2}\right)=$tr$\left[D_{1}\left(\alpha_{1}\right)D_{2}\left(\alpha_{2}\right)\rho\right]$,
$D_{i}\left(\alpha_{i}\right)$ is the displacement operator corresponding to
mode $i$, and $\rho$ is the density operator associated to the state.

In order to measure the success probability of a teleportation protocol, it is
convenient to use the fidelity of teleportation
$\mathcal{F=}$tr$\left(\rho_{in}\rho_{out}\right)$, an overlap between the
input state $\rho_{in}$ and the output (teleported) state $\rho_{out}$, which
can, in the CF form, be expressed as

$\mathcal{F=}\int\frac{d^{2}\eta}{\pi}\chi_{in}\left(\eta\right)\chi_{out}\left(-\eta\right).$
(46)

Substituting Eq.(45) into (46) yields

$\mathcal{F=}\int\frac{d^{2}\eta}{\pi}\left|\chi_{in}\left(\eta\right)\right|^{2}\chi_{E}\left(-\eta^{\ast},-\eta\right).$
(47)

In the following we use Eq.(47) to analyze the efficiency of teleportation for
$V\left|00\right\rangle$ as a quantum channel.

Let us first consider Braunstein and Kimble protocol [39] of QT for single-
mode coherent states $\left|\beta\right\rangle$, whose CF reads

$\chi_{\text{coh}}\left(\alpha\right)=\exp\left[-\frac{1}{2}\left|\alpha\right|^{2}+\alpha\beta^{\ast}-\alpha^{\ast}\beta\right].$
(48)

For the OTCSS, its CF is given by (see Appendix B)

$\chi\left(\alpha;\beta\right)=\exp\left[-\frac{1}{2}\left(\begin{array}[c]{cccc}\alpha^{\ast}&\alpha&\beta^{\ast}&\beta\end{array}\right)\frac{1}{4}M\left(\begin{array}[c]{cccc}\alpha^{\ast}&\alpha&\beta^{\ast}&\beta\end{array}\right)^{T}\right],$
(49)

where $M$ is defined in Eq.(42). Upon substituting Eqs.(48) and (49) into
(47), we worked out the fidelity for teleporting a coherent state based on the
OTCSS (19),

$\mathcal{F}=\frac{1}{1-f},$ (50)

where $f=\cosh\gamma\sinh 2\lambda-\cosh^{2}\lambda-\cosh
2\gamma\sinh^{2}\lambda.$ Eq.(50) indicates that the fidelity is only
dependent on the parameters $\lambda$ and $\gamma$, and is independent of
amplitude of the coherent state. In particular, when $\gamma=0$, Eq.(50) just
reduces to $\mathcal{F=}(1+\tanh\lambda)/2$ [40].

Next we consider to teleport the single-mode squeezed vacuum state,
$\exp\left[r/2\left(a^{2}-a^{{\dagger}2}\right)\right]\left|0\right\rangle,$
whose CF reads

$\chi_{sq}\left(\alpha\right)=\exp\left[-\frac{1}{2}\left|\alpha\right|^{2}\cosh
2r-\frac{1}{4}\left(\alpha^{2}+\alpha^{\ast 2}\right)\sinh 2r\right],$ (51)

substituting Eqs.(51),(49) into Eq.(47) yields the fidelity,

$\mathcal{F}\left(r\right)\mathcal{=}\frac{1}{\sqrt{\allowbreak f^{2}-2f\cosh
2r+1}}.$ (52)

In order to compare the fidelity obtained by the TSVS channel and the OTCSS
channel, we plot figure for the difference fidelity
($\mathcal{F}\left(r\right)-\mathcal{F}\left(0\right)$) as a function of
parameters ($\lambda$ and $\gamma$) in Fig.6. From Fig.6, one can see that
there is a region spanned by $\lambda$ and $\gamma$ in which the fidelity of
OTCSS channel is larger than the other one and the difference fidelity becomes
smaller with the increase of $r$.

Figure 6: (Color online) Plot of the fidelity $\mathcal{F}$ as a function of
parameters $\lambda$ and $\gamma$,(a) the initial coherent state, with
$r=0;$(b) the initial squeezed vacuum state with $r=1.$

##  7 Conclusion

In conclusion, we have introduced a one- and two-mode combination squeezed
state (OTCSS) which can be considered as a generalized two-mode squeezed state
and investigated the entanglement properties and quantum noncocality of this
state in terms of logarithmic negativity and the Bell’s inequality,
respectively. It is shown that this state presents larger entanglement than
that of the usual two-mode squeezed vacuum state (TSVS); In a certain smaller
regime of $\lambda$, it is found that the violation of Bell’s inequality
becomes more observable with increasing $\gamma$, which indicates that the
nonlocality of $V\left|00\right\rangle$ can be stronger than that of TSVS due
to the presence of $\gamma.$ In addition, application to quantum teleportation
with OTCSS is also considered, which shows that there is a region spanned by
$\lambda$ and $\gamma$ in which the fidelity of OTCSS channel is larger than
that of TSVS.

ACKNOWLEDGEMENT: Work supported by a grant from the Key Programs Foundation of
Ministry of Education of China (No. ) and the Research Foundation of the
Education Department of Jiangxi Province of China (No. GJJ10097).

Appendix A: Derivation of Eq.(29)

Using the order-invariance of Weyl ordered operators under similar
transformations (27) and Eqs.(9)-(12), we have

$\displaystyle U$
$\displaystyle=V^{-1}\genfrac{}{}{0.0pt}{}{:}{:}\delta\left(q_{1}-Q_{1}\right)\delta\left(p_{1}-P_{1}\right)\delta\left(q_{2}-Q_{2}\right)\delta\left(p_{2}-P_{2}\right)\genfrac{}{}{0.0pt}{}{:}{:}V$
$\displaystyle=\genfrac{}{}{0.0pt}{}{:}{:}\delta\left(q_{1}-Q_{1}\cosh\lambda-
Q_{2}e^{-\gamma}\sinh\lambda\right)\delta\left(q_{2}-Q_{2}\cosh\lambda-
Q_{1}e^{\gamma}\sinh\lambda\right)$
$\displaystyle\times\delta\left(p_{1}-P_{1}\cosh\lambda+P_{2}e^{\gamma}\sinh\lambda\right)\delta\left(p_{2}-P_{2}\cosh\lambda+P_{1}e^{-\gamma}\sinh\lambda\right)\genfrac{}{}{0.0pt}{}{:}{:}$
$\displaystyle=\genfrac{}{}{0.0pt}{}{:}{:}\delta\left(\left(\begin{array}[c]{c}q_{1}\\\
q_{2}\end{array}\right)-\left(\begin{array}[c]{cc}\cosh\lambda&e^{-\gamma}\sinh\lambda\\\
e^{\gamma}\sinh\lambda&\cosh\lambda\end{array}\right)\left(\begin{array}[c]{c}Q_{1}\\\
Q_{2}\end{array}\right)\right)$ (59)
$\displaystyle\times\delta\left(\left(\begin{array}[c]{c}p_{1}\\\
p_{2}\end{array}\right)-\left(\begin{array}[c]{cc}\cosh\lambda&-e^{\gamma}\sinh\lambda\\\
-e^{-\gamma}\sinh\lambda&\cosh\lambda\end{array}\right)\left(\begin{array}[c]{c}P_{1}\\\
P_{2}\end{array}\right)\right)\genfrac{}{}{0.0pt}{}{:}{:}$ (66)
$\displaystyle=\genfrac{}{}{0.0pt}{}{:}{:}\delta\left(\left(\begin{array}[c]{cc}\cosh\lambda&-e^{-\gamma}\sinh\lambda\\\
-e^{\gamma}\sinh\lambda&\cosh\lambda\end{array}\right)\left(\begin{array}[c]{c}q_{1}\\\
q_{2}\end{array}\right)-\left(\begin{array}[c]{c}Q_{1}\\\
Q_{2}\end{array}\right)\right)$ (73)
$\displaystyle\times\delta\left(\left(\begin{array}[c]{cc}\cosh\lambda&e^{\gamma}\sinh\lambda\\\
e^{-\gamma}\sinh\lambda&\cosh\lambda\end{array}\right)\left(\begin{array}[c]{c}p_{1}\\\
p_{2}\end{array}\right)-\left(\begin{array}[c]{c}P_{1}\\\
P_{2}\end{array}\right)\right)\genfrac{}{}{0.0pt}{}{:}{:},$ (A1)

which indicates that (comparing with Eq.(24))

$\displaystyle U$
$\displaystyle=\genfrac{}{}{0.0pt}{}{:}{:}\delta\left(q_{1}\cosh\lambda-
q_{2}e^{-\gamma}\sinh\lambda-
Q_{1}\right)\delta\left(p_{1}\cosh\lambda+p_{2}e^{\gamma}\sinh\lambda-
P_{1}\right)$ $\displaystyle\times\delta\left(q_{2}\cosh\lambda-
q_{1}e^{\gamma}\sinh\lambda-
Q_{2}\right)\delta\left(p_{2}\cosh\lambda+p_{1}e^{-\gamma}\sinh\lambda-
P_{2}\right)\genfrac{}{}{0.0pt}{}{:}{:}$ $\displaystyle=\text{Eq.(\ref{25})}.$
(A2)

Thus the Wigner function of $V\left|00\right\rangle$ is

$\displaystyle W\left(q_{1},p_{1};q_{2},p_{2}\right)$
$\displaystyle=\frac{1}{\pi^{2}}\exp\left\\{-\left(q_{1}\cosh\lambda-
q_{2}e^{-\gamma}\sinh\lambda\right)^{2}-\left(q_{2}\cosh\lambda-
q_{1}e^{\gamma}\sinh\lambda\right)^{2}\right.$
$\displaystyle\left.-\left(p_{1}\cosh\lambda+p_{2}e^{\gamma}\sinh\lambda\right)^{2}-\left(p_{2}\cosh\lambda+p_{1}e^{-\gamma}\sinh\lambda\right)^{2}\right\\}$
$\displaystyle=(\ref{25}).$ (A3)

Appendix B: Derivation of characteristic function of $V\left|00\right\rangle$

For two-mode quantum state $V\left|00\right\rangle$, its characteristic
function is given by

$\displaystyle\chi\left(q_{1},p_{1};q_{2},p_{2}\right)$
$\displaystyle=\mathtt{tr}\left[V\left|00\right\rangle\left\langle
00\right|V^{-1}D_{1}\left(q_{1},p_{1}\right)D_{2}\left(q_{2},p_{2}\right)\right]$
$\displaystyle=\left\langle
00\right|V^{-1}D_{1}\left(q_{1},p_{1}\right)D_{2}\left(q_{2},p_{2}\right)V\left|00\right\rangle,$
(B1)

where $D_{i}\left(q_{i},p_{i}\right)$ $\left(i=1,2\right)$ are the
displacement operators, defined by
$D_{i}\left(q_{i},p_{i}\right)=\exp\left[\mathtt{i}\left(p_{i}Q_{i}-q_{i}P_{i}\right)\right].$

Noticing that the Weyl ordering of $D_{i}\left(q_{i},p_{i}\right)$ is itself,
$D_{i}\left(q_{i},p_{i}\right)=\genfrac{}{}{0.0pt}{}{:}{:}D_{i}\left(q_{i},p_{i}\right)\genfrac{}{}{0.0pt}{}{:}{:}$,
and that a remarkable property of the invariance of Weyl ordered operators
under similar transformations (27), we have

$\displaystyle
V^{-1}D_{1}\left(q_{1},p_{1}\right)D_{2}\left(q_{2},p_{2}\right)V$
$\displaystyle=V^{-1}\genfrac{}{}{0.0pt}{}{:}{:}\exp\left[i\left(p_{1}Q_{1}-q_{1}P_{1}\right)\right]\exp\left[i\left(p_{2}Q_{2}-q_{2}P_{2}\right)\right]\genfrac{}{}{0.0pt}{}{:}{:}V$
$\displaystyle=\genfrac{}{}{0.0pt}{}{:}{:}\exp\left[i\left(p_{1}\left(Q_{1}\cosh\lambda+Q_{2}e^{-\gamma}\sinh\lambda\right)-q_{1}\left(P_{1}\cosh\lambda-
P_{2}e^{\gamma}\sinh\lambda\right)\right)\right]$
$\displaystyle\times\exp\left[i\left(p_{2}\left(Q_{2}\cosh\lambda+Q_{1}e^{\gamma}\sinh\lambda\right)-q_{2}\left(P_{2}\cosh\lambda-
P_{1}e^{-\gamma}\sinh\lambda\right)\right)\right]\genfrac{}{}{0.0pt}{}{:}{:}$
$\displaystyle=\genfrac{}{}{0.0pt}{}{:}{:}\exp\left[i\left(p_{1}^{\prime}Q_{1}-q_{1}^{\prime}P_{1}\right)\right]\exp\left[\allowbreak
i\left(p_{2}^{\prime}Q_{2}-q_{2}^{\prime}P_{2}\right)\right]\genfrac{}{}{0.0pt}{}{:}{:}$
$\displaystyle=D_{1}\left(q_{1}^{\prime},p_{1}^{\prime}\right)D_{2}\left(q_{2}^{\prime},p_{2}^{\prime}\right),$
(B2)

where

$\displaystyle q_{1}^{\prime}$ $\displaystyle=q_{1}\cosh\lambda-
q_{2}e^{-\gamma}\sinh\lambda,\text{
}p_{1}^{\prime}=p_{1}\cosh\lambda+p_{2}\allowbreak e^{\gamma}\sinh\lambda,$
$\displaystyle q_{2}^{\prime}$ $\displaystyle=q_{2}\cosh\lambda-
q_{1}e^{\gamma}\sinh\lambda,\text{
}p_{2}^{\prime}=p_{2}\cosh\lambda+p_{1}e^{-\gamma}\sinh\lambda.$ (B3)

Then substituting Eqs.(B2), (B3) into Eq.(B1) we can directly obtain the CF of
$V\left|00\right\rangle,$

$\displaystyle\chi\left(q_{1},p_{1};q_{2},p_{2}\right)$
$\displaystyle=\left\langle
00\right|D_{1}\left(q_{1}^{\prime},p_{1}^{\prime}\right)D_{2}\left(q_{2}^{\prime},p_{2}^{\prime}\right)\left|00\right\rangle$
$\displaystyle=\exp\left[-\frac{1}{2}\left(\begin{array}[c]{cccc}q_{1}&p_{1}&q_{2}&p_{2}\end{array}\right)\sigma\left(\begin{array}[c]{cccc}q_{1}&p_{1}&q_{2}&p_{2}\end{array}\right)^{T}\right],$
(B4)

or

$\chi\left(\alpha;\beta\right)=\exp\left[-\frac{1}{2}\left(\begin{array}[c]{cccc}\alpha^{\ast}&\alpha&\beta^{\ast}&\beta\end{array}\right)\bar{\sigma}\left(\begin{array}[c]{cccc}\alpha^{\ast}&\alpha&\beta^{\ast}&\beta\end{array}\right)^{T}\right],$
(B5)

where

$\sigma=\frac{1}{2}\left(\begin{array}[c]{cccc}m_{1}&0&-m_{3}&0\\\
0&m_{2}&0&m_{3}\\\ -m_{3}&0&m_{2}&0\\\
0&m_{3}&0&m_{1}\end{array}\right),\bar{\sigma}=N\sigma N^{T}=\frac{1}{4}M.$
(B6)

When $\gamma=0,$ $\left(m_{1}+m_{2}\right)\rightarrow 2\cosh
2\lambda,m_{3}\rightarrow\sinh 2\lambda,$we have

$\chi\left(\alpha;\beta\right)=\exp\left[-\frac{1}{2}\allowbreak\left(\left|\alpha\right|^{2}+\left|\beta\right|^{2}\right)\cosh
2\lambda+\frac{1}{2}\left(\alpha^{\ast}\beta^{\ast}+\alpha\beta\right)\sinh
2\lambda\allowbreak\right],$ (B7)

which is just the CF of the usual TSVS.

## References

  * [1] D. Bouwmeester et al., _The Physics of Quantum Information_ , (Springer, Berlin) 2000.
  * [2] M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information (Cambridge University Press) 2000.
  * [3] V. Buzek, J. Mod. Opt. 37 (1990) 303.
  * [4] R. Loudon, P. L. Knight, J. Mod. Opt. 34 (1987) 709.
  * [5] V. V. Dodonov, J. Opt. B: Quantum Semiclass. Opt. 4 (2002) R1.
  * [6] Hong-yi Fan and J. R. Klauder, Phys. Rev. A 49 (1994) 704.
  * [7] Hong-yi Fan and Y. Fan, Phys. Rev. A 54 (1996) 958.
  * [8] Li-yun Hu and Hong-yi Fan, Europhys. Lett. 85 (2009) 60001.
  * [9] A. Einstein, B. Poldolsky and N. Rosen, Phys. Rev. 47 (1935) 777.
  * [10] Li-yun Hu and Hong-yi Fan, Phys. Rev. A 80 (2009) 022115; Opt. Commun. 282 (2009) 3734.
  * [11] Hong-yi Fan and Li-yun Hu, Opt. Commun. 281 (2008) 1629; 281 (2008) 5571.
  * [12] Hong-yi Fan, J Opt B: Quantum Semiclass. Opt. 5 (2003) R147
  * [13] Hong-yi Fan, Phys. Rev. A 41 (1990) 1526.
  * [14] E. P. Wigner, Phys. Rev. 40 (1932) 749.
  * [15] R. F. O’Connell and E. P. Wigner, Phys. Lett. A 83 (1981) 145.
  * [16] W. P. Schleich, _Quantum Optics in Phase Space,_ Wiley-VCH, Berlin, 2001.
  * [17] Hong-yi Fan, J. Phys. A 25 (1992) 3443; Hong-yi Fan, Y. Fan, Int. J. Mod. Phys. A 17 (2002) 701.
  * [18] Hong-yi Fan, Mod. Phys. Lett. A 15 (2000) 2297.
  * [19] Hong-yi Fan, Ann. Phys. (New York) 323 (2008) 500; 323 (2008) 1502.
  * [20] G. Vidal and R. F. Werner, Phys. Rev. A 65 (2002) 032314.
  * [21] J. Eisert and M. B. Plenio, J. Mod. Opt. 46 (1999) 145.
  * [22] S. Virmani and M. B. Plenio, Phys. Lett. A 268 (2000) 31.
  * [23] L. M. Duan, G. Giedke, J. O. Cirac, and P. Zoller, Phys. Rev. Lett. 84 (2000) 2722.
  * [24] R. Simon, Phys. Rev. Lett. 84 (2000) 2726.
  * [25] J. Williamson, Am. J. Math. 58 (1936) 141; V. I. Arnold, Mathematical Methods of Classical Mechanics (Springer-Verlag, New York, 1978).
  * [26] A. Serafini, F. Illuminati, M. G. A. Paris, and S. De Siena, Phys. Rev. A 69 (2004) 022318.
  * [27] G. Adesso, A. Serafini, and F. Illuminati, Phys. Rev. A. 70 (2004) 022318.
  * [28] K. Banasek and K. Wodkiewicz, Phys. Rev. A. 58 (1998) 4345.
  * [29] K. Banasek and K. Wodkiewicz, Phys. Rev. Lett. 76 (1996) 4344; S. Wallentowitz and W. Volgel, Phys. Rev. A. 53 (1996) 4528.
  * [30] J. F. Clauser, M. A. Horne, A. Shimony, and R. A. Holt, Phys. Rev. Lett. 23 (1969) 880.
  * [31] S-W Lee, H. Jeong, and D. Jaksch, Phys. Rev. A. 80 (2009) 022104.
  * [32] J. F. Clauser, and M. A. Horne, Phys. Rev. D. 10 (1974) 526.
  * [33] C. H. Bennett, G. Brassard, C. Crepeau, R. Jozsa, A. Peres, and W. K. Wootters, Phys. Rev. Lett. 70 (1993) 1895.
  * [34] D. Bouwmeester, J. W. Pan, K. Mattle, M. Eibl, H.Weinfurther, and A. Zeilinger, Nature (London) 390 (1997) 575.
  * [35] D. Boschi, S. Branca, F. De Martini, L. Hardy, and S. Popescu, Phys. Rev. Lett. 80 (1998) 1121.
  * [36] L. Vaidmain, Phys. Rev. A 49 (1994) 1473.
  * [37] S. L. Braunstein and P. van Loock, Rev. Mod. Phys. 77 (2005) 513.
  * [38] P. Marian and T. A. Marian, Phys. Rev. A. 74 (2006) 042306.
  * [39] S. L. Braunstein and H. J. Kimble, Phys. Rev. Lett. 80 (1998) 869.
  * [40] Y. Yang, and F-L. Li, Phys. Rev. A. 80 (2009) 022315.